src/HOL/Lifting_Option.thy
changeset 55404 5cb95b79a51f
parent 55129 26bd1cba3ab5
child 55466 786edc984c98
     1.1 --- a/src/HOL/Lifting_Option.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Lifting_Option.thy	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4    unfolding option_rel_def by simp_all
     1.5  
     1.6  abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
     1.7 -  "option_pred \<equiv> option_case True"
     1.8 +  "option_pred \<equiv> case_option True"
     1.9  
    1.10  lemma option_rel_eq [relator_eq]:
    1.11    "option_rel (op =) = (op =)"
    1.12 @@ -100,8 +100,8 @@
    1.13  lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some"
    1.14    unfolding fun_rel_def by simp
    1.15  
    1.16 -lemma option_case_transfer [transfer_rule]:
    1.17 -  "(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case"
    1.18 +lemma case_option_transfer [transfer_rule]:
    1.19 +  "(B ===> (A ===> B) ===> option_rel A ===> B) case_option case_option"
    1.20    unfolding fun_rel_def split_option_all by simp
    1.21  
    1.22  lemma option_map_transfer [transfer_rule]:
    1.23 @@ -115,57 +115,4 @@
    1.24  
    1.25  end
    1.26  
    1.27 -
    1.28 -subsubsection {* BNF setup *}
    1.29 -
    1.30 -lemma option_rec_conv_option_case: "option_rec = option_case"
    1.31 -by (simp add: fun_eq_iff split: option.split)
    1.32 -
    1.33 -bnf "'a option"
    1.34 -  map: Option.map
    1.35 -  sets: Option.set
    1.36 -  bd: natLeq
    1.37 -  wits: None
    1.38 -  rel: option_rel
    1.39 -proof -
    1.40 -  show "Option.map id = id" by (rule Option.map.id)
    1.41 -next
    1.42 -  fix f g
    1.43 -  show "Option.map (g \<circ> f) = Option.map g \<circ> Option.map f"
    1.44 -    by (auto simp add: fun_eq_iff Option.map_def split: option.split)
    1.45 -next
    1.46 -  fix f g x
    1.47 -  assume "\<And>z. z \<in> Option.set x \<Longrightarrow> f z = g z"
    1.48 -  thus "Option.map f x = Option.map g x"
    1.49 -    by (simp cong: Option.map_cong)
    1.50 -next
    1.51 -  fix f
    1.52 -  show "Option.set \<circ> Option.map f = op ` f \<circ> Option.set"
    1.53 -    by fastforce
    1.54 -next
    1.55 -  show "card_order natLeq" by (rule natLeq_card_order)
    1.56 -next
    1.57 -  show "cinfinite natLeq" by (rule natLeq_cinfinite)
    1.58 -next
    1.59 -  fix x
    1.60 -  show "|Option.set x| \<le>o natLeq"
    1.61 -    by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric])
    1.62 -next
    1.63 -  fix R S
    1.64 -  show "option_rel R OO option_rel S \<le> option_rel (R OO S)"
    1.65 -    by (auto simp: option_rel_def split: option.splits)
    1.66 -next
    1.67 -  fix z
    1.68 -  assume "z \<in> Option.set None"
    1.69 -  thus False by simp
    1.70 -next
    1.71 -  fix R
    1.72 -  show "option_rel R =
    1.73 -        (Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
    1.74 -         Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
    1.75 -  unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
    1.76 -  by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
    1.77 -           split: option.splits)
    1.78 -qed
    1.79 -
    1.80  end