--- a/src/HOL/Library/FSet.thy Tue Feb 25 15:02:19 2014 +0100
+++ b/src/HOL/Library/FSet.thy Tue Feb 25 15:02:20 2014 +0100
@@ -176,16 +176,8 @@
lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter
parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp
-lemma compose_rel_to_Domainp:
- assumes "left_unique R"
- assumes "(R ===> op=) P P'"
- shows "(R OO Lifting.invariant P' OO R\<inverse>\<inverse>) x y \<longleftrightarrow> Domainp R x \<and> P x \<and> x = y"
-using assms unfolding OO_def conversep_iff Domainp_iff left_unique_def fun_rel_def invariant_def
-by blast
-
lift_definition fPow :: "'a fset \<Rightarrow> 'a fset fset" is Pow parametric Pow_transfer
-by (subst compose_rel_to_Domainp [OF _ finite_transfer]) (auto intro: transfer_raw finite_subset
- simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq)
+by (simp add: finite_subset)
lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer .
@@ -198,9 +190,7 @@
lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer
unfolding invariant_def Set.bind_def by clarsimp metis
-lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer
-by (subst(asm) compose_rel_to_Domainp [OF _ finite_transfer])
- (auto intro: transfer_raw simp add: fset.pcr_cr_eq[symmetric] Domainp_set fset.domain_eq invariant_def)
+lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer by simp
lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer .
lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer .
--- a/src/HOL/Quotient_Examples/Lift_DList.thy Tue Feb 25 15:02:19 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy Tue Feb 25 15:02:20 2014 +0100
@@ -45,19 +45,7 @@
lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr .
-lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat"
-proof -
- {
- fix x y
- have "list_all2 cr_dlist x y \<Longrightarrow> x = List.map list_of_dlist y"
- unfolding list_all2_iff cr_dlist_def by (induction x y rule: list_induct2') auto
- }
- note cr = this
- fix x :: "'a list list" and y :: "'a list list"
- assume "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\<inverse>\<inverse>) x y"
- then have "x = y" by (auto dest: cr simp add: Lifting.invariant_def)
- then show "?thesis x y" unfolding Lifting.invariant_def by auto
-qed
+lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat" by auto
text {* We can export code: *}
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Tue Feb 25 15:02:19 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Tue Feb 25 15:02:20 2014 +0100
@@ -71,7 +71,7 @@
using Quotient_rel [OF Quotient_fset] by simp
lift_definition fconcat :: "'a fset fset \<Rightarrow> 'a fset" is concat parametric concat_transfer
-proof -
+proof (simp only: fset.pcr_cr_eq)
fix xss yss :: "'a list list"
assume "(list_all2 cr_fset OO list_eq OO (list_all2 cr_fset)\<inverse>\<inverse>) xss yss"
then obtain uss vss where