src/HOL/Library/Quotient_Sum.thy
author blanchet
Thu Mar 06 13:36:15 2014 +0100 (2014-03-06)
changeset 55931 62156e694f3d
parent 55564 e81ee43ab290
child 55943 5c2df04e97d1
permissions -rw-r--r--
renamed 'map_sum' to 'sum_map'
     1 (*  Title:      HOL/Library/Quotient_Sum.thy
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 *)
     4 
     5 header {* Quotient infrastructure for the sum type *}
     6 
     7 theory Quotient_Sum
     8 imports Main Quotient_Syntax
     9 begin
    10 
    11 subsection {* Rules for the Quotient package *}
    12 
    13 lemma sum_rel_map1:
    14   "sum_rel R1 R2 (map_sum f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
    15   by (simp add: sum_rel_def split: sum.split)
    16 
    17 lemma sum_rel_map2:
    18   "sum_rel R1 R2 x (map_sum f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
    19   by (simp add: sum_rel_def split: sum.split)
    20 
    21 lemma map_sum_id [id_simps]:
    22   "map_sum id id = id"
    23   by (simp add: id_def map_sum.identity fun_eq_iff)
    24 
    25 lemma sum_rel_eq [id_simps]:
    26   "sum_rel (op =) (op =) = (op =)"
    27   by (simp add: sum_rel_def fun_eq_iff split: sum.split)
    28 
    29 lemma reflp_sum_rel:
    30   "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    31   unfolding reflp_def split_sum_all sum_rel_simps by fast
    32 
    33 lemma sum_symp:
    34   "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    35   unfolding symp_def split_sum_all sum_rel_simps by fast
    36 
    37 lemma sum_transp:
    38   "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
    39   unfolding transp_def split_sum_all sum_rel_simps by fast
    40 
    41 lemma sum_equivp [quot_equiv]:
    42   "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
    43   by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE)
    44 
    45 lemma sum_quotient [quot_thm]:
    46   assumes q1: "Quotient3 R1 Abs1 Rep1"
    47   assumes q2: "Quotient3 R2 Abs2 Rep2"
    48   shows "Quotient3 (sum_rel R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2)"
    49   apply (rule Quotient3I)
    50   apply (simp_all add: map_sum.compositionality comp_def map_sum.identity sum_rel_eq sum_rel_map1 sum_rel_map2
    51     Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
    52   using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
    53   apply (simp add: sum_rel_def comp_def split: sum.split)
    54   done
    55 
    56 declare [[mapQ3 sum = (sum_rel, sum_quotient)]]
    57 
    58 lemma sum_Inl_rsp [quot_respect]:
    59   assumes q1: "Quotient3 R1 Abs1 Rep1"
    60   assumes q2: "Quotient3 R2 Abs2 Rep2"
    61   shows "(R1 ===> sum_rel R1 R2) Inl Inl"
    62   by auto
    63 
    64 lemma sum_Inr_rsp [quot_respect]:
    65   assumes q1: "Quotient3 R1 Abs1 Rep1"
    66   assumes q2: "Quotient3 R2 Abs2 Rep2"
    67   shows "(R2 ===> sum_rel R1 R2) Inr Inr"
    68   by auto
    69 
    70 lemma sum_Inl_prs [quot_preserve]:
    71   assumes q1: "Quotient3 R1 Abs1 Rep1"
    72   assumes q2: "Quotient3 R2 Abs2 Rep2"
    73   shows "(Rep1 ---> map_sum Abs1 Abs2) Inl = Inl"
    74   apply(simp add: fun_eq_iff)
    75   apply(simp add: Quotient3_abs_rep[OF q1])
    76   done
    77 
    78 lemma sum_Inr_prs [quot_preserve]:
    79   assumes q1: "Quotient3 R1 Abs1 Rep1"
    80   assumes q2: "Quotient3 R2 Abs2 Rep2"
    81   shows "(Rep2 ---> map_sum Abs1 Abs2) Inr = Inr"
    82   apply(simp add: fun_eq_iff)
    83   apply(simp add: Quotient3_abs_rep[OF q2])
    84   done
    85 
    86 end