# HG changeset patch
# User blanchet
# Date 1394713094 -3600
# Node ID 1ba075db8fe477975a96df3d1661ca2caa3792c5
# Parent  fa88ff1d30e74bad1c35e5a0746338482eb5e07a
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'

diff -r fa88ff1d30e7 -r 1ba075db8fe4 src/HOL/Lifting_Option.thy
--- a/src/HOL/Lifting_Option.thy	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Lifting_Option.thy	Thu Mar 13 13:18:14 2014 +0100
@@ -17,8 +17,8 @@
     | _ \<Rightarrow> False)"
 by (auto split: prod.split option.split)
 
-abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
-  "option_pred \<equiv> case_option True"
+abbreviation (input) pred_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
+  "pred_option \<equiv> case_option True"
 
 lemma rel_option_eq [relator_eq]:
   "rel_option (op =) = (op =)"
@@ -35,7 +35,7 @@
 
 lemma Domainp_option[relator_domain]:
   assumes "Domainp A = P"
-  shows "Domainp (rel_option A) = (option_pred P)"
+  shows "Domainp (rel_option A) = (pred_option P)"
 using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
 by (auto iff: fun_eq_iff split: option.split)
 
@@ -64,7 +64,7 @@
   unfolding bi_unique_def split_option_all by simp
 
 lemma option_invariant_commute [invariant_commute]:
-  "rel_option (Lifting.invariant P) = Lifting.invariant (option_pred P)"
+  "rel_option (Lifting.invariant P) = Lifting.invariant (pred_option P)"
   by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all)
 
 subsection {* Quotient theorem for the Lifting package *}
diff -r fa88ff1d30e7 -r 1ba075db8fe4 src/HOL/Lifting_Product.thy
--- a/src/HOL/Lifting_Product.thy	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Lifting_Product.thy	Thu Mar 13 13:18:14 2014 +0100
@@ -10,12 +10,12 @@
 
 subsection {* Relator and predicator properties *}
 
-definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
-where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
+definition pred_prod :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+where "pred_prod R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
 
-lemma prod_pred_apply [simp]:
-  "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
-  by (simp add: prod_pred_def)
+lemma pred_prod_apply [simp]:
+  "pred_prod P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
+  by (simp add: pred_prod_def)
 
 lemmas rel_prod_eq[relator_eq] = prod.rel_eq
 lemmas rel_prod_mono[relator_mono] = prod.rel_mono
@@ -27,8 +27,8 @@
 lemma Domainp_prod[relator_domain]:
   assumes "Domainp T1 = P1"
   assumes "Domainp T2 = P2"
-  shows "Domainp (rel_prod T1 T2) = (prod_pred P1 P2)"
-using assms unfolding rel_prod_def prod_pred_def by blast
+  shows "Domainp (rel_prod T1 T2) = (pred_prod P1 P2)"
+using assms unfolding rel_prod_def pred_prod_def by blast
 
 lemma left_total_rel_prod [reflexivity_rule]:
   assumes "left_total R1"
@@ -62,8 +62,8 @@
   using assms unfolding bi_unique_def rel_prod_def by auto
 
 lemma prod_invariant_commute [invariant_commute]: 
-  "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
+  "rel_prod (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (pred_prod P1 P2)"
+  by (simp add: fun_eq_iff rel_prod_def pred_prod_def Lifting.invariant_def) blast
 
 subsection {* Quotient theorem for the Lifting package *}
 
@@ -109,4 +109,3 @@
 end
 
 end
-