src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 37591 d3daea901123
parent 36176 3fe7e97ccca8
child 37709 70fafefbcc98
equal deleted inserted replaced
37590:180e80b4eac1 37591:d3daea901123
   377         note Inr' = this
   377         note Inr' = this
   378         obtain ret_mrec h2 where mrec_rec: "mrec b h1 = (ret_mrec, h2)" by fastsimp
   378         obtain ret_mrec h2 where mrec_rec: "mrec b h1 = (ret_mrec, h2)" by fastsimp
   379         from this Inl 1(1) exec_f mrec show ?thesis
   379         from this Inl 1(1) exec_f mrec show ?thesis
   380         proof (cases "ret_mrec")
   380         proof (cases "ret_mrec")
   381           case (Inl aaa)
   381           case (Inl aaa)
   382           from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3)
   382           from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2) [OF exec_f [symmetric] Inl' Inr', of "aaa" "h2"] 1(3)
   383             show ?thesis
   383             show ?thesis
   384               apply auto
   384               apply auto
   385               apply (rule rec_case)
   385               apply (rule rec_case)
   386               unfolding MREC_def by auto
   386               unfolding MREC_def by auto
   387         next
   387         next