src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 36057 ca6610908ae9
parent 35423 6ef9525a5727
child 36078 59f6773a7d1d
equal deleted inserted replaced
36056:0c128c2c310d 36057:ca6610908ae9
   268   assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
   268   assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
   269   shows "(assert P x >>= f) = (assert P' x >>= f')"
   269   shows "(assert P x >>= f) = (assert P' x >>= f')"
   270   using assms by (auto simp add: assert_def return_bind raise_bind)
   270   using assms by (auto simp add: assert_def return_bind raise_bind)
   271 
   271 
   272 subsubsection {* A monadic combinator for simple recursive functions *}
   272 subsubsection {* A monadic combinator for simple recursive functions *}
   273  
   273 
   274 function (default "\<lambda>(f,g,x,h). (Inr Exn, undefined)") 
   274 text {* Using a locale to fix arguments f and g of MREC *}
       
   275 
       
   276 locale mrec =
       
   277 fixes
       
   278   f :: "'a => ('b + 'a) Heap"
       
   279   and g :: "'a => 'a => 'b => 'b Heap"
       
   280 begin
       
   281 
       
   282 function (default "\<lambda>(x,h). (Inr Exn, undefined)") 
   275   mrec 
   283   mrec 
   276 where
   284 where
   277   "mrec f g x h = 
   285   "mrec x h = 
   278    (case Heap_Monad.execute (f x) h of
   286    (case Heap_Monad.execute (f x) h of
   279      (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
   287      (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
   280    | (Inl (Inr s), h') \<Rightarrow> 
   288    | (Inl (Inr s), h') \<Rightarrow> 
   281           (case mrec f g s h' of
   289           (case mrec s h' of
   282              (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
   290              (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
   283            | (Inr e, h'') \<Rightarrow> (Inr e, h''))
   291            | (Inr e, h'') \<Rightarrow> (Inr e, h''))
   284    | (Inr e, h') \<Rightarrow> (Inr e, h')
   292    | (Inr e, h') \<Rightarrow> (Inr e, h')
   285    )"
   293    )"
   286 by auto
   294 by auto
   290 apply (induct rule:mrec_graph.induct) 
   298 apply (induct rule:mrec_graph.induct) 
   291 apply (rule accpI)
   299 apply (rule accpI)
   292 apply (erule mrec_rel.cases)
   300 apply (erule mrec_rel.cases)
   293 by simp
   301 by simp
   294 
   302 
   295 lemma f_default: "\<not> mrec_dom (f, g, x, h) \<Longrightarrow> mrec f g x h = (Inr Exn, undefined)"
   303 lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = (Inr Exn, undefined)"
   296   unfolding mrec_def 
   304   unfolding mrec_def 
   297   by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(f, g, x, h)", simplified])
   305   by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])
   298 
   306 
   299 lemma f_di_reverse: 
   307 lemma mrec_di_reverse: 
   300   assumes "\<not> mrec_dom (f, g, x, h)"
   308   assumes "\<not> mrec_dom (x, h)"
   301   shows "
   309   shows "
   302    (case Heap_Monad.execute (f x) h of
   310    (case Heap_Monad.execute (f x) h of
   303      (Inl (Inl r), h') \<Rightarrow> mrecalse
   311      (Inl (Inl r), h') \<Rightarrow> False
   304    | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (f, g, s, h')
   312    | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (s, h')
   305    | (Inr e, h') \<Rightarrow> mrecalse
   313    | (Inr e, h') \<Rightarrow> False
   306    )" 
   314    )" 
   307 using assms
   315 using assms
   308 by (auto split:prod.splits sum.splits)
   316 by (auto split:prod.splits sum.splits)
   309  (erule notE, rule accpI, elim mrec_rel.cases, simp)+
   317  (erule notE, rule accpI, elim mrec_rel.cases, simp)+
   310 
   318 
   311 
   319 
   312 lemma mrec_rule:
   320 lemma mrec_rule:
   313   "mrec f g x h = 
   321   "mrec x h = 
   314    (case Heap_Monad.execute (f x) h of
   322    (case Heap_Monad.execute (f x) h of
   315      (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
   323      (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
   316    | (Inl (Inr s), h') \<Rightarrow> 
   324    | (Inl (Inr s), h') \<Rightarrow> 
   317           (case mrec f g s h' of
   325           (case mrec s h' of
   318              (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
   326              (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
   319            | (Inr e, h'') \<Rightarrow> (Inr e, h''))
   327            | (Inr e, h'') \<Rightarrow> (Inr e, h''))
   320    | (Inr e, h') \<Rightarrow> (Inr e, h')
   328    | (Inr e, h') \<Rightarrow> (Inr e, h')
   321    )"
   329    )"
   322 apply (cases "mrec_dom (f,g,x,h)", simp)
   330 apply (cases "mrec_dom (x,h)", simp)
   323 apply (frule f_default)
   331 apply (frule mrec_default)
   324 apply (frule f_di_reverse, simp)
   332 apply (frule mrec_di_reverse, simp)
   325 by (auto split: sum.split prod.split simp: f_default)
   333 by (auto split: sum.split prod.split simp: mrec_default)
   326 
   334 
   327 
   335 
   328 definition
   336 definition
   329   "MREC f g x = Heap (mrec f g x)"
   337   "MREC x = Heap (mrec x)"
   330 
   338 
   331 lemma MREC_rule:
   339 lemma MREC_rule:
   332   "MREC f g x = 
   340   "MREC x = 
   333   (do y \<leftarrow> f x;
   341   (do y \<leftarrow> f x;
   334                 (case y of 
   342                 (case y of 
   335                 Inl r \<Rightarrow> return r
   343                 Inl r \<Rightarrow> return r
   336               | Inr s \<Rightarrow> 
   344               | Inr s \<Rightarrow> 
   337                 do z \<leftarrow> MREC f g s ;
   345                 do z \<leftarrow> MREC s ;
   338                    g x s z
   346                    g x s z
   339                 done) done)"
   347                 done) done)"
   340   unfolding MREC_def
   348   unfolding MREC_def
   341   unfolding bindM_def return_def
   349   unfolding bindM_def return_def
   342   apply simp
   350   apply simp
   343   apply (rule ext)
   351   apply (rule ext)
   344   apply (unfold mrec_rule[of f g x])
   352   apply (unfold mrec_rule[of x])
   345   by (auto split:prod.splits sum.splits)
   353   by (auto split:prod.splits sum.splits)
       
   354 
       
   355 
       
   356 lemma MREC_pinduct:
       
   357   assumes "Heap_Monad.execute (MREC x) h = (Inl r, h')"
       
   358   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"
       
   359   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
       
   360     \<Longrightarrow> Heap_Monad.execute (g x s z) h2 = (Inl r, h') \<Longrightarrow> P x h h' r"
       
   361   shows "P x h h' r"
       
   362 proof -
       
   363   from assms(1) have mrec: "mrec x h = (Inl r, h')"
       
   364     unfolding MREC_def execute.simps .
       
   365   from mrec have dom: "mrec_dom (x, h)"
       
   366     apply -
       
   367     apply (rule ccontr)
       
   368     apply (drule mrec_default) by auto
       
   369   from mrec have h'_r: "h' = (snd (mrec x h))" "r = (Sum_Type.Projl (fst (mrec x h)))"
       
   370     by auto
       
   371   from mrec have "P x h (snd (mrec x h)) (Sum_Type.Projl (fst (mrec x h)))"
       
   372   proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
       
   373     case (1 x h)
       
   374     obtain rr h' where "mrec x h = (rr, h')" by fastsimp
       
   375     obtain fret h1 where exec_f: "Heap_Monad.execute (f x) h = (fret, h1)" by fastsimp
       
   376     show ?case
       
   377     proof (cases fret)
       
   378       case (Inl a)
       
   379       note Inl' = this
       
   380       show ?thesis
       
   381       proof (cases a)
       
   382         case (Inl aa)
       
   383         from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
       
   384           by auto
       
   385       next
       
   386         case (Inr b)
       
   387         note Inr' = this
       
   388         obtain ret_mrec h2 where mrec_rec: "mrec b h1 = (ret_mrec, h2)" by fastsimp
       
   389         from this Inl 1(1) exec_f mrec show ?thesis
       
   390         proof (cases "ret_mrec")
       
   391           case (Inl aaa)
       
   392           from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3)
       
   393             show ?thesis
       
   394               apply auto
       
   395               apply (rule rec_case)
       
   396               unfolding MREC_def by auto
       
   397         next
       
   398           case (Inr b)
       
   399           from this Inl 1(1) exec_f mrec Inr' mrec_rec 1(3) show ?thesis by auto
       
   400         qed
       
   401       qed
       
   402     next
       
   403       case (Inr b)
       
   404       from this 1(1) mrec exec_f 1(3) show ?thesis by simp
       
   405     qed
       
   406   qed
       
   407   from this h'_r show ?thesis by simp
       
   408 qed
       
   409 
       
   410 end
       
   411 
       
   412 text {* Providing global versions of the constant and the theorems *}
       
   413 
       
   414 abbreviation "MREC == mrec.MREC"
       
   415 lemmas MREC_rule = mrec.MREC_rule
       
   416 lemmas MREC_pinduct = mrec.MREC_pinduct
   346 
   417 
   347 hide (open) const heap execute
   418 hide (open) const heap execute
   348 
   419 
   349 
   420 
   350 subsection {* Code generator setup *}
   421 subsection {* Code generator setup *}