diff options
Diffstat (limited to 'lib/isabelle/State_monad_lemmas.thy')
| -rw-r--r-- | lib/isabelle/State_monad_lemmas.thy | 161 |
1 files changed, 42 insertions, 119 deletions
diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy index 291157f5..e7286fcf 100644 --- a/lib/isabelle/State_monad_lemmas.thy +++ b/lib/isabelle/State_monad_lemmas.thy @@ -4,23 +4,15 @@ theory State_monad_lemmas Sail_values_lemmas begin -context +(*context notes returnS_def[simp] and failS_def[simp] and throwS_def[simp] and readS_def[simp] and updateS_def[simp] -begin - -abbreviation "bindS_aux f \<equiv> (\<lambda>r. case r of (Value a, s') \<Rightarrow> f a s' | (Ex e, s') \<Rightarrow> {(Ex e, s')})" -abbreviation "bindS_app ms f \<equiv> \<Union>(bindS_aux f ` ms)" +begin*) lemma bindS_ext_cong[fundef_cong]: assumes m: "m1 s = m2 s" and f: "\<And>a s'. (Value a, s') \<in> (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" shows "bindS m1 f1 s = bindS m2 f2 s" using assms unfolding bindS_def by (auto split: result.splits) -(* proof - - have "bindS_app (m2 s) f1 = bindS_app (m2 s) f2" - using f by (auto split: result.splits) - then show ?thesis using m by (auto simp: bindS_def) -qed *) lemma bindS_cong[fundef_cong]: assumes m: "m1 = m2" @@ -29,21 +21,16 @@ lemma bindS_cong[fundef_cong]: using assms by (intro ext bindS_ext_cong; blast) lemma bindS_returnS_left[simp]: "bindS (returnS x) f = f x" - by (auto simp add: bindS_def) + by (auto simp add: bindS_def returnS_def) lemma bindS_returnS_right[simp]: "bindS m returnS = (m :: ('regs, 'a, 'e) monadS)" - by (intro ext) (auto simp: bindS_def split: result.splits) -(* proof - - have "List.concat (map (bindS_aux returnS) ms) = ms" for ms :: "(('a, 'e) result \<times> 'regs sequential_state) list" - by (induction ms) (auto split: result.splits) - then show ?thesis unfolding bindS_def by blast -qed *) + by (intro ext) (auto simp: bindS_def returnS_def split: result.splits) lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)" - by (auto simp: bindS_def) + by (auto simp: bindS_def readS_def returnS_def) lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))" - by (auto simp: bindS_def) + by (auto simp: bindS_def updateS_def returnS_def) lemma result_cases: @@ -84,17 +71,6 @@ lemma monadS_eqI: shows "m = m'" using assms by (intro ext monadS_ext_eqI) -lemma - assumes "(Value a, s') \<in> bindS m f s" - obtains a' s'' where "(Value a', s'') \<in> m s" and "(Value a, s') \<in> f a' s''" - using assms by (auto simp: bindS_def split: result.splits) - -lemma - assumes "(Ex e, s') \<in> bindS m f s" - obtains (Left) "(Ex e, s') \<in> m s" - | (Right) a s'' where "(Value a, s'') \<in> m s" and "(Ex e, s') \<in> f a s''" - using assms by (auto simp: bindS_def split: result.splits) - lemma bindS_cases: assumes "(r, s') \<in> bindS m f s" obtains (Value) a a' s'' where "r = Value a" and "(Value a', s'') \<in> m s" and "(Value a, s') \<in> f a' s''" @@ -110,15 +86,9 @@ lemma bindS_intros: lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\<lambda>x. bindS (f x) g)" by (auto elim!: bindS_cases intro: bindS_intros monadS_eqI) -(*proof - - have "List.concat (map (bindS_aux g) (List.concat (map (bindS_aux f) xs))) = - List.concat (map (bindS_aux (\<lambda>x s. List.concat (map (bindS_aux g) (f x s)))) xs)" for xs - by (induction xs) (auto split: result.splits) - then show ?thesis unfolding bindS_def by auto -qed*) - -lemma bindS_failS[simp]: "bindS (failS msg) f = failS msg" by (auto simp: bindS_def) -lemma bindS_throwS[simp]: "bindS (throwS e) f = throwS e" by (auto simp: bindS_def) + +lemma bindS_failS[simp]: "bindS (failS msg) f = failS msg" by (auto simp: bindS_def failS_def) +lemma bindS_throwS[simp]: "bindS (throwS e) f = throwS e" by (auto simp: bindS_def throwS_def) declare seqS_def[simp] lemma Value_bindS_elim: @@ -132,18 +102,10 @@ lemma Ex_bindS_elim: | (Right) s'' a' where "(Value a', s'') \<in> m s" and "(Ex e, s') \<in> f a' s''" using assms by (auto elim: bindS_cases) -abbreviation - "try_catchS_aux h r \<equiv> - (case r of - (Value a, s') => returnS a s' - | (Ex (Throw e), s') => h e s' - | (Ex (Failure msg), s') => {(Ex (Failure msg), s')})" -abbreviation "try_catchS_app ms h \<equiv> \<Union>(try_catchS_aux h ` ms)" - lemma try_catchS_returnS[simp]: "try_catchS (returnS a) h = returnS a" and try_catchS_failS[simp]: "try_catchS (failS msg) h = failS msg" and try_catchS_throwS[simp]: "try_catchS (throwS e) h = h e" - by (auto simp: try_catchS_def) + by (auto simp: try_catchS_def returnS_def failS_def throwS_def) lemma try_catchS_cong[cong]: assumes "\<And>s. m1 s = m2 s" and "\<And>e s. h1 e s = h2 e s" @@ -155,13 +117,14 @@ lemma try_catchS_cases: obtains (Value) a where "r = Value a" and "(Value a, s') \<in> m s" | (Fail) msg where "r = Ex (Failure msg)" and "(Ex (Failure msg), s') \<in> m s" | (h) e s'' where "(Ex (Throw e), s'') \<in> m s" and "(r, s') \<in> h e s''" - using assms by (cases r rule: result_cases) (auto simp: try_catchS_def split: result.splits ex.splits) + using assms + by (cases r rule: result_cases) (auto simp: try_catchS_def returnS_def split: result.splits ex.splits) lemma try_catchS_intros: "\<And>m h s a s'. (Value a, s') \<in> m s \<Longrightarrow> (Value a, s') \<in> try_catchS m h s" "\<And>m h s msg s'. (Ex (Failure msg), s') \<in> m s \<Longrightarrow> (Ex (Failure msg), s') \<in> try_catchS m h s" "\<And>m h s e s'' r s'. (Ex (Throw e), s'') \<in> m s \<Longrightarrow> (r, s') \<in> h e s'' \<Longrightarrow> (r, s') \<in> try_catchS m h s" - by (auto simp: try_catchS_def intro: bexI[rotated]) + by (auto simp: try_catchS_def returnS_def intro: bexI[rotated]) fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) result \<times> 's) set" where "ignore_throw_aux (Value a, s') = {(Value a, s')}" @@ -169,42 +132,23 @@ fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) | "ignore_throw_aux (Ex (Failure msg), s') = {(Ex (Failure msg), s')}" definition "ignore_throw m s \<equiv> \<Union>(ignore_throw_aux ` m s)" -(*fun ignore_throw_aux :: "(('a, 'e1) result \<times> 's) \<Rightarrow> (('a, 'e2) result \<times> 's) list" where - "ignore_throw_aux r \<equiv> - (case r of - (Value a, s') => returnS a s' - | (Ex (Throw e), s') => h e s' - | (Ex (Failure msg), s') => {(Ex (Failure msg), s')})" -fun ignore_throw_app :: "(('a, 'e1) result \<times> 's) list \<Rightarrow> (('a, 'e2) result \<times> 's) list" where - "ignore_throw_app [] = []" -| "ignore_throw_app ((Value a, s) # ms) = (Value a, s) # ignore_throw_app ms" -| "ignore_throw_app ((Ex (Failure msg), s) # ms) = (Ex (Failure msg), s) # ignore_throw_app ms" -| "ignore_throw_app ((Ex (Throw e), s) # ms) = ignore_throw_app ms" -abbreviation ignore_throw :: "('r, 'a, 'e1) monadS \<Rightarrow> ('r, 'a, 'e2) monadS" where - "ignore_throw m \<equiv> \<lambda>s. ignore_throw_app (m s)" - -lemma [simp]: "ignore_throw_app ms = (Ex (Throw e), s) # ms' \<longleftrightarrow> False" - by (induction ms rule: ignore_throw_app.induct) auto - -lemma ignore_throw_app_append[simp]: - "ignore_throw_app (ms1 @ ms2) = ignore_throw_app ms1 @ ignore_throw_app ms2" - by (induction ms1 rule: ignore_throw_app.induct) auto - -lemma ignore_throw_app_bindS_app[simp]: - "ignore_throw_app (bindS_app ms f) = bindS_app (ignore_throw_app ms) (ignore_throw \<circ> f)" - by (induction ms rule: ignore_throw_app.induct) (auto split: result.splits)*) - -lemma [simp]: +lemma ignore_throw_cong: + assumes "\<And>s. m1 s = m2 s" + shows "ignore_throw m1 = ignore_throw m2" + using assms by (auto simp: ignore_throw_def) + +lemma ignore_throw_aux_member_simps[simp]: "(Value a, s') \<in> ignore_throw_aux ms \<longleftrightarrow> ms = (Value a, s')" "(Ex (Throw e), s') \<in> ignore_throw_aux ms \<longleftrightarrow> False" "(Ex (Failure msg), s') \<in> ignore_throw_aux ms \<longleftrightarrow> ms = (Ex (Failure msg), s')" by (cases ms rule: result_state_cases; auto)+ -(*lemma [simp]: "(Value a, s') \<in> ignore_throw m s \<longleftrightarrow> (Value a, s') \<in> m s" +lemma ignore_throw_member_simps[simp]: + "(Value a, s') \<in> ignore_throw m s \<longleftrightarrow> (Value a, s') \<in> m s" "(Value a, s') \<in> ignore_throw m s \<longleftrightarrow> (Value a, s') \<in> m s" "(Ex (Throw e), s') \<in> ignore_throw m s \<longleftrightarrow> False" - "(Ex (Failure msg), s') \<in> ignore_throw_aux ms \<longleftrightarrow> ms = (Ex (Failure msg), s')" - by (auto simp: ignore_throw_def)*) + "(Ex (Failure msg), s') \<in> ignore_throw m s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m s" + by (auto simp: ignore_throw_def) lemma ignore_throw_cases: assumes no_throw: "ignore_throw m s = m s" @@ -232,43 +176,21 @@ proof also have "\<dots> = bindS m2 (\<lambda>a. try_catchS (f a) h) s" using m2 by (intro bindS_ext_cong) auto finally show "try_catchS (bindS m1 f) h s = bindS m2 (\<lambda>a. try_catchS (f a) h) s" . qed -(*proof - fix s - have 1: "try_catchS_app (bindS_app ms f) h = - bindS_app (ignore_throw_app ms) (\<lambda>a s'. try_catchS_app (f a s') h)" - if "ignore_throw_app ms = ms" for ms - using that by (induction ms rule: ignore_throw_app.induct) auto - then show "try_catchS (bindS m1 f) h s = bindS m2 (\<lambda>a. try_catchS (f a) h) s" - using m1 unfolding try_catchS_def bindS_def m2[symmetric] by blast -qed*) - -(*lemma no_throwI: - fixes m1 :: "('regs, 'a, 'e1) monadS" and m2 :: "('regs, 'a, 'e2) monadS" - assumes "\<And>a s'. (Value a, s') \<in> m1 s \<longleftrightarrow> (Value a, s') \<in> m2 s" - and "\<And>msg s'. (Ex (Failure msg), s') \<in> m1 s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m2 s" - and "\<And>e s'. (Ex (Throw e), s') \<notin> m1 s" - and "\<And>e s'. (Ex (Throw e), s') \<notin> m2 s" - shows "ignore_throw m1 s = m2 s" - using assms by (intro monadS_ext_eqI) (auto simp: ignore_throw_def)*) - -(*lemma no_throw_bindSI: - assumes "ignore_throw m1 s = m2 s" -and "\<And>a s'. (Value a, s') \<in> m2 s \<Longrightarrow> ignore_throw (f1 a) s' = f2 a s'" -shows "ignore_throw (bindS m1 f1) s = bindS m2 f2 s" - using assms unfolding ignore_throw_bindS apply (intro monadS_ext_eqI) apply auto apply (auto elim!: bindS_cases intro: bindS_intros) - defer thm bindS_intros - apply (intro bindS_intros(3)) apply auto - apply (intro bindS_intros(3)) apply auto - done - -lemma - "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s" - unfolding read_mem_bytesS_def Let_def seqS_def - apply (intro no_throw_bindSI) - oops*) + +lemma no_throw_basic_builtins[simp]: + "ignore_throw (returnS a) = returnS a" + "\<And>f. ignore_throw (readS f) = readS f" + "\<And>f. ignore_throw (updateS f) = updateS f" + "ignore_throw (chooseS xs) = chooseS xs" + "ignore_throw (failS msg) = failS msg" + "ignore_throw (maybe_failS msg x) = maybe_failS msg x" + unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def + by (intro ext; auto split: option.splits)+ + +lemmas ignore_throw_option_case_distrib = + option.case_distrib[where h = "\<lambda>c. ignore_throw c s" and option = "c s" for c s] lemma no_throw_mem_builtins: - "\<And>a. ignore_throw (returnS a) = returnS a" "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s" "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s" "\<And>BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s" @@ -280,20 +202,21 @@ lemma no_throw_mem_builtins: unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def unfolding write_mem_valS_def write_mem_bytesS_def write_tagS_def unfolding excl_resultS_def undefined_boolS_def - by (auto simp: ignore_throw_def bindS_def chooseS_def Let_def split: option.splits prod.splits) + by (auto cong: bindS_cong bindS_ext_cong ignore_throw_cong option.case_cong + simp: option.case_distrib prod.case_distrib ignore_throw_option_case_distrib comp_def) lemma no_throw_read_memS: "ignore_throw (read_memS BCa BCb rk a sz) s = read_memS BCa BCb rk a sz s" by (auto simp: read_memS_def no_throw_mem_builtins cong: bindS_ext_cong) lemma no_throw_read_regvalS: "ignore_throw (read_regvalS r reg_name) s = read_regvalS r reg_name s" - by (cases r) (auto simp: ignore_throw_def bindS_def split: option.splits) + by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong) lemma no_throw_write_regvalS: "ignore_throw (write_regvalS r reg_name v) s = write_regvalS r reg_name v s" - by (cases r) (auto simp: ignore_throw_def bindS_def split: option.splits) + by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong) -lemmas no_throw_builtins[simp, intro] = +lemmas no_throw_builtins[simp] = no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS -end +(* end *) end |