src/HOL/Library/Quotient_Product.thy
changeset 53012 cb82606b8215
parent 51994 82cc2aeb7d13
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Tue Aug 13 15:59:22 2013 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Tue Aug 13 15:59:22 2013 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  (*  Title:      HOL/Library/Quotient_Product.thy
     1.5 -    Author:     Cezary Kaliszyk, Christian Urban and Brian Huffman
     1.6 +    Author:     Cezary Kaliszyk and Christian Urban
     1.7  *)
     1.8  
     1.9  header {* Quotient infrastructure for the product type *}
    1.10 @@ -8,137 +8,22 @@
    1.11  imports Main Quotient_Syntax
    1.12  begin
    1.13  
    1.14 -subsection {* Relator for product type *}
    1.15 -
    1.16 -definition
    1.17 -  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
    1.18 -where
    1.19 -  "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    1.20 -
    1.21 -definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.22 -where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
    1.23 -
    1.24 -lemma prod_rel_apply [simp]:
    1.25 -  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    1.26 -  by (simp add: prod_rel_def)
    1.27 -
    1.28 -lemma prod_pred_apply [simp]:
    1.29 -  "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
    1.30 -  by (simp add: prod_pred_def)
    1.31 +subsection {* Rules for the Quotient package *}
    1.32  
    1.33  lemma map_pair_id [id_simps]:
    1.34    shows "map_pair id id = id"
    1.35    by (simp add: fun_eq_iff)
    1.36  
    1.37 -lemma prod_rel_eq [id_simps, relator_eq]:
    1.38 +lemma prod_rel_eq [id_simps]:
    1.39    shows "prod_rel (op =) (op =) = (op =)"
    1.40    by (simp add: fun_eq_iff)
    1.41  
    1.42 -lemma prod_rel_mono[relator_mono]:
    1.43 -  assumes "A \<le> C"
    1.44 -  assumes "B \<le> D"
    1.45 -  shows "(prod_rel A B) \<le> (prod_rel C D)"
    1.46 -using assms by (auto simp: prod_rel_def)
    1.47 -
    1.48 -lemma prod_rel_OO[relator_distr]:
    1.49 -  "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
    1.50 -by (rule ext)+ (auto simp: prod_rel_def OO_def)
    1.51 -
    1.52 -lemma Domainp_prod[relator_domain]:
    1.53 -  assumes "Domainp T1 = P1"
    1.54 -  assumes "Domainp T2 = P2"
    1.55 -  shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
    1.56 -using assms unfolding prod_rel_def prod_pred_def by blast
    1.57 -
    1.58 -lemma reflp_prod_rel [reflexivity_rule]:
    1.59 -  assumes "reflp R1"
    1.60 -  assumes "reflp R2"
    1.61 -  shows "reflp (prod_rel R1 R2)"
    1.62 -using assms by (auto intro!: reflpI elim: reflpE)
    1.63 -
    1.64 -lemma left_total_prod_rel [reflexivity_rule]:
    1.65 -  assumes "left_total R1"
    1.66 -  assumes "left_total R2"
    1.67 -  shows "left_total (prod_rel R1 R2)"
    1.68 -  using assms unfolding left_total_def prod_rel_def by auto
    1.69 -
    1.70 -lemma left_unique_prod_rel [reflexivity_rule]:
    1.71 -  assumes "left_unique R1" and "left_unique R2"
    1.72 -  shows "left_unique (prod_rel R1 R2)"
    1.73 -  using assms unfolding left_unique_def prod_rel_def by auto
    1.74 -
    1.75  lemma prod_equivp [quot_equiv]:
    1.76    assumes "equivp R1"
    1.77    assumes "equivp R2"
    1.78    shows "equivp (prod_rel R1 R2)"
    1.79    using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
    1.80  
    1.81 -lemma right_total_prod_rel [transfer_rule]:
    1.82 -  assumes "right_total R1" and "right_total R2"
    1.83 -  shows "right_total (prod_rel R1 R2)"
    1.84 -  using assms unfolding right_total_def prod_rel_def by auto
    1.85 -
    1.86 -lemma right_unique_prod_rel [transfer_rule]:
    1.87 -  assumes "right_unique R1" and "right_unique R2"
    1.88 -  shows "right_unique (prod_rel R1 R2)"
    1.89 -  using assms unfolding right_unique_def prod_rel_def by auto
    1.90 -
    1.91 -lemma bi_total_prod_rel [transfer_rule]:
    1.92 -  assumes "bi_total R1" and "bi_total R2"
    1.93 -  shows "bi_total (prod_rel R1 R2)"
    1.94 -  using assms unfolding bi_total_def prod_rel_def by auto
    1.95 -
    1.96 -lemma bi_unique_prod_rel [transfer_rule]:
    1.97 -  assumes "bi_unique R1" and "bi_unique R2"
    1.98 -  shows "bi_unique (prod_rel R1 R2)"
    1.99 -  using assms unfolding bi_unique_def prod_rel_def by auto
   1.100 -
   1.101 -subsection {* Transfer rules for transfer package *}
   1.102 -
   1.103 -lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair"
   1.104 -  unfolding fun_rel_def prod_rel_def by simp
   1.105 -
   1.106 -lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst"
   1.107 -  unfolding fun_rel_def prod_rel_def by simp
   1.108 -
   1.109 -lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd"
   1.110 -  unfolding fun_rel_def prod_rel_def by simp
   1.111 -
   1.112 -lemma prod_case_transfer [transfer_rule]:
   1.113 -  "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case"
   1.114 -  unfolding fun_rel_def prod_rel_def by simp
   1.115 -
   1.116 -lemma curry_transfer [transfer_rule]:
   1.117 -  "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry"
   1.118 -  unfolding curry_def by transfer_prover
   1.119 -
   1.120 -lemma map_pair_transfer [transfer_rule]:
   1.121 -  "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D)
   1.122 -    map_pair map_pair"
   1.123 -  unfolding map_pair_def [abs_def] by transfer_prover
   1.124 -
   1.125 -lemma prod_rel_transfer [transfer_rule]:
   1.126 -  "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
   1.127 -    prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel"
   1.128 -  unfolding fun_rel_def by auto
   1.129 -
   1.130 -subsection {* Setup for lifting package *}
   1.131 -
   1.132 -lemma Quotient_prod[quot_map]:
   1.133 -  assumes "Quotient R1 Abs1 Rep1 T1"
   1.134 -  assumes "Quotient R2 Abs2 Rep2 T2"
   1.135 -  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2)
   1.136 -    (map_pair Rep1 Rep2) (prod_rel T1 T2)"
   1.137 -  using assms unfolding Quotient_alt_def by auto
   1.138 -
   1.139 -lemma prod_invariant_commute [invariant_commute]: 
   1.140 -  "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
   1.141 -  apply (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) 
   1.142 -  apply blast
   1.143 -done
   1.144 -
   1.145 -subsection {* Rules for quotient package *}
   1.146 -
   1.147  lemma prod_quotient [quot_thm]:
   1.148    assumes "Quotient3 R1 Abs1 Rep1"
   1.149    assumes "Quotient3 R2 Abs2 Rep2"