src/HOL/Sum_Type.thy
author nipkow
Mon, 13 Sep 2010 11:13:15 +0200
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 40271 6014e8252e57
permissions -rw-r--r--
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Sum_Type.thy
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     3
    Copyright   1992  University of Cambridge
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     4
*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     5
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
     6
header{*The Disjoint Sum of Two Types*}
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     7
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
     8
theory Sum_Type
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
     9
imports Typedef Inductive Fun
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    10
begin
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    11
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    12
subsection {* Construction of the sum type and its basic abstract operations *}
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    13
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    14
definition Inl_Rep :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    15
  "Inl_Rep a x y p \<longleftrightarrow> x = a \<and> p"
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    16
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    17
definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    18
  "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    19
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37388
diff changeset
    20
typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    21
  by auto
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    22
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    23
lemma Inl_RepI: "Inl_Rep a \<in> sum"
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    24
  by (auto simp add: sum_def)
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    25
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    26
lemma Inr_RepI: "Inr_Rep b \<in> sum"
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    27
  by (auto simp add: sum_def)
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    28
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    29
lemma inj_on_Abs_sum: "A \<subseteq> sum \<Longrightarrow> inj_on Abs_sum A"
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    30
  by (rule inj_on_inverseI, rule Abs_sum_inverse) auto
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    31
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    32
lemma Inl_Rep_inject: "inj_on Inl_Rep A"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    33
proof (rule inj_onI)
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    34
  show "\<And>a c. Inl_Rep a = Inl_Rep c \<Longrightarrow> a = c"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
    35
    by (auto simp add: Inl_Rep_def fun_eq_iff)
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    36
qed
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    37
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    38
lemma Inr_Rep_inject: "inj_on Inr_Rep A"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    39
proof (rule inj_onI)
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    40
  show "\<And>b d. Inr_Rep b = Inr_Rep d \<Longrightarrow> b = d"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
    41
    by (auto simp add: Inr_Rep_def fun_eq_iff)
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    42
qed
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    43
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    44
lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
    45
  by (auto simp add: Inl_Rep_def Inr_Rep_def fun_eq_iff)
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    46
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    47
definition Inl :: "'a \<Rightarrow> 'a + 'b" where
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    48
  "Inl = Abs_sum \<circ> Inl_Rep"
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    49
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    50
definition Inr :: "'b \<Rightarrow> 'a + 'b" where
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    51
  "Inr = Abs_sum \<circ> Inr_Rep"
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    52
29025
8c8859c0d734 move lemmas from Numeral_Type.thy to other theories
huffman
parents: 28524
diff changeset
    53
lemma inj_Inl [simp]: "inj_on Inl A"
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    54
by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)
29025
8c8859c0d734 move lemmas from Numeral_Type.thy to other theories
huffman
parents: 28524
diff changeset
    55
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    56
lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    57
using inj_Inl by (rule injD)
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    58
29025
8c8859c0d734 move lemmas from Numeral_Type.thy to other theories
huffman
parents: 28524
diff changeset
    59
lemma inj_Inr [simp]: "inj_on Inr A"
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    60
by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    61
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    62
lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    63
using inj_Inr by (rule injD)
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    64
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    65
lemma Inl_not_Inr: "Inl a \<noteq> Inr b"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    66
proof -
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    67
  from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" by auto
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    68
  with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    69
  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
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    70
  then show ?thesis by (simp add: Inl_def Inr_def)
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    71
qed
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    72
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    73
lemma Inr_not_Inl: "Inr b \<noteq> Inl a" 
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    74
  using Inl_not_Inr by (rule not_sym)
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    75
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    76
lemma sumE: 
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    77
  assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    78
    and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    79
  shows P
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    80
proof (rule Abs_sum_cases [of s])
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    81
  fix f 
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    82
  assume "s = Abs_sum f" and "f \<in> sum"
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    83
  with assms show P by (auto simp add: sum_def Inl_def Inr_def)
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    84
qed
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
    85
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37388
diff changeset
    86
