# HG changeset patch # User blanchet # Date 1394116158 -3600 # Node ID 7ab8f003fe413a0f6fcfb71e356eea7e3819816f # Parent 5c2df04e97d11015b516fab0be25ee94ec348863 renamed 'prod_rel' to 'rel_prod' diff -r 5c2df04e97d1 -r 7ab8f003fe41 NEWS --- a/NEWS Thu Mar 06 15:25:21 2014 +0100 +++ b/NEWS Thu Mar 06 15:29:18 2014 +0100 @@ -193,6 +193,7 @@ * The following map functions and relators have been renamed: sum_map ~> map_sum map_pair ~> map_prod + prod_rel ~> rel_prod sum_rel ~> rel_sum set_rel ~> rel_set filter_rel ~> rel_filter diff -r 5c2df04e97d1 -r 7ab8f003fe41 src/Doc/IsarRef/HOL_Specific.thy --- a/src/Doc/IsarRef/HOL_Specific.thy Thu Mar 06 15:25:21 2014 +0100 +++ b/src/Doc/IsarRef/HOL_Specific.thy Thu Mar 06 15:29:18 2014 +0100 @@ -1565,7 +1565,7 @@ using the same attribute. For example: @{text "bi_unique A \ (list_all2 A ===> op =) distinct distinct"}\\ - @{text "\bi_unique A; bi_unique B\ \ bi_unique (prod_rel A B)"} + @{text "\bi_unique A; bi_unique B\ \ bi_unique (rel_prod A B)"} \item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection of rules, which specify a domain of a transfer relation by a predicate. diff -r 5c2df04e97d1 -r 7ab8f003fe41 src/HOL/BNF_Examples/Process.thy --- a/src/HOL/BNF_Examples/Process.thy Thu Mar 06 15:25:21 2014 +0100 +++ b/src/HOL/BNF_Examples/Process.thy Thu Mar 06 15:29:18 2014 +0100 @@ -24,7 +24,7 @@ declare rel_pre_process_def[simp] rel_sum_def[simp] - prod_rel_def[simp] + rel_prod_def[simp] (* Constructors versus discriminators *) theorem isAction_isChoice: diff -r 5c2df04e97d1 -r 7ab8f003fe41 src/HOL/Basic_BNFs.thy --- a/src/HOL/Basic_BNFs.thy Thu Mar 06 15:25:21 2014 +0100 +++ b/src/HOL/Basic_BNFs.thy Thu Mar 06 15:29:18 2014 +0100 @@ -104,19 +104,19 @@ lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] definition - prod_rel :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a \ 'c \ 'b \ 'd \ bool" + rel_prod :: "('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)" + "rel_prod R1 R2 = (\(a, b) (c, d). R1 a c \ R2 b d)" -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 rel_prod_apply [simp]: + "rel_prod R1 R2 (a, b) (c, d) \ R1 a c \ R2 b d" + by (simp add: rel_prod_def) bnf "'a \ 'b" map: map_prod sets: fsts snds bd: natLeq - rel: prod_rel + rel: rel_prod proof (unfold prod_set_defs) show "map_prod id id = id" by (rule map_prod.id) next @@ -149,13 +149,13 @@ by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric]) next fix R1 R2 S1 S2 - show "prod_rel R1 R2 OO prod_rel S1 S2 \ prod_rel (R1 OO S1) (R2 OO S2)" by auto + show "rel_prod R1 R2 OO rel_prod S1 S2 \ rel_prod (R1 OO S1) (R2 OO S2)" by auto next fix R S - show "prod_rel R S = + show "rel_prod R S = (Grp {x. {fst x} \ Collect (split R) \ {snd x} \ Collect (split S)} (map_prod fst fst))\\ OO Grp {x. {fst x} \ Collect (split R) \ {snd x} \ Collect (split S)} (map_prod snd snd)" - unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff + unfolding prod_set_defs rel_prod_def Grp_def relcompp.simps conversep.simps fun_eq_iff by auto qed diff -r 5c2df04e97d1 -r 7ab8f003fe41 src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Thu Mar 06 15:25:21 2014 +0100 +++ b/src/HOL/Library/Mapping.thy Thu Mar 06 15:29:18 2014 +0100 @@ -43,7 +43,7 @@ lemma map_of_transfer [transfer_rule]: assumes [transfer_rule]: "bi_unique R1" - shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> rel_option R2) map_of map_of" + shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of" unfolding map_of_def by transfer_prover lemma tabulate_transfer: diff -r 5c2df04e97d1 -r 7ab8f003fe41 src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Thu Mar 06 15:25:21 2014 +0100 +++ b/src/HOL/Library/Quotient_Product.thy Thu Mar 06 15:29:18 2014 +0100 @@ -14,20 +14,20 @@ shows "map_prod id id = id" by (simp add: fun_eq_iff) -lemma prod_rel_eq [id_simps]: - shows "prod_rel (op =) (op =) = (op =)" +lemma rel_prod_eq [id_simps]: + shows "rel_prod (op =) (op =) = (op =)" by (simp add: fun_eq_iff) lemma prod_equivp [quot_equiv]: assumes "equivp R1" assumes "equivp R2" - shows "equivp (prod_rel R1 R2)" + shows "equivp (rel_prod R1 R2)" using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE) lemma prod_quotient [quot_thm]: assumes "Quotient3 R1 Abs1 Rep1" assumes "Quotient3 R2 Abs2 Rep2" - shows "Quotient3 (prod_rel R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2)" + shows "Quotient3 (rel_prod R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2)" apply (rule Quotient3I) apply (simp add: map_prod.compositionality comp_def map_prod.identity Quotient3_abs_rep [OF assms(1)] Quotient3_abs_rep [OF assms(2)]) @@ -36,12 +36,12 @@ apply (auto simp add: split_paired_all) done -declare [[mapQ3 prod = (prod_rel, prod_quotient)]] +declare [[mapQ3 prod = (rel_prod, prod_quotient)]] lemma Pair_rsp [quot_respect]: assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2" - shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" + shows "(R1 ===> R2 ===> rel_prod R1 R2) Pair Pair" by (rule Pair_transfer) lemma Pair_prs [quot_preserve]: @@ -55,7 +55,7 @@ lemma fst_rsp [quot_respect]: assumes "Quotient3 R1 Abs1 Rep1" assumes "Quotient3 R2 Abs2 Rep2" - shows "(prod_rel R1 R2 ===> R1) fst fst" + shows "(rel_prod R1 R2 ===> R1) fst fst" by auto lemma fst_prs [quot_preserve]: @@ -67,7 +67,7 @@ lemma snd_rsp [quot_respect]: assumes "Quotient3 R1 Abs1 Rep1" assumes "Quotient3 R2 Abs2 Rep2" - shows "(prod_rel R1 R2 ===> R2) snd snd" + shows "(rel_prod R1 R2 ===> R2) snd snd" by auto lemma snd_prs [quot_preserve]: @@ -77,7 +77,7 @@ by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2]) lemma split_rsp [quot_respect]: - shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" + shows "((R1 ===> R2 ===> (op =)) ===> (rel_prod R1 R2) ===> (op =)) split split" by (rule case_prod_transfer) lemma split_prs [quot_preserve]: @@ -88,18 +88,18 @@ lemma [quot_respect]: shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===> - prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel" - by (rule prod_rel_transfer) + rel_prod R2 R1 ===> rel_prod R2 R1 ===> op =) rel_prod rel_prod" + by (rule rel_prod_transfer) lemma [quot_preserve]: assumes q1: "Quotient3 R1 abs1 rep1" and q2: "Quotient3 R2 abs2 rep2" shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) ---> - map_prod rep1 rep2 ---> map_prod rep1 rep2 ---> id) prod_rel = prod_rel" + map_prod rep1 rep2 ---> map_prod rep1 rep2 ---> id) rel_prod = rel_prod" by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) lemma [quot_preserve]: - shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2) + shows"(rel_prod ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2) (l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \ R2 (rep2 l2) (rep2 r2))" by simp diff -r 5c2df04e97d1 -r 7ab8f003fe41 src/HOL/Lifting_Product.thy --- a/src/HOL/Lifting_Product.thy Thu Mar 06 15:25:21 2014 +0100 +++ b/src/HOL/Lifting_Product.thy Thu Mar 06 15:29:18 2014 +0100 @@ -17,60 +17,60 @@ "prod_pred P1 P2 (a, b) \ P1 a \ P2 b" by (simp add: prod_pred_def) -lemmas prod_rel_eq[relator_eq] = prod.rel_eq -lemmas prod_rel_mono[relator_mono] = prod.rel_mono +lemmas rel_prod_eq[relator_eq] = prod.rel_eq +lemmas rel_prod_mono[relator_mono] = prod.rel_mono -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 rel_prod_OO[relator_distr]: + "(rel_prod A B) OO (rel_prod C D) = rel_prod (A OO C) (B OO D)" +by (rule ext)+ (auto simp: rel_prod_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 + shows "Domainp (rel_prod T1 T2) = (prod_pred P1 P2)" +using assms unfolding rel_prod_def prod_pred_def by blast -lemma left_total_prod_rel [reflexivity_rule]: +lemma left_total_rel_prod [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 + shows "left_total (rel_prod R1 R2)" + using assms unfolding left_total_def rel_prod_def by auto -lemma left_unique_prod_rel [reflexivity_rule]: +lemma left_unique_rel_prod [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 + shows "left_unique (rel_prod R1 R2)" + using assms unfolding left_unique_def rel_prod_def by auto -lemma right_total_prod_rel [transfer_rule]: +lemma right_total_rel_prod [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 + shows "right_total (rel_prod R1 R2)" + using assms unfolding right_total_def rel_prod_def by auto -lemma right_unique_prod_rel [transfer_rule]: +lemma right_unique_rel_prod [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 + shows "right_unique (rel_prod R1 R2)" + using assms unfolding right_unique_def rel_prod_def by auto -lemma bi_total_prod_rel [transfer_rule]: +lemma bi_total_rel_prod [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 + shows "bi_total (rel_prod R1 R2)" + using assms unfolding bi_total_def rel_prod_def by auto -lemma bi_unique_prod_rel [transfer_rule]: +lemma bi_unique_rel_prod [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 + shows "bi_unique (rel_prod R1 R2)" + using assms unfolding bi_unique_def rel_prod_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 + "rel_prod (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)" + by (simp add: fun_eq_iff rel_prod_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_prod Abs1 Abs2) (map_prod Rep1 Rep2) (prod_rel T1 T2)" + shows "Quotient (rel_prod R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2) (rel_prod T1 T2)" using assms unfolding Quotient_alt_def by auto subsection {* Transfer rules for the Transfer package *} @@ -79,31 +79,31 @@ 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 Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair" + unfolding fun_rel_def rel_prod_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 fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst" + unfolding fun_rel_def rel_prod_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 snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd" + unfolding fun_rel_def rel_prod_def by simp lemma case_prod_transfer [transfer_rule]: - "((A ===> B ===> C) ===> prod_rel A B ===> C) case_prod case_prod" - unfolding fun_rel_def prod_rel_def by simp + "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod" + unfolding fun_rel_def rel_prod_def by simp lemma curry_transfer [transfer_rule]: - "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry" + "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry" unfolding curry_def by transfer_prover lemma map_prod_transfer [transfer_rule]: - "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D) + "((A ===> C) ===> (B ===> D) ===> rel_prod A B ===> rel_prod C D) map_prod map_prod" unfolding map_prod_def [abs_def] by transfer_prover -lemma prod_rel_transfer [transfer_rule]: +lemma rel_prod_transfer [transfer_rule]: "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> - prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel" + rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod" unfolding fun_rel_def by auto end diff -r 5c2df04e97d1 -r 7ab8f003fe41 src/HOL/List.thy --- a/src/HOL/List.thy Thu Mar 06 15:25:21 2014 +0100 +++ b/src/HOL/List.thy Thu Mar 06 15:29:18 2014 +0100 @@ -6793,11 +6793,11 @@ 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" + "(list_all2 A ===> list_all2 B ===> list_all2 (rel_prod A B)) zip zip" unfolding zip_def by transfer_prover lemma product_transfer [transfer_rule]: - "(list_all2 A ===> list_all2 B ===> list_all2 (prod_rel A B)) List.product List.product" + "(list_all2 A ===> list_all2 B ===> list_all2 (rel_prod A B)) List.product List.product" unfolding List.product_def by transfer_prover lemma product_lists_transfer [transfer_rule]: @@ -6868,7 +6868,7 @@ 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)) + "((A ===> op =) ===> list_all2 A ===> rel_prod (list_all2 A) (list_all2 A)) partition partition" unfolding partition_def by transfer_prover diff -r 5c2df04e97d1 -r 7ab8f003fe41 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 15:25:21 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 15:29:18 2014 +0100 @@ -42,7 +42,7 @@ @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff Union_Un_distrib image_iff o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; -val sum_prod_thms_rel = @{thms prod_rel_apply rel_sum_simps id_apply}; +val sum_prod_thms_rel = @{thms rel_prod_apply rel_sum_simps id_apply}; fun hhf_concl_conv cv ctxt ct = (case Thm.term_of ct of