renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
--- 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 *}
--- 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
-