squash trace: PR feedback

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

lib/Monads/trace/Trace_More_RG.thy

@@ -236,7 +236,7 @@ lemma rg_doesn't_grow_proof:
   apply (rule card_mono[OF y])
   apply clarsimp
   apply (rule ccontr)
-  apply (drule (2) use_validI[OF _ x, OF _ conjI refl])
+  apply (drule (2) use_validI[OF _ x, OF _ conjI])
   apply simp
   done
 
@@ -263,7 +263,7 @@ lemma rg_set_shrink_proof:
   apply (drule spec, erule mp)
   apply (clarsimp simp: subset_iff)
   apply (rule ccontr)
-  apply (drule(1) use_validI [OF _ x _ refl])
+  apply (drule(1) use_validI [OF _ x])
   apply simp
   done
 
@@ -279,18 +279,20 @@ lemma rg_shrinks_proof:
   apply (rule psubsetI)
    apply clarsimp
    apply (rule ccontr)
-   apply (drule (2) use_validI[OF _ x, OF _ conjI refl])
+   apply (drule (2) use_validI[OF _ x, OF _ conjI])
    apply simp
   by (metis use_validI w z)
 
-lemma use_validIE_R:
-  "\<lbrakk>(tr, Result (Inr r, s')) \<in> (rely f R s0 s); \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; P s0 s; s0' = last_st_tr tr s0\<rbrakk>
+lemma use_validIE_R':
+  "\<lbrakk>(tr, Result (Inr r, s')) \<in> rely f R s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; P s0 s; s0' = last_st_tr tr s0\<rbrakk>
    \<Longrightarrow> Q r s0' s'"
   unfolding validIE_def
