renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
authorblanchet
Thu Mar 13 13:18:14 2014 +0100 (2014-03-13)
changeset 560921ba075db8fe4
parent 56091 fa88ff1d30e7
child 56093 4eeb73a1feec
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
src/HOL/Lifting_Option.thy
src/HOL/Lifting_Product.thy
     1.1 --- a/src/HOL/Lifting_Option.thy	Thu Mar 13 13:18:14 2014 +0100
     1.2 +++ b/src/HOL/Lifting_Option.thy	Thu Mar 13 13:18:14 2014 +0100
     1.3 @@ -17,8 +17,8 @@
     1.4      | _ \<Rightarrow> False)"
     1.5  by (auto split: prod.split option.split)
     1.6  
     1.7 -abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
     1.8 -  "option_pred \<equiv> case_option True"
     1.9 +abbreviation (input) pred_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
    1.10 +  "pred_option \<equiv> case_option True"
    1.11  
    1.12  lemma rel_option_eq [relator_eq]:
    1.13    "rel_option (op =) = (op =)"
    1.14 @@ -35,7 +35,7 @@
    1.15  
    1.16  lemma Domainp_option[relator_domain]:
    1.17    assumes "Domainp A = P"
    1.18 -  shows "Domainp (rel_option A) = (option_pred P)"
    1.19 +  shows "Domainp (rel_option A) = (pred_option P)"
    1.20  using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
    1.21  by (auto iff: fun_eq_iff split: option.split)
    1.22  
    1.23 @@ -64,7 +64,7 @@
    1.24    unfolding bi_unique_def split_option_all by simp
    1.25  
    1.26  lemma option_invariant_commute [invariant_commute]:
    1.27 -  "rel_option (Lifting.invariant P) = Lifting.invariant (option_pred P)"
    1.28 +  "rel_option (Lifting.invariant P) = Lifting.invariant (pred_option P)"
    1.29    by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all)
    1.30  
    1.31  subsection {* Quotient theorem for the Lifting package *}
     2.1 --- a/src/HOL/Lifting_Product.thy	Thu Mar 13 13:18:14 2014 +0100
     2.2 +++ b/src/HOL/Lifting_Product.thy	Thu Mar 13 13:18:14 2014 +0100
     2.3 @@ -10,12 +10,12 @@
     2.4  
     2.5  subsection {* Relator and predicator properties *}
     2.6  
     2.7 -definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
     2.8 -where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
     2.9 +definition pred_prod :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    2.10 +where "pred_prod R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
    2.11  
    2.12 -lemma prod_pred_apply [simp]:
    2.13 -  "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
    2.14 -  by (simp add: prod_pred_def)
    2.15 +lemma pred_prod_apply [simp]:
    2.16 +  "pred_prod P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
    2.17 +  by (simp add: pred_prod_def)
    2.18  
    2.19  lemmas rel_prod_eq[relator_eq] = prod.rel_eq
    2.20  lemmas rel_prod_mono[relator_mono] = prod.rel_mono
    2.21 @@ -27,8 +27,8 @@
    2.22  lemma Domainp_prod[relator_domain]:
    2.23    assumes "Domainp T1 = P1"
    2.24    assumes "Domainp T2 = P2"
    2.25 -  shows "Domainp (rel_prod T1 T2) = (prod_pred P1 P2)"
    2.26 -using assms unfolding rel_prod_def prod_pred_def by blast
    2.27 +  shows "Domainp (rel_prod T1 T2) = (pred_prod P1 P2)"
    2.28 +using assms unfolding rel_prod_def pred_prod_def by blast
    2.29  
    2.30  lemma left_total_rel_prod [reflexivity_rule]:
    2.31    assumes "left_total R1"
    2.32 @@ -62,8 +62,8 @@
    2.33    using assms unfolding bi_unique_def rel_prod_def by auto
    2.34  
    2.35  lemma prod_invariant_commute [invariant_commute]: 
    2.36 -  "rel_prod (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
    2.37 -  by (simp add: fun_eq_iff rel_prod_def prod_pred_def Lifting.invariant_def) blast
    2.38 +  "rel_prod (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (pred_prod P1 P2)"
    2.39 +  by (simp add: fun_eq_iff rel_prod_def pred_prod_def Lifting.invariant_def) blast
    2.40  
    2.41  subsection {* Quotient theorem for the Lifting package *}
    2.42  
    2.43 @@ -109,4 +109,3 @@
    2.44  end
    2.45  
    2.46  end
    2.47 -