lib: move empty_fail lemmas up into NonDetMonadVCG
This enables a few more moves of remaining lemmas in NonDetMonadLemmaBucket into the theories they belong thematically. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
parent
f19364a38b
commit
d275068826
|
|
@ -13,10 +13,6 @@ theory Monad_Commute
|
|||
More_Monad (* for mapM_x *)
|
||||
begin
|
||||
|
||||
lemma empty_fail_not_snd:
|
||||
"\<lbrakk> \<not> snd (m s); empty_fail m \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> fst (m s)"
|
||||
by (fastforce simp: empty_fail_def)
|
||||
|
||||
|
||||
definition monad_commute where
|
||||
"monad_commute P a b \<equiv>
|
||||
|
|
|
|||
|
|
@ -523,4 +523,38 @@ lemma simple_bind_fail [simp]:
|
|||
"(gets X >>= (\<lambda>_. fail)) = fail"
|
||||
by (auto intro!: bind_fail_propagates)
|
||||
|
||||
lemma bind_inv_inv_comm:
|
||||
"\<lbrakk> \<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>;
|
||||
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 (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 (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 bind_apply_cong, simp_all)
|
||||
apply (clarsimp simp: bind_def split_def return_def)
|
||||
apply (auto | drule(1) empty_failD3)+
|
||||
done
|
||||
|
||||
lemma bind_known_operation_eq:
|
||||
"\<lbrakk> no_fail P f; \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<and> s = t\<rbrace>; P s; Q s; empty_fail f \<rbrakk>
|
||||
\<Longrightarrow> (f >>= g) s = g x t"
|
||||
apply (drule(1) no_failD)
|
||||
apply (subgoal_tac "fst (f s) = {(x, t)}")
|
||||
apply (clarsimp simp: bind_def)
|
||||
apply (fastforce simp: valid_def empty_fail_def)
|
||||
done
|
||||
|
||||
end
|
||||
|
|
@ -12,6 +12,11 @@ imports
|
|||
Strengthen
|
||||
begin
|
||||
|
||||
(* FIXME lib: split this theory into at least: Hoare logic things, Det, EmptyFail, NoFail *)
|
||||
(* FIXME lib: put definitions of det, empty_fail, no_fail, into Det, EmptyFail, NoFail *)
|
||||
(* FIXME lib: move Hoare logic stuff from NonDetMonadLemmas to here *)
|
||||
(* FIXME lib: move monad equalities from here to NonDetMonadLemmas *)
|
||||
|
||||
section "Satisfiability"
|
||||
|
||||
text \<open>
|
||||
|
|
@ -796,8 +801,7 @@ lemma empty_fail_return [simp, wp]:
|
|||
by (simp add: empty_fail_def return_def)
|
||||
|
||||
lemma empty_fail_bindE:
|
||||
"\<lbrakk> empty_fail f; \<And>rv. empty_fail (g rv) \<rbrakk>
|
||||
\<Longrightarrow> empty_fail (f >>=E g)"
|
||||
"\<lbrakk> empty_fail f; \<And>rv. empty_fail (g rv) \<rbrakk> \<Longrightarrow> empty_fail (f >>=E g)"
|
||||
apply (simp add: bindE_def)
|
||||
apply (erule empty_fail_bind)
|
||||
apply (simp add: lift_def throwError_def split: sum.split)
|
||||
|
|
@ -825,6 +829,10 @@ lemma empty_fail [simp]:
|
|||
"empty_fail fail"
|
||||
by (simp add: fail_def empty_fail_def)
|
||||
|
||||
lemma empty_fail_assert:
|
||||
"empty_fail (assert P)"
|
||||
unfolding assert_def by simp
|
||||
|
||||
lemma empty_fail_assert_opt [simp]:
|
||||
"empty_fail (assert_opt x)"
|
||||
by (simp add: assert_opt_def split: option.splits)
|
||||
|
|
@ -837,6 +845,44 @@ lemma empty_fail_gets_map[simp]:
|
|||
"empty_fail (gets_map f p)"
|
||||
unfolding gets_map_def by simp
|
||||
|
||||
lemma empty_fail_error_bits[simp]:
|
||||
"empty_fail (returnOk v)"
|
||||
"empty_fail (throwError v)"
|
||||
"empty_fail (liftE f) = empty_fail f"
|
||||
by (fastforce simp: returnOk_def throwError_def liftE_def empty_fail_def bind_def return_def)+
|
||||
|
||||
lemma empty_fail_whenEs:
|
||||
"empty_fail f \<Longrightarrow> empty_fail (whenE P f)"
|
||||
"empty_fail f \<Longrightarrow> empty_fail (unlessE P f)"
|
||||
by (auto simp add: whenE_def unlessE_def)
|
||||
|
||||
lemma empty_fail_assertE:
|
||||
"empty_fail (assertE P)"
|
||||
by (simp add: assertE_def split: if_split)
|
||||
|
||||
lemma empty_fail_get:
|
||||
"empty_fail get"
|
||||
by (simp add: empty_fail_def get_def)
|
||||
|
||||
lemma empty_fail_catch:
|
||||
"\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catch f g)"
|
||||
by (simp add: catch_def split: sum.split)
|
||||
|
||||
lemma empty_fail_select[simp]:
|
||||
"empty_fail (select V) = (V \<noteq> {})"
|
||||
by (clarsimp simp: select_def empty_fail_def)
|
||||
|
||||
lemma empty_fail_not_snd:
|
||||
"\<lbrakk> \<not> snd (m s); empty_fail m \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> fst (m s)"
|
||||
by (fastforce simp: empty_fail_def)
|
||||
|
||||
lemmas empty_failD2 = empty_fail_not_snd[rotated]
|
||||
|
||||
lemma empty_failD3:
|
||||
"\<lbrakk> empty_fail f; \<not> snd (f s) \<rbrakk> \<Longrightarrow> fst (f s) \<noteq> {}"
|
||||
by (drule(1) empty_failD2, clarsimp)
|
||||
|
||||
|
||||
subsection "Failure"
|
||||
|
||||
lemma fail_wp: "\<lbrace>\<lambda>x. True\<rbrace> fail \<lbrace>Q\<rbrace>"
|
||||
|
|
|
|||
|
|
@ -98,18 +98,6 @@ lemma mapME_x_inv_wp:
|
|||
apply assumption
|
||||
done
|
||||
|
||||
|
||||
lemma empty_fail_error_bits:
|
||||
"empty_fail (returnOk v)"
|
||||
"empty_fail (throwError v)"
|
||||
"empty_fail (liftE f) = empty_fail f"
|
||||
apply (simp_all add: returnOk_def throwError_def)
|
||||
apply (rule iffI, simp_all add: liftE_def)
|
||||
apply (simp add: empty_fail_def bind_def return_def)
|
||||
apply (erule allEI)
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
lemma mapM_upd:
|
||||
assumes "\<And>x rv s s'. (rv,s') \<in> fst (f x s) \<Longrightarrow> x \<in> set xs \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))"
|
||||
shows "(rv,s') \<in> fst (mapM f xs s) \<Longrightarrow> (rv, g s') \<in> fst (mapM f xs (g s))"
|
||||
|
|
@ -130,15 +118,6 @@ next
|
|||
done
|
||||
qed
|
||||
|
||||
lemma empty_fail_whenEs:
|
||||
"empty_fail f \<Longrightarrow> empty_fail (whenE P f)"
|
||||
"empty_fail f \<Longrightarrow> empty_fail (unlessE P f)"
|
||||
by (auto simp add: whenE_def unlessE_def empty_fail_error_bits split: if_split)
|
||||
|
||||
lemma empty_fail_assertE:
|
||||
"empty_fail (assertE P)"
|
||||
by (simp add: assertE_def empty_fail_error_bits split: if_split)
|
||||
|
||||
lemma gets_the_validE_R_wp:
|
||||
"\<lbrace>\<lambda>s. f s \<noteq> None \<and> isRight (the (f s)) \<and> Q (theRight (the (f s))) s\<rbrace>
|
||||
gets_the f
|
||||
|
|
@ -173,45 +152,12 @@ lemma list_case_return: (* FIXME lib: move to Lib *)
|
|||
= return (case xs of [] \<Rightarrow> v | y # ys \<Rightarrow> f y ys)"
|
||||
by (simp split: list.split)
|
||||
|
||||
lemma lifted_if_collapse: (* FIXME lib: move to Lib *)
|
||||
"(if P then \<top> else f) = (\<lambda>s. \<not>P \<longrightarrow> f s)"
|
||||
by auto
|
||||
|
||||
lemmas list_case_return2 = list_case_return (* FIXME lib: eliminate *)
|
||||
|
||||
lemma empty_fail_get:
|
||||
"empty_fail get"
|
||||
by (simp add: empty_fail_def get_def)
|
||||
|
||||
lemma empty_failD2:
|
||||
"\<lbrakk> empty_fail f; \<not> snd (f s) \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> fst (f s)"
|
||||
by (fastforce simp add: empty_fail_def)
|
||||
|
||||
lemma empty_failD3:
|
||||
"\<lbrakk> empty_fail f; \<not> snd (f s) \<rbrakk> \<Longrightarrow> fst (f s) \<noteq> {}"
|
||||
by (drule(1) empty_failD2, clarsimp)
|
||||
|
||||
lemma bind_inv_inv_comm:
|
||||
"\<lbrakk> \<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>;
|
||||
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 (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 (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 bind_apply_cong, simp_all)
|
||||
apply (clarsimp simp: bind_def split_def return_def)
|
||||
apply (auto | drule(1) empty_failD3)+
|
||||
done
|
||||
|
||||
lemma no_fail_mapM:
|
||||
"\<forall>x. no_fail \<top> (f x) \<Longrightarrow> no_fail \<top> (mapM f xs)"
|
||||
apply (induct xs)
|
||||
|
|
@ -220,11 +166,6 @@ lemma no_fail_mapM:
|
|||
apply (wp|fastforce)+
|
||||
done
|
||||
|
||||
|
||||
lemma lifted_if_collapse: (* FIXME lib: move to Lib *)
|
||||
"(if P then \<top> else f) = (\<lambda>s. \<not>P \<longrightarrow> f s)"
|
||||
by auto
|
||||
|
||||
lemma filterM_preserved:
|
||||
"\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> m x \<lbrace>\<lambda>rv. P\<rbrace> \<rbrakk>
|
||||
\<Longrightarrow> \<lbrace>P\<rbrace> filterM m xs \<lbrace>\<lambda>rv. P\<rbrace>"
|
||||
|
|
@ -314,10 +255,6 @@ lemma mapM_x_wp:
|
|||
shows "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv. P\<rbrace>"
|
||||
by (subst mapM_x_mapM) (wp mapM_wp x)
|
||||
|
||||
|
||||
lemma empty_fail_assert : "empty_fail (assert P)"
|
||||
unfolding assert_def by simp
|
||||
|
||||
lemma no_fail_mapM':
|
||||
assumes rl: "\<And>x. no_fail (\<lambda>_. P x) (f x)"
|
||||
shows "no_fail (\<lambda>_. \<forall>x \<in> set xs. P x) (mapM f xs)"
|
||||
|
|
@ -361,19 +298,6 @@ lemma empty_fail_sequence_x :
|
|||
shows "empty_fail (sequence_x ms)" using assms
|
||||
by (induct ms) (auto simp: sequence_x_def)
|
||||
|
||||
lemma bind_known_operation_eq:
|
||||
"\<lbrakk> no_fail P f; \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<and> s = t\<rbrace>; P s; Q s; empty_fail f \<rbrakk>
|
||||
\<Longrightarrow> (f >>= g) s = g x t"
|
||||
apply (drule(1) no_failD)
|
||||
apply (subgoal_tac "fst (f s) = {(x, t)}")
|
||||
apply (clarsimp simp: bind_def)
|
||||
apply (rule not_psubset_eq)
|
||||
apply (drule(1) empty_failD2, clarsimp)
|
||||
apply fastforce
|
||||
apply clarsimp
|
||||
apply (drule(1) use_valid, simp+)
|
||||
done
|
||||
|
||||
lemma mapME_set:
|
||||
assumes est: "\<And>x. \<lbrace>R\<rbrace> f x \<lbrace>P\<rbrace>, -"
|
||||
and invp: "\<And>x y. \<lbrace>R and P x\<rbrace> f y \<lbrace>\<lambda>_. P x\<rbrace>, -"
|
||||
|
|
@ -415,13 +339,6 @@ lemma empty_fail_mapM_x [simp]:
|
|||
apply (clarsimp simp: mapM_x_Cons)
|
||||
done
|
||||
|
||||
lemma empty_fail_catch:
|
||||
"\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catch f g)"
|
||||
apply (simp add: catch_def)
|
||||
apply (erule empty_fail_bind)
|
||||
apply (simp split: sum.split)
|
||||
done
|
||||
|
||||
lemma valid_isRight_theRight_split:
|
||||
"\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q True rv s\<rbrace>,\<lbrace>\<lambda>e s. \<forall>v. Q False v s\<rbrace> \<Longrightarrow>
|
||||
\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q (isRight rv) (theRight rv) s\<rbrace>"
|
||||
|
|
@ -470,12 +387,4 @@ lemma case_option_find_give_me_a_map:
|
|||
apply (simp add: lift_def throwError_def returnOk_def split: sum.split)
|
||||
done
|
||||
|
||||
lemma empty_fail_select [simp]: "empty_fail (select V) = (V \<noteq> {})"
|
||||
apply (clarsimp simp: select_def empty_fail_def)
|
||||
done
|
||||
|
||||
lemma empty_fail_liftE [simp]:
|
||||
"empty_fail (liftE X) = empty_fail X"
|
||||
by (rule empty_fail_error_bits)
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue