diff options
Diffstat (limited to 'lib/isabelle')
| -rw-r--r-- | lib/isabelle/Hoare.thy | 100 | ||||
| -rw-r--r-- | lib/isabelle/Makefile | 5 | ||||
| -rw-r--r-- | lib/isabelle/Prompt_monad_lemmas.thy | 1 | ||||
| -rw-r--r-- | lib/isabelle/State_lemmas.thy | 138 | ||||
| -rw-r--r-- | lib/isabelle/manual/Manual.thy | 19 |
5 files changed, 187 insertions, 76 deletions
diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy index ee7a5fa6..9271e2fa 100644 --- a/lib/isabelle/Hoare.thy +++ b/lib/isabelle/Hoare.thy @@ -42,19 +42,20 @@ lemma PrePost_weaken_post: shows "PrePost A f C" using assms by (blast intro: PrePost_consequence) -named_theorems PrePost_intro +named_theorems PrePost_compositeI +named_theorems PrePost_atomI -lemma PrePost_True_post[PrePost_intro, intro, simp]: +lemma PrePost_True_post[PrePost_atomI, intro, simp]: "PrePost P m (\<lambda>_ _. True)" unfolding PrePost_def by auto lemma PrePost_any: "PrePost (\<lambda>s. \<forall>(r, s') \<in> m s. Q r s') m Q" unfolding PrePost_def by auto -lemma PrePost_returnS[intro, PrePost_intro]: "PrePost (P (Value x)) (returnS x) P" +lemma PrePost_returnS[intro, PrePost_atomI]: "PrePost (P (Value x)) (returnS x) P" unfolding PrePost_def returnS_def by auto -lemma PrePost_bindS[intro, PrePost_intro]: +lemma PrePost_bindS[intro, PrePost_compositeI]: assumes f: "\<And>s a s'. (Value a, s') \<in> m s \<Longrightarrow> PrePost (R a) (f a) Q" and m: "PrePost P m (\<lambda>r. case r of Value a \<Rightarrow> R a | Ex e \<Rightarrow> Q (Ex e))" shows "PrePost P (bindS m f) Q" @@ -89,10 +90,10 @@ lemma PrePost_bindS_unit: shows "PrePost P (bindS m f) Q" using assms by auto -lemma PrePost_readS[intro, PrePost_intro]: "PrePost (\<lambda>s. P (Value (f s)) s) (readS f) P" +lemma PrePost_readS[intro, PrePost_atomI]: "PrePost (\<lambda>s. P (Value (f s)) s) (readS f) P" unfolding PrePost_def readS_def returnS_def by auto -lemma PrePost_updateS[intro, PrePost_intro]: "PrePost (\<lambda>s. P (Value ()) (f s)) (updateS f) P" +lemma PrePost_updateS[intro, PrePost_atomI]: "PrePost (\<lambda>s. P (Value ()) (f s)) (updateS f) P" unfolding PrePost_def updateS_def returnS_def by auto lemma PrePost_if: @@ -100,7 +101,7 @@ lemma PrePost_if: shows "PrePost P (if b then f else g) Q" using assms by auto -lemma PrePost_if_branch[PrePost_intro]: +lemma PrePost_if_branch[PrePost_compositeI]: assumes "b \<Longrightarrow> PrePost Pf f Q" and "\<not>b \<Longrightarrow> PrePost Pg g Q" shows "PrePost (if b then Pf else Pg) (if b then f else g) Q" using assms by auto @@ -115,35 +116,65 @@ lemma PrePost_if_else: shows "PrePost P (if b then f else g) Q" using assms by auto -lemma PrePost_prod_cases[PrePost_intro]: +lemma PrePost_prod_cases[PrePost_compositeI]: assumes "PrePost P (f (fst x) (snd x)) Q" shows "PrePost P (case x of (a, b) \<Rightarrow> f a b) Q" using assms by (auto split: prod.splits) -lemma PrePost_option_cases[PrePost_intro]: +lemma PrePost_option_cases[PrePost_compositeI]: assumes "\<And>a. PrePost (PS a) (s a) Q" and "PrePost PN n Q" shows "PrePost (case x of Some a \<Rightarrow> PS a | None \<Rightarrow> PN) (case x of Some a \<Rightarrow> s a | None \<Rightarrow> n) Q" using assms by (auto split: option.splits) -lemma PrePost_let[intro, PrePost_intro]: +lemma PrePost_let[intro, PrePost_compositeI]: assumes "PrePost P (m y) Q" shows "PrePost P (let x = y in m x) Q" using assms by auto -lemma PrePost_assert_expS[intro, PrePost_intro]: "PrePost (if c then P (Value ()) else P (Ex (Failure m))) (assert_expS c m) P" +lemma PrePost_and_boolS[PrePost_compositeI]: + assumes r: "PrePost R r Q" + and l: "PrePost P l (\<lambda>r. case r of Value True \<Rightarrow> R | _ \<Rightarrow> Q r)" + shows "PrePost P (and_boolS l r) Q" + unfolding and_boolS_def +proof (rule PrePost_bindS) + fix s a s' + assume "(Value a, s') \<in> l s" + show "PrePost (if a then R else Q (Value False)) (if a then r else returnS False) Q" + using r by auto +next + show "PrePost P l (\<lambda>r. case r of Value a \<Rightarrow> if a then R else Q (Value False) | Ex e \<Rightarrow> Q (Ex e))" + using l by (elim PrePost_weaken_post) (auto split: result.splits) +qed + +lemma PrePost_or_boolS[PrePost_compositeI]: + assumes r: "PrePost R r Q" + and l: "PrePost P l (\<lambda>r. case r of Value False \<Rightarrow> R | _ \<Rightarrow> Q r)" + shows "PrePost P (or_boolS l r) Q" + unfolding or_boolS_def +proof (rule PrePost_bindS) + fix s a s' + assume "(Value a, s') \<in> l s" + show "PrePost (if a then Q (Value True) else R) (if a then returnS True else r) Q" + using r by auto +next + show "PrePost P l (\<lambda>r. case r of Value a \<Rightarrow> if a then Q (Value True) else R | Ex e \<Rightarrow> Q (Ex e))" + using l by (elim PrePost_weaken_post) (auto split: result.splits) +qed + +lemma PrePost_assert_expS[intro, PrePost_atomI]: "PrePost (if c then P (Value ()) else P (Ex (Failure m))) (assert_expS c m) P" unfolding PrePost_def assert_expS_def by (auto simp: returnS_def failS_def) -lemma PrePost_chooseS[intro, PrePost_intro]: "PrePost (\<lambda>s. \<forall>x \<in> xs. Q (Value x) s) (chooseS xs) Q" +lemma PrePost_chooseS[intro, PrePost_atomI]: "PrePost (\<lambda>s. \<forall>x \<in> xs. Q (Value x) s) (chooseS xs) Q" by (auto simp: PrePost_def chooseS_def) -lemma PrePost_failS[intro, PrePost_intro]: "PrePost (Q (Ex (Failure msg))) (failS msg) Q" +lemma PrePost_failS[intro, PrePost_atomI]: "PrePost (Q (Ex (Failure msg))) (failS msg) Q" by (auto simp: PrePost_def failS_def) lemma case_result_combine[simp]: "(case r of Value a \<Rightarrow> Q (Value a) | Ex e \<Rightarrow> Q (Ex e)) = Q r" by (auto split: result.splits) -lemma PrePost_foreachS_Nil[intro, simp, PrePost_intro]: +lemma PrePost_foreachS_Nil[intro, simp, PrePost_atomI]: "PrePost (Q (Value vars)) (foreachS [] vars body) Q" by auto @@ -219,20 +250,21 @@ lemma PrePostE_weaken_post: shows "PrePostE A f C E" using assms by (blast intro: PrePostE_consequence) -named_theorems PrePostE_intro +named_theorems PrePostE_compositeI +named_theorems PrePostE_atomI -lemma PrePostE_True_post[PrePost_intro, intro, simp]: +lemma PrePostE_True_post[PrePostE_atomI, intro, simp]: "PrePostE P m (\<lambda>_ _. True) (\<lambda>_ _. True)" unfolding PrePost_defs by (auto split: result.splits) lemma PrePostE_any: "PrePostE (\<lambda>s. \<forall>(r, s') \<in> m s. case r of Value a \<Rightarrow> Q a s' | Ex e \<Rightarrow> E e s') m Q E" by (intro PrePostE_I) auto -lemma PrePostE_returnS[PrePostE_intro, intro, simp]: +lemma PrePostE_returnS[PrePostE_atomI, intro, simp]: "PrePostE (P x) (returnS x) P Q" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) -lemma PrePostE_bindS[intro, PrePostE_intro]: +lemma PrePostE_bindS[intro, PrePostE_compositeI]: assumes f: "\<And>s a s'. (Value a, s') \<in> m s \<Longrightarrow> PrePostE (R a) (f a) Q E" and m: "PrePostE P m R E" shows "PrePostE P (bindS m f) Q E" @@ -252,13 +284,13 @@ lemma PrePostE_bindS_unit: shows "PrePostE P (bindS m f) Q E" using assms by auto -lemma PrePostE_readS[PrePostE_intro, intro]: "PrePostE (\<lambda>s. Q (f s) s) (readS f) Q E" +lemma PrePostE_readS[PrePostE_atomI, intro]: "PrePostE (\<lambda>s. Q (f s) s) (readS f) Q E" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) -lemma PrePostE_updateS[PrePostE_intro, intro]: "PrePostE (\<lambda>s. Q () (f s)) (updateS f) Q E" +lemma PrePostE_updateS[PrePostE_atomI, intro]: "PrePostE (\<lambda>s. Q () (f s)) (updateS f) Q E" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) -lemma PrePostE_if_branch[PrePostE_intro]: +lemma PrePostE_if_branch[PrePostE_compositeI]: assumes "b \<Longrightarrow> PrePostE Pf f Q E" and "\<not>b \<Longrightarrow> PrePostE Pg g Q E" shows "PrePostE (if b then Pf else Pg) (if b then f else g) Q E" using assms by (auto) @@ -278,30 +310,44 @@ lemma PrePostE_if_else: shows "PrePostE P (if b then f else g) Q E" using assms by auto -lemma PrePostE_prod_cases[PrePostE_intro]: +lemma PrePostE_prod_cases[PrePostE_compositeI]: assumes "PrePostE P (f (fst x) (snd x)) Q E" shows "PrePostE P (case x of (a, b) \<Rightarrow> f a b) Q E" using assms by (auto split: prod.splits) -lemma PrePostE_option_cases[PrePostE_intro]: +lemma PrePostE_option_cases[PrePostE_compositeI]: assumes "\<And>a. PrePostE (PS a) (s a) Q E" and "PrePostE PN n Q E" shows "PrePostE (case x of Some a \<Rightarrow> PS a | None \<Rightarrow> PN) (case x of Some a \<Rightarrow> s a | None \<Rightarrow> n) Q E" using assms by (auto split: option.splits) -lemma PrePostE_let[PrePostE_intro]: +lemma PrePostE_let[PrePostE_compositeI]: assumes "PrePostE P (m y) Q E" shows "PrePostE P (let x = y in m x) Q E" using assms by auto -lemma PrePostE_assert_expS[PrePostE_intro, intro]: +lemma PrePostE_and_boolS[PrePostE_compositeI]: + assumes r: "PrePostE R r Q E" + and l: "PrePostE P l (\<lambda>r. if r then R else Q False) E" + shows "PrePostE P (and_boolS l r) Q E" + using assms unfolding PrePostE_def + by (intro PrePost_and_boolS) (auto elim: PrePost_weaken_post split: if_splits result.splits) + +lemma PrePostE_or_boolS[PrePostE_compositeI]: + assumes r: "PrePostE R r Q E" + and l: "PrePostE P l (\<lambda>r. if r then Q True else R) E" + shows "PrePostE P (or_boolS l r) Q E" + using assms unfolding PrePostE_def + by (intro PrePost_or_boolS) (auto elim: PrePost_weaken_post split: if_splits result.splits) + +lemma PrePostE_assert_expS[PrePostE_atomI, intro]: "PrePostE (if c then P () else Q (Failure m)) (assert_expS c m) P Q" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) -lemma PrePostE_failS[PrePost_intro, intro]: +lemma PrePostE_failS[PrePostE_atomI, intro]: "PrePostE (E (Failure msg)) (failS msg) Q E" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) -lemma PrePostE_chooseS[intro, PrePostE_intro]: +lemma PrePostE_chooseS[intro, PrePostE_atomI]: "PrePostE (\<lambda>s. \<forall>x \<in> xs. Q x s) (chooseS xs) Q E" unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre) diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index f8786321..b10dde78 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -1,6 +1,6 @@ THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \ Sail_operators_mwords.thy Sail_operators_bitlists.thy \ - State_monad.thy State.thy Prompt_monad.thy Prompt.thy + State_monad.thy State.thy State_lifting.thy Prompt_monad.thy Prompt.thy EXTRA_THYS = State_monad_lemmas.thy State_lemmas.thy Prompt_monad_lemmas.thy \ Sail_operators_mwords_lemmas.thy Hoare.thy @@ -51,5 +51,8 @@ State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_lemmas.thy lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< +State_lifting.thy: ../../src/gen_lib/state_lifting.lem Prompt.thy State.thy + lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $< + clean: -rm $(THYS) diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy index e883c2a0..7a3a108d 100644 --- a/lib/isabelle/Prompt_monad_lemmas.thy +++ b/lib/isabelle/Prompt_monad_lemmas.thy @@ -17,6 +17,7 @@ lemmas bind_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_e lemma bind_return[simp]: "bind (return a) f = f a" by (auto simp: return_def) +lemma bind_return_right[simp]: "bind x return = x" by (induction x) (auto simp: return_def) lemma bind_assoc[simp]: "bind (bind m f) g = bind m (\<lambda>x. bind (f x) g)" by (induction m f arbitrary: g rule: bind.induct) auto diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy index 84b08e6c..cf5e4dbf 100644 --- a/lib/isabelle/State_lemmas.thy +++ b/lib/isabelle/State_lemmas.thy @@ -1,16 +1,18 @@ theory State_lemmas - imports State + imports State State_lifting begin lemma All_liftState_dom: "liftState_dom (r, m)" by (induction m) (auto intro: liftState.domintros) termination liftState using All_liftState_dom by auto -lemma liftState_bind[simp]: +named_theorems liftState_simp + +lemma liftState_bind[liftState_simp]: "liftState r (bind m f) = bindS (liftState r m) (liftState r \<circ> f)" by (induction m f rule: bind.induct) auto -lemma liftState_return[simp]: "liftState r (return a) = returnS a" by (auto simp: return_def) +lemma liftState_return[liftState_simp]: "liftState r (return a) = returnS a" by (auto simp: return_def) lemma Value_liftState_Run: assumes "(Value a, s') \<in> liftState r m s" @@ -19,45 +21,58 @@ lemma Value_liftState_Run: auto simp add: failS_def throwS_def returnS_def simp del: read_regvalS.simps; blast elim: Value_bindS_elim) -lemmas liftState_if_distrib[simp] = if_distrib[where f = "liftState ra" for ra] - -lemma liftState_throw[simp]: "liftState r (throw e) = throwS e" by (auto simp: throw_def) -lemma liftState_assert[simp]: "liftState r (assert_exp c msg) = assert_expS c msg" by (auto simp: assert_exp_def assert_expS_def) -lemma liftState_exit[simp]: "liftState r (exit0 ()) = exitS ()" by (auto simp: exit0_def exitS_def) -lemma liftState_exclResult[simp]: "liftState r (excl_result ()) = excl_resultS ()" by (auto simp: excl_result_def) -lemma liftState_barrier[simp]: "liftState r (barrier bk) = returnS ()" by (auto simp: barrier_def) -lemma liftState_footprint[simp]: "liftState r (footprint ()) = returnS ()" by (auto simp: footprint_def) -lemma liftState_undefined[simp]: "liftState r (undefined_bool ()) = undefined_boolS ()" by (auto simp: undefined_bool_def) -lemma liftState_maybe_fail[simp]: "liftState r (maybe_fail msg x) = maybe_failS msg x" - by (auto simp: maybe_fail_def maybe_failS_def split: option.splits) - -lemma liftState_try_catch[simp]: +lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra] + +lemma liftState_throw[liftState_simp]: "liftState r (throw e) = throwS e" + by (auto simp: throw_def) +lemma liftState_assert[liftState_simp]: "liftState r (assert_exp c msg) = assert_expS c msg" + by (auto simp: assert_exp_def assert_expS_def) +lemma liftState_exit[liftState_simp]: "liftState r (exit0 ()) = exitS ()" + by (auto simp: exit0_def exitS_def) +lemma liftState_exclResult[liftState_simp]: "liftState r (excl_result ()) = excl_resultS ()" + by (auto simp: excl_result_def liftState_simp) +lemma liftState_barrier[liftState_simp]: "liftState r (barrier bk) = returnS ()" + by (auto simp: barrier_def) +lemma liftState_footprint[liftState_simp]: "liftState r (footprint ()) = returnS ()" + by (auto simp: footprint_def) +lemma liftState_undefined[liftState_simp]: "liftState r (undefined_bool ()) = undefined_boolS ()" + by (auto simp: undefined_bool_def liftState_simp) +lemma liftState_maybe_fail[liftState_simp]: "liftState r (maybe_fail msg x) = maybe_failS msg x" + by (auto simp: maybe_fail_def maybe_failS_def liftState_simp split: option.splits) +lemma liftState_and_boolM[liftState_simp]: + "liftState r (and_boolM x y) = and_boolS (liftState r x) (liftState r y)" + by (auto simp: and_boolM_def and_boolS_def liftState_simp cong: bindS_cong if_cong) +lemma liftState_or_boolM[liftState_simp]: + "liftState r (or_boolM x y) = or_boolS (liftState r x) (liftState r y)" + by (auto simp: or_boolM_def or_boolS_def liftState_simp cong: bindS_cong if_cong) + +lemma liftState_try_catch[liftState_simp]: "liftState r (try_catch m h) = try_catchS (liftState r m) (liftState r \<circ> h)" by (induction m h rule: try_catch_induct) (auto simp: try_catchS_bindS_no_throw) -lemma liftState_early_return[simp]: +lemma liftState_early_return[liftState_simp]: "liftState r (early_return r) = early_returnS r" - by (auto simp: early_return_def early_returnS_def) + by (auto simp: early_return_def early_returnS_def liftState_simp) -lemma liftState_catch_early_return[simp]: +lemma liftState_catch_early_return[liftState_simp]: "liftState r (catch_early_return m) = catch_early_returnS (liftState r m)" - by (auto simp: catch_early_return_def catch_early_returnS_def sum.case_distrib cong: sum.case_cong) + by (auto simp: catch_early_return_def catch_early_returnS_def sum.case_distrib liftState_simp cong: sum.case_cong) -lemma liftState_liftR[simp]: - "liftState r (liftR m) = liftSR (liftState r m)" - by (auto simp: liftR_def liftSR_def) +lemma liftState_liftR[liftState_simp]: + "liftState r (liftR m) = liftRS (liftState r m)" + by (auto simp: liftR_def liftRS_def liftState_simp) -lemma liftState_try_catchR[simp]: - "liftState r (try_catchR m h) = try_catchSR (liftState r m) (liftState r \<circ> h)" - by (auto simp: try_catchR_def try_catchSR_def sum.case_distrib cong: sum.case_cong) +lemma liftState_try_catchR[liftState_simp]: + "liftState r (try_catchR m h) = try_catchRS (liftState r m) (liftState r \<circ> h)" + by (auto simp: try_catchR_def try_catchRS_def sum.case_distrib liftState_simp cong: sum.case_cong) lemma liftState_read_mem_BC: assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a" shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz" using assms - by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def split: option.splits) + by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def liftState_simp split: option.splits) -lemma liftState_read_mem[simp]: +lemma liftState_read_mem[liftState_simp]: "\<And>a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz" "\<And>a. liftState r (read_mem BC_bitU_list BC_bitU_list rk a sz) = read_memS BC_bitU_list BC_bitU_list rk a sz" by (auto simp: liftState_read_mem_BC) @@ -67,14 +82,14 @@ lemma liftState_write_mem_ea_BC: shows "liftState r (write_mem_ea BCa rk a sz) = write_mem_eaS BCa rk a (nat sz)" using assms by (auto simp: write_mem_ea_def write_mem_eaS_def) -lemma liftState_write_mem_ea[simp]: +lemma liftState_write_mem_ea[liftState_simp]: "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = write_mem_eaS BC_mword rk a (nat sz)" "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = write_mem_eaS BC_bitU_list rk a (nat sz)" by (auto simp: liftState_write_mem_ea_BC) lemma liftState_write_mem_val: "liftState r (write_mem_val BC v) = write_mem_valS BC v" - by (auto simp: write_mem_val_def write_mem_valS_def split: option.splits) + by (auto simp: write_mem_val_def write_mem_valS_def liftState_simp split: option.splits) lemma liftState_read_reg_readS: assumes "\<And>s. Option.bind (get_regval' (name reg) s) (of_regval reg) = Some (read_from reg s)" @@ -93,22 +108,23 @@ lemma liftState_write_reg_updateS: shows "liftState (get_regval', set_regval') (write_reg reg v) = updateS (regstate_update (write_to reg v))" using assms by (auto simp: write_reg_def updateS_def returnS_def bindS_readS) -lemma liftState_iter_aux[simp]: +lemma liftState_iter_aux[liftState_simp]: shows "liftState r (iter_aux i f xs) = iterS_aux i (\<lambda>i x. liftState r (f i x)) xs" - by (induction i "\<lambda>i x. liftState r (f i x)" xs rule: iterS_aux.induct) (auto cong: bindS_cong) + by (induction i "\<lambda>i x. liftState r (f i x)" xs rule: iterS_aux.induct) + (auto simp: liftState_simp cong: bindS_cong) -lemma liftState_iteri[simp]: +lemma liftState_iteri[liftState_simp]: "liftState r (iteri f xs) = iteriS (\<lambda>i x. liftState r (f i x)) xs" - by (auto simp: iteri_def iteriS_def) + by (auto simp: iteri_def iteriS_def liftState_simp) -lemma liftState_iter[simp]: +lemma liftState_iter[liftState_simp]: "liftState r (iter f xs) = iterS (liftState r \<circ> f) xs" - by (auto simp: iter_def iterS_def) + by (auto simp: iter_def iterS_def liftState_simp) -lemma liftState_foreachM[simp]: +lemma liftState_foreachM[liftState_simp]: "liftState r (foreachM xs vars body) = foreachS xs vars (\<lambda>x vars. liftState r (body x vars))" by (induction xs vars "\<lambda>x vars. liftState r (body x vars)" rule: foreachS.induct) - (auto cong: bindS_cong) + (auto simp: liftState_simp cong: bindS_cong) lemma whileS_dom_step: assumes "whileS_dom (vars, cond, body, s)" @@ -156,7 +172,7 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState qed then show ?case using while while' that IH by auto qed auto - then show ?case by auto + then show ?case by (auto simp: liftState_simp) qed auto qed @@ -194,9 +210,51 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState show "\<exists>t. Run (body vars) t vars'" using k by (auto elim: Value_liftState_Run) show "\<exists>t'. Run (cond vars') t' False" using until that by (auto elim: Value_liftState_Run) qed - then show ?case using k until IH by (auto simp: comp_def) + then show ?case using k until IH by (auto simp: comp_def liftState_simp) qed auto qed auto qed +(* Simplification rules for monadic Boolean connectives *) + +lemma if_return_return[simp]: "(if a then return True else return False) = return a" by auto + +lemma and_boolM_simps[simp]: + "and_boolM (return b) y = (if b then y else return False)" + "and_boolM x (return True) = x" + "and_boolM x (return False) = x \<bind> (\<lambda>_. return False)" + "\<And>x y z. and_boolM (x \<bind> y) z = (x \<bind> (\<lambda>r. and_boolM (y r) z))" + by (auto simp: and_boolM_def) + +lemmas and_boolM_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolM x y" for y] + +lemma or_boolM_simps[simp]: + "or_boolM (return b) y = (if b then return True else y)" + "or_boolM x (return True) = x \<bind> (\<lambda>_. return True)" + "or_boolM x (return False) = x" + "\<And>x y z. or_boolM (x \<bind> y) z = (x \<bind> (\<lambda>r. or_boolM (y r) z))" + by (auto simp: or_boolM_def) + +lemmas or_boolM_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolM x y" for y] + +lemma if_returnS_returnS[simp]: "(if a then returnS True else returnS False) = returnS a" by auto + +lemma and_boolS_simps[simp]: + "and_boolS (returnS b) y = (if b then y else returnS False)" + "and_boolS x (returnS True) = x" + "and_boolS x (returnS False) = bindS x (\<lambda>_. returnS False)" + "\<And>x y z. and_boolS (bindS x y) z = (bindS x (\<lambda>r. and_boolS (y r) z))" + by (auto simp: and_boolS_def) + +lemmas and_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolS x y" for y] + +lemma or_boolS_simps[simp]: + "or_boolS (returnS b) y = (if b then returnS True else y)" + "or_boolS x (returnS True) = bindS x (\<lambda>_. returnS True)" + "or_boolS x (returnS False) = x" + "\<And>x y z. or_boolS (bindS x y) z = (bindS x (\<lambda>r. or_boolS (y r) z))" + by (auto simp: or_boolS_def) + +lemmas or_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolS x y" for y] + end diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy index 6cdfbfa1..0c83ebea 100644 --- a/lib/isabelle/manual/Manual.thy +++ b/lib/isabelle/manual/Manual.thy @@ -288,7 +288,7 @@ exception handler as arguments. The exception mechanism is also used to implement early returns by throwing and catching return values: A function body with one or more early returns of type @{typ 'a} (and exception type @{typ 'e}) is lifted to a monadic expression with exception type @{typ "('a + 'e)"} using -@{term liftSR}, such that an early return of the value @{term a} throws @{term "Inl a"}, and a +@{term liftRS}, such that an early return of the value @{term a} throws @{term "Inl a"}, and a regular exception @{term e} is thrown as @{term "Inr e"}. The function body is then wrapped in @{term catch_early_returnS} to lower it back to the default monad and exception type. These liftings and lowerings are automatically inserted by Sail for functions with early returns.\<^footnote>\<open>To be @@ -412,7 +412,9 @@ case, defined as @{thm [display, names_short] PrePostE_def} The theory includes standard proof rules for both of these variants, in particular rules giving weakest preconditions of the predefined primitives of the monad, collected under the names -@{attribute PrePost_intro} and @{attribute PrePostE_intro}, respectively. +@{attribute PrePost_atomI} for atoms such as @{term return} and @{attribute PrePost_compositeI} +for composites such as @{term bind} (or @{attribute PrePostE_atomI} and +@{attribute PrePostE_compositeI}, respectively, for the quadruple variant). The instruction we are considering is defined as @{thm [display] execute_ITYPE.simps[of _ rs for rs]} @@ -448,16 +450,17 @@ lemma shows "PrePostE pre (liftS instr) post (\<lambda>_ _. False)" unfolding pre_def instr_def post_def - by (simp add: rX_def wX_def cong: bindS_cong if_cong split del: if_split) - (rule PrePostE_strengthen_pre, (rule PrePostE_intro)+, auto simp: uint_0_iff) + by (simp add: rX_def wX_def liftState_simp cong: bindS_cong if_cong split del: if_split) + (rule PrePostE_strengthen_pre, (rule PrePostE_atomI PrePostE_compositeI)+, auto simp: uint_0_iff) text \<open>The proof begins with a simplification step, which not only unfolds the definitions of the auxiliary functions @{term rX} and @{term wX}, but also performs the lifting from the free monad to the state monad. We apply the rule @{thm [source] PrePostE_strengthen_pre} (in a -backward manner) to allow a weaker precondition, then use the rules in @{attribute PrePostE_intro} -to derive a weakest precondition, and then use @{method auto} to show that it is implied by -the given precondition. For more serious proofs, one will want to set up specialised proof -tactics. This example uses only basic proof methods, to make the reasoning steps more explicit.\<close> +backward manner) to allow a weaker precondition, then use the rules in +@{attribute PrePostE_compositeI} and @{attribute PrePostE_atomI} to derive a weakest precondition, +and then use @{method auto} to show that it is implied by the given precondition. For more serious +proofs, one will want to set up specialised proof tactics. This example uses only basic proof +methods, to make the reasoning steps more explicit.\<close> (*<*) end |