diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/State_lemmas.thy | 8 | ||||
| -rw-r--r-- | lib/isabelle/State_monad_lemmas.thy | 200 |
2 files changed, 179 insertions, 29 deletions
diff --git a/lib/isabelle/State_lemmas.thy b/lib/isabelle/State_lemmas.thy index 9c5dd8af..d8ab5db9 100644 --- a/lib/isabelle/State_lemmas.thy +++ b/lib/isabelle/State_lemmas.thy @@ -13,7 +13,7 @@ lemma liftState_bind[simp]: lemma liftState_return[simp]: "liftState r (return a) = returnS a" by (auto simp: return_def) lemma Value_liftState_Run: - assumes "(Value a, s') \<in> set (liftState r m s)" + assumes "(Value a, s') \<in> liftState r m s" obtains t where "Run m t a" by (use assms in \<open>induction r m arbitrary: s s' rule: liftState.induct\<close>; auto simp add: failS_def throwS_def returnS_def simp del: read_regvalS.simps; @@ -101,8 +101,8 @@ lemma liftState_foreachM[simp]: lemma whileS_dom_step: assumes "whileS_dom (vars, cond, body, s)" - and "(Value True, s') \<in> set (cond vars s)" - and "(Value vars', s'') \<in> set (body vars s')" + and "(Value True, s') \<in> cond vars s" + and "(Value vars', s'') \<in> body vars s'" shows "whileS_dom (vars', cond, body, s'')" by (use assms in \<open>induction vars cond body s arbitrary: vars' s' s'' rule: whileS.pinduct\<close>) (auto intro: whileS.domintros) @@ -143,7 +143,7 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState show "\<exists>t. Run (cond vars) t True" using while that by (auto elim: Value_liftState_Run) show "\<exists>t'. Run (body vars) t' vars'" using while' that by (auto elim: Value_liftState_Run) qed - then show ?case using while while' that by (auto intro: IH) + then show ?case using while while' that IH by auto qed auto then show ?case by auto qed auto diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy index d8730421..746fd315 100644 --- a/lib/isabelle/State_monad_lemmas.thy +++ b/lib/isabelle/State_monad_lemmas.thy @@ -8,34 +8,36 @@ 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> List.concat (List.map (bindS_aux f) ms)" +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)" lemma bindS_ext_cong[fundef_cong]: assumes m: "m1 s = m2 s" - and f: "\<And>a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a 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" -proof - + 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 (intro arg_cong[where f = List.concat]) (auto intro: map_ext split: result.splits) + using f by (auto split: result.splits) then show ?thesis using m by (auto simp: bindS_def) -qed +qed *) lemma bindS_cong[fundef_cong]: assumes m: "m1 = m2" - and f: "\<And>s a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" + and f: "\<And>s a s'. (Value a, s') \<in> (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" shows "bindS m1 f1 = bindS m2 f2" - using assms by (blast intro: bindS_ext_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) lemma bindS_returnS_right[simp]: "bindS m returnS = (m :: ('regs, 'a, 'e) monadS)" -proof - + 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 +qed *) lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)" by (auto simp: bindS_def) @@ -43,30 +45,100 @@ lemma bindS_readS: "bindS (readS f) m = (\<lambda>s. m (f s) s)" lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))" by (auto simp: bindS_def) -lemma bindS_assoc[simp]: "bindS (bindS m f) g = bindS m (\<lambda>x. bindS (f x) g)" + +lemma result_cases: + fixes r :: "('a, 'e) result" + obtains (Value) a where "r = Value a" + | (Throw) e where "r = Ex (Throw e)" + | (Failure) msg where "r = Ex (Failure msg)" +proof (cases r) + case (Ex ex) then show ?thesis by (cases ex; auto intro: that) +qed + +lemma result_state_cases: + fixes rs :: "('a, 'e) result \<times> 's" + obtains (Value) a s where "rs = (Value a, s)" + | (Throw) e s where "rs = (Ex (Throw e), s)" + | (Failure) msg s where "rs = (Ex (Failure msg), s)" proof - + obtain r s where rs: "rs = (r, s)" by (cases rs) + then show thesis by (cases r rule: result_cases) (auto intro: that) +qed + +lemma monadS_ext_eqI: + fixes m m' :: "('regs, 'a, 'e) monadS" + assumes "\<And>a s'. (Value a, s') \<in> m s \<longleftrightarrow> (Value a, s') \<in> m' s" + and "\<And>e s'. (Ex (Throw e), s') \<in> m s \<longleftrightarrow> (Ex (Throw e), s') \<in> m' s" + and "\<And>msg s'. (Ex (Failure msg), s') \<in> m s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m' s" + shows "m s = m' s" +proof (intro set_eqI) + fix x + show "x \<in> m s \<longleftrightarrow> x \<in> m' s" using assms by (cases x rule: result_state_cases) auto +qed + +lemma monadS_eqI: + fixes m m' :: "('regs, 'a, 'e) monadS" + assumes "\<And>s a s'. (Value a, s') \<in> m s \<longleftrightarrow> (Value a, s') \<in> m' s" + and "\<And>s e s'. (Ex (Throw e), s') \<in> m s \<longleftrightarrow> (Ex (Throw e), s') \<in> m' s" + and "\<And>s msg s'. (Ex (Failure msg), s') \<in> m s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m' s" + 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''" + | (Ex_Left) e where "r = Ex e" and "(Ex e, s') \<in> m s" + | (Ex_Right) e a s'' where "r = Ex e" and "(Value a, s'') \<in> m s" and "(Ex e, s') \<in> f a s''" + using assms by (cases r; auto simp: bindS_def split: result.splits) + +lemma bindS_intros: + "\<And>m f s a s' a' s''. (Value a', s'') \<in> m s \<Longrightarrow> (Value a, s') \<in> f a' s'' \<Longrightarrow> (Value a, s') \<in> bindS m f s" + "\<And>m f s e s'. (Ex e, s') \<in> m s \<Longrightarrow> (Ex e, s') \<in> bindS m f s" + "\<And>m f s e s' a s''. (Ex e, s') \<in> f a s'' \<Longrightarrow> (Value a, s'') \<in> m s \<Longrightarrow> (Ex e, s') \<in> bindS m f s" + by (auto simp: bindS_def intro: bexI[rotated]) + +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 +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) declare seqS_def[simp] lemma Value_bindS_elim: - assumes "(Value a, s') \<in> set (bindS m f s)" - obtains s'' a' where "(Value a', s'') \<in> set (m s)" and "(Value a, s') \<in> set (f a' s'')" - using assms by (auto simp: bindS_def; split result.splits; auto) + assumes "(Value a, s') \<in> bindS m f s" + obtains s'' a' where "(Value a', s'') \<in> m s" and "(Value a, s') \<in> f a' s''" + using assms by (auto elim: bindS_cases) + +lemma Ex_bindS_elim: + assumes "(Ex e, s') \<in> bindS m f s" + obtains (Left) "(Ex e, s') \<in> m s" + | (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> List.concat (List.map (try_catchS_aux h) ms)" + | (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" @@ -78,6 +150,31 @@ lemma try_catchS_cong[cong]: shows "try_catchS m1 h1 = try_catchS m2 h2" using assms by (intro arg_cong2[where f = try_catchS] ext) auto +lemma try_catchS_cases: + assumes "(r, s') \<in> try_catchS m h s" + 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) + +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]) + +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')}" +| "ignore_throw_aux (Ex (Throw e), s') = {}" +| "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" @@ -95,12 +192,31 @@ lemma ignore_throw_app_append[simp]: 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) + by (induction ms rule: ignore_throw_app.induct) (auto split: result.splits)*) + +lemma [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" + "(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)*) + +lemma ignore_throw_cases: + assumes no_throw: "ignore_throw m s = m s" + and r: "(r, s') \<in> m s" + obtains (Value) a where "r = Value a" + | (Failure) msg where "r = Ex (Failure msg)" + using r unfolding no_throw[symmetric] + by (cases r rule: result_cases) (auto simp: ignore_throw_def) lemma ignore_throw_bindS[simp]: "ignore_throw (bindS m f) = bindS (ignore_throw m) (ignore_throw \<circ> f)" - "ignore_throw (bindS m f) s = bindS (ignore_throw m) (ignore_throw \<circ> f) s" - unfolding bindS_def by auto + by (intro monadS_eqI) (auto simp: ignore_throw_def elim!: bindS_cases intro: bindS_intros) lemma try_catchS_bindS_no_throw: fixes m1 :: "('r, 'a, 'e1) monadS" and m2 :: "('r, 'a, 'e2) monadS" @@ -109,13 +225,47 @@ lemma try_catchS_bindS_no_throw: shows "try_catchS (bindS m1 f) h = bindS m2 (\<lambda>a. try_catchS (f a) h)" proof fix s + have "try_catchS (bindS m1 f) h s = bindS (ignore_throw m1) (\<lambda>a. try_catchS (f a) h) s" + by (intro monadS_ext_eqI; + auto elim!: bindS_cases try_catchS_cases elim: ignore_throw_cases[OF m1]; + auto simp: ignore_throw_def intro: bindS_intros try_catchS_intros) + 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 +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_mem_builtins: "\<And>a. ignore_throw (returnS a) = returnS a" @@ -130,16 +280,16 @@ 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: bindS_def chooseS_def Let_def split: option.splits prod.splits)+ + by (auto simp: ignore_throw_def bindS_def chooseS_def Let_def split: option.splits prod.splits) 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_cong) + 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: bindS_def split: option.splits) + by (cases r) (auto simp: ignore_throw_def bindS_def split: option.splits) 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: bindS_def split: option.splits) + by (cases r) (auto simp: ignore_throw_def bindS_def split: option.splits) lemmas no_throw_builtins[simp, intro] = no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS |