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