src/HOL/Lifting_Product.thy
changeset 55944 7ab8f003fe41
parent 55932 68c5104d2204
child 55945 e96383acecf9
--- 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