--- 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
--- 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 \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"}\\
- @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (prod_rel A B)"}
+ @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> 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.
--- 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:
--- 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 \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
+ rel_prod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
where
- "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
+ "rel_prod R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
-lemma prod_rel_apply [simp]:
- "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
- by (simp add: prod_rel_def)
+lemma rel_prod_apply [simp]:
+ "rel_prod R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
+ by (simp add: rel_prod_def)
bnf "'a \<times> '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 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
+ show "rel_prod R1 R2 OO rel_prod S1 S2 \<le> 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} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> 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
--- 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:
--- 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) \<and> R2 (rep2 l2) (rep2 r2))"
by simp
--- 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) \<longleftrightarrow> P1 a \<and> 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
--- 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
--- 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