# HG changeset patch
# User traytel
# Date 1415611759 -3600
# Node ID 7c507e6640476106fb0a00e4dd0976ea48dc9bf5
# Parent  4bee6d8c15004624578a572a2201c35f2bef3c1e
dropped redundant transfer rules (now proved and registered by datatype and plugins)

diff -r 4bee6d8c1500 -r 7c507e664047 src/HOL/Library/Quotient_List.thy
--- 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"
diff -r 4bee6d8c1500 -r 7c507e664047 src/HOL/List.thy
--- 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
diff -r 4bee6d8c1500 -r 7c507e664047 src/HOL/Quotient_Examples/Lift_FSet.thy
--- 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