src/HOL/Sum_Type.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58306 117ba6cbe414
child 60758 d8d85a8172b5
permissions -rw-r--r--
modernized header uniformly as section;
     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{*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 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 => 'b => bool => 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" where
    50   "Inl = Abs_sum \<circ> Inl_Rep"
    51 
    52 definition Inr :: "'b \<Rightarrow> 'a + 'b" where
    53   "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   from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" by auto
    70   with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
    71   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
    72   then show ?thesis by (simp add: Inl_def Inr_def)
    73 qed
    74 
    75 lemma Inr_not_Inl: "Inr b \<noteq> Inl a" 
    76   using Inl_not_Inr by (rule not_sym)
    77 
    78 lemma sumE: 
    79   assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
    80     and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
    81   shows P
    82 proof (rule Abs_sum_cases [of s])
    83   fix f 
    84   assume "s = Abs_sum f" and "f \<in> sum"
    85   with assms show P by (auto simp add: sum_def Inl_def Inr_def)
    86 qed
    87 
    88 free_constructors case_sum for
    89     isl: Inl projl
    90   | Inr projr
    91   by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
    92 
    93 text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
    94 
    95 setup {* Sign.mandatory_path "old" *}
    96 
    97 old_rep_datatype Inl Inr
    98 proof -
    99   fix P
   100   fix s :: "'a + 'b"
   101   assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
   102   then show "P s" by (auto intro: sumE [of s])
   103 qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
   104 
   105 setup {* Sign.parent_path *}
   106 
   107 text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
   108 
   109 setup {* Sign.mandatory_path "sum" *}
   110 
   111 declare
   112   old.sum.inject[iff del]
   113   old.sum.distinct(1)[simp del, induct_simp del]
   114 
   115 lemmas induct = old.sum.induct
   116 lemmas inducts = old.sum.inducts
   117 lemmas rec = old.sum.rec
   118 lemmas simps = sum.inject sum.distinct sum.case sum.rec
   119 
   120 setup {* Sign.parent_path *}
   121 
   122 primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
   123   "map_sum f1 f2 (Inl a) = Inl (f1 a)"
   124 | "map_sum f1 f2 (Inr a) = Inr (f2 a)"
   125 
   126 functor map_sum: map_sum proof -
   127   fix f g h i
   128   show "map_sum f g \<circ> map_sum h i = map_sum (f \<circ> h) (g \<circ> i)"
   129   proof
   130     fix s
   131     show "(map_sum f g \<circ> map_sum h i) s = map_sum (f \<circ> h) (g \<circ> i) s"
   132       by (cases s) simp_all
   133   qed
   134 next
   135   fix s
   136   show "map_sum id id = id"
   137   proof
   138     fix s
   139     show "map_sum id id s = id s" 
   140       by (cases s) simp_all
   141   qed
   142 qed
   143 
   144 lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
   145   by (auto intro: sum.induct)
   146 
   147 lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
   148 using split_sum_all[of "\<lambda>x. \<not>P x"] by blast
   149 
   150 subsection {* Projections *}
   151 
   152 lemma case_sum_KK [simp]: "case_sum (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)"
   153   by (rule ext) (simp split: sum.split)
   154 
   155 lemma surjective_sum: "case_sum (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f"
   156 proof
   157   fix s :: "'a + 'b"
   158   show "(case s of Inl (x\<Colon>'a) \<Rightarrow> f (Inl x) | Inr (y\<Colon>'b) \<Rightarrow> f (Inr y)) = f s"
   159     by (cases s) simp_all
   160 qed
   161 
   162 lemma case_sum_inject:
   163   assumes a: "case_sum f1 f2 = case_sum g1 g2"
   164   assumes r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
   165   shows P
   166 proof (rule r)
   167   show "f1 = g1" proof
   168     fix x :: 'a
   169     from a have "case_sum f1 f2 (Inl x) = case_sum g1 g2 (Inl x)" by simp
   170     then show "f1 x = g1 x" by simp
   171   qed
   172   show "f2 = g2" proof
   173     fix y :: 'b
   174     from a have "case_sum f1 f2 (Inr y) = case_sum g1 g2 (Inr y)" by simp
   175     then show "f2 y = g2 y" by simp
   176   qed
   177 qed
   178 
   179 primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
   180   "Suml f (Inl x) = f x"
   181 
   182 primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
   183   "Sumr f (Inr x) = f x"
   184 
   185 lemma Suml_inject:
   186   assumes "Suml f = Suml g" shows "f = g"
   187 proof
   188   fix x :: 'a
   189   let ?s = "Inl x \<Colon> 'a + 'b"
   190   from assms have "Suml f ?s = Suml g ?s" by simp
   191   then show "f x = g x" by simp
   192 qed
   193 
   194 lemma Sumr_inject:
   195   assumes "Sumr f = Sumr g" shows "f = g"
   196 proof
   197   fix x :: 'b
   198   let ?s = "Inr x \<Colon> 'a + 'b"
   199   from assms have "Sumr f ?s = Sumr g ?s" by simp
   200   then show "f x = g x" by simp
   201 qed
   202 
   203 
   204 subsection {* The Disjoint Sum of Sets *}
   205 
   206 definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where
   207   "A <+> B = Inl ` A \<union> Inr ` B"
   208 
   209 hide_const (open) Plus --"Valuable identifier"
   210 
   211 lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B"
   212 by (simp add: Plus_def)
   213 
   214 lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B"
   215 by (simp add: Plus_def)
   216 
   217 text {* Exhaustion rule for sums, a degenerate form of induction *}
   218 
   219 lemma PlusE [elim!]: 
   220   "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"
   221 by (auto simp add: Plus_def)
   222 
   223 lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
   224 by auto
   225 
   226 lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
   227 proof (rule set_eqI)
   228   fix u :: "'a + 'b"
   229   show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
   230 qed
   231 
   232 lemma UNIV_sum:
   233   "UNIV = Inl ` UNIV \<union> Inr ` UNIV"
   234 proof -
   235   { fix x :: "'a + 'b"
   236     assume "x \<notin> range Inr"
   237     then have "x \<in> range Inl"
   238     by (cases x) simp_all
   239   } then show ?thesis by auto
   240 qed
   241 
   242 hide_const (open) Suml Sumr sum
   243 
   244 end