src/HOL/Library/While_Combinator.thy
changeset 55466 786edc984c98
parent 54196 0c188a3c671a
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Feb 14 07:53:45 2014 +0100
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -85,7 +85,7 @@
     1.4  assumes TestCommute: "\<And>s. P s \<Longrightarrow> b s = b' (f s)"
     1.5  assumes BodyCommute: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> f (c s) = c' (f s)"
     1.6  assumes Initial: "P s"
     1.7 -shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
     1.8 +shows "map_option f (while_option b c s) = while_option b' c' (f s)"
     1.9  unfolding while_option_def
    1.10  proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject)
    1.11    fix k
    1.12 @@ -188,7 +188,7 @@
    1.13  
    1.14  lemma while_option_commute:
    1.15    assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" 
    1.16 -  shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
    1.17 +  shows "map_option f (while_option b c s) = while_option b' c' (f s)"
    1.18  by(rule while_option_commute_invariant[where P = "\<lambda>_. True"])
    1.19    (auto simp add: assms)
    1.20