changeset 36057 ca6610908ae9 parent 35423 6ef9525a5727 child 36078 59f6773a7d1d
```     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Mar 31 16:44:41 2010 +0200
1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Mar 31 16:44:41 2010 +0200
1.3 @@ -270,15 +270,23 @@
1.4    using assms by (auto simp add: assert_def return_bind raise_bind)
1.5
1.6  subsubsection {* A monadic combinator for simple recursive functions *}
1.7 -
1.8 -function (default "\<lambda>(f,g,x,h). (Inr Exn, undefined)")
1.9 +
1.10 +text {* Using a locale to fix arguments f and g of MREC *}
1.11 +
1.12 +locale mrec =
1.13 +fixes
1.14 +  f :: "'a => ('b + 'a) Heap"
1.15 +  and g :: "'a => 'a => 'b => 'b Heap"
1.16 +begin
1.17 +
1.18 +function (default "\<lambda>(x,h). (Inr Exn, undefined)")
1.19    mrec
1.20  where
1.21 -  "mrec f g x h =
1.22 +  "mrec x h =
1.23     (case Heap_Monad.execute (f x) h of
1.24       (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
1.25     | (Inl (Inr s), h') \<Rightarrow>
1.26 -          (case mrec f g s h' of
1.27 +          (case mrec s h' of
1.28               (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
1.29             | (Inr e, h'') \<Rightarrow> (Inr e, h''))
1.30     | (Inr e, h') \<Rightarrow> (Inr e, h')
1.31 @@ -292,17 +300,17 @@
1.32  apply (erule mrec_rel.cases)
1.33  by simp
1.34
1.35 -lemma f_default: "\<not> mrec_dom (f, g, x, h) \<Longrightarrow> mrec f g x h = (Inr Exn, undefined)"
1.36 +lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = (Inr Exn, undefined)"
1.37    unfolding mrec_def
1.38 -  by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(f, g, x, h)", simplified])
1.39 +  by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])
1.40
1.41 -lemma f_di_reverse:
1.42 -  assumes "\<not> mrec_dom (f, g, x, h)"
1.43 +lemma mrec_di_reverse:
1.44 +  assumes "\<not> mrec_dom (x, h)"
1.45    shows "
1.46     (case Heap_Monad.execute (f x) h of
1.47 -     (Inl (Inl r), h') \<Rightarrow> mrecalse
1.48 -   | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (f, g, s, h')
1.49 -   | (Inr e, h') \<Rightarrow> mrecalse
1.50 +     (Inl (Inl r), h') \<Rightarrow> False
1.51 +   | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (s, h')
1.52 +   | (Inr e, h') \<Rightarrow> False
1.53     )"
1.54  using assms
1.55  by (auto split:prod.splits sum.splits)
1.56 @@ -310,40 +318,103 @@
1.57
1.58
1.59  lemma mrec_rule:
1.60 -  "mrec f g x h =
1.61 +  "mrec x h =
1.62     (case Heap_Monad.execute (f x) h of
1.63       (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
1.64     | (Inl (Inr s), h') \<Rightarrow>
1.65 -          (case mrec f g s h' of
1.66 +          (case mrec s h' of
1.67               (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
1.68             | (Inr e, h'') \<Rightarrow> (Inr e, h''))
1.69     | (Inr e, h') \<Rightarrow> (Inr e, h')
1.70     )"
1.71 -apply (cases "mrec_dom (f,g,x,h)", simp)
1.72 -apply (frule f_default)
1.73 -apply (frule f_di_reverse, simp)
1.74 -by (auto split: sum.split prod.split simp: f_default)
1.75 +apply (cases "mrec_dom (x,h)", simp)
1.76 +apply (frule mrec_default)
1.77 +apply (frule mrec_di_reverse, simp)
1.78 +by (auto split: sum.split prod.split simp: mrec_default)
1.79
1.80
1.81  definition
1.82 -  "MREC f g x = Heap (mrec f g x)"
1.83 +  "MREC x = Heap (mrec x)"
1.84
1.85  lemma MREC_rule:
1.86 -  "MREC f g x =
1.87 +  "MREC x =
1.88    (do y \<leftarrow> f x;
1.89                  (case y of
1.90                  Inl r \<Rightarrow> return r
1.91                | Inr s \<Rightarrow>
1.92 -                do z \<leftarrow> MREC f g s ;
1.93 +                do z \<leftarrow> MREC s ;
1.94                     g x s z
1.95                  done) done)"
1.96    unfolding MREC_def
1.97    unfolding bindM_def return_def
1.98    apply simp
1.99    apply (rule ext)
1.100 -  apply (unfold mrec_rule[of f g x])
1.101 +  apply (unfold mrec_rule[of x])
1.102    by (auto split:prod.splits sum.splits)
1.103
1.104 +
1.105 +lemma MREC_pinduct:
1.106 +  assumes "Heap_Monad.execute (MREC x) h = (Inl r, h')"
1.107 +  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"
1.108 +  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
1.109 +    \<Longrightarrow> Heap_Monad.execute (g x s z) h2 = (Inl r, h') \<Longrightarrow> P x h h' r"
1.110 +  shows "P x h h' r"
1.111 +proof -
1.112 +  from assms(1) have mrec: "mrec x h = (Inl r, h')"
1.113 +    unfolding MREC_def execute.simps .
1.114 +  from mrec have dom: "mrec_dom (x, h)"
1.115 +    apply -
1.116 +    apply (rule ccontr)
1.117 +    apply (drule mrec_default) by auto
1.118 +  from mrec have h'_r: "h' = (snd (mrec x h))" "r = (Sum_Type.Projl (fst (mrec x h)))"
1.119 +    by auto
1.120 +  from mrec have "P x h (snd (mrec x h)) (Sum_Type.Projl (fst (mrec x h)))"
1.121 +  proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
1.122 +    case (1 x h)
1.123 +    obtain rr h' where "mrec x h = (rr, h')" by fastsimp
1.124 +    obtain fret h1 where exec_f: "Heap_Monad.execute (f x) h = (fret, h1)" by fastsimp
1.125 +    show ?case
1.126 +    proof (cases fret)
1.127 +      case (Inl a)
1.128 +      note Inl' = this
1.129 +      show ?thesis
1.130 +      proof (cases a)
1.131 +        case (Inl aa)
1.132 +        from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
1.133 +          by auto
1.134 +      next
1.135 +        case (Inr b)
1.136 +        note Inr' = this
1.137 +        obtain ret_mrec h2 where mrec_rec: "mrec b h1 = (ret_mrec, h2)" by fastsimp
1.138 +        from this Inl 1(1) exec_f mrec show ?thesis
1.139 +        proof (cases "ret_mrec")
1.140 +          case (Inl aaa)
1.141 +          from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3)
1.142 +            show ?thesis
1.143 +              apply auto
1.144 +              apply (rule rec_case)
1.145 +              unfolding MREC_def by auto
1.146 +        next
1.147 +          case (Inr b)
1.148 +          from this Inl 1(1) exec_f mrec Inr' mrec_rec 1(3) show ?thesis by auto
1.149 +        qed
1.150 +      qed
1.151 +    next
1.152 +      case (Inr b)
1.153 +      from this 1(1) mrec exec_f 1(3) show ?thesis by simp
1.154 +    qed
1.155 +  qed
1.156 +  from this h'_r show ?thesis by simp
1.157 +qed
1.158 +
1.159 +end
1.160 +
1.161 +text {* Providing global versions of the constant and the theorems *}
1.162 +
1.163 +abbreviation "MREC == mrec.MREC"
1.164 +lemmas MREC_rule = mrec.MREC_rule
1.165 +lemmas MREC_pinduct = mrec.MREC_pinduct
1.166 +
1.167  hide (open) const heap execute
1.168
1.169
```