src/HOL/Imperative_HOL/Mrec.thy
changeset 37792 ba0bc31b90d7
parent 37787 30dc3abf4a58
child 39754 150f831ce4a3
equal deleted inserted replaced
37791:0d6b64060543 37792:ba0bc31b90d7
    62 definition
    62 definition
    63   "MREC x = Heap_Monad.Heap (mrec x)"
    63   "MREC x = Heap_Monad.Heap (mrec x)"
    64 
    64 
    65 lemma MREC_rule:
    65 lemma MREC_rule:
    66   "MREC x = 
    66   "MREC x = 
    67   (do y \<leftarrow> f x;
    67   do { y \<leftarrow> f x;
    68                 (case y of 
    68                 (case y of 
    69                 Inl r \<Rightarrow> return r
    69                 Inl r \<Rightarrow> return r
    70               | Inr s \<Rightarrow> 
    70               | Inr s \<Rightarrow> 
    71                 do z \<leftarrow> MREC s ;
    71                 do { z \<leftarrow> MREC s ;
    72                    g x s z
    72                      g x s z })}"
    73                 done) done)"
       
    74   unfolding MREC_def
    73   unfolding MREC_def
    75   unfolding bind_def return_def
    74   unfolding bind_def return_def
    76   apply simp
    75   apply simp
    77   apply (rule ext)
    76   apply (rule ext)
    78   apply (unfold mrec_rule[of x])
    77   apply (unfold mrec_rule[of x])