# HG changeset patch
# User kuncar
# Date 1376402362 -7200
# Node ID 3fbcfa9118631a43d41ddc0fa8ef353e40e6c549
# Parent  cb82606b82157a1844212548e9ef95864e8a37e1
remove unnecessary dependencies on Library/Quotient_*

diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/BNF/Countable_Type.thy
--- a/src/HOL/BNF/Countable_Type.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/BNF/Countable_Type.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -11,7 +11,6 @@
 imports
   "~~/src/HOL/Cardinals/Cardinals"
   "~~/src/HOL/Library/Countable_Set"
-  "~~/src/HOL/Library/Quotient_Set"
 begin
 
 subsection{* Cardinal stuff *}
@@ -76,7 +75,7 @@
   ..
 lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
   by (rule countable_empty)
-lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric insert_transfer
+lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
   by (rule countable_insert)
 lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}"
   by (rule countable_insert[OF countable_empty])
diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/BNF/Examples/Derivation_Trees/DTree.thy
--- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -11,7 +11,7 @@
 imports Prelim
 begin
 
-hide_fact (open) Quotient_Product.prod_rel_def
+hide_fact (open) Lifting_Product.prod_rel_def
 
 typedecl N
 typedecl T
diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/BNF/Examples/Process.thy
--- a/src/HOL/BNF/Examples/Process.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/BNF/Examples/Process.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -11,7 +11,7 @@
 imports "../BNF"
 begin
 
-hide_fact (open) Quotient_Product.prod_rel_def
+hide_fact (open) Lifting_Product.prod_rel_def
 
 codatatype 'a process =
   isAction: Action (prefOf: 'a) (contOf: "'a process") |
diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/BNF/Examples/TreeFsetI.thy
--- a/src/HOL/BNF/Examples/TreeFsetI.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -12,7 +12,7 @@
 imports "../BNF"
 begin
 
-hide_fact (open) Quotient_Product.prod_rel_def
+hide_fact (open) Lifting_Product.prod_rel_def
 
 codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
 
diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -421,9 +421,15 @@
 shows "mmap f M = mmap g M"
 using assms by transfer (auto intro!: setsum_cong)
 
+context
+begin
+interpretation lifting_syntax .
+
 lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\<lambda>f. {a. 0 < f a}) set_of"
   unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto
 
+end
+
 lemma set_of_mmap: "set_of o mmap h = image h o set_of"
 proof (rule ext, unfold o_apply)
   fix M show "set_of (mmap h M) = h ` set_of M"
diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/IMP/Abs_Int_init.thy
--- a/src/HOL/IMP/Abs_Int_init.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_init.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -1,6 +1,5 @@
 theory Abs_Int_init
 imports "~~/src/HOL/Library/While_Combinator"
-        "~~/src/HOL/Library/Quotient_List"
         "~~/src/HOL/Library/Extended"
         Vars Collecting Abs_Int_Tests
 begin
diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/Library/Mapping.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -5,11 +5,15 @@
 header {* An abstract view on maps for code generation. *}
 
 theory Mapping
-imports Main Quotient_Option Quotient_List
+imports Main
 begin
 
 subsection {* Parametricity transfer rules *}
 
+context
+begin
+interpretation lifting_syntax .
+
 lemma empty_transfer: "(A ===> option_rel B) Map.empty Map.empty" by transfer_prover
 
 lemma lookup_transfer: "((A ===> B) ===> A ===> B) (\<lambda>m k. m k) (\<lambda>m k. m k)" by transfer_prover
@@ -72,6 +76,8 @@
       | Some v \<Rightarrow> m (k \<mapsto> (f v))))"
 by transfer_prover
 
+end
+
 subsection {* Type definition and primitive operations *}
 
 typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
@@ -154,12 +160,17 @@
 
 end
 
+context
+begin
+interpretation lifting_syntax .
+
 lemma [transfer_rule]:
   assumes [transfer_rule]: "bi_total A"
   assumes [transfer_rule]: "bi_unique B"
-  shows  "fun_rel (pcr_mapping A B) (fun_rel (pcr_mapping A B) HOL.iff) HOL.eq HOL.equal"
+  shows  "(pcr_mapping A B ===> pcr_mapping A B ===> op=) HOL.eq HOL.equal"
 by (unfold equal) transfer_prover
 
+end
 
 subsection {* Properties *}
 
diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/Library/RBT.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -5,7 +5,7 @@
 header {* Abstract type of RBT trees *}
 
 theory RBT 
-imports Main RBT_Impl Quotient_List
+imports Main RBT_Impl
 begin
 
 subsection {* Type definition *}
diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/Quotient_Examples/Lift_DList.thy
--- a/src/HOL/Quotient_Examples/Lift_DList.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -3,7 +3,7 @@
 *)
 
 theory Lift_DList
-imports Main "~~/src/HOL/Library/Quotient_List"
+imports Main
 begin
 
 subsection {* The type of distinct lists *}
diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -5,7 +5,7 @@
 header {* Lifting and transfer with a finite set type *}
 
 theory Lift_FSet
-imports "~~/src/HOL/Library/Quotient_List"
+imports Main
 begin
 
 subsection {* Equivalence relation and quotient type definition *}
@@ -25,6 +25,10 @@
 lemma equivp_list_eq: "equivp list_eq"
   by (intro equivpI reflp_list_eq symp_list_eq transp_list_eq)
 
+context
+begin
+interpretation lifting_syntax .
+
 lemma list_eq_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"
   shows "(list_all2 A ===> list_all2 A ===> op =) list_eq list_eq"
@@ -85,6 +89,13 @@
     done
 qed
 
+lemma member_transfer:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(A ===> list_all2 A ===> op=) (\<lambda>x xs. x \<in> set xs) (\<lambda>x xs. x \<in> set xs)"
+by transfer_prover
+
+end
+
 syntax
   "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
 
@@ -92,11 +103,6 @@
   "{|x, xs|}" == "CONST fcons x {|xs|}"
   "{|x|}"     == "CONST fcons x {||}"
 
-lemma member_transfer:
-  assumes [transfer_rule]: "bi_unique A"
-  shows "(A ===> list_all2 A ===> op=) (\<lambda>x xs. x \<in> set xs) (\<lambda>x xs. x \<in> set xs)"
-by transfer_prover
-
 lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is "\<lambda>x xs. x \<in> set xs"
    parametric member_transfer by simp
 
diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/ex/Transfer_Int_Nat.thy
--- a/src/HOL/ex/Transfer_Int_Nat.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/ex/Transfer_Int_Nat.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -5,7 +5,7 @@
 header {* Using the transfer method between nat and int *}
 
 theory Transfer_Int_Nat
-imports GCD "~~/src/HOL/Library/Quotient_List"
+imports GCD
 begin
 
 subsection {* Correspondence relation *}
@@ -20,6 +20,10 @@
 
 subsection {* Transfer rules *}
 
+context
+begin
+interpretation lifting_syntax .
+
 lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
   unfolding ZN_def bi_unique_def by simp
 
@@ -115,6 +119,8 @@
 lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
   unfolding listsum_def [abs_def] by transfer_prover
 
+end
+
 subsection {* Transfer examples *}
 
 lemma