src/HOL/Library/Quotient_Product.thy
changeset 40465 2989f9f3aa10
parent 39302 d7728f65b353
child 40541 7850b4cc1507
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Tue Nov 09 14:02:12 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Tue Nov 09 14:02:13 2010 +0100
     1.3 @@ -8,13 +8,16 @@
     1.4  imports Main Quotient_Syntax
     1.5  begin
     1.6  
     1.7 -fun
     1.8 -  prod_rel
     1.9 +definition
    1.10 +  prod_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.11  where
    1.12    "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    1.13  
    1.14  declare [[map prod = (prod_fun, prod_rel)]]
    1.15  
    1.16 +lemma prod_rel_apply [simp]:
    1.17 +  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    1.18 +  by (simp add: prod_rel_def)
    1.19  
    1.20  lemma prod_equivp[quot_equiv]:
    1.21    assumes a: "equivp R1"
    1.22 @@ -22,7 +25,7 @@
    1.23    shows "equivp (prod_rel R1 R2)"
    1.24    apply(rule equivpI)
    1.25    unfolding reflp_def symp_def transp_def
    1.26 -  apply(simp_all add: split_paired_all)
    1.27 +  apply(simp_all add: split_paired_all prod_rel_def)
    1.28    apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
    1.29    apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
    1.30    apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
    1.31 @@ -45,7 +48,7 @@
    1.32    assumes q1: "Quotient R1 Abs1 Rep1"
    1.33    assumes q2: "Quotient R2 Abs2 Rep2"
    1.34    shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
    1.35 -  by simp
    1.36 +  by (auto simp add: prod_rel_def)
    1.37  
    1.38  lemma Pair_prs[quot_preserve]:
    1.39    assumes q1: "Quotient R1 Abs1 Rep1"
    1.40 @@ -59,33 +62,29 @@
    1.41    assumes "Quotient R1 Abs1 Rep1"
    1.42    assumes "Quotient R2 Abs2 Rep2"
    1.43    shows "(prod_rel R1 R2 ===> R1) fst fst"
    1.44 -  by simp
    1.45 +  by auto
    1.46  
    1.47  lemma fst_prs[quot_preserve]:
    1.48    assumes q1: "Quotient R1 Abs1 Rep1"
    1.49    assumes q2: "Quotient R2 Abs2 Rep2"
    1.50    shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
    1.51 -  apply(simp add: fun_eq_iff)
    1.52 -  apply(simp add: Quotient_abs_rep[OF q1])
    1.53 -  done
    1.54 +  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
    1.55  
    1.56  lemma snd_rsp[quot_respect]:
    1.57    assumes "Quotient R1 Abs1 Rep1"
    1.58    assumes "Quotient R2 Abs2 Rep2"
    1.59    shows "(prod_rel R1 R2 ===> R2) snd snd"
    1.60 -  by simp
    1.61 +  by auto
    1.62  
    1.63  lemma snd_prs[quot_preserve]:
    1.64    assumes q1: "Quotient R1 Abs1 Rep1"
    1.65    assumes q2: "Quotient R2 Abs2 Rep2"
    1.66    shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
    1.67 -  apply(simp add: fun_eq_iff)
    1.68 -  apply(simp add: Quotient_abs_rep[OF q2])
    1.69 -  done
    1.70 +  by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
    1.71  
    1.72  lemma split_rsp[quot_respect]:
    1.73    shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
    1.74 -  by auto
    1.75 +  by (auto intro!: fun_relI elim!: fun_relE)
    1.76  
    1.77  lemma split_prs[quot_preserve]:
    1.78    assumes q1: "Quotient R1 Abs1 Rep1"
    1.79 @@ -96,7 +95,7 @@
    1.80  lemma [quot_respect]:
    1.81    shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
    1.82    prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel"
    1.83 -  by auto
    1.84 +  by (auto simp add: fun_rel_def)
    1.85  
    1.86  lemma [quot_preserve]:
    1.87    assumes q1: "Quotient R1 abs1 rep1"
    1.88 @@ -114,7 +113,7 @@
    1.89  
    1.90  lemma prod_fun_id[id_simps]:
    1.91    shows "prod_fun id id = id"
    1.92 -  by (simp add: prod_fun_def)
    1.93 +  by (simp add: fun_eq_iff)
    1.94  
    1.95  lemma prod_rel_eq[id_simps]:
    1.96    shows "prod_rel (op =) (op =) = (op =)"