src/HOL/Sum_Type.thy
author wenzelm
Mon, 12 Apr 2021 14:14:47 +0200
changeset 73563 55b66a45bc94
parent 67443 3abf6a722518
child 80932 261cd8722677
permissions -rw-r--r--
tuned;
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
63575
b9bd9e61fd63 misc tuning and modernization;
wenzelm
parents: 63400
diff changeset
     6
section \<open>The Disjoint Sum of Two Types\<close>
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
63575
b9bd9e61fd63 misc tuning and modernization;
wenzelm
parents: 63400
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
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    12
subsection \<open>Construction of the sum type and its basic abstract operations\<close>
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    13
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    14
definition Inl_Rep :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    15
  where "Inl_Rep a x y p \<longleftrightarrow> x = a \<and> p"
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    16
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    17
definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    18
  where "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
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45204
diff changeset
    20
definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45204
diff changeset
    21
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    22
typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool) set"
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45204
diff changeset
    23
  unfolding sum_def by auto
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    24
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    25
lemma Inl_RepI: "Inl_Rep a \<in> sum"
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    26
  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
    27
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    28
lemma Inr_RepI: "Inr_Rep b \<in> sum"
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    29
  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
    30
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    31
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
    32
  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
    33
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    34
lemma Inl_Rep_inject: "inj_on Inl_Rep A"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    35
proof (rule inj_onI)
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    36
  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
    37
    by (auto simp add: Inl_Rep_def fun_eq_iff)
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    38
qed
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    39
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    40
lemma Inr_Rep_inject: "inj_on Inr_Rep A"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    41
proof (rule inj_onI)
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    42
  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
    43
    by (auto simp add: Inr_Rep_def fun_eq_iff)
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    44
qed
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    45
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    46
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
    47
  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
    48
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    49
definition Inl :: "'a \<Rightarrow> 'a + 'b"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    50
  where "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
    51
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    52
definition Inr :: "'b \<Rightarrow> 'a + 'b"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    53
  where "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
    54
29025
8c8859c0d734 move lemmas from Numeral_Type.thy to other theories
huffman
parents: 28524
diff changeset
    55
lemma inj_Inl [simp]: "inj_on Inl A"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    56
  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
    57
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    58
lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    59
  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
    60
29025
8c8859c0d734 move lemmas from Numeral_Type.thy to other theories
huffman
parents: 28524
diff changeset
    61
lemma inj_Inr [simp]: "inj_on Inr A"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    62
  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
    63
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    64
lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    65
  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
    66
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    67
lemma Inl_not_Inr: "Inl a \<noteq> Inr b"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    68
proof -
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    69
  have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    70
    using Inl_RepI [of a] Inr_RepI [of b] by auto
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    71
  with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    72
  with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    73
    by auto
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    74
  then show ?thesis
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    75
    by (simp add: Inl_def Inr_def)
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    76
qed
15391
797ed46d724b converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
paulson
parents: 11609
diff changeset
    77
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    78
lemma Inr_not_Inl: "Inr b \<noteq> Inl a"
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    79
  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
    80
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    81
lemma sumE:
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    82
  assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    83
    and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    84
  shows P
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    85
proof (rule Abs_sum_cases [of s])
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    86
  fix f
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 36176
diff changeset
    87
  assume "s = Abs_sum f" and "f \<in> sum"
63575
b9bd9e61fd63 misc tuning and modernization;
wenzelm
parents: 63400
diff changeset
    88
  with assms show P
b9bd9e61fd63 misc tuning and modernization;
wenzelm
parents: 63400
diff changeset
    89
    by (auto simp add: sum_def Inl_def Inr_def)
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
    90
qed
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
    91
55469
b19dd108f0c2 aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents: 55468
diff changeset
    92
free_constructors case_sum for
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    93
  isl: Inl projl
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
    94
| Inr projr
58189
9d714be4f028 added 'plugins' option to control which hooks are enabled
blanchet
parents: 55931
diff changeset
    95
  by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
55393
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
    96
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61076
diff changeset
    97
text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
55442
blanchet
parents: 55414
diff changeset
    98
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    99
setup \<open>Sign.mandatory_path "old"\<close>
55393
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
   100
58306
117ba6cbe414 renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
blanchet
parents: 58189
diff changeset
   101
