src/HOL/Library/Quotient_List.thy
changeset 47929 3465c09222e0
parent 47923 ba9df9685e7c
child 47936 756f30eac792
--- a/src/HOL/Library/Quotient_List.thy	Tue May 15 13:06:15 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Tue May 15 12:07:16 2012 +0200
@@ -5,7 +5,7 @@
 header {* Quotient infrastructure for the list type *}
 
 theory Quotient_List
-imports Main Quotient_Set
+imports Main Quotient_Set Quotient_Product Quotient_Option
 begin
 
 subsection {* Relator for list type *}
@@ -123,6 +123,18 @@
     list_rec list_rec"
   unfolding fun_rel_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 by transfer_prover
+
+lemma butlast_transfer [transfer_rule]:
+  "(list_all2 A ===> list_all2 A) butlast butlast"
+  by (rule fun_relI, erule list_all2_induct, auto)
+
+lemma set_transfer [transfer_rule]:
+  "(list_all2 A ===> set_rel A) set set"
+  unfolding set_def by transfer_prover
+
 lemma map_transfer [transfer_rule]:
   "((A ===> B) ===> list_all2 A ===> list_all2 B) map map"
   unfolding List.map_def by transfer_prover
@@ -131,10 +143,18 @@
   "(list_all2 A ===> list_all2 A ===> list_all2 A) append append"
   unfolding List.append_def by transfer_prover
 
+lemma rev_transfer [transfer_rule]:
+  "(list_all2 A ===> list_all2 A) rev rev"
+  unfolding List.rev_def by transfer_prover
+
 lemma filter_transfer [transfer_rule]:
   "((A ===> op =) ===> list_all2 A ===> list_all2 A) filter filter"
   unfolding List.filter_def by transfer_prover
 
+lemma fold_transfer [transfer_rule]:
+  "((A ===> B ===> B) ===> list_all2 A ===> B ===> B) fold fold"
+  unfolding List.fold_def by transfer_prover
+
 lemma foldr_transfer [transfer_rule]:
   "((A ===> B ===> B) ===> list_all2 A ===> B ===> B) foldr foldr"
   unfolding List.foldr_def by transfer_prover
@@ -155,26 +175,87 @@
   "(op = ===> list_all2 A ===> list_all2 A) take take"
   unfolding List.take_def by transfer_prover
 
