author bulwahn Wed, 31 Mar 2010 16:44:41 +0200 changeset 36057 ca6610908ae9 parent 36056 0c128c2c310d child 36066 1493b43204e9 child 36070 d80e5d3c8fe1
adding MREC induction rule in Imperative HOL
```--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Mar 31 16:44:41 2010 +0200
@@ -270,15 +270,23 @@
using assms by (auto simp add: assert_def return_bind raise_bind)

subsubsection {* A monadic combinator for simple recursive functions *}
-
-function (default "\<lambda>(f,g,x,h). (Inr Exn, undefined)")
+
+text {* Using a locale to fix arguments f and g of MREC *}
+
+locale mrec =
+fixes
+  f :: "'a => ('b + 'a) Heap"
+  and g :: "'a => 'a => 'b => 'b Heap"
+begin
+
+function (default "\<lambda>(x,h). (Inr Exn, undefined)")
mrec
where
-  "mrec f g x h =
+  "mrec x h =
(case Heap_Monad.execute (f x) h of
(Inl (Inl r), h') \<Rightarrow> (Inl r, h')
| (Inl (Inr s), h') \<Rightarrow>
-          (case mrec f g s h' of
+          (case mrec s h' of
(Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
| (Inr e, h'') \<Rightarrow> (Inr e, h''))
| (Inr e, h') \<Rightarrow> (Inr e, h')
@@ -292,17 +300,17 @@
apply (erule mrec_rel.cases)
by simp

-lemma f_default: "\<not> mrec_dom (f, g, x, h) \<Longrightarrow> mrec f g x h = (Inr Exn, undefined)"
+lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = (Inr Exn, undefined)"
unfolding mrec_def
-  by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(f, g, x, h)", simplified])
+  by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])

-lemma f_di_reverse:
-  assumes "\<not> mrec_dom (f, g, x, h)"
+lemma mrec_di_reverse:
+  assumes "\<not> mrec_dom (x, h)"
shows "
(case Heap_Monad.execute (f x) h of
-     (Inl (Inl r), h') \<Rightarrow> mrecalse
-   | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (f, g, s, h')
-   | (Inr e, h') \<Rightarrow> mrecalse
+     (Inl (Inl r), h') \<Rightarrow> False
+   | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (s, h')
+   | (Inr e, h') \<Rightarrow> False
)"
using assms
by (auto split:prod.splits sum.splits)
@@ -310,40 +318,103 @@

lemma mrec_rule:
-  "mrec f g x h =
+  "mrec x h =
(case Heap_Monad.execute (f x) h of
(Inl (Inl r), h') \<Rightarrow> (Inl r, h')
| (Inl (Inr s), h') \<Rightarrow>
-          (case mrec f g s h' of
+          (case mrec s h' of
(Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
| (Inr e, h'') \<Rightarrow> (Inr e, h''))
| (Inr e, h') \<Rightarrow> (Inr e, h')
)"
-apply (cases "mrec_dom (f,g,x,h)", simp)
-apply (frule f_default)
-apply (frule f_di_reverse, simp)
-by (auto split: sum.split prod.split simp: f_default)
+apply (cases "mrec_dom (x,h)", simp)
+apply (frule mrec_default)
+apply (frule mrec_di_reverse, simp)
+by (auto split: sum.split prod.split simp: mrec_default)

definition
-  "MREC f g x = Heap (mrec f g x)"
+  "MREC x = Heap (mrec x)"

lemma MREC_rule:
-  "MREC f g x =
+  "MREC x =
(do y \<leftarrow> f x;
(case y of
Inl r \<Rightarrow> return r
| Inr s \<Rightarrow>
-                do z \<leftarrow> MREC f g s ;
+                do z \<leftarrow> MREC s ;
g x s z
done) done)"
unfolding MREC_def
unfolding bindM_def return_def
apply simp
apply (rule ext)
-  apply (unfold mrec_rule[of f g x])
+  apply (unfold mrec_rule[of x])
by (auto split:prod.splits sum.splits)

+
+lemma MREC_pinduct:
+  assumes "Heap_Monad.execute (MREC x) h = (Inl r, h')"
+  assumes non_rec_case: "\<And> x h h' r. Heap_Monad.execute (f x) h = (Inl (Inl r), h') \<Longrightarrow> P x h h' r"
+  assumes rec_case: "\<And> x h h1 h2 h' s z r. Heap_Monad.execute (f x) h = (Inl (Inr s), h1) \<Longrightarrow> Heap_Monad.execute (MREC s) h1 = (Inl z, h2) \<Longrightarrow> P s h1 h2 z
+    \<Longrightarrow> Heap_Monad.execute (g x s z) h2 = (Inl r, h') \<Longrightarrow> P x h h' r"
+  shows "P x h h' r"
+proof -
+  from assms(1) have mrec: "mrec x h = (Inl r, h')"
+    unfolding MREC_def execute.simps .
+  from mrec have dom: "mrec_dom (x, h)"
+    apply -
+    apply (rule ccontr)
+    apply (drule mrec_default) by auto
+  from mrec have h'_r: "h' = (snd (mrec x h))" "r = (Sum_Type.Projl (fst (mrec x h)))"
+    by auto
+  from mrec have "P x h (snd (mrec x h)) (Sum_Type.Projl (fst (mrec x h)))"
+  proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
+    case (1 x h)
+    obtain rr h' where "mrec x h = (rr, h')" by fastsimp
+    obtain fret h1 where exec_f: "Heap_Monad.execute (f x) h = (fret, h1)" by fastsimp
+    show ?case
+    proof (cases fret)
+      case (Inl a)
+      note Inl' = this
+      show ?thesis
+      proof (cases a)
+        case (Inl aa)
+        from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
+          by auto
+      next
+        case (Inr b)
+        note Inr' = this
+        obtain ret_mrec h2 where mrec_rec: "mrec b h1 = (ret_mrec, h2)" by fastsimp
+        from this Inl 1(1) exec_f mrec show ?thesis
+        proof (cases "ret_mrec")
+          case (Inl aaa)
+          from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3)
+            show ?thesis
+              apply auto
+              apply (rule rec_case)
+              unfolding MREC_def by auto
+        next
+          case (Inr b)
+          from this Inl 1(1) exec_f mrec Inr' mrec_rec 1(3) show ?thesis by auto
+        qed
+      qed
+    next
+      case (Inr b)
+      from this 1(1) mrec exec_f 1(3) show ?thesis by simp
+    qed
+  qed
+  from this h'_r show ?thesis by simp
+qed
+
+end
+
+text {* Providing global versions of the constant and the theorems *}
+
+abbreviation "MREC == mrec.MREC"
+lemmas MREC_rule = mrec.MREC_rule
+lemmas MREC_pinduct = mrec.MREC_pinduct
+
hide (open) const heap execute

```
```--- a/src/HOL/Imperative_HOL/Relational.thy	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Imperative_HOL/Relational.thy	Wed Mar 31 16:44:41 2010 +0200
@@ -469,7 +469,7 @@

(* thm crel_mapI is missing *)

-subsection {* Introduction rules for reference commands *}
+subsubsection {* Introduction rules for reference commands *}

lemma crel_lookupI:
shows "crel (!ref) h h (get_ref ref h)"
@@ -483,7 +483,7 @@
shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)

-subsection {* Introduction rules for the assert command *}
+subsubsection {* Introduction rules for the assert command *}

lemma crel_assertI:
assumes "P x"
@@ -492,7 +492,26 @@
unfolding assert_def
by (auto intro!: crel_ifI crel_returnI crel_raiseI)

-section {* Defintion of the noError predicate *}
+subsection {* Induction rule for the MREC combinator *}
+
+lemma MREC_induct:
+  assumes "crel (MREC f g x) h h' r"
+  assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
+  assumes "\<And> x h h1 h2 h' s z r. crel (f x) h h1 (Inr s) \<Longrightarrow> crel (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
+    \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
+  shows "P x h h' r"
+proof (rule MREC_pinduct[OF assms(1)[unfolded crel_def, symmetric]])
+  fix x h h1 h2 h' s z r
+  assume "Heap_Monad.execute (f x) h = (Inl (Inr s), h1)"
+    "Heap_Monad.execute (MREC f g s) h1 = (Inl z, h2)"
+    "P s h1 h2 z"
+    "Heap_Monad.execute (g x s z) h2 = (Inl r, h')"
+  from assms(3)[unfolded crel_def, OF this(1)[symmetric] this(2)[symmetric] this(3) this(4)[symmetric]]
+  show "P x h h' r" .
+next
+qed (auto simp add: assms(2)[unfolded crel_def])
+
+section {* Definition of the noError predicate *}

text {* We add a simple definitional setting for crel intro rules
where we only would like to show that the computation does not result in a exception for heap h,```