diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Sail2_state_lemmas.thy | 121 | ||||
| -rw-r--r-- | lib/isabelle/Sail2_values_lemmas.thy | 28 |
2 files changed, 148 insertions, 1 deletions
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy index edcd9593..c7d55d31 100644 --- a/lib/isabelle/Sail2_state_lemmas.thy +++ b/lib/isabelle/Sail2_state_lemmas.thy @@ -2,6 +2,8 @@ theory Sail2_state_lemmas imports Sail2_state Sail2_state_lifting begin +text \<open>Monad lifting\<close> + lemma All_liftState_dom: "liftState_dom (r, m)" by (induction m) (auto intro: liftState.domintros) termination liftState using All_liftState_dom by auto @@ -309,7 +311,7 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState qed auto qed -(* Simplification rules for monadic Boolean connectives *) +text \<open>Simplification rules for monadic Boolean connectives\<close> lemma if_return_return[simp]: "(if a then return True else return False) = return a" by auto @@ -392,4 +394,121 @@ lemma Run_and_boolM_E: lemma maybe_failS_Some[simp]: "maybe_failS msg (Some v) = returnS v" by (auto simp: maybe_failS_def) +text \<open>Event traces\<close> + +lemma Some_eq_bind_conv: "Some x = Option.bind f g \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)" + unfolding bind_eq_Some_conv[symmetric] by auto + +lemma if_then_Some_eq_Some: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)" + by auto + +lemma emitEventS_update_cases: + assumes "emitEventS ra e s = Some s'" + obtains + (Write_mem) wk addr sz v tag r + where "e = E_write_mem wk addr sz v tag r" + and "s' = put_mem_bytes addr sz v tag s" + | (Write_reg) r v rs' + where "e = E_write_reg r v" and "(snd ra) r v (regstate s) = Some rs'" + and "s' = s\<lparr>regstate := rs'\<rparr>" + | (Read) "s' = s" + using assms + by (elim emitEventS.elims) (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some) + +lemma runTraceS_singleton[simp]: "runTraceS ra [e] s = emitEventS ra e s" + by (cases "emitEventS ra e s"; auto) + +lemma runTraceS_ConsE: + assumes "runTraceS ra (e # t) s = Some s'" + obtains s'' where "emitEventS ra e s = Some s''" and "runTraceS ra t s'' = Some s'" + using assms by (auto simp: bind_eq_Some_conv) + +lemma runTraceS_ConsI: + assumes "emitEventS ra e s = Some s'" and "runTraceS ra t s' = Some s''" + shows "runTraceS ra (e # t) s = Some s''" + using assms by auto + +lemma runTraceS_Cons_tl: + assumes "emitEventS ra e s = Some s'" + shows "runTraceS ra (e # t) s = runTraceS ra t s'" + using assms by (elim emitEventS.elims) (auto simp: Some_eq_bind_conv bind_eq_Some_conv) + +lemma runTraceS_appendE: + assumes "runTraceS ra (t @ t') s = Some s'" + obtains s'' where "runTraceS ra t s = Some s''" and "runTraceS ra t' s'' = Some s'" +proof - + have "\<exists>s''. runTraceS ra t s = Some s'' \<and> runTraceS ra t' s'' = Some s'" + proof (use assms in \<open>induction t arbitrary: s\<close>) + case (Cons e t) + from Cons.prems + obtain s_e where "emitEventS ra e s = Some s_e" and "runTraceS ra (t @ t') s_e = Some s'" + by (auto elim: runTraceS_ConsE simp: bind_eq_Some_conv) + with Cons.IH[of s_e] show ?case by (auto intro: runTraceS_ConsI) + qed auto + then show ?thesis using that by blast +qed + +lemma runTraceS_nth_split: + assumes "runTraceS ra t s = Some s'" and n: "n < length t" + obtains s1 s2 where "runTraceS ra (take n t) s = Some s1" + and "emitEventS ra (t ! n) s1 = Some s2" + and "runTraceS ra (drop (Suc n) t) s2 = Some s'" +proof - + have "runTraceS ra (take n t @ t ! n # drop (Suc n) t) s = Some s'" + using assms + by (auto simp: id_take_nth_drop[OF n, symmetric]) + then show thesis by (blast elim: runTraceS_appendE runTraceS_ConsE intro: that) +qed + +text \<open>Memory accesses\<close> + +lemma get_mem_bytes_put_mem_bytes_same_addr: + assumes "length v = sz" + shows "get_mem_bytes addr sz (put_mem_bytes addr sz v tag s) = Some (v, if sz > 0 then tag else B1)" +proof (unfold assms[symmetric], induction v rule: rev_induct) + case Nil + then show ?case by (auto simp: get_mem_bytes_def) +next + case (snoc x xs) + then show ?case + by (cases tag) + (auto simp: get_mem_bytes_def put_mem_bytes_def Let_def and_bit_eq_iff foldl_and_bit_eq_iff + cong: option.case_cong split: if_splits option.splits) +qed + +lemma memstate_put_mem_bytes: + assumes "length v = sz" + shows "memstate (put_mem_bytes addr sz v tag s) addr' = + (if addr' \<in> {addr..<addr+sz} then Some (v ! (addr' - addr)) else memstate s addr')" + unfolding assms[symmetric] + by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def) + +lemma tagstate_put_mem_bytes: + assumes "length v = sz" + shows "tagstate (put_mem_bytes addr sz v tag s) addr' = + (if addr' \<in> {addr..<addr+sz} then Some tag else tagstate s addr')" + unfolding assms[symmetric] + by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def) + +lemma get_mem_bytes_cong: + assumes "\<forall>addr'. addr \<le> addr' \<and> addr' < addr + sz \<longrightarrow> + (memstate s' addr' = memstate s addr' \<and> tagstate s' addr' = tagstate s addr')" + shows "get_mem_bytes addr sz s' = get_mem_bytes addr sz s" +proof (use assms in \<open>induction sz\<close>) + case 0 + then show ?case by (auto simp: get_mem_bytes_def) +next + case (Suc sz) + then show ?case + by (auto simp: get_mem_bytes_def Let_def + intro!: map_option_cong map_cong foldl_cong + arg_cong[where f = just_list] arg_cong2[where f = and_bit]) +qed + +lemma get_mem_bytes_tagged_tagstate: + assumes "get_mem_bytes addr sz s = Some (v, B1)" + shows "\<forall>addr' \<in> {addr..<addr + sz}. tagstate s addr' = Some B1" + using assms + by (auto simp: get_mem_bytes_def foldl_and_bit_eq_iff Let_def split: option.splits) + end diff --git a/lib/isabelle/Sail2_values_lemmas.thy b/lib/isabelle/Sail2_values_lemmas.thy index 576cd8ea..27a6952f 100644 --- a/lib/isabelle/Sail2_values_lemmas.thy +++ b/lib/isabelle/Sail2_values_lemmas.thy @@ -123,6 +123,9 @@ lemma nth_upto[simp]: "i + int n \<le> j \<Longrightarrow> [i..j] ! n = i + int declare index_list.simps[simp del] +lemma genlist_add_upt[simp]: "genlist ((+) start) len = [start..<start + len]" + by (auto simp: genlist_def map_add_upt add.commute cong: map_cong) + 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" @@ -151,6 +154,31 @@ next then show ?case by (auto simp: repeat.simps) qed +lemma and_bit_B1[simp]: "and_bit B1 b = b" + by (cases b) auto + +lemma and_bit_idem[simp]: "and_bit b b = b" + by (cases b) auto + +lemma and_bit_eq_iff: + "and_bit b b' = B0 \<longleftrightarrow> (b = B0 \<or> b' = B0)" + "and_bit b b' = BU \<longleftrightarrow> (b = BU \<or> b' = BU) \<and> b \<noteq> B0 \<and> b' \<noteq> B0" + "and_bit b b' = B1 \<longleftrightarrow> (b = B1 \<and> b' = B1)" + by (cases b; cases b'; auto)+ + +lemma foldl_and_bit_eq_iff: + shows "foldl and_bit b bs = B0 \<longleftrightarrow> (b = B0 \<or> B0 \<in> set bs)" (is ?B0) + and "foldl and_bit b bs = B1 \<longleftrightarrow> (b = B1 \<and> set bs \<subseteq> {B1})" (is ?B1) + and "foldl and_bit b bs = BU \<longleftrightarrow> (b = BU \<or> BU \<in> set bs) \<and> b \<noteq> B0 \<and> B0 \<notin> set bs" (is ?BU) +proof - + have "?B0 \<and> ?B1 \<and> ?BU" + proof (induction bs arbitrary: b) + case (Cons b' bs) + show ?case using Cons.IH by (cases b; cases b') auto + qed auto + then show ?B0 and ?B1 and ?BU by auto +qed + lemma bool_of_bitU_simps[simp]: "bool_of_bitU B0 = Some False" "bool_of_bitU B1 = Some True" |