# HG changeset patch # User kuncar # Date 1376402362 -7200 # Node ID cb82606b82157a1844212548e9ef95864e8a37e1 # Parent aeee0a4be6cfad98f1790b2a02e5a588e4c7c978 move Lifting/Transfer relevant parts of Library/Quotient_* to Main diff -r aeee0a4be6cf -r cb82606b8215 src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Tue Aug 13 15:59:22 2013 +0200 +++ b/src/HOL/Library/Quotient_List.thy Tue Aug 13 15:59:22 2013 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Library/Quotient_List.thy - Author: Cezary Kaliszyk, Christian Urban and Brian Huffman + Author: Cezary Kaliszyk and Christian Urban *) header {* Quotient infrastructure for the list type *} @@ -8,13 +8,13 @@ imports Main Quotient_Set Quotient_Product Quotient_Option begin -subsection {* Relator for list type *} +subsection {* Rules for the Quotient package *} lemma map_id [id_simps]: "map id = id" by (fact List.map.id) -lemma list_all2_eq [id_simps, relator_eq]: +lemma list_all2_eq [id_simps]: "list_all2 (op =) = (op =)" proof (rule ext)+ fix xs ys @@ -22,66 +22,6 @@ by (induct xs ys rule: list_induct2') simp_all qed -lemma list_all2_mono[relator_mono]: - assumes "A \ B" - shows "(list_all2 A) \ (list_all2 B)" -using assms by (auto intro: list_all2_mono) - -lemma list_all2_OO[relator_distr]: "list_all2 A OO list_all2 B = list_all2 (A OO B)" -proof (intro ext iffI) - fix xs ys - assume "list_all2 (A OO B) xs ys" - thus "(list_all2 A OO list_all2 B) xs ys" - unfolding OO_def - by (induct, simp, simp add: list_all2_Cons1 list_all2_Cons2, fast) -next - fix xs ys - assume "(list_all2 A OO list_all2 B) xs ys" - then obtain zs where "list_all2 A xs zs" and "list_all2 B zs ys" .. - thus "list_all2 (A OO B) xs ys" - by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast) -qed - -lemma Domainp_list[relator_domain]: - assumes "Domainp A = P" - shows "Domainp (list_all2 A) = (list_all P)" -proof - - { - fix x - have *: "\x. (\y. A x y) = P x" using assms unfolding Domainp_iff by blast - have "(\y. (list_all2 A x y)) = list_all P x" - by (induction x) (simp_all add: * list_all2_Cons1) - } - then show ?thesis - unfolding Domainp_iff[abs_def] - by (auto iff: fun_eq_iff) -qed - -lemma reflp_list_all2[reflexivity_rule]: - assumes "reflp R" - shows "reflp (list_all2 R)" -proof (rule reflpI) - from assms have *: "\xs. R xs xs" by (rule reflpE) - fix xs - show "list_all2 R xs xs" - by (induct xs) (simp_all add: *) -qed - -lemma left_total_list_all2[reflexivity_rule]: - "left_total R \ left_total (list_all2 R)" - unfolding left_total_def - apply safe - apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1) -done - -lemma left_unique_list_all2 [reflexivity_rule]: - "left_unique R \ left_unique (list_all2 R)" - unfolding left_unique_def - apply (subst (2) all_comm, subst (1) all_comm) - apply (rule allI, rename_tac zs, induct_tac zs) - apply (auto simp add: list_all2_Cons2) - done - lemma list_symp: assumes "symp R" shows "symp (list_all2 R)" @@ -108,272 +48,6 @@ "equivp R \ equivp (list_all2 R)" by (blast intro: equivpI reflp_list_all2 list_symp list_transp elim: equivpE) -lemma right_total_list_all2 [transfer_rule]: - "right_total R \ right_total (list_all2 R)" - unfolding right_total_def - by (rule allI, induct_tac y, simp, simp add: list_all2_Cons2) - -lemma right_unique_list_all2 [transfer_rule]: - "right_unique R \ right_unique (list_all2 R)" - unfolding right_unique_def - apply (rule allI, rename_tac xs, induct_tac xs) - apply (auto simp add: list_all2_Cons1) - done - -lemma bi_total_list_all2 [transfer_rule]: - "bi_total A \ bi_total (list_all2 A)" - unfolding bi_total_def - apply safe - apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1) - apply (rename_tac ys, induct_tac ys, simp, simp add: list_all2_Cons2) - done - -lemma bi_unique_list_all2 [transfer_rule]: - "bi_unique A \ bi_unique (list_all2 A)" - unfolding bi_unique_def - apply (rule conjI) - apply (rule allI, rename_tac xs, induct_tac xs) - apply (simp, force simp add: list_all2_Cons1) - apply (subst (2) all_comm, subst (1) all_comm) - apply (rule allI, rename_tac xs, induct_tac xs) - apply (simp, force simp add: list_all2_Cons2) - done - -subsection {* Transfer rules for transfer package *} - -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 fun_rel_def by simp - -lemma list_case_transfer [transfer_rule]: - "(B ===> (A ===> list_all2 A ===> B) ===> list_all2 A ===> B) - list_case list_case" - unfolding fun_rel_def by (simp split: list.split) - -lemma list_rec_transfer [transfer_rule]: - "(B ===> (A ===> list_all2 A ===> B ===> B) ===> list_all2 A ===> B) - 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 - -lemma append_transfer [transfer_rule]: - "(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 - -lemma foldl_transfer [transfer_rule]: - "((B ===> A ===> B) ===> B ===> list_all2 A ===> B) foldl foldl" - unfolding List.foldl_def by transfer_prover - -lemma concat_transfer [transfer_rule]: - "(list_all2 (list_all2 A) ===> list_all2 A) concat concat" - unfolding List.concat_def by transfer_prover - -lemma drop_transfer [transfer_rule]: - "(op = ===> list_all2 A ===> list_all2 A) drop drop" - unfolding List.drop_def by transfer_prover - -lemma take_transfer [transfer_rule]: - "(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 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 (subst (4) list_all2_def [abs_def]) - apply (subst (3) list_all2_def [abs_def]) - apply transfer_prover - done - -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" - apply (rule fun_relI, rule set_relI) - apply (erule lists.induct, simp) - apply (simp only: set_rel_def list_all2_Cons1, metis lists.Cons) - apply (erule lists.induct, simp) - 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 - -lemma listsum_transfer[transfer_rule]: - assumes [transfer_rule]: "A 0 0" - assumes [transfer_rule]: "(A ===> A ===> A) op + op +" - shows "(list_all2 A ===> A) listsum listsum" - unfolding listsum_def[abs_def] - by transfer_prover - -subsection {* Setup for lifting package *} - -lemma Quotient_list[quot_map]: - assumes "Quotient R Abs Rep T" - shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)" -proof (unfold Quotient_alt_def, intro conjI allI impI) - from assms have 1: "\x y. T x y \ Abs x = y" - unfolding Quotient_alt_def by simp - fix xs ys assume "list_all2 T xs ys" thus "map Abs xs = ys" - by (induct, simp, simp add: 1) -next - from assms have 2: "\x. T (Rep x) x" - unfolding Quotient_alt_def by simp - fix xs show "list_all2 T (map Rep xs) xs" - by (induct xs, simp, simp add: 2) -next - from assms have 3: "\x y. R x y \ T x (Abs x) \ T y (Abs y) \ Abs x = Abs y" - unfolding Quotient_alt_def by simp - fix xs ys show "list_all2 R xs ys \ list_all2 T xs (map Abs xs) \ - list_all2 T ys (map Abs ys) \ map Abs xs = map Abs ys" - by (induct xs ys rule: list_induct2', simp_all, metis 3) -qed - -lemma list_invariant_commute [invariant_commute]: - "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)" - apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def) - apply (intro allI) - apply (induct_tac rule: list_induct2') - apply simp_all - apply metis -done - -subsection {* Rules for quotient package *} - lemma list_quotient3 [quot_thm]: assumes "Quotient3 R Abs Rep" shows "Quotient3 (list_all2 R) (map Abs) (map Rep)" diff -r aeee0a4be6cf -r cb82606b8215 src/HOL/Library/Quotient_Option.thy --- a/src/HOL/Library/Quotient_Option.thy Tue Aug 13 15:59:22 2013 +0200 +++ b/src/HOL/Library/Quotient_Option.thy Tue Aug 13 15:59:22 2013 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Library/Quotient_Option.thy - Author: Cezary Kaliszyk, Christian Urban and Brian Huffman + Author: Cezary Kaliszyk and Christian Urban *) header {* Quotient infrastructure for the option type *} @@ -8,31 +8,7 @@ imports Main Quotient_Syntax begin -subsection {* Relator for option type *} - -fun - option_rel :: "('a \ 'b \ bool) \ 'a option \ 'b option \ bool" -where - "option_rel R None None = True" -| "option_rel R (Some x) None = False" -| "option_rel R None (Some x) = False" -| "option_rel R (Some x) (Some y) = R x y" - -lemma option_rel_unfold: - "option_rel R x y = (case (x, y) of (None, None) \ True - | (Some x, Some y) \ R x y - | _ \ False)" - by (cases x) (cases y, simp_all)+ - -fun option_pred :: "('a \ bool) \ 'a option \ bool" -where - "option_pred R None = True" -| "option_pred R (Some x) = R x" - -lemma option_pred_unfold: - "option_pred P x = (case x of None \ True - | Some x \ P x)" -by (cases x) simp_all +subsection {* Rules for the Quotient package *} lemma option_rel_map1: "option_rel R (Option.map f x) y \ option_rel (\x. R (f x)) x y" @@ -46,37 +22,10 @@ "Option.map id = id" by (simp add: id_def Option.map.identity fun_eq_iff) -lemma option_rel_eq [id_simps, relator_eq]: +lemma option_rel_eq [id_simps]: "option_rel (op =) = (op =)" by (simp add: option_rel_unfold fun_eq_iff split: option.split) -lemma option_rel_mono[relator_mono]: - assumes "A \ B" - shows "(option_rel A) \ (option_rel B)" -using assms by (auto simp: option_rel_unfold split: option.splits) - -lemma option_rel_OO[relator_distr]: - "(option_rel A) OO (option_rel B) = option_rel (A OO B)" -by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split) - -lemma Domainp_option[relator_domain]: - assumes "Domainp A = P" - shows "Domainp (option_rel A) = (option_pred P)" -using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def] -by (auto iff: fun_eq_iff split: option.split) - -lemma reflp_option_rel[reflexivity_rule]: - "reflp R \ reflp (option_rel R)" - unfolding reflp_def split_option_all by simp - -lemma left_total_option_rel[reflexivity_rule]: - "left_total R \ left_total (option_rel R)" - unfolding left_total_def split_option_all split_option_ex by simp - -lemma left_unique_option_rel [reflexivity_rule]: - "left_unique R \ left_unique (option_rel R)" - unfolding left_unique_def split_option_all by simp - lemma option_symp: "symp R \ symp (option_rel R)" unfolding symp_def split_option_all option_rel.simps by fast @@ -89,65 +38,6 @@ "equivp R \ equivp (option_rel R)" by (blast intro: equivpI reflp_option_rel option_symp option_transp elim: equivpE) -lemma right_total_option_rel [transfer_rule]: - "right_total R \ right_total (option_rel R)" - unfolding right_total_def split_option_all split_option_ex by simp - -lemma right_unique_option_rel [transfer_rule]: - "right_unique R \ right_unique (option_rel R)" - unfolding right_unique_def split_option_all by simp - -lemma bi_total_option_rel [transfer_rule]: - "bi_total R \ bi_total (option_rel R)" - unfolding bi_total_def split_option_all split_option_ex by simp - -lemma bi_unique_option_rel [transfer_rule]: - "bi_unique R \ bi_unique (option_rel R)" - unfolding bi_unique_def split_option_all by simp - -subsection {* Transfer rules for transfer package *} - -lemma None_transfer [transfer_rule]: "(option_rel A) None None" - by simp - -lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some" - unfolding fun_rel_def by simp - -lemma option_case_transfer [transfer_rule]: - "(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case" - unfolding fun_rel_def split_option_all by simp - -lemma option_map_transfer [transfer_rule]: - "((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map" - unfolding Option.map_def by transfer_prover - -lemma option_bind_transfer [transfer_rule]: - "(option_rel A ===> (A ===> option_rel B) ===> option_rel B) - Option.bind Option.bind" - unfolding fun_rel_def split_option_all by simp - -subsection {* Setup for lifting package *} - -lemma Quotient_option[quot_map]: - assumes "Quotient R Abs Rep T" - shows "Quotient (option_rel R) (Option.map Abs) - (Option.map Rep) (option_rel T)" - using assms unfolding Quotient_alt_def option_rel_unfold - by (simp split: option.split) - -lemma option_invariant_commute [invariant_commute]: - "option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)" - apply (simp add: fun_eq_iff Lifting.invariant_def) - apply (intro allI) - apply (case_tac x rule: option.exhaust) - apply (case_tac xa rule: option.exhaust) - apply auto[2] - apply (case_tac xa rule: option.exhaust) - apply auto -done - -subsection {* Rules for quotient package *} - lemma option_quotient [quot_thm]: assumes "Quotient3 R Abs Rep" shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)" diff -r aeee0a4be6cf -r cb82606b8215 src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Tue Aug 13 15:59:22 2013 +0200 +++ b/src/HOL/Library/Quotient_Product.thy Tue Aug 13 15:59:22 2013 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Library/Quotient_Product.thy - Author: Cezary Kaliszyk, Christian Urban and Brian Huffman + Author: Cezary Kaliszyk and Christian Urban *) header {* Quotient infrastructure for the product type *} @@ -8,137 +8,22 @@ imports Main Quotient_Syntax begin -subsection {* Relator for product type *} - -definition - prod_rel :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a \ 'c \ 'b \ 'd \ bool" -where - "prod_rel R1 R2 = (\(a, b) (c, d). R1 a c \ R2 b d)" - -definition prod_pred :: "('a \ bool) \ ('b \ bool) \ 'a \ 'b \ bool" -where "prod_pred R1 R2 = (\(a, b). R1 a \ R2 b)" - -lemma prod_rel_apply [simp]: - "prod_rel R1 R2 (a, b) (c, d) \ R1 a c \ R2 b d" - by (simp add: prod_rel_def) - -lemma prod_pred_apply [simp]: - "prod_pred P1 P2 (a, b) \ P1 a \ P2 b" - by (simp add: prod_pred_def) +subsection {* Rules for the Quotient package *} lemma map_pair_id [id_simps]: shows "map_pair id id = id" by (simp add: fun_eq_iff) -lemma prod_rel_eq [id_simps, relator_eq]: +lemma prod_rel_eq [id_simps]: shows "prod_rel (op =) (op =) = (op =)" by (simp add: fun_eq_iff) -lemma prod_rel_mono[relator_mono]: - assumes "A \ C" - assumes "B \ D" - shows "(prod_rel A B) \ (prod_rel C D)" -using assms by (auto simp: prod_rel_def) - -lemma prod_rel_OO[relator_distr]: - "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)" -by (rule ext)+ (auto simp: prod_rel_def OO_def) - -lemma Domainp_prod[relator_domain]: - assumes "Domainp T1 = P1" - assumes "Domainp T2 = P2" - shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)" -using assms unfolding prod_rel_def prod_pred_def by blast - -lemma reflp_prod_rel [reflexivity_rule]: - assumes "reflp R1" - assumes "reflp R2" - shows "reflp (prod_rel R1 R2)" -using assms by (auto intro!: reflpI elim: reflpE) - -lemma left_total_prod_rel [reflexivity_rule]: - assumes "left_total R1" - assumes "left_total R2" - shows "left_total (prod_rel R1 R2)" - using assms unfolding left_total_def prod_rel_def by auto - -lemma left_unique_prod_rel [reflexivity_rule]: - assumes "left_unique R1" and "left_unique R2" - shows "left_unique (prod_rel R1 R2)" - using assms unfolding left_unique_def prod_rel_def by auto - lemma prod_equivp [quot_equiv]: assumes "equivp R1" assumes "equivp R2" shows "equivp (prod_rel R1 R2)" using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE) -lemma right_total_prod_rel [transfer_rule]: - assumes "right_total R1" and "right_total R2" - shows "right_total (prod_rel R1 R2)" - using assms unfolding right_total_def prod_rel_def by auto - -lemma right_unique_prod_rel [transfer_rule]: - assumes "right_unique R1" and "right_unique R2" - shows "right_unique (prod_rel R1 R2)" - using assms unfolding right_unique_def prod_rel_def by auto - -lemma bi_total_prod_rel [transfer_rule]: - assumes "bi_total R1" and "bi_total R2" - shows "bi_total (prod_rel R1 R2)" - using assms unfolding bi_total_def prod_rel_def by auto - -lemma bi_unique_prod_rel [transfer_rule]: - assumes "bi_unique R1" and "bi_unique R2" - shows "bi_unique (prod_rel R1 R2)" - using assms unfolding bi_unique_def prod_rel_def by auto - -subsection {* Transfer rules for transfer package *} - -lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair" - unfolding fun_rel_def prod_rel_def by simp - -lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst" - unfolding fun_rel_def prod_rel_def by simp - -lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd" - unfolding fun_rel_def prod_rel_def by simp - -lemma prod_case_transfer [transfer_rule]: - "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case" - unfolding fun_rel_def prod_rel_def by simp - -lemma curry_transfer [transfer_rule]: - "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry" - unfolding curry_def by transfer_prover - -lemma map_pair_transfer [transfer_rule]: - "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D) - map_pair map_pair" - unfolding map_pair_def [abs_def] by transfer_prover - -lemma prod_rel_transfer [transfer_rule]: - "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> - prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel" - unfolding fun_rel_def by auto - -subsection {* Setup for lifting package *} - -lemma Quotient_prod[quot_map]: - assumes "Quotient R1 Abs1 Rep1 T1" - assumes "Quotient R2 Abs2 Rep2 T2" - shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) - (map_pair Rep1 Rep2) (prod_rel T1 T2)" - using assms unfolding Quotient_alt_def by auto - -lemma prod_invariant_commute [invariant_commute]: - "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)" - apply (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) - apply blast -done - -subsection {* Rules for quotient package *} - lemma prod_quotient [quot_thm]: assumes "Quotient3 R1 Abs1 Rep1" assumes "Quotient3 R2 Abs2 Rep2" diff -r aeee0a4be6cf -r cb82606b8215 src/HOL/Library/Quotient_Set.thy --- a/src/HOL/Library/Quotient_Set.thy Tue Aug 13 15:59:22 2013 +0200 +++ b/src/HOL/Library/Quotient_Set.thy Tue Aug 13 15:59:22 2013 +0200 @@ -8,273 +8,7 @@ imports Main Quotient_Syntax begin -subsection {* Relator for set type *} - -definition set_rel :: "('a \ 'b \ bool) \ 'a set \ 'b set \ bool" - where "set_rel R = (\A B. (\x\A. \y\B. R x y) \ (\y\B. \x\A. R x y))" - -lemma set_relI: - assumes "\x. x \ A \ \y\B. R x y" - assumes "\y. y \ B \ \x\A. R x y" - shows "set_rel R A B" - using assms unfolding set_rel_def by simp - -lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)" - unfolding set_rel_def by auto - -lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)" - unfolding set_rel_def fun_eq_iff by auto - -lemma set_rel_mono[relator_mono]: - assumes "A \ B" - shows "set_rel A \ set_rel B" -using assms unfolding set_rel_def by blast - -lemma set_rel_OO[relator_distr]: "set_rel R OO set_rel S = set_rel (R OO S)" - apply (rule sym) - apply (intro ext, rename_tac X Z) - apply (rule iffI) - apply (rule_tac b="{y. (\x\X. R x y) \ (\z\Z. S y z)}" in relcomppI) - apply (simp add: set_rel_def, fast) - apply (simp add: set_rel_def, fast) - apply (simp add: set_rel_def, fast) - done - -lemma Domainp_set[relator_domain]: - assumes "Domainp T = R" - shows "Domainp (set_rel T) = (\A. Ball A R)" -using assms unfolding set_rel_def Domainp_iff[abs_def] -apply (intro ext) -apply (rule iffI) -apply blast -apply (rename_tac A, rule_tac x="{y. \x\A. T x y}" in exI, fast) -done - -lemma reflp_set_rel[reflexivity_rule]: "reflp R \ reflp (set_rel R)" - unfolding reflp_def set_rel_def by fast - -lemma left_total_set_rel[reflexivity_rule]: - "left_total A \ left_total (set_rel A)" - unfolding left_total_def set_rel_def - apply safe - apply (rename_tac X, rule_tac x="{y. \x\X. A x y}" in exI, fast) -done - -lemma left_unique_set_rel[reflexivity_rule]: - "left_unique A \ left_unique (set_rel A)" - unfolding left_unique_def set_rel_def - by fast - -lemma symp_set_rel: "symp R \ symp (set_rel R)" - unfolding symp_def set_rel_def by fast - -lemma transp_set_rel: "transp R \ transp (set_rel R)" - unfolding transp_def set_rel_def by fast - -lemma equivp_set_rel: "equivp R \ equivp (set_rel R)" - by (blast intro: equivpI reflp_set_rel symp_set_rel transp_set_rel - elim: equivpE) - -lemma right_total_set_rel [transfer_rule]: - "right_total A \ right_total (set_rel A)" - unfolding right_total_def set_rel_def - by (rule allI, rename_tac Y, rule_tac x="{x. \y\Y. A x y}" in exI, fast) - -lemma right_unique_set_rel [transfer_rule]: - "right_unique A \ right_unique (set_rel A)" - unfolding right_unique_def set_rel_def by fast - -lemma bi_total_set_rel [transfer_rule]: - "bi_total A \ bi_total (set_rel A)" - unfolding bi_total_def set_rel_def - apply safe - apply (rename_tac X, rule_tac x="{y. \x\X. A x y}" in exI, fast) - apply (rename_tac Y, rule_tac x="{x. \y\Y. A x y}" in exI, fast) - done - -lemma bi_unique_set_rel [transfer_rule]: - "bi_unique A \ bi_unique (set_rel A)" - unfolding bi_unique_def set_rel_def by fast - -subsection {* Transfer rules for transfer package *} - -subsubsection {* Unconditional transfer rules *} - -lemma empty_transfer [transfer_rule]: "(set_rel A) {} {}" - unfolding set_rel_def by simp - -lemma insert_transfer [transfer_rule]: - "(A ===> set_rel A ===> set_rel A) insert insert" - unfolding fun_rel_def set_rel_def by auto - -lemma union_transfer [transfer_rule]: - "(set_rel A ===> set_rel A ===> set_rel A) union union" - unfolding fun_rel_def set_rel_def by auto - -lemma Union_transfer [transfer_rule]: - "(set_rel (set_rel A) ===> set_rel A) Union Union" - unfolding fun_rel_def set_rel_def by simp fast - -lemma image_transfer [transfer_rule]: - "((A ===> B) ===> set_rel A ===> set_rel B) image image" - unfolding fun_rel_def set_rel_def by simp fast - -lemma UNION_transfer [transfer_rule]: - "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) UNION UNION" - unfolding SUP_def [abs_def] by transfer_prover - -lemma Ball_transfer [transfer_rule]: - "(set_rel A ===> (A ===> op =) ===> op =) Ball Ball" - unfolding set_rel_def fun_rel_def by fast - -lemma Bex_transfer [transfer_rule]: - "(set_rel A ===> (A ===> op =) ===> op =) Bex Bex" - unfolding set_rel_def fun_rel_def by fast - -lemma Pow_transfer [transfer_rule]: - "(set_rel A ===> set_rel (set_rel A)) Pow Pow" - apply (rule fun_relI, rename_tac X Y, rule set_relI) - apply (rename_tac X', rule_tac x="{y\Y. \x\X'. A x y}" in rev_bexI, clarsimp) - apply (simp add: set_rel_def, fast) - apply (rename_tac Y', rule_tac x="{x\X. \y\Y'. A x y}" in rev_bexI, clarsimp) - apply (simp add: set_rel_def, fast) - done - -lemma set_rel_transfer [transfer_rule]: - "((A ===> B ===> op =) ===> set_rel A ===> set_rel B ===> op =) - set_rel set_rel" - unfolding fun_rel_def set_rel_def by fast - - -subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *} - -lemma member_transfer [transfer_rule]: - assumes "bi_unique A" - shows "(A ===> set_rel A ===> op =) (op \) (op \)" - using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast - -lemma right_total_Collect_transfer[transfer_rule]: - assumes "right_total A" - shows "((A ===> op =) ===> set_rel A) (\P. Collect (\x. P x \ Domainp A x)) Collect" - using assms unfolding right_total_def set_rel_def fun_rel_def Domainp_iff by fast - -lemma Collect_transfer [transfer_rule]: - assumes "bi_total A" - shows "((A ===> op =) ===> set_rel A) Collect Collect" - using assms unfolding fun_rel_def set_rel_def bi_total_def by fast - -lemma inter_transfer [transfer_rule]: - assumes "bi_unique A" - shows "(set_rel A ===> set_rel A ===> set_rel A) inter inter" - using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast - -lemma Diff_transfer [transfer_rule]: - assumes "bi_unique A" - shows "(set_rel A ===> set_rel A ===> set_rel A) (op -) (op -)" - using assms unfolding fun_rel_def set_rel_def bi_unique_def - unfolding Ball_def Bex_def Diff_eq - by (safe, simp, metis, simp, metis) - -lemma subset_transfer [transfer_rule]: - assumes [transfer_rule]: "bi_unique A" - shows "(set_rel A ===> set_rel A ===> op =) (op \) (op \)" - unfolding subset_eq [abs_def] by transfer_prover - -lemma right_total_UNIV_transfer[transfer_rule]: - assumes "right_total A" - shows "(set_rel A) (Collect (Domainp A)) UNIV" - using assms unfolding right_total_def set_rel_def Domainp_iff by blast - -lemma UNIV_transfer [transfer_rule]: - assumes "bi_total A" - shows "(set_rel A) UNIV UNIV" - using assms unfolding set_rel_def bi_total_def by simp - -lemma right_total_Compl_transfer [transfer_rule]: - assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" - shows "(set_rel A ===> set_rel A) (\S. uminus S \ Collect (Domainp A)) uminus" - unfolding Compl_eq [abs_def] - by (subst Collect_conj_eq[symmetric]) transfer_prover - -lemma Compl_transfer [transfer_rule]: - assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" - shows "(set_rel A ===> set_rel A) uminus uminus" - unfolding Compl_eq [abs_def] by transfer_prover - -lemma right_total_Inter_transfer [transfer_rule]: - assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" - shows "(set_rel (set_rel A) ===> set_rel A) (\S. Inter S \ Collect (Domainp A)) Inter" - unfolding Inter_eq[abs_def] - by (subst Collect_conj_eq[symmetric]) transfer_prover - -lemma Inter_transfer [transfer_rule]: - assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" - shows "(set_rel (set_rel A) ===> set_rel A) Inter Inter" - unfolding Inter_eq [abs_def] by transfer_prover - -lemma filter_transfer [transfer_rule]: - assumes [transfer_rule]: "bi_unique A" - shows "((A ===> op=) ===> set_rel A ===> set_rel A) Set.filter Set.filter" - unfolding Set.filter_def[abs_def] fun_rel_def set_rel_def by blast - -lemma bi_unique_set_rel_lemma: - assumes "bi_unique R" and "set_rel R X Y" - obtains f where "Y = image f X" and "inj_on f X" and "\x\X. R x (f x)" -proof - let ?f = "\x. THE y. R x y" - from assms show f: "\x\X. R x (?f x)" - apply (clarsimp simp add: set_rel_def) - apply (drule (1) bspec, clarify) - apply (rule theI2, assumption) - apply (simp add: bi_unique_def) - apply assumption - done - from assms show "Y = image ?f X" - apply safe - apply (clarsimp simp add: set_rel_def) - apply (drule (1) bspec, clarify) - apply (rule image_eqI) - apply (rule the_equality [symmetric], assumption) - apply (simp add: bi_unique_def) - apply assumption - apply (clarsimp simp add: set_rel_def) - apply (frule (1) bspec, clarify) - apply (rule theI2, assumption) - apply (clarsimp simp add: bi_unique_def) - apply (simp add: bi_unique_def, metis) - done - show "inj_on ?f X" - apply (rule inj_onI) - apply (drule f [rule_format]) - apply (drule f [rule_format]) - apply (simp add: assms(1) [unfolded bi_unique_def]) - done -qed - -lemma finite_transfer [transfer_rule]: - "bi_unique A \ (set_rel A ===> op =) finite finite" - by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, - auto dest: finite_imageD) - -lemma card_transfer [transfer_rule]: - "bi_unique A \ (set_rel A ===> op =) card card" - by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image) - -subsection {* Setup for lifting package *} - -lemma Quotient_set[quot_map]: - assumes "Quotient R Abs Rep T" - shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)" - using assms unfolding Quotient_alt_def4 - apply (simp add: set_rel_OO[symmetric] set_rel_conversep) - apply (simp add: set_rel_def, fast) - done - -lemma set_invariant_commute [invariant_commute]: - "set_rel (Lifting.invariant P) = Lifting.invariant (\A. Ball A P)" - unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast - -subsection {* Contravariant set map (vimage) and set relator *} +subsection {* Contravariant set map (vimage) and set relator, rules for the Quotient package *} definition "vset_rel R xs ys \ \x y. R x y \ x \ xs \ y \ ys" diff -r aeee0a4be6cf -r cb82606b8215 src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Tue Aug 13 15:59:22 2013 +0200 +++ b/src/HOL/Library/Quotient_Sum.thy Tue Aug 13 15:59:22 2013 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Library/Quotient_Sum.thy - Author: Cezary Kaliszyk, Christian Urban and Brian Huffman + Author: Cezary Kaliszyk and Christian Urban *) header {* Quotient infrastructure for the sum type *} @@ -8,31 +8,7 @@ imports Main Quotient_Syntax begin -subsection {* Relator for sum type *} - -fun - sum_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ 'a + 'b \ 'c + 'd \ bool" -where - "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" -| "sum_rel R1 R2 (Inl a1) (Inr b2) = False" -| "sum_rel R1 R2 (Inr a2) (Inl b1) = False" -| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" - -lemma sum_rel_unfold: - "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \ R1 x y - | (Inr x, Inr y) \ R2 x y - | _ \ False)" - by (cases x) (cases y, simp_all)+ - -fun sum_pred :: "('a \ bool) \ ('b \ bool) \ 'a + 'b \ bool" -where - "sum_pred P1 P2 (Inl a) = P1 a" -| "sum_pred P1 P2 (Inr a) = P2 a" - -lemma sum_pred_unfold: - "sum_pred P1 P2 x = (case x of Inl x \ P1 x - | Inr x \ P2 x)" -by (cases x) simp_all +subsection {* Rules for the Quotient package *} lemma sum_rel_map1: "sum_rel R1 R2 (sum_map f1 f2 x) y \ sum_rel (\x. R1 (f1 x)) (\x. R2 (f2 x)) x y" @@ -46,39 +22,10 @@ "sum_map id id = id" by (simp add: id_def sum_map.identity fun_eq_iff) -lemma sum_rel_eq [id_simps, relator_eq]: +lemma sum_rel_eq [id_simps]: "sum_rel (op =) (op =) = (op =)" by (simp add: sum_rel_unfold fun_eq_iff split: sum.split) -lemma sum_rel_mono[relator_mono]: - assumes "A \ C" - assumes "B \ D" - shows "(sum_rel A B) \ (sum_rel C D)" -using assms by (auto simp: sum_rel_unfold split: sum.splits) - -lemma sum_rel_OO[relator_distr]: - "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)" -by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split) - -lemma Domainp_sum[relator_domain]: - assumes "Domainp R1 = P1" - assumes "Domainp R2 = P2" - shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)" -using assms -by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split) - -lemma reflp_sum_rel[reflexivity_rule]: - "reflp R1 \ reflp R2 \ reflp (sum_rel R1 R2)" - unfolding reflp_def split_sum_all sum_rel.simps by fast - -lemma left_total_sum_rel[reflexivity_rule]: - "left_total R1 \ left_total R2 \ left_total (sum_rel R1 R2)" - using assms unfolding left_total_def split_sum_all split_sum_ex by simp - -lemma left_unique_sum_rel [reflexivity_rule]: - "left_unique R1 \ left_unique R2 \ left_unique (sum_rel R1 R2)" - using assms unfolding left_unique_def split_sum_all by simp - lemma sum_symp: "symp R1 \ symp R2 \ symp (sum_rel R1 R2)" unfolding symp_def split_sum_all sum_rel.simps by fast @@ -91,50 +38,6 @@ "equivp R1 \ equivp R2 \ equivp (sum_rel R1 R2)" by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE) -lemma right_total_sum_rel [transfer_rule]: - "right_total R1 \ right_total R2 \ right_total (sum_rel R1 R2)" - unfolding right_total_def split_sum_all split_sum_ex by simp - -lemma right_unique_sum_rel [transfer_rule]: - "right_unique R1 \ right_unique R2 \ right_unique (sum_rel R1 R2)" - unfolding right_unique_def split_sum_all by simp - -lemma bi_total_sum_rel [transfer_rule]: - "bi_total R1 \ bi_total R2 \ bi_total (sum_rel R1 R2)" - using assms unfolding bi_total_def split_sum_all split_sum_ex by simp - -lemma bi_unique_sum_rel [transfer_rule]: - "bi_unique R1 \ bi_unique R2 \ bi_unique (sum_rel R1 R2)" - using assms unfolding bi_unique_def split_sum_all by simp - -subsection {* Transfer rules for transfer package *} - -lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl" - unfolding fun_rel_def by simp - -lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr" - unfolding fun_rel_def by simp - -lemma sum_case_transfer [transfer_rule]: - "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case" - unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split) - -subsection {* Setup for lifting package *} - -lemma Quotient_sum[quot_map]: - assumes "Quotient R1 Abs1 Rep1 T1" - assumes "Quotient R2 Abs2 Rep2 T2" - shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) - (sum_map Rep1 Rep2) (sum_rel T1 T2)" - using assms unfolding Quotient_alt_def - by (simp add: split_sum_all) - -lemma sum_invariant_commute [invariant_commute]: - "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)" - by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_unfold sum_pred_unfold split: sum.split) - -subsection {* Rules for quotient package *} - lemma sum_quotient [quot_thm]: assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2" diff -r aeee0a4be6cf -r cb82606b8215 src/HOL/Lifting_Option.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Lifting_Option.thy Tue Aug 13 15:59:22 2013 +0200 @@ -0,0 +1,125 @@ +(* Title: HOL/Lifting_Option.thy + Author: Brian Huffman and Ondrej Kuncar +*) + +header {* Setup for Lifting/Transfer for the option type *} + +theory Lifting_Option +imports Lifting FunDef +begin + +subsection {* Relator and predicator properties *} + +fun + option_rel :: "('a \ 'b \ bool) \ 'a option \ 'b option \ bool" +where + "option_rel R None None = True" +| "option_rel R (Some x) None = False" +| "option_rel R None (Some x) = False" +| "option_rel R (Some x) (Some y) = R x y" + +lemma option_rel_unfold: + "option_rel R x y = (case (x, y) of (None, None) \ True + | (Some x, Some y) \ R x y + | _ \ False)" + by (cases x) (cases y, simp_all)+ + +fun option_pred :: "('a \ bool) \ 'a option \ bool" +where + "option_pred R None = True" +| "option_pred R (Some x) = R x" + +lemma option_pred_unfold: + "option_pred P x = (case x of None \ True + | Some x \ P x)" +by (cases x) simp_all + +lemma option_rel_eq [relator_eq]: + "option_rel (op =) = (op =)" + by (simp add: option_rel_unfold fun_eq_iff split: option.split) + +lemma option_rel_mono[relator_mono]: + assumes "A \ B" + shows "(option_rel A) \ (option_rel B)" +using assms by (auto simp: option_rel_unfold split: option.splits) + +lemma option_rel_OO[relator_distr]: + "(option_rel A) OO (option_rel B) = option_rel (A OO B)" +by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split) + +lemma Domainp_option[relator_domain]: + assumes "Domainp A = P" + shows "Domainp (option_rel A) = (option_pred P)" +using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def] +by (auto iff: fun_eq_iff split: option.split) + +lemma reflp_option_rel[reflexivity_rule]: + "reflp R \ reflp (option_rel R)" + unfolding reflp_def split_option_all by simp + +lemma left_total_option_rel[reflexivity_rule]: + "left_total R \ left_total (option_rel R)" + unfolding left_total_def split_option_all split_option_ex by simp + +lemma left_unique_option_rel [reflexivity_rule]: + "left_unique R \ left_unique (option_rel R)" + unfolding left_unique_def split_option_all by simp + +lemma right_total_option_rel [transfer_rule]: + "right_total R \ right_total (option_rel R)" + unfolding right_total_def split_option_all split_option_ex by simp + +lemma right_unique_option_rel [transfer_rule]: + "right_unique R \ right_unique (option_rel R)" + unfolding right_unique_def split_option_all by simp + +lemma bi_total_option_rel [transfer_rule]: + "bi_total R \ bi_total (option_rel R)" + unfolding bi_total_def split_option_all split_option_ex by simp + +lemma bi_unique_option_rel [transfer_rule]: + "bi_unique R \ bi_unique (option_rel R)" + unfolding bi_unique_def split_option_all by simp + +lemma option_invariant_commute [invariant_commute]: + "option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)" + by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all) + +subsection {* Quotient theorem for the Lifting package *} + +lemma Quotient_option[quot_map]: + assumes "Quotient R Abs Rep T" + shows "Quotient (option_rel R) (Option.map Abs) + (Option.map Rep) (option_rel T)" + using assms unfolding Quotient_alt_def option_rel_unfold + by (simp split: option.split) + +subsection {* Transfer rules for the Transfer package *} + +context +begin +interpretation lifting_syntax . + +lemma None_transfer [transfer_rule]: "(option_rel A) None None" + by simp + +lemma Some_transfer [transfer_rule]: "(A ===> option_rel A) Some Some" + unfolding fun_rel_def by simp + +lemma option_case_transfer [transfer_rule]: + "(B ===> (A ===> B) ===> option_rel A ===> B) option_case option_case" + unfolding fun_rel_def split_option_all by simp + +lemma option_map_transfer [transfer_rule]: + "((A ===> B) ===> option_rel A ===> option_rel B) Option.map Option.map" + unfolding Option.map_def by transfer_prover + +lemma option_bind_transfer [transfer_rule]: + "(option_rel A ===> (A ===> option_rel B) ===> option_rel B) + Option.bind Option.bind" + unfolding fun_rel_def split_option_all by simp + +end + +end + diff -r aeee0a4be6cf -r cb82606b8215 src/HOL/Lifting_Product.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Lifting_Product.thy Tue Aug 13 15:59:22 2013 +0200 @@ -0,0 +1,135 @@ +(* Title: HOL/Lifting_Product.thy + Author: Brian Huffman and Ondrej Kuncar +*) + +header {* Setup for Lifting/Transfer for the product type *} + +theory Lifting_Product +imports Lifting +begin + +subsection {* Relator and predicator properties *} + +definition + prod_rel :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a \ 'c \ 'b \ 'd \ bool" +where + "prod_rel R1 R2 = (\(a, b) (c, d). R1 a c \ R2 b d)" + +definition prod_pred :: "('a \ bool) \ ('b \ bool) \ 'a \ 'b \ bool" +where "prod_pred R1 R2 = (\(a, b). R1 a \ R2 b)" + +lemma prod_rel_apply [simp]: + "prod_rel R1 R2 (a, b) (c, d) \ R1 a c \ R2 b d" + by (simp add: prod_rel_def) + +lemma prod_pred_apply [simp]: + "prod_pred P1 P2 (a, b) \ P1 a \ P2 b" + by (simp add: prod_pred_def) + +lemma prod_rel_eq [relator_eq]: + shows "prod_rel (op =) (op =) = (op =)" + by (simp add: fun_eq_iff) + +lemma prod_rel_mono[relator_mono]: + assumes "A \ C" + assumes "B \ D" + shows "(prod_rel A B) \ (prod_rel C D)" +using assms by (auto simp: prod_rel_def) + +lemma prod_rel_OO[relator_distr]: + "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)" +by (rule ext)+ (auto simp: prod_rel_def OO_def) + +lemma Domainp_prod[relator_domain]: + assumes "Domainp T1 = P1" + assumes "Domainp T2 = P2" + shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)" +using assms unfolding prod_rel_def prod_pred_def by blast + +lemma reflp_prod_rel [reflexivity_rule]: + assumes "reflp R1" + assumes "reflp R2" + shows "reflp (prod_rel R1 R2)" +using assms by (auto intro!: reflpI elim: reflpE) + +lemma left_total_prod_rel [reflexivity_rule]: + assumes "left_total R1" + assumes "left_total R2" + shows "left_total (prod_rel R1 R2)" + using assms unfolding left_total_def prod_rel_def by auto + +lemma left_unique_prod_rel [reflexivity_rule]: + assumes "left_unique R1" and "left_unique R2" + shows "left_unique (prod_rel R1 R2)" + using assms unfolding left_unique_def prod_rel_def by auto + +lemma right_total_prod_rel [transfer_rule]: + assumes "right_total R1" and "right_total R2" + shows "right_total (prod_rel R1 R2)" + using assms unfolding right_total_def prod_rel_def by auto + +lemma right_unique_prod_rel [transfer_rule]: + assumes "right_unique R1" and "right_unique R2" + shows "right_unique (prod_rel R1 R2)" + using assms unfolding right_unique_def prod_rel_def by auto + +lemma bi_total_prod_rel [transfer_rule]: + assumes "bi_total R1" and "bi_total R2" + shows "bi_total (prod_rel R1 R2)" + using assms unfolding bi_total_def prod_rel_def by auto + +lemma bi_unique_prod_rel [transfer_rule]: + assumes "bi_unique R1" and "bi_unique R2" + shows "bi_unique (prod_rel R1 R2)" + using assms unfolding bi_unique_def prod_rel_def by auto + +lemma prod_invariant_commute [invariant_commute]: + "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)" + by (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) blast + +subsection {* Quotient theorem for the Lifting package *} + +lemma Quotient_prod[quot_map]: + assumes "Quotient R1 Abs1 Rep1 T1" + assumes "Quotient R2 Abs2 Rep2 T2" + shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) + (map_pair Rep1 Rep2) (prod_rel T1 T2)" + using assms unfolding Quotient_alt_def by auto + +subsection {* Transfer rules for the Transfer package *} + +context +begin +interpretation lifting_syntax . + +lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair" + unfolding fun_rel_def prod_rel_def by simp + +lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst" + unfolding fun_rel_def prod_rel_def by simp + +lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd" + unfolding fun_rel_def prod_rel_def by simp + +lemma prod_case_transfer [transfer_rule]: + "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case" + unfolding fun_rel_def prod_rel_def by simp + +lemma curry_transfer [transfer_rule]: + "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry" + unfolding curry_def by transfer_prover + +lemma map_pair_transfer [transfer_rule]: + "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D) + map_pair map_pair" + unfolding map_pair_def [abs_def] by transfer_prover + +lemma prod_rel_transfer [transfer_rule]: + "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> + prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel" + unfolding fun_rel_def by auto + +end + +end + diff -r aeee0a4be6cf -r cb82606b8215 src/HOL/Lifting_Set.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Lifting_Set.thy Tue Aug 13 15:59:22 2013 +0200 @@ -0,0 +1,273 @@ +(* Title: HOL/Lifting_Set.thy + Author: Brian Huffman and Ondrej Kuncar +*) + +header {* Setup for Lifting/Transfer for the set type *} + +theory Lifting_Set +imports Lifting +begin + +subsection {* Relator and predicator properties *} + +definition set_rel :: "('a \ 'b \ bool) \ 'a set \ 'b set \ bool" + where "set_rel R = (\A B. (\x\A. \y\B. R x y) \ (\y\B. \x\A. R x y))" + +lemma set_relI: + assumes "\x. x \ A \ \y\B. R x y" + assumes "\y. y \ B \ \x\A. R x y" + shows "set_rel R A B" + using assms unfolding set_rel_def by simp + +lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)" + unfolding set_rel_def by auto + +lemma set_rel_eq [relator_eq]: "set_rel (op =) = (op =)" + unfolding set_rel_def fun_eq_iff by auto + +lemma set_rel_mono[relator_mono]: + assumes "A \ B" + shows "set_rel A \ set_rel B" +using assms unfolding set_rel_def by blast + +lemma set_rel_OO[relator_distr]: "set_rel R OO set_rel S = set_rel (R OO S)" + apply (rule sym) + apply (intro ext, rename_tac X Z) + apply (rule iffI) + apply (rule_tac b="{y. (\x\X. R x y) \ (\z\Z. S y z)}" in relcomppI) + apply (simp add: set_rel_def, fast) + apply (simp add: set_rel_def, fast) + apply (simp add: set_rel_def, fast) + done + +lemma Domainp_set[relator_domain]: + assumes "Domainp T = R" + shows "Domainp (set_rel T) = (\A. Ball A R)" +using assms unfolding set_rel_def Domainp_iff[abs_def] +apply (intro ext) +apply (rule iffI) +apply blast +apply (rename_tac A, rule_tac x="{y. \x\A. T x y}" in exI, fast) +done + +lemma reflp_set_rel[reflexivity_rule]: "reflp R \ reflp (set_rel R)" + unfolding reflp_def set_rel_def by fast + +lemma left_total_set_rel[reflexivity_rule]: + "left_total A \ left_total (set_rel A)" + unfolding left_total_def set_rel_def + apply safe + apply (rename_tac X, rule_tac x="{y. \x\X. A x y}" in exI, fast) +done + +lemma left_unique_set_rel[reflexivity_rule]: + "left_unique A \ left_unique (set_rel A)" + unfolding left_unique_def set_rel_def + by fast + +lemma right_total_set_rel [transfer_rule]: + "right_total A \ right_total (set_rel A)" + unfolding right_total_def set_rel_def + by (rule allI, rename_tac Y, rule_tac x="{x. \y\Y. A x y}" in exI, fast) + +lemma right_unique_set_rel [transfer_rule]: + "right_unique A \ right_unique (set_rel A)" + unfolding right_unique_def set_rel_def by fast + +lemma bi_total_set_rel [transfer_rule]: + "bi_total A \ bi_total (set_rel A)" + unfolding bi_total_def set_rel_def + apply safe + apply (rename_tac X, rule_tac x="{y. \x\X. A x y}" in exI, fast) + apply (rename_tac Y, rule_tac x="{x. \y\Y. A x y}" in exI, fast) + done + +lemma bi_unique_set_rel [transfer_rule]: + "bi_unique A \ bi_unique (set_rel A)" + unfolding bi_unique_def set_rel_def by fast + +lemma set_invariant_commute [invariant_commute]: + "set_rel (Lifting.invariant P) = Lifting.invariant (\A. Ball A P)" + unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast + +subsection {* Quotient theorem for the Lifting package *} + +lemma Quotient_set[quot_map]: + assumes "Quotient R Abs Rep T" + shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)" + using assms unfolding Quotient_alt_def4 + apply (simp add: set_rel_OO[symmetric] set_rel_conversep) + apply (simp add: set_rel_def, fast) + done + +subsection {* Transfer rules for the Transfer package *} + +subsubsection {* Unconditional transfer rules *} + +context +begin +interpretation lifting_syntax . + +lemma empty_transfer [transfer_rule]: "(set_rel A) {} {}" + unfolding set_rel_def by simp + +lemma insert_transfer [transfer_rule]: + "(A ===> set_rel A ===> set_rel A) insert insert" + unfolding fun_rel_def set_rel_def by auto + +lemma union_transfer [transfer_rule]: + "(set_rel A ===> set_rel A ===> set_rel A) union union" + unfolding fun_rel_def set_rel_def by auto + +lemma Union_transfer [transfer_rule]: + "(set_rel (set_rel A) ===> set_rel A) Union Union" + unfolding fun_rel_def set_rel_def by simp fast + +lemma image_transfer [transfer_rule]: + "((A ===> B) ===> set_rel A ===> set_rel B) image image" + unfolding fun_rel_def set_rel_def by simp fast + +lemma UNION_transfer [transfer_rule]: + "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) UNION UNION" + unfolding SUP_def [abs_def] by transfer_prover + +lemma Ball_transfer [transfer_rule]: + "(set_rel A ===> (A ===> op =) ===> op =) Ball Ball" + unfolding set_rel_def fun_rel_def by fast + +lemma Bex_transfer [transfer_rule]: + "(set_rel A ===> (A ===> op =) ===> op =) Bex Bex" + unfolding set_rel_def fun_rel_def by fast + +lemma Pow_transfer [transfer_rule]: + "(set_rel A ===> set_rel (set_rel A)) Pow Pow" + apply (rule fun_relI, rename_tac X Y, rule set_relI) + apply (rename_tac X', rule_tac x="{y\Y. \x\X'. A x y}" in rev_bexI, clarsimp) + apply (simp add: set_rel_def, fast) + apply (rename_tac Y', rule_tac x="{x\X. \y\Y'. A x y}" in rev_bexI, clarsimp) + apply (simp add: set_rel_def, fast) + done + +lemma set_rel_transfer [transfer_rule]: + "((A ===> B ===> op =) ===> set_rel A ===> set_rel B ===> op =) + set_rel set_rel" + unfolding fun_rel_def set_rel_def by fast + + +subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *} + +lemma member_transfer [transfer_rule]: + assumes "bi_unique A" + shows "(A ===> set_rel A ===> op =) (op \) (op \)" + using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast + +lemma right_total_Collect_transfer[transfer_rule]: + assumes "right_total A" + shows "((A ===> op =) ===> set_rel A) (\P. Collect (\x. P x \ Domainp A x)) Collect" + using assms unfolding right_total_def set_rel_def fun_rel_def Domainp_iff by fast + +lemma Collect_transfer [transfer_rule]: + assumes "bi_total A" + shows "((A ===> op =) ===> set_rel A) Collect Collect" + using assms unfolding fun_rel_def set_rel_def bi_total_def by fast + +lemma inter_transfer [transfer_rule]: + assumes "bi_unique A" + shows "(set_rel A ===> set_rel A ===> set_rel A) inter inter" + using assms unfolding fun_rel_def set_rel_def bi_unique_def by fast + +lemma Diff_transfer [transfer_rule]: + assumes "bi_unique A" + shows "(set_rel A ===> set_rel A ===> set_rel A) (op -) (op -)" + using assms unfolding fun_rel_def set_rel_def bi_unique_def + unfolding Ball_def Bex_def Diff_eq + by (safe, simp, metis, simp, metis) + +lemma subset_transfer [transfer_rule]: + assumes [transfer_rule]: "bi_unique A" + shows "(set_rel A ===> set_rel A ===> op =) (op \) (op \)" + unfolding subset_eq [abs_def] by transfer_prover + +lemma right_total_UNIV_transfer[transfer_rule]: + assumes "right_total A" + shows "(set_rel A) (Collect (Domainp A)) UNIV" + using assms unfolding right_total_def set_rel_def Domainp_iff by blast + +lemma UNIV_transfer [transfer_rule]: + assumes "bi_total A" + shows "(set_rel A) UNIV UNIV" + using assms unfolding set_rel_def bi_total_def by simp + +lemma right_total_Compl_transfer [transfer_rule]: + assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" + shows "(set_rel A ===> set_rel A) (\S. uminus S \ Collect (Domainp A)) uminus" + unfolding Compl_eq [abs_def] + by (subst Collect_conj_eq[symmetric]) transfer_prover + +lemma Compl_transfer [transfer_rule]: + assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" + shows "(set_rel A ===> set_rel A) uminus uminus" + unfolding Compl_eq [abs_def] by transfer_prover + +lemma right_total_Inter_transfer [transfer_rule]: + assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" + shows "(set_rel (set_rel A) ===> set_rel A) (\S. Inter S \ Collect (Domainp A)) Inter" + unfolding Inter_eq[abs_def] + by (subst Collect_conj_eq[symmetric]) transfer_prover + +lemma Inter_transfer [transfer_rule]: + assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" + shows "(set_rel (set_rel A) ===> set_rel A) Inter Inter" + unfolding Inter_eq [abs_def] by transfer_prover + +lemma filter_transfer [transfer_rule]: + assumes [transfer_rule]: "bi_unique A" + shows "((A ===> op=) ===> set_rel A ===> set_rel A) Set.filter Set.filter" + unfolding Set.filter_def[abs_def] fun_rel_def set_rel_def by blast + +lemma bi_unique_set_rel_lemma: + assumes "bi_unique R" and "set_rel R X Y" + obtains f where "Y = image f X" and "inj_on f X" and "\x\X. R x (f x)" +proof + let ?f = "\x. THE y. R x y" + from assms show f: "\x\X. R x (?f x)" + apply (clarsimp simp add: set_rel_def) + apply (drule (1) bspec, clarify) + apply (rule theI2, assumption) + apply (simp add: bi_unique_def) + apply assumption + done + from assms show "Y = image ?f X" + apply safe + apply (clarsimp simp add: set_rel_def) + apply (drule (1) bspec, clarify) + apply (rule image_eqI) + apply (rule the_equality [symmetric], assumption) + apply (simp add: bi_unique_def) + apply assumption + apply (clarsimp simp add: set_rel_def) + apply (frule (1) bspec, clarify) + apply (rule theI2, assumption) + apply (clarsimp simp add: bi_unique_def) + apply (simp add: bi_unique_def, metis) + done + show "inj_on ?f X" + apply (rule inj_onI) + apply (drule f [rule_format]) + apply (drule f [rule_format]) + apply (simp add: assms(1) [unfolded bi_unique_def]) + done +qed + +lemma finite_transfer [transfer_rule]: + "bi_unique A \ (set_rel A ===> op =) finite finite" + by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, + auto dest: finite_imageD) + +lemma card_transfer [transfer_rule]: + "bi_unique A \ (set_rel A ===> op =) card card" + by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image) + +end + +end diff -r aeee0a4be6cf -r cb82606b8215 src/HOL/Lifting_Sum.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Lifting_Sum.thy Tue Aug 13 15:59:22 2013 +0200 @@ -0,0 +1,119 @@ +(* Title: HOL/Lifting_Sum.thy + Author: Brian Huffman and Ondrej Kuncar +*) + +header {* Setup for Lifting/Transfer for the sum type *} + +theory Lifting_Sum +imports Lifting FunDef +begin + +subsection {* Relator and predicator properties *} + +fun + sum_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ 'a + 'b \ 'c + 'd \ bool" +where + "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" +| "sum_rel R1 R2 (Inl a1) (Inr b2) = False" +| "sum_rel R1 R2 (Inr a2) (Inl b1) = False" +| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" + +lemma sum_rel_unfold: + "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \ R1 x y + | (Inr x, Inr y) \ R2 x y + | _ \ False)" + by (cases x) (cases y, simp_all)+ + +fun sum_pred :: "('a \ bool) \ ('b \ bool) \ 'a + 'b \ bool" +where + "sum_pred P1 P2 (Inl a) = P1 a" +| "sum_pred P1 P2 (Inr a) = P2 a" + +lemma sum_pred_unfold: + "sum_pred P1 P2 x = (case x of Inl x \ P1 x + | Inr x \ P2 x)" +by (cases x) simp_all + +lemma sum_rel_eq [relator_eq]: + "sum_rel (op =) (op =) = (op =)" + by (simp add: sum_rel_unfold fun_eq_iff split: sum.split) + +lemma sum_rel_mono[relator_mono]: + assumes "A \ C" + assumes "B \ D" + shows "(sum_rel A B) \ (sum_rel C D)" +using assms by (auto simp: sum_rel_unfold split: sum.splits) + +lemma sum_rel_OO[relator_distr]: + "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)" +by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split) + +lemma Domainp_sum[relator_domain]: + assumes "Domainp R1 = P1" + assumes "Domainp R2 = P2" + shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)" +using assms +by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split) + +lemma reflp_sum_rel[reflexivity_rule]: + "reflp R1 \ reflp R2 \ reflp (sum_rel R1 R2)" + unfolding reflp_def split_sum_all sum_rel.simps by fast + +lemma left_total_sum_rel[reflexivity_rule]: + "left_total R1 \ left_total R2 \ left_total (sum_rel R1 R2)" + using assms unfolding left_total_def split_sum_all split_sum_ex by simp + +lemma left_unique_sum_rel [reflexivity_rule]: + "left_unique R1 \ left_unique R2 \ left_unique (sum_rel R1 R2)" + using assms unfolding left_unique_def split_sum_all by simp + +lemma right_total_sum_rel [transfer_rule]: + "right_total R1 \ right_total R2 \ right_total (sum_rel R1 R2)" + unfolding right_total_def split_sum_all split_sum_ex by simp + +lemma right_unique_sum_rel [transfer_rule]: + "right_unique R1 \ right_unique R2 \ right_unique (sum_rel R1 R2)" + unfolding right_unique_def split_sum_all by simp + +lemma bi_total_sum_rel [transfer_rule]: + "bi_total R1 \ bi_total R2 \ bi_total (sum_rel R1 R2)" + using assms unfolding bi_total_def split_sum_all split_sum_ex by simp + +lemma bi_unique_sum_rel [transfer_rule]: + "bi_unique R1 \ bi_unique R2 \ bi_unique (sum_rel R1 R2)" + using assms unfolding bi_unique_def split_sum_all by simp + +lemma sum_invariant_commute [invariant_commute]: + "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)" + by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_unfold sum_pred_unfold split: sum.split) + +subsection {* Quotient theorem for the Lifting package *} + +lemma Quotient_sum[quot_map]: + assumes "Quotient R1 Abs1 Rep1 T1" + assumes "Quotient R2 Abs2 Rep2 T2" + shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) + (sum_map Rep1 Rep2) (sum_rel T1 T2)" + using assms unfolding Quotient_alt_def + by (simp add: split_sum_all) + +subsection {* Transfer rules for the Transfer package *} + +context +begin +interpretation lifting_syntax . + +lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl" + unfolding fun_rel_def by simp + +lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr" + unfolding fun_rel_def by simp + +lemma sum_case_transfer [transfer_rule]: + "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case" + unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split) + +end + +end + diff -r aeee0a4be6cf -r cb82606b8215 src/HOL/List.thy --- a/src/HOL/List.thy Tue Aug 13 15:59:22 2013 +0200 +++ b/src/HOL/List.thy Tue Aug 13 15:59:22 2013 +0200 @@ -5,7 +5,7 @@ header {* The datatype of finite lists *} theory List -imports Presburger Code_Numeral Quotient ATP +imports Presburger Code_Numeral Quotient ATP Lifting_Set Lifting_Option Lifting_Product begin datatype 'a list = @@ -6228,5 +6228,338 @@ "wf (set xs) = acyclic (set xs)" by (simp add: wf_iff_acyclic_if_finite) +subsection {* Setup for Lifting/Transfer *} + +subsubsection {* Relator and predicator properties *} + +lemma list_all2_eq'[relator_eq]: + "list_all2 (op =) = (op =)" +by (rule ext)+ (simp add: list_all2_eq) + +lemma list_all2_mono'[relator_mono]: + assumes "A \ B" + shows "(list_all2 A) \ (list_all2 B)" +using assms by (auto intro: list_all2_mono) + +lemma list_all2_OO[relator_distr]: "list_all2 A OO list_all2 B = list_all2 (A OO B)" +proof (intro ext iffI) + fix xs ys + assume "list_all2 (A OO B) xs ys" + thus "(list_all2 A OO list_all2 B) xs ys" + unfolding OO_def + by (induct, simp, simp add: list_all2_Cons1 list_all2_Cons2, fast) +next + fix xs ys + assume "(list_all2 A OO list_all2 B) xs ys" + then obtain zs where "list_all2 A xs zs" and "list_all2 B zs ys" .. + thus "list_all2 (A OO B) xs ys" + by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast) +qed + +lemma Domainp_list[relator_domain]: + assumes "Domainp A = P" + shows "Domainp (list_all2 A) = (list_all P)" +proof - + { + fix x + have *: "\x. (\y. A x y) = P x" using assms unfolding Domainp_iff by blast + have "(\y. (list_all2 A x y)) = list_all P x" + by (induction x) (simp_all add: * list_all2_Cons1) + } + then show ?thesis + unfolding Domainp_iff[abs_def] + by (auto iff: fun_eq_iff) +qed + +lemma reflp_list_all2[reflexivity_rule]: + assumes "reflp R" + shows "reflp (list_all2 R)" +proof (rule reflpI) + from assms have *: "\xs. R xs xs" by (rule reflpE) + fix xs + show "list_all2 R xs xs" + by (induct xs) (simp_all add: *) +qed + +lemma left_total_list_all2[reflexivity_rule]: + "left_total R \ left_total (list_all2 R)" + unfolding left_total_def + apply safe + apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1) +done + +lemma left_unique_list_all2 [reflexivity_rule]: + "left_unique R \ left_unique (list_all2 R)" + unfolding left_unique_def + apply (subst (2) all_comm, subst (1) all_comm) + apply (rule allI, rename_tac zs, induct_tac zs) + apply (auto simp add: list_all2_Cons2) + done + +lemma right_total_list_all2 [transfer_rule]: + "right_total R \ right_total (list_all2 R)" + unfolding right_total_def + by (rule allI, induct_tac y, simp, simp add: list_all2_Cons2) + +lemma right_unique_list_all2 [transfer_rule]: + "right_unique R \ right_unique (list_all2 R)" + unfolding right_unique_def + apply (rule allI, rename_tac xs, induct_tac xs) + apply (auto simp add: list_all2_Cons1) + done + +lemma bi_total_list_all2 [transfer_rule]: + "bi_total A \ bi_total (list_all2 A)" + unfolding bi_total_def + apply safe + apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1) + apply (rename_tac ys, induct_tac ys, simp, simp add: list_all2_Cons2) + done + +lemma bi_unique_list_all2 [transfer_rule]: + "bi_unique A \ bi_unique (list_all2 A)" + unfolding bi_unique_def + apply (rule conjI) + apply (rule allI, rename_tac xs, induct_tac xs) + apply (simp, force simp add: list_all2_Cons1) + apply (subst (2) all_comm, subst (1) all_comm) + apply (rule allI, rename_tac xs, induct_tac xs) + apply (simp, force simp add: list_all2_Cons2) + done + +lemma list_invariant_commute [invariant_commute]: + "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)" + apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def) + apply (intro allI) + apply (induct_tac rule: list_induct2') + apply simp_all + apply fastforce +done + +subsubsection {* Quotient theorem for the Lifting package *} + +lemma Quotient_list[quot_map]: + assumes "Quotient R Abs Rep T" + shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)" +proof (unfold Quotient_alt_def, intro conjI allI impI) + from assms have 1: "\x y. T x y \ Abs x = y" + unfolding Quotient_alt_def by simp + fix xs ys assume "list_all2 T xs ys" thus "map Abs xs = ys" + by (induct, simp, simp add: 1) +next + from assms have 2: "\x. T (Rep x) x" + unfolding Quotient_alt_def by simp + fix xs show "list_all2 T (map Rep xs) xs" + by (induct xs, simp, simp add: 2) +next + from assms have 3: "\x y. R x y \ T x (Abs x) \ T y (Abs y) \ Abs x = Abs y" + unfolding Quotient_alt_def by simp + fix xs ys show "list_all2 R xs ys \ list_all2 T xs (map Abs xs) \ + list_all2 T ys (map Abs ys) \ map Abs xs = map Abs ys" + by (induct xs ys rule: list_induct2', simp_all, metis 3) +qed + +subsubsection {* Transfer rules for the Transfer package *} + +context +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 fun_rel_def by simp + +lemma list_case_transfer [transfer_rule]: + "(B ===> (A ===> list_all2 A ===> B) ===> list_all2 A ===> B) + list_case list_case" + unfolding fun_rel_def by (simp split: list.split) + +lemma list_rec_transfer [transfer_rule]: + "(B ===> (A ===> list_all2 A ===> B ===> B) ===> list_all2 A ===> B) + 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 + +lemma append_transfer [transfer_rule]: + "(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 + +lemma foldl_transfer [transfer_rule]: + "((B ===> A ===> B) ===> B ===> list_all2 A ===> B) foldl foldl" + unfolding List.foldl_def by transfer_prover + +lemma concat_transfer [transfer_rule]: + "(list_all2 (list_all2 A) ===> list_all2 A) concat concat" + unfolding List.concat_def by transfer_prover + +lemma drop_transfer [transfer_rule]: + "(op = ===> list_all2 A ===> list_all2 A) drop drop" + unfolding List.drop_def by transfer_prover + +lemma take_transfer [transfer_rule]: + "(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 rotate1_transfer [transfer_rule]: + "(list_all2 A ===> list_all2 A) rotate1 rotate1" + unfolding rotate1_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 (subst (4) list_all2_def [abs_def]) + apply (subst (3) list_all2_def [abs_def]) + apply transfer_prover + done + +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" + apply (rule fun_relI, rule set_relI) + apply (erule lists.induct, simp) + apply (simp only: set_rel_def list_all2_Cons1, metis lists.Cons) + apply (erule lists.induct, simp) + 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 + +lemma listsum_transfer[transfer_rule]: + assumes [transfer_rule]: "A 0 0" + assumes [transfer_rule]: "(A ===> A ===> A) op + op +" + shows "(list_all2 A ===> A) listsum listsum" + unfolding listsum_def[abs_def] + by transfer_prover + end +end diff -r aeee0a4be6cf -r cb82606b8215 src/HOL/Main.thy --- a/src/HOL/Main.thy Tue Aug 13 15:59:22 2013 +0200 +++ b/src/HOL/Main.thy Tue Aug 13 15:59:22 2013 +0200 @@ -1,7 +1,7 @@ header {* Main HOL *} theory Main -imports Predicate_Compile Nitpick Extraction +imports Predicate_Compile Nitpick Extraction Lifting_Sum begin text {* diff -r aeee0a4be6cf -r cb82606b8215 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Tue Aug 13 15:59:22 2013 +0200 +++ b/src/HOL/Rat.thy Tue Aug 13 15:59:22 2013 +0200 @@ -49,8 +49,8 @@ morphisms Rep_Rat Abs_Rat by (rule part_equivp_ratrel) -lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp cr_rat = (\x. snd x \ 0)" -by (simp add: rat.domain) +lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp pcr_rat = (\x. snd x \ 0)" +by (simp add: rat.domain_eq) subsubsection {* Representation and basic operations *}