+lemma list_update_transfer [transfer_rule]:
+  "(list_all2 A ===> op = ===> A ===> list_all2 A) list_update list_update"
+  unfolding list_update_def by transfer_prover
+
+lemma takeWhile_transfer [transfer_rule]:
+  "((A ===> op =) ===> list_all2 A ===> list_all2 A) takeWhile takeWhile"
+  unfolding takeWhile_def by transfer_prover
+
+lemma dropWhile_transfer [transfer_rule]:
+  "((A ===> op =) ===> list_all2 A ===> list_all2 A) dropWhile dropWhile"
+  unfolding dropWhile_def by transfer_prover
+
+lemma zip_transfer [transfer_rule]:
+  "(list_all2 A ===> list_all2 B ===> list_all2 (prod_rel A B)) zip zip"
+  unfolding zip_def by transfer_prover
+
+lemma insert_transfer [transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(A ===> list_all2 A ===> list_all2 A) List.insert List.insert"
+  unfolding List.insert_def [abs_def] by transfer_prover
+
+lemma find_transfer [transfer_rule]:
+  "((A ===> op =) ===> list_all2 A ===> option_rel A) List.find List.find"
+  unfolding List.find_def by transfer_prover
+
+lemma remove1_transfer [transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(A ===> list_all2 A ===> list_all2 A) remove1 remove1"
+  unfolding remove1_def by transfer_prover
+
+lemma removeAll_transfer [transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(A ===> list_all2 A ===> list_all2 A) removeAll removeAll"
+  unfolding removeAll_def by transfer_prover
+
+lemma distinct_transfer [transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(list_all2 A ===> op =) distinct distinct"
+  unfolding distinct_def by transfer_prover
+
+lemma remdups_transfer [transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(list_all2 A ===> list_all2 A) remdups remdups"
+  unfolding remdups_def by transfer_prover
+
+lemma replicate_transfer [transfer_rule]:
+  "(op = ===> A ===> list_all2 A) replicate replicate"
+  unfolding replicate_def by transfer_prover
+
 lemma length_transfer [transfer_rule]:
   "(list_all2 A ===> op =) length length"
   unfolding list_size_overloaded_def by transfer_prover
 
-lemma list_all_transfer [transfer_rule]:
-  "((A ===> op =) ===> list_all2 A ===> op =) list_all list_all"
-  unfolding fun_rel_def by (clarify, erule list_all2_induct, simp_all)
+lemma rotate1_transfer [transfer_rule]:
+  "(list_all2 A ===> list_all2 A) rotate1 rotate1"
+  unfolding rotate1_def by transfer_prover
+
+lemma funpow_transfer [transfer_rule]: (* FIXME: move to Transfer.thy *)
+  "(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
+  unfolding funpow_def by transfer_prover
+
+lemma rotate_transfer [transfer_rule]:
+  "(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 (rule fun_relI, rule fun_relI, erule list_all2_induct)
-  apply (rule fun_relI, erule list_all2_induct, simp, simp)
-  apply (rule fun_relI, erule list_all2_induct [of B])
-  apply (simp, simp add: fun_rel_def)
+  apply (subst (4) list_all2_def [abs_def])
+  apply (subst (3) list_all2_def [abs_def])
+  apply transfer_prover
   done
 
-lemma set_transfer [transfer_rule]:
-  "(list_all2 A ===> set_rel A) set set"
-  unfolding set_def by transfer_prover
+lemma sublist_transfer [transfer_rule]:
+  "(list_all2 A ===> set_rel (op =) ===> list_all2 A) sublist sublist"
+  unfolding sublist_def [abs_def] by transfer_prover
+
+lemma partition_transfer [transfer_rule]:
+  "((A ===> op =) ===> list_all2 A ===> prod_rel (list_all2 A) (list_all2 A))
+    partition partition"
+  unfolding partition_def by transfer_prover
 
 lemma lists_transfer [transfer_rule]:
   "(set_rel A ===> set_rel (list_all2 A)) lists lists"
@@ -185,6 +266,38 @@
   apply (simp only: set_rel_def list_all2_Cons2, metis lists.Cons)
   done
 
+lemma set_Cons_transfer [transfer_rule]:
+  "(set_rel A ===> set_rel (list_all2 A) ===> set_rel (list_all2 A))
+    set_Cons set_Cons"
+  unfolding fun_rel_def set_rel_def set_Cons_def
+  apply safe
+  apply (simp add: list_all2_Cons1, fast)
+  apply (simp add: list_all2_Cons2, fast)
+  done
+
+lemma listset_transfer [transfer_rule]:
+  "(list_all2 (set_rel A) ===> set_rel (list_all2 A)) listset listset"
+  unfolding listset_def by transfer_prover
+
+lemma null_transfer [transfer_rule]:
+  "(list_all2 A ===> op =) List.null List.null"
+  unfolding fun_rel_def List.null_def by auto
+
+lemma list_all_transfer [transfer_rule]:
+  "((A ===> op =) ===> list_all2 A ===> op =) list_all list_all"
+  unfolding list_all_iff [abs_def] by transfer_prover
+
+lemma list_ex_transfer [transfer_rule]:
+  "((A ===> op =) ===> list_all2 A ===> op =) list_ex list_ex"
+  unfolding list_ex_iff [abs_def] by transfer_prover
+
+lemma splice_transfer [transfer_rule]:
+  "(list_all2 A ===> list_all2 A ===> list_all2 A) splice splice"
+  apply (rule fun_relI, erule list_all2_induct, simp add: fun_rel_def, simp)
+  apply (rule fun_relI)
+  apply (erule_tac xs=x in list_all2_induct, simp, simp add: fun_rel_def)
+  done
+
 subsection {* Setup for lifting package *}
 
 lemma Quotient_list[quot_map]: