changeset 36057 ca6610908ae9 parent 35423 6ef9525a5727 child 36078 59f6773a7d1d
equal 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 *}`