adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib/monads: remove more uses of _tac methods 

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This commit is contained in:
Corey Lewis 2023-10-13 10:08:01 +11:00 committed by Achim D. Brucker
parent ec1f38c8bc
commit af3505401b
11 changed files with 71 additions and 89 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
lib/Monads/reader_option/Reader_Option_VCG.thy
View File

@ -116,8 +116,8 @@ lemma owhile_ovalid[wp]:
\<Longrightarrow> ovalid (I a) (owhile_inv C B a I M) Q"
unfolding owhile_inv_def owhile_def ovalid_def
apply clarify
apply (frule_tac I = "\<lambda>a. I a s" in option_while_rule)
apply auto
apply (frule (1) option_while_rule[where I = "\<lambda>a. I a s" for s])
apply auto
done
definition ovalid_property where "ovalid_property P x = (\<lambda>s f. (\<forall>r. Some r = x s f \<longrightarrow> P r s))"
@ -187,7 +187,7 @@ lemma owhile_NF[wp]:
\<Longrightarrow> ovalidNF (I a) (owhile_inv C B a I M) Q"
unfolding owhile_inv_def ovalidNF_def ovalid_def
apply clarify
apply (rule_tac I = I and M = "measure (\<lambda>r. M r s)" in owhile_rule)
apply (rule owhile_rule[where I = I and M = "measure (\<lambda>r. M r s)" and s = s for s])
apply fastforce
apply fastforce
apply fastforce

6
lib/Monads/trace/Trace_Det.thy
View File

@ -55,10 +55,8 @@ 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 clarsimp
apply (erule_tac x=s in allE)
apply clarsimp
done
apply (erule all_reg[rotated])
by clarsimp
lemma det_modify[iff]:
"det (modify f)"

8
lib/Monads/trace/Trace_Empty_Fail.thy
View File

