lib/wp: Adjust some problematic attributes.

In particular, some intro! attributes for some wp rules are removed.
These previously caused auto/fastforce to play a really strange role
in some proofs.

lib/Monad_WP/NonDetMonadVCG.thy

@@ -281,11 +281,11 @@ lemma hoare_True_E_R [simp]:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. True\<rbrace>, -"
   by (auto simp add: validE_R_def validE_def valid_def split: sum.splits)
 
-lemma hoare_post_conj [intro!]:
+lemma hoare_post_conj [intro]:
   "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q And R \<rbrace>"
   by (fastforce simp: valid_def split_def bipred_conj_def)
 
-lemma hoare_pre_disj [intro!]:
+lemma hoare_pre_disj [intro]:
   "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>; \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P or Q \<rbrace> a \<lbrace> R \<rbrace>"
   by (simp add:valid_def pred_disj_def)
 
@@ -336,14 +336,14 @@ lemma hoare_gets_sp:
 lemma hoare_return_drop_var [iff]: "\<lbrace> Q \<rbrace> return x \<lbrace> \<lambda>r. Q \<rbrace>"
   by (simp add:valid_def return_def)
 
-lemma hoare_gets [intro!]: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) s \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> gets f \<lbrace> Q \<rbrace>"
+lemma hoare_gets [intro]: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) s \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> gets f \<lbrace> Q \<rbrace>"
   by (simp add:valid_def gets_def get_def bind_def return_def)
 
-lemma hoare_modifyE_var [intro!]:
+lemma hoare_modifyE_var:
   "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> modify f \<lbrace> \<lambda>r s. Q s \<rbrace>"
   by(simp add: valid_def modify_def put_def get_def bind_def)
 
-lemma hoare_if [intro!]:
+lemma hoare_if:
   "\<lbrakk> P \<Longrightarrow> \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace>; \<not> P \<Longrightarrow> \<lbrace> Q \<rbrace> b \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow>
    \<lbrace> Q \<rbrace> if P then a else b \<lbrace> R \<rbrace>"
   by (simp add:valid_def)
@@ -1848,7 +1848,7 @@ lemma validNF_prop [wp_unsafe]:
 
 lemma validNF_post_conj [intro!]:
   "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>!; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q And R \<rbrace>!"
-  by (clarsimp simp: validNF_def)
+  by (auto simp: validNF_def)
 
 lemma no_fail_or:
   "\<lbrakk>no_fail P a; no_fail Q a\<rbrakk> \<Longrightarrow> no_fail (P or Q) a"
@@ -2093,8 +2093,8 @@ lemma validNF_nobindE [wp]:
   by clarsimp wp
 
 text {*
-Setup triple rules for validE_NF so that we can use the
-"wp_comb" attribute.
+Setup triple rules for @{term validE_NF} so that we can use
+wp combinator rules.
 *}
 
 definition "validE_NF_property Q E s b \<equiv> \<not> snd (b s)

lib/Monad_WP/wp/WPFix.thy

@@ -23,7 +23,7 @@ after goals are solved. They should be instantiated to True.
   2. Schematics which appear in multiple precondition positions. They should
 be instantiated to a conjunction and then separated.
   3/4. Schematics applied to datatype expressions such as @{term True} or
-@{term "Some x"}. See the theory Datatype_Schematic for details.
+@{term "Some x"}. See @{theory Datatype_Schematic} for details.
 *}
 
 lemma use_strengthen_prop_intro:
@@ -259,4 +259,4 @@ lemma demo2:
   apply (simp add: P17)
   done
 
-end
+end

lib/clib/AutoCorresModifiesProofs.thy

@@ -210,7 +210,7 @@ lemma guardE_inv[valid_inv]:
 lemma whenE_inv[valid_inv]:
   "\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> whenE c f \<lbrace>\<lambda>_. I\<rbrace>"
   apply (unfold whenE_def)
-  apply (blast intro: returnOk_inv)
+  apply (auto intro: returnOk_inv)
   done
 
 lemma unless_inv[valid_inv]:
@@ -221,7 +221,7 @@ lemma unless_inv[valid_inv]:
 lemma unlessE_inv[valid_inv]:
   "\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> unlessE c f \<lbrace>\<lambda>_. I\<rbrace>"
   apply (unfold unlessE_def)
-  by (blast intro: returnOk_inv)
+  by (auto intro: returnOk_inv)
 
 lemma handleE'_inv[valid_inv]:
   "\<lbrakk> \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> handleE' f h \<lbrace>\<lambda>_. I\<rbrace>"

lib/clib/AutoCorres_C.thy

@@ -75,10 +75,10 @@ FIXME: Move this change into AutoCorres itself, or the underlying VCG library.
 
 lemmas [wp del] =
   NonDetMonadEx.validE_whenE
-  NonDetMonadLemmaBucket.hoare_whenE_wp
+  NonDetMonadVCG.hoare_whenE_wps
 
 lemmas hoare_whenE_wp2 [wp] =
-  NonDetMonadLemmaBucket.hoare_whenE_wp[simplified if_apply_def2]
+  NonDetMonadVCG.hoare_whenE_wps[simplified if_apply_def2]
 
 section \<open>Rules for proving @{term ccorres_underlying} goals\<close>
 

tools/autocorres/ExecConcrete.thy

@@ -295,7 +295,7 @@ lemma exec_abstract_return_wp_nf [wp]:
 lemma exec_abstract_fail_wp_nf [wp]:
     "\<lbrace> \<lambda>s. False \<rbrace> exec_abstract st fail \<lbrace> P \<rbrace>!"
   apply wp
-  apply clarsimp
+  apply clarsimp?
   done
 
 lemma exec_abstract_fail_wp [wp]:

tools/autocorres/L2Opt.thy

@@ -96,6 +96,7 @@ lemma monad_equiv_gets [L2flow]:
         (\<lambda>r s. P s \<and> r = v' s) (\<lambda>_ _. False)"
   apply rule
    apply (clarsimp simp: L2_defs simp_expr_def)+
+  apply wpsimp
   done
 
 lemma monad_equiv_throw [L2flow]:
@@ -165,6 +166,7 @@ lemma monad_equiv_modify [L2flow]:
   apply rule
    apply (clarsimp simp: L2_defs simp_expr_def liftE_def modify_def put_def get_def bind_def)
   apply (clarsimp simp: L2_defs simp_expr_def)
+  apply wp
   apply force
   done