src/HOL/Sum_Type.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 12921 b7b0daf0d882
permissions -rw-r--r--
import -> imports
nipkow@10213
     1
(*  Title:      HOL/Sum_Type.ML
nipkow@10213
     2
    ID:         $Id$
nipkow@10213
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
nipkow@10213
     4
    Copyright   1991  University of Cambridge
nipkow@10213
     5
nipkow@10213
     6
The disjoint sum of two types
nipkow@10213
     7
*)
nipkow@10213
     8
nipkow@10213
     9
(** Inl_Rep and Inr_Rep: Representations of the constructors **)
nipkow@10213
    10
nipkow@10213
    11
(*This counts as a non-emptiness result for admitting 'a+'b as a type*)
nipkow@10213
    12
Goalw [Sum_def] "Inl_Rep(a) : Sum";
nipkow@10213
    13
by (EVERY1 [rtac CollectI, rtac disjI1, rtac exI, rtac refl]);
nipkow@10213
    14
qed "Inl_RepI";
nipkow@10213
    15
nipkow@10213
    16
Goalw [Sum_def] "Inr_Rep(b) : Sum";
nipkow@10213
    17
by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]);
nipkow@10213
    18
qed "Inr_RepI";
nipkow@10213
    19
nipkow@10213
    20
Goal "inj_on Abs_Sum Sum";
nipkow@10213
    21
by (rtac inj_on_inverseI 1);
nipkow@10213
    22
by (etac Abs_Sum_inverse 1);
nipkow@10213
    23
qed "inj_on_Abs_Sum";
nipkow@10213
    24
nipkow@10213
    25
(** Distinctness of Inl and Inr **)
nipkow@10213
    26
nipkow@10213
    27
Goalw [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)";
nipkow@10213
    28
by (EVERY1 [rtac notI,
nipkow@10213
    29
            etac (fun_cong RS fun_cong RS fun_cong RS iffE), 
nipkow@10213
    30
            rtac (notE RS ccontr),  etac (mp RS conjunct2), 
nipkow@10213
    31
            REPEAT o (ares_tac [refl,conjI]) ]);
nipkow@10213
    32
qed "Inl_Rep_not_Inr_Rep";
nipkow@10213
    33
nipkow@10213
    34
Goalw [Inl_def,Inr_def] "Inl(a) ~= Inr(b)";
nipkow@10213
    35
by (rtac (inj_on_Abs_Sum RS inj_on_contraD) 1);
nipkow@10213
    36
by (rtac Inl_Rep_not_Inr_Rep 1);
nipkow@10213
    37
by (rtac Inl_RepI 1);
nipkow@10213
    38
by (rtac Inr_RepI 1);
nipkow@10213
    39
qed "Inl_not_Inr";
nipkow@10213
    40
nipkow@10213
    41
bind_thm ("Inr_not_Inl", Inl_not_Inr RS not_sym);
nipkow@10213
    42
nipkow@10213
    43
AddIffs [Inl_not_Inr, Inr_not_Inl];
nipkow@10213
    44
nipkow@10213
    45
bind_thm ("Inl_neq_Inr", Inl_not_Inr RS notE);
nipkow@10213
    46
bind_thm ("Inr_neq_Inl", sym RS Inl_neq_Inr);
nipkow@10213
    47
nipkow@10213
    48
nipkow@10213
    49
(** Injectiveness of Inl and Inr **)
nipkow@10213
    50
nipkow@10213
    51
