src/HOL/Imperative_HOL/Mrec.thy
changeset 37787 30dc3abf4a58
parent 37772 026ed2fc15d4
child 37792 ba0bc31b90d7
equal deleted inserted replaced
37786:4eb98849c5c0 37787:30dc3abf4a58
    74   unfolding MREC_def
    74   unfolding MREC_def
    75   unfolding bind_def return_def
    75   unfolding bind_def return_def
    76   apply simp
    76   apply simp
    77   apply (rule ext)
    77   apply (rule ext)
    78   apply (unfold mrec_rule[of x])
    78   apply (unfold mrec_rule[of x])
    79   by (auto split: option.splits prod.splits sum.splits)
    79   by (auto simp add: execute_simps split: option.splits prod.splits sum.splits)
    80 
    80 
    81 lemma MREC_pinduct:
    81 lemma MREC_pinduct:
    82   assumes "execute (MREC x) h = Some (r, h')"
    82   assumes "execute (MREC x) h = Some (r, h')"
    83   assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
    83   assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
    84   assumes rec_case: "\<And> x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \<Longrightarrow> execute (MREC s) h1 = Some (z, h2) \<Longrightarrow> P s h1 h2 z
    84   assumes rec_case: "\<And> x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \<Longrightarrow> execute (MREC s) h1 = Some (z, h2) \<Longrightarrow> P s h1 h2 z