src/HOL/Imperative_HOL/Heap_Monad.thy
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