dropped redundant transfer rules (now proved and registered by datatype and plugins)
--- a/src/HOL/Library/Quotient_List.thy Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Library/Quotient_List.thy Mon Nov 10 10:29:19 2014 +0100
@@ -117,7 +117,7 @@
and q2: "Quotient3 R2 Abs2 Rep2"
shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map"
and "((R1 ===> op =) ===> (list_all2 R1) ===> op =) map map"
- unfolding list_all2_eq [symmetric] by (rule map_transfer)+
+ unfolding list_all2_eq [symmetric] by (rule list.map_transfer)+
lemma foldr_prs_aux:
assumes a: "Quotient3 R1 abs1 rep1"
@@ -169,7 +169,7 @@
lemma [quot_respect]:
"((R ===> R ===> op =) ===> list_all2 R ===> list_all2 R ===> op =) list_all2 list_all2"
- by (rule list_all2_transfer)
+ by (rule list.rel_transfer)
lemma [quot_preserve]:
assumes a: "Quotient3 R abs1 rep1"
--- a/src/HOL/List.thy Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/List.thy Mon Nov 10 10:29:19 2014 +0100
@@ -6449,23 +6449,6 @@
begin
interpretation lifting_syntax .
-lemma Nil_transfer [transfer_rule]: "(list_all2 A) [] []"
- by simp
-
-lemma Cons_transfer [transfer_rule]:
- "(A ===> list_all2 A ===> list_all2 A) Cons Cons"
- unfolding rel_fun_def by simp
-
-lemma case_list_transfer [transfer_rule]:
- "(B ===> (A ===> list_all2 A ===> B) ===> list_all2 A ===> B)
- case_list case_list"
- unfolding rel_fun_def by (simp split: list.split)
-
-lemma rec_list_transfer [transfer_rule]:
- "(B ===> (A ===> list_all2 A ===> B ===> B) ===> list_all2 A ===> B)
- rec_list rec_list"
- unfolding rel_fun_def by (clarify, erule list_all2_induct, simp_all)
-
lemma tl_transfer [transfer_rule]:
"(list_all2 A ===> list_all2 A) tl tl"
unfolding tl_def[abs_def] by transfer_prover
@@ -6474,17 +6457,9 @@
"(list_all2 A ===> list_all2 A) butlast butlast"
by (rule rel_funI, erule list_all2_induct, auto)
-lemma set_transfer [transfer_rule]:
- "(list_all2 A ===> rel_set A) set set"
- unfolding set_rec[abs_def] by transfer_prover
-
lemma map_rec: "map f xs = rec_list Nil (%x _ y. Cons (f x) y) xs"
by (induct xs) auto
-lemma map_transfer [transfer_rule]:
- "((A ===> B) ===> list_all2 A ===> list_all2 B) map map"
- unfolding map_rec[abs_def] by transfer_prover
-
lemma append_transfer [transfer_rule]:
"(list_all2 A ===> list_all2 A ===> list_all2 A) append append"
unfolding List.append_def by transfer_prover
@@ -6596,14 +6571,6 @@
"(op = ===> list_all2 A ===> list_all2 A) rotate rotate"
unfolding rotate_def [abs_def] by transfer_prover
-lemma list_all2_transfer [transfer_rule]:
- "((A ===> B ===> op =) ===> list_all2 A ===> list_all2 B ===> op =)
- list_all2 list_all2"
- apply (subst (4) list_all2_iff [abs_def])
- apply (subst (3) list_all2_iff [abs_def])
- apply transfer_prover
- done
-
lemma sublist_transfer [transfer_rule]:
"(list_all2 A ===> rel_set (op =) ===> list_all2 A) sublist sublist"
unfolding sublist_def [abs_def] by transfer_prover
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Mon Nov 10 10:29:19 2014 +0100
@@ -39,21 +39,21 @@
subsection {* Lifted constant definitions *}
-lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric Nil_transfer .
+lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric list.ctr_transfer(1) .
-lift_definition fcons :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons parametric Cons_transfer
+lift_definition fcons :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons parametric list.ctr_transfer(2)
by simp
lift_definition fappend :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is append parametric append_transfer
by simp
-lift_definition fmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is map parametric map_transfer
+lift_definition fmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is map parametric list.map_transfer
by simp
lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is filter parametric filter_transfer
by simp
-lift_definition fset :: "'a fset \<Rightarrow> 'a set" is set parametric set_transfer
+lift_definition fset :: "'a fset \<Rightarrow> 'a set" is set parametric list.set_transfer
by simp
text {* Constants with nested types (like concat) yield a more