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