src/HOL/Sum_Type.thy
 author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 41505 6d19301074cf child 45204 5e4a1270c000 permissions -rw-r--r--
new isCont theorems;
simplify some proofs.
```     1 (*  Title:      HOL/Sum_Type.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Copyright   1992  University of Cambridge
```
```     4 *)
```
```     5
```
```     6 header{*The Disjoint Sum of Two Types*}
```
```     7
```
```     8 theory Sum_Type
```
```     9 imports Typedef Inductive Fun
```
```    10 begin
```
```    11
```
```    12 subsection {* Construction of the sum type and its basic abstract operations *}
```
```    13
```
```    14 definition Inl_Rep :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
```
```    15   "Inl_Rep a x y p \<longleftrightarrow> x = a \<and> p"
```
```    16
```
```    17 definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
```
```    18   "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
```
```    19
```
```    20 typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
```
```    21   by auto
```
```    22
```
```    23 lemma Inl_RepI: "Inl_Rep a \<in> sum"
```
```    24   by (auto simp add: sum_def)
```
```    25
```
```    26 lemma Inr_RepI: "Inr_Rep b \<in> sum"
```
```    27   by (auto simp add: sum_def)
```
```    28
```
```    29 lemma inj_on_Abs_sum: "A \<subseteq> sum \<Longrightarrow> inj_on Abs_sum A"
```
```    30   by (rule inj_on_inverseI, rule Abs_sum_inverse) auto
```
```    31
```
```    32 lemma Inl_Rep_inject: "inj_on Inl_Rep A"
```
```    33 proof (rule inj_onI)
```
```    34   show "\<And>a c. Inl_Rep a = Inl_Rep c \<Longrightarrow> a = c"
```
```    35     by (auto simp add: Inl_Rep_def fun_eq_iff)
```
```    36 qed
```
```    37
```
```    38 lemma Inr_Rep_inject: "inj_on Inr_Rep A"
```
```    39 proof (rule inj_onI)
```
```    40   show "\<And>b d. Inr_Rep b = Inr_Rep d \<Longrightarrow> b = d"
```
```    41     by (auto simp add: Inr_Rep_def fun_eq_iff)
```
```    42 qed
```
```    43
```
```    44 lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b"
```
```    45   by (auto simp add: Inl_Rep_def Inr_Rep_def fun_eq_iff)
```
```    46
```
```    47 definition Inl :: "'a \<Rightarrow> 'a + 'b" where
```
```    48   "Inl = Abs_sum \<circ> Inl_Rep"
```
```    49
```
```    50 definition Inr :: "'b \<Rightarrow> 'a + 'b" where
```
```    51   "Inr = Abs_sum \<circ> Inr_Rep"
```
```    52
```
```    53 lemma inj_Inl [simp]: "inj_on Inl A"
```
```    54 by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)
```
```    55
```
```    56 lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y"
```
```    57 using inj_Inl by (rule injD)
```
```    58
```
```    59 lemma inj_Inr [simp]: "inj_on Inr A"
```
```    60 by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)
```
```    61
```
```    62 lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y"
```
```    63 using inj_Inr by (rule injD)
```
```    64
```
```    65 lemma Inl_not_Inr: "Inl a \<noteq> Inr b"
```
```    66 proof -
```
```    67   from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" by auto
```
```    68   with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
```
```    69   with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)" by auto
```
```    70   then show ?thesis by (simp add: Inl_def Inr_def)
```
```    71 qed
```
```    72
```
```    73 lemma Inr_not_Inl: "Inr b \<noteq> Inl a"
```
```    74   using Inl_not_Inr by (rule not_sym)
```
```    75
```
```    76 lemma sumE:
```
```    77   assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
```
```    78     and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
```
```    79   shows P
```
```    80 proof (rule Abs_sum_cases [of s])
```
```    81   fix f
```
```    82   assume "s = Abs_sum f" and "f \<in> sum"
```
```    83   with assms show P by (auto simp add: sum_def Inl_def Inr_def)
```
```    84 qed
```
```    85
```
```    86 rep_datatype Inl Inr
```
```    87 proof -
```
```    88   fix P
```
```    89   fix s :: "'a + 'b"
```
```    90   assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
```
```    91   then show "P s" by (auto intro: sumE [of s])
```
```    92 qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
```
```    93
```
```    94 primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
```
```    95   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
```
```    96 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
```
```    97
```
```    98 enriched_type sum_map: sum_map proof -
```
```    99   fix f g h i
```
```   100   show "sum_map f g \<circ> sum_map h i = sum_map (f \<circ> h) (g \<circ> i)"
```
```   101   proof
```
```   102     fix s
```
```   103     show "(sum_map f g \<circ> sum_map h i) s = sum_map (f \<circ> h) (g \<circ> i) s"
```
```   104       by (cases s) simp_all
```
```   105   qed
```
```   106 next
```
```   107   fix s
```
```   108   show "sum_map id id = id"
```
```   109   proof
```
```   110     fix s
```
```   111     show "sum_map id id s = id s"
```
```   112       by (cases s) simp_all
```
```   113   qed
```
```   114 qed
```
```   115
```
```   116
```
```   117 subsection {* Projections *}
```
```   118
```
```   119 lemma sum_case_KK [simp]: "sum_case (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)"
```
```   120   by (rule ext) (simp split: sum.split)
```
```   121
```
```   122 lemma surjective_sum: "sum_case (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f"
```
```   123 proof
```
```   124   fix s :: "'a + 'b"
```
```   125   show "(case s of Inl (x\<Colon>'a) \<Rightarrow> f (Inl x) | Inr (y\<Colon>'b) \<Rightarrow> f (Inr y)) = f s"
```
```   126     by (cases s) simp_all
```
```   127 qed
```
```   128
```
```   129 lemma sum_case_inject:
```
```   130   assumes a: "sum_case f1 f2 = sum_case g1 g2"
```
```   131   assumes r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
```
```   132   shows P
```
```   133 proof (rule r)
```
```   134   show "f1 = g1" proof
```
```   135     fix x :: 'a
```
```   136     from a have "sum_case f1 f2 (Inl x) = sum_case g1 g2 (Inl x)" by simp
```
```   137     then show "f1 x = g1 x" by simp
```
```   138   qed
```
```   139   show "f2 = g2" proof
```
```   140     fix y :: 'b
```
```   141     from a have "sum_case f1 f2 (Inr y) = sum_case g1 g2 (Inr y)" by simp
```
```   142     then show "f2 y = g2 y" by simp
```
```   143   qed
```
```   144 qed
```
```   145
```
```   146 lemma sum_case_weak_cong:
```
```   147   "s = t \<Longrightarrow> sum_case f g s = sum_case f g t"
```
```   148   -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
```
```   149   by simp
```
```   150
```
```   151 primrec Projl :: "'a + 'b \<Rightarrow> 'a" where
```
```   152   Projl_Inl: "Projl (Inl x) = x"
```
```   153
```
```   154 primrec Projr :: "'a + 'b \<Rightarrow> 'b" where
```
```   155   Projr_Inr: "Projr (Inr x) = x"
```
```   156
```
```   157 primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
```
```   158   "Suml f (Inl x) = f x"
```
```   159
```
```   160 primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
```
```   161   "Sumr f (Inr x) = f x"
```
```   162
```
```   163 lemma Suml_inject:
```
```   164   assumes "Suml f = Suml g" shows "f = g"
```
```   165 proof
```
```   166   fix x :: 'a
```
```   167   let ?s = "Inl x \<Colon> 'a + 'b"
```
```   168   from assms have "Suml f ?s = Suml g ?s" by simp
```
```   169   then show "f x = g x" by simp
```
```   170 qed
```
```   171
```
```   172 lemma Sumr_inject:
```
```   173   assumes "Sumr f = Sumr g" shows "f = g"
```
```   174 proof
```
```   175   fix x :: 'b
```
```   176   let ?s = "Inr x \<Colon> 'a + 'b"
```
```   177   from assms have "Sumr f ?s = Sumr g ?s" by simp
```
```   178   then show "f x = g x" by simp
```
```   179 qed
```
```   180
```
```   181
```
```   182 subsection {* The Disjoint Sum of Sets *}
```
```   183
```
```   184 definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where
```
```   185   "A <+> B = Inl ` A \<union> Inr ` B"
```
```   186
```
```   187 hide_const (open) Plus --"Valuable identifier"
```
```   188
```
```   189 lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B"
```
```   190 by (simp add: Plus_def)
```
```   191
```
```   192 lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B"
```
```   193 by (simp add: Plus_def)
```
```   194
```
```   195 text {* Exhaustion rule for sums, a degenerate form of induction *}
```
```   196
```
```   197 lemma PlusE [elim!]:
```
```   198   "u \<in> A <+> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> u = Inl x \<Longrightarrow> P) \<Longrightarrow> (\<And>y. y \<in> B \<Longrightarrow> u = Inr y \<Longrightarrow> P) \<Longrightarrow> P"
```
```   199 by (auto simp add: Plus_def)
```
```   200
```
```   201 lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
```
```   202 by auto
```
```   203
```
```   204 lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
```
```   205 proof (rule set_eqI)
```
```   206   fix u :: "'a + 'b"
```
```   207   show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
```
```   208 qed
```
```   209
```
```   210 hide_const (open) Suml Sumr Projl Projr
```
```   211
```
```   212 end
```