rep_datatype Inl Inr
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
    87
proof -
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
    88
  fix P
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
    89
  fix s :: "'a + 'b"
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
    90
  assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
    91
  then show "P s" by (auto intro: sumE [of s])
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    92
qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    93
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
    94
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    95
subsection {* Projections *}
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    96
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    97
lemma sum_case_KK [simp]: "sum_case (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)"
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
    98
  by (rule ext) (simp split: sum.split)
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
    99
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   100
lemma surjective_sum: "sum_case (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   101
proof
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   102
  fix s :: "'a + 'b"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   103
  show "(case s of Inl (x\<Colon>'a) \<Rightarrow> f (Inl x) | Inr (y\<Colon>'b) \<Rightarrow> f (Inr y)) = f s"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   104
    by (cases s) simp_all
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   105
qed
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   106
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   107
lemma sum_case_inject:
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   108
  assumes a: "sum_case f1 f2 = sum_case g1 g2"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   109
  assumes r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   110
  shows P
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   111
proof (rule r)
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   112
  show "f1 = g1" proof
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   113
    fix x :: 'a
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   114
    from a have "sum_case f1 f2 (Inl x) = sum_case g1 g2 (Inl x)" by simp
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   115
    then show "f1 x = g1 x" by simp
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   116
  qed
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   117
  show "f2 = g2" proof
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   118
    fix y :: 'b
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   119
    from a have "sum_case f1 f2 (Inr y) = sum_case g1 g2 (Inr y)" by simp
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   120
    then show "f2 y = g2 y" by simp
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   121
  qed
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   122
qed
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   123
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   124
lemma sum_case_weak_cong:
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   125
  "s = t \<Longrightarrow> sum_case f g s = sum_case f g t"
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   126
  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   127
  by simp
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   128
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   129
primrec Projl :: "'a + 'b \<Rightarrow> 'a" where
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   130
  Projl_Inl: "Projl (Inl x) = x"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   131
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   132
primrec Projr :: "'a + 'b \<Rightarrow> 'b" where
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   133
  Projr_Inr: "Projr (Inr x) = x"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   134
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   135
primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   136
  "Suml f (Inl x) = f x"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   137
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   138
primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   139
  "Sumr f (Inr x) = f x"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   140
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   141
lemma Suml_inject:
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   142
  assumes "Suml f = Suml g" shows "f = g"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   143
proof
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   144
  fix x :: 'a
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   145
  let ?s = "Inl x \<Colon> 'a + 'b"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   146
  from assms have "Suml f ?s = Suml g ?s" by simp
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   147
  then show "f x = g x" by simp
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   148
qed
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   149
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   150
lemma Sumr_inject:
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   151
  assumes "Sumr f = Sumr g" shows "f = g"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   152
proof
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   153
  fix x :: 'b
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   154
  let ?s = "Inr x \<Colon> 'a + 'b"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   155
  from assms have "Sumr f ?s = Sumr g ?s" by simp
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   156
  then show "f x = g x" by simp
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   157
qed
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   158
33995
ebf231de0c5c tuned whitespace
haftmann
parents: 33962
diff changeset
   159
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   160
subsection {* The Disjoint Sum of Sets *}
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   161
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   162
definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   163
  "A <+> B = Inl ` A \<union> Inr ` B"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   164
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   165
lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   166
by (simp add: Plus_def)
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   167
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   168
lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   169
by (simp add: Plus_def)
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   170
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   171
text {* Exhaustion rule for sums, a degenerate form of induction *}
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   172
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   173
lemma PlusE [elim!]: 
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   174
  "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"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   175
by (auto simp add: Plus_def)
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   176
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   177
lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   178
by auto
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   179
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   180
lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   181
proof (rule set_eqI)
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   182
  fix u :: "'a + 'b"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   183
  show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   184
qed
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   185
36176
3fe7e97ccca8 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents: 33995
diff changeset
   186
hide_const (open) Suml Sumr Projl Projr
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   187
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   188
end