@ -58,8 +58,7 @@ lemma empty_failD3:
lemma empty_fail_bindD1:
"empty_fail (a >>= b) \<Longrightarrow> empty_fail a"
unfolding empty_fail_def bind_def
apply clarsimp
apply (drule_tac x=s in spec)
apply (erule all_reg[rotated])
by (force simp: split_def mres_def vimage_def split: tmres.splits)
@ -112,10 +111,7 @@ lemma empty_fail_select[empty_fail_cond]:
lemma mres_bind_empty:
"mres ((f >>= g) s) = {}
\<Longrightarrow> mres (f s) = {} \<or> (\<forall>res\<in>mres (f s). mres (g (fst res) (snd res)) = {})"
apply clarsimp
apply (clarsimp simp: mres_def split_def vimage_def bind_def)
apply (rename_tac rv s' trace)
apply (drule_tac x=rv in spec, drule_tac x=s' in spec)
apply (clarsimp simp: bind_def mres_def split_def)
apply (clarsimp simp: image_def)
apply fastforce
done

4
lib/Monads/trace/Trace_Lemmas.thy
View File

@ -204,8 +204,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

1
lib/Monads/trace/Trace_Monad.thy
View File

@ -806,6 +806,7 @@ lemma parallel_def2:
apply (rule exI, rule conjI, assumption)+
apply (simp add: list_all2_conv_all_nth list_eq_iff_nth_eq split_def prod_eq_iff)
apply clarsimp
apply (rename_tac ys zs)
apply (rule_tac x="map (((\<noteq>) Env) o fst) ys" in exI)
apply (simp add: zip_map1 o_def split_def)
apply (strengthen subst[where P="\<lambda>xs. (xs, v) \<in> S" for v S, mk_strg I _ E])

27
lib/Monads/trace/Trace_Monad_Equations.thy
View File

@ -117,35 +117,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:
@ -531,7 +518,7 @@ lemma put_trace_mapM_x:
lemma rev_surj:
"surj rev"
by (rule_tac f=rev in surjI, simp)
by (rule surjI[where f=rev], simp)
lemma select_image:
"select (f ` S) = do x \<leftarrow> select S; return (f x) od"

80
lib/Monads/trace/Trace_More_VCG.thy
View File

@ -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)
@ -393,13 +391,12 @@ 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]
@ -416,11 +413,10 @@ lemma hoare_Ball_helper:
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:
@ -479,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> mres (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>mres (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
@ -522,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_all 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_all 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>
@ -589,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> mres (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:
@ -630,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:
@ -687,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>
@ -718,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 (fastforce 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 (fastforce 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>"

23
lib/Monads/trace/Trace_RG.thy
View File

@ -272,8 +272,8 @@ proof (induct n arbitrary: res)
case 0 then show ?case by auto
next
case (Suc n)
have drop_1: "\<And>tr res. (tr, res) \<in> f s \<Longrightarrow> \<exists>res'. (drop 1 tr, res') \<in> f s"
by (case_tac tr; fastforce dest: prefix_closedD[rotated] intro: Suc)
have drop_1: "(tr, res) \<in> f s \<Longrightarrow> \<exists>res'. (drop 1 tr, res') \<in> f s" for tr res
by (cases tr; fastforce dest: prefix_closedD[rotated] intro: Suc)
show ?case
using Suc.hyps[OF Suc.prems]
by (metis drop_1[simplified] drop_drop add_0 add_Suc)
@ -291,7 +291,8 @@ lemma parallel_prefix_closed[wp_split]:
"\<lbrakk>prefix_closed f; prefix_closed g\<rbrakk>
\<Longrightarrow> prefix_closed (parallel f g)"
apply (subst prefix_closed_def, clarsimp simp: parallel_def)
apply (case_tac f_steps; clarsimp)
apply (subst (asm) zip.zip_Cons)
apply (clarsimp split: list.splits)
apply (drule(1) prefix_closedD)+
apply fastforce
done
@ -338,7 +339,7 @@ lemma guar_cond_drop_Suc:
"\<lbrakk>guar_cond R s0 (drop (Suc n) xs);
fst (xs ! n) \<noteq> Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))\<rbrakk>
\<Longrightarrow> guar_cond R s0 (drop n xs)"
by (case_tac "n < length xs"; simp add: guar_cond_drop_Suc_eq)
by (cases "n < length xs"; simp add: guar_cond_drop_Suc_eq)
lemma rely_cond_Cons_eq:
"rely_cond R s0 (x # xs)
@ -427,8 +428,9 @@ proof -
hd_drop_conv_nth hd_append)
apply (fastforce simp: split_def intro!: nth_equalityI)
apply clarsimp
apply (erule_tac x=n in meta_allE)+
apply (drule meta_mp, erule rely_cond_is_drop, simp)
apply clarsimp
apply (erule meta_allE, drule meta_mp, assumption)+
apply (subst(asm) rely_cond_drop_Suc_eq[where xs="map f xs" for f xs], simp)
apply (clarsimp simp: last_st_tr_drop_map_zip_hd if_split[where P="\<lambda>x. x = Env"]
split_def)
@ -493,7 +495,7 @@ lemma put_trace_res:
\<Longrightarrow> \<exists>n. tr = drop n xs \<and> n \<le> length xs
\<and> res = (case n of 0 \<Rightarrow> Result ((), s) | _ \<Rightarrow> Incomplete)"
apply (clarsimp simp: put_trace_eq_drop)
apply (case_tac n; auto intro: exI[where x=0])
apply (auto simp: gr0_conv_Suc intro: exI[where x=0])
done
lemma put_trace_twp[wp]:
@ -732,13 +734,16 @@ lemmas modify_prefix_closed[simp] =
modify_wp[THEN valid_validI_wp[OF no_trace_all(3)], THEN validI_prefix_closed]
lemmas await_prefix_closed[simp] = Await_sync_twp[THEN validI_prefix_closed]
lemma repeat_n_prefix_closed[intro!]:
"prefix_closed f \<Longrightarrow> prefix_closed (repeat_n n f)"
apply (induct n; simp)
apply (auto intro: prefix_closed_bind)
done
lemma repeat_prefix_closed[intro!]:
"prefix_closed f \<Longrightarrow> prefix_closed (repeat f)"
apply (simp add: repeat_def)
apply (rule prefix_closed_bind; clarsimp)
apply (rename_tac n)
apply (induct_tac n; simp)
apply (auto intro: prefix_closed_bind)
done
lemma rely_cond_True[simp]:

2
lib/Monads/trace/Trace_VCG.thy
View File

@ -1016,7 +1016,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>"

2
lib/Monads/wp/WPFix.thy
View File

@ -242,11 +242,13 @@ lemma demo2:
\<and> (\<forall>x. I x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y)))
\<and> (\<forall>x. I x \<longrightarrow> (case x of None \<Rightarrow> R (Inr 9) | Some y \<Rightarrow> R (Inl (y - 1))))"
apply (intro exI conjI[rotated] allI)
apply (rename_tac x)
apply (case_tac x; simp)
apply wpfix
apply (rule P)
apply wpfix
apply (rule P)
apply (rename_tac x)
apply (case_tac x; simp)
apply wpfix
apply (rule P)

1
lib/Monads/wp/WPI.thy
View File

@ -116,6 +116,7 @@ private lemma
(atomic f (\<lambda>s. A' s \<and> Pres' s) (\<lambda>r s. A r s \<and> Pres r s) B Q' \<Longrightarrow> trip Ts) \<Longrightarrow> trip Ts"
apply (erule meta_mp)
apply (clarsimp simp: valid_def atomic_def)
apply (rename_tac P s r s')
apply (drule_tac x=P in spec)
apply (drule_tac x=P in meta_spec)
apply (drule_tac x=s in spec)+