# HG changeset patch # User haftmann # Date 1288353970 -7200 # Node ID af22d99f4446e4b852b4a560de53f9087abd2efa # Parent ee578bc82cbcc7b70d69e2dc704250e1a4e5b29c# Parent a03e288d79025c7a26a075275f72492bf385d458 merged diff -r ee578bc82cbc -r af22d99f4446 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Oct 29 12:49:05 2010 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Oct 29 14:06:10 2010 +0200 @@ -16,6 +16,10 @@ and transform the heap, or fail *} datatype 'a Heap = Heap "heap \ ('a \ heap) option" +lemma [code, code del]: + "(Code_Evaluation.term_of :: 'a::typerep Heap \ Code_Evaluation.term) = Code_Evaluation.term_of" + .. + primrec execute :: "'a Heap \ heap \ ('a \ heap) option" where [code del]: "execute (Heap f) = f" @@ -398,6 +402,82 @@ ultimately show ?case by (simp, simp only: execute_bind(1), simp add: execute_simps) qed + +subsection {* Partial function definition setup *} + +definition Heap_ord :: "'a Heap \ 'a Heap \ bool" where + "Heap_ord = img_ord execute (fun_ord option_ord)" + +definition Heap_lub :: "('a Heap \ bool) \ 'a Heap" where + "Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))" + +interpretation heap!: partial_function_definitions Heap_ord Heap_lub +proof - + have "partial_function_definitions (fun_ord option_ord) (fun_lub (flat_lub None))" + by (rule partial_function_lift) (rule flat_interpretation) + then have "partial_function_definitions (img_ord execute (fun_ord option_ord)) + (img_lub execute Heap (fun_lub (flat_lub None)))" + by (rule partial_function_image) (auto intro: Heap_eqI) + then show "partial_function_definitions Heap_ord Heap_lub" + by (simp only: Heap_ord_def Heap_lub_def) +qed + +abbreviation "mono_Heap \ monotone (fun_ord Heap_ord) Heap_ord" + +lemma Heap_ordI: + assumes "\h. execute x h = None \ execute x h = execute y h" + shows "Heap_ord x y" + using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def + by blast + +lemma Heap_ordE: + assumes "Heap_ord x y" + obtains "execute x h = None" | "execute x h = execute y h" + using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def + by atomize_elim blast + +lemma bind_mono[partial_function_mono]: + assumes mf: "mono_Heap B" and mg: "\y. mono_Heap (\f. C y f)" + shows "mono_Heap (\f. B f \= (\y. C y f))" +proof (rule monotoneI) + fix f g :: "'a \ 'b Heap" assume fg: "fun_ord Heap_ord f g" + from mf + have 1: "Heap_ord (B f) (B g)" by (rule monotoneD) (rule fg) + from mg + have 2: "\y'. Heap_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg) + + have "Heap_ord (B f \= (\y. C y f)) (B g \= (\y. C y f))" + (is "Heap_ord ?L ?R") + proof (rule Heap_ordI) + fix h + from 1 show "execute ?L h = None \ execute ?L h = execute ?R h" + by (rule Heap_ordE[where h = h]) (auto simp: execute_bind_case) + qed + also + have "Heap_ord (B g \= (\y'. C y' f)) (B g \= (\y'. C y' g))" + (is "Heap_ord ?L ?R") + proof (rule Heap_ordI) + fix h + show "execute ?L h = None \ execute ?L h = execute ?R h" + proof (cases "execute (B g) h") + case None + then have "execute ?L h = None" by (auto simp: execute_bind_case) + thus ?thesis .. + next + case Some + then obtain r h' where "execute (B g) h = Some (r, h')" + by (metis surjective_pairing) + then have "execute ?L h = execute (C r f) h'" + "execute ?R h = execute (C r g) h'" + by (auto simp: execute_bind_case) + with 2[of r] show ?thesis by (auto elim: Heap_ordE) + qed + qed + finally (heap.leq_trans) + show "Heap_ord (B f \= (\y. C y f)) (B g \= (\y'. C y' g))" . +qed + + subsection {* Code generator setup *} subsubsection {* Logical intermediate layer *} @@ -593,76 +673,6 @@ *} - -section {* Partial function definition setup *} - -definition "Heap_ord = img_ord execute (fun_ord option_ord)" -definition "Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))" - -interpretation heap!: - partial_function_definitions Heap_ord Heap_lub -unfolding Heap_ord_def Heap_lub_def -apply (rule partial_function_image) -apply (rule partial_function_lift) -apply (rule flat_interpretation) -by (auto intro: Heap_eqI) - -abbreviation "mono_Heap \ monotone (fun_ord Heap_ord) Heap_ord" - -lemma Heap_ordI: - assumes "\h. execute x h = None \ execute x h = execute y h" - shows "Heap_ord x y" -using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def -by blast - -lemma Heap_ordE: - assumes "Heap_ord x y" - obtains "execute x h = None" | "execute x h = execute y h" -using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def -by atomize_elim blast - - -lemma bind_mono[partial_function_mono]: -assumes mf: "mono_Heap B" and mg: "\y. mono_Heap (\f. C y f)" -shows "mono_Heap (\f. B f \= (\y. C y f))" -proof (rule monotoneI) - fix f g :: "'a \ 'b Heap" assume fg: "fun_ord Heap_ord f g" - from mf - have 1: "Heap_ord (B f) (B g)" by (rule monotoneD) (rule fg) - from mg - have 2: "\y'. Heap_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg) - - have "Heap_ord (B f \= (\y. C y f)) (B g \= (\y. C y f))" - (is "Heap_ord ?L ?R") - proof (rule Heap_ordI) - fix h - from 1 show "execute ?L h = None \ execute ?L h = execute ?R h" - by (rule Heap_ordE[where h = h]) (auto simp: execute_bind_case) - qed - also - have "Heap_ord (B g \= (\y'. C y' f)) (B g \= (\y'. C y' g))" - (is "Heap_ord ?L ?R") - proof (rule Heap_ordI) - fix h - show "execute ?L h = None \ execute ?L h = execute ?R h" - proof (cases "execute (B g) h") - case None - then have "execute ?L h = None" by (auto simp: execute_bind_case) - thus ?thesis .. - next - case Some - then obtain r h' where "execute (B g) h = Some (r, h')" - by (metis surjective_pairing) - then have "execute ?L h = execute (C r f) h'" - "execute ?R h = execute (C r g) h'" - by (auto simp: execute_bind_case) - with 2[of r] show ?thesis by (auto elim: Heap_ordE) - qed - qed - finally (heap.leq_trans) - show "Heap_ord (B f \= (\y. C y f)) (B g \= (\y'. C y' g))" . -qed - hide_const (open) Heap heap guard raise' fold_map end