src/HOL/Sum.ML
changeset 923 ff1574a81019
child 1188 0443e4dc8511
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Sum.ML	Fri Mar 03 12:02:25 1995 +0100
     1.3 @@ -0,0 +1,204 @@
     1.4 +(*  Title: 	HOL/Sum.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +
     1.9 +For Sum.thy.  The disjoint sum of two types
    1.10 +*)
    1.11 +
    1.12 +open Sum;
    1.13 +
    1.14 +(** Inl_Rep and Inr_Rep: Representations of the constructors **)
    1.15 +
    1.16 +(*This counts as a non-emptiness result for admitting 'a+'b as a type*)
    1.17 +goalw Sum.thy [Sum_def] "Inl_Rep(a) : Sum";
    1.18 +by (EVERY1 [rtac CollectI, rtac disjI1, rtac exI, rtac refl]);
    1.19 +qed "Inl_RepI";
    1.20 +
    1.21 +goalw Sum.thy [Sum_def] "Inr_Rep(b) : Sum";
    1.22 +by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]);
    1.23 +qed "Inr_RepI";
    1.24 +
    1.25 +goal Sum.thy "inj_onto Abs_Sum Sum";
    1.26 +by (rtac inj_onto_inverseI 1);
    1.27 +by (etac Abs_Sum_inverse 1);
    1.28 +qed "inj_onto_Abs_Sum";
    1.29 +
    1.30 +(** Distinctness of Inl and Inr **)
    1.31 +
    1.32 +goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)";
    1.33 +by (EVERY1 [rtac notI,
    1.34 +	    etac (fun_cong RS fun_cong RS fun_cong RS iffE), 
    1.35 +	    rtac (notE RS ccontr),  etac (mp RS conjunct2), 
    1.36 +	    REPEAT o (ares_tac [refl,conjI]) ]);
    1.37 +qed "Inl_Rep_not_Inr_Rep";
    1.38 +
    1.39 +goalw Sum.thy [Inl_def,Inr_def] "Inl(a) ~= Inr(b)";
    1.40 +by (rtac (inj_onto_Abs_Sum RS inj_onto_contraD) 1);
    1.41 +by (rtac Inl_Rep_not_Inr_Rep 1);
    1.42 +by (rtac Inl_RepI 1);
    1.43 +by (rtac Inr_RepI 1);
    1.44 +qed "Inl_not_Inr";
    1.45 +
    1.46 +bind_thm ("Inl_neq_Inr", (Inl_not_Inr RS notE));
    1.47 +val Inr_neq_Inl = sym RS Inl_neq_Inr;
    1.48 +
    1.49 +goal Sum.thy "(Inl(a)=Inr(b)) = False";
    1.50 +by (simp_tac (HOL_ss addsimps [Inl_not_Inr]) 1);
    1.51 +qed "Inl_Inr_eq";
    1.52 +
    1.53 +goal Sum.thy "(Inr(b)=Inl(a))  =  False";
    1.54 +by (simp_tac (HOL_ss addsimps [Inl_not_Inr RS not_sym]) 1);
    1.55 +qed "Inr_Inl_eq";
    1.56 +
    1.57 +
    1.58 +(** Injectiveness of Inl and Inr **)
    1.59 +
    1.60 +val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
    1.61 +by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
    1.62 +by (fast_tac HOL_cs 1);
    1.63 +qed "Inl_Rep_inject";
    1.64 +
    1.65 +val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
    1.66 +by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
    1.67 +by (fast_tac HOL_cs 1);
    1.68 +qed "Inr_Rep_inject";
    1.69 +
    1.70 +goalw Sum.thy [Inl_def] "inj(Inl)";
    1.71 +by (rtac injI 1);
    1.72 +by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inl_Rep_inject) 1);
    1.73 +by (rtac Inl_RepI 1);
    1.74 +by (rtac Inl_RepI 1);
    1.75 +qed "inj_Inl";
    1.76 +val Inl_inject = inj_Inl RS injD;
    1.77 +
    1.78 +goalw Sum.thy [Inr_def] "inj(Inr)";
    1.79 +by (rtac injI 1);
    1.80 +by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inr_Rep_inject) 1);
    1.81 +by (rtac Inr_RepI 1);
    1.82 +by (rtac Inr_RepI 1);
    1.83 +qed "inj_Inr";
    1.84 +val Inr_inject = inj_Inr RS injD;
    1.85 +
    1.86 +goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
    1.87 +by (fast_tac (HOL_cs addSEs [Inl_inject]) 1);
    1.88 +qed "Inl_eq";
    1.89 +
    1.90 +goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
    1.91 +by (fast_tac (HOL_cs addSEs [Inr_inject]) 1);
    1.92 +qed "Inr_eq";
    1.93 +
    1.94 +(*** Rules for the disjoint sum of two SETS ***)
    1.95 +
    1.96 +(** Introduction rules for the injections **)
    1.97 +
    1.98 +goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A plus B";
    1.99 +by (REPEAT (ares_tac [UnI1,imageI] 1));
   1.100 +qed "InlI";
   1.101 +
   1.102 +goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A plus B";
   1.103 +by (REPEAT (ares_tac [UnI2,imageI] 1));
   1.104 +qed "InrI";
   1.105 +
   1.106 +(** Elimination rules **)
   1.107 +
   1.108 +val major::prems = goalw Sum.thy [sum_def]
   1.109 +    "[| u: A plus B;  \
   1.110 +\       !!x. [| x:A;  u=Inl(x) |] ==> P; \
   1.111 +\       !!y. [| y:B;  u=Inr(y) |] ==> P \
   1.112 +\    |] ==> P";
   1.113 +by (rtac (major RS UnE) 1);
   1.114 +by (REPEAT (rtac refl 1
   1.115 +     ORELSE eresolve_tac (prems@[imageE,ssubst]) 1));
   1.116 +qed "plusE";
   1.117 +
   1.118 +
   1.119 +val sum_cs = set_cs addSIs [InlI, InrI] 
   1.120 +                    addSEs [plusE, Inl_neq_Inr, Inr_neq_Inl]
   1.121 +                    addSDs [Inl_inject, Inr_inject];
   1.122 +
   1.123 +
   1.124 +(** sum_case -- the selection operator for sums **)
   1.125 +
   1.126 +goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
   1.127 +by (fast_tac (sum_cs addIs [select_equality]) 1);
   1.128 +qed "sum_case_Inl";
   1.129 +
   1.130 +goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
   1.131 +by (fast_tac (sum_cs addIs [select_equality]) 1);
   1.132 +qed "sum_case_Inr";
   1.133 +
   1.134 +(** Exhaustion rule for sums -- a degenerate form of induction **)
   1.135 +
   1.136 +val prems = goalw Sum.thy [Inl_def,Inr_def]
   1.137 +    "[| !!x::'a. s = Inl(x) ==> P;  !!y::'b. s = Inr(y) ==> P \
   1.138 +\    |] ==> P";
   1.139 +by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
   1.140 +by (REPEAT (eresolve_tac [disjE,exE] 1
   1.141 +     ORELSE EVERY1 [resolve_tac prems, 
   1.142 +		    etac subst,
   1.143 +		    rtac (Rep_Sum_inverse RS sym)]));
   1.144 +qed "sumE";
   1.145 +
   1.146 +goal Sum.thy "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
   1.147 +by (EVERY1 [res_inst_tac [("s","s")] sumE, 
   1.148 +	    etac ssubst, rtac sum_case_Inl,
   1.149 +	    etac ssubst, rtac sum_case_Inr]);
   1.150 +qed "surjective_sum";
   1.151 +
   1.152 +goal Sum.thy "R(sum_case f g s) = \
   1.153 +\             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
   1.154 +by (rtac sumE 1);
   1.155 +by (etac ssubst 1);
   1.156 +by (stac sum_case_Inl 1);
   1.157 +by (fast_tac (set_cs addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
   1.158 +by (etac ssubst 1);
   1.159 +by (stac sum_case_Inr 1);
   1.160 +by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
   1.161 +qed "expand_sum_case";
   1.162 +
   1.163 +val sum_ss = prod_ss addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq, 
   1.164 +			       sum_case_Inl, sum_case_Inr];
   1.165 +
   1.166 +(*Prevents simplification of f and g: much faster*)
   1.167 +qed_goal "sum_case_weak_cong" Sum.thy
   1.168 +  "s=t ==> sum_case f g s = sum_case f g t"
   1.169 +  (fn [prem] => [rtac (prem RS arg_cong) 1]);
   1.170 +
   1.171 +
   1.172 +
   1.173 +
   1.174 +(** Rules for the Part primitive **)
   1.175 +
   1.176 +goalw Sum.thy [Part_def]
   1.177 +    "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part A h";
   1.178 +by (fast_tac set_cs 1);
   1.179 +qed "Part_eqI";
   1.180 +
   1.181 +val PartI = refl RSN (2,Part_eqI);
   1.182 +
   1.183 +val major::prems = goalw Sum.thy [Part_def]
   1.184 +    "[| a : Part A h;  !!z. [| a : A;  a=h(z) |] ==> P  \
   1.185 +\    |] ==> P";
   1.186 +by (rtac (major RS IntE) 1);
   1.187 +by (etac CollectE 1);
   1.188 +by (etac exE 1);
   1.189 +by (REPEAT (ares_tac prems 1));
   1.190 +qed "PartE";
   1.191 +
   1.192 +goalw Sum.thy [Part_def] "Part A h <= A";
   1.193 +by (rtac Int_lower1 1);
   1.194 +qed "Part_subset";
   1.195 +
   1.196 +goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
   1.197 +by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
   1.198 +qed "Part_mono";
   1.199 +
   1.200 +goalw Sum.thy [Part_def] "!!a. a : Part A h ==> a : A";
   1.201 +by (etac IntD1 1);
   1.202 +qed "PartD1";
   1.203 +
   1.204 +goal Sum.thy "Part A (%x.x) = A";
   1.205 +by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   1.206 +qed "Part_id";
   1.207 +