src/HOL/Sum_Type.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 33995 ebf231de0c5c
child 36176 3fe7e97ccca8
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     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 global
    21 
    22 typedef (Sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
    23   by auto
    24 
    25 local
    26 
    27 lemma Inl_RepI: "Inl_Rep a \<in> Sum"
    28   by (auto simp add: Sum_def)
    29 
    30 lemma Inr_RepI: "Inr_Rep b \<in> Sum"
    31   by (auto simp add: Sum_def)
    32 
    33 lemma inj_on_Abs_Sum: "A \<subseteq> Sum \<Longrightarrow> inj_on Abs_Sum A"
    34   by (rule inj_on_inverseI, rule Abs_Sum_inverse) auto
    35 
    36 lemma Inl_Rep_inject: "inj_on Inl_Rep A"
    37 proof (rule inj_onI)
    38   show "\<And>a c. Inl_Rep a = Inl_Rep c \<Longrightarrow> a = c"
    39     by (auto simp add: Inl_Rep_def expand_fun_eq)
    40 qed
    41 
    42 lemma Inr_Rep_inject: "inj_on Inr_Rep A"
    43 proof (rule inj_onI)
    44   show "\<And>b d. Inr_Rep b = Inr_Rep d \<Longrightarrow> b = d"
    45     by (auto simp add: Inr_Rep_def expand_fun_eq)
    46 qed
    47 
    48 lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b"
    49   by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq)
    50 
    51 definition Inl :: "'a \<Rightarrow> 'a + 'b" where
    52   "Inl = Abs_Sum \<circ> Inl_Rep"
    53 
    54 definition Inr :: "'b \<Rightarrow> 'a + 'b" where
    55   "Inr = Abs_Sum \<circ> Inr_Rep"
    56 
    57 lemma inj_Inl [simp]: "inj_on Inl A"
    58 by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_Sum Inl_RepI)
    59 
    60 lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y"
    61 using inj_Inl by (rule injD)
    62 
    63 lemma inj_Inr [simp]: "inj_on Inr A"
    64 by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_Sum Inr_RepI)
    65 
    66 lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y"
    67 using inj_Inr by (rule injD)
    68 
    69 lemma Inl_not_Inr: "Inl a \<noteq> Inr b"
    70 proof -
    71   from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> Sum" by auto
    72   with inj_on_Abs_Sum have "inj_on Abs_Sum {Inl_Rep a, Inr_Rep b}" .
    73   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
    74   then show ?thesis by (simp add: Inl_def Inr_def)
    75 qed
    76 
    77 lemma Inr_not_Inl: "Inr b \<noteq> Inl a" 
    78   using Inl_not_Inr by (rule not_sym)
    79 
    80 lemma sumE: 
    81   assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
    82     and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
    83   shows P
    84 proof (rule Abs_Sum_cases [of s])
    85   fix f 
    86   assume "s = Abs_Sum f" and "f \<in> Sum"
    87   with assms show P by (auto simp add: Sum_def Inl_def Inr_def)
    88 qed
    89 
    90 rep_datatype (sum) Inl Inr
    91 proof -
    92   fix P
    93   fix s :: "'a + 'b"
    94   assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
    95   then show "P s" by (auto intro: sumE [of s])
    96 qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
    97 
    98 
    99 subsection {* Projections *}
   100 
   101 lemma sum_case_KK [simp]: "sum_case (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)"
   102   by (rule ext) (simp split: sum.split)
   103 
   104 lemma surjective_sum: "sum_case (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f"
   105 proof
   106   fix s :: "'a + 'b"
   107   show "(case s of Inl (x\<Colon>'a) \<Rightarrow> f (Inl x) | Inr (y\<Colon>'b) \<Rightarrow> f (Inr y)) = f s"
   108     by (cases s) simp_all
   109 qed
   110 
   111 lemma sum_case_inject:
   112   assumes a: "sum_case f1 f2 = sum_case g1 g2"
   113   assumes r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
   114   shows P
   115 proof (rule r)
   116   show "f1 = g1" proof
   117     fix x :: 'a
   118     from a have "sum_case f1 f2 (Inl x) = sum_case g1 g2 (Inl x)" by simp
   119     then show "f1 x = g1 x" by simp
   120   qed
   121   show "f2 = g2" proof
   122     fix y :: 'b
   123     from a have "sum_case f1 f2 (Inr y) = sum_case g1 g2 (Inr y)" by simp
   124     then show "f2 y = g2 y" by simp
   125   qed
   126 qed
   127 
   128 lemma sum_case_weak_cong:
   129   "s = t \<Longrightarrow> sum_case f g s = sum_case f g t"
   130   -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
   131   by simp
   132 
   133 primrec Projl :: "'a + 'b \<Rightarrow> 'a" where
   134   Projl_Inl: "Projl (Inl x) = x"
   135 
   136 primrec Projr :: "'a + 'b \<Rightarrow> 'b" where
   137   Projr_Inr: "Projr (Inr x) = x"
   138 
   139 primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
   140   "Suml f (Inl x) = f x"
   141 
   142 primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
   143   "Sumr f (Inr x) = f x"
   144 
   145 lemma Suml_inject:
   146   assumes "Suml f = Suml g" shows "f = g"
   147 proof
   148   fix x :: 'a
   149   let ?s = "Inl x \<Colon> 'a + 'b"
   150   from assms have "Suml f ?s = Suml g ?s" by simp
   151   then show "f x = g x" by simp
   152 qed
   153 
   154 lemma Sumr_inject:
   155   assumes "Sumr f = Sumr g" shows "f = g"
   156 proof
   157   fix x :: 'b
   158   let ?s = "Inr x \<Colon> 'a + 'b"
   159   from assms have "Sumr f ?s = Sumr g ?s" by simp
   160   then show "f x = g x" by simp
   161 qed
   162 
   163 
   164 subsection {* The Disjoint Sum of Sets *}
   165 
   166 definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where
   167   "A <+> B = Inl ` A \<union> Inr ` B"
   168 
   169 lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B"
   170 by (simp add: Plus_def)
   171 
   172 lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B"
   173 by (simp add: Plus_def)
   174 
   175 text {* Exhaustion rule for sums, a degenerate form of induction *}
   176 
   177 lemma PlusE [elim!]: 
   178   "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"
   179 by (auto simp add: Plus_def)
   180 
   181 lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
   182 by auto
   183 
   184 lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
   185 proof (rule set_ext)
   186   fix u :: "'a + 'b"
   187   show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
   188 qed
   189 
   190 hide (open) const Suml Sumr Projl Projr
   191 
   192 end