-  by (frule(3) use_validI, simp)
+  by (frule(3) use_validI', simp)
+
+lemmas use_validIE_R = use_validIE_R'[OF _ _ _ refl]
 
 lemma use_validIE_guar:
-  "\<lbrakk>(tr, res) \<in> (rely f R s0 s); \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; P s0 s\<rbrakk>
+  "\<lbrakk>(tr, res) \<in> rely f R s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; P s0 s\<rbrakk>
    \<Longrightarrow> guar_cond G s0 tr"
   unfolding validIE_def
   by (frule(2) use_validI_guar, simp)
@@ -301,7 +303,7 @@ lemma validI_preservation_ex:
   apply (clarsimp simp: validI_def validI_prefix_closed[OF x] guar_by_rg[OF x])
   apply (erule subst[rotated, where P=P])
   apply (rule ext)
-  apply (erule use_validI [OF _ x _refl])
+  apply (erule use_validI [OF _ x])
   apply simp
   done
 
@@ -336,11 +338,6 @@ lemma opt_return_pres_lift_rg:
   shows      "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> case x of None \<Rightarrow> return () | Some v \<Rightarrow> f v \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. P\<rbrace>"
   by (wpsimp wp: x)
 
-\<comment> \<open>FIXME MC: this would be a pain to prove for validI, can it be deleted?
-lemma validI_return_unit:
-  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f >>= (\<lambda>_. return ()) \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r. Q\<rbrace>"
-  by (auto simp: validI_def in_bind in_return Ball_def)\<close>
-
 lemma rg_weak_lift_imp_conj:
   "\<lbrakk> \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> m -,\<lbrace>Q'\<rbrace>; \<lbrace>R\<rbrace>,\<lbrace>R\<rbrace> m -,\<lbrace>R'\<rbrace>; \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>\<top>\<top>\<top>\<rbrace> \<rbrakk>
    \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> Q s0 s) \<and> R s0 s \<and> S s0 s\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (P \<longrightarrow> Q' rv s0 s) \<and> R' rv s0 s\<rbrace>"
@@ -370,18 +367,18 @@ lemma P_bool_lift:
   apply (clarsimp simp: validI_def validI_prefix_closed[OF f])
   apply (rule back_subst[where P=P], assumption)
   apply (rule iffI)
-   apply (erule (1) use_validI [OF _ t _ refl])
+   apply (erule (1) use_validI [OF _ t])
   apply (rule classical)
-  apply (drule (1) use_validI [OF _ f _ refl])
+  apply (drule (1) use_validI [OF _ f])
   apply simp
   done
 
 lemma gets_sp: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> gets f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. P and (\<lambda>s0 s. f s = rv)\<rbrace>"
   by (wp, simp)
 
 lemma post_by_rg2:
-  "\<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; (tr, Result (rv, s')) \<in> rely f R s0 s; P s0 s; s0' = last_st_tr tr s0\<rbrakk>
-  \<Longrightarrow> Q rv s0' s'"
+  "\<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; (tr, Result (rv, s')) \<in> rely f R s0 s; P s0 s\<rbrakk>
+  \<Longrightarrow> Q rv (last_st_tr tr s0) s'"
   by (rule post_by_rg, assumption+)
 
 lemma rg_Ball_helper:
@@ -390,9 +387,9 @@ lemma rg_Ball_helper:
   shows "\<lbrace>\<lambda>s0 s. \<forall>x \<in> S s0 s. P x s0 s\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. \<forall>x \<in> S s0 s. Q x rv s0 s\<rbrace>"
   apply (clarsimp simp: validI_def validI_prefix_closed[OF x])
   apply (drule bspec, erule back_subst[where P="\<lambda>A. x\<in>A" for x])
-   apply (erule post_by_rg[OF y _ refl, rotated])
+   apply (erule post_by_rg[OF y, rotated])
    apply (rule refl)
-  apply (erule (1) post_by_rg[OF x _ refl])
+  apply (erule (1) post_by_rg[OF x])
   done
 
 lemma handy_prop_divs_rg:
@@ -402,13 +399,13 @@ lemma handy_prop_divs_rg:
              "\<lbrace>\<lambda>s0 s. P (Q s0 s \<or> R s0 s) \<and> S s0 s\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. P (Q' rv s0 s \<or> R' rv s0 s)\<rbrace>"
    apply (clarsimp simp: validI_def validI_prefix_closed[OF x(1)]
                   elim!: subst[rotated, where P=P])
-   apply (rule use_validI [OF _ x(1) _ refl], assumption)
-   apply (rule use_validI [OF _ x(2) _ refl], assumption)
+   apply (rule use_validI [OF _ x(1)], assumption)
+   apply (rule use_validI [OF _ x(2)], assumption)
    apply simp
   apply (clarsimp simp: validI_def validI_prefix_closed[OF x(1)]
                  elim!: subst[rotated, where P=P])
-  apply (rule use_validI [OF _ x(1) _ refl], assumption)
-  apply (rule use_validI [OF _ x(2) _ refl], assumption)
+  apply (rule use_validI [OF _ x(1)], assumption)
+  apply (rule use_validI [OF _ x(2)], assumption)
   apply simp
   done
 
@@ -501,14 +498,7 @@ lemma twp_split_const_ifE_R:
 lemma rg_disj_division:
   "\<lbrakk> P \<or> Q; P \<Longrightarrow> \<lbrace>R\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace> \<rbrakk>
    \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> R s0 s) \<and> (Q \<longrightarrow> T s0 s)\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>"
-  apply safe
-   apply (rule rg_weaken_pre)
-    apply simp
-   apply simp
-  apply (rule rg_weaken_pre)
-   apply simp
-  apply simp
-  done
+  by (fastforce intro: rg_weaken_pre)
 
 lemma rg_grab_asm:
   "\<lbrakk> P' \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<not> P' \<Longrightarrow> prefix_closed f \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P' \<and> P s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
@@ -524,7 +514,7 @@ lemma rg_grab_exs:
   assumes y: "prefix_closed f"
   shows      "\<lbrace>\<lambda>s0 s. \<exists>x. P x \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
   apply (clarsimp simp: validI_def y use_validI_guar[OF _ x])
-  apply (erule(2) use_validI [OF _ x _ refl])
+  apply (erule(2) use_validI [OF _ x])
   done
 
 lemma rg_prop_E:
