1.1 --- a/src/HOL/Datatype_Universe.ML Wed Dec 08 15:15:49 2004 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,561 +0,0 @@
1.4 -(* Title: HOL/Datatype_Universe.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 -
1.10 -(** apfst -- can be used in similar type definitions **)
1.11 -
1.12 -Goalw [apfst_def] "apfst f (a,b) = (f(a),b)";
1.13 -by (rtac split_conv 1);
1.14 -qed "apfst_conv";
1.15 -
1.16 -val [major,minor] = Goal
1.17 - "[| q = apfst f p; !!x y. [| p = (x,y); q = (f(x),y) |] ==> R \
1.18 -\ |] ==> R";
1.19 -by (rtac PairE 1);
1.20 -by (rtac minor 1);
1.21 -by (assume_tac 1);
1.22 -by (rtac (major RS trans) 1);
1.23 -by (etac ssubst 1);
1.24 -by (rtac apfst_conv 1);
1.25 -qed "apfst_convE";
1.26 -
1.27 -(** Push -- an injection, analogous to Cons on lists **)
1.28 -
1.29 -Goalw [Push_def] "Push i f = Push j g ==> i=j";
1.30 -by (etac (fun_cong RS box_equals) 1);
1.31 -by (rtac nat_case_0 1);
1.32 -by (rtac nat_case_0 1);
1.33 -qed "Push_inject1";
1.34 -
1.35 -Goalw [Push_def] "Push i f = Push j g ==> f=g";
1.36 -by (rtac (ext RS box_equals) 1);
1.37 -by (etac fun_cong 1);
1.38 -by (rtac (nat_case_Suc RS ext) 1);
1.39 -by (rtac (nat_case_Suc RS ext) 1);
1.40 -qed "Push_inject2";
1.41 -
1.42 -val [major,minor] = Goal
1.43 - "[| Push i f =Push j g; [| i=j; f=g |] ==> P \
1.44 -\ |] ==> P";
1.45 -by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1);
1.46 -qed "Push_inject";
1.47 -
1.48 -Goalw [Push_def] "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P";
1.49 -by (rtac Suc_neq_Zero 1);
1.50 -by (etac (fun_cong RS box_equals RS Inr_inject) 1);
1.51 -by (rtac nat_case_0 1);
1.52 -by (rtac refl 1);
1.53 -qed "Push_neq_K0";
1.54 -
1.55 -(*** Isomorphisms ***)
1.56 -
1.57 -Goal "inj(Rep_Node)";
1.58 -by (rtac inj_inverseI 1); (*cannot combine by RS: multiple unifiers*)
1.59 -by (rtac Rep_Node_inverse 1);
1.60 -qed "inj_Rep_Node";
1.61 -
1.62 -Goal "inj_on Abs_Node Node";
1.63 -by (rtac inj_on_inverseI 1);
1.64 -by (etac Abs_Node_inverse 1);
1.65 -qed "inj_on_Abs_Node";
1.66 -
1.67 -bind_thm ("Abs_Node_inj", inj_on_Abs_Node RS inj_onD);
1.68 -
1.69 -
1.70 -(*** Introduction rules for Node ***)
1.71 -
1.72 -Goalw [Node_def] "(%k. Inr 0, a) : Node";
1.73 -by (Blast_tac 1);
1.74 -qed "Node_K0_I";
1.75 -
1.76 -Goalw [Node_def,Push_def]
1.77 - "p: Node ==> apfst (Push i) p : Node";
1.78 -by (fast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
1.79 -qed "Node_Push_I";
1.80 -
1.81 -
1.82 -(*** Distinctness of constructors ***)
1.83 -
1.84 -(** Scons vs Atom **)
1.85 -
1.86 -Goalw [Atom_def,Scons_def,Push_Node_def,One_nat_def]
1.87 - "Scons M N ~= Atom(a)";
1.88 -by (rtac notI 1);
1.89 -by (etac (equalityD2 RS subsetD RS UnE) 1);
1.90 -by (rtac singletonI 1);
1.91 -by (REPEAT (eresolve_tac [imageE, Abs_Node_inj RS apfst_convE,
1.92 - Pair_inject, sym RS Push_neq_K0] 1
1.93 - ORELSE resolve_tac [Node_K0_I, Rep_Node RS Node_Push_I] 1));
1.94 -qed "Scons_not_Atom";
1.95 -bind_thm ("Atom_not_Scons", Scons_not_Atom RS not_sym);
1.96 -
1.97 -
1.98 -(*** Injectiveness ***)
1.99 -
1.100 -(** Atomic nodes **)
1.101 -
1.102 -Goalw [Atom_def] "inj(Atom)";
1.103 -by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inj]) 1);
1.104 -qed "inj_Atom";
1.105 -bind_thm ("Atom_inject", inj_Atom RS injD);
1.106 -
1.107 -Goal "(Atom(a)=Atom(b)) = (a=b)";
1.108 -by (blast_tac (claset() addSDs [Atom_inject]) 1);
1.109 -qed "Atom_Atom_eq";
1.110 -AddIffs [Atom_Atom_eq];
1.111 -
1.112 -Goalw [Leaf_def,o_def] "inj(Leaf)";
1.113 -by (rtac injI 1);
1.114 -by (etac (Atom_inject RS Inl_inject) 1);
1.115 -qed "inj_Leaf";
1.116 -
1.117 -bind_thm ("Leaf_inject", inj_Leaf RS injD);
1.118 -AddSDs [Leaf_inject];
1.119 -
1.120 -Goalw [Numb_def,o_def] "inj(Numb)";
1.121 -by (rtac injI 1);
1.122 -by (etac (Atom_inject RS Inr_inject) 1);
1.123 -qed "inj_Numb";
1.124 -
1.125 -bind_thm ("Numb_inject", inj_Numb RS injD);
1.126 -AddSDs [Numb_inject];
1.127 -
1.128 -(** Injectiveness of Push_Node **)
1.129 -
1.130 -val [major,minor] = Goalw [Push_Node_def]
1.131 - "[| Push_Node i m =Push_Node j n; [| i=j; m=n |] ==> P \
1.132 -\ |] ==> P";
1.133 -by (rtac (major RS Abs_Node_inj RS apfst_convE) 1);
1.134 -by (REPEAT (resolve_tac [Rep_Node RS Node_Push_I] 1));
1.135 -by (etac (sym RS apfst_convE) 1);
1.136 -by (rtac minor 1);
1.137 -by (etac Pair_inject 1);
1.138 -by (etac (Push_inject1 RS sym) 1);
1.139 -by (rtac (inj_Rep_Node RS injD) 1);
1.140 -by (etac trans 1);
1.141 -by (safe_tac (claset() addSEs [Push_inject,sym]));
1.142 -qed "Push_Node_inject";
1.143 -
1.144 -
1.145 -(** Injectiveness of Scons **)
1.146 -
1.147 -Goalw [Scons_def,One_nat_def] "Scons M N <= Scons M' N' ==> M<=M'";
1.148 -by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
1.149 -qed "Scons_inject_lemma1";
1.150 -
1.151 -Goalw [Scons_def,One_nat_def] "Scons M N <= Scons M' N' ==> N<=N'";
1.152 -by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
1.153 -qed "Scons_inject_lemma2";
1.154 -
1.155 -Goal "Scons M N = Scons M' N' ==> M=M'";
1.156 -by (etac equalityE 1);
1.157 -by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
1.158 -qed "Scons_inject1";
1.159 -
1.160 -Goal "Scons M N = Scons M' N' ==> N=N'";
1.161 -by (etac equalityE 1);
1.162 -by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
1.163 -qed "Scons_inject2";
1.164 -
1.165 -val [major,minor] = Goal
1.166 - "[| Scons M N = Scons M' N'; [| M=M'; N=N' |] ==> P \
1.167 -\ |] ==> P";
1.168 -by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
1.169 -qed "Scons_inject";
1.170 -
1.171 -Goal "(Scons M N = Scons M' N') = (M=M' & N=N')";
1.172 -by (blast_tac (claset() addSEs [Scons_inject]) 1);
1.173 -qed "Scons_Scons_eq";
1.174 -
1.175 -(*** Distinctness involving Leaf and Numb ***)
1.176 -
1.177 -(** Scons vs Leaf **)
1.178 -
1.179 -Goalw [Leaf_def,o_def] "Scons M N ~= Leaf(a)";
1.180 -by (rtac Scons_not_Atom 1);
1.181 -qed "Scons_not_Leaf";
1.182 -bind_thm ("Leaf_not_Scons", Scons_not_Leaf RS not_sym);
1.183 -
1.184 -AddIffs [Scons_not_Leaf, Leaf_not_Scons];
1.185 -
1.186 -
1.187 -(** Scons vs Numb **)
1.188 -
1.189 -Goalw [Numb_def,o_def] "Scons M N ~= Numb(k)";
1.190 -by (rtac Scons_not_Atom 1);
1.191 -qed "Scons_not_Numb";
1.192 -bind_thm ("Numb_not_Scons", Scons_not_Numb RS not_sym);
1.193 -
1.194 -AddIffs [Scons_not_Numb, Numb_not_Scons];
1.195 -
1.196 -
1.197 -(** Leaf vs Numb **)
1.198 -
1.199 -Goalw [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)";
1.200 -by (simp_tac (simpset() addsimps [Inl_not_Inr]) 1);
1.201 -qed "Leaf_not_Numb";
1.202 -bind_thm ("Numb_not_Leaf", Leaf_not_Numb RS not_sym);
1.203 -
1.204 -AddIffs [Leaf_not_Numb, Numb_not_Leaf];
1.205 -
1.206 -
1.207 -(*** ndepth -- the depth of a node ***)
1.208 -
1.209 -Addsimps [apfst_conv];
1.210 -AddIffs [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq];
1.211 -
1.212 -
1.213 -Goalw [ndepth_def] "ndepth (Abs_Node(%k. Inr 0, x)) = 0";
1.214 -by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split_conv]);
1.215 -by (rtac Least_equality 1);
1.216 -by Auto_tac;
1.217 -qed "ndepth_K0";
1.218 -
1.219 -Goal "nat_case (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k";
1.220 -by (induct_tac "k" 1);
1.221 -by (ALLGOALS Simp_tac);
1.222 -by (rtac impI 1);
1.223 -by (etac Least_le 1);
1.224 -val lemma = result();
1.225 -
1.226 -Goalw [ndepth_def,Push_Node_def]
1.227 - "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))";
1.228 -by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1);
1.229 -by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1);
1.230 -by Safe_tac;
1.231 -by (etac ssubst 1); (*instantiates type variables!*)
1.232 -by (Simp_tac 1);
1.233 -by (rtac Least_equality 1);
1.234 -by (rewtac Push_def);
1.235 -by (auto_tac (claset(), simpset() addsimps [lemma]));
1.236 -by (etac LeastI 1);
1.237 -qed "ndepth_Push_Node";
1.238 -
1.239 -
1.240 -(*** ntrunc applied to the various node sets ***)
1.241 -
1.242 -Goalw [ntrunc_def] "ntrunc 0 M = {}";
1.243 -by (Blast_tac 1);
1.244 -qed "ntrunc_0";
1.245 -
1.246 -Goalw [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)";
1.247 -by (fast_tac (claset() addss (simpset() addsimps [ndepth_K0])) 1);
1.248 -qed "ntrunc_Atom";
1.249 -
1.250 -Goalw [Leaf_def,o_def] "ntrunc (Suc k) (Leaf a) = Leaf(a)";
1.251 -by (rtac ntrunc_Atom 1);
1.252 -qed "ntrunc_Leaf";
1.253 -
1.254 -Goalw [Numb_def,o_def] "ntrunc (Suc k) (Numb i) = Numb(i)";
1.255 -by (rtac ntrunc_Atom 1);
1.256 -qed "ntrunc_Numb";
1.257 -
1.258 -Goalw [Scons_def,ntrunc_def,One_nat_def]
1.259 - "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)";
1.260 -by (safe_tac (claset() addSIs [imageI]));
1.261 -by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
1.262 -by (REPEAT (rtac Suc_less_SucD 1 THEN
1.263 - rtac (ndepth_Push_Node RS subst) 1 THEN
1.264 - assume_tac 1));
1.265 -qed "ntrunc_Scons";
1.266 -
1.267 -Addsimps [ntrunc_0, ntrunc_Atom, ntrunc_Leaf, ntrunc_Numb, ntrunc_Scons];
1.268 -
1.269 -
1.270 -(** Injection nodes **)
1.271 -
1.272 -Goalw [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
1.273 -by (Simp_tac 1);
1.274 -by (rewtac Scons_def);
1.275 -by (Blast_tac 1);
1.276 -qed "ntrunc_one_In0";
1.277 -
1.278 -Goalw [In0_def]
1.279 - "ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)";
1.280 -by (Simp_tac 1);
1.281 -qed "ntrunc_In0";
1.282 -
1.283 -Goalw [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
1.284 -by (Simp_tac 1);
1.285 -by (rewtac Scons_def);
1.286 -by (Blast_tac 1);
1.287 -qed "ntrunc_one_In1";
1.288 -
1.289 -Goalw [In1_def]
1.290 - "ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)";
1.291 -by (Simp_tac 1);
1.292 -qed "ntrunc_In1";
1.293 -
1.294 -Addsimps [ntrunc_one_In0, ntrunc_In0, ntrunc_one_In1, ntrunc_In1];
1.295 -
1.296 -
1.297 -(*** Cartesian Product ***)
1.298 -
1.299 -Goalw [uprod_def] "[| M:A; N:B |] ==> Scons M N : uprod A B";
1.300 -by (REPEAT (ares_tac [singletonI,UN_I] 1));
1.301 -qed "uprodI";
1.302 -
1.303 -(*The general elimination rule*)
1.304 -val major::prems = Goalw [uprod_def]
1.305 - "[| c : uprod A B; \
1.306 -\ !!x y. [| x:A; y:B; c = Scons x y |] ==> P \
1.307 -\ |] ==> P";
1.308 -by (cut_facts_tac [major] 1);
1.309 -by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1
1.310 - ORELSE resolve_tac prems 1));
1.311 -qed "uprodE";
1.312 -
1.313 -(*Elimination of a pair -- introduces no eigenvariables*)
1.314 -val prems = Goal
1.315 - "[| Scons M N : uprod A B; [| M:A; N:B |] ==> P \
1.316 -\ |] ==> P";
1.317 -by (rtac uprodE 1);
1.318 -by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Scons_inject,ssubst] 1));
1.319 -qed "uprodE2";
1.320 -
1.321 -
1.322 -(*** Disjoint Sum ***)
1.323 -
1.324 -Goalw [usum_def] "M:A ==> In0(M) : usum A B";
1.325 -by (Blast_tac 1);
1.326 -qed "usum_In0I";
1.327 -
1.328 -Goalw [usum_def] "N:B ==> In1(N) : usum A B";
1.329 -by (Blast_tac 1);
1.330 -qed "usum_In1I";
1.331 -
1.332 -val major::prems = Goalw [usum_def]
1.333 - "[| u : usum A B; \
1.334 -\ !!x. [| x:A; u=In0(x) |] ==> P; \
1.335 -\ !!y. [| y:B; u=In1(y) |] ==> P \
1.336 -\ |] ==> P";
1.337 -by (rtac (major RS UnE) 1);
1.338 -by (REPEAT (rtac refl 1
1.339 - ORELSE eresolve_tac (prems@[imageE,ssubst]) 1));
1.340 -qed "usumE";
1.341 -
1.342 -
1.343 -(** Injection **)
1.344 -
1.345 -Goalw [In0_def,In1_def,One_nat_def] "In0(M) ~= In1(N)";
1.346 -by (rtac notI 1);
1.347 -by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
1.348 -qed "In0_not_In1";
1.349 -
1.350 -bind_thm ("In1_not_In0", In0_not_In1 RS not_sym);
1.351 -
1.352 -AddIffs [In0_not_In1, In1_not_In0];
1.353 -
1.354 -Goalw [In0_def] "In0(M) = In0(N) ==> M=N";
1.355 -by (etac (Scons_inject2) 1);
1.356 -qed "In0_inject";
1.357 -
1.358 -Goalw [In1_def] "In1(M) = In1(N) ==> M=N";
1.359 -by (etac (Scons_inject2) 1);
1.360 -qed "In1_inject";
1.361 -
1.362 -Goal "(In0 M = In0 N) = (M=N)";
1.363 -by (blast_tac (claset() addSDs [In0_inject]) 1);
1.364 -qed "In0_eq";
1.365 -
1.366 -Goal "(In1 M = In1 N) = (M=N)";
1.367 -by (blast_tac (claset() addSDs [In1_inject]) 1);
1.368 -qed "In1_eq";
1.369 -
1.370 -AddIffs [In0_eq, In1_eq];
1.371 -
1.372 -Goal "inj In0";
1.373 -by (blast_tac (claset() addSIs [injI]) 1);
1.374 -qed "inj_In0";
1.375 -
1.376 -Goal "inj In1";
1.377 -by (blast_tac (claset() addSIs [injI]) 1);
1.378 -qed "inj_In1";
1.379 -
1.380 -
1.381 -(*** Function spaces ***)
1.382 -
1.383 -Goalw [Lim_def] "Lim f = Lim g ==> f = g";
1.384 -by (rtac ext 1);
1.385 -by (blast_tac (claset() addSEs [Push_Node_inject]) 1);
1.386 -qed "Lim_inject";
1.387 -
1.388 -
1.389 -(*** proving equality of sets and functions using ntrunc ***)
1.390 -
1.391 -Goalw [ntrunc_def] "ntrunc k M <= M";
1.392 -by (Blast_tac 1);
1.393 -qed "ntrunc_subsetI";
1.394 -
1.395 -val [major] = Goalw [ntrunc_def] "(!!k. ntrunc k M <= N) ==> M<=N";
1.396 -by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2,
1.397 - major RS subsetD]) 1);
1.398 -qed "ntrunc_subsetD";
1.399 -
1.400 -(*A generalized form of the take-lemma*)
1.401 -val [major] = Goal "(!!k. ntrunc k M = ntrunc k N) ==> M=N";
1.402 -by (rtac equalityI 1);
1.403 -by (ALLGOALS (rtac ntrunc_subsetD));
1.404 -by (ALLGOALS (rtac (ntrunc_subsetI RSN (2, subset_trans))));
1.405 -by (rtac (major RS equalityD1) 1);
1.406 -by (rtac (major RS equalityD2) 1);
1.407 -qed "ntrunc_equality";
1.408 -
1.409 -val [major] = Goalw [o_def]
1.410 - "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2";
1.411 -by (rtac (ntrunc_equality RS ext) 1);
1.412 -by (rtac (major RS fun_cong) 1);
1.413 -qed "ntrunc_o_equality";
1.414 -
1.415 -(*** Monotonicity ***)
1.416 -
1.417 -Goalw [uprod_def] "[| A<=A'; B<=B' |] ==> uprod A B <= uprod A' B'";
1.418 -by (Blast_tac 1);
1.419 -qed "uprod_mono";
1.420 -
1.421 -Goalw [usum_def] "[| A<=A'; B<=B' |] ==> usum A B <= usum A' B'";
1.422 -by (Blast_tac 1);
1.423 -qed "usum_mono";
1.424 -
1.425 -Goalw [Scons_def] "[| M<=M'; N<=N' |] ==> Scons M N <= Scons M' N'";
1.426 -by (Blast_tac 1);
1.427 -qed "Scons_mono";
1.428 -
1.429 -Goalw [In0_def] "M<=N ==> In0(M) <= In0(N)";
1.430 -by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
1.431 -qed "In0_mono";
1.432 -
1.433 -Goalw [In1_def] "M<=N ==> In1(M) <= In1(N)";
1.434 -by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
1.435 -qed "In1_mono";
1.436 -
1.437 -
1.438 -(*** Split and Case ***)
1.439 -
1.440 -Goalw [Split_def] "Split c (Scons M N) = c M N";
1.441 -by (Blast_tac 1);
1.442 -qed "Split";
1.443 -
1.444 -Goalw [Case_def] "Case c d (In0 M) = c(M)";
1.445 -by (Blast_tac 1);
1.446 -qed "Case_In0";
1.447 -
1.448 -Goalw [Case_def] "Case c d (In1 N) = d(N)";
1.449 -by (Blast_tac 1);
1.450 -qed "Case_In1";
1.451 -
1.452 -Addsimps [Split, Case_In0, Case_In1];
1.453 -
1.454 -
1.455 -(**** UN x. B(x) rules ****)
1.456 -
1.457 -Goalw [ntrunc_def] "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))";
1.458 -by (Blast_tac 1);
1.459 -qed "ntrunc_UN1";
1.460 -
1.461 -Goalw [Scons_def] "Scons (UN x. f x) M = (UN x. Scons (f x) M)";
1.462 -by (Blast_tac 1);
1.463 -qed "Scons_UN1_x";
1.464 -
1.465 -Goalw [Scons_def] "Scons M (UN x. f x) = (UN x. Scons M (f x))";
1.466 -by (Blast_tac 1);
1.467 -qed "Scons_UN1_y";
1.468 -
1.469 -Goalw [In0_def] "In0(UN x. f(x)) = (UN x. In0(f(x)))";
1.470 -by (rtac Scons_UN1_y 1);
1.471 -qed "In0_UN1";
1.472 -
1.473 -Goalw [In1_def] "In1(UN x. f(x)) = (UN x. In1(f(x)))";
1.474 -by (rtac Scons_UN1_y 1);
1.475 -qed "In1_UN1";
1.476 -
1.477 -
1.478 -(*** Equality for Cartesian Product ***)
1.479 -
1.480 -Goalw [dprod_def]
1.481 - "[| (M,M'):r; (N,N'):s |] ==> (Scons M N, Scons M' N') : dprod r s";
1.482 -by (Blast_tac 1);
1.483 -qed "dprodI";
1.484 -
1.485 -(*The general elimination rule*)
1.486 -val major::prems = Goalw [dprod_def]
1.487 - "[| c : dprod r s; \
1.488 -\ !!x y x' y'. [| (x,x') : r; (y,y') : s; c = (Scons x y, Scons x' y') |] ==> P \
1.489 -\ |] ==> P";
1.490 -by (cut_facts_tac [major] 1);
1.491 -by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, mem_splitE, singletonE]));
1.492 -by (REPEAT (ares_tac prems 1 ORELSE hyp_subst_tac 1));
1.493 -qed "dprodE";
1.494 -
1.495 -
1.496 -(*** Equality for Disjoint Sum ***)
1.497 -
1.498 -Goalw [dsum_def] "(M,M'):r ==> (In0(M), In0(M')) : dsum r s";
1.499 -by (Blast_tac 1);
1.500 -qed "dsum_In0I";
1.501 -
1.502 -Goalw [dsum_def] "(N,N'):s ==> (In1(N), In1(N')) : dsum r s";
1.503 -by (Blast_tac 1);
1.504 -qed "dsum_In1I";
1.505 -
1.506 -val major::prems = Goalw [dsum_def]
1.507 - "[| w : dsum r s; \
1.508 -\ !!x x'. [| (x,x') : r; w = (In0(x), In0(x')) |] ==> P; \
1.509 -\ !!y y'. [| (y,y') : s; w = (In1(y), In1(y')) |] ==> P \
1.510 -\ |] ==> P";
1.511 -by (cut_facts_tac [major] 1);
1.512 -by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, UnE, mem_splitE, singletonE]));
1.513 -by (DEPTH_SOLVE (ares_tac prems 1 ORELSE hyp_subst_tac 1));
1.514 -qed "dsumE";
1.515 -
1.516 -AddSIs [uprodI, dprodI];
1.517 -AddIs [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
1.518 -AddSEs [uprodE, dprodE, usumE, dsumE];
1.519 -
1.520 -
1.521 -(*** Monotonicity ***)
1.522 -
1.523 -Goal "[| r<=r'; s<=s' |] ==> dprod r s <= dprod r' s'";
1.524 -by (Blast_tac 1);
1.525 -qed "dprod_mono";
1.526 -
1.527 -Goal "[| r<=r'; s<=s' |] ==> dsum r s <= dsum r' s'";
1.528 -by (Blast_tac 1);
1.529 -qed "dsum_mono";
1.530 -
1.531 -
1.532 -(*** Bounding theorems ***)
1.533 -
1.534 -Goal "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)";
1.535 -by (Blast_tac 1);
1.536 -qed "dprod_Sigma";
1.537 -
1.538 -bind_thm ("dprod_subset_Sigma", [dprod_mono, dprod_Sigma] MRS subset_trans |> standard);
1.539 -
1.540 -(*Dependent version*)
1.541 -Goal "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))";
1.542 -by Safe_tac;
1.543 -by (stac Split 1);
1.544 -by (Blast_tac 1);
1.545 -qed "dprod_subset_Sigma2";
1.546 -
1.547 -Goal "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)";
1.548 -by (Blast_tac 1);
1.549 -qed "dsum_Sigma";
1.550 -
1.551 -bind_thm ("dsum_subset_Sigma", [dsum_mono, dsum_Sigma] MRS subset_trans |> standard);
1.552 -
1.553 -
1.554 -(*** Domain ***)
1.555 -
1.556 -Goal "Domain (dprod r s) = uprod (Domain r) (Domain s)";
1.557 -by Auto_tac;
1.558 -qed "Domain_dprod";
1.559 -
1.560 -Goal "Domain (dsum r s) = usum (Domain r) (Domain s)";
1.561 -by Auto_tac;
1.562 -qed "Domain_dsum";
1.563 -
1.564 -Addsimps [Domain_dprod, Domain_dsum];
2.1 --- a/src/HOL/Datatype_Universe.thy Wed Dec 08 15:15:49 2004 +0100
2.2 +++ b/src/HOL/Datatype_Universe.thy Thu Dec 09 12:03:06 2004 +0100
2.3 @@ -3,97 +3,637 @@
2.4 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
2.5 Copyright 1993 University of Cambridge
2.6
2.7 -Declares the type ('a, 'b) node, a subtype of (nat=>'b+nat) * ('a+nat)
2.8 -
2.9 -Defines "Cartesian Product" and "Disjoint Sum" as set operations.
2.10 Could <*> be generalized to a general summation (Sigma)?
2.11 *)
2.12
2.13 -Datatype_Universe = NatArith + Sum_Type +
2.14 +header{*Analogues of the Cartesian Product and Disjoint Sum for Datatypes*}
2.15
2.16 +theory Datatype_Universe
2.17 +imports NatArith Sum_Type
2.18 +begin
2.19
2.20 -(** lists, trees will be sets of nodes **)
2.21
2.22 typedef (Node)
2.23 ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
2.24 + --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
2.25 + by auto
2.26
2.27 -types
2.28 - 'a item = ('a, unit) node set
2.29 - ('a, 'b) dtree = ('a, 'b) node set
2.30 +text{*Datatypes will be represented by sets of type @{text node}*}
2.31 +
2.32 +types 'a item = "('a, unit) node set"
2.33 + ('a, 'b) dtree = "('a, 'b) node set"
2.34
2.35 consts
2.36 apfst :: "['a=>'c, 'a*'b] => 'c*'b"
2.37 Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
2.38
2.39 Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
2.40 - ndepth :: ('a, 'b) node => nat
2.41 + ndepth :: "('a, 'b) node => nat"
2.42
2.43 Atom :: "('a + nat) => ('a, 'b) dtree"
2.44 - Leaf :: 'a => ('a, 'b) dtree
2.45 - Numb :: nat => ('a, 'b) dtree
2.46 - Scons :: [('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree
2.47 - In0,In1 :: ('a, 'b) dtree => ('a, 'b) dtree
2.48 - Lim :: ('b => ('a, 'b) dtree) => ('a, 'b) dtree
2.49 + Leaf :: "'a => ('a, 'b) dtree"
2.50 + Numb :: "nat => ('a, 'b) dtree"
2.51 + Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
2.52 + In0 :: "('a, 'b) dtree => ('a, 'b) dtree"
2.53 + In1 :: "('a, 'b) dtree => ('a, 'b) dtree"
2.54 + Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
2.55
2.56 - ntrunc :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree
2.57 + ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
2.58
2.59 - uprod :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set
2.60 - usum :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set
2.61 + uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
2.62 + usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
2.63
2.64 - Split :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
2.65 - Case :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
2.66 + Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
2.67 + Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
2.68
2.69 - dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
2.70 + dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
2.71 => (('a, 'b) dtree * ('a, 'b) dtree)set"
2.72 - dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
2.73 + dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
2.74 => (('a, 'b) dtree * ('a, 'b) dtree)set"
2.75
2.76
2.77 defs
2.78
2.79 - Push_Node_def "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
2.80 + Push_Node_def: "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
2.81
2.82 (*crude "lists" of nats -- needed for the constructions*)
2.83 - apfst_def "apfst == (%f (x,y). (f(x),y))"
2.84 - Push_def "Push == (%b h. nat_case b h)"
2.85 + apfst_def: "apfst == (%f (x,y). (f(x),y))"
2.86 + Push_def: "Push == (%b h. nat_case b h)"
2.87
2.88 (** operations on S-expressions -- sets of nodes **)
2.89
2.90 (*S-expression constructors*)
2.91 - Atom_def "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
2.92 - Scons_def "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
2.93 + Atom_def: "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
2.94 + Scons_def: "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
2.95
2.96 (*Leaf nodes, with arbitrary or nat labels*)
2.97 - Leaf_def "Leaf == Atom o Inl"
2.98 - Numb_def "Numb == Atom o Inr"
2.99 + Leaf_def: "Leaf == Atom o Inl"
2.100 + Numb_def: "Numb == Atom o Inr"
2.101
2.102 (*Injections of the "disjoint sum"*)
2.103 - In0_def "In0(M) == Scons (Numb 0) M"
2.104 - In1_def "In1(M) == Scons (Numb 1) M"
2.105 + In0_def: "In0(M) == Scons (Numb 0) M"
2.106 + In1_def: "In1(M) == Scons (Numb 1) M"
2.107
2.108 (*Function spaces*)
2.109 - Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
2.110 + Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
2.111
2.112 (*the set of nodes with depth less than k*)
2.113 - ndepth_def "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
2.114 - ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}"
2.115 + ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
2.116 + ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}"
2.117
2.118 (*products and sums for the "universe"*)
2.119 - uprod_def "uprod A B == UN x:A. UN y:B. { Scons x y }"
2.120 - usum_def "usum A B == In0`A Un In1`B"
2.121 + uprod_def: "uprod A B == UN x:A. UN y:B. { Scons x y }"
2.122 + usum_def: "usum A B == In0`A Un In1`B"
2.123
2.124 (*the corresponding eliminators*)
2.125 - Split_def "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
2.126 + Split_def: "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
2.127
2.128 - Case_def "Case c d M == THE u. (EX x . M = In0(x) & u = c(x))
2.129 + Case_def: "Case c d M == THE u. (EX x . M = In0(x) & u = c(x))
2.130 | (EX y . M = In1(y) & u = d(y))"
2.131
2.132
2.133 (** equality for the "universe" **)
2.134
2.135 - dprod_def "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
2.136 + dprod_def: "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
2.137
2.138 - dsum_def "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
2.139 + dsum_def: "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
2.140 (UN (y,y'):s. {(In1(y),In1(y'))})"
2.141
2.142 +
2.143 +
2.144 +(** apfst -- can be used in similar type definitions **)
2.145 +
2.146 +lemma apfst_conv [simp]: "apfst f (a,b) = (f(a),b)"
2.147 +by (simp add: apfst_def)
2.148 +
2.149 +
2.150 +lemma apfst_convE:
2.151 + "[| q = apfst f p; !!x y. [| p = (x,y); q = (f(x),y) |] ==> R
2.152 + |] ==> R"
2.153 +by (force simp add: apfst_def)
2.154 +
2.155 +(** Push -- an injection, analogous to Cons on lists **)
2.156 +
2.157 +lemma Push_inject1: "Push i f = Push j g ==> i=j"
2.158 +apply (simp add: Push_def expand_fun_eq)
2.159 +apply (drule_tac x=0 in spec, simp)
2.160 +done
2.161 +
2.162 +lemma Push_inject2: "Push i f = Push j g ==> f=g"
2.163 +apply (auto simp add: Push_def expand_fun_eq)
2.164 +apply (drule_tac x="Suc x" in spec, simp)
2.165 +done
2.166 +
2.167 +lemma Push_inject:
2.168 + "[| Push i f =Push j g; [| i=j; f=g |] ==> P |] ==> P"
2.169 +by (blast dest: Push_inject1 Push_inject2)
2.170 +
2.171 +lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"
2.172 +by (auto simp add: Push_def expand_fun_eq split: nat.split_asm)
2.173 +
2.174 +(*** Isomorphisms ***)
2.175 +
2.176 +lemma inj_Rep_Node: "inj(Rep_Node)"
2.177 +apply (rule inj_on_inverseI)
2.178 +apply (rule Rep_Node_inverse)
2.179 +done
2.180 +
2.181 +lemma inj_on_Abs_Node: "inj_on Abs_Node Node"
2.182 +apply (rule inj_on_inverseI)
2.183 +apply (erule Abs_Node_inverse)
2.184 +done
2.185 +
2.186 +lemmas Abs_Node_inj = inj_on_Abs_Node [THEN inj_onD, standard]
2.187 +
2.188 +
2.189 +(*** Introduction rules for Node ***)
2.190 +
2.191 +lemma Node_K0_I: "(%k. Inr 0, a) : Node"
2.192 +by (simp add: Node_def)
2.193 +
2.194 +lemma Node_Push_I:
2.195 + "p: Node ==> apfst (Push i) p : Node"
2.196 +apply (simp add: Node_def Push_def)
2.197 +apply (fast intro!: apfst_conv nat_case_Suc [THEN trans])
2.198 +done
2.199 +
2.200 +
2.201 +subsubsection{*Freeness: Distinctness of Constructors*}
2.202 +
2.203 +(** Scons vs Atom **)
2.204 +
2.205 +lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)"
2.206 +apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def)
2.207 +apply (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I]
2.208 + dest!: Abs_Node_inj
2.209 + elim!: apfst_convE sym [THEN Push_neq_K0])
2.210 +done
2.211 +
2.212 +lemmas Atom_not_Scons = Scons_not_Atom [THEN not_sym, standard, iff]
2.213 +
2.214 +
2.215 +(*** Injectiveness ***)
2.216 +
2.217 +(** Atomic nodes **)
2.218 +
2.219 +lemma inj_Atom: "inj(Atom)"
2.220 +apply (simp add: Atom_def)
2.221 +apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj)
2.222 +done
2.223 +lemmas Atom_inject = inj_Atom [THEN injD, standard]
2.224 +
2.225 +lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)"
2.226 +by (blast dest!: Atom_inject)
2.227 +
2.228 +lemma inj_Leaf: "inj(Leaf)"
2.229 +apply (simp add: Leaf_def o_def)
2.230 +apply (rule inj_onI)
2.231 +apply (erule Atom_inject [THEN Inl_inject])
2.232 +done
2.233 +
2.234 +lemmas Leaf_inject = inj_Leaf [THEN injD, standard, dest!]
2.235 +
2.236 +lemma inj_Numb: "inj(Numb)"
2.237 +apply (simp add: Numb_def o_def)
2.238 +apply (rule inj_onI)
2.239 +apply (erule Atom_inject [THEN Inr_inject])
2.240 +done
2.241 +
2.242 +lemmas Numb_inject = inj_Numb [THEN injD, standard, dest!]
2.243 +
2.244 +
2.245 +(** Injectiveness of Push_Node **)
2.246 +
2.247 +lemma Push_Node_inject:
2.248 + "[| Push_Node i m =Push_Node j n; [| i=j; m=n |] ==> P
2.249 + |] ==> P"
2.250 +apply (simp add: Push_Node_def)
2.251 +apply (erule Abs_Node_inj [THEN apfst_convE])
2.252 +apply (rule Rep_Node [THEN Node_Push_I])+
2.253 +apply (erule sym [THEN apfst_convE])
2.254 +apply (blast intro: inj_Rep_Node [THEN injD] trans sym elim!: Push_inject)
2.255 +done
2.256 +
2.257 +
2.258 +(** Injectiveness of Scons **)
2.259 +
2.260 +lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'"
2.261 +apply (simp add: Scons_def One_nat_def)
2.262 +apply (blast dest!: Push_Node_inject)
2.263 +done
2.264 +
2.265 +lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'"
2.266 +apply (simp add: Scons_def One_nat_def)
2.267 +apply (blast dest!: Push_Node_inject)
2.268 +done
2.269 +
2.270 +lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'"
2.271 +apply (erule equalityE)
2.272 +apply (rules intro: equalityI Scons_inject_lemma1)
2.273 +done
2.274 +
2.275 +lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'"
2.276 +apply (erule equalityE)
2.277 +apply (rules intro: equalityI Scons_inject_lemma2)
2.278 +done
2.279 +
2.280 +lemma Scons_inject:
2.281 + "[| Scons M N = Scons M' N'; [| M=M'; N=N' |] ==> P |] ==> P"
2.282 +by (rules dest: Scons_inject1 Scons_inject2)
2.283 +
2.284 +lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')"
2.285 +by (blast elim!: Scons_inject)
2.286 +
2.287 +(*** Distinctness involving Leaf and Numb ***)
2.288 +
2.289 +(** Scons vs Leaf **)
2.290 +
2.291 +lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
2.292 +by (simp add: Leaf_def o_def Scons_not_Atom)
2.293 +
2.294 +lemmas Leaf_not_Scons = Scons_not_Leaf [THEN not_sym, standard, iff]
2.295 +
2.296 +
2.297 +(** Scons vs Numb **)
2.298 +
2.299 +lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
2.300 +by (simp add: Numb_def o_def Scons_not_Atom)
2.301 +
2.302 +lemmas Numb_not_Scons = Scons_not_Numb [THEN not_sym, standard, iff]
2.303 +
2.304 +
2.305 +
2.306 +(** Leaf vs Numb **)
2.307 +
2.308 +lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
2.309 +by (simp add: Leaf_def Numb_def)
2.310 +
2.311 +lemmas Numb_not_Leaf = Leaf_not_Numb [THEN not_sym, standard, iff]
2.312 +
2.313 +
2.314 +
2.315 +(*** ndepth -- the depth of a node ***)
2.316 +
2.317 +lemma ndepth_K0: "ndepth (Abs_Node(%k. Inr 0, x)) = 0"
2.318 +by (simp add: ndepth_def Node_K0_I [THEN Abs_Node_inverse] Least_equality)
2.319 +
2.320 +lemma ndepth_Push_Node_aux:
2.321 + "nat_case (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k"
2.322 +apply (induct_tac "k", auto)
2.323 +apply (erule Least_le)
2.324 +done
2.325 +
2.326 +lemma ndepth_Push_Node:
2.327 + "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))"
2.328 +apply (insert Rep_Node [of n, unfolded Node_def])
2.329 +apply (auto simp add: ndepth_def Push_Node_def
2.330 + Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse])
2.331 +apply (rule Least_equality)
2.332 +apply (auto simp add: Push_def ndepth_Push_Node_aux)
2.333 +apply (erule LeastI)
2.334 +done
2.335 +
2.336 +
2.337 +(*** ntrunc applied to the various node sets ***)
2.338 +
2.339 +lemma ntrunc_0 [simp]: "ntrunc 0 M = {}"
2.340 +by (simp add: ntrunc_def)
2.341 +
2.342 +lemma ntrunc_Atom [simp]: "ntrunc (Suc k) (Atom a) = Atom(a)"
2.343 +by (auto simp add: Atom_def ntrunc_def ndepth_K0)
2.344 +
2.345 +lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)"
2.346 +by (simp add: Leaf_def o_def ntrunc_Atom)
2.347 +
2.348 +lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)"
2.349 +by (simp add: Numb_def o_def ntrunc_Atom)
2.350 +
2.351 +lemma ntrunc_Scons [simp]:
2.352 + "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"
2.353 +by (auto simp add: Scons_def ntrunc_def One_nat_def ndepth_Push_Node)
2.354 +
2.355 +
2.356 +
2.357 +(** Injection nodes **)
2.358 +
2.359 +lemma ntrunc_one_In0 [simp]: "ntrunc (Suc 0) (In0 M) = {}"
2.360 +apply (simp add: In0_def)
2.361 +apply (simp add: Scons_def)
2.362 +done
2.363 +
2.364 +lemma ntrunc_In0 [simp]: "ntrunc (Suc(Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"
2.365 +by (simp add: In0_def)
2.366 +
2.367 +lemma ntrunc_one_In1 [simp]: "ntrunc (Suc 0) (In1 M) = {}"
2.368 +apply (simp add: In1_def)
2.369 +apply (simp add: Scons_def)
2.370 +done
2.371 +
2.372 +lemma ntrunc_In1 [simp]: "ntrunc (Suc(Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)"
2.373 +by (simp add: In1_def)
2.374 +
2.375 +
2.376 +subsection{*Set Constructions*}
2.377 +
2.378 +
2.379 +(*** Cartesian Product ***)
2.380 +
2.381 +lemma uprodI [intro!]: "[| M:A; N:B |] ==> Scons M N : uprod A B"
2.382 +by (simp add: uprod_def)
2.383 +
2.384 +(*The general elimination rule*)
2.385 +lemma uprodE [elim!]:
2.386 + "[| c : uprod A B;
2.387 + !!x y. [| x:A; y:B; c = Scons x y |] ==> P
2.388 + |] ==> P"
2.389 +by (auto simp add: uprod_def)
2.390 +
2.391 +
2.392 +(*Elimination of a pair -- introduces no eigenvariables*)
2.393 +lemma uprodE2: "[| Scons M N : uprod A B; [| M:A; N:B |] ==> P |] ==> P"
2.394 +by (auto simp add: uprod_def)
2.395 +
2.396 +
2.397 +(*** Disjoint Sum ***)
2.398 +
2.399 +lemma usum_In0I [intro]: "M:A ==> In0(M) : usum A B"
2.400 +by (simp add: usum_def)
2.401 +
2.402 +lemma usum_In1I [intro]: "N:B ==> In1(N) : usum A B"
2.403 +by (simp add: usum_def)
2.404 +
2.405 +lemma usumE [elim!]:
2.406 + "[| u : usum A B;
2.407 + !!x. [| x:A; u=In0(x) |] ==> P;
2.408 + !!y. [| y:B; u=In1(y) |] ==> P
2.409 + |] ==> P"
2.410 +by (auto simp add: usum_def)
2.411 +
2.412 +
2.413 +(** Injection **)
2.414 +
2.415 +lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
2.416 +by (auto simp add: In0_def In1_def One_nat_def)
2.417 +
2.418 +lemmas In1_not_In0 = In0_not_In1 [THEN not_sym, standard, iff]
2.419 +
2.420 +lemma In0_inject: "In0(M) = In0(N) ==> M=N"
2.421 +by (simp add: In0_def)
2.422 +
2.423 +lemma In1_inject: "In1(M) = In1(N) ==> M=N"
2.424 +by (simp add: In1_def)
2.425 +
2.426 +lemma In0_eq [iff]: "(In0 M = In0 N) = (M=N)"
2.427 +by (blast dest!: In0_inject)
2.428 +
2.429 +lemma In1_eq [iff]: "(In1 M = In1 N) = (M=N)"
2.430 +by (blast dest!: In1_inject)
2.431 +
2.432 +lemma inj_In0: "inj In0"
2.433 +by (blast intro!: inj_onI)
2.434 +
2.435 +lemma inj_In1: "inj In1"
2.436 +by (blast intro!: inj_onI)
2.437 +
2.438 +
2.439 +(*** Function spaces ***)
2.440 +
2.441 +lemma Lim_inject: "Lim f = Lim g ==> f = g"
2.442 +apply (simp add: Lim_def)
2.443 +apply (rule ext)
2.444 +apply (blast elim!: Push_Node_inject)
2.445 +done
2.446 +
2.447 +
2.448 +(*** proving equality of sets and functions using ntrunc ***)
2.449 +
2.450 +lemma ntrunc_subsetI: "ntrunc k M <= M"
2.451 +by (auto simp add: ntrunc_def)
2.452 +
2.453 +lemma ntrunc_subsetD: "(!!k. ntrunc k M <= N) ==> M<=N"
2.454 +by (auto simp add: ntrunc_def)
2.455 +
2.456 +(*A generalized form of the take-lemma*)
2.457 +lemma ntrunc_equality: "(!!k. ntrunc k M = ntrunc k N) ==> M=N"
2.458 +apply (rule equalityI)
2.459 +apply (rule_tac [!] ntrunc_subsetD)
2.460 +apply (rule_tac [!] ntrunc_subsetI [THEN [2] subset_trans], auto)
2.461 +done
2.462 +
2.463 +lemma ntrunc_o_equality:
2.464 + "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2"
2.465 +apply (rule ntrunc_equality [THEN ext])
2.466 +apply (simp add: expand_fun_eq)
2.467 +done
2.468 +
2.469 +
2.470 +(*** Monotonicity ***)
2.471 +
2.472 +lemma uprod_mono: "[| A<=A'; B<=B' |] ==> uprod A B <= uprod A' B'"
2.473 +by (simp add: uprod_def, blast)
2.474 +
2.475 +lemma usum_mono: "[| A<=A'; B<=B' |] ==> usum A B <= usum A' B'"
2.476 +by (simp add: usum_def, blast)
2.477 +
2.478 +lemma Scons_mono: "[| M<=M'; N<=N' |] ==> Scons M N <= Scons M' N'"
2.479 +by (simp add: Scons_def, blast)
2.480 +
2.481 +lemma In0_mono: "M<=N ==> In0(M) <= In0(N)"
2.482 +by (simp add: In0_def subset_refl Scons_mono)
2.483 +
2.484 +lemma In1_mono: "M<=N ==> In1(M) <= In1(N)"
2.485 +by (simp add: In1_def subset_refl Scons_mono)
2.486 +
2.487 +
2.488 +(*** Split and Case ***)
2.489 +
2.490 +lemma Split [simp]: "Split c (Scons M N) = c M N"
2.491 +by (simp add: Split_def)
2.492 +
2.493 +lemma Case_In0 [simp]: "Case c d (In0 M) = c(M)"
2.494 +by (simp add: Case_def)
2.495 +
2.496 +lemma Case_In1 [simp]: "Case c d (In1 N) = d(N)"
2.497 +by (simp add: Case_def)
2.498 +
2.499 +
2.500 +
2.501 +(**** UN x. B(x) rules ****)
2.502 +
2.503 +lemma ntrunc_UN1: "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))"
2.504 +by (simp add: ntrunc_def, blast)
2.505 +
2.506 +lemma Scons_UN1_x: "Scons (UN x. f x) M = (UN x. Scons (f x) M)"
2.507 +by (simp add: Scons_def, blast)
2.508 +
2.509 +lemma Scons_UN1_y: "Scons M (UN x. f x) = (UN x. Scons M (f x))"
2.510 +by (simp add: Scons_def, blast)
2.511 +
2.512 +lemma In0_UN1: "In0(UN x. f(x)) = (UN x. In0(f(x)))"
2.513 +by (simp add: In0_def Scons_UN1_y)
2.514 +
2.515 +lemma In1_UN1: "In1(UN x. f(x)) = (UN x. In1(f(x)))"
2.516 +by (simp add: In1_def Scons_UN1_y)
2.517 +
2.518 +
2.519 +(*** Equality for Cartesian Product ***)
2.520 +
2.521 +lemma dprodI [intro!]:
2.522 + "[| (M,M'):r; (N,N'):s |] ==> (Scons M N, Scons M' N') : dprod r s"
2.523 +by (auto simp add: dprod_def)
2.524 +
2.525 +(*The general elimination rule*)
2.526 +lemma dprodE [elim!]:
2.527 + "[| c : dprod r s;
2.528 + !!x y x' y'. [| (x,x') : r; (y,y') : s;
2.529 + c = (Scons x y, Scons x' y') |] ==> P
2.530 + |] ==> P"
2.531 +by (auto simp add: dprod_def)
2.532 +
2.533 +
2.534 +(*** Equality for Disjoint Sum ***)
2.535 +
2.536 +lemma dsum_In0I [intro]: "(M,M'):r ==> (In0(M), In0(M')) : dsum r s"
2.537 +by (auto simp add: dsum_def)
2.538 +
2.539 +lemma dsum_In1I [intro]: "(N,N'):s ==> (In1(N), In1(N')) : dsum r s"
2.540 +by (auto simp add: dsum_def)
2.541 +
2.542 +lemma dsumE [elim!]:
2.543 + "[| w : dsum r s;
2.544 + !!x x'. [| (x,x') : r; w = (In0(x), In0(x')) |] ==> P;
2.545 + !!y y'. [| (y,y') : s; w = (In1(y), In1(y')) |] ==> P
2.546 + |] ==> P"
2.547 +by (auto simp add: dsum_def)
2.548 +
2.549 +
2.550 +(*** Monotonicity ***)
2.551 +
2.552 +lemma dprod_mono: "[| r<=r'; s<=s' |] ==> dprod r s <= dprod r' s'"
2.553 +by blast
2.554 +
2.555 +lemma dsum_mono: "[| r<=r'; s<=s' |] ==> dsum r s <= dsum r' s'"
2.556 +by blast
2.557 +
2.558 +
2.559 +(*** Bounding theorems ***)
2.560 +
2.561 +lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"
2.562 +by blast
2.563 +
2.564 +lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma, standard]
2.565 +
2.566 +(*Dependent version*)
2.567 +lemma dprod_subset_Sigma2:
2.568 + "(dprod (Sigma A B) (Sigma C D)) <=
2.569 + Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
2.570 +by auto
2.571 +
2.572 +lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"
2.573 +by blast
2.574 +
2.575 +lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
2.576 +
2.577 +
2.578 +(*** Domain ***)
2.579 +
2.580 +lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
2.581 +by auto
2.582 +
2.583 +lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
2.584 +by auto
2.585 +
2.586 +ML
2.587 +{*
2.588 +val apfst_conv = thm "apfst_conv";
2.589 +val apfst_convE = thm "apfst_convE";
2.590 +val Push_inject1 = thm "Push_inject1";
2.591 +val Push_inject2 = thm "Push_inject2";
2.592 +val Push_inject = thm "Push_inject";
2.593 +val Push_neq_K0 = thm "Push_neq_K0";
2.594 +val inj_Rep_Node = thm "inj_Rep_Node";
2.595 +val inj_on_Abs_Node = thm "inj_on_Abs_Node";
2.596 +val Abs_Node_inj = thm "Abs_Node_inj";
2.597 +val Node_K0_I = thm "Node_K0_I";
2.598 +val Node_Push_I = thm "Node_Push_I";
2.599 +val Scons_not_Atom = thm "Scons_not_Atom";
2.600 +val Atom_not_Scons = thm "Atom_not_Scons";
2.601 +val inj_Atom = thm "inj_Atom";
2.602 +val Atom_inject = thm "Atom_inject";
2.603 +val Atom_Atom_eq = thm "Atom_Atom_eq";
2.604 +val inj_Leaf = thm "inj_Leaf";
2.605 +val Leaf_inject = thm "Leaf_inject";
2.606 +val inj_Numb = thm "inj_Numb";
2.607 +val Numb_inject = thm "Numb_inject";
2.608 +val Push_Node_inject = thm "Push_Node_inject";
2.609 +val Scons_inject1 = thm "Scons_inject1";
2.610 +val Scons_inject2 = thm "Scons_inject2";
2.611 +val Scons_inject = thm "Scons_inject";
2.612 +val Scons_Scons_eq = thm "Scons_Scons_eq";
2.613 +val Scons_not_Leaf = thm "Scons_not_Leaf";
2.614 +val Leaf_not_Scons = thm "Leaf_not_Scons";
2.615 +val Scons_not_Numb = thm "Scons_not_Numb";
2.616 +val Numb_not_Scons = thm "Numb_not_Scons";
2.617 +val Leaf_not_Numb = thm "Leaf_not_Numb";
2.618 +val Numb_not_Leaf = thm "Numb_not_Leaf";
2.619 +val ndepth_K0 = thm "ndepth_K0";
2.620 +val ndepth_Push_Node_aux = thm "ndepth_Push_Node_aux";
2.621 +val ndepth_Push_Node = thm "ndepth_Push_Node";
2.622 +val ntrunc_0 = thm "ntrunc_0";
2.623 +val ntrunc_Atom = thm "ntrunc_Atom";
2.624 +val ntrunc_Leaf = thm "ntrunc_Leaf";
2.625 +val ntrunc_Numb = thm "ntrunc_Numb";
2.626 +val ntrunc_Scons = thm "ntrunc_Scons";
2.627 +val ntrunc_one_In0 = thm "ntrunc_one_In0";
2.628 +val ntrunc_In0 = thm "ntrunc_In0";
2.629 +val ntrunc_one_In1 = thm "ntrunc_one_In1";
2.630 +val ntrunc_In1 = thm "ntrunc_In1";
2.631 +val uprodI = thm "uprodI";
2.632 +val uprodE = thm "uprodE";
2.633 +val uprodE2 = thm "uprodE2";
2.634 +val usum_In0I = thm "usum_In0I";
2.635 +val usum_In1I = thm "usum_In1I";
2.636 +val usumE = thm "usumE";
2.637 +val In0_not_In1 = thm "In0_not_In1";
2.638 +val In1_not_In0 = thm "In1_not_In0";
2.639 +val In0_inject = thm "In0_inject";
2.640 +val In1_inject = thm "In1_inject";
2.641 +val In0_eq = thm "In0_eq";
2.642 +val In1_eq = thm "In1_eq";
2.643 +val inj_In0 = thm "inj_In0";
2.644 +val inj_In1 = thm "inj_In1";
2.645 +val Lim_inject = thm "Lim_inject";
2.646 +val ntrunc_subsetI = thm "ntrunc_subsetI";
2.647 +val ntrunc_subsetD = thm "ntrunc_subsetD";
2.648 +val ntrunc_equality = thm "ntrunc_equality";
2.649 +val ntrunc_o_equality = thm "ntrunc_o_equality";
2.650 +val uprod_mono = thm "uprod_mono";
2.651 +val usum_mono = thm "usum_mono";
2.652 +val Scons_mono = thm "Scons_mono";
2.653 +val In0_mono = thm "In0_mono";
2.654 +val In1_mono = thm "In1_mono";
2.655 +val Split = thm "Split";
2.656 +val Case_In0 = thm "Case_In0";
2.657 +val Case_In1 = thm "Case_In1";
2.658 +val ntrunc_UN1 = thm "ntrunc_UN1";
2.659 +val Scons_UN1_x = thm "Scons_UN1_x";
2.660 +val Scons_UN1_y = thm "Scons_UN1_y";
2.661 +val In0_UN1 = thm "In0_UN1";
2.662 +val In1_UN1 = thm "In1_UN1";
2.663 +val dprodI = thm "dprodI";
2.664 +val dprodE = thm "dprodE";
2.665 +val dsum_In0I = thm "dsum_In0I";
2.666 +val dsum_In1I = thm "dsum_In1I";
2.667 +val dsumE = thm "dsumE";
2.668 +val dprod_mono = thm "dprod_mono";
2.669 +val dsum_mono = thm "dsum_mono";
2.670 +val dprod_Sigma = thm "dprod_Sigma";
2.671 +val dprod_subset_Sigma = thm "dprod_subset_Sigma";
2.672 +val dprod_subset_Sigma2 = thm "dprod_subset_Sigma2";
2.673 +val dsum_Sigma = thm "dsum_Sigma";
2.674 +val dsum_subset_Sigma = thm "dsum_subset_Sigma";
2.675 +val Domain_dprod = thm "Domain_dprod";
2.676 +val Domain_dsum = thm "Domain_dsum";
2.677 +*}
2.678 +
2.679 end
3.1 --- a/src/HOL/IsaMakefile Wed Dec 08 15:15:49 2004 +0100
3.2 +++ b/src/HOL/IsaMakefile Thu Dec 09 12:03:06 2004 +0100
3.3 @@ -81,7 +81,7 @@
3.4 $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
3.5 $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
3.6 $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
3.7 - Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \
3.8 + Datatype.thy Datatype_Universe.thy \
3.9 Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
3.10 Fun.thy Gfp.thy Hilbert_Choice.thy HOL.ML \
3.11 HOL.thy HOL_lemmas.ML Inductive.thy Infinite_Set.thy Integ/Numeral.thy \