old_rep_datatype Inl Inr
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   102
proof -
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   103
  fix P
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   104
  fix s :: "'a + 'b"
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
   105
  assume x: "\<And>x::'a. P (Inl x)" and y: "\<And>y::'b. P (Inr y)"
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   106
  then show "P s" by (auto intro: sumE [of s])
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   107
qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   108
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   109
setup \<open>Sign.parent_path\<close>
55393
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
   110
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61076
diff changeset
   111
text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
55442
blanchet
parents: 55414
diff changeset
   112
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   113
setup \<open>Sign.mandatory_path "sum"\<close>
55393
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
   114
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
   115
declare
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
   116
  old.sum.inject[iff del]
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
   117
  old.sum.distinct(1)[simp del, induct_simp del]
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
   118
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
   119
lemmas induct = old.sum.induct
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
   120
lemmas inducts = old.sum.inducts
55642
63beb38e9258 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents: 55575
diff changeset
   121
lemmas rec = old.sum.rec
63beb38e9258 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents: 55575
diff changeset
   122
lemmas simps = sum.inject sum.distinct sum.case sum.rec
55393
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
   123
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   124
setup \<open>Sign.parent_path\<close>
55393
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
   125
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   126
primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
63575
b9bd9e61fd63 misc tuning and modernization;
wenzelm
parents: 63400
diff changeset
   127
  where
b9bd9e61fd63 misc tuning and modernization;
wenzelm
parents: 63400
diff changeset
   128
    "map_sum f1 f2 (Inl a) = Inl (f1 a)"
b9bd9e61fd63 misc tuning and modernization;
wenzelm
parents: 63400
diff changeset
   129
  | "map_sum f1 f2 (Inr a) = Inr (f2 a)"
40610
70776ecfe324 mapper for sum type
haftmann
parents: 40271
diff changeset
   130
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   131
functor map_sum: map_sum
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   132
proof -
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   133
  show "map_sum f g \<circ> map_sum h i = map_sum (f \<circ> h) (g \<circ> i)" for f g h i
41372
551eb49a6e91 tuned type_lifting declarations
haftmann
parents: 40968
diff changeset
   134
  proof
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   135
    show "(map_sum f g \<circ> map_sum h i) s = map_sum (f \<circ> h) (g \<circ> i) s" for s
41372
551eb49a6e91 tuned type_lifting declarations
haftmann
parents: 40968
diff changeset
   136
      by (cases s) simp_all
551eb49a6e91 tuned type_lifting declarations
haftmann
parents: 40968
diff changeset
   137
  qed
55931
62156e694f3d renamed 'map_sum' to 'sum_map'
blanchet
parents: 55642
diff changeset
   138
  show "map_sum id id = id"
41372
551eb49a6e91 tuned type_lifting declarations
haftmann
parents: 40968
diff changeset
   139
  proof
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   140
    show "map_sum id id s = id s" for s
41372
551eb49a6e91 tuned type_lifting declarations
haftmann
parents: 40968
diff changeset
   141
      by (cases s) simp_all
551eb49a6e91 tuned type_lifting declarations
haftmann
parents: 40968
diff changeset
   142
  qed
40610
70776ecfe324 mapper for sum type
haftmann
parents: 40271
diff changeset
   143
qed
70776ecfe324 mapper for sum type
haftmann
parents: 40271
diff changeset
   144
53010
ec5e6f69bd65 move useful lemmas to Main
kuncar
parents: 49948
diff changeset
   145
lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
ec5e6f69bd65 move useful lemmas to Main
kuncar
parents: 49948
diff changeset
   146
  by (auto intro: sum.induct)
ec5e6f69bd65 move useful lemmas to Main
kuncar
parents: 49948
diff changeset
   147
ec5e6f69bd65 move useful lemmas to Main
kuncar
parents: 49948
diff changeset
   148
lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   149
  using split_sum_all[of "\<lambda>x. \<not>P x"] by blast
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   150
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   151
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   152
subsection \<open>Projections\<close>
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   153
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55403
diff changeset
   154
lemma case_sum_KK [simp]: "case_sum (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)"
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   155
  by (rule ext) (simp split: sum.split)
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   156
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55403
diff changeset
   157
lemma surjective_sum: "case_sum (\<lambda>x::'a. f (Inl x)) (\<lambda>y::'b. f (Inr y)) = f"
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   158
proof
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   159
  fix s :: "'a + 'b"
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
   160
  show "(case s of Inl (x::'a) \<Rightarrow> f (Inl x) | Inr (y::'b) \<Rightarrow> f (Inr y)) = f s"
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   161
    by (cases s) simp_all
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   162
qed
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   163
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55403
diff changeset
   164