@@ -586,19 +576,6 @@ lemma weak_if_twp':
    \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>"
   by (auto simp: validI_def)
 
-\<comment> \<open>FIXME MC: this one also isn't obvious, and the valid equivalent doesn't seem to be used anywhere.
-lemma bindE_split_recursive_asm:
-  assumes x: "\<And>x s'. \<lbrakk> (Inr x, s') \<in> mres (f s) \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. B x s0 s \<and> s = s'\<rbrace>,\<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>"
-  shows      "\<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>B\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s0 st. A s0 st \<and> st = s\<rbrace>,\<lbrace>R\<rbrace> f >>=E g \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>"
-  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 (clarsimp simp: in_throwError split: sum.splits)
-  apply (drule x)
-  apply (clarsimp simp: validE_def valid_def)
-  apply (drule(1) bspec, simp split: sum.splits)
-  done\<close>
-
 lemma validE_R_abstract_rv:
   "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<forall>rv'. Q rv' s0 s\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   by (erule rg_strengthen_postE; simp)
@@ -657,15 +634,6 @@ lemma validIE_case_prod:
   "\<lbrakk> \<And>x y. validIE (P x y) R (f x y) G Q E \<rbrakk> \<Longrightarrow> validIE (case_prod P v) R (case_prod (\<lambda>x y. f x y) v) G Q E"
   by (simp add: split_def)
 
-\<comment> \<open>FIXME MC: these also aren't obvious, and the valid equivalents don't seem to be used anywhere.
-lemma validI_pre_satisfies_post:
-  "\<lbrakk> \<And>s0 s r' s0' s'. P s0 s \<Longrightarrow> Q r' s0' s'; prefix_closed m \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace> Q \<rbrace>"
-  by (clarsimp simp: validI_def)
-
-lemma validIE_pre_satisfies_post:
-  "\<lbrakk> \<And>s0 s r' s0 s'. P s0 s \<Longrightarrow> Q r' s0 s'; \<And>s0 s r' s0 s'. P s0 s \<Longrightarrow> R r' s0 s' \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace> Q \<rbrace>,\<lbrace> R \<rbrace>"
-  by (clarsimp simp: validIE_def2 split: sum.splits)\<close>
-
 lemma rg_validIE_E_conjI:
   "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk>  \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv s0 s. E rv s0 s \<and> E' rv s0 s\<rbrace>"
   by (fastforce simp: validIE_def validI_def split: sum.splits)

lib/Monads/trace/Trace_RG.thy

@@ -147,30 +147,29 @@ abbreviation validIE_E ::
 
 text \<open>
   The following abbreviations are convenient to separate reasoning about postconditions and the
-  guard.\<close>
-\<comment> \<open>FIXME MC: name\<close>
-abbreviation validI' ::
+  guarantee condition.\<close>
+abbreviation validI_no_guarantee ::
   "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's rg_pred \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
   ("(\<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>)/ _ /(-,/ \<lbrace>_\<rbrace>)") where
   "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q\<rbrace> \<equiv> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>,\<lbrace>Q\<rbrace>"
 
-abbreviation (input) invariantI' ::
+abbreviation (input) invariantI_no_guarantee ::
   "('s,'a) tmonad \<Rightarrow> 's rg_pred \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
   ("_/ \<lbrace>_\<rbrace>,/ -,/ \<lbrace>_\<rbrace>" [59,0] 60) where
   "f \<lbrace>R\<rbrace>, -, \<lbrace>P\<rbrace> \<equiv> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>"
 
