# HG changeset patch # User huffman # Date 1337076436 -7200 # Node ID 3465c09222e0099f3c635bc91136b7ab0c1e77ee # Parent fb2bc5a1eb32ba6b41c0a74a3fce0dc2db87dda6 transfer rules for many more list constants diff -r fb2bc5a1eb32 -r 3465c09222e0 src/HOL/Library/Quotient_List.thy --- 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]: