src/HOL/Library/Quotient_Sum.thy
changeset 40820 fd9c98ead9a9
parent 40610 70776ecfe324
child 41372 551eb49a6e91
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue Nov 30 15:58:09 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Nov 30 15:58:09 2010 +0100
     1.3 @@ -18,53 +18,68 @@
     1.4  
     1.5  declare [[map sum = (sum_map, sum_rel)]]
     1.6  
     1.7 +lemma sum_rel_unfold:
     1.8 +  "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
     1.9 +    | (Inr x, Inr y) \<Rightarrow> R2 x y
    1.10 +    | _ \<Rightarrow> False)"
    1.11 +  by (cases x) (cases y, simp_all)+
    1.12  
    1.13 -text {* should probably be in @{theory Sum_Type} *}
    1.14 -lemma split_sum_all:
    1.15 -  shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
    1.16 -  apply(auto)
    1.17 -  apply(case_tac x)
    1.18 -  apply(simp_all)
    1.19 -  done
    1.20 +lemma sum_rel_map1:
    1.21 +  "sum_rel R1 R2 (sum_map f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
    1.22 +  by (simp add: sum_rel_unfold split: sum.split)
    1.23 +
    1.24 +lemma sum_rel_map2:
    1.25 +  "sum_rel R1 R2 x (sum_map f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
    1.26 +  by (simp add: sum_rel_unfold split: sum.split)
    1.27 +
    1.28 +lemma sum_map_id [id_simps]:
    1.29 +  "sum_map id id = id"
    1.30 +  by (simp add: id_def sum_map.identity fun_eq_iff)
    1.31  
    1.32 -lemma sum_equivp[quot_equiv]:
    1.33 -  assumes a: "equivp R1"
    1.34 -  assumes b: "equivp R2"
    1.35 -  shows "equivp (sum_rel R1 R2)"
    1.36 -  apply(rule equivpI)
    1.37 -  unfolding reflp_def symp_def transp_def
    1.38 -  apply(simp_all add: split_sum_all)
    1.39 -  apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
    1.40 -  apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
    1.41 -  apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
    1.42 -  done
    1.43 +lemma sum_rel_eq [id_simps]:
    1.44 +  "sum_rel (op =) (op =) = (op =)"
    1.45 +  by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
    1.46 +
    1.47 +lemma sum_reflp:
    1.48 +  "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    1.49 +  by (auto simp add: sum_rel_unfold split: sum.splits intro!: reflpI elim: reflpE)
    1.50  
    1.51 -lemma sum_quotient[quot_thm]:
    1.52 +lemma sum_symp:
    1.53 +  "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    1.54 +  by (auto simp add: sum_rel_unfold split: sum.splits intro!: sympI elim: sympE)
    1.55 +
    1.56 +lemma sum_transp:
    1.57 +  "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
    1.58 +  by (auto simp add: sum_rel_unfold split: sum.splits intro!: transpI elim: transpE)
    1.59 +
    1.60 +lemma sum_equivp [quot_equiv]:
    1.61 +  "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
    1.62 +  by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
    1.63 +  
    1.64 +lemma sum_quotient [quot_thm]:
    1.65    assumes q1: "Quotient R1 Abs1 Rep1"
    1.66    assumes q2: "Quotient R2 Abs2 Rep2"
    1.67    shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
    1.68 -  unfolding Quotient_def
    1.69 -  apply(simp add: split_sum_all)
    1.70 -  apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
    1.71 -  apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
    1.72 -  using q1 q2
    1.73 -  unfolding Quotient_def
    1.74 -  apply(blast)+
    1.75 +  apply (rule QuotientI)
    1.76 +  apply (simp_all add: sum_map.compositionality sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
    1.77 +    Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])
    1.78 +  using Quotient_rel [OF q1] Quotient_rel [OF q2]
    1.79 +  apply (simp add: sum_rel_unfold split: sum.split)
    1.80    done
    1.81  
    1.82 -lemma sum_Inl_rsp[quot_respect]:
    1.83 +lemma sum_Inl_rsp [quot_respect]:
    1.84    assumes q1: "Quotient R1 Abs1 Rep1"
    1.85    assumes q2: "Quotient R2 Abs2 Rep2"
    1.86    shows "(R1 ===> sum_rel R1 R2) Inl Inl"
    1.87    by auto
    1.88  
    1.89 -lemma sum_Inr_rsp[quot_respect]:
    1.90 +lemma sum_Inr_rsp [quot_respect]:
    1.91    assumes q1: "Quotient R1 Abs1 Rep1"
    1.92    assumes q2: "Quotient R2 Abs2 Rep2"
    1.93    shows "(R2 ===> sum_rel R1 R2) Inr Inr"
    1.94    by auto
    1.95  
    1.96 -lemma sum_Inl_prs[quot_preserve]:
    1.97 +lemma sum_Inl_prs [quot_preserve]:
    1.98    assumes q1: "Quotient R1 Abs1 Rep1"
    1.99    assumes q2: "Quotient R2 Abs2 Rep2"
   1.100    shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
   1.101 @@ -72,7 +87,7 @@
   1.102    apply(simp add: Quotient_abs_rep[OF q1])
   1.103    done
   1.104  
   1.105 -lemma sum_Inr_prs[quot_preserve]:
   1.106 +lemma sum_Inr_prs [quot_preserve]:
   1.107    assumes q1: "Quotient R1 Abs1 Rep1"
   1.108    assumes q2: "Quotient R2 Abs2 Rep2"
   1.109    shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
   1.110 @@ -80,12 +95,4 @@
   1.111    apply(simp add: Quotient_abs_rep[OF q2])
   1.112    done
   1.113  
   1.114 -lemma sum_map_id[id_simps]:
   1.115 -  shows "sum_map id id = id"
   1.116 -  by (simp add: fun_eq_iff split_sum_all)
   1.117 -
   1.118 -lemma sum_rel_eq[id_simps]:
   1.119 -  shows "sum_rel (op =) (op =) = (op =)"
   1.120 -  by (simp add: fun_eq_iff split_sum_all)
   1.121 -
   1.122  end