-abbreviation validIE' ::
+abbreviation validIE_no_guarantee ::
   "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's rg_pred \<Rightarrow> ('s, 'a + 'b) tmonad \<Rightarrow> ('b \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow>
    ('a \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
   ("(\<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>)/ _ /(-,/ \<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>)") where
   "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<equiv> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
 
-abbreviation validIE_R' ::
+abbreviation validIE_R_no_guarantee ::
   "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's rg_pred \<Rightarrow> ('s, 'a + 'b) tmonad \<Rightarrow> ('b \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
   ("(\<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>)/ _ /(-,/ \<lbrace>_\<rbrace>,/ -)") where
   "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>Q\<rbrace>,- \<equiv> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>\<lambda>_ _ _. True\<rbrace>"
 
-abbreviation validIE_E' ::
+abbreviation validIE_E_no_guarantee ::
   "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's rg_pred \<Rightarrow> ('s, 'a + 'b) tmonad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
   ("(\<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>)/ _ /(-,/ -,/ \<lbrace>_\<rbrace>)") where
   "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f -,-,\<lbrace>E\<rbrace> \<equiv> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>,\<lbrace>\<lambda>_ _ _. True\<rbrace>,\<lbrace>E\<rbrace>"
@@ -413,31 +412,31 @@ lemma rg_post_disjI2:
   "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. Q' rv\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0. Q rv s0 or Q' rv s0\<rbrace>"
   unfolding validI_def by auto
 
-\<comment> \<open>FIXME MC: do we want the last assumption?  It might make unification easier in unusual cases but so
-           far is always just resolved with refl. \<close>
-lemma use_validI:
-  "\<lbrakk>(tr, Result (rv, s')) \<in> (rely f R s0 s); \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; P s0 s; s0' = last_st_tr tr s0\<rbrakk>
+lemma use_validI':
+  "\<lbrakk>(tr, Result (rv, s')) \<in> rely f R s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; P s0 s; s0' = last_st_tr tr s0\<rbrakk>
    \<Longrightarrow> Q rv s0' s'"
   unfolding validI_def by auto
 
+lemmas use_validI = use_validI'[OF _ _ _ refl]
+
 lemmas post_by_rg = use_validI[rotated]
 
 lemma use_validI_guar:
-  "\<lbrakk>(tr, res) \<in> (rely f R s0 s); \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; P s0 s\<rbrakk>
+  "\<lbrakk>(tr, res) \<in> rely f R s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; P s0 s\<rbrakk>
    \<Longrightarrow> guar_cond G s0 tr"
   unfolding validI_def by auto
 
 lemmas guar_by_rg = use_validI_guar[rotated]
 
 lemma in_inv_by_rgD:
-  "\<lbrakk>\<And>P. f \<lbrace>R\<rbrace>,-,\<lbrace>P\<rbrace>; (tr, Result (rv, s')) \<in> (rely f R s0 s)\<rbrakk> \<Longrightarrow> s' = s"
+  "\<lbrakk>\<And>P. f \<lbrace>R\<rbrace>,-,\<lbrace>P\<rbrace>; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> s' = s"
   unfolding validI_def
   apply (drule meta_spec[where x="\<lambda>_. (=) s"])
   apply blast
   done
 
 lemma last_st_in_inv_by_rgD:
-  "\<lbrakk>\<And>P. f \<lbrace>R\<rbrace>,-,\<lbrace>P\<rbrace>; (tr, Result (rv, s')) \<in> (rely f R s0 s)\<rbrakk> \<Longrightarrow> last_st_tr tr s0 = s0"
+  "\<lbrakk>\<And>P. f \<lbrace>R\<rbrace>,-,\<lbrace>P\<rbrace>; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> last_st_tr tr s0 = s0"
   unfolding validI_def
   apply (drule meta_spec[where x="\<lambda>s0' _. s0' = s0"])
   apply blast
@@ -1091,10 +1090,10 @@ lemma rg_liftP_ext:
   apply (rule conjI, clarsimp simp: rely_def, erule (2) validI_GD[OF assms])
   apply clarsimp
   apply (erule subst2[rotated 2, where P=P])
-   apply (drule use_validI, rule assms, rule refl, rule refl)
+   apply (drule use_validI, rule assms, rule refl)
    apply simp
   apply (rule ext)
-  apply (drule use_validI, rule assms, rule refl, rule refl)
+  apply (drule use_validI, rule assms, rule refl)
   apply simp
   done