transfer rules for many more list constants
authorhuffman
Tue May 15 12:07:16 2012 +0200 (2012-05-15)
changeset 479293465c09222e0
parent 47928 fb2bc5a1eb32
child 47930 c06aa331bb76
transfer rules for many more list constants
src/HOL/Library/Quotient_List.thy
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Tue May 15 13:06:15 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Tue May 15 12:07:16 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Quotient infrastructure for the list type *}
     1.5  
     1.6  theory Quotient_List
     1.7 -imports Main Quotient_Set
     1.8 +imports Main Quotient_Set Quotient_Product Quotient_Option
     1.9  begin
    1.10  
    1.11  subsection {* Relator for list type *}
    1.12 @@ -123,6 +123,18 @@
    1.13      list_rec list_rec"
    1.14    unfolding fun_rel_def by (clarify, erule list_all2_induct, simp_all)
    1.15  
    1.16 +lemma tl_transfer [transfer_rule]:
    1.17 +  "(list_all2 A ===> list_all2 A) tl tl"
    1.18 +  unfolding tl_def by transfer_prover
    1.19 +
    1.20 +lemma butlast_transfer [transfer_rule]:
    1.21 +  "(list_all2 A ===> list_all2 A) butlast butlast"
    1.22 +  by (rule fun_relI, erule list_all2_induct, auto)
    1.23 +
    1.24 +lemma set_transfer [transfer_rule]:
    1.25 +  "(list_all2 A ===> set_rel A) set set"
    1.26 +  unfolding set_def by transfer_prover
    1.27 +
    1.28  lemma map_transfer [transfer_rule]:
    1.29    "((A ===> B) ===> list_all2 A ===> list_all2 B) map map"
    1.30    unfolding List.map_def by transfer_prover
    1.31 @@ -131,10 +143,18 @@
    1.32    "(list_all2 A ===> list_all2 A ===> list_all2 A) append append"
    1.33    unfolding List.append_def by transfer_prover
    1.34  
    1.35 +lemma rev_transfer [transfer_rule]:
    1.36 +  "(list_all2 A ===> list_all2 A) rev rev"
    1.37 +  unfolding List.rev_def by transfer_prover
    1.38 +
    1.39  lemma filter_transfer [transfer_rule]:
    1.40    "((A ===> op =) ===> list_all2 A ===> list_all2 A) filter filter"
    1.41    unfolding List.filter_def by transfer_prover
    1.42  
    1.43 +lemma fold_transfer [transfer_rule]:
    1.44 +  "((A ===> B ===> B) ===> list_all2 A ===> B ===> B) fold fold"
    1.45 +  unfolding List.fold_def by transfer_prover
    1.46 +
    1.47  lemma foldr_transfer [transfer_rule]:
    1.48    "((A ===> B ===> B) ===> list_all2 A ===> B ===> B) foldr foldr"
    1.49    unfolding List.foldr_def by transfer_prover
    1.50 @@ -155,26 +175,87 @@
    1.51    "(op = ===> list_all2 A ===> list_all2 A) take take"
    1.52    unfolding List.take_def by transfer_prover
    1.53  
    1.54 +lemma list_update_transfer [transfer_rule]:
    1.55 +  "(list_all2 A ===> op = ===> A ===> list_all2 A) list_update list_update"
    1.56 +  unfolding list_update_def by transfer_prover
    1.57 +
    1.58 +lemma takeWhile_transfer [transfer_rule]:
    1.59 +  "((A ===> op =) ===> list_all2 A ===> list_all2 A) takeWhile takeWhile"
    1.60 +  unfolding takeWhile_def by transfer_prover
    1.61 +
    1.62 +lemma dropWhile_transfer [transfer_rule]:
    1.63 +  "((A ===> op =) ===> list_all2 A ===> list_all2 A) dropWhile dropWhile"
    1.64 +  unfolding dropWhile_def by transfer_prover
    1.65 +
    1.66 +lemma zip_transfer [transfer_rule]:
    1.67 +  "(list_all2 A ===> list_all2 B ===> list_all2 (prod_rel A B)) zip zip"
    1.68 +  unfolding zip_def by transfer_prover
    1.69 +
    1.70 +lemma insert_transfer [transfer_rule]:
    1.71 +  assumes [transfer_rule]: "bi_unique A"
    1.72 +  shows "(A ===> list_all2 A ===> list_all2 A) List.insert List.insert"
    1.73 +  unfolding List.insert_def [abs_def] by transfer_prover
    1.74 +
    1.75 +lemma find_transfer [transfer_rule]:
    1.76 +  "((A ===> op =) ===> list_all2 A ===> option_rel A) List.find List.find"
    1.77 +  unfolding List.find_def by transfer_prover
    1.78 +
    1.79 +lemma remove1_transfer [transfer_rule]:
    1.80 +  assumes [transfer_rule]: "bi_unique A"
    1.81 +  shows "(A ===> list_all2 A ===> list_all2 A) remove1 remove1"
    1.82 +  unfolding remove1_def by transfer_prover
    1.83 +
    1.84 +lemma removeAll_transfer [transfer_rule]:
    1.85 +  assumes [transfer_rule]: "bi_unique A"
    1.86 +  shows "(A ===> list_all2 A ===> list_all2 A) removeAll removeAll"
    1.87 +  unfolding removeAll_def by transfer_prover
    1.88 +
    1.89 +lemma distinct_transfer [transfer_rule]:
    1.90 +  assumes [transfer_rule]: "bi_unique A"
    1.91 +  shows "(list_all2 A ===> op =) distinct distinct"
    1.92 +  unfolding distinct_def by transfer_prover
    1.93 +
    1.94 +lemma remdups_transfer [transfer_rule]:
    1.95 +  assumes [transfer_rule]: "bi_unique A"
    1.96 +  shows "(list_all2 A ===> list_all2 A) remdups remdups"
    1.97 +  unfolding remdups_def by transfer_prover
    1.98 +
    1.99 +lemma replicate_transfer [transfer_rule]:
   1.100 +  "(op = ===> A ===> list_all2 A) replicate replicate"
   1.101 +  unfolding replicate_def by transfer_prover
   1.102 +
   1.103  lemma length_transfer [transfer_rule]:
   1.104    "(list_all2 A ===> op =) length length"
   1.105    unfolding list_size_overloaded_def by transfer_prover
   1.106  
   1.107 -lemma list_all_transfer [transfer_rule]:
   1.108 -  "((A ===> op =) ===> list_all2 A ===> op =) list_all list_all"
   1.109 -  unfolding fun_rel_def by (clarify, erule list_all2_induct, simp_all)
   1.110 +lemma rotate1_transfer [transfer_rule]:
   1.111 +  "(list_all2 A ===> list_all2 A) rotate1 rotate1"
   1.112 +  unfolding rotate1_def by transfer_prover
   1.113 +
   1.114 +lemma funpow_transfer [transfer_rule]: (* FIXME: move to Transfer.thy *)
   1.115 +  "(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
   1.116 +  unfolding funpow_def by transfer_prover
   1.117 +
   1.118 +lemma rotate_transfer [transfer_rule]:
   1.119 +  "(op = ===> list_all2 A ===> list_all2 A) rotate rotate"
   1.120 +  unfolding rotate_def [abs_def] by transfer_prover
   1.121  
   1.122  lemma list_all2_transfer [transfer_rule]:
   1.123    "((A ===> B ===> op =) ===> list_all2 A ===> list_all2 B ===> op =)
   1.124      list_all2 list_all2"
   1.125 -  apply (rule fun_relI, rule fun_relI, erule list_all2_induct)
   1.126 -  apply (rule fun_relI, erule list_all2_induct, simp, simp)
   1.127 -  apply (rule fun_relI, erule list_all2_induct [of B])
   1.128 -  apply (simp, simp add: fun_rel_def)
   1.129 +  apply (subst (4) list_all2_def [abs_def])
   1.130 +  apply (subst (3) list_all2_def [abs_def])
   1.131 +  apply transfer_prover
   1.132    done
   1.133  
   1.134 -lemma set_transfer [transfer_rule]:
   1.135 -  "(list_all2 A ===> set_rel A) set set"
   1.136 -  unfolding set_def by transfer_prover
   1.137 +lemma sublist_transfer [transfer_rule]:
   1.138 +  "(list_all2 A ===> set_rel (op =) ===> list_all2 A) sublist sublist"
   1.139 +  unfolding sublist_def [abs_def] by transfer_prover
   1.140 +
   1.141 +lemma partition_transfer [transfer_rule]:
   1.142 +  "((A ===> op =) ===> list_all2 A ===> prod_rel (list_all2 A) (list_all2 A))
   1.143 +    partition partition"
   1.144 +  unfolding partition_def by transfer_prover
   1.145  
   1.146  lemma lists_transfer [transfer_rule]:
   1.147    "(set_rel A ===> set_rel (list_all2 A)) lists lists"
   1.148 @@ -185,6 +266,38 @@
   1.149    apply (simp only: set_rel_def list_all2_Cons2, metis lists.Cons)
   1.150    done
   1.151  
   1.152 +lemma set_Cons_transfer [transfer_rule]:
   1.153 +  "(set_rel A ===> set_rel (list_all2 A) ===> set_rel (list_all2 A))
   1.154 +    set_Cons set_Cons"
   1.155 +  unfolding fun_rel_def set_rel_def set_Cons_def
   1.156 +  apply safe
   1.157 +  apply (simp add: list_all2_Cons1, fast)
   1.158 +  apply (simp add: list_all2_Cons2, fast)
   1.159 +  done
   1.160 +
   1.161 +lemma listset_transfer [transfer_rule]:
   1.162 +  "(list_all2 (set_rel A) ===> set_rel (list_all2 A)) listset listset"
   1.163 +  unfolding listset_def by transfer_prover
   1.164 +
   1.165 +lemma null_transfer [transfer_rule]:
   1.166 +  "(list_all2 A ===> op =) List.null List.null"
   1.167 +  unfolding fun_rel_def List.null_def by auto
   1.168 +
   1.169 +lemma list_all_transfer [transfer_rule]:
   1.170 +  "((A ===> op =) ===> list_all2 A ===> op =) list_all list_all"
   1.171 +  unfolding list_all_iff [abs_def] by transfer_prover
   1.172 +
   1.173 +lemma list_ex_transfer [transfer_rule]:
   1.174 +  "((A ===> op =) ===> list_all2 A ===> op =) list_ex list_ex"
   1.175 +  unfolding list_ex_iff [abs_def] by transfer_prover
   1.176 +
   1.177 +lemma splice_transfer [transfer_rule]:
   1.178 +  "(list_all2 A ===> list_all2 A ===> list_all2 A) splice splice"
   1.179 +  apply (rule fun_relI, erule list_all2_induct, simp add: fun_rel_def, simp)
   1.180 +  apply (rule fun_relI)
   1.181 +  apply (erule_tac xs=x in list_all2_induct, simp, simp add: fun_rel_def)
   1.182 +  done
   1.183 +
   1.184  subsection {* Setup for lifting package *}
   1.185  
   1.186  lemma Quotient_list[quot_map]: