src/HOL/Library/Quotient_Product.thy
changeset 51956 a4d81cdebf8b
parent 51377 7da251a6c16e
child 51994 82cc2aeb7d13
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Mon May 13 12:13:24 2013 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Mon May 13 13:59:04 2013 +0200
     1.3 @@ -15,10 +15,17 @@
     1.4  where
     1.5    "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
     1.6  
     1.7 +definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
     1.8 +where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
     1.9 +
    1.10  lemma prod_rel_apply [simp]:
    1.11    "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    1.12    by (simp add: prod_rel_def)
    1.13  
    1.14 +lemma prod_pred_apply [simp]:
    1.15 +  "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
    1.16 +  by (simp add: prod_pred_def)
    1.17 +
    1.18  lemma map_pair_id [id_simps]:
    1.19    shows "map_pair id id = id"
    1.20    by (simp add: fun_eq_iff)
    1.21 @@ -37,6 +44,12 @@
    1.22    "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
    1.23  by (rule ext)+ (auto simp: prod_rel_def OO_def)
    1.24  
    1.25 +lemma Domainp_prod[relator_domain]:
    1.26 +  assumes "Domainp T1 = P1"
    1.27 +  assumes "Domainp T2 = P2"
    1.28 +  shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
    1.29 +using assms unfolding prod_rel_def prod_pred_def by blast
    1.30 +
    1.31  lemma prod_reflp [reflexivity_rule]:
    1.32    assumes "reflp R1"
    1.33    assumes "reflp R2"
    1.34 @@ -113,9 +126,6 @@
    1.35      (map_pair Rep1 Rep2) (prod_rel T1 T2)"
    1.36    using assms unfolding Quotient_alt_def by auto
    1.37  
    1.38 -definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.39 -where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
    1.40 -
    1.41  lemma prod_invariant_commute [invariant_commute]: 
    1.42    "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
    1.43    apply (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def)