src/HOL/Library/Quotient_Sum.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 62954 c5d0fdc260fa
child 67399 eab6ce8368fa
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Library/Quotient_Sum.thy
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 *)
     4 
     5 section \<open>Quotient infrastructure for the sum type\<close>
     6 
     7 theory Quotient_Sum
     8 imports Quotient_Syntax
     9 begin
    10 
    11 subsection \<open>Rules for the Quotient package\<close>
    12 
    13 lemma rel_sum_map1:
    14   "rel_sum R1 R2 (map_sum f1 f2 x) y \<longleftrightarrow> rel_sum (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
    15   by (rule sum.rel_map(1))
    16 
    17 lemma rel_sum_map2:
    18   "rel_sum R1 R2 x (map_sum f1 f2 y) \<longleftrightarrow> rel_sum (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
    19   by (rule sum.rel_map(2))
    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 rel_sum_eq [id_simps]:
    26   "rel_sum (op =) (op =) = (op =)"
    27   by (rule sum.rel_eq)
    28 
    29 lemma reflp_rel_sum:
    30   "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (rel_sum R1 R2)"
    31   unfolding reflp_def split_sum_all rel_sum_simps by fast
    32 
    33 lemma sum_symp:
    34   "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (rel_sum R1 R2)"
    35   unfolding symp_def split_sum_all rel_sum_simps by fast
    36 
    37 lemma sum_transp:
    38   "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (rel_sum R1 R2)"
    39   unfolding transp_def split_sum_all rel_sum_simps by fast
    40 
    41 lemma sum_equivp [quot_equiv]:
    42   "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (rel_sum R1 R2)"
    43   by (blast intro: equivpI reflp_rel_sum 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 (rel_sum 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 rel_sum_eq rel_sum_map1 rel_sum_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 (fastforce elim!: rel_sum.cases simp add: comp_def split: sum.split)
    54   done
    55 
    56 declare [[mapQ3 sum = (rel_sum, 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 ===> rel_sum 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 ===> rel_sum 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