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