src/HOL/Imperative_HOL/Mrec.thy
 author wenzelm Thu May 24 17:25:53 2012 +0200 (2012-05-24) changeset 47988 e4b69e10b990 parent 44890 22f665a2e91c permissions -rw-r--r--
tuned proofs;
 haftmann@37772 ` 1` ```theory Mrec ``` haftmann@37772 ` 2` ```imports Heap_Monad ``` haftmann@37772 ` 3` ```begin ``` haftmann@37772 ` 4` haftmann@37772 ` 5` ```subsubsection {* A monadic combinator for simple recursive functions *} ``` haftmann@37772 ` 6` haftmann@37772 ` 7` ```text {* Using a locale to fix arguments f and g of MREC *} ``` haftmann@37772 ` 8` haftmann@37772 ` 9` ```locale mrec = ``` haftmann@37772 ` 10` ``` fixes f :: "'a \ ('b + 'a) Heap" ``` haftmann@37772 ` 11` ``` and g :: "'a \ 'a \ 'b \ 'b Heap" ``` haftmann@37772 ` 12` ```begin ``` haftmann@37772 ` 13` haftmann@37772 ` 14` ```function (default "\(x, h). None") mrec :: "'a \ heap \ ('b \ heap) option" where ``` haftmann@37772 ` 15` ``` "mrec x h = (case execute (f x) h of ``` haftmann@37772 ` 16` ``` Some (Inl r, h') \ Some (r, h') ``` haftmann@37772 ` 17` ``` | Some (Inr s, h') \ (case mrec s h' of ``` haftmann@37772 ` 18` ``` Some (z, h'') \ execute (g x s z) h'' ``` haftmann@37772 ` 19` ``` | None \ None) ``` haftmann@37772 ` 20` ``` | None \ None)" ``` haftmann@37772 ` 21` ```by auto ``` haftmann@37772 ` 22` haftmann@37772 ` 23` ```lemma graph_implies_dom: ``` haftmann@37772 ` 24` ``` "mrec_graph x y \ mrec_dom x" ``` haftmann@37772 ` 25` ```apply (induct rule:mrec_graph.induct) ``` haftmann@37772 ` 26` ```apply (rule accpI) ``` haftmann@37772 ` 27` ```apply (erule mrec_rel.cases) ``` haftmann@37772 ` 28` ```by simp ``` haftmann@37772 ` 29` haftmann@37772 ` 30` ```lemma mrec_default: "\ mrec_dom (x, h) \ mrec x h = None" ``` haftmann@37772 ` 31` ``` unfolding mrec_def ``` haftmann@37772 ` 32` ``` by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified]) ``` haftmann@37772 ` 33` haftmann@37772 ` 34` ```lemma mrec_di_reverse: ``` haftmann@37772 ` 35` ``` assumes "\ mrec_dom (x, h)" ``` haftmann@37772 ` 36` ``` shows " ``` haftmann@37772 ` 37` ``` (case execute (f x) h of ``` haftmann@37772 ` 38` ``` Some (Inl r, h') \ False ``` haftmann@37772 ` 39` ``` | Some (Inr s, h') \ \ mrec_dom (s, h') ``` haftmann@37772 ` 40` ``` | None \ False ``` haftmann@37772 ` 41` ``` )" ``` haftmann@37772 ` 42` ```using assms apply (auto split: option.split sum.split) ``` haftmann@37772 ` 43` ```apply (rule ccontr) ``` haftmann@37772 ` 44` ```apply (erule notE, rule accpI, elim mrec_rel.cases, auto)+ ``` haftmann@37772 ` 45` ```done ``` haftmann@37772 ` 46` haftmann@37772 ` 47` ```lemma mrec_rule: ``` haftmann@37772 ` 48` ``` "mrec x h = ``` haftmann@37772 ` 49` ``` (case execute (f x) h of ``` haftmann@37772 ` 50` ``` Some (Inl r, h') \ Some (r, h') ``` haftmann@37772 ` 51` ``` | Some (Inr s, h') \ ``` haftmann@37772 ` 52` ``` (case mrec s h' of ``` haftmann@37772 ` 53` ``` Some (z, h'') \ execute (g x s z) h'' ``` haftmann@37772 ` 54` ``` | None \ None) ``` haftmann@37772 ` 55` ``` | None \ None ``` haftmann@37772 ` 56` ``` )" ``` krauss@39754 ` 57` ```apply (cases "mrec_dom (x,h)", simp add: mrec.psimps) ``` haftmann@37772 ` 58` ```apply (frule mrec_default) ``` haftmann@37772 ` 59` ```apply (frule mrec_di_reverse, simp) ``` haftmann@37772 ` 60` ```by (auto split: sum.split option.split simp: mrec_default) ``` haftmann@37772 ` 61` haftmann@37772 ` 62` ```definition ``` haftmann@37772 ` 63` ``` "MREC x = Heap_Monad.Heap (mrec x)" ``` haftmann@37772 ` 64` haftmann@37772 ` 65` ```lemma MREC_rule: ``` haftmann@37772 ` 66` ``` "MREC x = ``` krauss@37792 ` 67` ``` do { y \ f x; ``` haftmann@37772 ` 68` ``` (case y of ``` haftmann@37772 ` 69` ``` Inl r \ return r ``` haftmann@37772 ` 70` ``` | Inr s \ ``` krauss@37792 ` 71` ``` do { z \ MREC s ; ``` krauss@37792 ` 72` ``` g x s z })}" ``` haftmann@37772 ` 73` ``` unfolding MREC_def ``` haftmann@37772 ` 74` ``` unfolding bind_def return_def ``` haftmann@37772 ` 75` ``` apply simp ``` haftmann@37772 ` 76` ``` apply (rule ext) ``` haftmann@37772 ` 77` ``` apply (unfold mrec_rule[of x]) ``` haftmann@37787 ` 78` ``` by (auto simp add: execute_simps split: option.splits prod.splits sum.splits) ``` haftmann@37772 ` 79` haftmann@37772 ` 80` ```lemma MREC_pinduct: ``` haftmann@37772 ` 81` ``` assumes "execute (MREC x) h = Some (r, h')" ``` haftmann@37772 ` 82` ``` assumes non_rec_case: "\ x h h' r. execute (f x) h = Some (Inl r, h') \ P x h h' r" ``` haftmann@37772 ` 83` ``` assumes rec_case: "\ x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \ execute (MREC s) h1 = Some (z, h2) \ P s h1 h2 z ``` haftmann@37772 ` 84` ``` \ execute (g x s z) h2 = Some (r, h') \ P x h h' r" ``` haftmann@37772 ` 85` ``` shows "P x h h' r" ``` haftmann@37772 ` 86` ```proof - ``` haftmann@37772 ` 87` ``` from assms(1) have mrec: "mrec x h = Some (r, h')" ``` haftmann@37772 ` 88` ``` unfolding MREC_def execute.simps . ``` haftmann@37772 ` 89` ``` from mrec have dom: "mrec_dom (x, h)" ``` haftmann@37772 ` 90` ``` apply - ``` haftmann@37772 ` 91` ``` apply (rule ccontr) ``` haftmann@37772 ` 92` ``` apply (drule mrec_default) by auto ``` haftmann@37772 ` 93` ``` from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))" ``` haftmann@37772 ` 94` ``` by auto ``` haftmann@37772 ` 95` ``` from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))" ``` haftmann@37772 ` 96` ``` proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom]) ``` haftmann@37772 ` 97` ``` case (1 x h) ``` nipkow@44890 ` 98` ``` obtain rr h' where "the (mrec x h) = (rr, h')" by fastforce ``` haftmann@37772 ` 99` ``` show ?case ``` haftmann@37772 ` 100` ``` proof (cases "execute (f x) h") ``` haftmann@37772 ` 101` ``` case (Some result) ``` nipkow@44890 ` 102` ``` then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastforce ``` haftmann@37772 ` 103` ``` note Inl' = this ``` haftmann@37772 ` 104` ``` show ?thesis ``` haftmann@37772 ` 105` ``` proof (cases a) ``` haftmann@37772 ` 106` ``` case (Inl aa) ``` haftmann@37772 ` 107` ``` from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis ``` krauss@39754 ` 108` ``` by (auto simp: mrec.psimps) ``` haftmann@37772 ` 109` ``` next ``` haftmann@37772 ` 110` ``` case (Inr b) ``` haftmann@37772 ` 111` ``` note Inr' = this ``` haftmann@37772 ` 112` ``` show ?thesis ``` haftmann@37772 ` 113` ``` proof (cases "mrec b h1") ``` haftmann@37772 ` 114` ``` case (Some result) ``` nipkow@44890 ` 115` ``` then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastforce ``` haftmann@37772 ` 116` ``` moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))" ``` haftmann@37772 ` 117` ``` apply (intro 1(2)) ``` haftmann@37772 ` 118` ``` apply (auto simp add: Inr Inl') ``` haftmann@37772 ` 119` ``` done ``` haftmann@37772 ` 120` ``` moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3) ``` haftmann@37772 ` 121` ``` ultimately show ?thesis ``` haftmann@37772 ` 122` ``` apply auto ``` haftmann@37772 ` 123` ``` apply (rule rec_case) ``` haftmann@37772 ` 124` ``` apply auto ``` krauss@39754 ` 125` ``` unfolding MREC_def by (auto simp: mrec.psimps) ``` haftmann@37772 ` 126` ``` next ``` haftmann@37772 ` 127` ``` case None ``` krauss@39754 ` 128` ``` from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by (auto simp: mrec.psimps) ``` haftmann@37772 ` 129` ``` qed ``` haftmann@37772 ` 130` ``` qed ``` haftmann@37772 ` 131` ``` next ``` haftmann@37772 ` 132` ``` case None ``` krauss@39754 ` 133` ``` from this 1(1) mrec 1(3) show ?thesis by (simp add: mrec.psimps) ``` haftmann@37772 ` 134` ``` qed ``` haftmann@37772 ` 135` ``` qed ``` haftmann@37772 ` 136` ``` from this h'_r show ?thesis by simp ``` haftmann@37772 ` 137` ```qed ``` haftmann@37772 ` 138` haftmann@37772 ` 139` ```end ``` haftmann@37772 ` 140` haftmann@37772 ` 141` ```text {* Providing global versions of the constant and the theorems *} ``` haftmann@37772 ` 142` haftmann@37772 ` 143` ```abbreviation "MREC == mrec.MREC" ``` haftmann@37772 ` 144` ```lemmas MREC_rule = mrec.MREC_rule ``` haftmann@37772 ` 145` ```lemmas MREC_pinduct = mrec.MREC_pinduct ``` haftmann@37772 ` 146` haftmann@37772 ` 147` ```lemma MREC_induct: ``` haftmann@40671 ` 148` ``` assumes "effect (MREC f g x) h h' r" ``` haftmann@40671 ` 149` ``` assumes "\ x h h' r. effect (f x) h h' (Inl r) \ P x h h' r" ``` haftmann@40671 ` 150` ``` assumes "\ x h h1 h2 h' s z r. effect (f x) h h1 (Inr s) \ effect (MREC f g s) h1 h2 z \ P s h1 h2 z ``` haftmann@40671 ` 151` ``` \ effect (g x s z) h2 h' r \ P x h h' r" ``` haftmann@37772 ` 152` ``` shows "P x h h' r" ``` haftmann@40671 ` 153` ```proof (rule MREC_pinduct[OF assms(1) [unfolded effect_def]]) ``` haftmann@37772 ` 154` ``` fix x h h1 h2 h' s z r ``` haftmann@37772 ` 155` ``` assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)" ``` haftmann@37772 ` 156` ``` "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)" ``` haftmann@37772 ` 157` ``` "P s h1 h2 z" ``` haftmann@37772 ` 158` ``` "Heap_Monad.execute (g x s z) h2 = Some (r, h')" ``` haftmann@40671 ` 159` ``` from assms(3) [unfolded effect_def, OF this(1) this(2) this(3) this(4)] ``` haftmann@37772 ` 160` ``` show "P x h h' r" . ``` haftmann@37772 ` 161` ```next ``` haftmann@40671 ` 162` ```qed (auto simp add: assms(2)[unfolded effect_def]) ``` haftmann@37772 ` 163` haftmann@37772 ` 164` ```end ```