src/HOL/Library/Quotient_Sum.thy
 author Manuel Eberl Mon Mar 26 16:14:16 2018 +0200 (18 months ago) changeset 67951 655aa11359dc parent 67399 eab6ce8368fa permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
```     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 (=) (=) = (=)"
```
```    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
```