# HG changeset patch
# User kuncar
# Date 1393336940 -3600
# Node ID 07906fc6af7a1e8db706769a2e1b98d71abbe731
# Parent  66df76dd26400348af6c0cb1472f2a5e8a49d4cb
simplify and repair proofs due to df0fda378813

diff -r 66df76dd2640 -r 07906fc6af7a src/HOL/Library/FSet.thy
--- 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 .
diff -r 66df76dd2640 -r 07906fc6af7a src/HOL/Quotient_Examples/Lift_DList.thy
--- 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: *}
 
diff -r 66df76dd2640 -r 07906fc6af7a src/HOL/Quotient_Examples/Lift_FSet.thy
--- 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