lib/monads/nondet: remove uses of _tac methods

In particular, try to remove as many as possible _tac methods that refer
to system-generated variable names. Any remaining uses are explicitly
protected by a rename_tac.

Signed-off-by: Corey Lewis <[email protected]>

lib/Monads/nondet/Nondet_Det.thy

@@ -51,13 +51,9 @@ lemma det_UN:
 lemma bind_detI[simp, intro!]:
   "\<lbrakk> det f; \<forall>x. det (g x) \<rbrakk> \<Longrightarrow> det (f >>= g)"
   unfolding bind_def det_def
+  apply (erule all_reg[rotated])
   apply clarsimp
-  apply (erule_tac x=s in allE)
-  apply clarsimp
-  apply (erule_tac x="a" in allE)
-  apply (erule_tac x="b" in allE)
-  apply clarsimp
-  done
+  by (metis fst_conv snd_conv)
 
 lemma det_modify[iff]:
   "det (modify f)"

lib/Monads/nondet/Nondet_Lemmas.thy

@@ -192,8 +192,8 @@ lemma liftE_liftM:
 lemma liftME_liftM:
   "liftME f = liftM (case_sum Inl (Inr \<circ> f))"
   unfolding liftME_def liftM_def bindE_def returnOk_def lift_def
-  apply (rule ext, rename_tac x)
-  apply (rule_tac f="bind x" in arg_cong)
+  apply (rule ext)
+  apply (rule arg_cong[where f="bind m" for m])
   apply (fastforce simp: throwError_def split: sum.splits)
   done
 
@@ -341,10 +341,10 @@ lemma whileLoop_unroll':
 lemma whileLoopE_unroll:
   "whileLoopE C B r = condition (C r) (B r >>=E whileLoopE C B) (returnOk r)"
   unfolding whileLoopE_def
-  apply (rule ext, rename_tac x)
+  apply (rule ext)
   apply (subst whileLoop_unroll)
   apply (clarsimp simp: bindE_def returnOk_def lift_def split: condition_splits)
-  apply (rule_tac f="\<lambda>a. (B r >>= a) x" in arg_cong)
+  apply (rule arg_cong[where f="\<lambda>a. (B r >>= a) x" for x])
   apply (rule ext)+
   apply (clarsimp simp: lift_def split: sum.splits)
   apply (subst whileLoop_unroll)

lib/Monads/nondet/Nondet_Monad_Equations.thy

@@ -177,35 +177,22 @@ lemma gets_the_returns:
   by (simp_all add: returnOk_def throwError_def
                     gets_the_return)
 
-lemma all_rv_choice_fn_eq_pred:
-  "\<lbrakk> \<And>rv. P rv \<Longrightarrow> \<exists>fn. f rv = g fn \<rbrakk> \<Longrightarrow> \<exists>fn. \<forall>rv. P rv \<longrightarrow> f rv = g (fn rv)"
-  apply (rule_tac x="\<lambda>rv. SOME h. f rv = g h" in exI)
-  apply (clarsimp split: if_split)
-  by (meson someI_ex)
-
-lemma all_rv_choice_fn_eq:
-  "\<lbrakk> \<And>rv. \<exists>fn. f rv = g fn \<rbrakk>
-   \<Longrightarrow> \<exists>fn. f = (\<lambda>rv. g (fn rv))"
-  using all_rv_choice_fn_eq_pred[where f=f and g=g and P=\<top>]
-  by (simp add: fun_eq_iff)
-
 lemma gets_the_eq_bind:
