diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Hoare.thy | 131 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_operators_mwords_lemmas.thy | 57 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_prompt_monad_lemmas.thy | 41 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_state_lemmas.thy | 109 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_values_lemmas.thy | 140 |
5 files changed, 460 insertions, 18 deletions
diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy index 88807c7c..76750117 100644 --- a/lib/isabelle/Hoare.thy +++ b/lib/isabelle/Hoare.thy @@ -253,6 +253,27 @@ lemma PrePostE_weaken_post: named_theorems PrePostE_compositeI named_theorems PrePostE_atomI +lemma PrePostE_conj_conds: + assumes "PrePostE P1 m Q1 E1" + and "PrePostE P2 m Q2 E2" + shows "PrePostE (\<lambda>s. P1 s \<and> P2 s) m (\<lambda>r s. Q1 r s \<and> Q2 r s) (\<lambda>e s. E1 e s \<and> E2 e s)" + using assms by (auto intro: PrePostE_I elim: PrePostE_elim) + +lemmas PrePostE_conj_conds_consequence = PrePostE_conj_conds[THEN PrePostE_consequence] + +lemma PrePostE_post_mp: + assumes "PrePostE P m Q' E" + and "PrePostE P m (\<lambda>r s. Q' r s \<longrightarrow> Q r s) E" + shows "PrePostE P m Q E" + using PrePostE_conj_conds[OF assms] by (auto intro: PrePostE_weaken_post) + +lemma PrePostE_cong: + assumes "\<And>s. P1 s \<longleftrightarrow> P2 s" and "\<And>s. P1 s \<Longrightarrow> m1 s = m2 s" and "\<And>r s. Q1 r s \<longleftrightarrow> Q2 r s" + and "\<And>e s. E1 e s \<longleftrightarrow> E2 e s" + shows "PrePostE P1 m1 Q1 E1 \<longleftrightarrow> PrePostE P2 m2 Q2 E2" + using assms unfolding PrePostE_def PrePost_def + by (auto split: result.splits) + lemma PrePostE_True_post[PrePostE_atomI, intro, simp]: "PrePostE P m (\<lambda>_ _. True) (\<lambda>_ _. True)" unfolding PrePost_defs by (auto split: result.splits) @@ -320,6 +341,11 @@ lemma PrePostE_option_cases[PrePostE_compositeI]: 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_sum_cases[PrePostE_compositeI]: + assumes "\<And>a. PrePostE (Pl a) (l a) Q E" and "\<And>b. PrePostE (Pr b) (r b) Q E" + shows "PrePostE (case x of Inl a \<Rightarrow> Pl a | Inr b \<Rightarrow> Pr b) (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b) Q E" + using assms by (auto split: sum.splits) + lemma PrePostE_let[PrePostE_compositeI]: assumes "PrePostE P (m y) Q E" shows "PrePostE P (let x = y in m x) Q E" @@ -347,10 +373,51 @@ 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_maybe_failS[PrePostE_atomI]: + "PrePostE (\<lambda>s. case v of Some v \<Rightarrow> Q v s | None \<Rightarrow> E (Failure msg) s) (maybe_failS msg v) Q E" + by (auto simp: maybe_failS_def split: option.splits) + +lemma PrePostE_exitS[PrePostE_atomI, intro]: "PrePostE (E (Failure ''exit'')) (exitS msg) Q E" + unfolding exitS_def PrePostE_def PrePost_def failS_def by auto + 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) +lemma PrePostE_throwS[PrePostE_atomI]: "PrePostE (E (Throw e)) (throwS e) Q E" + by (intro PrePostE_I) (auto simp: throwS_def) + +lemma PrePostE_try_catchS[PrePostE_compositeI]: + assumes Ph: "\<And>s e s'. (Ex (Throw e), s') \<in> m s \<Longrightarrow> PrePostE (Ph e) (h e) Q E" + and m: "PrePostE P m Q (\<lambda>ex. case ex of Throw e \<Rightarrow> Ph e | Failure msg \<Rightarrow> E (Failure msg))" + shows "PrePostE P (try_catchS m h) Q E" + unfolding PrePostE_def +proof (intro PrePostI) + fix s r s' + assume "(r, s') \<in> try_catchS m h s" and P: "P s" + then show "(case r of Value a \<Rightarrow> Q a | result.Ex e \<Rightarrow> E e) s'" using m + proof (cases rule: try_catchS_cases) + case (h e s'') + then have "Ph e s''" using P m by (auto elim!: PrePostE_elim) + then show ?thesis using Ph[OF h(1)] h(2) by (auto elim!: PrePostE_elim) + qed (auto elim!: PrePostE_elim) +qed + +lemma PrePostE_catch_early_returnS[PrePostE_compositeI]: + assumes "PrePostE P m Q (\<lambda>ex. case ex of Throw (Inl a) \<Rightarrow> Q a | Throw (Inr e) \<Rightarrow> E (Throw e) | Failure msg \<Rightarrow> E (Failure msg))" + shows "PrePostE P (catch_early_returnS m) Q E" + unfolding catch_early_returnS_def + by (rule PrePostE_try_catchS, rule PrePostE_sum_cases[OF PrePostE_returnS PrePostE_throwS]) + (auto intro: assms) + +lemma PrePostE_early_returnS[PrePostE_atomI]: "PrePostE (E (Throw (Inl r))) (early_returnS r) Q E" + by (auto simp: early_returnS_def intro: PrePostE_throwS) + +lemma PrePostE_liftRS[PrePostE_compositeI]: + assumes "PrePostE P m Q (\<lambda>ex. case ex of Throw e \<Rightarrow> E (Throw (Inr e)) | Failure msg \<Rightarrow> E (Failure msg))" + shows "PrePostE P (liftRS m) Q E" + using assms unfolding liftRS_def by (intro PrePostE_try_catchS[OF PrePostE_throwS]) + lemma PrePostE_foreachS_Cons: assumes "\<And>s vars' s'. (Value vars', s') \<in> body x vars s \<Longrightarrow> PrePostE (Q vars') (foreachS xs vars' body) Q E" and "PrePostE (Q vars) (body x vars) Q E" @@ -363,6 +430,70 @@ lemma PrePostE_foreachS_invariant: using assms unfolding PrePostE_def by (intro PrePost_foreachS_invariant[THEN PrePost_strengthen_pre]) auto +lemma PrePostE_untilS: + assumes dom: "\<And>s. Inv Q vars s \<Longrightarrow> untilS_dom (vars, cond, body, s)" + and cond: "\<And>vars. PrePostE (Inv' Q vars) (cond vars) (\<lambda>c s'. Inv Q vars s' \<and> (c \<longrightarrow> Q vars s')) E" + and body: "\<And>vars. PrePostE (Inv Q vars) (body vars) (Inv' Q) E" + shows "PrePostE (Inv Q vars) (untilS vars cond body) Q E" +proof (unfold PrePostE_def, rule PrePostI) + fix s r s' + assume Inv_s: "Inv Q vars s" and r: "(r, s') \<in> untilS vars cond body s" + with dom[OF Inv_s] cond body + show "(case r of Value a \<Rightarrow> Q a | result.Ex e \<Rightarrow> E e) s'" + proof (induction vars cond body s rule: untilS.pinduct[case_names Step]) + case (Step vars cond body s) + consider + (Value) vars' c sb sc where "(Value vars', sb) \<in> body vars s" and "(Value c, sc) \<in> cond vars' sb" + and "if c then r = Value vars' \<and> s' = sc else (r, s') \<in> untilS vars' cond body sc" + | (Ex) e where "(Ex e, s') \<in> bindS (body vars) cond s" and "r = Ex e" + using Step(1,6) + by (auto simp: untilS.psimps returnS_def Ex_bindS_iff elim!: bindS_cases split: if_splits; fastforce) + then show ?case + proof cases + case Value + then show ?thesis using Step.IH[OF Value(1,2) _ Step(3,4)] Step(3,4,5) + by (auto split: if_splits elim: PrePostE_elim) + next + case Ex + then show ?thesis using Step(3,4,5) by (auto elim!: bindS_cases PrePostE_elim) + qed + qed +qed + +lemma PrePostE_untilS_pure_cond: + assumes dom: "\<And>s. Inv Q vars s \<Longrightarrow> untilS_dom (vars, returnS \<circ> cond, body, s)" + and body: "\<And>vars. PrePostE (Inv Q vars) (body vars) (\<lambda>vars' s'. Inv Q vars' s' \<and> (cond vars' \<longrightarrow> Q vars' s')) E" + shows "PrePostE (Inv Q vars) (untilS vars (returnS \<circ> cond) body) Q E" + using assms by (intro PrePostE_untilS) (auto simp: comp_def) + +lemma PrePostE_liftState_untilM: + assumes dom: "\<And>s. Inv Q vars s \<Longrightarrow> untilM_dom (vars, cond, body)" + and cond: "\<And>vars. PrePostE (Inv' Q vars) (liftState r (cond vars)) (\<lambda>c s'. Inv Q vars s' \<and> (c \<longrightarrow> Q vars s')) E" + and body: "\<And>vars. PrePostE (Inv Q vars) (liftState r (body vars)) (Inv' Q) E" + shows "PrePostE (Inv Q vars) (liftState r (untilM vars cond body)) Q E" +proof - + have domS: "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" if "Inv Q vars s" for s + using dom that by (intro untilM_dom_untilS_dom) + then have "PrePostE (Inv Q vars) (untilS vars (liftState r \<circ> cond) (liftState r \<circ> body)) Q E" + using cond body by (auto intro: PrePostE_untilS simp: comp_def) + moreover have "liftState r (untilM vars cond body) s = untilS vars (liftState r \<circ> cond) (liftState r \<circ> body) s" + if "Inv Q vars s" for s + unfolding liftState_untilM[OF domS[OF that] dom[OF that]] .. + ultimately show ?thesis by (auto cong: PrePostE_cong) +qed + +lemma PrePostE_liftState_untilM_pure_cond: + assumes dom: "\<And>s. Inv Q vars s \<Longrightarrow> untilM_dom (vars, return \<circ> cond, body)" + and body: "\<And>vars. PrePostE (Inv Q vars) (liftState r (body vars)) (\<lambda>vars' s'. Inv Q vars' s' \<and> (cond vars' \<longrightarrow> Q vars' s')) E" + shows "PrePostE (Inv Q vars) (liftState r (untilM vars (return \<circ> cond) body)) Q E" + using assms by (intro PrePostE_liftState_untilM) (auto simp: comp_def liftState_simp) + +lemma PrePostE_undefined_boolS[PrePostE_atomI]: + "PrePostE (\<lambda>s. \<forall>b. Q b s) + (undefined_boolS unit) Q E" + unfolding undefined_boolS_def seqS_def + by (auto intro: PrePostE_strengthen_pre PrePostE_chooseS) + lemma PrePostE_bool_of_bitU_nondetS_any: "PrePostE (\<lambda>s. \<forall>b. Q b s) (bool_of_bitU_nondetS b) Q E" unfolding bool_of_bitU_nondetS_def undefined_boolS_def diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy index 2a6272c2..fd54c93a 100644 --- a/lib/isabelle/Sail2_operators_mwords_lemmas.thy +++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy @@ -78,6 +78,57 @@ lemma len_of_minus_One_minus_nonneg_lt_len_of[simp]: "n \<ge> 0 \<Longrightarrow> nat (int LENGTH('a::len) - 1 - n) < LENGTH('a)" by (metis diff_mono diff_zero len_gt_0 nat_eq_iff2 nat_less_iff order_refl zle_diff1_eq) +declare subrange_vec_dec_def[simp] + +lemma update_subrange_vec_dec_update_subrange_list_dec: + assumes "0 \<le> j" and "j \<le> i" and "i < int LENGTH('a)" + shows "update_subrange_vec_dec (w :: 'a::len word) i j w' = + of_bl (update_subrange_list_dec (to_bl w) i j (to_bl w'))" + using assms + unfolding update_subrange_vec_dec_def update_subrange_list_dec_def update_subrange_list_inc_def + by (auto simp: word_update_def split_at_def Let_def nat_diff_distrib min_def) + +lemma subrange_vec_dec_subrange_list_dec: + assumes "0 \<le> j" and "j \<le> i" and "i < int LENGTH('a)" and "int LENGTH('b) = i - j + 1" + shows "subrange_vec_dec (w :: 'a::len word) i j = (of_bl (subrange_list_dec (to_bl w) i j) :: 'b::len word)" + using assms unfolding subrange_vec_dec_def + by (auto simp: subrange_list_dec_drop_take slice_take of_bl_drop') + +lemma slice_simp[simp]: "slice w lo len = Word.slice (nat lo) w" + by (auto simp: slice_def) + +declare slice_id[simp] + +lemma of_bools_of_bl[simp]: "of_bools_method BC_mword = of_bl" + by (auto simp: BC_mword_defs) + +lemma of_bl_bin_word_of_int: + "len = LENGTH('a) \<Longrightarrow> of_bl (bin_to_bl_aux len n []) = (word_of_int n :: ('a::len) word)" + by (auto simp: of_bl_def bin_bl_bin') + +lemma get_slice_int_0_bin_to_bl[simp]: + "len > 0 \<Longrightarrow> get_slice_int len n 0 = of_bl (bin_to_bl (nat len) n)" + unfolding get_slice_int_def get_slice_int_bv_def subrange_list_def + by (auto simp: subrange_list_dec_drop_take len_bin_to_bl_aux) + +lemma to_bl_of_bl[simp]: + fixes bl :: "bool list" + defines w: "w \<equiv> of_bl bl :: 'a::len word" + assumes len: "length bl = LENGTH('a)" + shows "to_bl w = bl" + using len unfolding w by (intro word_bl.Abs_inverse) auto + +lemma reverse_endianness_byte[simp]: + "LENGTH('a) = 8 \<Longrightarrow> reverse_endianness (w :: 'a::len word) = w" + unfolding reverse_endianness_def by (auto simp: reverse_endianness_list_simps) + +lemma reverse_reverse_endianness[simp]: + "8 dvd LENGTH('a) \<Longrightarrow> reverse_endianness (reverse_endianness w) = (w :: 'a::len word)" + unfolding reverse_endianness_def by (simp) + +lemma replicate_bits_zero[simp]: "replicate_bits 0 n = 0" + by (intro word_eqI) (auto simp: replicate_bits_def test_bit_of_bl rev_nth nth_repeat simp del: repeat.simps) + declare extz_vec_def[simp] declare exts_vec_def[simp] declare concat_vec_def[simp] @@ -109,4 +160,10 @@ lemma arith_vec_int_simps[simp]: unfolding add_vec_int_def sub_vec_int_def mult_vec_int_def by (auto simp: arith_op_bv_int_def BC_mword_defs word_add_def word_sub_wi word_mult_def) +lemma shiftl_simp[simp]: "shiftl w l = w << (nat l)" + by (auto simp: shiftl_def shiftl_mword_def) + +lemma shiftr_simp[simp]: "shiftr w l = w >> (nat l)" + by (auto simp: shiftr_def shiftr_mword_def) + end diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy index 3ca1729f..25eb9f52 100644 --- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy +++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy @@ -129,6 +129,16 @@ lemma bind_T_cases: | (Bind) m' where "s' = bind m' f" and "(m, e, m') \<in> T" using assms by (cases; blast elim: bind.elims) +lemma Run_bindI: + fixes m :: "('r, 'a, 'e) monad" + assumes "Run m t1 a1" + and "Run (f a1) t2 a2" + shows "Run (m \<bind> f) (t1 @ t2) a2" +proof (use assms in \<open>induction m t1 "Done a1 :: ('r, 'a, 'e) monad" rule: Traces.induct\<close>) + case (Step s e s'' t) + then show ?case by (elim T.cases) auto +qed auto + lemma Run_bindE: fixes m :: "('rv, 'b, 'e) monad" and a :: 'a assumes "Run (bind m f) t a" @@ -161,6 +171,31 @@ lemma Run_DoneE: lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a" by (auto elim: Run_DoneE) +lemma Run_bindE_ignore_trace: + assumes "Run (m \<bind> f) t a" + obtains tm tf am where "Run m tm am" and "Run (f am) tf a" + using assms by (elim Run_bindE) + +lemma Run_letE: + assumes "Run (let x = y in f x) t a" + obtains "Run (f y) t a" + using assms by auto + +lemma Run_ifE: + assumes "Run (if b then f else g) t a" + obtains "b" and "Run f t a" | "\<not>b" and "Run g t a" + using assms by (auto split: if_splits) + +lemma Run_returnE: + assumes "Run (return x) t a" + obtains "t = []" and "a = x" + using assms by (auto simp: return_def) + +lemma Run_early_returnE: + assumes "Run (early_return x) t a" + shows P + using assms by (auto simp: early_return_def throw_def elim: Traces_cases) + lemma bind_cong[fundef_cong]: assumes m: "m1 = m2" and f: "\<And>t a. Run m2 t a \<Longrightarrow> f1 a = f2 a" @@ -168,4 +203,10 @@ lemma bind_cong[fundef_cong]: unfolding m using f by (induction m2 f1 arbitrary: f2 rule: bind.induct; unfold bind.simps; blast) +lemma liftR_read_reg[simp]: "liftR (read_reg reg) = read_reg reg" by (auto simp: read_reg_def liftR_def split: option.splits) +lemma try_catch_return[simp]: "try_catch (return x) h = return x" by (auto simp: return_def) +lemma liftR_return[simp]: "liftR (return x) = return x" by (auto simp: liftR_def) +lemma liftR_undefined_bool[simp]: "liftR (undefined_bool ()) = undefined_bool ()" by (auto simp: undefined_bool_def liftR_def) +lemma assert_exp_True_return[simp]: "assert_exp True msg = return ()" by (auto simp: assert_exp_def return_def) + end diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index 8f04e850..ba69d0d8 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -23,21 +23,13 @@ lemma Value_liftState_Run: lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra] -lemma member_set_nth: - assumes "x \<in> set xs" - obtains n where "x = xs ! n" and "n < length xs" -proof (use assms in \<open>induction xs arbitrary: thesis\<close>) - case (Cons a xs) print_cases - show ?case proof cases - assume "x = a" - then show ?thesis using Cons(2)[where n = 0] Cons(3) by auto - next - assume "x \<noteq> a" - then obtain n where "x = xs ! n" and "n < length xs" using Cons by auto - then show ?thesis using Cons(2)[of "Suc n"] by auto - qed -qed auto +lemma Value_bindS_iff: + "(Value b, s'') \<in> bindS m f s \<longleftrightarrow> (\<exists>a s'. (Value a, s') \<in> m s \<and> (Value b, s'') \<in> f a s')" + by (auto elim!: bindS_cases intro: bindS_intros) +lemma Ex_bindS_iff: + "(Ex e, s'') \<in> bindS m f s \<longleftrightarrow> (Ex e, s'') \<in> m s \<or> (\<exists>a s'. (Value a, s') \<in> m s \<and> (Ex e, s'') \<in> f a s')" + by (auto elim!: bindS_cases intro: bindS_intros) lemma liftState_throw[liftState_simp]: "liftState r (throw e) = throwS e" by (auto simp: throw_def) @@ -67,7 +59,7 @@ lemma liftState_try_catch[liftState_simp]: by (induction m h rule: try_catch_induct) (auto simp: try_catchS_bindS_no_throw) lemma liftState_early_return[liftState_simp]: - "liftState r (early_return r) = early_returnS r" + "liftState r (early_return x) = early_returnS x" by (auto simp: early_return_def early_returnS_def liftState_simp) lemma liftState_catch_early_return[liftState_simp]: @@ -158,6 +150,68 @@ lemma liftState_internal_pick[liftState_simp]: simp del: repeat.simps cong: option.case_cong) +lemma liftRS_returnS[simp]: "liftRS (returnS x) = returnS x" + by (auto simp: liftRS_def) + +lemma liftRS_bindS: + fixes m :: "('regs, 'a, 'e) monadS" and f :: "'a \<Rightarrow> ('regs, 'b, 'e) monadS" + shows "(liftRS (bindS m f) :: ('regs, 'b, 'r, 'e) monadRS) = bindS (liftRS m) (liftRS \<circ> f)" +proof (intro ext set_eqI iffI) + fix s and rs' :: "('b, 'r + 'e) result \<times> 'regs sequential_state" + assume lhs: "rs' \<in> liftRS (bindS m f) s" + then show "rs' \<in> bindS (liftRS m) (liftRS \<circ> f) s" + by (cases rs') + (fastforce simp: liftRS_def throwS_def elim!: bindS_cases try_catchS_cases + intro: bindS_intros try_catchS_intros) +next + fix s and rs' :: "('b, 'r + 'e) result \<times> 'regs sequential_state" + assume "rs' \<in> bindS (liftRS m) (liftRS \<circ> f) s" + then show "rs' \<in> liftRS (bindS m f) s" + by (cases rs') + (fastforce simp: liftRS_def throwS_def elim!: bindS_cases try_catchS_cases + intro: bindS_intros try_catchS_intros) +qed + +lemma liftRS_assert_expS_True[simp]: "liftRS (assert_expS True msg) = returnS ()" + by (auto simp: liftRS_def assert_expS_def) + +lemma untilM_domI: + fixes V :: "'vars \<Rightarrow> nat" + assumes "Inv vars" + and "\<And>vars t vars' t'. \<lbrakk>Inv vars; Run (body vars) t vars'; Run (cond vars') t' False\<rbrakk> \<Longrightarrow> V vars' < V vars \<and> Inv vars'" + shows "untilM_dom (vars, cond, body)" + using assms + by (induction vars rule: measure_induct_rule[where f = V]) + (auto intro: untilM.domintros) + +lemma untilM_dom_untilS_dom: + assumes "untilM_dom (vars, cond, body)" + shows "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" + using assms + by (induction vars cond body arbitrary: s rule: untilM.pinduct) + (rule untilS.domintros, auto elim!: Value_liftState_Run) + +lemma measure2_induct: + fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> nat" + assumes "\<And>x1 y1. (\<And>x2 y2. f x2 y2 < f x1 y1 \<Longrightarrow> P x2 y2) \<Longrightarrow> P x1 y1" + shows "P x y" +proof - + have "P (fst x) (snd x)" for x + by (induction x rule: measure_induct_rule[where f = "\<lambda>x. f (fst x) (snd x)"]) (auto intro: assms) + then show ?thesis by auto +qed + +lemma untilS_domI: + fixes V :: "'vars \<Rightarrow> 'regs sequential_state \<Rightarrow> nat" + assumes "Inv vars s" + and "\<And>vars s vars' s' s''. + \<lbrakk>Inv vars s; (Value vars', s') \<in> body vars s; (Value False, s'') \<in> cond vars' s'\<rbrakk> + \<Longrightarrow> V vars' s'' < V vars s \<and> Inv vars' s''" + shows "untilS_dom (vars, cond, body, s)" + using assms + by (induction vars s rule: measure2_induct[where f = V]) + (auto intro: untilS.domintros) + lemma whileS_dom_step: assumes "whileS_dom (vars, cond, body, s)" and "(Value True, s') \<in> cond vars s" @@ -262,6 +316,9 @@ lemma and_boolM_return_if: "and_boolM (return b) y = (if b then y else return False)" by (auto simp: and_boolM_def) +lemma and_boolM_return_return_and[simp]: "and_boolM (return l) (return r) = return (l \<and> r)" + 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]: @@ -275,6 +332,9 @@ lemma or_boolM_return_if: "or_boolM (return b) y = (if b then return True else y)" by (auto simp: or_boolM_def) +lemma or_boolM_return_return_or[simp]: "or_boolM (return l) (return r) = return (l \<or> r)" + 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 @@ -292,8 +352,12 @@ lemma and_boolS_returnS_if: lemmas and_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolS x y" for y] +lemma and_boolS_returnS_True[simp]: "and_boolS (returnS True) c = c" + by (auto simp: and_boolS_def) + lemma or_boolS_simps[simp]: "or_boolS (returnS b) (returnS c) = returnS (b \<or> c)" + "or_boolS (returnS False) m = m" "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))" @@ -305,4 +369,19 @@ lemma or_boolS_returnS_if: lemmas or_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolS x y" for y] +lemma Run_or_boolM_E: + assumes "Run (or_boolM l r) t a" + obtains "Run l t True" and "a" + | tl tr where "Run l tl False" and "Run r tr a" and "t = tl @ tr" + using assms by (auto simp: or_boolM_def elim!: Run_bindE Run_ifE Run_returnE) + +lemma Run_and_boolM_E: + assumes "Run (and_boolM l r) t a" + obtains "Run l t False" and "\<not>a" + | tl tr where "Run l tl True" and "Run r tr a" and "t = tl @ tr" + using assms by (auto simp: and_boolM_def elim!: Run_bindE Run_ifE Run_returnE) + +lemma maybe_failS_Some[simp]: "maybe_failS msg (Some v) = returnS v" + by (auto simp: maybe_failS_def) + end diff --git a/lib/isabelle/Sail2_values_lemmas.thy b/lib/isabelle/Sail2_values_lemmas.thy index b50d8942..576cd8ea 100644 --- a/lib/isabelle/Sail2_values_lemmas.thy +++ b/lib/isabelle/Sail2_values_lemmas.thy @@ -2,18 +2,135 @@ theory Sail2_values_lemmas imports Sail2_values begin +lemma while_domI: + fixes V :: "'vars \<Rightarrow> nat" + assumes "\<And>vars. cond vars \<Longrightarrow> V (body vars) < V vars" + shows "while_dom (vars, cond, body)" + by (induction vars rule: measure_induct_rule[where f = V]) + (use assms in \<open>auto intro: while.domintros\<close>) + lemma nat_of_int_nat_simps[simp]: "nat_of_int = nat" by (auto simp: nat_of_int_def) termination reverse_endianness_list by (lexicographic_order simp add: drop_list_def) +declare reverse_endianness_list.simps[simp del] +declare take_list_def[simp] +declare drop_list_def[simp] + +function take_chunks :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where + "take_chunks n [] = []" +| "take_chunks 0 xs = []" +| "take_chunks n xs = take n xs # take_chunks n (drop n xs)" if "n > 0" and "xs \<noteq> []" + by auto blast +termination by lexicographic_order + +lemma take_chunks_length_leq_n: "length xs \<le> n \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> take_chunks n xs = [xs]" + by (cases n) auto + +lemma take_chunks_append: "n dvd length a \<Longrightarrow> take_chunks n (a @ b) = take_chunks n a @ take_chunks n b" + by (induction n a rule: take_chunks.induct) (auto simp: dvd_imp_le) + +lemma Suc8_plus8: "Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc x))))))) = 8 + x" + by auto + +lemma byte_chunks_take_chunks_8: + assumes "8 dvd length xs" + shows "byte_chunks xs = Some (take_chunks 8 xs)" +proof - + have Suc8_plus8: "Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc x))))))) = 8 + x" for x + by auto + from assms show ?thesis + by (induction xs rule: byte_chunks.induct) (auto simp: Suc8_plus8 nat_dvd_not_less) +qed + +lemma reverse_endianness_list_rev_take_chunks: + "reverse_endianness_list bits = List.concat (rev (take_chunks 8 bits))" + by (induction "8 :: nat" bits rule: take_chunks.induct) + (auto simp: reverse_endianness_list.simps) + +lemma reverse_endianness_list_simps: + "length bits \<le> 8 \<Longrightarrow> reverse_endianness_list bits = bits" + "length bits > 8 \<Longrightarrow> reverse_endianness_list bits = reverse_endianness_list (drop 8 bits) @ take 8 bits" + by (cases bits; auto simp: reverse_endianness_list_rev_take_chunks)+ + +lemma reverse_endianness_list_append: + assumes "8 dvd length a" + shows "reverse_endianness_list (a @ b) = reverse_endianness_list b @ reverse_endianness_list a" + using assms by (auto simp: reverse_endianness_list_rev_take_chunks take_chunks_append) + +lemma length_reverse_endianness_list[simp]: + "length (reverse_endianness_list l) = length l" + by (induction l rule: reverse_endianness_list.induct) (auto simp: reverse_endianness_list.simps) + +lemma reverse_endianness_list_take_8[simp]: + "reverse_endianness_list (take 8 bits) = take 8 bits" + by (auto simp: reverse_endianness_list_simps) + +lemma reverse_reverse_endianness_list[simp]: + assumes "8 dvd length l" + shows "reverse_endianness_list (reverse_endianness_list l) = l" +proof (use assms in \<open>induction l rule: reverse_endianness_list.induct[case_names Step]\<close>) + case (Step bits) + then show ?case + by (auto simp: reverse_endianness_list.simps[of bits] reverse_endianness_list_append) +qed + +declare repeat.simps[simp del] + +lemma length_repeat[simp]: "length (repeat xs n) = nat n * length xs" +proof (induction xs n rule: repeat.induct[case_names Step]) + case (Step xs n) + then show ?case unfolding repeat.simps[of xs n] + by (auto simp del: mult_Suc simp: mult_Suc[symmetric]) +qed + +lemma nth_repeat: + assumes "i < nat n * length xs" + shows "repeat xs n ! i = xs ! (i mod length xs)" +proof (use assms in \<open>induction xs n arbitrary: i rule: repeat.induct[case_names Step]\<close>) + case (Step xs n i) + show ?case + using Step.prems Step.IH[of "i - length xs"] + unfolding repeat.simps[of xs n] + by (auto simp: nth_append mod_geq[symmetric] nat_diff_distrib diff_mult_distrib) +qed termination index_list by (relation "measure (\<lambda>(i, j, step). nat ((j - i + step) * sgn step))") auto +lemma index_list_Zero[simp]: "index_list i j 0 = []" + by auto + +lemma index_list_singleton[simp]: "n \<noteq> 0 \<Longrightarrow> index_list i i n = [i]" + by auto + +lemma index_list_simps: + "0 < step \<Longrightarrow> from \<le> to \<Longrightarrow> index_list from to step = from # index_list (from + step) to step" + "0 < step \<Longrightarrow> from > to \<Longrightarrow> index_list from to step = []" + "0 > step \<Longrightarrow> from \<ge> to \<Longrightarrow> index_list from to step = from # index_list (from + step) to step" + "0 > step \<Longrightarrow> from < to \<Longrightarrow> index_list from to step = []" + by auto + +lemma index_list_step1_upto[simp]: "index_list i j 1 = [i..j]" + by (induction i j "1 :: int" rule: index_list.induct) + (auto simp: index_list_simps upto.simps) + +lemma length_upto[simp]: "i \<le> j \<Longrightarrow> length [i..j] = nat (j - i + 1)" + by (induction i j rule: upto.induct) (auto simp: upto.simps) + +lemma nth_upto[simp]: "i + int n \<le> j \<Longrightarrow> [i..j] ! n = i + int n" + by (induction i j arbitrary: n rule: upto.induct) + (auto simp: upto.simps nth_Cons split: nat.splits) + +declare index_list.simps[simp del] + lemma just_list_map_Some[simp]: "just_list (map Some v) = Some v" by (induction v) auto lemma just_list_None_iff[simp]: "just_list xs = None \<longleftrightarrow> None \<in> set xs" by (induction xs) (auto split: option.splits) +lemma just_list_None_member_None: "None \<in> set xs \<Longrightarrow> just_list xs = None" + by auto + lemma just_list_Some_iff[simp]: "just_list xs = Some ys \<longleftrightarrow> xs = map Some ys" by (induction xs arbitrary: ys) (auto split: option.splits) @@ -28,10 +145,10 @@ lemma repeat_singleton_replicate[simp]: proof (induction n) case (nonneg n) have "nat (1 + int m) = Suc m" for m by auto - then show ?case by (induction n) auto + then show ?case by (induction n) (auto simp: repeat.simps) next case (neg n) - then show ?case by auto + then show ?case by (auto simp: repeat.simps) qed lemma bool_of_bitU_simps[simp]: @@ -102,6 +219,15 @@ lemma unsigned_bits_of_mword[simp]: "unsigned_method BC_bitU_list (bits_of_method BC_mword a) = Some (uint a)" by (auto simp: BC_bitU_list_def BC_mword_defs unsigned_of_bits_def unsigned_of_bools_def) +definition mem_bytes_of_word :: "'a::len word \<Rightarrow> bitU list list" where + "mem_bytes_of_word w = rev (take_chunks 8 (map bitU_of_bool (to_bl w)))" + +lemma mem_bytes_of_bits_mem_bytes_of_word[simp]: + assumes "8 dvd LENGTH('a)" + shows "mem_bytes_of_bits BC_mword (w :: 'a::len word) = Some (mem_bytes_of_word w)" + using assms + by (auto simp: mem_bytes_of_bits_def bytes_of_bits_def BC_mword_defs byte_chunks_take_chunks_8 mem_bytes_of_word_def) + lemma bits_of_bitU_list[simp]: "bits_of_method BC_bitU_list v = v" "of_bits_method BC_bitU_list v = Some v" @@ -158,6 +284,14 @@ lemma update_list_dec_update[simp]: "update_list_dec xs n x = xs[length xs - nat (n + 1) := x]" by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int) +lemma update_list_dec_update_rev: + "0 \<le> n \<Longrightarrow> nat n < length xs \<Longrightarrow> update_list_dec xs n x = rev ((rev xs)[nat n := x])" + by (auto simp: update_list_dec_def add.commute diff_diff_add nat_minus_as_int rev_update) + +lemma access_list_dec_update_list_dec[simp]: + "0 \<le> n \<Longrightarrow> nat n < length xs \<Longrightarrow> access_list_dec (update_list_dec xs n x) n = x" + by (auto simp: access_list_dec_rev_nth update_list_dec_update_rev) + lemma bools_of_nat_aux_simps[simp]: "\<And>len. len \<le> 0 \<Longrightarrow> bools_of_nat_aux len x acc = acc" "\<And>len. bools_of_nat_aux (int (Suc len)) x acc = @@ -200,7 +334,7 @@ proof (induction len arbitrary: n acc) qed auto lemma bools_of_int_bin_to_bl[simp]: - "bools_of_int (int len) n = bin_to_bl len n" + "bools_of_int len n = bin_to_bl (nat len) n" by (auto simp: bools_of_int_def Let_def map_Not_bin_to_bl rbl_succ[unfolded bin_to_bl_def]) end |