src/HOL/Library/Quotient_Product.thy
changeset 40820 fd9c98ead9a9
parent 40607 30d512bf47a7
child 41372 551eb49a6e91
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Tue Nov 30 15:58:09 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Tue Nov 30 15:58:09 2010 +0100
     1.3 @@ -19,38 +19,39 @@
     1.4    "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
     1.5    by (simp add: prod_rel_def)
     1.6  
     1.7 -lemma prod_equivp[quot_equiv]:
     1.8 -  assumes a: "equivp R1"
     1.9 -  assumes b: "equivp R2"
    1.10 +lemma map_pair_id [id_simps]:
    1.11 +  shows "map_pair id id = id"
    1.12 +  by (simp add: fun_eq_iff)
    1.13 +
    1.14 +lemma prod_rel_eq [id_simps]:
    1.15 +  shows "prod_rel (op =) (op =) = (op =)"
    1.16 +  by (simp add: fun_eq_iff)
    1.17 +
    1.18 +lemma prod_equivp [quot_equiv]:
    1.19 +  assumes "equivp R1"
    1.20 +  assumes "equivp R2"
    1.21    shows "equivp (prod_rel R1 R2)"
    1.22 -  apply(rule equivpI)
    1.23 -  unfolding reflp_def symp_def transp_def
    1.24 -  apply(simp_all add: split_paired_all prod_rel_def)
    1.25 -  apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
    1.26 -  apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
    1.27 -  apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
    1.28 +  using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
    1.29 +
    1.30 +lemma prod_quotient [quot_thm]:
    1.31 +  assumes "Quotient R1 Abs1 Rep1"
    1.32 +  assumes "Quotient R2 Abs2 Rep2"
    1.33 +  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
    1.34 +  apply (rule QuotientI)
    1.35 +  apply (simp add: map_pair.compositionality map_pair.identity
    1.36 +     Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)])
    1.37 +  apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)])
    1.38 +  using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)]
    1.39 +  apply (auto simp add: split_paired_all)
    1.40    done
    1.41  
    1.42 -lemma prod_quotient[quot_thm]:
    1.43 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.44 -  assumes q2: "Quotient R2 Abs2 Rep2"
    1.45 -  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
    1.46 -  unfolding Quotient_def
    1.47 -  apply(simp add: split_paired_all)
    1.48 -  apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
    1.49 -  apply(simp add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
    1.50 -  using q1 q2
    1.51 -  unfolding Quotient_def
    1.52 -  apply(blast)
    1.53 -  done
    1.54 -
    1.55 -lemma Pair_rsp[quot_respect]:
    1.56 +lemma Pair_rsp [quot_respect]:
    1.57    assumes q1: "Quotient R1 Abs1 Rep1"
    1.58    assumes q2: "Quotient R2 Abs2 Rep2"
    1.59    shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
    1.60    by (auto simp add: prod_rel_def)
    1.61  
    1.62 -lemma Pair_prs[quot_preserve]:
    1.63 +lemma Pair_prs [quot_preserve]:
    1.64    assumes q1: "Quotient R1 Abs1 Rep1"
    1.65    assumes q2: "Quotient R2 Abs2 Rep2"
    1.66    shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
    1.67 @@ -58,35 +59,35 @@
    1.68    apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    1.69    done
    1.70  
    1.71 -lemma fst_rsp[quot_respect]:
    1.72 +lemma fst_rsp [quot_respect]:
    1.73    assumes "Quotient R1 Abs1 Rep1"
    1.74    assumes "Quotient R2 Abs2 Rep2"
    1.75    shows "(prod_rel R1 R2 ===> R1) fst fst"
    1.76    by auto
    1.77  
    1.78 -lemma fst_prs[quot_preserve]:
    1.79 +lemma fst_prs [quot_preserve]:
    1.80    assumes q1: "Quotient R1 Abs1 Rep1"
    1.81    assumes q2: "Quotient R2 Abs2 Rep2"
    1.82    shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
    1.83    by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
    1.84  
    1.85 -lemma snd_rsp[quot_respect]:
    1.86 +lemma snd_rsp [quot_respect]:
    1.87    assumes "Quotient R1 Abs1 Rep1"
    1.88    assumes "Quotient R2 Abs2 Rep2"
    1.89    shows "(prod_rel R1 R2 ===> R2) snd snd"
    1.90    by auto
    1.91  
    1.92 -lemma snd_prs[quot_preserve]:
    1.93 +lemma snd_prs [quot_preserve]:
    1.94    assumes q1: "Quotient R1 Abs1 Rep1"
    1.95    assumes q2: "Quotient R2 Abs2 Rep2"
    1.96    shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
    1.97    by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
    1.98  
    1.99 -lemma split_rsp[quot_respect]:
   1.100 +lemma split_rsp [quot_respect]:
   1.101    shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
   1.102    by (auto intro!: fun_relI elim!: fun_relE)
   1.103  
   1.104 -lemma split_prs[quot_preserve]:
   1.105 +lemma split_prs [quot_preserve]:
   1.106    assumes q1: "Quotient R1 Abs1 Rep1"
   1.107    and     q2: "Quotient R2 Abs2 Rep2"
   1.108    shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
   1.109 @@ -111,12 +112,4 @@
   1.110  
   1.111  declare Pair_eq[quot_preserve]
   1.112  
   1.113 -lemma map_pair_id[id_simps]:
   1.114 -  shows "map_pair id id = id"
   1.115 -  by (simp add: fun_eq_iff)
   1.116 -
   1.117 -lemma prod_rel_eq[id_simps]:
   1.118 -  shows "prod_rel (op =) (op =) = (op =)"
   1.119 -  by (simp add: fun_eq_iff)
   1.120 -
   1.121  end