-  "\<lbrakk> \<exists>fn. f = gets_the (fn o fn'); \<And>rv. \<exists>fn. g rv = gets_the (fn o fn') \<rbrakk>
+  "\<lbrakk> f = gets_the (fn_f o fn'); \<And>rv. g rv = gets_the (fn_g rv o fn') \<rbrakk>
    \<Longrightarrow> \<exists>fn. (f >>= g) = gets_the (fn o fn')"
-  apply (clarsimp dest!: all_rv_choice_fn_eq)
-  apply (rule_tac x="\<lambda>s. case (fn s) of None \<Rightarrow> None | Some v \<Rightarrow> fna v s" in exI)
+  apply clarsimp
+  apply (rule exI[where x="\<lambda>s. case (fn_f s) of None \<Rightarrow> None | Some v \<Rightarrow> fn_g v s"])
   apply (simp add: gets_the_def bind_assoc exec_gets
                    assert_opt_def fun_eq_iff
             split: option.split)
   done
 
 lemma gets_the_eq_bindE:
-  "\<lbrakk> \<exists>fn. f = gets_the (fn o fn'); \<And>rv. \<exists>fn. g rv = gets_the (fn o fn') \<rbrakk>
+  "\<lbrakk> f = gets_the (fn_f o fn'); \<And>rv. g rv = gets_the (fn_g rv o fn') \<rbrakk>
    \<Longrightarrow> \<exists>fn. (f >>=E g) = gets_the (fn o fn')"
-  apply (simp add: bindE_def)
-  apply (erule gets_the_eq_bind)
+  unfolding bindE_def
+  apply (erule gets_the_eq_bind[where fn_g="\<lambda>rv s. case rv of Inl e \<Rightarrow> Some (Inl e) | Inr v \<Rightarrow> fn_g v s"])
   apply (simp add: lift_def gets_the_returns split: sum.split)
-  apply fastforce
   done
 
 lemma gets_the_fail:
@@ -469,8 +456,8 @@ lemma monad_eq_split:
   shows "(g >>= f) s = (g >>= f') s"
 proof -
   have pre: "\<And>rv s'. \<lbrakk>(rv, s') \<in> fst (g s)\<rbrakk> \<Longrightarrow> f rv s' = f' rv s'"
-    using assms unfolding valid_def
-    by (erule_tac x=s in allE) auto
+    using assms unfolding valid_def apply -
+    by (erule allE[where x=s]) auto
   show ?thesis
     by (simp add: bind_def image_def case_prod_unfold pre)
 qed
@@ -541,16 +528,15 @@ lemma bind_inv_inv_comm:
      empty_fail f; empty_fail g \<rbrakk> \<Longrightarrow>
    do x \<leftarrow> f; y \<leftarrow> g; n x y od = do y \<leftarrow> g; x \<leftarrow> f; n x y od"
   apply (rule ext)
-  apply (rename_tac s)
-  apply (rule_tac s="(do (x, y) \<leftarrow> do x \<leftarrow> f; y \<leftarrow> (\<lambda>_. g s) ; (\<lambda>_. return (x, y) s) od;
-                         n x y od) s" in trans)
+  apply (rule trans[where s="(do (x, y) \<leftarrow> do x \<leftarrow> f; y \<leftarrow> (\<lambda>_. g s) ; (\<lambda>_. return (x, y) s) od;
+                                 n x y od) s" for s])
    apply (simp add: bind_assoc)
    apply (intro bind_apply_cong, simp_all)[1]
     apply (metis in_inv_by_hoareD)
    apply (simp add: return_def bind_def)
    apply (metis in_inv_by_hoareD)
-  apply (rule_tac s="(do (x, y) \<leftarrow> do y \<leftarrow> g; x \<leftarrow> (\<lambda>_. f s) ; (\<lambda>_. return (x, y) s) od;
-                      n x y od) s" in trans[rotated])
+  apply (rule trans[where s="(do (x, y) \<leftarrow> do y \<leftarrow> g; x \<leftarrow> (\<lambda>_. f s) ; (\<lambda>_. return (x, y) s) od;
+                                 n x y od) s" for s, rotated])
    apply (simp add: bind_assoc)
    apply (intro bind_apply_cong, simp_all)[1]
     apply (metis in_inv_by_hoareD)

lib/Monads/nondet/Nondet_More_VCG.thy

@@ -137,8 +137,8 @@ lemma hoare_split_bind_case_sum:
              "\<And>rv. \<lbrace>S rv\<rbrace> h rv \<lbrace>Q\<rbrace>"
   assumes y: "\<lbrace>P\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>"
   shows      "\<lbrace>P\<rbrace> f >>= case_sum g h \<lbrace>Q\<rbrace>"
-  apply (rule hoare_seq_ext [OF _ y[unfolded validE_def]])
-  apply (case_tac x, simp_all add: x)
+  apply (rule hoare_seq_ext[OF _ y[unfolded validE_def]])
+  apply (wpsimp wp: x split: sum.splits)
   done
 
 lemma hoare_split_bind_case_sumE:
@@ -147,8 +147,8 @@ lemma hoare_split_bind_case_sumE:
   assumes y: "\<lbrace>P\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>"
   shows      "\<lbrace>P\<rbrace> f >>= case_sum g h \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   apply (unfold validE_def)
-  apply (rule hoare_seq_ext [OF _ y[unfolded validE_def]])
-  apply (case_tac x, simp_all add: x [unfolded validE_def])
+  apply (rule hoare_seq_ext[OF _ y[unfolded validE_def]])
+  apply (wpsimp wp: x[unfolded validE_def] split: sum.splits)
   done
 
 lemma assertE_sp:
@@ -256,12 +256,11 @@ lemma doesn't_grow_proof:
   assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
   shows      "\<lbrace>\<lambda>s. card (S s) < n \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. card (S s) < n\<rbrace>"
   apply (clarsimp simp: valid_def)
-  apply (subgoal_tac "S b \<subseteq> S s")
-   apply (drule card_mono [OF y], simp)
+  apply (erule le_less_trans[rotated])
+  apply (rule card_mono[OF y])
   apply clarsimp
   apply (rule ccontr)
-  apply (subgoal_tac "x \<notin> S b", simp)
-  apply (erule use_valid [OF _ x])
+  apply (drule (2) use_valid[OF _ x, OF _ conjI])
   apply simp
   done
 
@@ -297,13 +296,12 @@ lemma shrinks_proof:
   assumes w: "\<And>s. P s \<Longrightarrow> x \<in> S s"
   shows      "\<lbrace>\<lambda>s. card (S s) \<le> n \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. card (S s) < n\<rbrace>"
   apply (clarsimp simp: valid_def)
-  apply (subgoal_tac "S b \<subset> S s")
-   apply (drule psubset_card_mono [OF y], simp)
+  apply (erule less_le_trans[rotated])
+  apply (rule psubset_card_mono[OF y])
   apply (rule psubsetI)
    apply clarsimp
    apply (rule ccontr)
-   apply (subgoal_tac "x \<notin> S b", simp)
-   apply (erule use_valid [OF _ x])
+   apply (drule (2) use_valid[OF _ x, OF _ conjI])
    apply simp
   by (metis use_valid w z)
 
@@ -397,34 +395,28 @@ lemma P_bool_lift:
   assumes f: "\<lbrace>\<lambda>s. \<not>Q s\<rbrace> f \<lbrace>\<lambda>r s. \<not>Q s\<rbrace>"
   shows "\<lbrace>\<lambda>s. P (Q s)\<rbrace> f \<lbrace>\<lambda>r s. P (Q s)\<rbrace>"
   apply (clarsimp simp: valid_def)
-  apply (subgoal_tac "Q b = Q s")
-   apply simp
+  apply (rule back_subst[where P=P], assumption)
   apply (rule iffI)
-   apply (rule classical)
-   apply (drule (1) use_valid [OF _ f])
-   apply simp
-  apply (erule (1) use_valid [OF _ t])
+   apply (erule (1) use_valid [OF _ t])
+  apply (rule classical)
+  apply (drule (1) use_valid [OF _ f])
+  apply simp
   done
 
 lemmas fail_inv = hoare_fail_any[where Q="\<lambda>_. P" and P=P for P]
 
 lemma gets_sp: "\<lbrace>P\<rbrace> gets f \<lbrace>\<lambda>rv. P and (\<lambda>s. f s = rv)\<rbrace>"
   by (wp, simp)
 
-lemma post_by_hoare2:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; (r, s') \<in> fst (f s); P s \<rbrakk> \<Longrightarrow> Q r s'"
-  by (rule post_by_hoare, assumption+)
-
 lemma hoare_Ball_helper:
   assumes x: "\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>"
   assumes y: "\<And>P. \<lbrace>\<lambda>s. P (S s)\<rbrace> f \<lbrace>\<lambda>rv s. P (S s)\<rbrace>"
   shows "\<lbrace>\<lambda>s. \<forall>x \<in> S s. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> S s. Q x rv s\<rbrace>"
   apply (clarsimp simp: valid_def)
-  apply (subgoal_tac "S b = S s")
-   apply (erule post_by_hoare2 [OF x])
-   apply (clarsimp simp: Ball_def)
-  apply (erule_tac P1="\<lambda>x. x = S s" in post_by_hoare2 [OF y])
-  apply (rule refl)
+  apply (drule bspec, erule back_subst[where P="\<lambda>A. x\<in>A" for x])
+   apply (erule post_by_hoare[OF y, rotated])
+   apply (rule refl)
+  apply (erule (1) post_by_hoare[OF x])
   done
 
 lemma handy_prop_divs:
@@ -483,14 +475,14 @@ lemma hoare_in_monad_post:
   assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x. P\<rbrace>"
   shows      "\<lbrace>\<top>\<rbrace> f \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (f s)\<rbrace>"
   apply (clarsimp simp: valid_def)
-  apply (subgoal_tac "s = b", simp)
-  apply (simp add: state_unchanged [OF x])
+  apply (rule back_subst[where P="\<lambda>s. x\<in>fst (f s)" for x], assumption)
+  apply (simp add: state_unchanged[OF x])
   done
 
 lemma list_case_throw_validE_R:
   "\<lbrakk> \<And>y ys. xs = y # ys \<Longrightarrow> \<lbrace>P\<rbrace> f y ys \<lbrace>Q\<rbrace>,- \<rbrakk> \<Longrightarrow>
    \<lbrace>P\<rbrace> case xs of [] \<Rightarrow> throwError e | x # xs \<Rightarrow> f x xs \<lbrace>Q\<rbrace>,-"
-  apply (case_tac xs, simp_all)
+  apply (cases xs, simp_all)
   apply wp
   done
 
@@ -526,13 +518,13 @@ lemma wp_split_const_if:
   assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
   assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>"
   shows "\<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> f \<lbrace>\<lambda>rv s. (G \<longrightarrow> Q rv s) \<and> (\<not> G \<longrightarrow> Q' rv s)\<rbrace>"
-  by (case_tac G, simp_all add: x y)
+  by (cases G; simp add: x y)
 
 lemma wp_split_const_if_R:
   assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
   assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
   shows "\<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> f \<lbrace>\<lambda>rv s. (G \<longrightarrow> Q rv s) \<and> (\<not> G \<longrightarrow> Q' rv s)\<rbrace>,-"
-  by (case_tac G, simp_all add: x y)
+  by (cases G; simp add: x y)
 
 lemma hoare_disj_division:
   "\<lbrakk> P \<or> Q; P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk>
@@ -593,11 +585,12 @@ lemma univ_wp:
 lemma univ_get_wp:
   assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>"
   shows "\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> fst (f s). s = s' \<longrightarrow> Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>"
-  apply (rule hoare_pre_imp [OF _ univ_wp])
+  apply (rule hoare_pre_imp[OF _ univ_wp])
   apply clarsimp
   apply (drule bspec, assumption, simp)
-  apply (subgoal_tac "s = b", simp)
-  apply (simp add: state_unchanged [OF x])
+  apply (drule mp)
+   apply (simp add: state_unchanged[OF x])
+  apply simp
   done
 
 lemma other_hoare_in_monad_post:
@@ -634,10 +627,10 @@ lemma bindE_split_recursive_asm:
   apply (clarsimp simp: validE_def valid_def bindE_def in_bind lift_def)
   apply (erule allE, erule(1) impE)
   apply (drule(1) bspec, simp)
-  apply (case_tac x, simp_all add: in_throwError)
+  apply (clarsimp simp: in_throwError split: sum.splits)
   apply (drule x)
   apply (clarsimp simp: validE_def valid_def)
-  apply (drule(1) bspec, simp)
+  apply (drule(1) bspec, simp split: sum.splits)
   done
 
 lemma validE_R_abstract_rv:
@@ -691,9 +684,8 @@ lemma valid_rv_split:
 lemma hoare_rv_split:
   "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (Q rv s)\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (\<not>rv) \<longrightarrow> (Q rv s)\<rbrace>\<rbrakk>
    \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
-  apply (clarsimp simp: valid_def)
-  apply (case_tac a, fastforce+)
-  done
+  apply (clarsimp simp: valid_def split_def)
+  by (metis (full_types) fst_eqD snd_conv)
 
 lemma combine_validE:
   "\<lbrakk> \<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; \<lbrace> P' \<rbrace> x \<lbrace> Q' \<rbrace>,\<lbrace> E' \<rbrace> \<rbrakk>
@@ -722,23 +714,19 @@ lemma validE_pre_satisfies_post:
 
 lemma hoare_validE_R_conjI:
   "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - ; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, - \<rbrakk>  \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, -"
-  apply (clarsimp simp: Ball_def validE_R_def validE_def valid_def)
-  by (case_tac a; fastforce)
+  by (clarsimp simp: Ball_def validE_R_def validE_def valid_def split: sum.splits)
 
 lemma hoare_validE_E_conjI:
   "\<lbrakk> \<lbrace>P\<rbrace> f -, \<lbrace>Q\<rbrace> ; \<lbrace>P\<rbrace> f -, \<lbrace>Q'\<rbrace> \<rbrakk>  \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
-  apply (clarsimp simp: Ball_def validE_E_def validE_def valid_def)
-  by (case_tac a; fastforce)
+  by (clarsimp simp: Ball_def validE_E_def validE_def valid_def split: sum.splits)
 
 lemma validE_R_post_conjD1:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
-  apply (clarsimp simp: validE_R_def validE_def valid_def)
-  by (case_tac a; fastforce)
+  by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
 
 lemma validE_R_post_conjD2:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,-"
-  apply (clarsimp simp: validE_R_def validE_def valid_def)
-  by (case_tac a; fastforce)
+  by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
 
 lemma throw_opt_wp[wp]:
   "\<lbrace>if v = None then E ex else Q (the v)\<rbrace> throw_opt ex v \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"

lib/Monads/nondet/Nondet_VCG.thy

@@ -982,7 +982,7 @@ lemmas liftME_E_E_wp[wp_split] = validE_validE_E [OF liftME_wp, simplified, OF v
 lemma assert_opt_wp:
   "\<lbrace>\<lambda>s. x \<noteq> None \<longrightarrow> Q (the x) s\<rbrace> assert_opt x \<lbrace>Q\<rbrace>"
   unfolding assert_opt_def
-  by (case_tac x; wpsimp wp: fail_wp return_wp)
+  by (cases x; wpsimp wp: fail_wp return_wp)
 
 lemma gets_the_wp:
   "\<lbrace>\<lambda>s. (f s \<noteq> None) \<longrightarrow> Q (the (f s)) s\<rbrace> gets_the f \<lbrace>Q\<rbrace>"