--- 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])
--- 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
--- 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") |
--- 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")
--- 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"
--- 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
--- 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 *}
--- 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 *}
--- 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 *}
--- 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
--- 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