Goalw [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
nipkow@10213
    52
by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
nipkow@10213
    53
by (Blast_tac 1);
nipkow@10213
    54
qed "Inl_Rep_inject";
nipkow@10213
    55
nipkow@10213
    56
Goalw [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
nipkow@10213
    57
by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
nipkow@10213
    58
by (Blast_tac 1);
nipkow@10213
    59
qed "Inr_Rep_inject";
nipkow@10213
    60
nipkow@10213
    61
Goalw [Inl_def] "inj(Inl)";
nipkow@10213
    62
by (rtac injI 1);
nipkow@10213
    63
by (etac (inj_on_Abs_Sum RS inj_onD RS Inl_Rep_inject) 1);
nipkow@10213
    64
by (rtac Inl_RepI 1);
nipkow@10213
    65
by (rtac Inl_RepI 1);
nipkow@10213
    66
qed "inj_Inl";
nipkow@10213
    67
bind_thm ("Inl_inject", inj_Inl RS injD);
nipkow@10213
    68
nipkow@10213
    69
Goalw [Inr_def] "inj(Inr)";
nipkow@10213
    70
by (rtac injI 1);
nipkow@10213
    71
by (etac (inj_on_Abs_Sum RS inj_onD RS Inr_Rep_inject) 1);
nipkow@10213
    72
by (rtac Inr_RepI 1);
nipkow@10213
    73
by (rtac Inr_RepI 1);
nipkow@10213
    74
qed "inj_Inr";
nipkow@10213
    75
bind_thm ("Inr_inject", inj_Inr RS injD);
nipkow@10213
    76
nipkow@10213
    77
Goal "(Inl(x)=Inl(y)) = (x=y)";
nipkow@10213
    78
by (blast_tac (claset() addSDs [Inl_inject]) 1);
nipkow@10213
    79
qed "Inl_eq";
nipkow@10213
    80
nipkow@10213
    81
Goal "(Inr(x)=Inr(y)) = (x=y)";
nipkow@10213
    82
by (blast_tac (claset() addSDs [Inr_inject]) 1);
nipkow@10213
    83
qed "Inr_eq";
nipkow@10213
    84
nipkow@10213
    85
AddIffs [Inl_eq, Inr_eq];
nipkow@10213
    86
nipkow@10213
    87
(*** Rules for the disjoint sum of two SETS ***)
nipkow@10213
    88
nipkow@10213
    89
(** Introduction rules for the injections **)
nipkow@10213
    90
nipkow@10213
    91
Goalw [sum_def] "a : A ==> Inl(a) : A <+> B";
nipkow@10213
    92
by (Blast_tac 1);
nipkow@10213
    93
qed "InlI";
nipkow@10213
    94
nipkow@10213
    95
Goalw [sum_def] "b : B ==> Inr(b) : A <+> B";
nipkow@10213
    96
by (Blast_tac 1);
nipkow@10213
    97
qed "InrI";
nipkow@10213
    98
nipkow@10213
    99
(** Elimination rules **)
nipkow@10213
   100
nipkow@10213
   101
val major::prems = Goalw [sum_def]
nipkow@10213
   102
    "[| u: A <+> B;  \
nipkow@10213
   103
\       !!x. [| x:A;  u=Inl(x) |] ==> P; \
nipkow@10213
   104
\       !!y. [| y:B;  u=Inr(y) |] ==> P \
nipkow@10213
   105
\    |] ==> P";
nipkow@10213
   106
by (rtac (major RS UnE) 1);
nipkow@10213
   107
by (REPEAT (rtac refl 1
nipkow@10213
   108
     ORELSE eresolve_tac (prems@[imageE,ssubst]) 1));
nipkow@10213
   109
qed "PlusE";
nipkow@10213
   110
nipkow@10213
   111
nipkow@10213
   112
AddSIs [InlI, InrI]; 
nipkow@10213
   113
AddSEs [PlusE];
nipkow@10213
   114
nipkow@10213
   115
nipkow@10213
   116
(** Exhaustion rule for sums -- a degenerate form of induction **)
nipkow@10213
   117
nipkow@10213
   118
val prems = Goalw [Inl_def,Inr_def]
nipkow@10213
   119
    "[| !!x::'a. s = Inl(x) ==> P;  !!y::'b. s = Inr(y) ==> P \
nipkow@10213
   120
\    |] ==> P";
nipkow@10213
   121
by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
nipkow@10213
   122
by (REPEAT (eresolve_tac [disjE,exE] 1
nipkow@10213
   123
     ORELSE EVERY1 [resolve_tac prems, 
nipkow@10213
   124
                    etac subst,
nipkow@10213
   125
                    rtac (Rep_Sum_inverse RS sym)]));
nipkow@10213
   126
qed "sumE";
nipkow@10213
   127
nipkow@10213
   128
val prems = Goal "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
nipkow@10213
   129
by (res_inst_tac [("s","x")] sumE 1);
nipkow@10213
   130
by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
nipkow@10213
   131
qed "sum_induct";
nipkow@10213
   132
nipkow@10213
   133
nipkow@10213
   134
(** Rules for the Part primitive **)
nipkow@10213
   135
nipkow@10213
   136
Goalw [Part_def] "[| a : A;  a=h(b) |] ==> a : Part A h";
nipkow@10213
   137
by (Blast_tac 1);
nipkow@10213
   138
qed "Part_eqI";
nipkow@10213
   139
nipkow@10213
   140
bind_thm ("PartI", refl RSN (2,Part_eqI));
nipkow@10213
   141
nipkow@10213
   142
val major::prems = Goalw [Part_def]
nipkow@10213
   143
    "[| a : Part A h;  !!z. [| a : A;  a=h(z) |] ==> P  \
nipkow@10213
   144
\    |] ==> P";
nipkow@10213
   145
by (rtac (major RS IntE) 1);
nipkow@10213
   146
by (etac CollectE 1);
nipkow@10213
   147
by (etac exE 1);
nipkow@10213
   148
by (REPEAT (ares_tac prems 1));
nipkow@10213
   149
qed "PartE";
nipkow@10213
   150
nipkow@10213
   151
AddIs  [Part_eqI];
nipkow@10213
   152
AddSEs [PartE];
nipkow@10213
   153
nipkow@10213
   154
Goalw [Part_def] "Part A h <= A";
nipkow@10213
   155
by (rtac Int_lower1 1);
nipkow@10213
   156
qed "Part_subset";
nipkow@10213
   157
nipkow@10213
   158
Goal "A<=B ==> Part A h <= Part B h";
nipkow@10213
   159
by (Blast_tac 1);
nipkow@10213
   160
qed "Part_mono";
nipkow@10213
   161
wenzelm@12921
   162
bind_thms ("basic_monos", basic_monos @ [Part_mono]);
nipkow@10213
   163
nipkow@10213
   164
Goalw [Part_def] "a : Part A h ==> a : A";
nipkow@10213
   165
by (etac IntD1 1);
nipkow@10213
   166
qed "PartD1";
nipkow@10213
   167
nipkow@10213
   168
Goal "Part A (%x. x) = A";
nipkow@10213
   169
by (Blast_tac 1);
nipkow@10213
   170
qed "Part_id";
nipkow@10213
   171
nipkow@10213
   172
Goal "Part (A Int B) h = (Part A h) Int (Part B h)";
nipkow@10213
   173
by (Blast_tac 1);
nipkow@10213
   174
qed "Part_Int";
nipkow@10213
   175
nipkow@10213
   176
Goal "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}";
nipkow@10213
   177
by (Blast_tac 1);
nipkow@10213
   178
qed "Part_Collect";