assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D B C R (Q rv) (Q' rv') (g rv) (g' rv')"
assumes r1: "equiv_valid_2 D A B R' P P' f f'"
assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>"
assumes hoare': "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>"
shows "equiv_valid_2 D A C R (\<lambda> s. P s \<and> S s) (\<lambda> s. P' s \<and> S' s) (f >>= g) (f' >>= g')"
using assms
unfolding bind_def equiv_valid_2_def valid_def
apply fastforce
done
(* almost all of the time, the second relation doesn't change *)
lemma equiv_valid_2_bind:
assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D A A R (Q rv) (Q' rv') (g rv) (g' rv')"
assumes r1: "equiv_valid_2 D A A R' P P' f f'"
assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>"
assumes hoare': "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>"
shows "equiv_valid_2 D A A R (\<lambda> s. P s \<and> S s) (\<lambda> s. P' s \<and> S' s) (f >>= g) (f' >>= g')"
using assms by (blast intro: equiv_valid_2_bind_general)
lemma equiv_valid_2_guard_imp:
assumes reads_res: "equiv_valid_2 D A B R Q Q' f f'"
assumes guard_imp: "\<And> s. P s \<Longrightarrow> Q s"
assumes guard_imp': "\<And> s. P' s \<Longrightarrow> Q' s"
shows "equiv_valid_2 D A B R P P' f f'"
using assms
by (fastforce simp: equiv_valid_2_def)
lemma equiv_valid_2_bind_pre:
assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D A A R (Q rv) (Q' rv') (g rv) (g' rv')"
assumes r1: "equiv_valid_2 D A A R' P P' f f'"
assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>"
assumes hoare': "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>"
assumes guard_imp: "\<And> s. T s \<Longrightarrow> P s \<and> S s"
assumes guard_imp': "\<And> s. T' s \<Longrightarrow> P' s \<and> S' s"
shows "equiv_valid_2 D A A R T T' (f >>= g) (f' >>= g')"
using assms by (blast intro: equiv_valid_2_bind[THEN equiv_valid_2_guard_imp])
lemma return_ev2:
assumes rel: "\<And> s t. \<lbrakk>P s; P' t; I s t; A s t\<rbrakk> \<Longrightarrow> R a b"
shows "equiv_valid_2 I A A R P P' (return a) (return b)"
by(auto simp: equiv_valid_2_def return_def rel)
lemma equiv_valid_2_liftE:
"equiv_valid_2 D A B R P P' f f' \<Longrightarrow>
equiv_valid_2 D A B (E \<oplus> R) P P' (liftE f) (liftE f')"
apply(unfold liftE_def)
apply(rule equiv_valid_2_guard_imp)
apply(rule_tac Q="\<top>\<top>" and Q'="\<top>\<top>" and R'=R in equiv_valid_2_bind_general)
apply(fastforce intro: return_ev2)
apply assumption
apply(rule wp_post_taut)+
by(simp_all)
lemma equiv_valid_2_liftE_bindE_general:
assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D B C R (Q rv) (Q' rv') (g rv) (g' rv')"
assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>"
assumes hoare': "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>"
assumes r1: "equiv_valid_2 D A B R' P P' f f'"
shows "equiv_valid_2 D A C R (P and S) (P' and S') (liftE f >>=E g) (liftE f' >>=E g')"
apply(unfold bindE_def)
apply(rule equiv_valid_2_guard_imp)
apply(rule_tac Q="\<lambda> rv. K (\<forall> v. rv \<noteq> Inl v) and (\<lambda> s. \<forall> v. rv = Inr v \<longrightarrow> Q v s)" and Q'="\<lambda> rv. K (\<forall> v. rv \<noteq> Inl v) and (\<lambda> s. \<forall> v. rv = Inr v \<longrightarrow> Q' v s)" in equiv_valid_2_bind_general)
assumes "Q \<Longrightarrow> equiv_valid D A B P f"
shows "equiv_valid D A B (P and K Q) f"
using assms by (fastforce simp: equiv_valid_def2 equiv_valid_2_def)
declare K_def [simp del]
lemmas gen_asm_ev =
gen_asm_ev'[where P="\<top>", simplified]
gen_asm_ev'
gen_asm_ev'[simplified K_def, where P="\<top>", simplified]
gen_asm_ev'[simplified K_def]
declare K_def [simp]
text {*
This is a further streamlined version that we expect to get the most from
automating, and for the most part, we shouldn't need to deal with the
extra generality of the properties above.
*}
abbreviation equiv_valid_inv where
"equiv_valid_inv I A P f \<equiv> equiv_valid I A A P f"
abbreviation equiv_valid_rv_inv where
"equiv_valid_rv_inv I A R P f \<equiv> equiv_valid_rv I A A R P f"
lemma get_evrv:
"equiv_valid_rv_inv I A (I And A) \<top> get"
by(auto simp: equiv_valid_2_def get_def)
lemma equiv_valid_rv_bind_general:
assumes ev1:
"equiv_valid_rv I A B W P f"
assumes ev2:
"\<And> rv rv'. W rv rv' \<Longrightarrow> equiv_valid_2 I B C R (Q rv) (Q rv') (g rv) (g rv')"
assumes hoare:
"\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
shows "equiv_valid_rv I A C R P (f >>= g)"
apply(rule equiv_valid_2_guard_imp)
apply(rule equiv_valid_2_bind_general[OF ev2])
apply(assumption)
apply(rule ev1)
apply(rule hoare)
apply(rule hoare)
apply(simp_all)
done
lemma equiv_valid_rv_bind:
assumes ev1:
"equiv_valid_rv_inv I A W P f"
assumes ev2:
"\<And> rv rv'. W rv rv' \<Longrightarrow> equiv_valid_2 I A A R (Q rv) (Q rv') (g rv) (g rv')"
assumes hoare:
"\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
shows "equiv_valid_rv_inv I A R P (f >>= g)"
using assms by(blast intro: equiv_valid_rv_bind_general)
lemma modify_ev2:
assumes "\<And> s t. \<lbrakk>I s t; A s t; P s; P' t\<rbrakk> \<Longrightarrow> R () () \<and> I (f s) (f' t) \<and> B (f s) (f' t)"
shows
"equiv_valid_2 I A B R P P' (modify f) (modify f')"
apply(clarsimp simp: equiv_valid_2_def in_monad)
using assms by auto
lemma put_ev2:
assumes "\<And> s t. \<lbrakk>I s t; A s t; P s; P' t\<rbrakk> \<Longrightarrow> R () () \<and> I x x' \<and> B x x'"
shows
"equiv_valid_2 I A B R P P' (put x) (put x')"
apply(clarsimp simp: equiv_valid_2_def in_monad)
using assms by auto
lemma get_bind_ev2:
assumes "\<And> rv rv'. \<lbrakk>I rv rv'; A rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 I A B R (P and (op = rv)) (P' and (op = rv')) (f rv) (f' rv')"
shows "equiv_valid_2 I A B R P P' (get >>= f) (get >>= f')"
apply(rule equiv_valid_2_guard_imp)
apply(rule_tac R'="I And A" in equiv_valid_2_bind_general)
apply(rule assms, simp+)
apply(rule get_evrv)
apply(wp get_sp)
by(auto)
lemma return_ev_pre:
"equiv_valid_inv I A P (return x)"
apply (simp add: equiv_valid_def2 return_ev2)
done
lemmas return_ev = return_ev_pre[where P=\<top>]
lemma fail_ev2_l:
"equiv_valid_2 I A B R P P' fail f'"
by(simp add: equiv_valid_2_def fail_def)
lemma fail_ev2_r:
"equiv_valid_2 I A B R P P' f fail"
by(simp add: equiv_valid_2_def fail_def)
lemma fail_ev_pre:
"equiv_valid I A B P fail"
apply (simp add: equiv_valid_def2 fail_ev2_l)
done
lemmas fail_ev = fail_ev_pre[where P=\<top>]
lemma assert_ev2:
"R () () \<Longrightarrow> equiv_valid_2 I A A R P P' (assert a) (assert b)"
apply(simp add: assert_def fail_ev2_l fail_ev2_r)
apply(blast intro: return_ev2)
done
lemma liftE_ev:
"equiv_valid I A B P f \<Longrightarrow> equiv_valid I A B P (liftE f)"
unfolding liftE_def
apply (rule bind_ev_general[THEN equiv_valid_guard_imp, OF return_ev _ wp_post_taut])
apply fastforce+ (* schematic instantiation *)
done
lemma if_ev:
assumes "b \<Longrightarrow> equiv_valid I A B P f"
assumes "\<not> b \<Longrightarrow> equiv_valid I A B Q g"
shows "equiv_valid I A B (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s)) (if b then f else g)"
(* Of course, when we know that progress is always made, we can do better *)
lemma liftE_bindE_ev_general:
assumes r2: "\<And> val. equiv_valid I B C (Q val) (g val)"
assumes r1: "equiv_valid I A B P f"
assumes hoare: "\<lbrace> R \<rbrace> f \<lbrace> Q \<rbrace>"
shows "equiv_valid I A C (\<lambda> s. P s \<and> R s) (liftE f >>=E g)"
apply(simp add: bindE_def)
apply(rule_tac Q="\<lambda> rv. K (\<forall> v. rv \<noteq> Inl v) and (\<lambda> s. \<forall> v. rv = Inr v \<longrightarrow> Q v s)" in bind_ev_general)
"\<lbrakk> G \<Longrightarrow> spec_equiv_valid_inv s' I A P f;
\<not> G \<Longrightarrow> spec_equiv_valid_inv s' I A P' f'
\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv s' I A (\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)) (if G then f else f')"
"equiv_valid_2 I A A R P P' f f' \<Longrightarrow>
spec_equiv_valid_2_inv s I A R P P' f f'"
apply(simp add: spec_equiv_valid_2_inv_def)
apply(erule equiv_valid_2_guard_imp, auto)
done
lemma spec_equiv_valid_2_inv_guard_imp:
"\<lbrakk>spec_equiv_valid_2_inv s I A R Q Q' f f'; \<And> s. P s \<Longrightarrow> Q s; \<And> s. P' s \<Longrightarrow> Q' s\<rbrakk> \<Longrightarrow>
assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (P x) (m x)"
assumes inv: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> \<lambda>s. \<forall>x\<in>set lst. P x s \<rbrace> m x \<lbrace> \<lambda>_ s. \<forall>x\<in>set lst. P x s \<rbrace>"
shows "equiv_valid_inv D A (\<lambda> s. \<forall>x\<in>set lst. P x s) (mapM m lst)"
assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (P x) (m x)"
assumes inv: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> \<lambda>s. \<forall>x\<in>set lst. P x s \<rbrace> m x \<lbrace> \<lambda>_ s. \<forall>x\<in>set lst. P x s \<rbrace>"
shows "equiv_valid_inv D A (\<lambda> s. \<forall>x\<in>set lst. P x s) (mapM_x m lst)"
"\<lbrakk>P' \<Longrightarrow> equiv_valid_2 I A B R P Q f f'\<rbrakk> \<Longrightarrow>
equiv_valid_2 I A B R P (Q and (K P')) f f'"
apply(fastforce simp: equiv_valid_2_def)
done
lemma gen_asm_ev2_l:
"\<lbrakk>P \<Longrightarrow> equiv_valid_2 I A B R Q P' f f'\<rbrakk> \<Longrightarrow>
equiv_valid_2 I A B R (Q and (K P)) P' f f'"
apply(fastforce simp: equiv_valid_2_def)
done
lemma gen_asm_ev2_r':
"\<lbrakk>P' \<Longrightarrow> equiv_valid_2 I A B R P \<top> f f'\<rbrakk> \<Longrightarrow>
equiv_valid_2 I A B R P (\<lambda>s. P') f f'"
apply(fastforce simp: equiv_valid_2_def)
done
lemma gen_asm_ev2_l':
"\<lbrakk>P \<Longrightarrow> equiv_valid_2 I A B R \<top> P' f f'\<rbrakk> \<Longrightarrow>
equiv_valid_2 I A B R (\<lambda>s. P) P' f f'"
apply(fastforce simp: equiv_valid_2_def)
done
lemma equiv_valid_rv_liftE_bindE:
assumes ev1:
"equiv_valid_rv_inv I A W P f"
assumes ev2:
"\<And> rv rv'. W rv rv' \<Longrightarrow> equiv_valid_2 I A A R (Q rv) (Q rv') (g rv) (g rv')"
assumes hoare:
"\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
shows "equiv_valid_rv_inv I A R P ((liftE f) >>=E g)"
apply(unfold bindE_def)
apply(rule_tac Q="\<lambda> rv. K (\<forall> v. rv \<noteq> Inl v) and (\<lambda> s. \<forall> v. rv = Inr v \<longrightarrow> Q v s)" in equiv_valid_rv_bind)