src/HOL/Sum_Type.thy
 author paulson Tue Apr 25 16:39:54 2017 +0100 (2017-04-25) changeset 65578 e4997c181cce parent 63575 b9bd9e61fd63 child 67443 3abf6a722518 permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
```     1 (*  Title:      HOL/Sum_Type.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Copyright   1992  University of Cambridge
```
```     4 *)
```
```     5
```
```     6 section \<open>The Disjoint Sum of Two Types\<close>
```
```     7
```
```     8 theory Sum_Type
```
```     9   imports Typedef Inductive Fun
```
```    10 begin
```
```    11
```
```    12 subsection \<open>Construction of the sum type and its basic abstract operations\<close>
```
```    13
```
```    14 definition Inl_Rep :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool"
```
```    15   where "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"
```
```    18   where "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
```
```    19
```
```    20 definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
```
```    21
```
```    22 typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool) set"
```
```    23   unfolding sum_def by auto
```
```    24
```
```    25 lemma Inl_RepI: "Inl_Rep a \<in> sum"
```
```    26   by (auto simp add: sum_def)
```
```    27
```
```    28 lemma Inr_RepI: "Inr_Rep b \<in> sum"
```
```    29   by (auto simp add: sum_def)
```
```    30
```
```    31 lemma inj_on_Abs_sum: "A \<subseteq> sum \<Longrightarrow> inj_on Abs_sum A"
```
```    32   by (rule inj_on_inverseI, rule Abs_sum_inverse) auto
```
```    33
```
```    34 lemma Inl_Rep_inject: "inj_on Inl_Rep A"
```
```    35 proof (rule inj_onI)
```
```    36   show "\<And>a c. Inl_Rep a = Inl_Rep c \<Longrightarrow> a = c"
```
```    37     by (auto simp add: Inl_Rep_def fun_eq_iff)
```
```    38 qed
```
```    39
```
```    40 lemma Inr_Rep_inject: "inj_on Inr_Rep A"
```
```    41 proof (rule inj_onI)
```
```    42   show "\<And>b d. Inr_Rep b = Inr_Rep d \<Longrightarrow> b = d"
```
```    43     by (auto simp add: Inr_Rep_def fun_eq_iff)
```
```    44 qed
```
```    45
```
```    46 lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b"
```
```    47   by (auto simp add: Inl_Rep_def Inr_Rep_def fun_eq_iff)
```
```    48
```
```    49 definition Inl :: "'a \<Rightarrow> 'a + 'b"
```
```    50   where "Inl = Abs_sum \<circ> Inl_Rep"
```
```    51
```
```    52 definition Inr :: "'b \<Rightarrow> 'a + 'b"
```
```    53   where "Inr = Abs_sum \<circ> Inr_Rep"
```
```    54
```
```    55 lemma inj_Inl [simp]: "inj_on Inl A"
```
```    56   by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)
```
```    57
```
```    58 lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y"
```
```    59   using inj_Inl by (rule injD)
```
```    60
```
```    61 lemma inj_Inr [simp]: "inj_on Inr A"
```
```    62   by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)
```
```    63
```
```    64 lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y"
```
```    65   using inj_Inr by (rule injD)
```
```    66
```
```    67 lemma Inl_not_Inr: "Inl a \<noteq> Inr b"
```
```    68 proof -
```
```    69   have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum"
```
```    70     using Inl_RepI [of a] Inr_RepI [of b] by auto
```
```    71   with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
```
```    72   with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)"
```
```    73     by auto
```
```    74   then show ?thesis
```
```    75     by (simp add: Inl_def Inr_def)
```
```    76 qed
```
```    77
```
```    78 lemma Inr_not_Inl: "Inr b \<noteq> Inl a"
```
```    79   using Inl_not_Inr by (rule not_sym)
```
```    80
```
```    81 lemma sumE:
```
```    82   assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
```
```    83     and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
```
```    84   shows P
```
```    85 proof (rule Abs_sum_cases [of s])
```
```    86   fix f
```
```    87   assume "s = Abs_sum f" and "f \<in> sum"
```
```    88   with assms show P
```
```    89     by (auto simp add: sum_def Inl_def Inr_def)
```
```    90 qed
```
```    91
```
```    92 free_constructors case_sum for
```
```    93   isl: Inl projl
```
```    94 | Inr projr
```
```    95   by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
```
```    96
```
```    97 text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
```
```    98
```
```    99 setup \<open>Sign.mandatory_path "old"\<close>
```
```   100
```
```   101 old_rep_datatype Inl Inr
```
```   102 proof -
```
```   103   fix P
```
```   104   fix s :: "'a + 'b"
```
```   105   assume x: "\<And>x::'a. P (Inl x)" and y: "\<And>y::'b. P (Inr y)"
```
```   106   then show "P s" by (auto intro: sumE [of s])
```
```   107 qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
```
```   108
```
```   109 setup \<open>Sign.parent_path\<close>
```
```   110
```
```   111 text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
```
```   112
```
```   113 setup \<open>Sign.mandatory_path "sum"\<close>
```
```   114
```
```   115 declare
```
```   116   old.sum.inject[iff del]
```
```   117   old.sum.distinct(1)[simp del, induct_simp del]
```
```   118
```
```   119 lemmas induct = old.sum.induct
```
```   120 lemmas inducts = old.sum.inducts
```
```   121 lemmas rec = old.sum.rec
```
```   122 lemmas simps = sum.inject sum.distinct sum.case sum.rec
```
```   123
```
```   124 setup \<open>Sign.parent_path\<close>
```
```   125
```
```   126 primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
```
```   127   where
```
```   128     "map_sum f1 f2 (Inl a) = Inl (f1 a)"
```
```   129   | "map_sum f1 f2 (Inr a) = Inr (f2 a)"
```
```   130
```
```   131 functor map_sum: map_sum
```
```   132 proof -
```
```   133   show "map_sum f g \<circ> map_sum h i = map_sum (f \<circ> h) (g \<circ> i)" for f g h i
```
```   134   proof
```
```   135     show "(map_sum f g \<circ> map_sum h i) s = map_sum (f \<circ> h) (g \<circ> i) s" for s
```
```   136       by (cases s) simp_all
```
```   137   qed
```
```   138   show "map_sum id id = id"
```
```   139   proof
```
```   140     show "map_sum id id s = id s" for s
```
```   141       by (cases s) simp_all
```
```   142   qed
```
```   143 qed
```
```   144
```
```   145 lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
```
```   146   by (auto intro: sum.induct)
```
```   147
```
```   148 lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
```
```   149   using split_sum_all[of "\<lambda>x. \<not>P x"] by blast
```
```   150
```
```   151
```
```   152 subsection \<open>Projections\<close>
```
```   153
```
```   154 lemma case_sum_KK [simp]: "case_sum (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)"
```
```   155   by (rule ext) (simp split: sum.split)
```
```   156
```
```   157 lemma surjective_sum: "case_sum (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f"
```
```   158 proof
```
```   159   fix s :: "'a + 'b"
```
```   160   show "(case s of Inl (x::'a) \<Rightarrow> f (Inl x) | Inr (y::'b) \<Rightarrow> f (Inr y)) = f s"
```
```   161     by (cases s) simp_all
```
```   162 qed
```
```   163
```
```   164 lemma case_sum_inject:
```
```   165   assumes a: "case_sum f1 f2 = case_sum g1 g2"
```
```   166     and r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
```
```   167   shows P
```
```   168 proof (rule r)
```
```   169   show "f1 = g1"
```
```   170   proof
```
```   171     fix x :: 'a
```
```   172     from a have "case_sum f1 f2 (Inl x) = case_sum g1 g2 (Inl x)" by simp
```
```   173     then show "f1 x = g1 x" by simp
```
```   174   qed
```
```   175   show "f2 = g2"
```
```   176   proof
```
```   177     fix y :: 'b
```
```   178     from a have "case_sum f1 f2 (Inr y) = case_sum g1 g2 (Inr y)" by simp
```
```   179     then show "f2 y = g2 y" by simp
```
```   180   qed
```
```   181 qed
```
```   182
```
```   183 primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c"
```
```   184   where "Suml f (Inl x) = f x"
```
```   185
```
```   186 primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c"
```
```   187   where "Sumr f (Inr x) = f x"
```
```   188
```
```   189 lemma Suml_inject:
```
```   190   assumes "Suml f = Suml g"
```
```   191   shows "f = g"
```
```   192 proof
```
```   193   fix x :: 'a
```
```   194   let ?s = "Inl x :: 'a + 'b"
```
```   195   from assms have "Suml f ?s = Suml g ?s" by simp
```
```   196   then show "f x = g x" by simp
```
```   197 qed
```
```   198
```
```   199 lemma Sumr_inject:
```
```   200   assumes "Sumr f = Sumr g"
```
```   201   shows "f = g"
```
```   202 proof
```
```   203   fix x :: 'b
```
```   204   let ?s = "Inr x :: 'a + 'b"
```
```   205   from assms have "Sumr f ?s = Sumr g ?s" by simp
```
```   206   then show "f x = g x" by simp
```
```   207 qed
```
```   208
```
```   209
```
```   210 subsection \<open>The Disjoint Sum of Sets\<close>
```
```   211
```
```   212 definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set"  (infixr "<+>" 65)
```
```   213   where "A <+> B = Inl ` A \<union> Inr ` B"
```
```   214
```
```   215 hide_const (open) Plus \<comment> "Valuable identifier"
```
```   216
```
```   217 lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B"
```
```   218   by (simp add: Plus_def)
```
```   219
```
```   220 lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B"
```
```   221   by (simp add: Plus_def)
```
```   222
```
```   223 text \<open>Exhaustion rule for sums, a degenerate form of induction\<close>
```
```   224
```
```   225 lemma PlusE [elim!]:
```
```   226   "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"
```
```   227   by (auto simp add: Plus_def)
```
```   228
```
```   229 lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
```
```   230   by auto
```
```   231
```
```   232 lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
```
```   233 proof (rule set_eqI)
```
```   234   fix u :: "'a + 'b"
```
```   235   show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
```
```   236 qed
```
```   237
```
```   238 lemma UNIV_sum: "UNIV = Inl ` UNIV \<union> Inr ` UNIV"
```
```   239 proof -
```
```   240   have "x \<in> range Inl" if "x \<notin> range Inr" for x :: "'a + 'b"
```
```   241     using that by (cases x) simp_all
```
```   242   then show ?thesis by auto
```
```   243 qed
```
```   244
```
```   245 hide_const (open) Suml Sumr sum
```
```   246
```
```   247 end
```