converted Arith, Univ, func to Isar format!
authorpaulson
Sat May 18 20:08:17 2002 +0200 (2002-05-18)
changeset 13163e320a52ff711
parent 13162 660a71e712af
child 13164 dfc399c684e4
converted Arith, Univ, func to Isar format!
src/ZF/Arith.ML
src/ZF/Arith.thy
src/ZF/Integ/IntDiv.ML
src/ZF/IsaMakefile
src/ZF/OrderType.thy
src/ZF/Univ.ML
src/ZF/Univ.thy
src/ZF/func.ML
src/ZF/func.thy
     1.1 --- a/src/ZF/Arith.ML	Fri May 17 16:54:25 2002 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,516 +0,0 @@
     1.4 -(*  Title:      ZF/Arith.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1992  University of Cambridge
     1.8 -
     1.9 -Arithmetic operators and their definitions
    1.10 -
    1.11 -Proofs about elementary arithmetic: addition, multiplication, etc.
    1.12 -*)
    1.13 -
    1.14 -(*"Difference" is subtraction of natural numbers.
    1.15 -  There are no negative numbers; we have
    1.16 -     m #- n = 0  iff  m<=n   and     m #- n = succ(k) iff m>n.
    1.17 -  Also, rec(m, 0, %z w.z) is pred(m).   
    1.18 -*)
    1.19 -
    1.20 -Addsimps [rec_type, nat_0_le];
    1.21 -bind_thms ("nat_typechecks", [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat]);
    1.22 -
    1.23 -Goal "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)";
    1.24 -by (etac rev_mp 1);
    1.25 -by (induct_tac "k" 1);
    1.26 -by (Simp_tac 1);
    1.27 -by (Blast_tac 1);
    1.28 -val lemma = result();
    1.29 -
    1.30 -(* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
    1.31 -bind_thm ("zero_lt_natE", lemma RS bexE);
    1.32 -
    1.33 -
    1.34 -(** natify: coercion to "nat" **)
    1.35 -
    1.36 -Goalw [pred_def] "pred(succ(y)) = y";
    1.37 -by Auto_tac;  
    1.38 -qed "pred_succ_eq";
    1.39 -Addsimps [pred_succ_eq];
    1.40 -
    1.41 -Goal "natify(succ(x)) = succ(natify(x))";
    1.42 -by (rtac (natify_def RS def_Vrecursor RS trans) 1);
    1.43 -by Auto_tac;  
    1.44 -qed "natify_succ";
    1.45 -
    1.46 -Goal "natify(0) = 0";
    1.47 -by (rtac (natify_def RS def_Vrecursor RS trans) 1);
    1.48 -by Auto_tac;  
    1.49 -qed "natify_0";
    1.50 -Addsimps [natify_0];
    1.51 -
    1.52 -Goal "ALL z. x ~= succ(z) ==> natify(x) = 0";
    1.53 -by (rtac (natify_def RS def_Vrecursor RS trans) 1);
    1.54 -by Auto_tac;  
    1.55 -qed "natify_non_succ";
    1.56 -
    1.57 -Goal "natify(x) : nat";
    1.58 -by (eps_ind_tac "x" 1);
    1.59 -by (case_tac "EX z. x1 = succ(z)" 1);
    1.60 -by (auto_tac (claset(), simpset() addsimps [natify_succ, natify_non_succ]));  
    1.61 -qed "natify_in_nat";
    1.62 -AddIffs [natify_in_nat];
    1.63 -AddTCs [natify_in_nat];
    1.64 -
    1.65 -Goal "n : nat ==> natify(n) = n";
    1.66 -by (induct_tac "n" 1);
    1.67 -by (auto_tac (claset(), simpset() addsimps [natify_succ]));  
    1.68 -qed "natify_ident";
    1.69 -Addsimps [natify_ident];
    1.70 -
    1.71 -Goal "[|natify(x) = y;  x: nat|] ==> x=y";
    1.72 -by Auto_tac; 
    1.73 -qed "natify_eqE";
    1.74 -
    1.75 -
    1.76 -(*** Collapsing rules: to remove natify from arithmetic expressions ***)
    1.77 -
    1.78 -Goal "natify(natify(x)) = natify(x)";
    1.79 -by (Simp_tac 1);
    1.80 -qed "natify_idem";
    1.81 -Addsimps [natify_idem];
    1.82 -
    1.83 -(** Addition **)
    1.84 -
    1.85 -Goal "natify(m) #+ n = m #+ n";
    1.86 -by (simp_tac (simpset() addsimps [add_def]) 1);
    1.87 -qed "add_natify1";
    1.88 -
    1.89 -Goal "m #+ natify(n) = m #+ n";
    1.90 -by (simp_tac (simpset() addsimps [add_def]) 1);
    1.91 -qed "add_natify2";
    1.92 -Addsimps [add_natify1, add_natify2];
    1.93 -
    1.94 -(** Multiplication **)
    1.95 -
    1.96 -Goal "natify(m) #* n = m #* n";
    1.97 -by (simp_tac (simpset() addsimps [mult_def]) 1);
    1.98 -qed "mult_natify1";
    1.99 -
   1.100 -Goal "m #* natify(n) = m #* n";
   1.101 -by (simp_tac (simpset() addsimps [mult_def]) 1);
   1.102 -qed "mult_natify2";
   1.103 -Addsimps [mult_natify1, mult_natify2];
   1.104 -
   1.105 -(** Difference **)
   1.106 -
   1.107 -Goal "natify(m) #- n = m #- n";
   1.108 -by (simp_tac (simpset() addsimps [diff_def]) 1);
   1.109 -qed "diff_natify1";
   1.110 -
   1.111 -Goal "m #- natify(n) = m #- n";
   1.112 -by (simp_tac (simpset() addsimps [diff_def]) 1);
   1.113 -qed "diff_natify2";
   1.114 -Addsimps [diff_natify1, diff_natify2];
   1.115 -
   1.116 -(** Remainder **)
   1.117 -
   1.118 -Goal "natify(m) mod n = m mod n";
   1.119 -by (simp_tac (simpset() addsimps [mod_def]) 1);
   1.120 -qed "mod_natify1";
   1.121 -
   1.122 -Goal "m mod natify(n) = m mod n";
   1.123 -by (simp_tac (simpset() addsimps [mod_def]) 1);
   1.124 -qed "mod_natify2";
   1.125 -Addsimps [mod_natify1, mod_natify2];
   1.126 -
   1.127 -(** Quotient **)
   1.128 -
   1.129 -Goal "natify(m) div n = m div n";
   1.130 -by (simp_tac (simpset() addsimps [div_def]) 1);
   1.131 -qed "div_natify1";
   1.132 -
   1.133 -Goal "m div natify(n) = m div n";
   1.134 -by (simp_tac (simpset() addsimps [div_def]) 1);
   1.135 -qed "div_natify2";
   1.136 -Addsimps [div_natify1, div_natify2];
   1.137 -
   1.138 -
   1.139 -(*** Typing rules ***)
   1.140 -
   1.141 -(** Addition **)
   1.142 -
   1.143 -Goal "[| m:nat;  n:nat |] ==> raw_add (m, n) : nat";
   1.144 -by (induct_tac "m" 1);
   1.145 -by Auto_tac;
   1.146 -qed "raw_add_type";
   1.147 -
   1.148 -Goal "m #+ n : nat";
   1.149 -by (simp_tac (simpset() addsimps [add_def, raw_add_type]) 1);
   1.150 -qed "add_type";
   1.151 -AddIffs [add_type];
   1.152 -AddTCs [add_type];
   1.153 -
   1.154 -(** Multiplication **)
   1.155 -
   1.156 -Goal "[| m:nat;  n:nat |] ==> raw_mult (m, n) : nat";
   1.157 -by (induct_tac "m" 1);
   1.158 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [raw_add_type])));
   1.159 -qed "raw_mult_type";
   1.160 -
   1.161 -Goal "m #* n : nat";
   1.162 -by (simp_tac (simpset() addsimps [mult_def, raw_mult_type]) 1);
   1.163 -qed "mult_type";
   1.164 -AddIffs [mult_type];
   1.165 -AddTCs [mult_type];
   1.166 -
   1.167 -
   1.168 -(** Difference **)
   1.169 -
   1.170 -Goal "[| m:nat;  n:nat |] ==> raw_diff (m, n) : nat";
   1.171 -by (induct_tac "n" 1);
   1.172 -by Auto_tac;
   1.173 -by (fast_tac (claset() addIs [nat_case_type]) 1);
   1.174 -qed "raw_diff_type";
   1.175 -
   1.176 -Goal "m #- n : nat";
   1.177 -by (simp_tac (simpset() addsimps [diff_def, raw_diff_type]) 1);
   1.178 -qed "diff_type";
   1.179 -AddIffs [diff_type];
   1.180 -AddTCs [diff_type];
   1.181 -
   1.182 -Goalw [diff_def] "0 #- n = 0";
   1.183 -by (rtac (natify_in_nat RS nat_induct) 1);
   1.184 -by Auto_tac;
   1.185 -qed "diff_0_eq_0";
   1.186 -
   1.187 -(*Must simplify BEFORE the induction: else we get a critical pair*)
   1.188 -Goal "succ(m) #- succ(n) = m #- n";
   1.189 -by (simp_tac (simpset() addsimps [natify_succ, diff_def]) 1);
   1.190 -by (res_inst_tac [("x1","n")] (natify_in_nat RS nat_induct) 1);
   1.191 -by Auto_tac;
   1.192 -qed "diff_succ_succ";
   1.193 -
   1.194 -(*This defining property is no longer wanted*)
   1.195 -Delsimps [raw_diff_succ];  
   1.196 -
   1.197 -(*Natify has weakened this law, compared with the older approach*)
   1.198 -Goal "m #- 0 = natify(m)";
   1.199 -by (asm_simp_tac (simpset() addsimps [diff_def]) 1);
   1.200 -qed "diff_0";
   1.201 -
   1.202 -Addsimps [diff_0, diff_0_eq_0, diff_succ_succ];
   1.203 -
   1.204 -Goal "m:nat ==> (m #- n) le m";
   1.205 -by (subgoal_tac "(m #- natify(n)) le m" 1);
   1.206 -by (res_inst_tac [("m","m"), ("n","natify(n)")] diff_induct 2);
   1.207 -by (etac leE 6);
   1.208 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [le_iff])));
   1.209 -qed "diff_le_self";
   1.210 -
   1.211 -
   1.212 -(*** Addition ***)
   1.213 -
   1.214 -(*Natify has weakened this law, compared with the older approach*)
   1.215 -Goal "0 #+ m = natify(m)";
   1.216 -by (asm_simp_tac (simpset() addsimps [add_def]) 1);
   1.217 -qed "add_0_natify";
   1.218 -
   1.219 -Goal "succ(m) #+ n = succ(m #+ n)";
   1.220 -by (asm_simp_tac (simpset() addsimps [natify_succ, add_def]) 1);
   1.221 -qed "add_succ";
   1.222 -
   1.223 -Addsimps [add_0_natify, add_succ];
   1.224 -
   1.225 -Goal "m: nat ==> 0 #+ m = m";
   1.226 -by (Asm_simp_tac 1);
   1.227 -qed "add_0";
   1.228 -
   1.229 -(*Associative law for addition*)
   1.230 -Goal "(m #+ n) #+ k = m #+ (n #+ k)";
   1.231 -by (subgoal_tac "(natify(m) #+ natify(n)) #+ natify(k) = \
   1.232 -\                natify(m) #+ (natify(n) #+ natify(k))" 1);
   1.233 -by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   1.234 -by Auto_tac;
   1.235 -qed "add_assoc";
   1.236 -
   1.237 -(*The following two lemmas are used for add_commute and sometimes
   1.238 -  elsewhere, since they are safe for rewriting.*)
   1.239 -Goal "m #+ 0 = natify(m)";
   1.240 -by (subgoal_tac "natify(m) #+ 0 = natify(m)" 1);
   1.241 -by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   1.242 -by Auto_tac;
   1.243 -qed "add_0_right_natify";
   1.244 -
   1.245 -Goalw [add_def] "m #+ succ(n) = succ(m #+ n)";
   1.246 -by (res_inst_tac [("n","natify(m)")] nat_induct 1);
   1.247 -by (auto_tac (claset(), simpset() addsimps [natify_succ]));  
   1.248 -qed "add_succ_right";
   1.249 -
   1.250 -Addsimps [add_0_right_natify, add_succ_right];
   1.251 -
   1.252 -Goal "m: nat ==> m #+ 0 = m";
   1.253 -by Auto_tac;
   1.254 -qed "add_0_right";
   1.255 -
   1.256 -(*Commutative law for addition*)  
   1.257 -Goal "m #+ n = n #+ m";
   1.258 -by (subgoal_tac "natify(m) #+ natify(n) = natify(n) #+ natify(m)" 1);
   1.259 -by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   1.260 -by Auto_tac;
   1.261 -qed "add_commute";
   1.262 -
   1.263 -(*for a/c rewriting*)
   1.264 -Goal "m#+(n#+k)=n#+(m#+k)";
   1.265 -by (rtac (add_commute RS trans) 1);
   1.266 -by (rtac (add_assoc RS trans) 1);
   1.267 -by (rtac (add_commute RS subst_context) 1);
   1.268 -qed "add_left_commute";
   1.269 -
   1.270 -(*Addition is an AC-operator*)
   1.271 -bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
   1.272 -
   1.273 -(*Cancellation law on the left*)
   1.274 -Goal "[| raw_add(k, m) = raw_add(k, n);  k:nat |] ==> m=n";
   1.275 -by (etac rev_mp 1);
   1.276 -by (induct_tac "k" 1);
   1.277 -by Auto_tac;
   1.278 -qed "raw_add_left_cancel";
   1.279 -
   1.280 -Goalw [add_def] "k #+ m = k #+ n ==> natify(m) = natify(n)";
   1.281 -by (dtac raw_add_left_cancel 1);
   1.282 -by Auto_tac;
   1.283 -qed "add_left_cancel_natify";
   1.284 -
   1.285 -Goal "[| i = j;  i #+ m = j #+ n;  m:nat;  n:nat |] ==> m = n";
   1.286 -by (force_tac (claset() addSDs [add_left_cancel_natify], simpset()) 1);
   1.287 -qed "add_left_cancel";
   1.288 -
   1.289 -(*Thanks to Sten Agerholm*)
   1.290 -Goal "k#+m le k#+n ==> natify(m) le natify(n)";
   1.291 -by (res_inst_tac [("P", "natify(k)#+m le natify(k)#+n")] rev_mp 1);
   1.292 -by (res_inst_tac [("n","natify(k)")] nat_induct 2);
   1.293 -by Auto_tac;
   1.294 -qed "add_le_elim1_natify";
   1.295 -
   1.296 -Goal "[| k#+m le k#+n; m: nat; n: nat |] ==> m le n";
   1.297 -by (dtac add_le_elim1_natify 1);
   1.298 -by Auto_tac;
   1.299 -qed "add_le_elim1";
   1.300 -
   1.301 -Goal "k#+m < k#+n ==> natify(m) < natify(n)";
   1.302 -by (res_inst_tac [("P", "natify(k)#+m < natify(k)#+n")] rev_mp 1);
   1.303 -by (res_inst_tac [("n","natify(k)")] nat_induct 2);
   1.304 -by Auto_tac;
   1.305 -qed "add_lt_elim1_natify";
   1.306 -
   1.307 -Goal "[| k#+m < k#+n; m: nat; n: nat |] ==> m < n";
   1.308 -by (dtac add_lt_elim1_natify 1);
   1.309 -by Auto_tac;
   1.310 -qed "add_lt_elim1";
   1.311 -
   1.312 -
   1.313 -(*** Monotonicity of Addition ***)
   1.314 -
   1.315 -(*strict, in 1st argument; proof is by rule induction on 'less than'.
   1.316 -  Still need j:nat, for consider j = omega.  Then we can have i<omega,
   1.317 -  which is the same as i:nat, but natify(j)=0, so the conclusion fails.*)
   1.318 -Goal "[| i<j; j:nat |] ==> i#+k < j#+k";
   1.319 -by (ftac lt_nat_in_nat 1);
   1.320 -by (assume_tac 1);
   1.321 -by (etac succ_lt_induct 1);
   1.322 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI])));
   1.323 -qed "add_lt_mono1";
   1.324 -
   1.325 -(*strict, in both arguments*)
   1.326 -Goal "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
   1.327 -by (rtac (add_lt_mono1 RS lt_trans) 1);
   1.328 -by (REPEAT (assume_tac 1));
   1.329 -by (EVERY [stac add_commute 1,
   1.330 -           stac add_commute 1,
   1.331 -           rtac add_lt_mono1 1]);
   1.332 -by (REPEAT (assume_tac 1));
   1.333 -qed "add_lt_mono";
   1.334 -
   1.335 -(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
   1.336 -val lt_mono::ford::prems = Goal
   1.337 -     "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
   1.338 -\        !!i. i:k ==> Ord(f(i));                \
   1.339 -\        i le j;  j:k                           \
   1.340 -\     |] ==> f(i) le f(j)";
   1.341 -by (cut_facts_tac prems 1);
   1.342 -by (blast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
   1.343 -qed "Ord_lt_mono_imp_le_mono";
   1.344 -
   1.345 -(*le monotonicity, 1st argument*)
   1.346 -Goal "[| i le j; j:nat |] ==> i#+k le j#+k";
   1.347 -by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1);
   1.348 -by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1));
   1.349 -qed "add_le_mono1";
   1.350 -
   1.351 -(* le monotonicity, BOTH arguments*)
   1.352 -Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
   1.353 -by (rtac (add_le_mono1 RS le_trans) 1);
   1.354 -by (REPEAT (assume_tac 1));
   1.355 -by (EVERY [stac add_commute 1,
   1.356 -           stac add_commute 1,
   1.357 -           rtac add_le_mono1 1]);
   1.358 -by (REPEAT (assume_tac 1));
   1.359 -qed "add_le_mono";
   1.360 -
   1.361 -(** Subtraction is the inverse of addition. **)
   1.362 -
   1.363 -Goal "(n#+m) #- n = natify(m)";
   1.364 -by (subgoal_tac "(natify(n) #+ m) #- natify(n) = natify(m)" 1);
   1.365 -by (res_inst_tac [("n","natify(n)")] nat_induct 2);
   1.366 -by Auto_tac;
   1.367 -qed "diff_add_inverse";
   1.368 -
   1.369 -Goal "(m#+n) #- n = natify(m)";
   1.370 -by (simp_tac (simpset() addsimps [inst "m" "m" add_commute, 
   1.371 -				  diff_add_inverse]) 1);
   1.372 -qed "diff_add_inverse2";
   1.373 -
   1.374 -Goal "(k#+m) #- (k#+n) = m #- n";
   1.375 -by (subgoal_tac "(natify(k) #+ natify(m)) #- (natify(k) #+ natify(n)) = \
   1.376 -\                natify(m) #- natify(n)" 1);
   1.377 -by (res_inst_tac [("n","natify(k)")] nat_induct 2);
   1.378 -by Auto_tac;
   1.379 -qed "diff_cancel";
   1.380 -
   1.381 -Goal "(m#+k) #- (n#+k) = m #- n";
   1.382 -by (simp_tac (simpset() addsimps [inst "n" "k" add_commute, diff_cancel]) 1);
   1.383 -qed "diff_cancel2";
   1.384 -
   1.385 -Goal "n #- (n#+m) = 0";
   1.386 -by (subgoal_tac "natify(n) #- (natify(n) #+ natify(m)) = 0" 1);
   1.387 -by (res_inst_tac [("n","natify(n)")] nat_induct 2);
   1.388 -by Auto_tac;
   1.389 -qed "diff_add_0";
   1.390 -
   1.391 -
   1.392 -(** Lemmas for the CancelNumerals simproc **)
   1.393 -
   1.394 -Goal "(u #+ m = u #+ n) <-> (0 #+ m = natify(n))";
   1.395 -by Auto_tac;  
   1.396 -by (blast_tac (claset() addDs [add_left_cancel_natify]) 1);
   1.397 -by (asm_full_simp_tac (simpset() addsimps [add_def]) 1);
   1.398 -qed "eq_add_iff";
   1.399 -
   1.400 -Goal "(u #+ m < u #+ n) <-> (0 #+ m < natify(n))";
   1.401 -by (auto_tac (claset(), simpset() addsimps [add_lt_elim1_natify]));
   1.402 -by (dtac add_lt_mono1 1);
   1.403 -by (auto_tac (claset(), simpset() addsimps [inst "m" "u" add_commute]));
   1.404 -qed "less_add_iff";
   1.405 -
   1.406 -Goal "((u #+ m) #- (u #+ n)) = ((0 #+ m) #- n)";
   1.407 -by (asm_simp_tac (simpset() addsimps [diff_cancel]) 1);
   1.408 -qed "diff_add_eq";
   1.409 -
   1.410 -(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
   1.411 -Goal "u = u' ==> (t==u) == (t==u')";
   1.412 -by Auto_tac;
   1.413 -qed "eq_cong2";
   1.414 -
   1.415 -Goal "u <-> u' ==> (t==u) == (t==u')";
   1.416 -by Auto_tac;
   1.417 -qed "iff_cong2";
   1.418 -
   1.419 -
   1.420 -(*** Multiplication [the simprocs need these laws] ***)
   1.421 -
   1.422 -Goal "0 #* m = 0";
   1.423 -by (simp_tac (simpset() addsimps [mult_def]) 1);
   1.424 -qed "mult_0";
   1.425 -
   1.426 -Goal "succ(m) #* n = n #+ (m #* n)";
   1.427 -by (simp_tac (simpset() addsimps [add_def, mult_def, natify_succ, 
   1.428 -                                  raw_mult_type]) 1);
   1.429 -qed "mult_succ";
   1.430 -
   1.431 -Addsimps [mult_0, mult_succ];
   1.432 -
   1.433 -(*right annihilation in product*)
   1.434 -Goalw [mult_def] "m #* 0 = 0";
   1.435 -by (res_inst_tac [("n","natify(m)")] nat_induct 1);
   1.436 -by Auto_tac;
   1.437 -qed "mult_0_right";
   1.438 -
   1.439 -(*right successor law for multiplication*)
   1.440 -Goal "m #* succ(n) = m #+ (m #* n)";
   1.441 -by (subgoal_tac "natify(m) #* succ(natify(n)) = \
   1.442 -\                natify(m) #+ (natify(m) #* natify(n))" 1);
   1.443 -by (full_simp_tac (simpset() addsimps [natify_succ, add_def, mult_def]) 1);
   1.444 -by (res_inst_tac [("n","natify(m)")] nat_induct 1);
   1.445 -by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
   1.446 -qed "mult_succ_right";
   1.447 -
   1.448 -Addsimps [mult_0_right, mult_succ_right];
   1.449 -
   1.450 -Goal "1 #* n = natify(n)";
   1.451 -by Auto_tac;
   1.452 -qed "mult_1_natify";
   1.453 -
   1.454 -Goal "n #* 1 = natify(n)";
   1.455 -by Auto_tac;
   1.456 -qed "mult_1_right_natify";
   1.457 -
   1.458 -Addsimps [mult_1_natify, mult_1_right_natify];
   1.459 -
   1.460 -Goal "n : nat ==> 1 #* n = n";
   1.461 -by (Asm_simp_tac 1);
   1.462 -qed "mult_1";
   1.463 -
   1.464 -Goal "n : nat ==> n #* 1 = n";
   1.465 -by (Asm_simp_tac 1);
   1.466 -qed "mult_1_right";
   1.467 -
   1.468 -(*Commutative law for multiplication*)
   1.469 -Goal "m #* n = n #* m";
   1.470 -by (subgoal_tac "natify(m) #* natify(n) = natify(n) #* natify(m)" 1);
   1.471 -by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   1.472 -by Auto_tac;
   1.473 -qed "mult_commute";
   1.474 -
   1.475 -(*addition distributes over multiplication*)
   1.476 -Goal "(m #+ n) #* k = (m #* k) #+ (n #* k)";
   1.477 -by (subgoal_tac "(natify(m) #+ natify(n)) #* natify(k) = \
   1.478 -\                (natify(m) #* natify(k)) #+ (natify(n) #* natify(k))" 1);
   1.479 -by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   1.480 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_assoc RS sym])));
   1.481 -qed "add_mult_distrib";
   1.482 -
   1.483 -(*Distributive law on the left*)
   1.484 -Goal "k #* (m #+ n) = (k #* m) #+ (k #* n)";
   1.485 -by (subgoal_tac "natify(k) #* (natify(m) #+ natify(n)) = \
   1.486 -\                (natify(k) #* natify(m)) #+ (natify(k) #* natify(n))" 1);
   1.487 -by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   1.488 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
   1.489 -qed "add_mult_distrib_left";
   1.490 -
   1.491 -(*Associative law for multiplication*)
   1.492 -Goal "(m #* n) #* k = m #* (n #* k)";
   1.493 -by (subgoal_tac "(natify(m) #* natify(n)) #* natify(k) = \
   1.494 -\                natify(m) #* (natify(n) #* natify(k))" 1);
   1.495 -by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   1.496 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_mult_distrib])));
   1.497 -qed "mult_assoc";
   1.498 -
   1.499 -(*for a/c rewriting*)
   1.500 -Goal "m #* (n #* k) = n #* (m #* k)";
   1.501 -by (rtac (mult_commute RS trans) 1);
   1.502 -by (rtac (mult_assoc RS trans) 1);
   1.503 -by (rtac (mult_commute RS subst_context) 1);
   1.504 -qed "mult_left_commute";
   1.505 -
   1.506 -bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
   1.507 -
   1.508 -
   1.509 -Goal "[| m:nat; n:nat |] \
   1.510 -\     ==> (m < succ(n)) <-> (m = 0 | (EX j:nat. m = succ(j) & j < n))";
   1.511 -by (induct_tac "m" 1);
   1.512 -by Auto_tac;
   1.513 -qed "lt_succ_eq_0_disj";
   1.514 -
   1.515 -Goal "[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)";
   1.516 -by (eres_inst_tac [("m", "k")] diff_induct  1);
   1.517 -by Auto_tac;
   1.518 -qed_spec_mp "less_diff_conv";
   1.519 -
     2.1 --- a/src/ZF/Arith.thy	Fri May 17 16:54:25 2002 +0200
     2.2 +++ b/src/ZF/Arith.thy	Sat May 18 20:08:17 2002 +0200
     2.3 @@ -4,62 +4,581 @@
     2.4      Copyright   1992  University of Cambridge
     2.5  
     2.6  Arithmetic operators and their definitions
     2.7 +
     2.8 +Proofs about elementary arithmetic: addition, multiplication, etc.
     2.9  *)
    2.10  
    2.11 -Arith = Univ + 
    2.12 +(*"Difference" is subtraction of natural numbers.
    2.13 +  There are no negative numbers; we have
    2.14 +     m #- n = 0  iff  m<=n   and     m #- n = succ(k) iff m>n.
    2.15 +  Also, rec(m, 0, %z w.z) is pred(m).   
    2.16 +*)
    2.17 +
    2.18 +theory Arith = Univ:
    2.19  
    2.20  constdefs
    2.21 -  pred   :: i=>i    (*inverse of succ*)
    2.22 +  pred   :: "i=>i"    (*inverse of succ*)
    2.23      "pred(y) == THE x. y = succ(x)"
    2.24  
    2.25 -  natify :: i=>i    (*coerces non-nats to nats*)
    2.26 +  natify :: "i=>i"    (*coerces non-nats to nats*)
    2.27      "natify == Vrecursor(%f a. if a = succ(pred(a)) then succ(f`pred(a))
    2.28                                                      else 0)"
    2.29  
    2.30  consts
    2.31 -    raw_add, raw_diff, raw_mult  :: [i,i]=>i
    2.32 +  raw_add  :: "[i,i]=>i"
    2.33 +  raw_diff  :: "[i,i]=>i"
    2.34 +  raw_mult  :: "[i,i]=>i"
    2.35  
    2.36  primrec
    2.37    "raw_add (0, n) = n"
    2.38    "raw_add (succ(m), n) = succ(raw_add(m, n))"
    2.39  
    2.40  primrec
    2.41 -  raw_diff_0     "raw_diff(m, 0) = m"
    2.42 -  raw_diff_succ  "raw_diff(m, succ(n)) = 
    2.43 -                    nat_case(0, %x. x, raw_diff(m, n))"
    2.44 +  raw_diff_0:     "raw_diff(m, 0) = m"
    2.45 +  raw_diff_succ:  "raw_diff(m, succ(n)) =
    2.46 +                     nat_case(0, %x. x, raw_diff(m, n))"
    2.47  
    2.48  primrec
    2.49    "raw_mult(0, n) = 0"
    2.50    "raw_mult(succ(m), n) = raw_add (n, raw_mult(m, n))"
    2.51 - 
    2.52 +
    2.53  constdefs
    2.54 -  add :: [i,i]=>i                    (infixl "#+" 65)
    2.55 +  add :: "[i,i]=>i"                    (infixl "#+" 65)
    2.56      "m #+ n == raw_add (natify(m), natify(n))"
    2.57  
    2.58 -  diff :: [i,i]=>i                    (infixl "#-" 65)
    2.59 +  diff :: "[i,i]=>i"                    (infixl "#-" 65)
    2.60      "m #- n == raw_diff (natify(m), natify(n))"
    2.61  
    2.62 -  mult :: [i,i]=>i                    (infixl "#*" 70)
    2.63 +  mult :: "[i,i]=>i"                    (infixl "#*" 70)
    2.64      "m #* n == raw_mult (natify(m), natify(n))"
    2.65  
    2.66 -  raw_div  :: [i,i]=>i
    2.67 -    "raw_div (m, n) == 
    2.68 +  raw_div  :: "[i,i]=>i"
    2.69 +    "raw_div (m, n) ==
    2.70         transrec(m, %j f. if j<n | n=0 then 0 else succ(f`(j#-n)))"
    2.71  
    2.72 -  raw_mod  :: [i,i]=>i
    2.73 -    "raw_mod (m, n) == 
    2.74 +  raw_mod  :: "[i,i]=>i"
    2.75 +    "raw_mod (m, n) ==
    2.76         transrec(m, %j f. if j<n | n=0 then j else f`(j#-n))"
    2.77  
    2.78 -  div  :: [i,i]=>i                    (infixl "div" 70) 
    2.79 +  div  :: "[i,i]=>i"                    (infixl "div" 70)
    2.80      "m div n == raw_div (natify(m), natify(n))"
    2.81  
    2.82 -  mod  :: [i,i]=>i                    (infixl "mod" 70)
    2.83 +  mod  :: "[i,i]=>i"                    (infixl "mod" 70)
    2.84      "m mod n == raw_mod (natify(m), natify(n))"
    2.85  
    2.86  syntax (xsymbols)
    2.87 -  "mult"      :: [i, i] => i               (infixr "#\\<times>" 70)
    2.88 +  "mult"      :: "[i,i] => i"               (infixr "#\<times>" 70)
    2.89  
    2.90  syntax (HTML output)
    2.91 -  "mult"      :: [i, i] => i               (infixr "#\\<times>" 70)
    2.92 +  "mult"      :: "[i, i] => i"               (infixr "#\<times>" 70)
    2.93 +
    2.94 +
    2.95 +declare rec_type [simp]
    2.96 +        nat_0_le [simp]
    2.97 +
    2.98 +
    2.99 +lemma zero_lt_lemma: "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)"
   2.100 +apply (erule rev_mp)
   2.101 +apply (induct_tac "k", auto)
   2.102 +done
   2.103 +
   2.104 +(* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
   2.105 +lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard]
   2.106 +
   2.107 +
   2.108 +(** natify: coercion to "nat" **)
   2.109 +
   2.110 +lemma pred_succ_eq [simp]: "pred(succ(y)) = y"
   2.111 +by (unfold pred_def, auto)
   2.112 +
   2.113 +lemma natify_succ: "natify(succ(x)) = succ(natify(x))"
   2.114 +by (rule natify_def [THEN def_Vrecursor, THEN trans], auto)
   2.115 +
   2.116 +lemma natify_0 [simp]: "natify(0) = 0"
   2.117 +by (rule natify_def [THEN def_Vrecursor, THEN trans], auto)
   2.118 +
   2.119 +lemma natify_non_succ: "ALL z. x ~= succ(z) ==> natify(x) = 0"
   2.120 +by (rule natify_def [THEN def_Vrecursor, THEN trans], auto)
   2.121 +
   2.122 +lemma natify_in_nat [iff,TC]: "natify(x) : nat"
   2.123 +apply (rule_tac a=x in eps_induct)
   2.124 +apply (case_tac "EX z. x = succ(z)")
   2.125 +apply (auto simp add: natify_succ natify_non_succ)
   2.126 +done
   2.127 +
   2.128 +lemma natify_ident [simp]: "n : nat ==> natify(n) = n"
   2.129 +apply (induct_tac "n")
   2.130 +apply (auto simp add: natify_succ)
   2.131 +done
   2.132 +
   2.133 +lemma natify_eqE: "[|natify(x) = y;  x: nat|] ==> x=y"
   2.134 +by auto
   2.135 +
   2.136 +
   2.137 +(*** Collapsing rules: to remove natify from arithmetic expressions ***)
   2.138 +
   2.139 +lemma natify_idem [simp]: "natify(natify(x)) = natify(x)"
   2.140 +by simp
   2.141 +
   2.142 +(** Addition **)
   2.143 +
   2.144 +lemma add_natify1 [simp]: "natify(m) #+ n = m #+ n"
   2.145 +by (simp add: add_def)
   2.146 +
   2.147 +lemma add_natify2 [simp]: "m #+ natify(n) = m #+ n"
   2.148 +by (simp add: add_def)
   2.149 +
   2.150 +(** Multiplication **)
   2.151 +
   2.152 +lemma mult_natify1 [simp]: "natify(m) #* n = m #* n"
   2.153 +by (simp add: mult_def)
   2.154 +
   2.155 +lemma mult_natify2 [simp]: "m #* natify(n) = m #* n"
   2.156 +by (simp add: mult_def)
   2.157 +
   2.158 +(** Difference **)
   2.159 +
   2.160 +lemma diff_natify1 [simp]: "natify(m) #- n = m #- n"
   2.161 +by (simp add: diff_def)
   2.162 +
   2.163 +lemma diff_natify2 [simp]: "m #- natify(n) = m #- n"
   2.164 +by (simp add: diff_def)
   2.165 +
   2.166 +(** Remainder **)
   2.167 +
   2.168 +lemma mod_natify1 [simp]: "natify(m) mod n = m mod n"
   2.169 +by (simp add: mod_def)
   2.170 +
   2.171 +lemma mod_natify2 [simp]: "m mod natify(n) = m mod n"
   2.172 +by (simp add: mod_def)
   2.173 +
   2.174 +
   2.175 +(** Quotient **)
   2.176 +
   2.177 +lemma div_natify1 [simp]: "natify(m) div n = m div n"
   2.178 +by (simp add: div_def)
   2.179 +
   2.180 +lemma div_natify2 [simp]: "m div natify(n) = m div n"
   2.181 +by (simp add: div_def)
   2.182 +
   2.183 +
   2.184 +(*** Typing rules ***)
   2.185 +
   2.186 +(** Addition **)
   2.187 +
   2.188 +lemma raw_add_type: "[| m:nat;  n:nat |] ==> raw_add (m, n) : nat"
   2.189 +by (induct_tac "m", auto)
   2.190 +
   2.191 +lemma add_type [iff,TC]: "m #+ n : nat"
   2.192 +by (simp add: add_def raw_add_type)
   2.193 +
   2.194 +(** Multiplication **)
   2.195 +
   2.196 +lemma raw_mult_type: "[| m:nat;  n:nat |] ==> raw_mult (m, n) : nat"
   2.197 +apply (induct_tac "m")
   2.198 +apply (simp_all add: raw_add_type)
   2.199 +done
   2.200 +
   2.201 +lemma mult_type [iff,TC]: "m #* n : nat"
   2.202 +by (simp add: mult_def raw_mult_type)
   2.203 +
   2.204 +
   2.205 +(** Difference **)
   2.206 +
   2.207 +lemma raw_diff_type: "[| m:nat;  n:nat |] ==> raw_diff (m, n) : nat"
   2.208 +apply (induct_tac "n", auto)
   2.209 +apply (fast intro: nat_case_type)
   2.210 +done
   2.211 +
   2.212 +lemma diff_type [iff,TC]: "m #- n : nat"
   2.213 +by (simp add: diff_def raw_diff_type)
   2.214 +
   2.215 +lemma diff_0_eq_0 [simp]: "0 #- n = 0"
   2.216 +apply (unfold diff_def)
   2.217 +apply (rule natify_in_nat [THEN nat_induct], auto)
   2.218 +done
   2.219 +
   2.220 +(*Must simplify BEFORE the induction: else we get a critical pair*)
   2.221 +lemma diff_succ_succ [simp]: "succ(m) #- succ(n) = m #- n"
   2.222 +apply (simp add: natify_succ diff_def)
   2.223 +apply (rule_tac x1 = "n" in natify_in_nat [THEN nat_induct], auto)
   2.224 +done
   2.225 +
   2.226 +(*This defining property is no longer wanted*)
   2.227 +declare raw_diff_succ [simp del]
   2.228 +
   2.229 +(*Natify has weakened this law, compared with the older approach*)
   2.230 +lemma diff_0 [simp]: "m #- 0 = natify(m)"
   2.231 +by (simp add: diff_def)
   2.232 +
   2.233 +lemma diff_le_self: "m:nat ==> (m #- n) le m"
   2.234 +apply (subgoal_tac " (m #- natify (n)) le m")
   2.235 +apply (rule_tac [2] m = "m" and n = "natify (n) " in diff_induct)
   2.236 +apply (erule_tac [6] leE)
   2.237 +apply (simp_all add: le_iff)
   2.238 +done
   2.239 +
   2.240 +
   2.241 +(*** Addition ***)
   2.242 +
   2.243 +(*Natify has weakened this law, compared with the older approach*)
   2.244 +lemma add_0_natify [simp]: "0 #+ m = natify(m)"
   2.245 +by (simp add: add_def)
   2.246 +
   2.247 +lemma add_succ [simp]: "succ(m) #+ n = succ(m #+ n)"
   2.248 +by (simp add: natify_succ add_def)
   2.249 +
   2.250 +lemma add_0: "m: nat ==> 0 #+ m = m"
   2.251 +by simp
   2.252 +
   2.253 +(*Associative law for addition*)
   2.254 +lemma add_assoc: "(m #+ n) #+ k = m #+ (n #+ k)"
   2.255 +apply (subgoal_tac "(natify(m) #+ natify(n)) #+ natify(k) =
   2.256 +                    natify(m) #+ (natify(n) #+ natify(k))")
   2.257 +apply (rule_tac [2] n = "natify(m)" in nat_induct)
   2.258 +apply auto
   2.259 +done
   2.260 +
   2.261 +(*The following two lemmas are used for add_commute and sometimes
   2.262 +  elsewhere, since they are safe for rewriting.*)
   2.263 +lemma add_0_right_natify [simp]: "m #+ 0 = natify(m)"
   2.264 +apply (subgoal_tac "natify(m) #+ 0 = natify(m)")
   2.265 +apply (rule_tac [2] n = "natify(m)" in nat_induct)
   2.266 +apply auto
   2.267 +done
   2.268 +
   2.269 +lemma add_succ_right [simp]: "m #+ succ(n) = succ(m #+ n)"
   2.270 +apply (unfold add_def)
   2.271 +apply (rule_tac n = "natify(m) " in nat_induct)
   2.272 +apply (auto simp add: natify_succ)
   2.273 +done
   2.274 +
   2.275 +lemma add_0_right: "m: nat ==> m #+ 0 = m"
   2.276 +by auto
   2.277 +
   2.278 +(*Commutative law for addition*)
   2.279 +lemma add_commute: "m #+ n = n #+ m"
   2.280 +apply (subgoal_tac "natify(m) #+ natify(n) = natify(n) #+ natify(m) ")
   2.281 +apply (rule_tac [2] n = "natify(m) " in nat_induct)
   2.282 +apply auto
   2.283 +done
   2.284 +
   2.285 +(*for a/c rewriting*)
   2.286 +lemma add_left_commute: "m#+(n#+k)=n#+(m#+k)"
   2.287 +apply (rule add_commute [THEN trans])
   2.288 +apply (rule add_assoc [THEN trans])
   2.289 +apply (rule add_commute [THEN subst_context])
   2.290 +done
   2.291 +
   2.292 +(*Addition is an AC-operator*)
   2.293 +lemmas add_ac = add_assoc add_commute add_left_commute
   2.294 +
   2.295 +(*Cancellation law on the left*)
   2.296 +lemma raw_add_left_cancel:
   2.297 +     "[| raw_add(k, m) = raw_add(k, n);  k:nat |] ==> m=n"
   2.298 +apply (erule rev_mp)
   2.299 +apply (induct_tac "k", auto)
   2.300 +done
   2.301 +
   2.302 +lemma add_left_cancel_natify: "k #+ m = k #+ n ==> natify(m) = natify(n)"
   2.303 +apply (unfold add_def)
   2.304 +apply (drule raw_add_left_cancel, auto)
   2.305 +done
   2.306 +
   2.307 +lemma add_left_cancel:
   2.308 +     "[| i = j;  i #+ m = j #+ n;  m:nat;  n:nat |] ==> m = n"
   2.309 +by (force dest!: add_left_cancel_natify)
   2.310 +
   2.311 +(*Thanks to Sten Agerholm*)
   2.312 +lemma add_le_elim1_natify: "k#+m le k#+n ==> natify(m) le natify(n)"
   2.313 +apply (rule_tac P = "natify(k) #+m le natify(k) #+n" in rev_mp)
   2.314 +apply (rule_tac [2] n = "natify(k) " in nat_induct)
   2.315 +apply auto
   2.316 +done
   2.317 +
   2.318 +lemma add_le_elim1: "[| k#+m le k#+n; m: nat; n: nat |] ==> m le n"
   2.319 +by (drule add_le_elim1_natify, auto)
   2.320 +
   2.321 +lemma add_lt_elim1_natify: "k#+m < k#+n ==> natify(m) < natify(n)"
   2.322 +apply (rule_tac P = "natify(k) #+m < natify(k) #+n" in rev_mp)
   2.323 +apply (rule_tac [2] n = "natify(k) " in nat_induct)
   2.324 +apply auto
   2.325 +done
   2.326 +
   2.327 +lemma add_lt_elim1: "[| k#+m < k#+n; m: nat; n: nat |] ==> m < n"
   2.328 +by (drule add_lt_elim1_natify, auto)
   2.329 +
   2.330 +
   2.331 +(*** Monotonicity of Addition ***)
   2.332 +
   2.333 +(*strict, in 1st argument; proof is by rule induction on 'less than'.
   2.334 +  Still need j:nat, for consider j = omega.  Then we can have i<omega,
   2.335 +  which is the same as i:nat, but natify(j)=0, so the conclusion fails.*)
   2.336 +lemma add_lt_mono1: "[| i<j; j:nat |] ==> i#+k < j#+k"
   2.337 +apply (frule lt_nat_in_nat, assumption)
   2.338 +apply (erule succ_lt_induct)
   2.339 +apply (simp_all add: leI)
   2.340 +done
   2.341 +
   2.342 +(*strict, in both arguments*)
   2.343 +lemma add_lt_mono:
   2.344 + "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l"
   2.345 +apply (rule add_lt_mono1 [THEN lt_trans], assumption+)
   2.346 +apply (subst add_commute, subst add_commute, rule add_lt_mono1, assumption+)
   2.347 +done
   2.348 +
   2.349 +(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
   2.350 +lemma Ord_lt_mono_imp_le_mono:
   2.351 +  assumes lt_mono: "!!i j. [| i<j; j:k |] ==> f(i) < f(j)"
   2.352 +      and ford:    "!!i. i:k ==> Ord(f(i))"
   2.353 +      and leij:    "i le j"
   2.354 +      and jink:    "j:k"
   2.355 +  shows "f(i) le f(j)"
   2.356 +apply (insert leij jink) 
   2.357 +apply (blast intro!: leCI lt_mono ford elim!: leE)
   2.358 +done
   2.359 +
   2.360 +(*le monotonicity, 1st argument*)
   2.361 +lemma add_le_mono1: "[| i le j; j:nat |] ==> i#+k le j#+k"
   2.362 +apply (rule_tac f = "%j. j#+k" in Ord_lt_mono_imp_le_mono, typecheck) 
   2.363 +apply (blast intro: add_lt_mono1 add_type [THEN nat_into_Ord])+
   2.364 +done
   2.365 +
   2.366 +(* le monotonicity, BOTH arguments*)
   2.367 +lemma add_le_mono: "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l"
   2.368 +apply (rule add_le_mono1 [THEN le_trans], assumption+)
   2.369 +apply (subst add_commute, subst add_commute, rule add_le_mono1, assumption+)
   2.370 +done
   2.371 +
   2.372 +(** Subtraction is the inverse of addition. **)
   2.373 +
   2.374 +lemma diff_add_inverse: "(n#+m) #- n = natify(m)"
   2.375 +apply (subgoal_tac " (natify(n) #+ m) #- natify(n) = natify(m) ")
   2.376 +apply (rule_tac [2] n = "natify(n) " in nat_induct)
   2.377 +apply auto
   2.378 +done
   2.379 +
   2.380 +lemma diff_add_inverse2: "(m#+n) #- n = natify(m)"
   2.381 +by (simp add: add_commute [of m] diff_add_inverse)
   2.382 +
   2.383 +lemma diff_cancel: "(k#+m) #- (k#+n) = m #- n"
   2.384 +apply (subgoal_tac "(natify(k) #+ natify(m)) #- (natify(k) #+ natify(n)) =
   2.385 +                    natify(m) #- natify(n) ")
   2.386 +apply (rule_tac [2] n = "natify(k) " in nat_induct)
   2.387 +apply auto
   2.388 +done
   2.389 +
   2.390 +lemma diff_cancel2: "(m#+k) #- (n#+k) = m #- n"
   2.391 +by (simp add: add_commute [of _ k] diff_cancel)
   2.392 +
   2.393 +lemma diff_add_0: "n #- (n#+m) = 0"
   2.394 +apply (subgoal_tac "natify(n) #- (natify(n) #+ natify(m)) = 0")
   2.395 +apply (rule_tac [2] n = "natify(n) " in nat_induct)
   2.396 +apply auto
   2.397 +done
   2.398 +
   2.399 +
   2.400 +(** Lemmas for the CancelNumerals simproc **)
   2.401 +
   2.402 +lemma eq_add_iff: "(u #+ m = u #+ n) <-> (0 #+ m = natify(n))"
   2.403 +apply auto
   2.404 +apply (blast dest: add_left_cancel_natify)
   2.405 +apply (simp add: add_def)
   2.406 +done
   2.407 +
   2.408 +lemma less_add_iff: "(u #+ m < u #+ n) <-> (0 #+ m < natify(n))"
   2.409 +apply (auto simp add: add_lt_elim1_natify)
   2.410 +apply (drule add_lt_mono1)
   2.411 +apply (auto simp add: add_commute [of u])
   2.412 +done
   2.413 +
   2.414 +lemma diff_add_eq: "((u #+ m) #- (u #+ n)) = ((0 #+ m) #- n)"
   2.415 +by (simp add: diff_cancel)
   2.416 +
   2.417 +(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
   2.418 +lemma eq_cong2: "u = u' ==> (t==u) == (t==u')"
   2.419 +by auto
   2.420 +
   2.421 +lemma iff_cong2: "u <-> u' ==> (t==u) == (t==u')"
   2.422 +by auto
   2.423 +
   2.424 +
   2.425 +(*** Multiplication [the simprocs need these laws] ***)
   2.426 +
   2.427 +lemma mult_0 [simp]: "0 #* m = 0"
   2.428 +by (simp add: mult_def)
   2.429 +
   2.430 +lemma mult_succ [simp]: "succ(m) #* n = n #+ (m #* n)"
   2.431 +by (simp add: add_def mult_def natify_succ raw_mult_type)
   2.432 +
   2.433 +(*right annihilation in product*)
   2.434 +lemma mult_0_right [simp]: "m #* 0 = 0"
   2.435 +apply (unfold mult_def)
   2.436 +apply (rule_tac n = "natify(m) " in nat_induct)
   2.437 +apply auto
   2.438 +done
   2.439 +
   2.440 +(*right successor law for multiplication*)
   2.441 +lemma mult_succ_right [simp]: "m #* succ(n) = m #+ (m #* n)"
   2.442 +apply (subgoal_tac "natify(m) #* succ (natify(n)) =
   2.443 +                    natify(m) #+ (natify(m) #* natify(n))")
   2.444 +apply (simp (no_asm_use) add: natify_succ add_def mult_def)
   2.445 +apply (rule_tac n = "natify(m) " in nat_induct)
   2.446 +apply (simp_all add: add_ac)
   2.447 +done
   2.448 +
   2.449 +lemma mult_1_natify [simp]: "1 #* n = natify(n)"
   2.450 +by auto
   2.451 +
   2.452 +lemma mult_1_right_natify [simp]: "n #* 1 = natify(n)"
   2.453 +by auto
   2.454 +
   2.455 +lemma mult_1: "n : nat ==> 1 #* n = n"
   2.456 +by simp
   2.457 +
   2.458 +lemma mult_1_right: "n : nat ==> n #* 1 = n"
   2.459 +by simp
   2.460 +
   2.461 +(*Commutative law for multiplication*)
   2.462 +lemma mult_commute: "m #* n = n #* m"
   2.463 +apply (subgoal_tac "natify(m) #* natify(n) = natify(n) #* natify(m) ")
   2.464 +apply (rule_tac [2] n = "natify(m) " in nat_induct)
   2.465 +apply auto
   2.466 +done
   2.467 +
   2.468 +(*addition distributes over multiplication*)
   2.469 +lemma add_mult_distrib: "(m #+ n) #* k = (m #* k) #+ (n #* k)"
   2.470 +apply (subgoal_tac "(natify(m) #+ natify(n)) #* natify(k) =
   2.471 +                    (natify(m) #* natify(k)) #+ (natify(n) #* natify(k))")
   2.472 +apply (rule_tac [2] n = "natify(m) " in nat_induct)
   2.473 +apply (simp_all add: add_assoc [symmetric])
   2.474 +done
   2.475 +
   2.476 +(*Distributive law on the left*)
   2.477 +lemma add_mult_distrib_left: "k #* (m #+ n) = (k #* m) #+ (k #* n)"
   2.478 +apply (subgoal_tac "natify(k) #* (natify(m) #+ natify(n)) =
   2.479 +                    (natify(k) #* natify(m)) #+ (natify(k) #* natify(n))")
   2.480 +apply (rule_tac [2] n = "natify(m) " in nat_induct)
   2.481 +apply (simp_all add: add_ac)
   2.482 +done
   2.483 +
   2.484 +(*Associative law for multiplication*)
   2.485 +lemma mult_assoc: "(m #* n) #* k = m #* (n #* k)"
   2.486 +apply (subgoal_tac "(natify(m) #* natify(n)) #* natify(k) =
   2.487 +                    natify(m) #* (natify(n) #* natify(k))")
   2.488 +apply (rule_tac [2] n = "natify(m) " in nat_induct)
   2.489 +apply (simp_all add: add_mult_distrib)
   2.490 +done
   2.491 +
   2.492 +(*for a/c rewriting*)
   2.493 +lemma mult_left_commute: "m #* (n #* k) = n #* (m #* k)"
   2.494 +apply (rule mult_commute [THEN trans])
   2.495 +apply (rule mult_assoc [THEN trans])
   2.496 +apply (rule mult_commute [THEN subst_context])
   2.497 +done
   2.498 +
   2.499 +lemmas mult_ac = mult_assoc mult_commute mult_left_commute
   2.500 +
   2.501 +
   2.502 +lemma lt_succ_eq_0_disj:
   2.503 +     "[| m:nat; n:nat |]
   2.504 +      ==> (m < succ(n)) <-> (m = 0 | (EX j:nat. m = succ(j) & j < n))"
   2.505 +by (induct_tac "m", auto)
   2.506 +
   2.507 +lemma less_diff_conv [rule_format]:
   2.508 +     "[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)"
   2.509 +by (erule_tac m = "k" in diff_induct, auto)
   2.510 +
   2.511 +lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat
   2.512 +
   2.513 +ML
   2.514 +{*
   2.515 +val pred_def = thm "pred_def";
   2.516 +val raw_div_def = thm "raw_div_def";
   2.517 +val raw_mod_def = thm "raw_mod_def";
   2.518 +val div_def = thm "div_def";
   2.519 +val mod_def = thm "mod_def";
   2.520 +
   2.521 +val zero_lt_lemma = thm "zero_lt_lemma";
   2.522 +val zero_lt_natE = thm "zero_lt_natE";
   2.523 +val pred_succ_eq = thm "pred_succ_eq";
   2.524 +val natify_succ = thm "natify_succ";
   2.525 +val natify_0 = thm "natify_0";
   2.526 +val natify_non_succ = thm "natify_non_succ";
   2.527 +val natify_in_nat = thm "natify_in_nat";
   2.528 +val natify_ident = thm "natify_ident";
   2.529 +val natify_eqE = thm "natify_eqE";
   2.530 +val natify_idem = thm "natify_idem";
   2.531 +val add_natify1 = thm "add_natify1";
   2.532 +val add_natify2 = thm "add_natify2";
   2.533 +val mult_natify1 = thm "mult_natify1";
   2.534 +val mult_natify2 = thm "mult_natify2";
   2.535 +val diff_natify1 = thm "diff_natify1";
   2.536 +val diff_natify2 = thm "diff_natify2";
   2.537 +val mod_natify1 = thm "mod_natify1";
   2.538 +val mod_natify2 = thm "mod_natify2";
   2.539 +val div_natify1 = thm "div_natify1";
   2.540 +val div_natify2 = thm "div_natify2";
   2.541 +val raw_add_type = thm "raw_add_type";
   2.542 +val add_type = thm "add_type";
   2.543 +val raw_mult_type = thm "raw_mult_type";
   2.544 +val mult_type = thm "mult_type";
   2.545 +val raw_diff_type = thm "raw_diff_type";
   2.546 +val diff_type = thm "diff_type";
   2.547 +val diff_0_eq_0 = thm "diff_0_eq_0";
   2.548 +val diff_succ_succ = thm "diff_succ_succ";
   2.549 +val diff_0 = thm "diff_0";
   2.550 +val diff_le_self = thm "diff_le_self";
   2.551 +val add_0_natify = thm "add_0_natify";
   2.552 +val add_succ = thm "add_succ";
   2.553 +val add_0 = thm "add_0";
   2.554 +val add_assoc = thm "add_assoc";
   2.555 +val add_0_right_natify = thm "add_0_right_natify";
   2.556 +val add_succ_right = thm "add_succ_right";
   2.557 +val add_0_right = thm "add_0_right";
   2.558 +val add_commute = thm "add_commute";
   2.559 +val add_left_commute = thm "add_left_commute";
   2.560 +val raw_add_left_cancel = thm "raw_add_left_cancel";
   2.561 +val add_left_cancel_natify = thm "add_left_cancel_natify";
   2.562 +val add_left_cancel = thm "add_left_cancel";
   2.563 +val add_le_elim1_natify = thm "add_le_elim1_natify";
   2.564 +val add_le_elim1 = thm "add_le_elim1";
   2.565 +val add_lt_elim1_natify = thm "add_lt_elim1_natify";
   2.566 +val add_lt_elim1 = thm "add_lt_elim1";
   2.567 +val add_lt_mono1 = thm "add_lt_mono1";
   2.568 +val add_lt_mono = thm "add_lt_mono";
   2.569 +val Ord_lt_mono_imp_le_mono = thm "Ord_lt_mono_imp_le_mono";
   2.570 +val add_le_mono1 = thm "add_le_mono1";
   2.571 +val add_le_mono = thm "add_le_mono";
   2.572 +val diff_add_inverse = thm "diff_add_inverse";
   2.573 +val diff_add_inverse2 = thm "diff_add_inverse2";
   2.574 +val diff_cancel = thm "diff_cancel";
   2.575 +val diff_cancel2 = thm "diff_cancel2";
   2.576 +val diff_add_0 = thm "diff_add_0";
   2.577 +val eq_add_iff = thm "eq_add_iff";
   2.578 +val less_add_iff = thm "less_add_iff";
   2.579 +val diff_add_eq = thm "diff_add_eq";
   2.580 +val eq_cong2 = thm "eq_cong2";
   2.581 +val iff_cong2 = thm "iff_cong2";
   2.582 +val mult_0 = thm "mult_0";
   2.583 +val mult_succ = thm "mult_succ";
   2.584 +val mult_0_right = thm "mult_0_right";
   2.585 +val mult_succ_right = thm "mult_succ_right";
   2.586 +val mult_1_natify = thm "mult_1_natify";
   2.587 +val mult_1_right_natify = thm "mult_1_right_natify";
   2.588 +val mult_1 = thm "mult_1";
   2.589 +val mult_1_right = thm "mult_1_right";
   2.590 +val mult_commute = thm "mult_commute";
   2.591 +val add_mult_distrib = thm "add_mult_distrib";
   2.592 +val add_mult_distrib_left = thm "add_mult_distrib_left";
   2.593 +val mult_assoc = thm "mult_assoc";
   2.594 +val mult_left_commute = thm "mult_left_commute";
   2.595 +val lt_succ_eq_0_disj = thm "lt_succ_eq_0_disj";
   2.596 +val less_diff_conv = thm "less_diff_conv";
   2.597 +
   2.598 +val add_ac = thms "add_ac";
   2.599 +val mult_ac = thms "mult_ac";
   2.600 +val nat_typechecks = thms "nat_typechecks";
   2.601 +*}
   2.602  
   2.603  end
     3.1 --- a/src/ZF/Integ/IntDiv.ML	Fri May 17 16:54:25 2002 +0200
     3.2 +++ b/src/ZF/Integ/IntDiv.ML	Sat May 18 20:08:17 2002 +0200
     3.3 @@ -57,14 +57,14 @@
     3.4  by Auto_tac;
     3.5  qed "zneg_or_0_add_zneg_or_0_imp_zneg_or_0";
     3.6  
     3.7 -
     3.8  Goal "[| #0 $< k; k \\<in> int |] ==> 0 < zmagnitude(k)";
     3.9  by (dtac zero_zless_imp_znegative_zminus 1);
    3.10  by (dtac zneg_int_of 2);
    3.11  by (auto_tac (claset(), simpset() addsimps [inst "x" "k" zminus_equation]));  
    3.12  by (subgoal_tac "0 < zmagnitude($# succ(x))" 1);
    3.13  by (Asm_full_simp_tac 1);
    3.14 -by (asm_full_simp_tac (simpset_of Arith.thy addsimps [zmagnitude_int_of]) 1);
    3.15 +by (asm_full_simp_tac (FOL_ss addsimps [zmagnitude_int_of]) 1);
    3.16 +by (Asm_full_simp_tac 1); 
    3.17  qed "zero_lt_zmagnitude";
    3.18  
    3.19  
     4.1 --- a/src/ZF/IsaMakefile	Fri May 17 16:54:25 2002 +0200
     4.2 +++ b/src/ZF/IsaMakefile	Sat May 18 20:08:17 2002 +0200
     4.3 @@ -28,7 +28,7 @@
     4.4  FOL:
     4.5  	@cd $(SRC)/FOL; $(ISATOOL) make FOL
     4.6  
     4.7 -$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.ML Arith.thy ArithSimp.ML	\
     4.8 +$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.ML	\
     4.9    ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy		\
    4.10    CardinalArith.ML CardinalArith.thy Cardinal_AC.thy \
    4.11    Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy Finite.ML Finite.thy	\
    4.12 @@ -45,9 +45,9 @@
    4.13    Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
    4.14    Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
    4.15    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
    4.16 -  Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML	\
    4.17 +  Trancl.ML Trancl.thy Univ.thy Update.ML Update.thy WF.ML	\
    4.18    WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML domrange.ML	\
    4.19 -  domrange.thy equalities.ML equalities.thy func.ML func.thy		\
    4.20 +  domrange.thy equalities.ML equalities.thy func.thy		\
    4.21    ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML		\
    4.22    subset.ML subset.thy thy_syntax.ML upair.ML upair.thy
    4.23  	@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
     5.1 --- a/src/ZF/OrderType.thy	Fri May 17 16:54:25 2002 +0200
     5.2 +++ b/src/ZF/OrderType.thy	Sat May 18 20:08:17 2002 +0200
     5.3 @@ -180,8 +180,7 @@
     5.4  lemma ordermap_mono:
     5.5       "[| <w,x>: r;  wf[A](r);  w: A; x: A |]
     5.6        ==> ordermap(A,r)`w : ordermap(A,r)`x"
     5.7 -apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption)
     5.8 -apply blast
     5.9 +apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption, blast)
    5.10  done
    5.11  
    5.12  (*linearity of r is crucial here*)
     6.1 --- a/src/ZF/Univ.ML	Fri May 17 16:54:25 2002 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,765 +0,0 @@
     6.4 -(*  Title:      ZF/Univ
     6.5 -    ID:         $Id$
     6.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 -    Copyright   1994  University of Cambridge
     6.8 -
     6.9 -The cumulative hierarchy and a small universe for recursive types
    6.10 -*)
    6.11 -
    6.12 -(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
    6.13 -Goal "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
    6.14 -by (stac (Vfrom_def RS def_transrec) 1);
    6.15 -by (Simp_tac 1);
    6.16 -qed "Vfrom";
    6.17 -
    6.18 -(** Monotonicity **)
    6.19 -
    6.20 -Goal "A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)";
    6.21 -by (eps_ind_tac "i" 1);
    6.22 -by (rtac (impI RS allI) 1);
    6.23 -by (stac Vfrom 1);
    6.24 -by (stac Vfrom 1);
    6.25 -by (etac Un_mono 1);
    6.26 -by (rtac UN_mono 1);
    6.27 -by (assume_tac 1);
    6.28 -by (rtac Pow_mono 1);
    6.29 -by (etac (bspec RS spec RS mp) 1);
    6.30 -by (assume_tac 1);
    6.31 -by (rtac subset_refl 1);
    6.32 -qed_spec_mp "Vfrom_mono";
    6.33 -
    6.34 -
    6.35 -(** A fundamental equality: Vfrom does not require ordinals! **)
    6.36 -
    6.37 -Goal "Vfrom(A,x) <= Vfrom(A,rank(x))";
    6.38 -by (eps_ind_tac "x" 1);
    6.39 -by (stac Vfrom 1);
    6.40 -by (stac Vfrom 1);
    6.41 -by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
    6.42 -qed "Vfrom_rank_subset1";
    6.43 -
    6.44 -Goal "Vfrom(A,rank(x)) <= Vfrom(A,x)";
    6.45 -by (eps_ind_tac "x" 1);
    6.46 -by (stac Vfrom 1);
    6.47 -by (stac Vfrom 1);
    6.48 -by (rtac (subset_refl RS Un_mono) 1);
    6.49 -by (rtac UN_least 1);
    6.50 -(*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*)
    6.51 -by (etac (rank RS equalityD1 RS subsetD RS UN_E) 1);
    6.52 -by (rtac subset_trans 1);
    6.53 -by (etac UN_upper 2);
    6.54 -by (rtac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1);
    6.55 -by (etac (ltI RS le_imp_subset) 1);
    6.56 -by (rtac (Ord_rank RS Ord_succ) 1);
    6.57 -by (etac bspec 1);
    6.58 -by (assume_tac 1);
    6.59 -qed "Vfrom_rank_subset2";
    6.60 -
    6.61 -Goal "Vfrom(A,rank(x)) = Vfrom(A,x)";
    6.62 -by (rtac equalityI 1);
    6.63 -by (rtac Vfrom_rank_subset2 1);
    6.64 -by (rtac Vfrom_rank_subset1 1);
    6.65 -qed "Vfrom_rank_eq";
    6.66 -
    6.67 -
    6.68 -(*** Basic closure properties ***)
    6.69 -
    6.70 -Goal "y:x ==> 0 : Vfrom(A,x)";
    6.71 -by (stac Vfrom 1);
    6.72 -by (Blast_tac 1);
    6.73 -qed "zero_in_Vfrom";
    6.74 -
    6.75 -Goal "i <= Vfrom(A,i)";
    6.76 -by (eps_ind_tac "i" 1);
    6.77 -by (stac Vfrom 1);
    6.78 -by (Blast_tac 1);
    6.79 -qed "i_subset_Vfrom";
    6.80 -
    6.81 -Goal "A <= Vfrom(A,i)";
    6.82 -by (stac Vfrom 1);
    6.83 -by (rtac Un_upper1 1);
    6.84 -qed "A_subset_Vfrom";
    6.85 -
    6.86 -bind_thm ("A_into_Vfrom", A_subset_Vfrom RS subsetD);
    6.87 -
    6.88 -Goal "a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
    6.89 -by (stac Vfrom 1);
    6.90 -by (Blast_tac 1);
    6.91 -qed "subset_mem_Vfrom";
    6.92 -
    6.93 -(** Finite sets and ordered pairs **)
    6.94 -
    6.95 -Goal "a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))";
    6.96 -by (rtac subset_mem_Vfrom 1);
    6.97 -by Safe_tac;
    6.98 -qed "singleton_in_Vfrom";
    6.99 -
   6.100 -Goal "[| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))";
   6.101 -by (rtac subset_mem_Vfrom 1);
   6.102 -by Safe_tac;
   6.103 -qed "doubleton_in_Vfrom";
   6.104 -
   6.105 -Goalw [Pair_def]
   6.106 -    "[| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> \
   6.107 -\         <a,b> : Vfrom(A,succ(succ(i)))";
   6.108 -by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
   6.109 -qed "Pair_in_Vfrom";
   6.110 -
   6.111 -Goal "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
   6.112 -by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1));
   6.113 -by (rtac (Vfrom_mono RSN (2,subset_trans)) 2);
   6.114 -by (REPEAT (ares_tac [subset_refl, subset_succI] 1));
   6.115 -qed "succ_in_Vfrom";
   6.116 -
   6.117 -(*** 0, successor and limit equations fof Vfrom ***)
   6.118 -
   6.119 -Goal "Vfrom(A,0) = A";
   6.120 -by (stac Vfrom 1);
   6.121 -by (Blast_tac 1);
   6.122 -qed "Vfrom_0";
   6.123 -
   6.124 -Goal "Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
   6.125 -by (rtac (Vfrom RS trans) 1);
   6.126 -by (rtac (succI1 RS RepFunI RS Union_upper RSN
   6.127 -              (2, equalityI RS subst_context)) 1);
   6.128 -by (rtac UN_least 1);
   6.129 -by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
   6.130 -by (etac (ltI RS le_imp_subset) 1);
   6.131 -by (etac Ord_succ 1);
   6.132 -qed "Vfrom_succ_lemma";
   6.133 -
   6.134 -Goal "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
   6.135 -by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1);
   6.136 -by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1);
   6.137 -by (stac rank_succ 1);
   6.138 -by (rtac (Ord_rank RS Vfrom_succ_lemma) 1);
   6.139 -qed "Vfrom_succ";
   6.140 -
   6.141 -(*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
   6.142 -  the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
   6.143 -Goal "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
   6.144 -by (stac Vfrom 1);
   6.145 -by (rtac equalityI 1);
   6.146 -(*first inclusion*)
   6.147 -by (rtac Un_least 1);
   6.148 -by (rtac (A_subset_Vfrom RS subset_trans) 1);
   6.149 -by (rtac UN_upper 1);
   6.150 -by (assume_tac 1);
   6.151 -by (rtac UN_least 1);
   6.152 -by (etac UnionE 1);
   6.153 -by (rtac subset_trans 1);
   6.154 -by (etac UN_upper 2 THEN stac Vfrom 1 THEN 
   6.155 -    etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
   6.156 -(*opposite inclusion*)
   6.157 -by (rtac UN_least 1);
   6.158 -by (stac Vfrom 1);
   6.159 -by (Blast_tac 1);
   6.160 -qed "Vfrom_Union";
   6.161 -
   6.162 -(*** Vfrom applied to Limit ordinals ***)
   6.163 -
   6.164 -(*NB. limit ordinals are non-empty;
   6.165 -                        Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
   6.166 -val [limiti] = goal (the_context ())
   6.167 -    "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
   6.168 -by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1);
   6.169 -by (stac (limiti RS Limit_Union_eq) 1);
   6.170 -by (rtac refl 1);
   6.171 -qed "Limit_Vfrom_eq";
   6.172 -
   6.173 -Goal "[| a: Vfrom(A,j);  Limit(i);  j<i |] ==> a : Vfrom(A,i)";
   6.174 -by (rtac (Limit_Vfrom_eq RS equalityD2 RS subsetD) 1);
   6.175 -by (REPEAT (ares_tac [ltD RS UN_I] 1));
   6.176 -qed "Limit_VfromI";
   6.177 -
   6.178 -val prems = Goal
   6.179 -    "[| a: Vfrom(A,i);  ~R ==> Limit(i);               \
   6.180 -\       !!x. [| x<i;  a: Vfrom(A,x) |] ==> R    \
   6.181 -\    |] ==> R";
   6.182 -by (rtac classical 1);
   6.183 -by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1);
   6.184 -by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1));
   6.185 -qed "Limit_VfromE";
   6.186 -
   6.187 -bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom);
   6.188 -
   6.189 -val [major,limiti] = goal (the_context ())
   6.190 -    "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)";
   6.191 -by (rtac ([major,limiti] MRS Limit_VfromE) 1);
   6.192 -by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
   6.193 -by (etac (limiti RS Limit_has_succ) 1);
   6.194 -qed "singleton_in_VLimit";
   6.195 -
   6.196 -bind_thm ("Vfrom_UnI1", Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD));
   6.197 -bind_thm ("Vfrom_UnI2", Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD));
   6.198 -
   6.199 -(*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*)
   6.200 -val [aprem,bprem,limiti] = goal (the_context ())
   6.201 -    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
   6.202 -\    {a,b} : Vfrom(A,i)";
   6.203 -by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
   6.204 -by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
   6.205 -by (rtac ([doubleton_in_Vfrom, limiti] MRS Limit_VfromI) 1);
   6.206 -by (etac Vfrom_UnI1 1);
   6.207 -by (etac Vfrom_UnI2 1);
   6.208 -by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
   6.209 -qed "doubleton_in_VLimit";
   6.210 -
   6.211 -val [aprem,bprem,limiti] = goal (the_context ())
   6.212 -    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> \
   6.213 -\    <a,b> : Vfrom(A,i)";
   6.214 -(*Infer that a, b occur at ordinals x,xa < i.*)
   6.215 -by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
   6.216 -by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
   6.217 -by (rtac ([Pair_in_Vfrom, limiti] MRS Limit_VfromI) 1);
   6.218 -(*Infer that succ(succ(x Un xa)) < i *)
   6.219 -by (etac Vfrom_UnI1 1);
   6.220 -by (etac Vfrom_UnI2 1);
   6.221 -by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1));
   6.222 -qed "Pair_in_VLimit";
   6.223 -
   6.224 -Goal "Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)";
   6.225 -by (REPEAT (ares_tac [subsetI,Pair_in_VLimit] 1
   6.226 -     ORELSE eresolve_tac [SigmaE, ssubst] 1));
   6.227 -qed "product_VLimit";
   6.228 -
   6.229 -bind_thm ("Sigma_subset_VLimit",
   6.230 -          [Sigma_mono, product_VLimit] MRS subset_trans);
   6.231 -
   6.232 -bind_thm ("nat_subset_VLimit", 
   6.233 -          [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans);
   6.234 -
   6.235 -Goal "[| n: nat;  Limit(i) |] ==> n : Vfrom(A,i)";
   6.236 -by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1));
   6.237 -qed "nat_into_VLimit";
   6.238 -
   6.239 -(** Closure under disjoint union **)
   6.240 -
   6.241 -bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom);
   6.242 -
   6.243 -Goal "Limit(i) ==> 1 : Vfrom(A,i)";
   6.244 -by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1));
   6.245 -qed "one_in_VLimit";
   6.246 -
   6.247 -Goalw [Inl_def]
   6.248 -    "[| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)";
   6.249 -by (REPEAT (ares_tac [zero_in_VLimit, Pair_in_VLimit] 1));
   6.250 -qed "Inl_in_VLimit";
   6.251 -
   6.252 -Goalw [Inr_def]
   6.253 -    "[| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)";
   6.254 -by (REPEAT (ares_tac [one_in_VLimit, Pair_in_VLimit] 1));
   6.255 -qed "Inr_in_VLimit";
   6.256 -
   6.257 -Goal "Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
   6.258 -by (blast_tac (claset() addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
   6.259 -qed "sum_VLimit";
   6.260 -
   6.261 -bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans);
   6.262 -
   6.263 -
   6.264 -
   6.265 -(*** Properties assuming Transset(A) ***)
   6.266 -
   6.267 -Goal "Transset(A) ==> Transset(Vfrom(A,i))";
   6.268 -by (eps_ind_tac "i" 1);
   6.269 -by (stac Vfrom 1);
   6.270 -by (blast_tac (claset() addSIs [Transset_Union_family, Transset_Un,
   6.271 -                            Transset_Pow]) 1);
   6.272 -qed "Transset_Vfrom";
   6.273 -
   6.274 -Goal "Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
   6.275 -by (rtac (Vfrom_succ RS trans) 1);
   6.276 -by (rtac (Un_upper2 RSN (2,equalityI)) 1);
   6.277 -by (rtac (subset_refl RSN (2,Un_least)) 1);
   6.278 -by (rtac (A_subset_Vfrom RS subset_trans) 1);
   6.279 -by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
   6.280 -qed "Transset_Vfrom_succ";
   6.281 -
   6.282 -Goalw [Pair_def,Transset_def] "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
   6.283 -by (Blast_tac 1);
   6.284 -qed "Transset_Pair_subset";
   6.285 -
   6.286 -Goal "[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |] ==> \
   6.287 -\          <a,b> : Vfrom(A,i)";
   6.288 -by (etac (Transset_Pair_subset RS conjE) 1);
   6.289 -by (etac Transset_Vfrom 1);
   6.290 -by (REPEAT (ares_tac [Pair_in_VLimit] 1));
   6.291 -qed "Transset_Pair_subset_VLimit";
   6.292 -
   6.293 -Goal "[| X: Vfrom(A,j);  Transset(A) |] ==> Union(X) : Vfrom(A, succ(j))";
   6.294 -by (dtac Transset_Vfrom 1);
   6.295 -by (rtac subset_mem_Vfrom 1);
   6.296 -by (rewtac Transset_def);
   6.297 -by (Blast_tac 1);
   6.298 -qed "Union_in_Vfrom";
   6.299 -
   6.300 -Goal "[| X: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Union(X) : Vfrom(A,i)";
   6.301 -by (rtac (Limit_VfromE) 1 THEN REPEAT (assume_tac 1));
   6.302 -by (blast_tac (claset() addIs [Limit_has_succ, Limit_VfromI, Union_in_Vfrom]) 1); 
   6.303 -qed "Union_in_VLimit";
   6.304 -
   6.305 -
   6.306 -(*** Closure under product/sum applied to elements -- thus Vfrom(A,i) 
   6.307 -     is a model of simple type theory provided A is a transitive set
   6.308 -     and i is a limit ordinal
   6.309 -***)
   6.310 -
   6.311 -(*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*)
   6.312 -val [aprem,bprem,limiti,step] = Goal
   6.313 -  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);                 \
   6.314 -\     !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) \
   6.315 -\              |] ==> EX k. h(x,y): Vfrom(A,k) & k<i |] ==>     \
   6.316 -\  h(a,b) : Vfrom(A,i)";
   6.317 -(*Infer that a, b occur at ordinals x,xa < i.*)
   6.318 -by (rtac ([aprem,limiti] MRS Limit_VfromE) 1);
   6.319 -by (rtac ([bprem,limiti] MRS Limit_VfromE) 1);
   6.320 -by (res_inst_tac [("j1", "x Un xa Un 2")] (step RS exE) 1);
   6.321 -by (blast_tac (claset() addIs [Limit_VfromI, limiti]) 5);
   6.322 -by (etac (Vfrom_UnI2 RS Vfrom_UnI1) 4);
   6.323 -by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3);
   6.324 -by (rtac (succI1 RS UnI2) 2);
   6.325 -by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1));
   6.326 -qed "in_VLimit";
   6.327 -
   6.328 -(** products **)
   6.329 -
   6.330 -Goal "[| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==> \
   6.331 -\         a*b : Vfrom(A, succ(succ(succ(j))))";
   6.332 -by (dtac Transset_Vfrom 1);
   6.333 -by (rtac subset_mem_Vfrom 1);
   6.334 -by (rewtac Transset_def);
   6.335 -by (blast_tac (claset() addIs [Pair_in_Vfrom]) 1);
   6.336 -qed "prod_in_Vfrom";
   6.337 -
   6.338 -val [aprem,bprem,limiti,transset] = goal (the_context ())
   6.339 -  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
   6.340 -\  a*b : Vfrom(A,i)";
   6.341 -by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
   6.342 -by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset,
   6.343 -                      limiti RS Limit_has_succ] 1));
   6.344 -qed "prod_in_VLimit";
   6.345 -
   6.346 -(** Disjoint sums, aka Quine ordered pairs **)
   6.347 -
   6.348 -Goalw [sum_def]
   6.349 -    "[| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A);  1:j |] ==> \
   6.350 -\         a+b : Vfrom(A, succ(succ(succ(j))))";
   6.351 -by (dtac Transset_Vfrom 1);
   6.352 -by (rtac subset_mem_Vfrom 1);
   6.353 -by (rewtac Transset_def);
   6.354 -by (blast_tac (claset() addIs [zero_in_Vfrom, Pair_in_Vfrom, 
   6.355 -                           i_subset_Vfrom RS subsetD]) 1);
   6.356 -qed "sum_in_Vfrom";
   6.357 -
   6.358 -val [aprem,bprem,limiti,transset] = goal (the_context ())
   6.359 -  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
   6.360 -\  a+b : Vfrom(A,i)";
   6.361 -by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
   6.362 -by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset,
   6.363 -                      limiti RS Limit_has_succ] 1));
   6.364 -qed "sum_in_VLimit";
   6.365 -
   6.366 -(** function space! **)
   6.367 -
   6.368 -Goalw [Pi_def]
   6.369 -    "[| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==> \
   6.370 -\         a->b : Vfrom(A, succ(succ(succ(succ(j)))))";
   6.371 -by (dtac Transset_Vfrom 1);
   6.372 -by (rtac subset_mem_Vfrom 1);
   6.373 -by (rtac (Collect_subset RS subset_trans) 1);
   6.374 -by (stac Vfrom 1);
   6.375 -by (rtac (subset_trans RS subset_trans) 1);
   6.376 -by (rtac Un_upper2 3);
   6.377 -by (rtac (succI1 RS UN_upper) 2);
   6.378 -by (rtac Pow_mono 1);
   6.379 -by (rewtac Transset_def);
   6.380 -by (blast_tac (claset() addIs [Pair_in_Vfrom]) 1);
   6.381 -qed "fun_in_Vfrom";
   6.382 -
   6.383 -val [aprem,bprem,limiti,transset] = goal (the_context ())
   6.384 -  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \
   6.385 -\  a->b : Vfrom(A,i)";
   6.386 -by (rtac ([aprem,bprem,limiti] MRS in_VLimit) 1);
   6.387 -by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset,
   6.388 -                      limiti RS Limit_has_succ] 1));
   6.389 -qed "fun_in_VLimit";
   6.390 -
   6.391 -Goalw [Pi_def]
   6.392 -    "[| a: Vfrom(A,j);  Transset(A) |] ==> Pow(a) : Vfrom(A, succ(succ(j)))";
   6.393 -by (dtac Transset_Vfrom 1);
   6.394 -by (rtac subset_mem_Vfrom 1);
   6.395 -by (rewtac Transset_def);
   6.396 -by (stac Vfrom 1);
   6.397 -by (Blast_tac 1);
   6.398 -qed "Pow_in_Vfrom";
   6.399 -
   6.400 -Goal "[| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
   6.401 -by (blast_tac (claset() addEs [Limit_VfromE]
   6.402 -	                addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1);
   6.403 -qed "Pow_in_VLimit";
   6.404 -
   6.405 -
   6.406 -(*** The set Vset(i) ***)
   6.407 -
   6.408 -Goal "Vset(i) = (UN j:i. Pow(Vset(j)))";
   6.409 -by (stac Vfrom 1);
   6.410 -by (Blast_tac 1);
   6.411 -qed "Vset";
   6.412 -
   6.413 -bind_thm ("Vset_succ", Transset_0 RS Transset_Vfrom_succ);
   6.414 -
   6.415 -bind_thm ("Transset_Vset", Transset_0 RS Transset_Vfrom);
   6.416 -
   6.417 -(** Characterisation of the elements of Vset(i) **)
   6.418 -
   6.419 -Goal "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
   6.420 -by (etac trans_induct 1);
   6.421 -by (stac Vset 1);
   6.422 -by Safe_tac;
   6.423 -by (stac rank 1);
   6.424 -by (rtac UN_succ_least_lt 1);
   6.425 -by (Blast_tac 2);
   6.426 -by (REPEAT (ares_tac [ltI] 1));
   6.427 -qed_spec_mp "VsetD";
   6.428 -
   6.429 -Goal "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
   6.430 -by (etac trans_induct 1);
   6.431 -by (rtac allI 1);
   6.432 -by (stac Vset 1);
   6.433 -by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
   6.434 -val lemma = result();
   6.435 -
   6.436 -Goal "rank(x)<i ==> x : Vset(i)";
   6.437 -by (etac ltE 1);
   6.438 -by (etac (lemma RS spec RS mp) 1);
   6.439 -by (assume_tac 1);
   6.440 -qed "VsetI";
   6.441 -
   6.442 -(*Merely a lemma for the result following*)
   6.443 -Goal "Ord(i) ==> b : Vset(i) <-> rank(b) < i";
   6.444 -by (rtac iffI 1);
   6.445 -by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1));
   6.446 -qed "Vset_Ord_rank_iff";
   6.447 -
   6.448 -Goal "b : Vset(a) <-> rank(b) < rank(a)";
   6.449 -by (rtac (Vfrom_rank_eq RS subst) 1);
   6.450 -by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1);
   6.451 -qed "Vset_rank_iff";
   6.452 -Addsimps [Vset_rank_iff];
   6.453 -
   6.454 -(*This is rank(rank(a)) = rank(a) *)
   6.455 -Addsimps [Ord_rank RS rank_of_Ord];
   6.456 -
   6.457 -Goal "Ord(i) ==> rank(Vset(i)) = i";
   6.458 -by (stac rank 1);
   6.459 -by (rtac equalityI 1);
   6.460 -by Safe_tac;
   6.461 -by (EVERY' [rtac UN_I, 
   6.462 -            etac (i_subset_Vfrom RS subsetD),
   6.463 -            etac (Ord_in_Ord RS rank_of_Ord RS ssubst),
   6.464 -            assume_tac,
   6.465 -            rtac succI1] 3);
   6.466 -by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1));
   6.467 -qed "rank_Vset";
   6.468 -
   6.469 -(** Lemmas for reasoning about sets in terms of their elements' ranks **)
   6.470 -
   6.471 -Goal "a <= Vset(rank(a))";
   6.472 -by (rtac subsetI 1);
   6.473 -by (etac (rank_lt RS VsetI) 1);
   6.474 -qed "arg_subset_Vset_rank";
   6.475 -
   6.476 -val [iprem] = Goal
   6.477 -    "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
   6.478 -by (rtac ([subset_refl, arg_subset_Vset_rank] MRS 
   6.479 -          Int_greatest RS subset_trans) 1);
   6.480 -by (rtac (Ord_rank RS iprem) 1);
   6.481 -qed "Int_Vset_subset";
   6.482 -
   6.483 -(** Set up an environment for simplification **)
   6.484 -
   6.485 -Goalw [Inl_def] "rank(a) < rank(Inl(a))";
   6.486 -by (rtac rank_pair2 1);
   6.487 -qed "rank_Inl";
   6.488 -
   6.489 -Goalw [Inr_def] "rank(a) < rank(Inr(a))";
   6.490 -by (rtac rank_pair2 1);
   6.491 -qed "rank_Inr";
   6.492 -
   6.493 -bind_thms ("rank_rls", [rank_Inl, rank_Inr, rank_pair1, rank_pair2]);
   6.494 -bind_thms ("rank_trans_rls", rank_rls @ (rank_rls RLN (2, [lt_trans])));
   6.495 -
   6.496 -val rank_ss = simpset() addsimps [VsetI] addsimps rank_trans_rls;
   6.497 -
   6.498 -(** Recursion over Vset levels! **)
   6.499 -
   6.500 -(*NOT SUITABLE FOR REWRITING: recursive!*)
   6.501 -Goalw [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
   6.502 -by (stac transrec 1);
   6.503 -by (Simp_tac 1);
   6.504 -by (rtac (refl RS lam_cong RS subst_context) 1);
   6.505 -by (Asm_full_simp_tac 1);
   6.506 -qed "Vrec";
   6.507 -
   6.508 -(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   6.509 -val rew::prems = Goal
   6.510 -    "[| !!x. h(x)==Vrec(x,H) |] ==> \
   6.511 -\    h(a) = H(a, lam x: Vset(rank(a)). h(x))";
   6.512 -by (rewtac rew);
   6.513 -by (rtac Vrec 1);
   6.514 -qed "def_Vrec";
   6.515 -
   6.516 -(*NOT SUITABLE FOR REWRITING: recursive!*)
   6.517 -Goalw [Vrecursor_def]
   6.518 -     "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x),  a)";
   6.519 -by (stac transrec 1);
   6.520 -by (Simp_tac 1);
   6.521 -by (rtac (refl RS lam_cong RS subst_context) 1);
   6.522 -by (Asm_full_simp_tac 1);
   6.523 -qed "Vrecursor";
   6.524 -
   6.525 -(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
   6.526 -Goal "h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x),  a)";
   6.527 -by (Asm_simp_tac 1);
   6.528 -by (rtac Vrecursor 1);
   6.529 -qed "def_Vrecursor";
   6.530 -
   6.531 -
   6.532 -(*** univ(A) ***)
   6.533 -
   6.534 -Goalw [univ_def] "A<=B ==> univ(A) <= univ(B)";
   6.535 -by (etac Vfrom_mono 1);
   6.536 -by (rtac subset_refl 1);
   6.537 -qed "univ_mono";
   6.538 -
   6.539 -Goalw [univ_def] "Transset(A) ==> Transset(univ(A))";
   6.540 -by (etac Transset_Vfrom 1);
   6.541 -qed "Transset_univ";
   6.542 -
   6.543 -(** univ(A) as a limit **)
   6.544 -
   6.545 -Goalw [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
   6.546 -by (rtac (Limit_nat RS Limit_Vfrom_eq) 1);
   6.547 -qed "univ_eq_UN";
   6.548 -
   6.549 -Goal "c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
   6.550 -by (rtac (subset_UN_iff_eq RS iffD1) 1);
   6.551 -by (etac (univ_eq_UN RS subst) 1);
   6.552 -qed "subset_univ_eq_Int";
   6.553 -
   6.554 -val [aprem, iprem] = Goal
   6.555 -    "[| a <= univ(X);                           \
   6.556 -\       !!i. i:nat ==> a Int Vfrom(X,i) <= b    \
   6.557 -\    |] ==> a <= b";
   6.558 -by (stac (aprem RS subset_univ_eq_Int) 1);
   6.559 -by (rtac UN_least 1);
   6.560 -by (etac iprem 1);
   6.561 -qed "univ_Int_Vfrom_subset";
   6.562 -
   6.563 -val prems = Goal
   6.564 -    "[| a <= univ(X);   b <= univ(X);   \
   6.565 -\       !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
   6.566 -\    |] ==> a = b";
   6.567 -by (rtac equalityI 1);
   6.568 -by (ALLGOALS
   6.569 -    (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN'
   6.570 -     eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN'
   6.571 -     rtac Int_lower1));
   6.572 -qed "univ_Int_Vfrom_eq";
   6.573 -
   6.574 -(** Closure properties **)
   6.575 -
   6.576 -Goalw [univ_def] "0 : univ(A)";
   6.577 -by (rtac (nat_0I RS zero_in_Vfrom) 1);
   6.578 -qed "zero_in_univ";
   6.579 -
   6.580 -Goalw [univ_def] "A <= univ(A)";
   6.581 -by (rtac A_subset_Vfrom 1);
   6.582 -qed "A_subset_univ";
   6.583 -
   6.584 -bind_thm ("A_into_univ", A_subset_univ RS subsetD);
   6.585 -
   6.586 -(** Closure under unordered and ordered pairs **)
   6.587 -
   6.588 -Goalw [univ_def] "a: univ(A) ==> {a} : univ(A)";
   6.589 -by (REPEAT (ares_tac [singleton_in_VLimit, Limit_nat] 1));
   6.590 -qed "singleton_in_univ";
   6.591 -
   6.592 -Goalw [univ_def] 
   6.593 -    "[| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)";
   6.594 -by (REPEAT (ares_tac [doubleton_in_VLimit, Limit_nat] 1));
   6.595 -qed "doubleton_in_univ";
   6.596 -
   6.597 -Goalw [univ_def]
   6.598 -    "[| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)";
   6.599 -by (REPEAT (ares_tac [Pair_in_VLimit, Limit_nat] 1));
   6.600 -qed "Pair_in_univ";
   6.601 -
   6.602 -Goalw [univ_def]
   6.603 -     "[| X: univ(A);  Transset(A) |] ==> Union(X) : univ(A)";
   6.604 -by (REPEAT (ares_tac [Union_in_VLimit, Limit_nat] 1));
   6.605 -qed "Union_in_univ";
   6.606 -
   6.607 -Goalw [univ_def] "univ(A)*univ(A) <= univ(A)";
   6.608 -by (rtac (Limit_nat RS product_VLimit) 1);
   6.609 -qed "product_univ";
   6.610 -
   6.611 -
   6.612 -(** The natural numbers **)
   6.613 -
   6.614 -Goalw [univ_def] "nat <= univ(A)";
   6.615 -by (rtac i_subset_Vfrom 1);
   6.616 -qed "nat_subset_univ";
   6.617 -
   6.618 -(* n:nat ==> n:univ(A) *)
   6.619 -bind_thm ("nat_into_univ", (nat_subset_univ RS subsetD));
   6.620 -
   6.621 -(** instances for 1 and 2 **)
   6.622 -
   6.623 -Goalw [univ_def] "1 : univ(A)";
   6.624 -by (rtac (Limit_nat RS one_in_VLimit) 1);
   6.625 -qed "one_in_univ";
   6.626 -
   6.627 -(*unused!*)
   6.628 -Goal "2 : univ(A)";
   6.629 -by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
   6.630 -qed "two_in_univ";
   6.631 -
   6.632 -Goalw [bool_def] "bool <= univ(A)";
   6.633 -by (blast_tac (claset() addSIs [zero_in_univ,one_in_univ]) 1);
   6.634 -qed "bool_subset_univ";
   6.635 -
   6.636 -bind_thm ("bool_into_univ", (bool_subset_univ RS subsetD));
   6.637 -
   6.638 -
   6.639 -(** Closure under disjoint union **)
   6.640 -
   6.641 -Goalw [univ_def] "a: univ(A) ==> Inl(a) : univ(A)";
   6.642 -by (etac (Limit_nat RSN (2,Inl_in_VLimit)) 1);
   6.643 -qed "Inl_in_univ";
   6.644 -
   6.645 -Goalw [univ_def] "b: univ(A) ==> Inr(b) : univ(A)";
   6.646 -by (etac (Limit_nat RSN (2,Inr_in_VLimit)) 1);
   6.647 -qed "Inr_in_univ";
   6.648 -
   6.649 -Goalw [univ_def] "univ(C)+univ(C) <= univ(C)";
   6.650 -by (rtac (Limit_nat RS sum_VLimit) 1);
   6.651 -qed "sum_univ";
   6.652 -
   6.653 -bind_thm ("sum_subset_univ", [sum_mono, sum_univ] MRS subset_trans);
   6.654 -
   6.655 -
   6.656 -(** Closure under binary union -- use Un_least **)
   6.657 -(** Closure under Collect -- use  (Collect_subset RS subset_trans)  **)
   6.658 -(** Closure under RepFun -- use   RepFun_subset  **)
   6.659 -
   6.660 -
   6.661 -(*** Finite Branching Closure Properties ***)
   6.662 -
   6.663 -(** Closure under finite powerset **)
   6.664 -
   6.665 -Goal "[| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
   6.666 -by (etac Fin_induct 1);
   6.667 -by (blast_tac (claset() addSDs [Limit_has_0]) 1);
   6.668 -by Safe_tac;
   6.669 -by (etac Limit_VfromE 1);
   6.670 -by (assume_tac 1);
   6.671 -by (blast_tac (claset() addSIs [Un_least_lt] addIs [Vfrom_UnI1, Vfrom_UnI2]) 1);
   6.672 -qed "Fin_Vfrom_lemma";
   6.673 -
   6.674 -Goal "Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
   6.675 -by (rtac subsetI 1);
   6.676 -by (dtac Fin_Vfrom_lemma 1);
   6.677 -by Safe_tac;
   6.678 -by (resolve_tac [Vfrom RS ssubst] 1);
   6.679 -by (blast_tac (claset() addSDs [ltD]) 1);
   6.680 -qed "Fin_VLimit";
   6.681 -
   6.682 -bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans);
   6.683 -
   6.684 -Goalw [univ_def] "Fin(univ(A)) <= univ(A)";
   6.685 -by (rtac (Limit_nat RS Fin_VLimit) 1);
   6.686 -qed "Fin_univ";
   6.687 -
   6.688 -(** Closure under finite powers (functions from a fixed natural number) **)
   6.689 -
   6.690 -Goal "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
   6.691 -by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
   6.692 -by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit,
   6.693 -                      nat_subset_VLimit, subset_refl] 1));
   6.694 -qed "nat_fun_VLimit";
   6.695 -
   6.696 -bind_thm ("nat_fun_subset_VLimit", [Pi_mono, nat_fun_VLimit] MRS subset_trans);
   6.697 -
   6.698 -Goalw [univ_def] "n: nat ==> n -> univ(A) <= univ(A)";
   6.699 -by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
   6.700 -qed "nat_fun_univ";
   6.701 -
   6.702 -
   6.703 -(** Closure under finite function space **)
   6.704 -
   6.705 -(*General but seldom-used version; normally the domain is fixed*)
   6.706 -Goal "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)";
   6.707 -by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1);
   6.708 -by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1));
   6.709 -qed "FiniteFun_VLimit1";
   6.710 -
   6.711 -Goalw [univ_def] "univ(A) -||> univ(A) <= univ(A)";
   6.712 -by (rtac (Limit_nat RS FiniteFun_VLimit1) 1);
   6.713 -qed "FiniteFun_univ1";
   6.714 -
   6.715 -(*Version for a fixed domain*)
   6.716 -Goal "[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)";
   6.717 -by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1);
   6.718 -by (etac FiniteFun_VLimit1 1);
   6.719 -qed "FiniteFun_VLimit";
   6.720 -
   6.721 -Goalw [univ_def]
   6.722 -    "W <= univ(A) ==> W -||> univ(A) <= univ(A)";
   6.723 -by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1);
   6.724 -qed "FiniteFun_univ";
   6.725 -
   6.726 -Goal "[| f: W -||> univ(A);  W <= univ(A) |] ==> f : univ(A)";
   6.727 -by (eresolve_tac [FiniteFun_univ RS subsetD] 1);
   6.728 -by (assume_tac 1);
   6.729 -qed "FiniteFun_in_univ";
   6.730 -
   6.731 -(*Remove <= from the rule above*)
   6.732 -bind_thm ("FiniteFun_in_univ'", subsetI RSN (2, FiniteFun_in_univ));
   6.733 -
   6.734 -
   6.735 -(**** For QUniv.  Properties of Vfrom analogous to the "take-lemma" ****)
   6.736 -
   6.737 -(*** Intersecting a*b with Vfrom... ***)
   6.738 -
   6.739 -(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
   6.740 -Goal "[| {a,b} : Vfrom(X,succ(i));  Transset(X) |]  \
   6.741 -\     ==> a: Vfrom(X,i)  &  b: Vfrom(X,i)";
   6.742 -by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
   6.743 -by (assume_tac 1);
   6.744 -by (Fast_tac 1);
   6.745 -qed "doubleton_in_Vfrom_D";
   6.746 -
   6.747 -(*This weaker version says a, b exist at the same level*)
   6.748 -bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D);
   6.749 -
   6.750 -(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
   6.751 -      implies a, b : Vfrom(X,i), which is useless for induction.
   6.752 -    Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
   6.753 -      implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
   6.754 -    The combination gives a reduction by precisely one level, which is
   6.755 -      most convenient for proofs.
   6.756 -**)
   6.757 -
   6.758 -Goalw [Pair_def]
   6.759 -    "[| <a,b> : Vfrom(X,succ(i));  Transset(X) |]  \
   6.760 -\    ==> a: Vfrom(X,i)  &  b: Vfrom(X,i)";
   6.761 -by (blast_tac (claset() addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
   6.762 -qed "Pair_in_Vfrom_D";
   6.763 -
   6.764 -Goal "Transset(X) ==>          \
   6.765 -\      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
   6.766 -by (blast_tac (claset() addSDs [Pair_in_Vfrom_D]) 1);
   6.767 -qed "product_Int_Vfrom_subset";
   6.768 -
     7.1 --- a/src/ZF/Univ.thy	Fri May 17 16:54:25 2002 +0200
     7.2 +++ b/src/ZF/Univ.thy	Sat May 18 20:08:17 2002 +0200
     7.3 @@ -11,30 +11,885 @@
     7.4    But Ind_Syntax.univ refers to the constant "Univ.univ"
     7.5  *)
     7.6  
     7.7 -Univ = Epsilon + Sum + Finite + mono +
     7.8 +theory Univ = Epsilon + Sum + Finite + mono:
     7.9  
    7.10 -consts
    7.11 -    Vfrom       :: [i,i]=>i
    7.12 -    Vset        :: i=>i
    7.13 -    Vrec        :: [i, [i,i]=>i] =>i
    7.14 -    Vrecursor   :: [[i,i]=>i, i] =>i
    7.15 -    univ        :: i=>i
    7.16 +constdefs
    7.17 +  Vfrom       :: "[i,i]=>i"
    7.18 +    "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
    7.19  
    7.20 +syntax   Vset        :: "i=>i"
    7.21  translations
    7.22      "Vset(x)"   ==      "Vfrom(0,x)"
    7.23  
    7.24  
    7.25 -defs
    7.26 -    Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
    7.27 +constdefs
    7.28 +  Vrec        :: "[i, [i,i]=>i] =>i"
    7.29 +    "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
    7.30 + 		 	   H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
    7.31 +
    7.32 +  Vrecursor   :: "[[i,i]=>i, i] =>i"
    7.33 +    "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
    7.34 +				H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
    7.35 +
    7.36 +  univ        :: "i=>i"
    7.37 +    "univ(A) == Vfrom(A,nat)"
    7.38 +
    7.39 +
    7.40 +text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
    7.41 +lemma Vfrom: "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))"
    7.42 +apply (subst Vfrom_def [THEN def_transrec])
    7.43 +apply simp
    7.44 +done
    7.45 +
    7.46 +subsubsection{* Monotonicity *}
    7.47 +
    7.48 +lemma Vfrom_mono [rule_format]:
    7.49 +     "A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)"
    7.50 +apply (rule_tac a=i in eps_induct)
    7.51 +apply (rule impI [THEN allI])
    7.52 +apply (subst Vfrom)
    7.53 +apply (subst Vfrom)
    7.54 +apply (erule Un_mono)
    7.55 +apply (erule UN_mono, blast) 
    7.56 +done
    7.57 +
    7.58 +
    7.59 +subsubsection{* A fundamental equality: Vfrom does not require ordinals! *}
    7.60 +
    7.61 +lemma Vfrom_rank_subset1: "Vfrom(A,x) <= Vfrom(A,rank(x))"
    7.62 +apply (rule_tac a=x in eps_induct)
    7.63 +apply (subst Vfrom)
    7.64 +apply (subst Vfrom)
    7.65 +apply (blast intro!: rank_lt [THEN ltD])
    7.66 +done
    7.67 +
    7.68 +lemma Vfrom_rank_subset2: "Vfrom(A,rank(x)) <= Vfrom(A,x)"
    7.69 +apply (rule_tac a=x in eps_induct)
    7.70 +apply (subst Vfrom)
    7.71 +apply (subst Vfrom)
    7.72 +apply (rule subset_refl [THEN Un_mono])
    7.73 +apply (rule UN_least)
    7.74 +txt{*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*}
    7.75 +apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E])
    7.76 +apply (rule subset_trans)
    7.77 +apply (erule_tac [2] UN_upper)
    7.78 +apply (rule subset_refl [THEN Vfrom_mono, THEN subset_trans, THEN Pow_mono])
    7.79 +apply (erule ltI [THEN le_imp_subset])
    7.80 +apply (rule Ord_rank [THEN Ord_succ])
    7.81 +apply (erule bspec, assumption)
    7.82 +done
    7.83 +
    7.84 +lemma Vfrom_rank_eq: "Vfrom(A,rank(x)) = Vfrom(A,x)"
    7.85 +apply (rule equalityI)
    7.86 +apply (rule Vfrom_rank_subset2)
    7.87 +apply (rule Vfrom_rank_subset1)
    7.88 +done
    7.89 +
    7.90 +
    7.91 +subsection{* Basic closure properties *}
    7.92 +
    7.93 +lemma zero_in_Vfrom: "y:x ==> 0 : Vfrom(A,x)"
    7.94 +by (subst Vfrom, blast)
    7.95 +
    7.96 +lemma i_subset_Vfrom: "i <= Vfrom(A,i)"
    7.97 +apply (rule_tac a=i in eps_induct)
    7.98 +apply (subst Vfrom, blast)
    7.99 +done
   7.100 +
   7.101 +lemma A_subset_Vfrom: "A <= Vfrom(A,i)"
   7.102 +apply (subst Vfrom)
   7.103 +apply (rule Un_upper1)
   7.104 +done
   7.105 +
   7.106 +lemmas A_into_Vfrom = A_subset_Vfrom [THEN subsetD]
   7.107 +
   7.108 +lemma subset_mem_Vfrom: "a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))"
   7.109 +by (subst Vfrom, blast)
   7.110 +
   7.111 +subsubsection{* Finite sets and ordered pairs *}
   7.112 +
   7.113 +lemma singleton_in_Vfrom: "a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))"
   7.114 +by (rule subset_mem_Vfrom, safe)
   7.115 +
   7.116 +lemma doubleton_in_Vfrom:
   7.117 +     "[| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))"
   7.118 +by (rule subset_mem_Vfrom, safe)
   7.119 +
   7.120 +lemma Pair_in_Vfrom:
   7.121 +    "[| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> <a,b> : Vfrom(A,succ(succ(i)))"
   7.122 +apply (unfold Pair_def)
   7.123 +apply (blast intro: doubleton_in_Vfrom) 
   7.124 +done
   7.125 +
   7.126 +lemma succ_in_Vfrom: "a <= Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))"
   7.127 +apply (intro subset_mem_Vfrom succ_subsetI, assumption)
   7.128 +apply (erule subset_trans) 
   7.129 +apply (rule Vfrom_mono [OF subset_refl subset_succI]) 
   7.130 +done
   7.131 +
   7.132 +subsection{* 0, successor and limit equations fof Vfrom *}
   7.133 +
   7.134 +lemma Vfrom_0: "Vfrom(A,0) = A"
   7.135 +by (subst Vfrom, blast)
   7.136 +
   7.137 +lemma Vfrom_succ_lemma: "Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
   7.138 +apply (rule Vfrom [THEN trans])
   7.139 +apply (rule equalityI [THEN subst_context, 
   7.140 +                       OF _ succI1 [THEN RepFunI, THEN Union_upper]])
   7.141 +apply (rule UN_least)
   7.142 +apply (rule subset_refl [THEN Vfrom_mono, THEN Pow_mono])
   7.143 +apply (erule ltI [THEN le_imp_subset])
   7.144 +apply (erule Ord_succ)
   7.145 +done
   7.146 +
   7.147 +lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
   7.148 +apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst])
   7.149 +apply (rule_tac x1 = "i" in Vfrom_rank_eq [THEN subst])
   7.150 +apply (subst rank_succ)
   7.151 +apply (rule Ord_rank [THEN Vfrom_succ_lemma])
   7.152 +done
   7.153 +
   7.154 +(*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
   7.155 +  the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
   7.156 +lemma Vfrom_Union: "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))"
   7.157 +apply (subst Vfrom)
   7.158 +apply (rule equalityI)
   7.159 +txt{*first inclusion*}
   7.160 +apply (rule Un_least)
   7.161 +apply (rule A_subset_Vfrom [THEN subset_trans])
   7.162 +apply (rule UN_upper, assumption)
   7.163 +apply (rule UN_least)
   7.164 +apply (erule UnionE)
   7.165 +apply (rule subset_trans)
   7.166 +apply (erule_tac [2] UN_upper,
   7.167 +       subst Vfrom, erule subset_trans [OF UN_upper Un_upper2])
   7.168 +txt{*opposite inclusion*}
   7.169 +apply (rule UN_least)
   7.170 +apply (subst Vfrom, blast)
   7.171 +done
   7.172 +
   7.173 +subsection{* Vfrom applied to Limit ordinals *}
   7.174 +
   7.175 +(*NB. limit ordinals are non-empty:
   7.176 +      Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
   7.177 +lemma Limit_Vfrom_eq:
   7.178 +    "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))"
   7.179 +apply (rule Limit_has_0 [THEN ltD, THEN Vfrom_Union, THEN subst], assumption)
   7.180 +apply (simp add: Limit_Union_eq) 
   7.181 +done
   7.182 +
   7.183 +lemma Limit_VfromI: "[| a: Vfrom(A,j);  Limit(i);  j<i |] ==> a : Vfrom(A,i)"
   7.184 +apply (rule Limit_Vfrom_eq [THEN equalityD2, THEN subsetD], assumption)
   7.185 +apply (blast intro: ltD) 
   7.186 +done
   7.187 +
   7.188 +lemma Limit_VfromE:
   7.189 +    "[| a: Vfrom(A,i);  ~R ==> Limit(i);
   7.190 +        !!x. [| x<i;  a: Vfrom(A,x) |] ==> R
   7.191 +     |] ==> R"
   7.192 +apply (rule classical)
   7.193 +apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
   7.194 +prefer 2 apply assumption
   7.195 +apply blast 
   7.196 +apply (blast intro: ltI  Limit_is_Ord)
   7.197 +done
   7.198 +
   7.199 +lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
   7.200 +
   7.201 +lemma singleton_in_VLimit:
   7.202 +    "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)"
   7.203 +apply (erule Limit_VfromE, assumption)
   7.204 +apply (erule singleton_in_Vfrom [THEN Limit_VfromI], assumption)
   7.205 +apply (blast intro: Limit_has_succ) 
   7.206 +done
   7.207 +
   7.208 +lemmas Vfrom_UnI1 = 
   7.209 +    Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard]
   7.210 +lemmas Vfrom_UnI2 = 
   7.211 +    Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard]
   7.212 +
   7.213 +text{*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*}
   7.214 +lemma doubleton_in_VLimit:
   7.215 +    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> {a,b} : Vfrom(A,i)"
   7.216 +apply (erule Limit_VfromE, assumption)
   7.217 +apply (erule Limit_VfromE, assumption)
   7.218 +apply (blast intro:  Limit_VfromI [OF doubleton_in_Vfrom]
   7.219 +                     Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
   7.220 +done
   7.221 +
   7.222 +lemma Pair_in_VLimit:
   7.223 +    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> <a,b> : Vfrom(A,i)"
   7.224 +txt{*Infer that a, b occur at ordinals x,xa < i.*}
   7.225 +apply (erule Limit_VfromE, assumption)
   7.226 +apply (erule Limit_VfromE, assumption)
   7.227 +txt{*Infer that succ(succ(x Un xa)) < i *}
   7.228 +apply (blast intro:  Limit_VfromI [OF Pair_in_Vfrom]
   7.229 +                     Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
   7.230 +done
   7.231 +
   7.232 +lemma product_VLimit: "Limit(i) ==> Vfrom(A,i) * Vfrom(A,i) <= Vfrom(A,i)"
   7.233 +by (blast intro: Pair_in_VLimit)
   7.234 +
   7.235 +lemmas Sigma_subset_VLimit =
   7.236 +     subset_trans [OF Sigma_mono product_VLimit]
   7.237 +
   7.238 +lemmas nat_subset_VLimit =
   7.239 +     subset_trans [OF nat_le_Limit [THEN le_imp_subset] i_subset_Vfrom]
   7.240 +
   7.241 +lemma nat_into_VLimit: "[| n: nat;  Limit(i) |] ==> n : Vfrom(A,i)"
   7.242 +by (blast intro: nat_subset_VLimit [THEN subsetD])
   7.243 +
   7.244 +subsubsection{* Closure under disjoint union *}
   7.245 +
   7.246 +lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
   7.247 +
   7.248 +lemma one_in_VLimit: "Limit(i) ==> 1 : Vfrom(A,i)"
   7.249 +by (blast intro: nat_into_VLimit)
   7.250 +
   7.251 +lemma Inl_in_VLimit:
   7.252 +    "[| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)"
   7.253 +apply (unfold Inl_def)
   7.254 +apply (blast intro: zero_in_VLimit Pair_in_VLimit)
   7.255 +done
   7.256 +
   7.257 +lemma Inr_in_VLimit:
   7.258 +    "[| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)"
   7.259 +apply (unfold Inr_def)
   7.260 +apply (blast intro: one_in_VLimit Pair_in_VLimit)
   7.261 +done
   7.262 +
   7.263 +lemma sum_VLimit: "Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)"
   7.264 +by (blast intro!: Inl_in_VLimit Inr_in_VLimit)
   7.265 +
   7.266 +lemmas sum_subset_VLimit = subset_trans [OF sum_mono sum_VLimit]
   7.267 +
   7.268 +
   7.269 +
   7.270 +subsection{* Properties assuming Transset(A) *}
   7.271 +
   7.272 +lemma Transset_Vfrom: "Transset(A) ==> Transset(Vfrom(A,i))"
   7.273 +apply (rule_tac a=i in eps_induct)
   7.274 +apply (subst Vfrom)
   7.275 +apply (blast intro!: Transset_Union_family Transset_Un Transset_Pow)
   7.276 +done
   7.277 +
   7.278 +lemma Transset_Vfrom_succ:
   7.279 +     "Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))"
   7.280 +apply (rule Vfrom_succ [THEN trans])
   7.281 +apply (rule equalityI [OF _ Un_upper2])
   7.282 +apply (rule Un_least [OF _ subset_refl])
   7.283 +apply (rule A_subset_Vfrom [THEN subset_trans])
   7.284 +apply (erule Transset_Vfrom [THEN Transset_iff_Pow [THEN iffD1]])
   7.285 +done
   7.286 +
   7.287 +lemma Transset_Pair_subset: "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C"
   7.288 +by (unfold Pair_def Transset_def, blast)
   7.289 +
   7.290 +lemma Transset_Pair_subset_VLimit:
   7.291 +     "[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |]
   7.292 +      ==> <a,b> : Vfrom(A,i)"
   7.293 +apply (erule Transset_Pair_subset [THEN conjE])
   7.294 +apply (erule Transset_Vfrom)
   7.295 +apply (blast intro: Pair_in_VLimit)
   7.296 +done
   7.297 +
   7.298 +lemma Union_in_Vfrom:
   7.299 +     "[| X: Vfrom(A,j);  Transset(A) |] ==> Union(X) : Vfrom(A, succ(j))"
   7.300 +apply (drule Transset_Vfrom)
   7.301 +apply (rule subset_mem_Vfrom)
   7.302 +apply (unfold Transset_def, blast)
   7.303 +done
   7.304 +
   7.305 +lemma Union_in_VLimit:
   7.306 +     "[| X: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Union(X) : Vfrom(A,i)"
   7.307 +apply (rule Limit_VfromE, assumption+)
   7.308 +apply (blast intro: Limit_has_succ Limit_VfromI Union_in_Vfrom)
   7.309 +done
   7.310 +
   7.311 +
   7.312 +(*** Closure under product/sum applied to elements -- thus Vfrom(A,i)
   7.313 +     is a model of simple type theory provided A is a transitive set
   7.314 +     and i is a limit ordinal
   7.315 +***)
   7.316 +
   7.317 +text{*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*}
   7.318 +lemma in_VLimit:
   7.319 +  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);
   7.320 +      !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) |]
   7.321 +               ==> EX k. h(x,y): Vfrom(A,k) & k<i |]
   7.322 +   ==> h(a,b) : Vfrom(A,i)"
   7.323 +txt{*Infer that a, b occur at ordinals x,xa < i.*}
   7.324 +apply (erule Limit_VfromE, assumption)
   7.325 +apply (erule Limit_VfromE, assumption, atomize)
   7.326 +apply (drule_tac x=a in spec) 
   7.327 +apply (drule_tac x=b in spec) 
   7.328 +apply (drule_tac x="x Un xa Un 2" in spec) 
   7.329 +txt{*FIXME: can do better using simprule about Un and <*}
   7.330 +apply (simp add: Vfrom_UnI2 [THEN Vfrom_UnI1] Vfrom_UnI1 [THEN Vfrom_UnI1]) 
   7.331 +apply (blast intro: Limit_has_0 Limit_has_succ Un_least_lt Limit_VfromI)
   7.332 +done
   7.333 +
   7.334 +subsubsection{* products *}
   7.335 +
   7.336 +lemma prod_in_Vfrom:
   7.337 +    "[| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |]
   7.338 +     ==> a*b : Vfrom(A, succ(succ(succ(j))))"
   7.339 +apply (drule Transset_Vfrom)
   7.340 +apply (rule subset_mem_Vfrom)
   7.341 +apply (unfold Transset_def)
   7.342 +apply (blast intro: Pair_in_Vfrom)
   7.343 +done
   7.344 +
   7.345 +lemma prod_in_VLimit:
   7.346 +  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |]
   7.347 +   ==> a*b : Vfrom(A,i)"
   7.348 +apply (erule in_VLimit, assumption+)
   7.349 +apply (blast intro: prod_in_Vfrom Limit_has_succ)
   7.350 +done
   7.351 +
   7.352 +subsubsection{* Disjoint sums, aka Quine ordered pairs *}
   7.353 +
   7.354 +lemma sum_in_Vfrom:
   7.355 +    "[| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A);  1:j |]
   7.356 +     ==> a+b : Vfrom(A, succ(succ(succ(j))))"
   7.357 +apply (unfold sum_def)
   7.358 +apply (drule Transset_Vfrom)
   7.359 +apply (rule subset_mem_Vfrom)
   7.360 +apply (unfold Transset_def)
   7.361 +apply (blast intro: zero_in_Vfrom Pair_in_Vfrom i_subset_Vfrom [THEN subsetD])
   7.362 +done
   7.363 +
   7.364 +lemma sum_in_VLimit:
   7.365 +  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |]
   7.366 +   ==> a+b : Vfrom(A,i)"
   7.367 +apply (erule in_VLimit, assumption+)
   7.368 +apply (blast intro: sum_in_Vfrom Limit_has_succ)
   7.369 +done
   7.370 +
   7.371 +subsubsection{* function space! *}
   7.372 +
   7.373 +lemma fun_in_Vfrom:
   7.374 +    "[| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==>
   7.375 +          a->b : Vfrom(A, succ(succ(succ(succ(j)))))"
   7.376 +apply (unfold Pi_def)
   7.377 +apply (drule Transset_Vfrom)
   7.378 +apply (rule subset_mem_Vfrom)
   7.379 +apply (rule Collect_subset [THEN subset_trans])
   7.380 +apply (subst Vfrom)
   7.381 +apply (rule subset_trans [THEN subset_trans])
   7.382 +apply (rule_tac [3] Un_upper2)
   7.383 +apply (rule_tac [2] succI1 [THEN UN_upper])
   7.384 +apply (rule Pow_mono)
   7.385 +apply (unfold Transset_def)
   7.386 +apply (blast intro: Pair_in_Vfrom)
   7.387 +done
   7.388 +
   7.389 +lemma fun_in_VLimit:
   7.390 +  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |]
   7.391 +   ==> a->b : Vfrom(A,i)"
   7.392 +apply (erule in_VLimit, assumption+)
   7.393 +apply (blast intro: fun_in_Vfrom Limit_has_succ)
   7.394 +done
   7.395 +
   7.396 +lemma Pow_in_Vfrom:
   7.397 +    "[| a: Vfrom(A,j);  Transset(A) |] ==> Pow(a) : Vfrom(A, succ(succ(j)))"
   7.398 +apply (drule Transset_Vfrom)
   7.399 +apply (rule subset_mem_Vfrom)
   7.400 +apply (unfold Transset_def)
   7.401 +apply (subst Vfrom, blast)
   7.402 +done
   7.403 +
   7.404 +lemma Pow_in_VLimit:
   7.405 +     "[| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)"
   7.406 +by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom Limit_VfromI)
   7.407 +
   7.408 +
   7.409 +subsection{* The set Vset(i) *}
   7.410 +
   7.411 +lemma Vset: "Vset(i) = (UN j:i. Pow(Vset(j)))"
   7.412 +by (subst Vfrom, blast)
   7.413 +
   7.414 +lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard]
   7.415 +lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard]
   7.416 +
   7.417 +subsubsection{* Characterisation of the elements of Vset(i) *}
   7.418 +
   7.419 +lemma VsetD [rule_format]: "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i"
   7.420 +apply (erule trans_induct)
   7.421 +apply (subst Vset, safe)
   7.422 +apply (subst rank)
   7.423 +apply (blast intro: ltI UN_succ_least_lt) 
   7.424 +done
   7.425 +
   7.426 +lemma VsetI_lemma [rule_format]:
   7.427 +     "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)"
   7.428 +apply (erule trans_induct)
   7.429 +apply (rule allI)
   7.430 +apply (subst Vset)
   7.431 +apply (blast intro!: rank_lt [THEN ltD])
   7.432 +done
   7.433 +
   7.434 +lemma VsetI: "rank(x)<i ==> x : Vset(i)"
   7.435 +by (blast intro: VsetI_lemma elim: ltE)
   7.436 +
   7.437 +text{*Merely a lemma for the next result*}
   7.438 +lemma Vset_Ord_rank_iff: "Ord(i) ==> b : Vset(i) <-> rank(b) < i"
   7.439 +by (blast intro: VsetD VsetI)
   7.440 +
   7.441 +lemma Vset_rank_iff [simp]: "b : Vset(a) <-> rank(b) < rank(a)"
   7.442 +apply (rule Vfrom_rank_eq [THEN subst])
   7.443 +apply (rule Ord_rank [THEN Vset_Ord_rank_iff])
   7.444 +done
   7.445 +
   7.446 +text{*This is rank(rank(a)) = rank(a) *}
   7.447 +declare Ord_rank [THEN rank_of_Ord, simp]
   7.448 +
   7.449 +lemma rank_Vset: "Ord(i) ==> rank(Vset(i)) = i"
   7.450 +apply (subst rank)
   7.451 +apply (rule equalityI, safe)
   7.452 +apply (blast intro: VsetD [THEN ltD]) 
   7.453 +apply (blast intro: VsetD [THEN ltD] Ord_trans) 
   7.454 +apply (blast intro: i_subset_Vfrom [THEN subsetD]
   7.455 +                    Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
   7.456 +done
   7.457 +
   7.458 +subsubsection{* Lemmas for reasoning about sets in terms of their elements' ranks *}
   7.459  
   7.460 -    Vrec_def
   7.461 -        "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
   7.462 -                             H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
   7.463 +lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
   7.464 +apply (rule subsetI)
   7.465 +apply (erule rank_lt [THEN VsetI])
   7.466 +done
   7.467 +
   7.468 +lemma Int_Vset_subset:
   7.469 +    "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b"
   7.470 +apply (rule subset_trans) 
   7.471 +apply (rule Int_greatest [OF subset_refl arg_subset_Vset_rank])
   7.472 +apply (blast intro: Ord_rank) 
   7.473 +done
   7.474 +
   7.475 +subsubsection{* Set up an environment for simplification *}
   7.476 +
   7.477 +lemma rank_Inl: "rank(a) < rank(Inl(a))"
   7.478 +apply (unfold Inl_def)
   7.479 +apply (rule rank_pair2)
   7.480 +done
   7.481 +
   7.482 +lemma rank_Inr: "rank(a) < rank(Inr(a))"
   7.483 +apply (unfold Inr_def)
   7.484 +apply (rule rank_pair2)
   7.485 +done
   7.486 +
   7.487 +lemmas rank_rls = rank_Inl rank_Inr rank_pair1 rank_pair2
   7.488 +
   7.489 +subsubsection{* Recursion over Vset levels! *}
   7.490 +
   7.491 +text{*NOT SUITABLE FOR REWRITING: recursive!*}
   7.492 +lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
   7.493 +apply (unfold Vrec_def)
   7.494 +apply (subst transrec)
   7.495 +apply simp
   7.496 +apply (rule refl [THEN lam_cong, THEN subst_context], simp)
   7.497 +done
   7.498 +
   7.499 +text{*This form avoids giant explosions in proofs.  NOTE USE OF == *}
   7.500 +lemma def_Vrec:
   7.501 +    "[| !!x. h(x)==Vrec(x,H) |] ==>
   7.502 +     h(a) = H(a, lam x: Vset(rank(a)). h(x))"
   7.503 +apply simp 
   7.504 +apply (rule Vrec)
   7.505 +done
   7.506 +
   7.507 +text{*NOT SUITABLE FOR REWRITING: recursive!*}
   7.508 +lemma Vrecursor:
   7.509 +     "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x),  a)"
   7.510 +apply (unfold Vrecursor_def)
   7.511 +apply (subst transrec, simp)
   7.512 +apply (rule refl [THEN lam_cong, THEN subst_context], simp)
   7.513 +done
   7.514 +
   7.515 +text{*This form avoids giant explosions in proofs.  NOTE USE OF == *}
   7.516 +lemma def_Vrecursor:
   7.517 +     "h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x),  a)"
   7.518 +apply simp
   7.519 +apply (rule Vrecursor)
   7.520 +done
   7.521 +
   7.522 +
   7.523 +subsection{* univ(A) *}
   7.524 +
   7.525 +lemma univ_mono: "A<=B ==> univ(A) <= univ(B)"
   7.526 +apply (unfold univ_def)
   7.527 +apply (erule Vfrom_mono)
   7.528 +apply (rule subset_refl)
   7.529 +done
   7.530 +
   7.531 +lemma Transset_univ: "Transset(A) ==> Transset(univ(A))"
   7.532 +apply (unfold univ_def)
   7.533 +apply (erule Transset_Vfrom)
   7.534 +done
   7.535 +
   7.536 +subsubsection{* univ(A) as a limit *}
   7.537 +
   7.538 +lemma univ_eq_UN: "univ(A) = (UN i:nat. Vfrom(A,i))"
   7.539 +apply (unfold univ_def)
   7.540 +apply (rule Limit_nat [THEN Limit_Vfrom_eq])
   7.541 +done
   7.542 +
   7.543 +lemma subset_univ_eq_Int: "c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))"
   7.544 +apply (rule subset_UN_iff_eq [THEN iffD1])
   7.545 +apply (erule univ_eq_UN [THEN subst])
   7.546 +done
   7.547 +
   7.548 +lemma univ_Int_Vfrom_subset:
   7.549 +    "[| a <= univ(X);
   7.550 +        !!i. i:nat ==> a Int Vfrom(X,i) <= b |]
   7.551 +     ==> a <= b"
   7.552 +apply (subst subset_univ_eq_Int, assumption)
   7.553 +apply (rule UN_least, simp) 
   7.554 +done
   7.555 +
   7.556 +lemma univ_Int_Vfrom_eq:
   7.557 +    "[| a <= univ(X);   b <= univ(X);
   7.558 +        !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i)
   7.559 +     |] ==> a = b"
   7.560 +apply (rule equalityI)
   7.561 +apply (rule univ_Int_Vfrom_subset, assumption)
   7.562 +apply (blast elim: equalityCE) 
   7.563 +apply (rule univ_Int_Vfrom_subset, assumption)
   7.564 +apply (blast elim: equalityCE) 
   7.565 +done
   7.566 +
   7.567 +subsubsection{* Closure properties *}
   7.568 +
   7.569 +lemma zero_in_univ: "0 : univ(A)"
   7.570 +apply (unfold univ_def)
   7.571 +apply (rule nat_0I [THEN zero_in_Vfrom])
   7.572 +done
   7.573 +
   7.574 +lemma A_subset_univ: "A <= univ(A)"
   7.575 +apply (unfold univ_def)
   7.576 +apply (rule A_subset_Vfrom)
   7.577 +done
   7.578 +
   7.579 +lemmas A_into_univ = A_subset_univ [THEN subsetD, standard]
   7.580 +
   7.581 +subsubsection{* Closure under unordered and ordered pairs *}
   7.582 +
   7.583 +lemma singleton_in_univ: "a: univ(A) ==> {a} : univ(A)"
   7.584 +apply (unfold univ_def)
   7.585 +apply (blast intro: singleton_in_VLimit Limit_nat)
   7.586 +done
   7.587 +
   7.588 +lemma doubleton_in_univ:
   7.589 +    "[| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)"
   7.590 +apply (unfold univ_def)
   7.591 +apply (blast intro: doubleton_in_VLimit Limit_nat)
   7.592 +done
   7.593 +
   7.594 +lemma Pair_in_univ:
   7.595 +    "[| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)"
   7.596 +apply (unfold univ_def)
   7.597 +apply (blast intro: Pair_in_VLimit Limit_nat)
   7.598 +done
   7.599 +
   7.600 +lemma Union_in_univ:
   7.601 +     "[| X: univ(A);  Transset(A) |] ==> Union(X) : univ(A)"
   7.602 +apply (unfold univ_def)
   7.603 +apply (blast intro: Union_in_VLimit Limit_nat)
   7.604 +done
   7.605 +
   7.606 +lemma product_univ: "univ(A)*univ(A) <= univ(A)"
   7.607 +apply (unfold univ_def)
   7.608 +apply (rule Limit_nat [THEN product_VLimit])
   7.609 +done
   7.610 +
   7.611 +
   7.612 +subsubsection{* The natural numbers *}
   7.613 +
   7.614 +lemma nat_subset_univ: "nat <= univ(A)"
   7.615 +apply (unfold univ_def)
   7.616 +apply (rule i_subset_Vfrom)
   7.617 +done
   7.618 +
   7.619 +text{* n:nat ==> n:univ(A) *}
   7.620 +lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard]
   7.621 +
   7.622 +subsubsection{* instances for 1 and 2 *}
   7.623 +
   7.624 +lemma one_in_univ: "1 : univ(A)"
   7.625 +apply (unfold univ_def)
   7.626 +apply (rule Limit_nat [THEN one_in_VLimit])
   7.627 +done
   7.628 +
   7.629 +text{*unused!*}
   7.630 +lemma two_in_univ: "2 : univ(A)"
   7.631 +by (blast intro: nat_into_univ)
   7.632 +
   7.633 +lemma bool_subset_univ: "bool <= univ(A)"
   7.634 +apply (unfold bool_def)
   7.635 +apply (blast intro!: zero_in_univ one_in_univ)
   7.636 +done
   7.637 +
   7.638 +lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard]
   7.639 +
   7.640 +
   7.641 +subsubsection{* Closure under disjoint union *}
   7.642 +
   7.643 +lemma Inl_in_univ: "a: univ(A) ==> Inl(a) : univ(A)"
   7.644 +apply (unfold univ_def)
   7.645 +apply (erule Inl_in_VLimit [OF _ Limit_nat])
   7.646 +done
   7.647 +
   7.648 +lemma Inr_in_univ: "b: univ(A) ==> Inr(b) : univ(A)"
   7.649 +apply (unfold univ_def)
   7.650 +apply (erule Inr_in_VLimit [OF _ Limit_nat])
   7.651 +done
   7.652 +
   7.653 +lemma sum_univ: "univ(C)+univ(C) <= univ(C)"
   7.654 +apply (unfold univ_def)
   7.655 +apply (rule Limit_nat [THEN sum_VLimit])
   7.656 +done
   7.657 +
   7.658 +lemmas sum_subset_univ = subset_trans [OF sum_mono sum_univ]
   7.659 +
   7.660 +
   7.661 +subsubsection{* Closure under binary union -- use Un_least *}
   7.662 +subsubsection{* Closure under Collect -- use  (Collect_subset RS subset_trans)  *}
   7.663 +subsubsection{* Closure under RepFun -- use   RepFun_subset  *}
   7.664 +
   7.665 +
   7.666 +subsection{* Finite Branching Closure Properties *}
   7.667 +
   7.668 +subsubsection{* Closure under finite powerset *}
   7.669 +
   7.670 +lemma Fin_Vfrom_lemma:
   7.671 +     "[| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i"
   7.672 +apply (erule Fin_induct)
   7.673 +apply (blast dest!: Limit_has_0, safe)
   7.674 +apply (erule Limit_VfromE, assumption)
   7.675 +apply (blast intro!: Un_least_lt intro: Vfrom_UnI1 Vfrom_UnI2)
   7.676 +done
   7.677  
   7.678 -    Vrecursor_def
   7.679 -        "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
   7.680 -                                    H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
   7.681 +lemma Fin_VLimit: "Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)"
   7.682 +apply (rule subsetI)
   7.683 +apply (drule Fin_Vfrom_lemma, safe)
   7.684 +apply (rule Vfrom [THEN ssubst])
   7.685 +apply (blast dest!: ltD)
   7.686 +done
   7.687 +
   7.688 +lemmas Fin_subset_VLimit = subset_trans [OF Fin_mono Fin_VLimit]
   7.689 +
   7.690 +lemma Fin_univ: "Fin(univ(A)) <= univ(A)"
   7.691 +apply (unfold univ_def)
   7.692 +apply (rule Limit_nat [THEN Fin_VLimit])
   7.693 +done
   7.694 +
   7.695 +subsubsection{* Closure under finite powers (functions from a fixed natural number) *}
   7.696 +
   7.697 +lemma nat_fun_VLimit:
   7.698 +     "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"
   7.699 +apply (erule nat_fun_subset_Fin [THEN subset_trans])
   7.700 +apply (blast del: subsetI
   7.701 +    intro: subset_refl Fin_subset_VLimit Sigma_subset_VLimit nat_subset_VLimit)
   7.702 +done
   7.703 +
   7.704 +lemmas nat_fun_subset_VLimit = subset_trans [OF Pi_mono nat_fun_VLimit]
   7.705 +
   7.706 +lemma nat_fun_univ: "n: nat ==> n -> univ(A) <= univ(A)"
   7.707 +apply (unfold univ_def)
   7.708 +apply (erule nat_fun_VLimit [OF _ Limit_nat])
   7.709 +done
   7.710 +
   7.711 +
   7.712 +subsubsection{* Closure under finite function space *}
   7.713 +
   7.714 +text{*General but seldom-used version; normally the domain is fixed*}
   7.715 +lemma FiniteFun_VLimit1:
   7.716 +     "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)"
   7.717 +apply (rule FiniteFun.dom_subset [THEN subset_trans])
   7.718 +apply (blast del: subsetI
   7.719 +             intro: Fin_subset_VLimit Sigma_subset_VLimit subset_refl)
   7.720 +done
   7.721 +
   7.722 +lemma FiniteFun_univ1: "univ(A) -||> univ(A) <= univ(A)"
   7.723 +apply (unfold univ_def)
   7.724 +apply (rule Limit_nat [THEN FiniteFun_VLimit1])
   7.725 +done
   7.726 +
   7.727 +text{*Version for a fixed domain*}
   7.728 +lemma FiniteFun_VLimit:
   7.729 +     "[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)"
   7.730 +apply (rule subset_trans) 
   7.731 +apply (erule FiniteFun_mono [OF _ subset_refl])
   7.732 +apply (erule FiniteFun_VLimit1)
   7.733 +done
   7.734 +
   7.735 +lemma FiniteFun_univ:
   7.736 +    "W <= univ(A) ==> W -||> univ(A) <= univ(A)"
   7.737 +apply (unfold univ_def)
   7.738 +apply (erule FiniteFun_VLimit [OF _ Limit_nat])
   7.739 +done
   7.740 +
   7.741 +lemma FiniteFun_in_univ:
   7.742 +     "[| f: W -||> univ(A);  W <= univ(A) |] ==> f : univ(A)"
   7.743 +by (erule FiniteFun_univ [THEN subsetD], assumption)
   7.744 +
   7.745 +text{*Remove <= from the rule above*}
   7.746 +lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI]
   7.747 +
   7.748 +
   7.749 +subsection{** For QUniv.  Properties of Vfrom analogous to the "take-lemma" **}
   7.750 +
   7.751 +subsection{* Intersecting a*b with Vfrom... *}
   7.752 +
   7.753 +text{*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*}
   7.754 +lemma doubleton_in_Vfrom_D:
   7.755 +     "[| {a,b} : Vfrom(X,succ(i));  Transset(X) |]
   7.756 +      ==> a: Vfrom(X,i)  &  b: Vfrom(X,i)"
   7.757 +by (drule Transset_Vfrom_succ [THEN equalityD1, THEN subsetD, THEN PowD], 
   7.758 +    assumption, fast)
   7.759 +
   7.760 +text{*This weaker version says a, b exist at the same level*}
   7.761 +lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D, standard]
   7.762 +
   7.763 +(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
   7.764 +      implies a, b : Vfrom(X,i), which is useless for induction.
   7.765 +    Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
   7.766 +      implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
   7.767 +    The combination gives a reduction by precisely one level, which is
   7.768 +      most convenient for proofs.
   7.769 +**)
   7.770 +
   7.771 +lemma Pair_in_Vfrom_D:
   7.772 +    "[| <a,b> : Vfrom(X,succ(i));  Transset(X) |]
   7.773 +     ==> a: Vfrom(X,i)  &  b: Vfrom(X,i)"
   7.774 +apply (unfold Pair_def)
   7.775 +apply (blast dest!: doubleton_in_Vfrom_D Vfrom_doubleton_D)
   7.776 +done
   7.777 +
   7.778 +lemma product_Int_Vfrom_subset:
   7.779 +     "Transset(X) ==>
   7.780 +      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))"
   7.781 +by (blast dest!: Pair_in_Vfrom_D)
   7.782 +
   7.783 +
   7.784 +ML
   7.785 +{*
   7.786  
   7.787 -    univ_def    "univ(A) == Vfrom(A,nat)"
   7.788 +val Vfrom = thm "Vfrom";
   7.789 +val Vfrom_mono = thm "Vfrom_mono";
   7.790 +val Vfrom_rank_subset1 = thm "Vfrom_rank_subset1";
   7.791 +val Vfrom_rank_subset2 = thm "Vfrom_rank_subset2";
   7.792 +val Vfrom_rank_eq = thm "Vfrom_rank_eq";
   7.793 +val zero_in_Vfrom = thm "zero_in_Vfrom";
   7.794 +val i_subset_Vfrom = thm "i_subset_Vfrom";
   7.795 +val A_subset_Vfrom = thm "A_subset_Vfrom";
   7.796 +val subset_mem_Vfrom = thm "subset_mem_Vfrom";
   7.797 +val singleton_in_Vfrom = thm "singleton_in_Vfrom";
   7.798 +val doubleton_in_Vfrom = thm "doubleton_in_Vfrom";
   7.799 +val Pair_in_Vfrom = thm "Pair_in_Vfrom";
   7.800 +val succ_in_Vfrom = thm "succ_in_Vfrom";
   7.801 +val Vfrom_0 = thm "Vfrom_0";
   7.802 +val Vfrom_succ_lemma = thm "Vfrom_succ_lemma";
   7.803 +val Vfrom_succ = thm "Vfrom_succ";
   7.804 +val Vfrom_Union = thm "Vfrom_Union";
   7.805 +val Limit_Vfrom_eq = thm "Limit_Vfrom_eq";
   7.806 +val Limit_VfromI = thm "Limit_VfromI";
   7.807 +val Limit_VfromE = thm "Limit_VfromE";
   7.808 +val zero_in_VLimit = thm "zero_in_VLimit";
   7.809 +val singleton_in_VLimit = thm "singleton_in_VLimit";
   7.810 +val Vfrom_UnI1 = thm "Vfrom_UnI1";
   7.811 +val Vfrom_UnI2 = thm "Vfrom_UnI2";
   7.812 +val doubleton_in_VLimit = thm "doubleton_in_VLimit";
   7.813 +val Pair_in_VLimit = thm "Pair_in_VLimit";
   7.814 +val product_VLimit = thm "product_VLimit";
   7.815 +val Sigma_subset_VLimit = thm "Sigma_subset_VLimit";
   7.816 +val nat_subset_VLimit = thm "nat_subset_VLimit";
   7.817 +val nat_into_VLimit = thm "nat_into_VLimit";
   7.818 +val zero_in_VLimit = thm "zero_in_VLimit";
   7.819 +val one_in_VLimit = thm "one_in_VLimit";
   7.820 +val Inl_in_VLimit = thm "Inl_in_VLimit";
   7.821 +val Inr_in_VLimit = thm "Inr_in_VLimit";
   7.822 +val sum_VLimit = thm "sum_VLimit";
   7.823 +val sum_subset_VLimit = thm "sum_subset_VLimit";
   7.824 +val Transset_Vfrom = thm "Transset_Vfrom";
   7.825 +val Transset_Vfrom_succ = thm "Transset_Vfrom_succ";
   7.826 +val Transset_Pair_subset = thm "Transset_Pair_subset";
   7.827 +val Transset_Pair_subset_VLimit = thm "Transset_Pair_subset_VLimit";
   7.828 +val Union_in_Vfrom = thm "Union_in_Vfrom";
   7.829 +val Union_in_VLimit = thm "Union_in_VLimit";
   7.830 +val in_VLimit = thm "in_VLimit";
   7.831 +val prod_in_Vfrom = thm "prod_in_Vfrom";
   7.832 +val prod_in_VLimit = thm "prod_in_VLimit";
   7.833 +val sum_in_Vfrom = thm "sum_in_Vfrom";
   7.834 +val sum_in_VLimit = thm "sum_in_VLimit";
   7.835 +val fun_in_Vfrom = thm "fun_in_Vfrom";
   7.836 +val fun_in_VLimit = thm "fun_in_VLimit";
   7.837 +val Pow_in_Vfrom = thm "Pow_in_Vfrom";
   7.838 +val Pow_in_VLimit = thm "Pow_in_VLimit";
   7.839 +val Vset = thm "Vset";
   7.840 +val Vset_succ = thm "Vset_succ";
   7.841 +val Transset_Vset = thm "Transset_Vset";
   7.842 +val VsetD = thm "VsetD";
   7.843 +val VsetI_lemma = thm "VsetI_lemma";
   7.844 +val VsetI = thm "VsetI";
   7.845 +val Vset_Ord_rank_iff = thm "Vset_Ord_rank_iff";
   7.846 +val Vset_rank_iff = thm "Vset_rank_iff";
   7.847 +val rank_Vset = thm "rank_Vset";
   7.848 +val arg_subset_Vset_rank = thm "arg_subset_Vset_rank";
   7.849 +val Int_Vset_subset = thm "Int_Vset_subset";
   7.850 +val rank_Inl = thm "rank_Inl";
   7.851 +val rank_Inr = thm "rank_Inr";
   7.852 +val Vrec = thm "Vrec";
   7.853 +val def_Vrec = thm "def_Vrec";
   7.854 +val Vrecursor = thm "Vrecursor";
   7.855 +val def_Vrecursor = thm "def_Vrecursor";
   7.856 +val univ_mono = thm "univ_mono";
   7.857 +val Transset_univ = thm "Transset_univ";
   7.858 +val univ_eq_UN = thm "univ_eq_UN";
   7.859 +val subset_univ_eq_Int = thm "subset_univ_eq_Int";
   7.860 +val univ_Int_Vfrom_subset = thm "univ_Int_Vfrom_subset";
   7.861 +val univ_Int_Vfrom_eq = thm "univ_Int_Vfrom_eq";
   7.862 +val zero_in_univ = thm "zero_in_univ";
   7.863 +val A_subset_univ = thm "A_subset_univ";
   7.864 +val A_into_univ = thm "A_into_univ";
   7.865 +val singleton_in_univ = thm "singleton_in_univ";
   7.866 +val doubleton_in_univ = thm "doubleton_in_univ";
   7.867 +val Pair_in_univ = thm "Pair_in_univ";
   7.868 +val Union_in_univ = thm "Union_in_univ";
   7.869 +val product_univ = thm "product_univ";
   7.870 +val nat_subset_univ = thm "nat_subset_univ";
   7.871 +val nat_into_univ = thm "nat_into_univ";
   7.872 +val one_in_univ = thm "one_in_univ";
   7.873 +val two_in_univ = thm "two_in_univ";
   7.874 +val bool_subset_univ = thm "bool_subset_univ";
   7.875 +val bool_into_univ = thm "bool_into_univ";
   7.876 +val Inl_in_univ = thm "Inl_in_univ";
   7.877 +val Inr_in_univ = thm "Inr_in_univ";
   7.878 +val sum_univ = thm "sum_univ";
   7.879 +val sum_subset_univ = thm "sum_subset_univ";
   7.880 +val Fin_Vfrom_lemma = thm "Fin_Vfrom_lemma";
   7.881 +val Fin_VLimit = thm "Fin_VLimit";
   7.882 +val Fin_subset_VLimit = thm "Fin_subset_VLimit";
   7.883 +val Fin_univ = thm "Fin_univ";
   7.884 +val nat_fun_VLimit = thm "nat_fun_VLimit";
   7.885 +val nat_fun_subset_VLimit = thm "nat_fun_subset_VLimit";
   7.886 +val nat_fun_univ = thm "nat_fun_univ";
   7.887 +val FiniteFun_VLimit1 = thm "FiniteFun_VLimit1";
   7.888 +val FiniteFun_univ1 = thm "FiniteFun_univ1";
   7.889 +val FiniteFun_VLimit = thm "FiniteFun_VLimit";
   7.890 +val FiniteFun_univ = thm "FiniteFun_univ";
   7.891 +val FiniteFun_in_univ = thm "FiniteFun_in_univ";
   7.892 +val FiniteFun_in_univ' = thm "FiniteFun_in_univ'";
   7.893 +val doubleton_in_Vfrom_D = thm "doubleton_in_Vfrom_D";
   7.894 +val Vfrom_doubleton_D = thm "Vfrom_doubleton_D";
   7.895 +val Pair_in_Vfrom_D = thm "Pair_in_Vfrom_D";
   7.896 +val product_Int_Vfrom_subset = thm "product_Int_Vfrom_subset";
   7.897 +
   7.898 +val rank_rls = thms "rank_rls";
   7.899 +val rank_ss = simpset() addsimps [VsetI] 
   7.900 +              addsimps rank_rls @ (rank_rls RLN (2, [lt_trans]));
   7.901 +
   7.902 +*}
   7.903  
   7.904  end
     8.1 --- a/src/ZF/func.ML	Fri May 17 16:54:25 2002 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,479 +0,0 @@
     8.4 -(*  Title:      ZF/func
     8.5 -    ID:         $Id$
     8.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 -    Copyright   1991  University of Cambridge
     8.8 -
     8.9 -Functions in Zermelo-Fraenkel Set Theory
    8.10 -*)
    8.11 -
    8.12 -(*** The Pi operator -- dependent function space ***)
    8.13 -
    8.14 -Goalw [Pi_def]
    8.15 -    "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)";
    8.16 -by (Blast_tac 1);
    8.17 -qed "Pi_iff";
    8.18 -
    8.19 -(*For upward compatibility with the former definition*)
    8.20 -Goalw [Pi_def, function_def]
    8.21 -    "f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)";
    8.22 -by (Blast_tac 1);
    8.23 -qed "Pi_iff_old";
    8.24 -
    8.25 -Goal "f: Pi(A,B) ==> function(f)";
    8.26 -by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
    8.27 -qed "fun_is_function";
    8.28 -
    8.29 -(*Functions are relations*)
    8.30 -Goalw [Pi_def] "f: Pi(A,B) ==> f <= Sigma(A,B)";  
    8.31 -by (Blast_tac 1);
    8.32 -qed "fun_is_rel";
    8.33 -
    8.34 -val prems = Goalw [Pi_def]
    8.35 -    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
    8.36 -by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
    8.37 -qed "Pi_cong";
    8.38 -
    8.39 -(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
    8.40 -  flex-flex pairs and the "Check your prover" error.  Most
    8.41 -  Sigmas and Pis are abbreviated as * or -> *)
    8.42 -
    8.43 -(*Weakening one function type to another; see also Pi_type*)
    8.44 -Goalw [Pi_def] "[| f: A->B;  B<=D |] ==> f: A->D";
    8.45 -by (Best_tac 1);
    8.46 -qed "fun_weaken_type";
    8.47 -
    8.48 -(*** Function Application ***)
    8.49 -
    8.50 -Goalw [Pi_def, function_def] "[| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c";
    8.51 -by (Blast_tac 1);
    8.52 -qed "apply_equality2";
    8.53 -
    8.54 -Goalw [apply_def, function_def] "[| <a,b>: f;  function(f) |] ==> f`a = b";
    8.55 -by (Blast_tac 1);
    8.56 -qed "function_apply_equality";
    8.57 -
    8.58 -Goalw [Pi_def] "[| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b";
    8.59 -by (blast_tac (claset() addIs [function_apply_equality]) 1);
    8.60 -qed "apply_equality";
    8.61 -
    8.62 -(*Applying a function outside its domain yields 0*)
    8.63 -Goalw [apply_def] "a ~: domain(f) ==> f`a = 0";
    8.64 -by (rtac the_0 1);
    8.65 -by (Blast_tac 1);
    8.66 -qed "apply_0";
    8.67 -
    8.68 -Goal "[| f: Pi(A,B);  c: f |] ==> EX x:A.  c = <x,f`x>";
    8.69 -by (ftac fun_is_rel 1);
    8.70 -by (blast_tac (claset() addDs [apply_equality]) 1);
    8.71 -qed "Pi_memberD";
    8.72 -
    8.73 -Goal "[| function(f);  a : domain(f)|] ==> <a,f`a>: f";
    8.74 -by (asm_full_simp_tac (simpset() addsimps [function_def, apply_def]) 1); 
    8.75 -by (rtac theI2 1);
    8.76 -by Auto_tac;  
    8.77 -qed "function_apply_Pair";
    8.78 -
    8.79 -Goal "[| f: Pi(A,B);  a:A |] ==> <a,f`a>: f";
    8.80 -by (asm_full_simp_tac (simpset() addsimps [Pi_iff]) 1); 
    8.81 -by (blast_tac (claset() addIs [function_apply_Pair]) 1); 
    8.82 -qed "apply_Pair";
    8.83 -
    8.84 -(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
    8.85 -Goal "[| f: Pi(A,B);  a:A |] ==> f`a : B(a)"; 
    8.86 -by (rtac (fun_is_rel RS subsetD RS SigmaE2) 1);
    8.87 -by (REPEAT (ares_tac [apply_Pair] 1));
    8.88 -qed "apply_type";
    8.89 -AddTCs [apply_type];
    8.90 -
    8.91 -(*This version is acceptable to the simplifier*)
    8.92 -Goal "[| f: A->B;  a:A |] ==> f`a : B"; 
    8.93 -by (REPEAT (ares_tac [apply_type] 1));
    8.94 -qed "apply_funtype";
    8.95 -
    8.96 -Goal "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b";
    8.97 -by (ftac fun_is_rel 1);
    8.98 -by (blast_tac (claset() addSIs [apply_Pair, apply_equality]) 1);
    8.99 -qed "apply_iff";
   8.100 -
   8.101 -(*Refining one Pi type to another*)
   8.102 -val pi_prem::prems = Goal
   8.103 -    "[| f: Pi(A,C);  !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)";
   8.104 -by (cut_facts_tac [pi_prem] 1);
   8.105 -by (asm_full_simp_tac (FOL_ss addsimps [Pi_iff]) 1);
   8.106 -by (blast_tac (claset() addIs prems addSDs [pi_prem RS Pi_memberD]) 1);
   8.107 -qed "Pi_type";
   8.108 -
   8.109 -(*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*)
   8.110 -Goal "(f : Pi(A, %x. {y:B(x). P(x,y)})) \
   8.111 -\     <->  f : Pi(A,B) & (ALL x: A. P(x, f`x))";
   8.112 -by (blast_tac (claset() addIs [Pi_type] addDs [apply_type]) 1);
   8.113 -qed "Pi_Collect_iff";
   8.114 -
   8.115 -val [major,minor] = Goal 
   8.116 -        "[| f : Pi(A,B);  !!x. x:A ==> B(x)<=C(x) |] ==> f : Pi(A,C)";
   8.117 -by (fast_tac (claset() addSIs [major RS Pi_type, minor RS subsetD,
   8.118 -                major RS apply_type]) 1);
   8.119 -qed "Pi_weaken_type";
   8.120 -
   8.121 -
   8.122 -(** Elimination of membership in a function **)
   8.123 -
   8.124 -Goal "[| <a,b> : f;  f: Pi(A,B) |] ==> a : A";
   8.125 -by (REPEAT (ares_tac [fun_is_rel RS subsetD RS SigmaD1] 1));
   8.126 -qed "domain_type";
   8.127 -
   8.128 -Goal "[| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)";
   8.129 -by (etac (fun_is_rel RS subsetD RS SigmaD2) 1);
   8.130 -by (assume_tac 1);
   8.131 -qed "range_type";
   8.132 -
   8.133 -Goal "[| <a,b>: f;  f: Pi(A,B) |] ==> a:A & b:B(a) & f`a = b";
   8.134 -by (blast_tac (claset() addIs [domain_type, range_type, apply_equality]) 1);
   8.135 -qed "Pair_mem_PiD";
   8.136 -
   8.137 -(*** Lambda Abstraction ***)
   8.138 -
   8.139 -Goalw [lam_def] "a:A ==> <a,b(a)> : (lam x:A. b(x))";  
   8.140 -by (etac RepFunI 1);
   8.141 -qed "lamI";
   8.142 -
   8.143 -val major::prems = Goalw [lam_def]
   8.144 -    "[| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P  \
   8.145 -\    |] ==>  P";  
   8.146 -by (rtac (major RS RepFunE) 1);
   8.147 -by (REPEAT (ares_tac prems 1));
   8.148 -qed "lamE";
   8.149 -
   8.150 -Goal "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)";  
   8.151 -by (REPEAT (eresolve_tac [asm_rl,lamE,Pair_inject,ssubst] 1));
   8.152 -qed "lamD";
   8.153 -
   8.154 -val prems = Goalw [lam_def, Pi_def, function_def]
   8.155 -    "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)";  
   8.156 -by (blast_tac (claset() addIs prems) 1);
   8.157 -qed "lam_type";
   8.158 -AddTCs [lam_type];
   8.159 -
   8.160 -Goal "(lam x:A. b(x)) : A -> {b(x). x:A}";
   8.161 -by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
   8.162 -qed "lam_funtype";
   8.163 -
   8.164 -Goal "a : A ==> (lam x:A. b(x)) ` a = b(a)";
   8.165 -by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
   8.166 -qed "beta";
   8.167 -
   8.168 -Goalw [lam_def] "(lam x:0. b(x)) = 0";
   8.169 -by (Simp_tac 1);
   8.170 -qed "lam_empty";
   8.171 -
   8.172 -Goalw [lam_def] "domain(Lambda(A,b)) = A";
   8.173 -by (Blast_tac 1);
   8.174 -qed "domain_lam";
   8.175 -
   8.176 -Addsimps [beta, lam_empty, domain_lam];
   8.177 -
   8.178 -(*congruence rule for lambda abstraction*)
   8.179 -val prems = Goalw [lam_def] 
   8.180 -    "[| A=A';  !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')";
   8.181 -by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
   8.182 -qed "lam_cong";
   8.183 -
   8.184 -Addcongs [lam_cong];
   8.185 -
   8.186 -val [major] = Goal
   8.187 -    "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
   8.188 -by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
   8.189 -by (rtac ballI 1);
   8.190 -by (stac beta 1);
   8.191 -by (assume_tac 1);
   8.192 -by (etac (major RS theI) 1);
   8.193 -qed "lam_theI";
   8.194 -
   8.195 -Goal "[| (lam x:A. f(x)) = (lam x:A. g(x));  a:A |] ==> f(a)=g(a)";
   8.196 -by (fast_tac (claset() addSIs [lamI] addEs [equalityE, lamE]) 1);
   8.197 -qed "lam_eqE";
   8.198 -
   8.199 -
   8.200 -(*Empty function spaces*)
   8.201 -Goalw [Pi_def, function_def] "Pi(0,A) = {0}";
   8.202 -by (Blast_tac 1);
   8.203 -qed "Pi_empty1";
   8.204 -Addsimps [Pi_empty1];
   8.205 -
   8.206 -(*The singleton function*)
   8.207 -Goalw [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
   8.208 -by (Blast_tac 1);
   8.209 -qed "singleton_fun";
   8.210 -Addsimps [singleton_fun];
   8.211 -
   8.212 -Goalw [Pi_def, function_def] "(A->0) = (if A=0 then {0} else 0)";
   8.213 -by (Force_tac 1);
   8.214 -qed "Pi_empty2";
   8.215 -Addsimps [Pi_empty2];
   8.216 -
   8.217 -Goal "(A->X)=0 \\<longleftrightarrow> X=0 & (A \\<noteq> 0)";
   8.218 -by Auto_tac;  
   8.219 -by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 1);
   8.220 -qed "fun_space_empty_iff";
   8.221 -AddIffs [fun_space_empty_iff];
   8.222 -
   8.223 -
   8.224 -(** Extensionality **)
   8.225 -
   8.226 -(*Semi-extensionality!*)
   8.227 -val prems = Goal
   8.228 -    "[| f : Pi(A,B);  g: Pi(C,D);  A<=C; \
   8.229 -\       !!x. x:A ==> f`x = g`x       |] ==> f<=g";
   8.230 -by (rtac subsetI 1);
   8.231 -by (eresolve_tac (prems RL [Pi_memberD RS bexE]) 1);
   8.232 -by (etac ssubst 1);
   8.233 -by (resolve_tac (prems RL [ssubst]) 1);
   8.234 -by (REPEAT (ares_tac (prems@[apply_Pair,subsetD]) 1));
   8.235 -qed "fun_subset";
   8.236 -
   8.237 -val prems = Goal
   8.238 -    "[| f : Pi(A,B);  g: Pi(A,D);  \
   8.239 -\       !!x. x:A ==> f`x = g`x       |] ==> f=g";
   8.240 -by (REPEAT (ares_tac (prems @ (prems RL [sym]) @
   8.241 -                      [subset_refl,equalityI,fun_subset]) 1));
   8.242 -qed "fun_extension";
   8.243 -
   8.244 -Goal "f : Pi(A,B) ==> (lam x:A. f`x) = f";
   8.245 -by (rtac fun_extension 1);
   8.246 -by (REPEAT (ares_tac [lam_type,apply_type,beta] 1));
   8.247 -qed "eta";
   8.248 -
   8.249 -Addsimps [eta];
   8.250 -
   8.251 -Goal "[| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g";
   8.252 -by (blast_tac (claset() addIs [fun_extension]) 1);
   8.253 -qed "fun_extension_iff";
   8.254 -
   8.255 -(*thanks to Mark Staples*)
   8.256 -Goal "[| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)";
   8.257 -by (rtac iffI 1);
   8.258 -by (asm_full_simp_tac ZF_ss 2);
   8.259 -by (rtac fun_extension 1);
   8.260 -by (REPEAT (atac 1));
   8.261 -by (dtac (apply_Pair RSN (2,subsetD)) 1);
   8.262 -by (REPEAT (atac 1));
   8.263 -by (rtac (apply_equality RS sym) 1);
   8.264 -by (REPEAT (atac 1)) ;
   8.265 -qed "fun_subset_eq";
   8.266 -
   8.267 -
   8.268 -(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
   8.269 -val prems = Goal
   8.270 -    "[| f: Pi(A,B);        \
   8.271 -\       !!b. [| ALL x:A. b(x):B(x);  f = (lam x:A. b(x)) |] ==> P   \
   8.272 -\    |] ==> P";
   8.273 -by (resolve_tac prems 1);
   8.274 -by (rtac (eta RS sym) 2);
   8.275 -by (REPEAT (ares_tac (prems@[ballI,apply_type]) 1));
   8.276 -qed "Pi_lamE";
   8.277 -
   8.278 -
   8.279 -(** Images of functions **)
   8.280 -
   8.281 -Goalw [lam_def] "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}";
   8.282 -by (Blast_tac 1);
   8.283 -qed "image_lam";
   8.284 -
   8.285 -Goal "[| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}";
   8.286 -by (etac (eta RS subst) 1);
   8.287 -by (asm_full_simp_tac (simpset() addsimps [image_lam, subset_iff]) 1);
   8.288 -qed "image_fun";
   8.289 -
   8.290 -Goal "[| f: Pi(A,B);  x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)";
   8.291 -by (blast_tac (claset() addDs [apply_equality, apply_Pair]) 1);
   8.292 -qed "Pi_image_cons";
   8.293 -
   8.294 -
   8.295 -(*** properties of "restrict" ***)
   8.296 -
   8.297 -Goalw [restrict_def]
   8.298 -    "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) <= f";
   8.299 -by (blast_tac (claset() addIs [apply_Pair]) 1);
   8.300 -qed "restrict_subset";
   8.301 -
   8.302 -Goalw [restrict_def, function_def]
   8.303 -    "function(f) ==> function(restrict(f,A))";  
   8.304 -by (Blast_tac 1); 
   8.305 -qed "function_restrictI";
   8.306 -
   8.307 -Goal "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) : Pi(A,B)";  
   8.308 -by (asm_full_simp_tac
   8.309 -    (simpset() addsimps [Pi_iff, function_def, restrict_def]) 1); 
   8.310 -by (Blast_tac 1); 
   8.311 -qed "restrict_type2";
   8.312 -
   8.313 -(*Fails with the new definition of restrict
   8.314 -    "[| !!x. x:A ==> f`x: B(x) |] ==> restrict(f,A) : Pi(A,B)";  
   8.315 -qed "restrict_type";
   8.316 -*)
   8.317 -
   8.318 -(*FIXME: move to FOL?*)
   8.319 -Goal "EX x. a = x";
   8.320 -by Auto_tac;
   8.321 -qed "ex_equals_triv"; 
   8.322 -
   8.323 -Goal "a : A ==> restrict(f,A) ` a = f`a";
   8.324 -by (asm_full_simp_tac
   8.325 -    (simpset() addsimps [apply_def, restrict_def, ex_equals_triv]) 1); 
   8.326 -qed "restrict";
   8.327 -
   8.328 -Goalw [restrict_def] "restrict(f,0) = 0";
   8.329 -by (Simp_tac 1);
   8.330 -qed "restrict_empty";
   8.331 -Addsimps [restrict_empty];
   8.332 -
   8.333 -Goalw [restrict_def, lam_def] "domain(restrict(Lambda(A,f),C)) = A Int C";
   8.334 -by (rtac equalityI 1);  
   8.335 -by (auto_tac (claset(), simpset() addsimps [domain_iff])); 
   8.336 -qed "domain_restrict_lam";
   8.337 -Addsimps [domain_restrict_lam];
   8.338 -
   8.339 -Goalw [restrict_def] "restrict(restrict(r,A),B) = restrict(r, A Int B)";
   8.340 -by (Blast_tac 1); 
   8.341 -qed "restrict_restrict";
   8.342 -Addsimps [restrict_restrict];
   8.343 -
   8.344 -Goalw [restrict_def] "domain(restrict(f,C)) = domain(f) Int C"; 
   8.345 -by (auto_tac (claset(), simpset() addsimps [domain_def])); 
   8.346 -qed "domain_restrict";
   8.347 -Addsimps [domain_restrict];
   8.348 -
   8.349 -Goal "f <= Sigma(A,B) ==> restrict(f,A) = f"; 
   8.350 -by (asm_full_simp_tac (simpset() addsimps [restrict_def]) 1);  
   8.351 -by (Blast_tac 1); 
   8.352 -qed "restrict_idem";
   8.353 -Addsimps [restrict_idem];
   8.354 -
   8.355 -Goal "restrict(f,A) ` a = (if a : A then f`a else 0)";
   8.356 -by (asm_full_simp_tac (simpset() addsimps [restrict, apply_0]) 1); 
   8.357 -qed "restrict_if";
   8.358 -Addsimps [restrict_if];
   8.359 -
   8.360 -(*No longer true and no longer needed
   8.361 -val prems = Goalw [restrict_def]
   8.362 -    "[| A=B;  !!x. x:B ==> f`x=g`x |] ==> restrict(f,A) = restrict(g,B)";
   8.363 -qed "restrict_eqI";
   8.364 -*)
   8.365 -
   8.366 -Goalw [restrict_def, lam_def]
   8.367 -    "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
   8.368 -by Auto_tac; 
   8.369 -qed "restrict_lam_eq";
   8.370 -
   8.371 -Goal "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))";
   8.372 -by (rtac equalityI 1);
   8.373 -by (blast_tac (claset() addIs [apply_Pair, impOfSubs restrict_subset]) 2);
   8.374 -by (auto_tac (claset() addSDs [Pi_memberD],
   8.375 -	       simpset() addsimps [restrict_def, lam_def]));
   8.376 -qed "fun_cons_restrict_eq";
   8.377 -
   8.378 -
   8.379 -(*** Unions of functions ***)
   8.380 -
   8.381 -(** The Union of a set of COMPATIBLE functions is a function **)
   8.382 -
   8.383 -Goalw [function_def]
   8.384 -    "[| ALL x:S. function(x); \
   8.385 -\            ALL x:S. ALL y:S. x<=y | y<=x  |] ==>  \
   8.386 -\         function(Union(S))";
   8.387 -by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1);
   8.388 -	(*by (Blast_tac 1);  takes too long...*)
   8.389 -qed "function_Union";
   8.390 -
   8.391 -Goalw [Pi_def]
   8.392 -    "[| ALL f:S. EX C D. f:C->D; \
   8.393 -\            ALL f:S. ALL y:S. f<=y | y<=f  |] ==>  \
   8.394 -\         Union(S) : domain(Union(S)) -> range(Union(S))";
   8.395 -by (blast_tac (subset_cs addSIs [rel_Union, function_Union]) 1);
   8.396 -qed "fun_Union";
   8.397 -
   8.398 -
   8.399 -(** The Union of 2 disjoint functions is a function **)
   8.400 -
   8.401 -bind_thms ("Un_rls", [Un_subset_iff, SUM_Un_distrib1, prod_Un_distrib2, 
   8.402 -              Un_upper1 RSN (2, subset_trans), 
   8.403 -              Un_upper2 RSN (2, subset_trans)]);
   8.404 -
   8.405 -Goal "[| f: A->B;  g: C->D;  A Int C = 0  |]  \
   8.406 -\                 ==> (f Un g) : (A Un C) -> (B Un D)";
   8.407 -(*Prove the product and domain subgoals using distributive laws*)
   8.408 -by (asm_full_simp_tac (simpset() addsimps [Pi_iff,extension]@Un_rls) 1);
   8.409 -by (rewtac function_def);
   8.410 -by (Blast_tac 1);
   8.411 -qed "fun_disjoint_Un";
   8.412 -
   8.413 -Goal "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
   8.414 -\             (f Un g)`a = f`a";
   8.415 -by (rtac (apply_Pair RS UnI1 RS apply_equality) 1);
   8.416 -by (REPEAT (ares_tac [fun_disjoint_Un] 1));
   8.417 -qed "fun_disjoint_apply1";
   8.418 -
   8.419 -Goal "[| c:C;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
   8.420 -\             (f Un g)`c = g`c";
   8.421 -by (rtac (apply_Pair RS UnI2 RS apply_equality) 1);
   8.422 -by (REPEAT (ares_tac [fun_disjoint_Un] 1));
   8.423 -qed "fun_disjoint_apply2";
   8.424 -
   8.425 -(** Domain and range of a function/relation **)
   8.426 -
   8.427 -Goalw [Pi_def] "f : Pi(A,B) ==> domain(f)=A";
   8.428 -by (Blast_tac 1);
   8.429 -qed "domain_of_fun";
   8.430 -
   8.431 -Goal "[| f : Pi(A,B);  a: A |] ==> f`a : range(f)";
   8.432 -by (etac (apply_Pair RS rangeI) 1);
   8.433 -by (assume_tac 1);
   8.434 -qed "apply_rangeI";
   8.435 -
   8.436 -Goal "f : Pi(A,B) ==> f : A->range(f)";
   8.437 -by (REPEAT (ares_tac [Pi_type, apply_rangeI] 1));
   8.438 -qed "range_of_fun";
   8.439 -
   8.440 -(*** Extensions of functions ***)
   8.441 -
   8.442 -Goal "[| f: A->B;  c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
   8.443 -by (forward_tac [singleton_fun RS fun_disjoint_Un] 1);
   8.444 -by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2);
   8.445 -by (Blast_tac 1);
   8.446 -qed "fun_extend";
   8.447 -
   8.448 -Goal "[| f: A->B;  c~:A;  b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
   8.449 -by (blast_tac (claset() addIs [fun_extend RS fun_weaken_type]) 1);
   8.450 -qed "fun_extend3";
   8.451 -
   8.452 -Goal "[| f: A->B;  a:A;  c~:A |] ==> cons(<c,b>,f)`a = f`a";
   8.453 -by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
   8.454 -by (rtac fun_extend 3);
   8.455 -by (REPEAT (assume_tac 1));
   8.456 -qed "fun_extend_apply1";
   8.457 -
   8.458 -Goal "[| f: A->B;  c~:A |] ==> cons(<c,b>,f)`c = b";
   8.459 -by (rtac (consI1 RS apply_equality) 1);
   8.460 -by (rtac fun_extend 1);
   8.461 -by (REPEAT (assume_tac 1));
   8.462 -qed "fun_extend_apply2";
   8.463 -
   8.464 -bind_thm ("singleton_apply", [singletonI, singleton_fun] MRS apply_equality);
   8.465 -Addsimps [singleton_apply];
   8.466 -
   8.467 -(*For Finite.ML.  Inclusion of right into left is easy*)
   8.468 -Goal "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
   8.469 -by (rtac equalityI 1);
   8.470 -by (safe_tac (claset() addSEs [fun_extend3]));
   8.471 -(*Inclusion of left into right*)
   8.472 -by (subgoal_tac "restrict(x, A) : A -> B" 1);
   8.473 -by (blast_tac (claset() addIs [restrict_type2]) 2);
   8.474 -by (rtac UN_I 1 THEN assume_tac 1);
   8.475 -by (rtac (apply_funtype RS UN_I) 1 THEN REPEAT (ares_tac [consI1] 1));
   8.476 -by (Simp_tac 1);
   8.477 -by (rtac fun_extension 1 THEN REPEAT (ares_tac [fun_extend] 1));
   8.478 -by (etac consE 1);
   8.479 -by (ALLGOALS 
   8.480 -    (asm_simp_tac (simpset() addsimps [restrict, fun_extend_apply1, 
   8.481 -                                      fun_extend_apply2])));
   8.482 -qed "cons_fun_eq";
     9.1 --- a/src/ZF/func.thy	Fri May 17 16:54:25 2002 +0200
     9.2 +++ b/src/ZF/func.thy	Sat May 18 20:08:17 2002 +0200
     9.3 @@ -1,3 +1,470 @@
     9.4 -(*Dummy theory to document dependencies *)
     9.5 +(*  Title:      ZF/func.thy
     9.6 +    ID:         $Id$
     9.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.8 +    Copyright   1991  University of Cambridge
     9.9 +
    9.10 +Functions in Zermelo-Fraenkel Set Theory
    9.11 +*)
    9.12 +
    9.13 +theory func = domrange + equalities:
    9.14 +
    9.15 +(*** The Pi operator -- dependent function space ***)
    9.16 +
    9.17 +lemma Pi_iff:
    9.18 +    "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)"
    9.19 +by (unfold Pi_def, blast)
    9.20 +
    9.21 +(*For upward compatibility with the former definition*)
    9.22 +lemma Pi_iff_old:
    9.23 +    "f: Pi(A,B) <-> f<=Sigma(A,B) & (ALL x:A. EX! y. <x,y>: f)"
    9.24 +by (unfold Pi_def function_def, blast)
    9.25 +
    9.26 +lemma fun_is_function: "f: Pi(A,B) ==> function(f)"
    9.27 +by (simp only: Pi_iff)
    9.28 +
    9.29 +(*Functions are relations*)
    9.30 +lemma fun_is_rel: "f: Pi(A,B) ==> f <= Sigma(A,B)"
    9.31 +by (unfold Pi_def, blast)
    9.32 +
    9.33 +lemma Pi_cong:
    9.34 +    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')"
    9.35 +by (simp add: Pi_def cong add: Sigma_cong)
    9.36 +
    9.37 +(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
    9.38 +  flex-flex pairs and the "Check your prover" error.  Most
    9.39 +  Sigmas and Pis are abbreviated as * or -> *)
    9.40 +
    9.41 +(*Weakening one function type to another; see also Pi_type*)
    9.42 +lemma fun_weaken_type: "[| f: A->B;  B<=D |] ==> f: A->D"
    9.43 +by (unfold Pi_def, best)
    9.44 +
    9.45 +(*** Function Application ***)
    9.46 +
    9.47 +lemma apply_equality2: "[| <a,b>: f;  <a,c>: f;  f: Pi(A,B) |] ==> b=c"
    9.48 +by (unfold Pi_def function_def, blast)
    9.49 +
    9.50 +lemma function_apply_equality: "[| <a,b>: f;  function(f) |] ==> f`a = b"
    9.51 +by (unfold apply_def function_def, blast)
    9.52 +
    9.53 +lemma apply_equality: "[| <a,b>: f;  f: Pi(A,B) |] ==> f`a = b"
    9.54 +apply (unfold Pi_def)
    9.55 +apply (blast intro: function_apply_equality)
    9.56 +done
    9.57 +
    9.58 +(*Applying a function outside its domain yields 0*)
    9.59 +lemma apply_0: "a ~: domain(f) ==> f`a = 0"
    9.60 +apply (unfold apply_def)
    9.61 +apply (rule the_0, blast)
    9.62 +done
    9.63 +
    9.64 +lemma Pi_memberD: "[| f: Pi(A,B);  c: f |] ==> EX x:A.  c = <x,f`x>"
    9.65 +apply (frule fun_is_rel)
    9.66 +apply (blast dest: apply_equality)
    9.67 +done
    9.68 +
    9.69 +lemma function_apply_Pair: "[| function(f);  a : domain(f)|] ==> <a,f`a>: f"
    9.70 +apply (simp add: function_def apply_def)
    9.71 +apply (rule theI2, auto)
    9.72 +done
    9.73 +
    9.74 +lemma apply_Pair: "[| f: Pi(A,B);  a:A |] ==> <a,f`a>: f"
    9.75 +apply (simp add: Pi_iff)
    9.76 +apply (blast intro: function_apply_Pair)
    9.77 +done
    9.78 +
    9.79 +(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
    9.80 +lemma apply_type [TC]: "[| f: Pi(A,B);  a:A |] ==> f`a : B(a)"
    9.81 +by (blast intro: apply_Pair dest: fun_is_rel)
    9.82 +
    9.83 +(*This version is acceptable to the simplifier*)
    9.84 +lemma apply_funtype: "[| f: A->B;  a:A |] ==> f`a : B"
    9.85 +by (blast dest: apply_type)
    9.86 +
    9.87 +lemma apply_iff: "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"
    9.88 +apply (frule fun_is_rel)
    9.89 +apply (blast intro!: apply_Pair apply_equality)
    9.90 +done
    9.91 +
    9.92 +(*Refining one Pi type to another*)
    9.93 +lemma Pi_type: "[| f: Pi(A,C);  !!x. x:A ==> f`x : B(x) |] ==> f : Pi(A,B)"
    9.94 +apply (simp only: Pi_iff)
    9.95 +apply (blast dest: function_apply_equality)
    9.96 +done
    9.97 +
    9.98 +(*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*)
    9.99 +lemma Pi_Collect_iff:
   9.100 +     "(f : Pi(A, %x. {y:B(x). P(x,y)}))
   9.101 +      <->  f : Pi(A,B) & (ALL x: A. P(x, f`x))"
   9.102 +by (blast intro: Pi_type dest: apply_type)
   9.103 +
   9.104 +lemma Pi_weaken_type:
   9.105 +        "[| f : Pi(A,B);  !!x. x:A ==> B(x)<=C(x) |] ==> f : Pi(A,C)"
   9.106 +by (blast intro: Pi_type dest: apply_type)
   9.107 +
   9.108 +
   9.109 +(** Elimination of membership in a function **)
   9.110 +
   9.111 +lemma domain_type: "[| <a,b> : f;  f: Pi(A,B) |] ==> a : A"
   9.112 +by (blast dest: fun_is_rel)
   9.113 +
   9.114 +lemma range_type: "[| <a,b> : f;  f: Pi(A,B) |] ==> b : B(a)"
   9.115 +by (blast dest: fun_is_rel)
   9.116 +
   9.117 +lemma Pair_mem_PiD: "[| <a,b>: f;  f: Pi(A,B) |] ==> a:A & b:B(a) & f`a = b"
   9.118 +by (blast intro: domain_type range_type apply_equality)
   9.119 +
   9.120 +(*** Lambda Abstraction ***)
   9.121 +
   9.122 +lemma lamI: "a:A ==> <a,b(a)> : (lam x:A. b(x))"
   9.123 +apply (unfold lam_def)
   9.124 +apply (erule RepFunI)
   9.125 +done
   9.126 +
   9.127 +lemma lamE:
   9.128 +    "[| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P
   9.129 +     |] ==>  P"
   9.130 +by (simp add: lam_def, blast)
   9.131 +
   9.132 +lemma lamD: "[| <a,c>: (lam x:A. b(x)) |] ==> c = b(a)"
   9.133 +by (simp add: lam_def)
   9.134 +
   9.135 +lemma lam_type [TC]:
   9.136 +    "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)"
   9.137 +by (simp add: lam_def Pi_def function_def, blast)
   9.138 +
   9.139 +lemma lam_funtype: "(lam x:A. b(x)) : A -> {b(x). x:A}"
   9.140 +by (blast intro: lam_type);
   9.141 +
   9.142 +lemma beta [simp]: "a : A ==> (lam x:A. b(x)) ` a = b(a)"
   9.143 +by (blast intro: apply_equality lam_funtype lamI)
   9.144 +
   9.145 +lemma lam_empty [simp]: "(lam x:0. b(x)) = 0"
   9.146 +by (simp add: lam_def)
   9.147 +
   9.148 +lemma domain_lam [simp]: "domain(Lambda(A,b)) = A"
   9.149 +by (simp add: lam_def, blast)
   9.150 +
   9.151 +(*congruence rule for lambda abstraction*)
   9.152 +lemma lam_cong [cong]:
   9.153 +    "[| A=A';  !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')"
   9.154 +by (simp only: lam_def cong add: RepFun_cong)
   9.155 +
   9.156 +lemma lam_theI:
   9.157 +    "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)"
   9.158 +apply (rule_tac x = "lam x: A. THE y. Q (x,y) " in exI)
   9.159 +apply (rule ballI)
   9.160 +apply (subst beta, assumption)
   9.161 +apply (blast intro: theI)
   9.162 +done
   9.163 +
   9.164 +lemma lam_eqE: "[| (lam x:A. f(x)) = (lam x:A. g(x));  a:A |] ==> f(a)=g(a)"
   9.165 +by (fast intro!: lamI elim: equalityE lamE)
   9.166 +
   9.167 +
   9.168 +(*Empty function spaces*)
   9.169 +lemma Pi_empty1 [simp]: "Pi(0,A) = {0}"
   9.170 +by (unfold Pi_def function_def, blast)
   9.171 +
   9.172 +(*The singleton function*)
   9.173 +lemma singleton_fun [simp]: "{<a,b>} : {a} -> {b}"
   9.174 +by (unfold Pi_def function_def, blast)
   9.175 +
   9.176 +lemma Pi_empty2 [simp]: "(A->0) = (if A=0 then {0} else 0)"
   9.177 +by (unfold Pi_def function_def, force)
   9.178 +
   9.179 +lemma  fun_space_empty_iff [iff]: "(A->X)=0 \<longleftrightarrow> X=0 & (A \<noteq> 0)"
   9.180 +apply auto
   9.181 +apply (fast intro!: equals0I intro: lam_type)
   9.182 +done
   9.183 +
   9.184 +
   9.185 +(** Extensionality **)
   9.186 +
   9.187 +(*Semi-extensionality!*)
   9.188 +
   9.189 +lemma fun_subset:
   9.190 +    "[| f : Pi(A,B);  g: Pi(C,D);  A<=C;
   9.191 +        !!x. x:A ==> f`x = g`x       |] ==> f<=g"
   9.192 +by (force dest: Pi_memberD intro: apply_Pair)
   9.193 +
   9.194 +lemma fun_extension:
   9.195 +    "[| f : Pi(A,B);  g: Pi(A,D);
   9.196 +        !!x. x:A ==> f`x = g`x       |] ==> f=g"
   9.197 +by (blast del: subsetI intro: subset_refl sym fun_subset)
   9.198 +
   9.199 +lemma eta [simp]: "f : Pi(A,B) ==> (lam x:A. f`x) = f"
   9.200 +apply (rule fun_extension)
   9.201 +apply (auto simp add: lam_type apply_type beta)
   9.202 +done
   9.203 +
   9.204 +lemma fun_extension_iff:
   9.205 +     "[| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g"
   9.206 +by (blast intro: fun_extension)
   9.207 +
   9.208 +(*thm by Mark Staples, proof by lcp*)
   9.209 +lemma fun_subset_eq: "[| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
   9.210 +by (blast dest: apply_Pair
   9.211 +	  intro: fun_extension apply_equality [symmetric])
   9.212 +
   9.213 +
   9.214 +(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
   9.215 +lemma Pi_lamE:
   9.216 +  assumes major: "f: Pi(A,B)"
   9.217 +      and minor: "!!b. [| ALL x:A. b(x):B(x);  f = (lam x:A. b(x)) |] ==> P"
   9.218 +  shows "P"
   9.219 +apply (rule minor)
   9.220 +apply (rule_tac [2] eta [symmetric])
   9.221 +apply (blast intro: major apply_type)+
   9.222 +done
   9.223 +
   9.224 +
   9.225 +(** Images of functions **)
   9.226 +
   9.227 +lemma image_lam: "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}"
   9.228 +by (unfold lam_def, blast)
   9.229 +
   9.230 +lemma image_fun: "[| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}"
   9.231 +apply (erule eta [THEN subst])
   9.232 +apply (simp add: image_lam subset_iff)
   9.233 +done
   9.234 +
   9.235 +lemma Pi_image_cons:
   9.236 +     "[| f: Pi(A,B);  x: A |] ==> f `` cons(x,y) = cons(f`x, f``y)"
   9.237 +by (blast dest: apply_equality apply_Pair)
   9.238 +
   9.239  
   9.240 -func = domrange + equalities
   9.241 +(*** properties of "restrict" ***)
   9.242 +
   9.243 +lemma restrict_subset:
   9.244 +    "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) <= f"
   9.245 +apply (unfold restrict_def)
   9.246 +apply (blast intro: apply_Pair)
   9.247 +done
   9.248 +
   9.249 +lemma function_restrictI:
   9.250 +    "function(f) ==> function(restrict(f,A))"
   9.251 +by (unfold restrict_def function_def, blast)
   9.252 +
   9.253 +lemma restrict_type2: "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A) : Pi(A,B)"
   9.254 +by (simp add: Pi_iff function_def restrict_def, blast)
   9.255 +
   9.256 +lemma restrict: "a : A ==> restrict(f,A) ` a = f`a"
   9.257 +by (simp add: apply_def restrict_def)
   9.258 +
   9.259 +lemma restrict_empty [simp]: "restrict(f,0) = 0"
   9.260 +apply (unfold restrict_def)
   9.261 +apply (simp (no_asm))
   9.262 +done
   9.263 +
   9.264 +lemma domain_restrict_lam [simp]: "domain(restrict(Lambda(A,f),C)) = A Int C"
   9.265 +apply (unfold restrict_def lam_def)
   9.266 +apply (rule equalityI)
   9.267 +apply (auto simp add: domain_iff)
   9.268 +done
   9.269 +
   9.270 +lemma restrict_restrict [simp]:
   9.271 +     "restrict(restrict(r,A),B) = restrict(r, A Int B)"
   9.272 +by (unfold restrict_def, blast)
   9.273 +
   9.274 +lemma domain_restrict [simp]: "domain(restrict(f,C)) = domain(f) Int C"
   9.275 +apply (unfold restrict_def)
   9.276 +apply (auto simp add: domain_def)
   9.277 +done
   9.278 +
   9.279 +lemma restrict_idem [simp]: "f <= Sigma(A,B) ==> restrict(f,A) = f"
   9.280 +by (simp add: restrict_def, blast)
   9.281 +
   9.282 +lemma restrict_if [simp]: "restrict(f,A) ` a = (if a : A then f`a else 0)"
   9.283 +by (simp add: restrict apply_0)
   9.284 +
   9.285 +lemma restrict_lam_eq:
   9.286 +    "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))"
   9.287 +by (unfold restrict_def lam_def, auto)
   9.288 +
   9.289 +lemma fun_cons_restrict_eq:
   9.290 +     "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))"
   9.291 +apply (rule equalityI)
   9.292 +prefer 2 apply (blast intro: apply_Pair restrict_subset [THEN subsetD])
   9.293 +apply (auto dest!: Pi_memberD simp add: restrict_def lam_def)
   9.294 +done
   9.295 +
   9.296 +
   9.297 +(*** Unions of functions ***)
   9.298 +
   9.299 +(** The Union of a set of COMPATIBLE functions is a function **)
   9.300 +
   9.301 +lemma function_Union:
   9.302 +    "[| ALL x:S. function(x);
   9.303 +        ALL x:S. ALL y:S. x<=y | y<=x  |]
   9.304 +     ==> function(Union(S))"
   9.305 +by (unfold function_def, blast) 
   9.306 +
   9.307 +lemma fun_Union:
   9.308 +    "[| ALL f:S. EX C D. f:C->D;
   9.309 +             ALL f:S. ALL y:S. f<=y | y<=f  |] ==>
   9.310 +          Union(S) : domain(Union(S)) -> range(Union(S))"
   9.311 +apply (unfold Pi_def)
   9.312 +apply (blast intro!: rel_Union function_Union)
   9.313 +done
   9.314 +
   9.315 +
   9.316 +(** The Union of 2 disjoint functions is a function **)
   9.317 +
   9.318 +lemmas Un_rls = Un_subset_iff SUM_Un_distrib1 prod_Un_distrib2
   9.319 +                subset_trans [OF _ Un_upper1]
   9.320 +                subset_trans [OF _ Un_upper2]
   9.321 +
   9.322 +lemma fun_disjoint_Un:
   9.323 +     "[| f: A->B;  g: C->D;  A Int C = 0  |]
   9.324 +      ==> (f Un g) : (A Un C) -> (B Un D)"
   9.325 +(*Prove the product and domain subgoals using distributive laws*)
   9.326 +apply (simp add: Pi_iff extension Un_rls)
   9.327 +apply (unfold function_def, blast)
   9.328 +done
   9.329 +
   9.330 +lemma fun_disjoint_apply1:
   9.331 +     "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |]
   9.332 +      ==> (f Un g)`a = f`a"
   9.333 +apply (rule apply_Pair [THEN UnI1, THEN apply_equality], assumption+)
   9.334 +apply (blast intro: fun_disjoint_Un ) 
   9.335 +done
   9.336 +
   9.337 +lemma fun_disjoint_apply2:
   9.338 +     "[| c:C;  f: A->B;  g: C->D;  A Int C = 0 |]
   9.339 +      ==> (f Un g)`c = g`c"
   9.340 +apply (rule apply_Pair [THEN UnI2, THEN apply_equality], assumption+)
   9.341 +apply (blast intro: fun_disjoint_Un ) 
   9.342 +done
   9.343 +
   9.344 +(** Domain and range of a function/relation **)
   9.345 +
   9.346 +lemma domain_of_fun: "f : Pi(A,B) ==> domain(f)=A"
   9.347 +by (unfold Pi_def, blast)
   9.348 +
   9.349 +lemma apply_rangeI: "[| f : Pi(A,B);  a: A |] ==> f`a : range(f)"
   9.350 +by (erule apply_Pair [THEN rangeI], assumption)
   9.351 +
   9.352 +lemma range_of_fun: "f : Pi(A,B) ==> f : A->range(f)"
   9.353 +by (blast intro: Pi_type apply_rangeI)
   9.354 +
   9.355 +(*** Extensions of functions ***)
   9.356 +
   9.357 +lemma fun_extend:
   9.358 +     "[| f: A->B;  c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)"
   9.359 +apply (frule singleton_fun [THEN fun_disjoint_Un], blast)
   9.360 +apply (simp add: cons_eq) 
   9.361 +done
   9.362 +
   9.363 +lemma fun_extend3:
   9.364 +     "[| f: A->B;  c~:A;  b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B"
   9.365 +by (blast intro: fun_extend [THEN fun_weaken_type])
   9.366 +
   9.367 +lemma fun_extend_apply1: "[| f: A->B;  a:A;  c~:A |] ==> cons(<c,b>,f)`a = f`a"
   9.368 +apply (rule apply_Pair [THEN consI2, THEN apply_equality])
   9.369 +apply (rule_tac [3] fun_extend, assumption+)
   9.370 +done
   9.371 +
   9.372 +lemma fun_extend_apply2: "[| f: A->B;  c~:A |] ==> cons(<c,b>,f)`c = b"
   9.373 +apply (rule consI1 [THEN apply_equality])
   9.374 +apply (rule fun_extend, assumption+)
   9.375 +done
   9.376 +
   9.377 +lemmas singleton_apply = apply_equality [OF singletonI singleton_fun, simp]
   9.378 +
   9.379 +(*For Finite.ML.  Inclusion of right into left is easy*)
   9.380 +lemma cons_fun_eq:
   9.381 +     "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"
   9.382 +apply (rule equalityI)
   9.383 +apply (safe elim!: fun_extend3)
   9.384 +(*Inclusion of left into right*)
   9.385 +apply (subgoal_tac "restrict (x, A) : A -> B")
   9.386 + prefer 2 apply (blast intro: restrict_type2)
   9.387 +apply (rule UN_I, assumption)
   9.388 +apply (rule apply_funtype [THEN UN_I]) 
   9.389 +  apply assumption
   9.390 + apply (rule consI1) 
   9.391 +apply (simp (no_asm))
   9.392 +apply (rule fun_extension) 
   9.393 +  apply assumption
   9.394 + apply (blast intro: fun_extend) 
   9.395 +apply (erule consE)
   9.396 +apply (simp_all add: restrict fun_extend_apply1 fun_extend_apply2)
   9.397 +done
   9.398 +
   9.399 +ML
   9.400 +{*
   9.401 +val Pi_iff = thm "Pi_iff";
   9.402 +val Pi_iff_old = thm "Pi_iff_old";
   9.403 +val fun_is_function = thm "fun_is_function";
   9.404 +val fun_is_rel = thm "fun_is_rel";
   9.405 +val Pi_cong = thm "Pi_cong";
   9.406 +val fun_weaken_type = thm "fun_weaken_type";
   9.407 +val apply_equality2 = thm "apply_equality2";
   9.408 +val function_apply_equality = thm "function_apply_equality";
   9.409 +val apply_equality = thm "apply_equality";
   9.410 +val apply_0 = thm "apply_0";
   9.411 +val Pi_memberD = thm "Pi_memberD";
   9.412 +val function_apply_Pair = thm "function_apply_Pair";
   9.413 +val apply_Pair = thm "apply_Pair";
   9.414 +val apply_type = thm "apply_type";
   9.415 +val apply_funtype = thm "apply_funtype";
   9.416 +val apply_iff = thm "apply_iff";
   9.417 +val Pi_type = thm "Pi_type";
   9.418 +val Pi_Collect_iff = thm "Pi_Collect_iff";
   9.419 +val Pi_weaken_type = thm "Pi_weaken_type";
   9.420 +val domain_type = thm "domain_type";
   9.421 +val range_type = thm "range_type";
   9.422 +val Pair_mem_PiD = thm "Pair_mem_PiD";
   9.423 +val lamI = thm "lamI";
   9.424 +val lamE = thm "lamE";
   9.425 +val lamD = thm "lamD";
   9.426 +val lam_type = thm "lam_type";
   9.427 +val lam_funtype = thm "lam_funtype";
   9.428 +val beta = thm "beta";
   9.429 +val lam_empty = thm "lam_empty";
   9.430 +val domain_lam = thm "domain_lam";
   9.431 +val lam_cong = thm "lam_cong";
   9.432 +val lam_theI = thm "lam_theI";
   9.433 +val lam_eqE = thm "lam_eqE";
   9.434 +val Pi_empty1 = thm "Pi_empty1";
   9.435 +val singleton_fun = thm "singleton_fun";
   9.436 +val Pi_empty2 = thm "Pi_empty2";
   9.437 +val fun_space_empty_iff = thm "fun_space_empty_iff";
   9.438 +val fun_subset = thm "fun_subset";
   9.439 +val fun_extension = thm "fun_extension";
   9.440 +val eta = thm "eta";
   9.441 +val fun_extension_iff = thm "fun_extension_iff";
   9.442 +val fun_subset_eq = thm "fun_subset_eq";
   9.443 +val Pi_lamE = thm "Pi_lamE";
   9.444 +val image_lam = thm "image_lam";
   9.445 +val image_fun = thm "image_fun";
   9.446 +val Pi_image_cons = thm "Pi_image_cons";
   9.447 +val restrict_subset = thm "restrict_subset";
   9.448 +val function_restrictI = thm "function_restrictI";
   9.449 +val restrict_type2 = thm "restrict_type2";
   9.450 +val restrict = thm "restrict";
   9.451 +val restrict_empty = thm "restrict_empty";
   9.452 +val domain_restrict_lam = thm "domain_restrict_lam";
   9.453 +val restrict_restrict = thm "restrict_restrict";
   9.454 +val domain_restrict = thm "domain_restrict";
   9.455 +val restrict_idem = thm "restrict_idem";
   9.456 +val restrict_if = thm "restrict_if";
   9.457 +val restrict_lam_eq = thm "restrict_lam_eq";
   9.458 +val fun_cons_restrict_eq = thm "fun_cons_restrict_eq";
   9.459 +val function_Union = thm "function_Union";
   9.460 +val fun_Union = thm "fun_Union";
   9.461 +val fun_disjoint_Un = thm "fun_disjoint_Un";
   9.462 +val fun_disjoint_apply1 = thm "fun_disjoint_apply1";
   9.463 +val fun_disjoint_apply2 = thm "fun_disjoint_apply2";
   9.464 +val domain_of_fun = thm "domain_of_fun";
   9.465 +val apply_rangeI = thm "apply_rangeI";
   9.466 +val range_of_fun = thm "range_of_fun";
   9.467 +val fun_extend = thm "fun_extend";
   9.468 +val fun_extend3 = thm "fun_extend3";
   9.469 +val fun_extend_apply1 = thm "fun_extend_apply1";
   9.470 +val fun_extend_apply2 = thm "fun_extend_apply2";
   9.471 +val singleton_apply = thm "singleton_apply";
   9.472 +val cons_fun_eq = thm "cons_fun_eq";
   9.473 +*}
   9.474 +
   9.475 +end