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