--- a/src/HOL/Lifting_Option.thy Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Lifting_Option.thy Wed Feb 12 08:35:56 2014 +0100
@@ -26,7 +26,7 @@
unfolding option_rel_def by simp_all
abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
- "option_pred \<equiv> option_case True"
+ "option_pred \<equiv> case_option True"
lemma option_rel_eq [relator_eq]:
"option_rel (op =) = (op =)"
@@ -100,8 +100,8 @@
lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some"
unfolding fun_rel_def by simp
-lemma option_case_transfer [transfer_rule]:
- "(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case"
+lemma case_option_transfer [transfer_rule]:
+ "(B ===> (A ===> B) ===> option_rel A ===> B) case_option case_option"
unfolding fun_rel_def split_option_all by simp
lemma option_map_transfer [transfer_rule]:
@@ -115,57 +115,4 @@
end
-
-subsubsection {* BNF setup *}
-
-lemma option_rec_conv_option_case: "option_rec = option_case"
-by (simp add: fun_eq_iff split: option.split)
-
-bnf "'a option"
- map: Option.map
- sets: Option.set
- bd: natLeq
- wits: None
- rel: option_rel
-proof -
- show "Option.map id = id" by (rule Option.map.id)
-next
- fix f g
- show "Option.map (g \<circ> f) = Option.map g \<circ> Option.map f"
- by (auto simp add: fun_eq_iff Option.map_def split: option.split)
-next
- fix f g x
- assume "\<And>z. z \<in> Option.set x \<Longrightarrow> f z = g z"
- thus "Option.map f x = Option.map g x"
- by (simp cong: Option.map_cong)
-next
- fix f
- show "Option.set \<circ> Option.map f = op ` f \<circ> Option.set"
- by fastforce
-next
- show "card_order natLeq" by (rule natLeq_card_order)
-next
- show "cinfinite natLeq" by (rule natLeq_cinfinite)
-next
- fix x
- show "|Option.set x| \<le>o natLeq"
- by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric])
-next
- fix R S
- show "option_rel R OO option_rel S \<le> option_rel (R OO S)"
- by (auto simp: option_rel_def split: option.splits)
-next
- fix z
- assume "z \<in> Option.set None"
- thus False by simp
-next
- fix R
- show "option_rel R =
- (Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
- Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
- unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
- by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
- split: option.splits)
-qed
-
end