src/HOL/Sum.ML
author paulson
Mon Jul 19 15:24:35 1999 +0200 (1999-07-19)
changeset 7031 972b5f62f476
parent 7014 11ee650edcd2
child 7087 67c6706578ed
permissions -rw-r--r--
getting rid of qed_goal
     1 (*  Title:      HOL/Sum.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 
    47 val Inr_neq_Inl = sym RS Inl_neq_Inr;
    48 
    49 
    50 (** Injectiveness of Inl and Inr **)
    51 
    52 Goalw [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
    53 by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
    54 by (Blast_tac 1);
    55 qed "Inl_Rep_inject";
    56 
    57 Goalw [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
    58 by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
    59 by (Blast_tac 1);
    60 qed "Inr_Rep_inject";
    61 
    62 Goalw [Inl_def] "inj(Inl)";
    63 by (rtac injI 1);
    64 by (etac (inj_on_Abs_Sum RS inj_onD RS Inl_Rep_inject) 1);
    65 by (rtac Inl_RepI 1);
    66 by (rtac Inl_RepI 1);
    67 qed "inj_Inl";
    68 val Inl_inject = inj_Inl RS injD;
    69 
    70 Goalw [Inr_def] "inj(Inr)";
    71 by (rtac injI 1);
    72 by (etac (inj_on_Abs_Sum RS inj_onD RS Inr_Rep_inject) 1);
    73 by (rtac Inr_RepI 1);
    74 by (rtac Inr_RepI 1);
    75 qed "inj_Inr";
    76 val Inr_inject = inj_Inr RS injD;
    77 
    78 Goal "(Inl(x)=Inl(y)) = (x=y)";
    79 by (blast_tac (claset() addSDs [Inl_inject]) 1);
    80 qed "Inl_eq";
    81 
    82 Goal "(Inr(x)=Inr(y)) = (x=y)";
    83 by (blast_tac (claset() addSDs [Inr_inject]) 1);
    84 qed "Inr_eq";
    85 
    86 AddIffs [Inl_eq, Inr_eq];
    87 
    88 (*** Rules for the disjoint sum of two SETS ***)
    89 
    90 (** Introduction rules for the injections **)
    91 
    92 Goalw [sum_def] "a : A ==> Inl(a) : A Plus B";
    93 by (Blast_tac 1);
    94 qed "InlI";
    95 
    96 Goalw [sum_def] "b : B ==> Inr(b) : A Plus B";
    97 by (Blast_tac 1);
    98 qed "InrI";
    99 
   100 (** Elimination rules **)
   101 
   102 val major::prems = Goalw [sum_def]
   103     "[| u: A Plus B;  \
   104 \       !!x. [| x:A;  u=Inl(x) |] ==> P; \
   105 \       !!y. [| y:B;  u=Inr(y) |] ==> P \
   106 \    |] ==> P";
   107 by (rtac (major RS UnE) 1);
   108 by (REPEAT (rtac refl 1
   109      ORELSE eresolve_tac (prems@[imageE,ssubst]) 1));
   110 qed "PlusE";
   111 
   112 
   113 AddSIs [InlI, InrI]; 
   114 AddSEs [PlusE];
   115 
   116 
   117 (** sum_case -- the selection operator for sums **)
   118 
   119 Goalw [sum_case_def] "sum_case f g (Inl x) = f(x)";
   120 by (Blast_tac 1);
   121 qed "sum_case_Inl";
   122 
   123 Goalw [sum_case_def] "sum_case f g (Inr x) = g(x)";
   124 by (Blast_tac 1);
   125 qed "sum_case_Inr";
   126 
   127 Addsimps [sum_case_Inl, sum_case_Inr];
   128 
   129 (** Exhaustion rule for sums -- a degenerate form of induction **)
   130 
   131 val prems = Goalw [Inl_def,Inr_def]
   132     "[| !!x::'a. s = Inl(x) ==> P;  !!y::'b. s = Inr(y) ==> P \
   133 \    |] ==> P";
   134 by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
   135 by (REPEAT (eresolve_tac [disjE,exE] 1
   136      ORELSE EVERY1 [resolve_tac prems, 
   137                     etac subst,
   138                     rtac (Rep_Sum_inverse RS sym)]));
   139 qed "sumE";
   140 
   141 val prems = Goal "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
   142 by (res_inst_tac [("s","x")] sumE 1);
   143 by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
   144 qed "sum_induct";
   145 
   146 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
   147 by (EVERY1 [res_inst_tac [("s","s")] sumE, 
   148             etac ssubst, rtac sum_case_Inl,
   149             etac ssubst, rtac sum_case_Inr]);
   150 qed "surjective_sum";
   151 
   152 Goal "R(sum_case f g s) = \
   153 \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
   154 by (res_inst_tac [("s","s")] sumE 1);
   155 by Auto_tac;
   156 qed "split_sum_case";
   157 
   158 Goal "P (sum_case f g s) = \
   159 \     (~ ((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))";
   160 by (stac split_sum_case 1);
   161 by (Blast_tac 1);
   162 qed "split_sum_case_asm";
   163 
   164 (*Prevents simplification of f and g: much faster*)
   165 Goal "s=t ==> sum_case f g s = sum_case f g t";
   166 by (etac arg_cong 1);
   167 qed "sum_case_weak_cong";
   168 
   169 val [p1,p2] = Goal "[| sum_case f1 f2 = sum_case g1 g2;  \
   170   \  [| f1 = g1; f2 = g2 |] ==> P |] ==> P";
   171 by (cut_facts_tac [p1] 1);
   172 br p2 1;
   173 br ext 1;
   174 by (dres_inst_tac [("x","Inl x")] fun_cong 1);
   175 by (Asm_full_simp_tac 1);
   176 br ext 1;
   177 by (dres_inst_tac [("x","Inr x")] fun_cong 1);
   178 by (Asm_full_simp_tac 1);
   179 qed "sum_case_inject";
   180 
   181 
   182 (** Rules for the Part primitive **)
   183 
   184 Goalw [Part_def] "[| a : A;  a=h(b) |] ==> a : Part A h";
   185 by (Blast_tac 1);
   186 qed "Part_eqI";
   187 
   188 val PartI = refl RSN (2,Part_eqI);
   189 
   190 val major::prems = Goalw [Part_def]
   191     "[| a : Part A h;  !!z. [| a : A;  a=h(z) |] ==> P  \
   192 \    |] ==> P";
   193 by (rtac (major RS IntE) 1);
   194 by (etac CollectE 1);
   195 by (etac exE 1);
   196 by (REPEAT (ares_tac prems 1));
   197 qed "PartE";
   198 
   199 AddIs  [Part_eqI];
   200 AddSEs [PartE];
   201 
   202 Goalw [Part_def] "Part A h <= A";
   203 by (rtac Int_lower1 1);
   204 qed "Part_subset";
   205 
   206 Goal "A<=B ==> Part A h <= Part B h";
   207 by (Blast_tac 1);
   208 qed "Part_mono";
   209 
   210 val basic_monos = basic_monos @ [Part_mono];
   211 
   212 Goalw [Part_def] "a : Part A h ==> a : A";
   213 by (etac IntD1 1);
   214 qed "PartD1";
   215 
   216 Goal "Part A (%x. x) = A";
   217 by (Blast_tac 1);
   218 qed "Part_id";
   219 
   220 Goal "Part (A Int B) h = (Part A h) Int (Part B h)";
   221 by (Blast_tac 1);
   222 qed "Part_Int";
   223 
   224 (*For inductive definitions*)
   225 Goal "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}";
   226 by (Blast_tac 1);
   227 qed "Part_Collect";