lemma case_sum_inject:
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55403
diff changeset
   165
  assumes a: "case_sum f1 f2 = case_sum g1 g2"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   166
    and r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   167
  shows P
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   168
proof (rule r)
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   169
  show "f1 = g1"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   170
  proof
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   171
    fix x :: 'a
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55403
diff changeset
   172
    from a have "case_sum f1 f2 (Inl x) = case_sum g1 g2 (Inl x)" by simp
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   173
    then show "f1 x = g1 x" by simp
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   174
  qed
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   175
  show "f2 = g2"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   176
  proof
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   177
    fix y :: 'b
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55403
diff changeset
   178
    from a have "case_sum f1 f2 (Inr y) = case_sum g1 g2 (Inr y)" by simp
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   179
    then show "f2 y = g2 y" by simp
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   180
  qed
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   181
qed
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   182
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   183
primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   184
  where "Suml f (Inl x) = f x"
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   185
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   186
primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   187
  where "Sumr f (Inr x) = f x"
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   188
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   189
lemma Suml_inject:
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   190
  assumes "Suml f = Suml g"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   191
  shows "f = g"
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   192
proof
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   193
  fix x :: 'a
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
   194
  let ?s = "Inl x :: 'a + 'b"
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   195
  from assms have "Suml f ?s = Suml g ?s" by simp
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   196
  then show "f x = g x" by simp
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   197
qed
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   198
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   199
lemma Sumr_inject:
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   200
  assumes "Sumr f = Sumr g"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   201
  shows "f = g"
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   202
proof
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   203
  fix x :: 'b
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
   204
  let ?s = "Inr x :: 'a + 'b"
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   205
  from assms have "Sumr f ?s = Sumr g ?s" by simp
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   206
  then show "f x = g x" by simp
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   207
qed
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   208
33995
ebf231de0c5c tuned whitespace
haftmann
parents: 33962
diff changeset
   209
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   210
subsection \<open>The Disjoint Sum of Sets\<close>
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   211
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   212
definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set"  (infixr "<+>" 65)
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   213
  where "A <+> B = Inl ` A \<union> Inr ` B"
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   214
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 63575
diff changeset
   215
hide_const (open) Plus \<comment> \<open>Valuable identifier\<close>
40271
6014e8252e57 hide Sum_Type.Plus
nipkow
parents: 39302
diff changeset
   216
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   217
lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   218
  by (simp add: Plus_def)
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   219
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   220
lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   221
  by (simp add: Plus_def)
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   222
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   223
text \<open>Exhaustion rule for sums, a degenerate form of induction\<close>
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   224
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   225
lemma PlusE [elim!]:
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   226
  "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"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   227
  by (auto simp add: Plus_def)
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   228
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   229
lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   230
  by auto
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   231
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   232
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
   233
proof (rule set_eqI)
33962
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   234
  fix u :: "'a + 'b"
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   235
  show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
abf9fa17452a modernized; dropped ancient constant Part
haftmann
parents: 33961
diff changeset
   236
qed
33961
03f2ab6a4ea6 centralized sum type matter in Sum_Type.thy
haftmann
parents: 31080
diff changeset
   237
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   238
lemma UNIV_sum: "UNIV = Inl ` UNIV \<union> Inr ` UNIV"
49948
744934b818c7 moved quite generic material from theory Enum to more appropriate places
haftmann
parents: 49834
diff changeset
   239
proof -
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   240
  have "x \<in> range Inl" if "x \<notin> range Inr" for x :: "'a + 'b"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   241
    using that by (cases x) simp_all
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61799
diff changeset
   242
  then show ?thesis by auto
49948
744934b818c7 moved quite generic material from theory Enum to more appropriate places
haftmann
parents: 49834
diff changeset
   243
qed
744934b818c7 moved quite generic material from theory Enum to more appropriate places
haftmann
parents: 49834
diff changeset
   244
55393
ce5cebfaedda se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
blanchet
parents: 53010
diff changeset
   245
hide_const (open) Suml Sumr sum
45204
5e4a1270c000 hide typedef-generated constants Product_Type.prod and Sum_Type.sum
huffman
parents: 41505
diff changeset
   246
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   247
end