conversion of many files to Isar format
authorpaulson
Sat Jun 29 21:33:06 2002 +0200 (2002-06-29)
changeset 1325901fa0c8dbc92
parent 13258 8f394f266025
child 13260 ea36a40c004f
conversion of many files to Isar format
src/ZF/ArithSimp.ML
src/ZF/ArithSimp.thy
src/ZF/Inductive.thy
src/ZF/IsaMakefile
src/ZF/QPair.ML
src/ZF/QPair.thy
src/ZF/arith_data.ML
src/ZF/equalities.thy
src/ZF/ex/Primes.thy
src/ZF/mono.ML
src/ZF/mono.thy
src/ZF/subset.ML
src/ZF/subset.thy
src/ZF/upair.ML
src/ZF/upair.thy
     1.1 --- a/src/ZF/ArithSimp.ML	Fri Jun 28 20:01:09 2002 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,588 +0,0 @@
     1.4 -(*  Title:      ZF/ArithSimp.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   2000  University of Cambridge
     1.8 -
     1.9 -Arithmetic with simplification
    1.10 -*)
    1.11 -
    1.12 -
    1.13 -Addsimprocs ArithData.nat_cancel;
    1.14 -
    1.15 -
    1.16 -(*** Difference ***)
    1.17 -
    1.18 -Goal "m #- m = 0";
    1.19 -by (subgoal_tac "natify(m) #- natify(m) = 0" 1);
    1.20 -by (rtac (natify_in_nat RS nat_induct) 2);
    1.21 -by Auto_tac;
    1.22 -qed "diff_self_eq_0";
    1.23 -
    1.24 -(**Addition is the inverse of subtraction**)
    1.25 -
    1.26 -(*We need m:nat even if we replace the RHS by natify(m), for consider e.g.
    1.27 -  n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 ~= 0 = natify(m).*)
    1.28 -Goal "[| n le m;  m:nat |] ==> n #+ (m#-n) = m";
    1.29 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
    1.30 -by (etac rev_mp 1);
    1.31 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.32 -by Auto_tac;
    1.33 -qed "add_diff_inverse";
    1.34 -
    1.35 -Goal "[| n le m;  m:nat |] ==> (m#-n) #+ n = m";
    1.36 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
    1.37 -by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1);
    1.38 -qed "add_diff_inverse2";
    1.39 -
    1.40 -(*Proof is IDENTICAL to that of add_diff_inverse*)
    1.41 -Goal "[| n le m;  m:nat |] ==> succ(m) #- n = succ(m#-n)";
    1.42 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
    1.43 -by (etac rev_mp 1);
    1.44 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.45 -by (ALLGOALS Asm_simp_tac);
    1.46 -qed "diff_succ";
    1.47 -
    1.48 -Goal "[| m: nat; n: nat |] ==> 0 < (n #- m)   <->   m<n";
    1.49 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.50 -by (ALLGOALS Asm_simp_tac);
    1.51 -qed "zero_less_diff";
    1.52 -Addsimps [zero_less_diff];
    1.53 -
    1.54 -
    1.55 -(** Difference distributes over multiplication **)
    1.56 -
    1.57 -Goal "(m #- n) #* k = (m #* k) #- (n #* k)";
    1.58 -by (subgoal_tac "(natify(m) #- natify(n)) #* natify(k) = \
    1.59 -\                (natify(m) #* natify(k)) #- (natify(n) #* natify(k))" 1);
    1.60 -by (res_inst_tac [("m","natify(m)"),("n","natify(n)")] diff_induct 2);
    1.61 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [diff_cancel])));
    1.62 -qed "diff_mult_distrib" ;
    1.63 -
    1.64 -Goal "k #* (m #- n) = (k #* m) #- (k #* n)";
    1.65 -by (simp_tac
    1.66 -    (simpset() addsimps [inst "m" "k" mult_commute, diff_mult_distrib]) 1);
    1.67 -qed "diff_mult_distrib2";
    1.68 -
    1.69 -
    1.70 -(*** Remainder ***)
    1.71 -
    1.72 -(*We need m:nat even with natify*)
    1.73 -Goal "[| 0<n;  n le m;  m:nat |] ==> m #- n < m";
    1.74 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
    1.75 -by (etac rev_mp 1);
    1.76 -by (etac rev_mp 1);
    1.77 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.78 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self])));
    1.79 -qed "div_termination";
    1.80 -
    1.81 -bind_thms ("div_rls",   (*for mod and div*)
    1.82 -    nat_typechecks @
    1.83 -    [Ord_transrec_type, apply_funtype, div_termination RS ltD,
    1.84 -     nat_into_Ord, not_lt_iff_le RS iffD1]);
    1.85 -
    1.86 -val div_ss = simpset() addsimps [div_termination RS ltD,
    1.87 -				 not_lt_iff_le RS iffD2];
    1.88 -
    1.89 -Goalw [raw_mod_def] "[| m:nat;  n:nat |] ==> raw_mod (m, n) : nat";
    1.90 -by (rtac Ord_transrec_type 1);
    1.91 -by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]));
    1.92 -by (REPEAT (ares_tac div_rls 1));
    1.93 -qed "raw_mod_type";
    1.94 -
    1.95 -Goalw [mod_def] "m mod n : nat";
    1.96 -by (simp_tac (simpset() addsimps [mod_def, raw_mod_type]) 1);
    1.97 -qed "mod_type";
    1.98 -AddTCs [mod_type];
    1.99 -AddIffs [mod_type];
   1.100 -
   1.101 -
   1.102 -(** Aribtrary definitions for division by zero.  Useful to simplify 
   1.103 -    certain equations **)
   1.104 -
   1.105 -Goalw [div_def] "a div 0 = 0";
   1.106 -by (rtac (raw_div_def RS def_transrec RS trans) 1);
   1.107 -by (Asm_simp_tac 1);
   1.108 -qed "DIVISION_BY_ZERO_DIV";  (*NOT for adding to default simpset*)
   1.109 -
   1.110 -Goalw [mod_def] "a mod 0 = natify(a)";
   1.111 -by (rtac (raw_mod_def RS def_transrec RS trans) 1);
   1.112 -by (Asm_simp_tac 1);
   1.113 -qed "DIVISION_BY_ZERO_MOD";  (*NOT for adding to default simpset*)
   1.114 -
   1.115 -fun div_undefined_case_tac s i =
   1.116 -  case_tac s i THEN 
   1.117 -  asm_full_simp_tac
   1.118 -         (simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]) (i+1) THEN
   1.119 -  asm_full_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV, 
   1.120 -		 	 	         DIVISION_BY_ZERO_MOD]) i;
   1.121 -
   1.122 -Goal "m<n ==> raw_mod (m,n) = m";
   1.123 -by (rtac (raw_mod_def RS def_transrec RS trans) 1);
   1.124 -by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1);
   1.125 -qed "raw_mod_less";
   1.126 -
   1.127 -Goal "[| m<n; n : nat |] ==> m mod n = m";
   1.128 -by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
   1.129 -by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_less]) 1);
   1.130 -qed "mod_less";
   1.131 -
   1.132 -Goal "[| 0<n; n le m;  m:nat |] ==> raw_mod (m, n) = raw_mod (m#-n, n)";
   1.133 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   1.134 -by (rtac (raw_mod_def RS def_transrec RS trans) 1);
   1.135 -by (asm_simp_tac div_ss 1);
   1.136 -by (Blast_tac 1);
   1.137 -qed "raw_mod_geq";
   1.138 -
   1.139 -Goal "[| n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
   1.140 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   1.141 -by (div_undefined_case_tac "n=0" 1);
   1.142 -by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_geq]) 1);
   1.143 -qed "mod_geq";
   1.144 -
   1.145 -Addsimps [mod_less];
   1.146 -
   1.147 -
   1.148 -(*** Division ***)
   1.149 -
   1.150 -Goalw [raw_div_def] "[| m:nat;  n:nat |] ==> raw_div (m, n) : nat";
   1.151 -by (rtac Ord_transrec_type 1);
   1.152 -by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]));
   1.153 -by (REPEAT (ares_tac div_rls 1));
   1.154 -qed "raw_div_type";
   1.155 -
   1.156 -Goalw [div_def] "m div n : nat";
   1.157 -by (simp_tac (simpset() addsimps [div_def, raw_div_type]) 1);
   1.158 -qed "div_type";
   1.159 -AddTCs [div_type];
   1.160 -AddIffs [div_type];
   1.161 -
   1.162 -Goal "m<n ==> raw_div (m,n) = 0";
   1.163 -by (rtac (raw_div_def RS def_transrec RS trans) 1);
   1.164 -by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1);
   1.165 -qed "raw_div_less";
   1.166 -
   1.167 -Goal "[| m<n; n : nat |] ==> m div n = 0";
   1.168 -by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
   1.169 -by (asm_simp_tac (simpset() addsimps [div_def, raw_div_less]) 1);
   1.170 -qed "div_less";
   1.171 -
   1.172 -Goal "[| 0<n;  n le m;  m:nat |] ==> raw_div(m,n) = succ(raw_div(m#-n, n))";
   1.173 -by (subgoal_tac "n ~= 0" 1);
   1.174 -by (Blast_tac 2);
   1.175 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   1.176 -by (rtac (raw_div_def RS def_transrec RS trans) 1);
   1.177 -by (asm_simp_tac div_ss 1);
   1.178 -qed "raw_div_geq";
   1.179 -
   1.180 -Goal "[| 0<n;  n le m;  m:nat |] ==> m div n = succ ((m#-n) div n)";
   1.181 -by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
   1.182 -by (asm_simp_tac (simpset() addsimps [div_def, raw_div_geq]) 1);
   1.183 -qed "div_geq";
   1.184 -
   1.185 -Addsimps [div_less, div_geq];
   1.186 -
   1.187 -
   1.188 -(*A key result*)
   1.189 -Goal "[| m: nat;  n: nat |] ==> (m div n)#*n #+ m mod n = m";
   1.190 -by (div_undefined_case_tac "n=0" 1);
   1.191 -by (etac complete_induct 1);
   1.192 -by (case_tac "x<n" 1);
   1.193 -(*case n le x*)
   1.194 -by (asm_full_simp_tac
   1.195 -     (simpset() addsimps [not_lt_iff_le, add_assoc, mod_geq,
   1.196 -                         div_termination RS ltD, add_diff_inverse]) 2);
   1.197 -(*case x<n*)
   1.198 -by (Asm_simp_tac 1);
   1.199 -val lemma = result();
   1.200 -
   1.201 -Goal "(m div n)#*n #+ m mod n = natify(m)";
   1.202 -by (subgoal_tac
   1.203 -    "(natify(m) div natify(n))#*natify(n) #+ natify(m) mod natify(n) = \
   1.204 -\    natify(m)" 1);
   1.205 -by (stac lemma 2);
   1.206 -by Auto_tac;
   1.207 -qed "mod_div_equality_natify";
   1.208 -
   1.209 -Goal "m: nat ==> (m div n)#*n #+ m mod n = m";
   1.210 -by (asm_simp_tac (simpset() addsimps [mod_div_equality_natify]) 1);
   1.211 -qed "mod_div_equality";
   1.212 -
   1.213 -
   1.214 -(*** Further facts about mod (mainly for mutilated chess board) ***)
   1.215 -
   1.216 -Goal "[| 0<n;  m:nat;  n:nat |] \
   1.217 -\     ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
   1.218 -by (etac complete_induct 1);
   1.219 -by (excluded_middle_tac "succ(x)<n" 1);
   1.220 -(* case succ(x) < n *)
   1.221 -by (asm_simp_tac (simpset() addsimps [nat_le_refl RS lt_trans, 
   1.222 -				      succ_neq_self]) 2);
   1.223 -by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2);
   1.224 -(* case n le succ(x) *)
   1.225 -by (asm_full_simp_tac (simpset() addsimps [mod_geq, not_lt_iff_le]) 1);
   1.226 -by (etac leE 1);
   1.227 -(*equality case*)
   1.228 -by (asm_full_simp_tac (simpset() addsimps [diff_self_eq_0]) 2);
   1.229 -by (asm_simp_tac (simpset() addsimps [mod_geq, div_termination RS ltD, 
   1.230 -				      diff_succ]) 1);
   1.231 -val lemma = result();
   1.232 -
   1.233 -Goal "n:nat ==> \
   1.234 -\     succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
   1.235 -by (case_tac "n=0" 1);
   1.236 -by (asm_simp_tac (simpset() addsimps [natify_succ, DIVISION_BY_ZERO_MOD]) 1);
   1.237 -by (subgoal_tac
   1.238 -    "natify(succ(m)) mod n = \
   1.239 -\      (if succ(natify(m) mod n) = n then 0 else succ(natify(m) mod n))" 1);
   1.240 -by (stac natify_succ 2);
   1.241 -by (rtac lemma 2);
   1.242 -by (auto_tac(claset(), 
   1.243 -	     simpset() delsimps [natify_succ] 
   1.244 -             addsimps [nat_into_Ord RS Ord_0_lt_iff]));
   1.245 -qed "mod_succ";
   1.246 -
   1.247 -Goal "[| 0<n;  n:nat |] ==> m mod n < n";
   1.248 -by (subgoal_tac "natify(m) mod n < n" 1);
   1.249 -by (res_inst_tac [("i","natify(m)")] complete_induct 2);
   1.250 -by (case_tac "x<n" 3);
   1.251 -(*case x<n*)
   1.252 -by (Asm_simp_tac 3);
   1.253 -(*case n le x*)
   1.254 -by (asm_full_simp_tac
   1.255 -     (simpset() addsimps [mod_geq, not_lt_iff_le, div_termination RS ltD]) 3);
   1.256 -by Auto_tac;
   1.257 -qed "mod_less_divisor";
   1.258 -
   1.259 -Goal "m mod 1 = 0";
   1.260 -by (cut_inst_tac [("n","1")] mod_less_divisor 1);
   1.261 -by Auto_tac; 
   1.262 -qed "mod_1_eq";
   1.263 -Addsimps [mod_1_eq]; 
   1.264 -
   1.265 -Goal "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
   1.266 -by (subgoal_tac "k mod 2: 2" 1);
   1.267 -by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
   1.268 -by (dtac ltD 1);
   1.269 -by Auto_tac;
   1.270 -qed "mod2_cases";
   1.271 -
   1.272 -Goal "succ(succ(m)) mod 2 = m mod 2";
   1.273 -by (subgoal_tac "m mod 2: 2" 1);
   1.274 -by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
   1.275 -by (auto_tac (claset(), simpset() addsimps [mod_succ]));  
   1.276 -qed "mod2_succ_succ";
   1.277 -
   1.278 -Addsimps [mod2_succ_succ];
   1.279 -
   1.280 -Goal "(m#+m#+n) mod 2 = n mod 2";
   1.281 -by (subgoal_tac "(natify(m)#+natify(m)#+n) mod 2 = n mod 2" 1);
   1.282 -by (res_inst_tac [("n","natify(m)")] nat_induct 2);
   1.283 -by Auto_tac;
   1.284 -qed "mod2_add_more";
   1.285 -
   1.286 -Goal "(m#+m) mod 2 = 0";
   1.287 -by (cut_inst_tac [("n","0")] mod2_add_more 1);
   1.288 -by Auto_tac;
   1.289 -qed "mod2_add_self";
   1.290 -
   1.291 -Addsimps [mod2_add_more, mod2_add_self];
   1.292 -
   1.293 -
   1.294 -(**** Additional theorems about "le" ****)
   1.295 -
   1.296 -Goal "m:nat ==> m le (m #+ n)";
   1.297 -by (Asm_simp_tac 1);
   1.298 -qed "add_le_self";
   1.299 -
   1.300 -Goal "m:nat ==> m le (n #+ m)";
   1.301 -by (Asm_simp_tac 1);
   1.302 -qed "add_le_self2";
   1.303 -
   1.304 -(*** Monotonicity of Multiplication ***)
   1.305 -
   1.306 -Goal "[| i le j; j:nat |] ==> (i#*k) le (j#*k)";
   1.307 -by (subgoal_tac "natify(i)#*natify(k) le j#*natify(k)" 1);
   1.308 -by (ftac lt_nat_in_nat 2);
   1.309 -by (res_inst_tac [("n","natify(k)")] nat_induct 3);
   1.310 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_le_mono])));
   1.311 -qed "mult_le_mono1";
   1.312 -
   1.313 -(* le monotonicity, BOTH arguments*)
   1.314 -Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l";
   1.315 -by (rtac (mult_le_mono1 RS le_trans) 1);
   1.316 -by (REPEAT (assume_tac 1));
   1.317 -by (EVERY [stac mult_commute 1,
   1.318 -           stac mult_commute 1,
   1.319 -           rtac mult_le_mono1 1]);
   1.320 -by (REPEAT (assume_tac 1));
   1.321 -qed "mult_le_mono";
   1.322 -
   1.323 -(*strict, in 1st argument; proof is by induction on k>0.
   1.324 -  I can't see how to relax the typing conditions.*)
   1.325 -Goal "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
   1.326 -by (etac zero_lt_natE 1);
   1.327 -by (ftac lt_nat_in_nat 2);
   1.328 -by (ALLGOALS Asm_simp_tac);
   1.329 -by (induct_tac "x" 1);
   1.330 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
   1.331 -qed "mult_lt_mono2";
   1.332 -
   1.333 -Goal "[| i<j; 0<k; j:nat; k:nat |] ==> i#*k < j#*k";
   1.334 -by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, 
   1.335 -				      inst "n" "k" mult_commute]) 1);
   1.336 -qed "mult_lt_mono1";
   1.337 -
   1.338 -Goal "m#+n = 0 <-> natify(m)=0 & natify(n)=0";
   1.339 -by (subgoal_tac "natify(m) #+ natify(n) = 0 <-> natify(m)=0 & natify(n)=0" 1);
   1.340 -by (res_inst_tac [("n","natify(m)")] natE 2);
   1.341 - by (res_inst_tac [("n","natify(n)")] natE 4);
   1.342 -by Auto_tac;  
   1.343 -qed "add_eq_0_iff";
   1.344 -AddIffs [add_eq_0_iff];
   1.345 -
   1.346 -Goal "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)";
   1.347 -by (subgoal_tac "0 < natify(m)#*natify(n) <-> \
   1.348 -\                0 < natify(m) & 0 < natify(n)" 1);
   1.349 -by (res_inst_tac [("n","natify(m)")] natE 2);
   1.350 - by (res_inst_tac [("n","natify(n)")] natE 4);
   1.351 -  by (res_inst_tac [("n","natify(n)")] natE 3);
   1.352 -by Auto_tac;  
   1.353 -qed "zero_lt_mult_iff";
   1.354 -
   1.355 -Goal "m#*n = 1 <-> natify(m)=1 & natify(n)=1";
   1.356 -by (subgoal_tac "natify(m) #* natify(n) = 1 <-> natify(m)=1 & natify(n)=1" 1);
   1.357 -by (res_inst_tac [("n","natify(m)")] natE 2);
   1.358 - by (res_inst_tac [("n","natify(n)")] natE 4);
   1.359 -by Auto_tac;  
   1.360 -qed "mult_eq_1_iff";
   1.361 -AddIffs [zero_lt_mult_iff, mult_eq_1_iff];
   1.362 -
   1.363 -Goal "[|m: nat; n: nat|] ==> (m #* n = 0) <-> (m = 0 | n = 0)";
   1.364 -by Auto_tac;
   1.365 -by (etac natE 1);  
   1.366 -by (etac natE 2);
   1.367 -by Auto_tac; 
   1.368 -qed "mult_is_zero";
   1.369 -
   1.370 -Goal "(m #* n = 0) <-> (natify(m) = 0 | natify(n) = 0)";
   1.371 -by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] mult_is_zero 1); 
   1.372 -by Auto_tac; 
   1.373 -qed "mult_is_zero_natify";
   1.374 -AddIffs [mult_is_zero_natify];
   1.375 -
   1.376 -
   1.377 -(** Cancellation laws for common factors in comparisons **)
   1.378 -
   1.379 -Goal "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) <-> (0<k & m<n)";
   1.380 -by (safe_tac (claset() addSIs [mult_lt_mono1]));
   1.381 -by (etac natE 1);
   1.382 -by Auto_tac;  
   1.383 -by (rtac (not_le_iff_lt RS iffD1) 1); 
   1.384 -by (dtac (not_le_iff_lt RSN (2,rev_iffD2)) 3); 
   1.385 -by (blast_tac (claset() addIs [mult_le_mono1]) 5); 
   1.386 -by Auto_tac;  
   1.387 -val lemma = result();
   1.388 -
   1.389 -Goal "(m#*k < n#*k) <-> (0 < natify(k) & natify(m) < natify(n))";
   1.390 -by (rtac iff_trans 1);
   1.391 -by (rtac lemma 2);
   1.392 -by Auto_tac;  
   1.393 -qed "mult_less_cancel2";
   1.394 -
   1.395 -Goal "(k#*m < k#*n) <-> (0 < natify(k) & natify(m) < natify(n))";
   1.396 -by (simp_tac (simpset() addsimps [mult_less_cancel2, 
   1.397 -                                  inst "m" "k" mult_commute]) 1);
   1.398 -qed "mult_less_cancel1";
   1.399 -Addsimps [mult_less_cancel1, mult_less_cancel2];
   1.400 -
   1.401 -Goal "(m#*k le n#*k) <-> (0 < natify(k) --> natify(m) le natify(n))";
   1.402 -by (asm_simp_tac (simpset() addsimps [not_lt_iff_le RS iff_sym]) 1);
   1.403 -by Auto_tac;  
   1.404 -qed "mult_le_cancel2";
   1.405 -
   1.406 -Goal "(k#*m le k#*n) <-> (0 < natify(k) --> natify(m) le natify(n))";
   1.407 -by (asm_simp_tac (simpset() addsimps [not_lt_iff_le RS iff_sym]) 1);
   1.408 -by Auto_tac;  
   1.409 -qed "mult_le_cancel1";
   1.410 -Addsimps [mult_le_cancel1, mult_le_cancel2];
   1.411 -
   1.412 -Goal "k : nat ==> k #* m le k \\<longleftrightarrow> (0 < k \\<longrightarrow> natify(m) le 1)";
   1.413 -by (cut_inst_tac [("k","k"),("m","m"),("n","1")] mult_le_cancel1 1);
   1.414 -by Auto_tac;
   1.415 -qed "mult_le_cancel_le1";
   1.416 -
   1.417 -Goal "[| Ord(m); Ord(n) |] ==> m=n <-> (m le n & n le m)";
   1.418 -by (blast_tac (claset() addIs [le_anti_sym]) 1); 
   1.419 -qed "Ord_eq_iff_le";
   1.420 -
   1.421 -Goal "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) <-> (m=n | k=0)";
   1.422 -by (asm_simp_tac (simpset() addsimps [inst "m" "m#*k" Ord_eq_iff_le,
   1.423 -                                      inst "m" "m" Ord_eq_iff_le]) 1); 
   1.424 -by (auto_tac (claset(), simpset() addsimps [Ord_0_lt_iff]));  
   1.425 -val lemma = result();
   1.426 -
   1.427 -Goal "(m#*k = n#*k) <-> (natify(m) = natify(n) | natify(k) = 0)";
   1.428 -by (rtac iff_trans 1);
   1.429 -by (rtac lemma 2);
   1.430 -by Auto_tac;  
   1.431 -qed "mult_cancel2";
   1.432 -
   1.433 -Goal "(k#*m = k#*n) <-> (natify(m) = natify(n) | natify(k) = 0)";
   1.434 -by (simp_tac (simpset() addsimps [mult_cancel2, inst "m" "k" mult_commute]) 1);
   1.435 -qed "mult_cancel1";
   1.436 -Addsimps [mult_cancel1, mult_cancel2];
   1.437 -
   1.438 -
   1.439 -(** Cancellation law for division **)
   1.440 -
   1.441 -Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n";
   1.442 -by (eres_inst_tac [("i","m")] complete_induct 1);
   1.443 -by (excluded_middle_tac "x<n" 1);
   1.444 -by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff, 
   1.445 -                                     mult_lt_mono2]) 2);
   1.446 -by (asm_full_simp_tac
   1.447 -     (simpset() addsimps [not_lt_iff_le, 
   1.448 -                         zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq,
   1.449 -                         diff_mult_distrib2 RS sym,
   1.450 -                         div_termination RS ltD]) 1);
   1.451 -qed "div_cancel_raw";
   1.452 -
   1.453 -Goal "[| 0 < natify(n);  0 < natify(k) |] ==> (k#*m) div (k#*n) = m div n";
   1.454 -by (cut_inst_tac [("k","natify(k)"),("m","natify(m)"),("n","natify(n)")] 
   1.455 -    div_cancel_raw 1);
   1.456 -by Auto_tac; 
   1.457 -qed "div_cancel";
   1.458 -
   1.459 -
   1.460 -(** Distributive law for remainder (mod) **)
   1.461 -
   1.462 -Goal "[| k:nat; m:nat; n:nat |] ==> (k#*m) mod (k#*n) = k #* (m mod n)";
   1.463 -by (div_undefined_case_tac "k=0" 1);
   1.464 -by (div_undefined_case_tac "n=0" 1);
   1.465 -by (eres_inst_tac [("i","m")] complete_induct 1);
   1.466 -by (case_tac "x<n" 1);
   1.467 - by (asm_simp_tac
   1.468 -     (simpset() addsimps [mod_less, zero_lt_mult_iff, mult_lt_mono2]) 1);
   1.469 -by (asm_full_simp_tac
   1.470 -     (simpset() addsimps [not_lt_iff_le, 
   1.471 -                         zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq,
   1.472 -                         diff_mult_distrib2 RS sym,
   1.473 -                         div_termination RS ltD]) 1);
   1.474 -qed "mult_mod_distrib_raw";
   1.475 -
   1.476 -Goal "k #* (m mod n) = (k#*m) mod (k#*n)";
   1.477 -by (cut_inst_tac [("k","natify(k)"),("m","natify(m)"),("n","natify(n)")] 
   1.478 -    mult_mod_distrib_raw 1);
   1.479 -by Auto_tac; 
   1.480 -qed "mod_mult_distrib2";
   1.481 -
   1.482 -Goal "(m mod n) #* k = (m#*k) mod (n#*k)";
   1.483 -by (simp_tac (simpset() addsimps [mult_commute, mod_mult_distrib2]) 1); 
   1.484 -qed "mult_mod_distrib";
   1.485 -
   1.486 -Goal "n \\<in> nat ==> (m #+ n) mod n = m mod n";
   1.487 -by (subgoal_tac "(n #+ m) mod n = (n #+ m #- n) mod n" 1);
   1.488 -by (stac (mod_geq RS sym) 2);
   1.489 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
   1.490 -qed "mod_add_self2_raw";
   1.491 -
   1.492 -Goal "(m #+ n) mod n = m mod n";
   1.493 -by (cut_inst_tac [("n","natify(n)")] mod_add_self2_raw 1);
   1.494 -by Auto_tac; 
   1.495 -qed "mod_add_self2";
   1.496 -
   1.497 -Goal "(n#+m) mod n = m mod n";
   1.498 -by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
   1.499 -qed "mod_add_self1";
   1.500 -Addsimps [mod_add_self1, mod_add_self2];
   1.501 -
   1.502 -
   1.503 -Goal "k \\<in> nat ==> (m #+ k#*n) mod n = m mod n";
   1.504 -by (etac nat_induct 1); 
   1.505 -by (ALLGOALS
   1.506 -    (asm_simp_tac 
   1.507 -     (simpset() addsimps [inst "n" "n" add_left_commute])));
   1.508 -qed "mod_mult_self1_raw";
   1.509 -
   1.510 -Goal "(m #+ k#*n) mod n = m mod n";
   1.511 -by (cut_inst_tac [("k","natify(k)")] mod_mult_self1_raw 1);
   1.512 -by Auto_tac; 
   1.513 -qed "mod_mult_self1";
   1.514 -
   1.515 -Goal "(m #+ n#*k) mod n = m mod n";
   1.516 -by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
   1.517 -qed "mod_mult_self2";
   1.518 -
   1.519 -Addsimps [mod_mult_self1, mod_mult_self2];
   1.520 -
   1.521 -(*Lemma for gcd*)
   1.522 -Goal "m = m#*n ==> natify(n)=1 | m=0";
   1.523 -by (subgoal_tac "m: nat" 1);
   1.524 -by (etac ssubst 2);
   1.525 -by (rtac disjCI 1);
   1.526 -by (dtac sym 1);
   1.527 -by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
   1.528 -by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 3);
   1.529 -by Auto_tac;
   1.530 -by (subgoal_tac "m #* n = 0" 1);
   1.531 -by (stac (mult_natify2 RS sym) 2);
   1.532 -by (auto_tac (claset(), simpset() delsimps [mult_natify2]));  
   1.533 -qed "mult_eq_self_implies_10";
   1.534 -
   1.535 -Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
   1.536 -by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
   1.537 -by (etac rev_mp 1);
   1.538 -by (induct_tac "n" 1);
   1.539 -by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
   1.540 -by (blast_tac (claset() addSEs [leE] 
   1.541 -                        addSIs [add_0_right RS sym, add_succ_right RS sym]) 1);
   1.542 -qed_spec_mp "less_imp_succ_add";
   1.543 -
   1.544 -Goal "[| m: nat; n: nat |] ==> (m<n) <-> (EX k: nat. n = succ(m#+k))";
   1.545 -by (auto_tac (claset() addIs [less_imp_succ_add], simpset()));
   1.546 -qed "less_iff_succ_add";
   1.547 -
   1.548 -(* on nat *)
   1.549 -
   1.550 -Goal "m #- n = 0 <-> natify(m) le natify(n)";
   1.551 -by (auto_tac (claset(), simpset() addsimps 
   1.552 -      [le_iff, diff_self_eq_0]));
   1.553 -by (full_simp_tac (simpset() addsimps [less_iff_succ_add ]) 2);
   1.554 -by (Clarify_tac 2);
   1.555 -by (subgoal_tac "natify(m) #- natify(n) = 0" 3);
   1.556 -by (etac subst 3);
   1.557 -by (ALLGOALS(asm_full_simp_tac (simpset() 
   1.558 -             addsimps [diff_self_eq_0])));
   1.559 -by (subgoal_tac "natify(m) #- natify(n) = 0" 2);
   1.560 -by (etac subst 2);
   1.561 -by (etac ssubst  3);
   1.562 -by (rtac (not_le_iff_lt RS iffD1) 1);
   1.563 -by (auto_tac (claset(), simpset() addsimps [le_iff]));
   1.564 -by (subgoal_tac "natify(m) #- natify(n) = 0" 1);
   1.565 -by (Asm_simp_tac 2);
   1.566 -by (thin_tac "m #- n = 0" 1);
   1.567 -by (dtac ([natify_in_nat, natify_in_nat] MRS zero_less_diff RS iffD2) 1);
   1.568 -by Auto_tac;
   1.569 -qed "diff_is_0_iff";
   1.570 -
   1.571 -Goal "[| a:nat; b:nat |] ==> \
   1.572 -\ (P(a #- b)) <-> ((a < b -->P(0)) & (ALL d:nat. a = b #+ d --> P(d)))";
   1.573 -by (case_tac "a le b" 1);
   1.574 -by (subgoal_tac "natify(a) le natify(b)" 1);
   1.575 -by (dtac (diff_is_0_iff RS iffD2) 1);
   1.576 -by Safe_tac;
   1.577 -by (ALLGOALS(Asm_full_simp_tac));
   1.578 -by (ALLGOALS(rotate_tac ~1));
   1.579 -by (ALLGOALS(asm_full_simp_tac  (simpset() addsimps [le_iff])));
   1.580 -by (Clarify_tac 2);
   1.581 -by (ALLGOALS(dtac not_lt_imp_le));
   1.582 -by (ALLGOALS(Asm_full_simp_tac));
   1.583 -by (ALLGOALS(dres_inst_tac [("x", "a #- b")] bspec));
   1.584 -by (ALLGOALS(Asm_simp_tac));
   1.585 -by (ALLGOALS(dtac add_diff_inverse));
   1.586 -by (ALLGOALS(rotate_tac ~1));
   1.587 -by (ALLGOALS(Asm_full_simp_tac));
   1.588 -qed "nat_diff_split";
   1.589 -
   1.590 -
   1.591 -
     2.1 --- a/src/ZF/ArithSimp.thy	Fri Jun 28 20:01:09 2002 +0200
     2.2 +++ b/src/ZF/ArithSimp.thy	Sat Jun 29 21:33:06 2002 +0200
     2.3 @@ -8,4 +8,585 @@
     2.4  
     2.5  theory ArithSimp = Arith
     2.6  files "arith_data.ML":
     2.7 +
     2.8 +(*** Difference ***)
     2.9 +
    2.10 +lemma diff_self_eq_0: "m #- m = 0"
    2.11 +apply (subgoal_tac "natify (m) #- natify (m) = 0")
    2.12 +apply (rule_tac [2] natify_in_nat [THEN nat_induct], auto)
    2.13 +done
    2.14 +
    2.15 +(**Addition is the inverse of subtraction**)
    2.16 +
    2.17 +(*We need m:nat even if we replace the RHS by natify(m), for consider e.g.
    2.18 +  n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 ~= 0 = natify(m).*)
    2.19 +lemma add_diff_inverse: "[| n le m;  m:nat |] ==> n #+ (m#-n) = m"
    2.20 +apply (frule lt_nat_in_nat, erule nat_succI)
    2.21 +apply (erule rev_mp)
    2.22 +apply (rule_tac m = "m" and n = "n" in diff_induct, auto)
    2.23 +done
    2.24 +
    2.25 +lemma add_diff_inverse2: "[| n le m;  m:nat |] ==> (m#-n) #+ n = m"
    2.26 +apply (frule lt_nat_in_nat, erule nat_succI)
    2.27 +apply (simp (no_asm_simp) add: add_commute add_diff_inverse)
    2.28 +done
    2.29 +
    2.30 +(*Proof is IDENTICAL to that of add_diff_inverse*)
    2.31 +lemma diff_succ: "[| n le m;  m:nat |] ==> succ(m) #- n = succ(m#-n)"
    2.32 +apply (frule lt_nat_in_nat, erule nat_succI)
    2.33 +apply (erule rev_mp)
    2.34 +apply (rule_tac m = "m" and n = "n" in diff_induct)
    2.35 +apply (simp_all (no_asm_simp))
    2.36 +done
    2.37 +
    2.38 +lemma zero_less_diff [simp]:
    2.39 +     "[| m: nat; n: nat |] ==> 0 < (n #- m)   <->   m<n"
    2.40 +apply (rule_tac m = "m" and n = "n" in diff_induct)
    2.41 +apply (simp_all (no_asm_simp))
    2.42 +done
    2.43 +
    2.44 +
    2.45 +(** Difference distributes over multiplication **)
    2.46 +
    2.47 +lemma diff_mult_distrib: "(m #- n) #* k = (m #* k) #- (n #* k)"
    2.48 +apply (subgoal_tac " (natify (m) #- natify (n)) #* natify (k) = (natify (m) #* natify (k)) #- (natify (n) #* natify (k))")
    2.49 +apply (rule_tac [2] m = "natify (m) " and n = "natify (n) " in diff_induct)
    2.50 +apply (simp_all add: diff_cancel)
    2.51 +done
    2.52 +
    2.53 +lemma diff_mult_distrib2: "k #* (m #- n) = (k #* m) #- (k #* n)"
    2.54 +apply (simp (no_asm) add: mult_commute [of k] diff_mult_distrib)
    2.55 +done
    2.56 +
    2.57 +
    2.58 +(*** Remainder ***)
    2.59 +
    2.60 +(*We need m:nat even with natify*)
    2.61 +lemma div_termination: "[| 0<n;  n le m;  m:nat |] ==> m #- n < m"
    2.62 +apply (frule lt_nat_in_nat, erule nat_succI)
    2.63 +apply (erule rev_mp)
    2.64 +apply (erule rev_mp)
    2.65 +apply (rule_tac m = "m" and n = "n" in diff_induct)
    2.66 +apply (simp_all (no_asm_simp) add: diff_le_self)
    2.67 +done
    2.68 +
    2.69 +(*for mod and div*)
    2.70 +lemmas div_rls = 
    2.71 +    nat_typechecks Ord_transrec_type apply_funtype 
    2.72 +    div_termination [THEN ltD]
    2.73 +    nat_into_Ord not_lt_iff_le [THEN iffD1]
    2.74 +
    2.75 +lemma raw_mod_type: "[| m:nat;  n:nat |] ==> raw_mod (m, n) : nat"
    2.76 +apply (unfold raw_mod_def)
    2.77 +apply (rule Ord_transrec_type)
    2.78 +apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff])
    2.79 +apply (blast intro: div_rls) 
    2.80 +done
    2.81 +
    2.82 +lemma mod_type [TC,iff]: "m mod n : nat"
    2.83 +apply (unfold mod_def)
    2.84 +apply (simp (no_asm) add: mod_def raw_mod_type)
    2.85 +done
    2.86 +
    2.87 +
    2.88 +(** Aribtrary definitions for division by zero.  Useful to simplify 
    2.89 +    certain equations **)
    2.90 +
    2.91 +lemma DIVISION_BY_ZERO_DIV: "a div 0 = 0"
    2.92 +apply (unfold div_def)
    2.93 +apply (rule raw_div_def [THEN def_transrec, THEN trans])
    2.94 +apply (simp (no_asm_simp))
    2.95 +done  (*NOT for adding to default simpset*)
    2.96 +
    2.97 +lemma DIVISION_BY_ZERO_MOD: "a mod 0 = natify(a)"
    2.98 +apply (unfold mod_def)
    2.99 +apply (rule raw_mod_def [THEN def_transrec, THEN trans])
   2.100 +apply (simp (no_asm_simp))
   2.101 +done  (*NOT for adding to default simpset*)
   2.102 +
   2.103 +lemma raw_mod_less: "m<n ==> raw_mod (m,n) = m"
   2.104 +apply (rule raw_mod_def [THEN def_transrec, THEN trans])
   2.105 +apply (simp (no_asm_simp) add: div_termination [THEN ltD])
   2.106 +done
   2.107 +
   2.108 +lemma mod_less [simp]: "[| m<n; n : nat |] ==> m mod n = m"
   2.109 +apply (frule lt_nat_in_nat, assumption)
   2.110 +apply (simp (no_asm_simp) add: mod_def raw_mod_less)
   2.111 +done
   2.112 +
   2.113 +lemma raw_mod_geq:
   2.114 +     "[| 0<n; n le m;  m:nat |] ==> raw_mod (m, n) = raw_mod (m#-n, n)"
   2.115 +apply (frule lt_nat_in_nat, erule nat_succI)
   2.116 +apply (rule raw_mod_def [THEN def_transrec, THEN trans])
   2.117 +apply (simp add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2], blast)
   2.118 +done
   2.119 +
   2.120 +
   2.121 +lemma mod_geq: "[| n le m;  m:nat |] ==> m mod n = (m#-n) mod n"
   2.122 +apply (frule lt_nat_in_nat, erule nat_succI)
   2.123 +apply (case_tac "n=0")
   2.124 + apply (simp add: DIVISION_BY_ZERO_MOD)
   2.125 +apply (simp add: mod_def raw_mod_geq nat_into_Ord [THEN Ord_0_lt_iff])
   2.126 +done
   2.127 +
   2.128 +
   2.129 +(*** Division ***)
   2.130 +
   2.131 +lemma raw_div_type: "[| m:nat;  n:nat |] ==> raw_div (m, n) : nat"
   2.132 +apply (unfold raw_div_def)
   2.133 +apply (rule Ord_transrec_type)
   2.134 +apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff])
   2.135 +apply (blast intro: div_rls) 
   2.136 +done
   2.137 +
   2.138 +lemma div_type [TC,iff]: "m div n : nat"
   2.139 +apply (unfold div_def)
   2.140 +apply (simp (no_asm) add: div_def raw_div_type)
   2.141 +done
   2.142 +
   2.143 +lemma raw_div_less: "m<n ==> raw_div (m,n) = 0"
   2.144 +apply (rule raw_div_def [THEN def_transrec, THEN trans])
   2.145 +apply (simp (no_asm_simp) add: div_termination [THEN ltD])
   2.146 +done
   2.147 +
   2.148 +lemma div_less [simp]: "[| m<n; n : nat |] ==> m div n = 0"
   2.149 +apply (frule lt_nat_in_nat, assumption)
   2.150 +apply (simp (no_asm_simp) add: div_def raw_div_less)
   2.151 +done
   2.152 +
   2.153 +lemma raw_div_geq: "[| 0<n;  n le m;  m:nat |] ==> raw_div(m,n) = succ(raw_div(m#-n, n))"
   2.154 +apply (subgoal_tac "n ~= 0")
   2.155 +prefer 2 apply blast
   2.156 +apply (frule lt_nat_in_nat, erule nat_succI)
   2.157 +apply (rule raw_div_def [THEN def_transrec, THEN trans])
   2.158 +apply (simp add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2] ) 
   2.159 +done
   2.160 +
   2.161 +lemma div_geq [simp]:
   2.162 +     "[| 0<n;  n le m;  m:nat |] ==> m div n = succ ((m#-n) div n)"
   2.163 +apply (frule lt_nat_in_nat, erule nat_succI)
   2.164 +apply (simp (no_asm_simp) add: div_def raw_div_geq)
   2.165 +done
   2.166 +
   2.167 +declare div_less [simp] div_geq [simp]
   2.168 +
   2.169 +
   2.170 +(*A key result*)
   2.171 +lemma mod_div_lemma: "[| m: nat;  n: nat |] ==> (m div n)#*n #+ m mod n = m"
   2.172 +apply (case_tac "n=0")
   2.173 + apply (simp add: DIVISION_BY_ZERO_MOD)
   2.174 +apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff])
   2.175 +apply (erule complete_induct)
   2.176 +apply (case_tac "x<n")
   2.177 +txt{*case x<n*}
   2.178 +apply (simp (no_asm_simp))
   2.179 +txt{*case n le x*}
   2.180 +apply (simp add: not_lt_iff_le add_assoc mod_geq div_termination [THEN ltD] add_diff_inverse)
   2.181 +done
   2.182 +
   2.183 +lemma mod_div_equality_natify: "(m div n)#*n #+ m mod n = natify(m)"
   2.184 +apply (subgoal_tac " (natify (m) div natify (n))#*natify (n) #+ natify (m) mod natify (n) = natify (m) ")
   2.185 +apply force 
   2.186 +apply (subst mod_div_lemma, auto)
   2.187 +done
   2.188 +
   2.189 +lemma mod_div_equality: "m: nat ==> (m div n)#*n #+ m mod n = m"
   2.190 +apply (simp (no_asm_simp) add: mod_div_equality_natify)
   2.191 +done
   2.192 +
   2.193 +
   2.194 +(*** Further facts about mod (mainly for mutilated chess board) ***)
   2.195 +
   2.196 +lemma mod_succ_lemma:
   2.197 +     "[| 0<n;  m:nat;  n:nat |]  
   2.198 +      ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))"
   2.199 +apply (erule complete_induct)
   2.200 +apply (case_tac "succ (x) <n")
   2.201 +txt{* case succ(x) < n *}
   2.202 + apply (simp (no_asm_simp) add: nat_le_refl [THEN lt_trans] succ_neq_self)
   2.203 + apply (simp add: ltD [THEN mem_imp_not_eq])
   2.204 +txt{* case n le succ(x) *}
   2.205 +apply (simp add: mod_geq not_lt_iff_le)
   2.206 +apply (erule leE)
   2.207 + apply (simp (no_asm_simp) add: mod_geq div_termination [THEN ltD] diff_succ)
   2.208 +txt{*equality case*}
   2.209 +apply (simp add: diff_self_eq_0)
   2.210 +done
   2.211 +
   2.212 +lemma mod_succ:
   2.213 +  "n:nat ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))"
   2.214 +apply (case_tac "n=0")
   2.215 + apply (simp (no_asm_simp) add: natify_succ DIVISION_BY_ZERO_MOD)
   2.216 +apply (subgoal_tac "natify (succ (m)) mod n = (if succ (natify (m) mod n) = n then 0 else succ (natify (m) mod n))")
   2.217 + prefer 2
   2.218 + apply (subst natify_succ)
   2.219 + apply (rule mod_succ_lemma)
   2.220 +  apply (auto simp del: natify_succ simp add: nat_into_Ord [THEN Ord_0_lt_iff])
   2.221 +done
   2.222 +
   2.223 +lemma mod_less_divisor: "[| 0<n;  n:nat |] ==> m mod n < n"
   2.224 +apply (subgoal_tac "natify (m) mod n < n")
   2.225 +apply (rule_tac [2] i = "natify (m) " in complete_induct)
   2.226 +apply (case_tac [3] "x<n", auto) 
   2.227 +txt{* case n le x*}
   2.228 +apply (simp add: mod_geq not_lt_iff_le div_termination [THEN ltD])
   2.229 +done
   2.230 +
   2.231 +lemma mod_1_eq [simp]: "m mod 1 = 0"
   2.232 +by (cut_tac n = "1" in mod_less_divisor, auto)
   2.233 +
   2.234 +lemma mod2_cases: "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)"
   2.235 +apply (subgoal_tac "k mod 2: 2")
   2.236 + prefer 2 apply (simp add: mod_less_divisor [THEN ltD])
   2.237 +apply (drule ltD, auto)
   2.238 +done
   2.239 +
   2.240 +lemma mod2_succ_succ [simp]: "succ(succ(m)) mod 2 = m mod 2"
   2.241 +apply (subgoal_tac "m mod 2: 2")
   2.242 + prefer 2 apply (simp add: mod_less_divisor [THEN ltD])
   2.243 +apply (auto simp add: mod_succ)
   2.244 +done
   2.245 +
   2.246 +lemma mod2_add_more [simp]: "(m#+m#+n) mod 2 = n mod 2"
   2.247 +apply (subgoal_tac " (natify (m) #+natify (m) #+n) mod 2 = n mod 2")
   2.248 +apply (rule_tac [2] n = "natify (m) " in nat_induct)
   2.249 +apply auto
   2.250 +done
   2.251 +
   2.252 +lemma mod2_add_self [simp]: "(m#+m) mod 2 = 0"
   2.253 +by (cut_tac n = "0" in mod2_add_more, auto)
   2.254 +
   2.255 +
   2.256 +(**** Additional theorems about "le" ****)
   2.257 +
   2.258 +lemma add_le_self: "m:nat ==> m le (m #+ n)"
   2.259 +apply (simp (no_asm_simp))
   2.260 +done
   2.261 +
   2.262 +lemma add_le_self2: "m:nat ==> m le (n #+ m)"
   2.263 +apply (simp (no_asm_simp))
   2.264 +done
   2.265 +
   2.266 +(*** Monotonicity of Multiplication ***)
   2.267 +
   2.268 +lemma mult_le_mono1: "[| i le j; j:nat |] ==> (i#*k) le (j#*k)"
   2.269 +apply (subgoal_tac "natify (i) #*natify (k) le j#*natify (k) ")
   2.270 +apply (frule_tac [2] lt_nat_in_nat)
   2.271 +apply (rule_tac [3] n = "natify (k) " in nat_induct)
   2.272 +apply (simp_all add: add_le_mono)
   2.273 +done
   2.274 +
   2.275 +(* le monotonicity, BOTH arguments*)
   2.276 +lemma mult_le_mono: "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l"
   2.277 +apply (rule mult_le_mono1 [THEN le_trans], assumption+)
   2.278 +apply (subst mult_commute, subst mult_commute, rule mult_le_mono1, assumption+)
   2.279 +done
   2.280 +
   2.281 +(*strict, in 1st argument; proof is by induction on k>0.
   2.282 +  I can't see how to relax the typing conditions.*)
   2.283 +lemma mult_lt_mono2: "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j"
   2.284 +apply (erule zero_lt_natE)
   2.285 +apply (frule_tac [2] lt_nat_in_nat)
   2.286 +apply (simp_all (no_asm_simp))
   2.287 +apply (induct_tac "x")
   2.288 +apply (simp_all (no_asm_simp) add: add_lt_mono)
   2.289 +done
   2.290 +
   2.291 +lemma mult_lt_mono1: "[| i<j; 0<k; j:nat; k:nat |] ==> i#*k < j#*k"
   2.292 +apply (simp (no_asm_simp) add: mult_lt_mono2 mult_commute [of _ k])
   2.293 +done
   2.294 +
   2.295 +lemma add_eq_0_iff [iff]: "m#+n = 0 <-> natify(m)=0 & natify(n)=0"
   2.296 +apply (subgoal_tac "natify (m) #+ natify (n) = 0 <-> natify (m) =0 & natify (n) =0")
   2.297 +apply (rule_tac [2] n = "natify (m) " in natE)
   2.298 + apply (rule_tac [4] n = "natify (n) " in natE)
   2.299 +apply auto
   2.300 +done
   2.301 +
   2.302 +lemma zero_lt_mult_iff [iff]: "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)"
   2.303 +apply (subgoal_tac "0 < natify (m) #*natify (n) <-> 0 < natify (m) & 0 < natify (n) ")
   2.304 +apply (rule_tac [2] n = "natify (m) " in natE)
   2.305 + apply (rule_tac [4] n = "natify (n) " in natE)
   2.306 +  apply (rule_tac [3] n = "natify (n) " in natE)
   2.307 +apply auto
   2.308 +done
   2.309 +
   2.310 +lemma mult_eq_1_iff [iff]: "m#*n = 1 <-> natify(m)=1 & natify(n)=1"
   2.311 +apply (subgoal_tac "natify (m) #* natify (n) = 1 <-> natify (m) =1 & natify (n) =1")
   2.312 +apply (rule_tac [2] n = "natify (m) " in natE)
   2.313 + apply (rule_tac [4] n = "natify (n) " in natE)
   2.314 +apply auto
   2.315 +done
   2.316 +
   2.317 +
   2.318 +lemma mult_is_zero: "[|m: nat; n: nat|] ==> (m #* n = 0) <-> (m = 0 | n = 0)"
   2.319 +apply auto
   2.320 +apply (erule natE)
   2.321 +apply (erule_tac [2] natE, auto)
   2.322 +done
   2.323 +
   2.324 +lemma mult_is_zero_natify [iff]:
   2.325 +     "(m #* n = 0) <-> (natify(m) = 0 | natify(n) = 0)"
   2.326 +apply (cut_tac m = "natify (m) " and n = "natify (n) " in mult_is_zero)
   2.327 +apply auto
   2.328 +done
   2.329 +
   2.330 +
   2.331 +(** Cancellation laws for common factors in comparisons **)
   2.332 +
   2.333 +lemma mult_less_cancel_lemma:
   2.334 +     "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) <-> (0<k & m<n)"
   2.335 +apply (safe intro!: mult_lt_mono1)
   2.336 +apply (erule natE, auto)
   2.337 +apply (rule not_le_iff_lt [THEN iffD1])
   2.338 +apply (drule_tac [3] not_le_iff_lt [THEN [2] rev_iffD2])
   2.339 +prefer 5 apply (blast intro: mult_le_mono1, auto)
   2.340 +done
   2.341 +
   2.342 +lemma mult_less_cancel2 [simp]:
   2.343 +     "(m#*k < n#*k) <-> (0 < natify(k) & natify(m) < natify(n))"
   2.344 +apply (rule iff_trans)
   2.345 +apply (rule_tac [2] mult_less_cancel_lemma, auto)
   2.346 +done
   2.347 +
   2.348 +lemma mult_less_cancel1 [simp]:
   2.349 +     "(k#*m < k#*n) <-> (0 < natify(k) & natify(m) < natify(n))"
   2.350 +apply (simp (no_asm) add: mult_less_cancel2 mult_commute [of k])
   2.351 +done
   2.352 +
   2.353 +lemma mult_le_cancel2 [simp]: "(m#*k le n#*k) <-> (0 < natify(k) --> natify(m) le natify(n))"
   2.354 +apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])
   2.355 +apply auto
   2.356 +done
   2.357 +
   2.358 +lemma mult_le_cancel1 [simp]: "(k#*m le k#*n) <-> (0 < natify(k) --> natify(m) le natify(n))"
   2.359 +apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])
   2.360 +apply auto
   2.361 +done
   2.362 +
   2.363 +lemma mult_le_cancel_le1: "k : nat ==> k #* m le k \<longleftrightarrow> (0 < k \<longrightarrow> natify(m) le 1)"
   2.364 +by (cut_tac k = "k" and m = "m" and n = "1" in mult_le_cancel1, auto)
   2.365 +
   2.366 +lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n <-> (m le n & n le m)"
   2.367 +by (blast intro: le_anti_sym)
   2.368 +
   2.369 +lemma mult_cancel2_lemma:
   2.370 +     "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) <-> (m=n | k=0)"
   2.371 +apply (simp (no_asm_simp) add: Ord_eq_iff_le [of "m#*k"] Ord_eq_iff_le [of m])
   2.372 +apply (auto simp add: Ord_0_lt_iff)
   2.373 +done
   2.374 +
   2.375 +lemma mult_cancel2 [simp]:
   2.376 +     "(m#*k = n#*k) <-> (natify(m) = natify(n) | natify(k) = 0)"
   2.377 +apply (rule iff_trans)
   2.378 +apply (rule_tac [2] mult_cancel2_lemma, auto)
   2.379 +done
   2.380 +
   2.381 +lemma mult_cancel1 [simp]:
   2.382 +     "(k#*m = k#*n) <-> (natify(m) = natify(n) | natify(k) = 0)"
   2.383 +apply (simp (no_asm) add: mult_cancel2 mult_commute [of k])
   2.384 +done
   2.385 +
   2.386 +
   2.387 +(** Cancellation law for division **)
   2.388 +
   2.389 +lemma div_cancel_raw:
   2.390 +     "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n"
   2.391 +apply (erule_tac i = "m" in complete_induct)
   2.392 +apply (case_tac "x<n")
   2.393 + apply (simp add: div_less zero_lt_mult_iff mult_lt_mono2)
   2.394 +apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono]
   2.395 +          div_geq diff_mult_distrib2 [symmetric] div_termination [THEN ltD])
   2.396 +done
   2.397 +
   2.398 +lemma div_cancel:
   2.399 +     "[| 0 < natify(n);  0 < natify(k) |] ==> (k#*m) div (k#*n) = m div n"
   2.400 +apply (cut_tac k = "natify (k) " and m = "natify (m)" and n = "natify (n)" 
   2.401 +       in div_cancel_raw)
   2.402 +apply auto
   2.403 +done
   2.404 +
   2.405 +
   2.406 +(** Distributive law for remainder (mod) **)
   2.407 +
   2.408 +lemma mult_mod_distrib_raw:
   2.409 +     "[| k:nat; m:nat; n:nat |] ==> (k#*m) mod (k#*n) = k #* (m mod n)"
   2.410 +apply (case_tac "k=0")
   2.411 + apply (simp add: DIVISION_BY_ZERO_MOD)
   2.412 +apply (case_tac "n=0")
   2.413 + apply (simp add: DIVISION_BY_ZERO_MOD)
   2.414 +apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff])
   2.415 +apply (erule_tac i = "m" in complete_induct)
   2.416 +apply (case_tac "x<n")
   2.417 + apply (simp (no_asm_simp) add: mod_less zero_lt_mult_iff mult_lt_mono2)
   2.418 +apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono] 
   2.419 +         mod_geq diff_mult_distrib2 [symmetric] div_termination [THEN ltD])
   2.420 +done
   2.421 +
   2.422 +lemma mod_mult_distrib2: "k #* (m mod n) = (k#*m) mod (k#*n)"
   2.423 +apply (cut_tac k = "natify (k) " and m = "natify (m)" and n = "natify (n)" 
   2.424 +       in mult_mod_distrib_raw)
   2.425 +apply auto
   2.426 +done
   2.427 +
   2.428 +lemma mult_mod_distrib: "(m mod n) #* k = (m#*k) mod (n#*k)"
   2.429 +apply (simp (no_asm) add: mult_commute mod_mult_distrib2)
   2.430 +done
   2.431 +
   2.432 +lemma mod_add_self2_raw: "n \<in> nat ==> (m #+ n) mod n = m mod n"
   2.433 +apply (subgoal_tac " (n #+ m) mod n = (n #+ m #- n) mod n")
   2.434 +apply (simp add: add_commute) 
   2.435 +apply (subst mod_geq [symmetric], auto) 
   2.436 +done
   2.437 +
   2.438 +lemma mod_add_self2 [simp]: "(m #+ n) mod n = m mod n"
   2.439 +apply (cut_tac n = "natify (n) " in mod_add_self2_raw)
   2.440 +apply auto
   2.441 +done
   2.442 +
   2.443 +lemma mod_add_self1 [simp]: "(n#+m) mod n = m mod n"
   2.444 +apply (simp (no_asm_simp) add: add_commute mod_add_self2)
   2.445 +done
   2.446 +
   2.447 +lemma mod_mult_self1_raw: "k \<in> nat ==> (m #+ k#*n) mod n = m mod n"
   2.448 +apply (erule nat_induct)
   2.449 +apply (simp_all (no_asm_simp) add: add_left_commute [of _ n])
   2.450 +done
   2.451 +
   2.452 +lemma mod_mult_self1 [simp]: "(m #+ k#*n) mod n = m mod n"
   2.453 +apply (cut_tac k = "natify (k) " in mod_mult_self1_raw)
   2.454 +apply auto
   2.455 +done
   2.456 +
   2.457 +lemma mod_mult_self2 [simp]: "(m #+ n#*k) mod n = m mod n"
   2.458 +apply (simp (no_asm) add: mult_commute mod_mult_self1)
   2.459 +done
   2.460 +
   2.461 +(*Lemma for gcd*)
   2.462 +lemma mult_eq_self_implies_10: "m = m#*n ==> natify(n)=1 | m=0"
   2.463 +apply (subgoal_tac "m: nat")
   2.464 + prefer 2 
   2.465 + apply (erule ssubst)
   2.466 + apply simp  
   2.467 +apply (rule disjCI)
   2.468 +apply (drule sym)
   2.469 +apply (rule Ord_linear_lt [of "natify(n)" 1])
   2.470 +apply simp_all  
   2.471 + apply (subgoal_tac "m #* n = 0", simp) 
   2.472 + apply (subst mult_natify2 [symmetric])
   2.473 + apply (simp del: mult_natify2)
   2.474 +apply (drule nat_into_Ord [THEN Ord_0_lt, THEN [2] mult_lt_mono2], auto)
   2.475 +done
   2.476 +
   2.477 +lemma less_imp_succ_add [rule_format]:
   2.478 +     "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)"
   2.479 +apply (frule lt_nat_in_nat, assumption)
   2.480 +apply (erule rev_mp)
   2.481 +apply (induct_tac "n")
   2.482 +apply (simp_all (no_asm) add: le_iff)
   2.483 +apply (blast elim!: leE intro!: add_0_right [symmetric] add_succ_right [symmetric])
   2.484 +done
   2.485 +
   2.486 +lemma less_iff_succ_add:
   2.487 +     "[| m: nat; n: nat |] ==> (m<n) <-> (EX k: nat. n = succ(m#+k))"
   2.488 +by (auto intro: less_imp_succ_add)
   2.489 +
   2.490 +(* on nat *)
   2.491 +
   2.492 +lemma diff_is_0_lemma:
   2.493 +     "[| m: nat; n: nat |] ==> m #- n = 0 <-> m le n"
   2.494 +apply (rule_tac m = "m" and n = "n" in diff_induct, simp_all)
   2.495 +done
   2.496 +
   2.497 +lemma diff_is_0_iff: "m #- n = 0 <-> natify(m) le natify(n)"
   2.498 +by (simp add: diff_is_0_lemma [symmetric])
   2.499 +
   2.500 +lemma nat_lt_imp_diff_eq_0:
   2.501 +     "[| a:nat; b:nat; a<b |] ==> a #- b = 0"
   2.502 +by (simp add: diff_is_0_iff le_iff) 
   2.503 +
   2.504 +lemma nat_diff_split:
   2.505 +     "[| a:nat; b:nat |] ==>  
   2.506 +      (P(a #- b)) <-> ((a < b -->P(0)) & (ALL d:nat. a = b #+ d --> P(d)))"
   2.507 +apply (case_tac "a < b")
   2.508 + apply (force simp add: nat_lt_imp_diff_eq_0)
   2.509 +apply (rule iffI, simp_all) 
   2.510 + apply clarify 
   2.511 + apply (rotate_tac -1) 
   2.512 + apply simp 
   2.513 +apply (drule_tac x="a#-b" in bspec)
   2.514 +apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse) 
   2.515 +done
   2.516 +
   2.517 +ML
   2.518 +{*
   2.519 +val diff_self_eq_0 = thm "diff_self_eq_0";
   2.520 +val add_diff_inverse = thm "add_diff_inverse";
   2.521 +val add_diff_inverse2 = thm "add_diff_inverse2";
   2.522 +val diff_succ = thm "diff_succ";
   2.523 +val zero_less_diff = thm "zero_less_diff";
   2.524 +val diff_mult_distrib = thm "diff_mult_distrib";
   2.525 +val diff_mult_distrib2 = thm "diff_mult_distrib2";
   2.526 +val div_termination = thm "div_termination";
   2.527 +val raw_mod_type = thm "raw_mod_type";
   2.528 +val mod_type = thm "mod_type";
   2.529 +val DIVISION_BY_ZERO_DIV = thm "DIVISION_BY_ZERO_DIV";
   2.530 +val DIVISION_BY_ZERO_MOD = thm "DIVISION_BY_ZERO_MOD";
   2.531 +val raw_mod_less = thm "raw_mod_less";
   2.532 +val mod_less = thm "mod_less";
   2.533 +val raw_mod_geq = thm "raw_mod_geq";
   2.534 +val mod_geq = thm "mod_geq";
   2.535 +val raw_div_type = thm "raw_div_type";
   2.536 +val div_type = thm "div_type";
   2.537 +val raw_div_less = thm "raw_div_less";
   2.538 +val div_less = thm "div_less";
   2.539 +val raw_div_geq = thm "raw_div_geq";
   2.540 +val div_geq = thm "div_geq";
   2.541 +val mod_div_equality_natify = thm "mod_div_equality_natify";
   2.542 +val mod_div_equality = thm "mod_div_equality";
   2.543 +val mod_succ = thm "mod_succ";
   2.544 +val mod_less_divisor = thm "mod_less_divisor";
   2.545 +val mod_1_eq = thm "mod_1_eq";
   2.546 +val mod2_cases = thm "mod2_cases";
   2.547 +val mod2_succ_succ = thm "mod2_succ_succ";
   2.548 +val mod2_add_more = thm "mod2_add_more";
   2.549 +val mod2_add_self = thm "mod2_add_self";
   2.550 +val add_le_self = thm "add_le_self";
   2.551 +val add_le_self2 = thm "add_le_self2";
   2.552 +val mult_le_mono1 = thm "mult_le_mono1";
   2.553 +val mult_le_mono = thm "mult_le_mono";
   2.554 +val mult_lt_mono2 = thm "mult_lt_mono2";
   2.555 +val mult_lt_mono1 = thm "mult_lt_mono1";
   2.556 +val add_eq_0_iff = thm "add_eq_0_iff";
   2.557 +val zero_lt_mult_iff = thm "zero_lt_mult_iff";
   2.558 +val mult_eq_1_iff = thm "mult_eq_1_iff";
   2.559 +val mult_is_zero = thm "mult_is_zero";
   2.560 +val mult_is_zero_natify = thm "mult_is_zero_natify";
   2.561 +val mult_less_cancel2 = thm "mult_less_cancel2";
   2.562 +val mult_less_cancel1 = thm "mult_less_cancel1";
   2.563 +val mult_le_cancel2 = thm "mult_le_cancel2";
   2.564 +val mult_le_cancel1 = thm "mult_le_cancel1";
   2.565 +val mult_le_cancel_le1 = thm "mult_le_cancel_le1";
   2.566 +val Ord_eq_iff_le = thm "Ord_eq_iff_le";
   2.567 +val mult_cancel2 = thm "mult_cancel2";
   2.568 +val mult_cancel1 = thm "mult_cancel1";
   2.569 +val div_cancel_raw = thm "div_cancel_raw";
   2.570 +val div_cancel = thm "div_cancel";
   2.571 +val mult_mod_distrib_raw = thm "mult_mod_distrib_raw";
   2.572 +val mod_mult_distrib2 = thm "mod_mult_distrib2";
   2.573 +val mult_mod_distrib = thm "mult_mod_distrib";
   2.574 +val mod_add_self2_raw = thm "mod_add_self2_raw";
   2.575 +val mod_add_self2 = thm "mod_add_self2";
   2.576 +val mod_add_self1 = thm "mod_add_self1";
   2.577 +val mod_mult_self1_raw = thm "mod_mult_self1_raw";
   2.578 +val mod_mult_self1 = thm "mod_mult_self1";
   2.579 +val mod_mult_self2 = thm "mod_mult_self2";
   2.580 +val mult_eq_self_implies_10 = thm "mult_eq_self_implies_10";
   2.581 +val less_imp_succ_add = thm "less_imp_succ_add";
   2.582 +val less_iff_succ_add = thm "less_iff_succ_add";
   2.583 +val diff_is_0_iff = thm "diff_is_0_iff";
   2.584 +val nat_lt_imp_diff_eq_0 = thm "nat_lt_imp_diff_eq_0";
   2.585 +val nat_diff_split = thm "nat_diff_split";
   2.586 +*}
   2.587 +
   2.588  end
     3.1 --- a/src/ZF/Inductive.thy	Fri Jun 28 20:01:09 2002 +0200
     3.2 +++ b/src/ZF/Inductive.thy	Sat Jun 29 21:33:06 2002 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  (Co)Inductive Definitions for Zermelo-Fraenkel Set Theory.
     3.5  *)
     3.6  
     3.7 -theory Inductive = Fixedpt + mono
     3.8 +theory Inductive = Fixedpt + mono + QPair
     3.9    files
    3.10      "ind_syntax.ML"
    3.11      "Tools/cartprod.ML"
     4.1 --- a/src/ZF/IsaMakefile	Fri Jun 28 20:01:09 2002 +0200
     4.2 +++ b/src/ZF/IsaMakefile	Sat Jun 29 21:33:06 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.thy ArithSimp.ML	\
     4.8 +$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy \
     4.9    ArithSimp.thy Bool.thy Cardinal.thy		\
    4.10    CardinalArith.thy Cardinal_AC.thy \
    4.11    Datatype.ML Datatype.thy Epsilon.thy Finite.thy	\
    4.12 @@ -45,8 +45,8 @@
    4.13    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
    4.14    Trancl.thy Univ.thy Update.thy \
    4.15    WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy	\
    4.16 -  ind_syntax.ML mono.ML mono.thy pair.thy simpdata.ML		\
    4.17 -  subset.ML subset.thy thy_syntax.ML upair.ML upair.thy
    4.18 +  ind_syntax.ML mono.thy pair.thy simpdata.ML		\
    4.19 +  thy_syntax.ML upair.thy
    4.20  	@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
    4.21  
    4.22  
     5.1 --- a/src/ZF/QPair.ML	Fri Jun 28 20:01:09 2002 +0200
     5.2 +++ b/src/ZF/QPair.ML	Sat Jun 29 21:33:06 2002 +0200
     5.3 @@ -328,3 +328,30 @@
     5.4  Goal "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
     5.5  by (Blast_tac 1);
     5.6  qed "Part_qsum_equality";
     5.7 +
     5.8 +
     5.9 +(*** Monotonicity ***)
    5.10 +
    5.11 +Goalw [QPair_def] "[| a<=c;  b<=d |] ==> <a;b> <= <c;d>";
    5.12 +by (REPEAT (ares_tac [sum_mono] 1));
    5.13 +qed "QPair_mono";
    5.14 +
    5.15 +Goal "[| A<=C;  ALL x:A. B(x) <= D(x) |] ==>  \
    5.16 +\                          QSigma(A,B) <= QSigma(C,D)";
    5.17 +by (Blast_tac 1);
    5.18 +qed "QSigma_mono_lemma";
    5.19 +bind_thm ("QSigma_mono", ballI RSN (2,QSigma_mono_lemma));
    5.20 +
    5.21 +Goalw [QInl_def] "a<=b ==> QInl(a) <= QInl(b)";
    5.22 +by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1));
    5.23 +qed "QInl_mono";
    5.24 +
    5.25 +Goalw [QInr_def] "a<=b ==> QInr(a) <= QInr(b)";
    5.26 +by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1));
    5.27 +qed "QInr_mono";
    5.28 +
    5.29 +Goal "[| A<=C;  B<=D |] ==> A <+> B <= C <+> D";
    5.30 +by (Blast_tac 1);
    5.31 +qed "qsum_mono";
    5.32 +
    5.33 +
     6.1 --- a/src/ZF/QPair.thy	Fri Jun 28 20:01:09 2002 +0200
     6.2 +++ b/src/ZF/QPair.thy	Sat Jun 29 21:33:06 2002 +0200
     6.3 @@ -11,7 +11,7 @@
     6.4  1966.
     6.5  *)
     6.6  
     6.7 -QPair = Sum +
     6.8 +QPair = Sum + mono +
     6.9  
    6.10  consts
    6.11    QPair     :: "[i, i] => i"                      ("<(_;/ _)>")
     7.1 --- a/src/ZF/arith_data.ML	Fri Jun 28 20:01:09 2002 +0200
     7.2 +++ b/src/ZF/arith_data.ML	Sat Jun 29 21:33:06 2002 +0200
     7.3 @@ -218,6 +218,10 @@
     7.4  
     7.5  end;
     7.6  
     7.7 +(*Install the simprocs!*)
     7.8 +Addsimprocs ArithData.nat_cancel;
     7.9 +
    7.10 +
    7.11  (*examples:
    7.12  print_depth 22;
    7.13  set timing;
     8.1 --- a/src/ZF/equalities.thy	Fri Jun 28 20:01:09 2002 +0200
     8.2 +++ b/src/ZF/equalities.thy	Sat Jun 29 21:33:06 2002 +0200
     8.3 @@ -3,13 +3,14 @@
     8.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.5      Copyright   1992  University of Cambridge
     8.6  
     8.7 -Converse, domain, range of a relation or function.
     8.8  
     8.9 -And set theory equalities involving Union, Intersection, Inclusion, etc.
    8.10 -    (Thanks also to Philippe de Groote.)
    8.11 +Basic equations (and inclusions) involving union, intersection, 
    8.12 +converse, domain, range, etc.
    8.13 +
    8.14 +Thanks also to Philippe de Groote.
    8.15  *)
    8.16  
    8.17 -theory equalities = pair + subset:
    8.18 +theory equalities = pair:
    8.19  
    8.20  (*FIXME: move to ZF.thy or even to FOL.thy??*)
    8.21  lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
    8.22 @@ -23,6 +24,33 @@
    8.23  lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
    8.24  by blast
    8.25  
    8.26 +(** Monotonicity of implications -- some could go to FOL **)
    8.27 +
    8.28 +lemma in_mono: "A<=B ==> x:A --> x:B"
    8.29 +by blast
    8.30 +
    8.31 +lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"
    8.32 +by fast (*or (IntPr.fast_tac 1)*)
    8.33 +
    8.34 +lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"
    8.35 +by fast (*or (IntPr.fast_tac 1)*)
    8.36 +
    8.37 +lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"
    8.38 +by fast (*or (IntPr.fast_tac 1)*)
    8.39 +
    8.40 +lemma imp_refl: "P-->P"
    8.41 +by (rule impI, assumption)
    8.42 +
    8.43 +(*The quantifier monotonicity rules are also intuitionistically valid*)
    8.44 +lemma ex_mono:
    8.45 +    "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))"
    8.46 +by blast
    8.47 +
    8.48 +lemma all_mono:
    8.49 +    "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))"
    8.50 +by blast
    8.51 +
    8.52 +
    8.53  lemma the_eq_0 [simp]: "(THE x. False) = 0"
    8.54  by (blast intro: the_0)
    8.55  
    8.56 @@ -77,143 +105,27 @@
    8.57  by blast
    8.58  
    8.59  
    8.60 -(*** domain ***)
    8.61 -
    8.62 -lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>: r)"
    8.63 -by (unfold domain_def, blast)
    8.64 +(** cons; Finite Sets **)
    8.65  
    8.66 -lemma domainI [intro]: "<a,b>: r ==> a: domain(r)"
    8.67 -by (unfold domain_def, blast)
    8.68 -
    8.69 -lemma domainE [elim!]:
    8.70 -    "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P"
    8.71 -by (unfold domain_def, blast)
    8.72 -
    8.73 -lemma domain_subset: "domain(Sigma(A,B)) <= A"
    8.74 +lemma cons_subsetI: "[| a:C; B<=C |] ==> cons(a,B) <= C"
    8.75  by blast
    8.76  
    8.77 -(*** range ***)
    8.78 -
    8.79 -lemma rangeI [intro]: "<a,b>: r ==> b : range(r)"
    8.80 -apply (unfold range_def)
    8.81 -apply (erule converseI [THEN domainI])
    8.82 -done
    8.83 -
    8.84 -lemma rangeE [elim!]: "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P"
    8.85 -by (unfold range_def, blast)
    8.86 -
    8.87 -lemma range_subset: "range(A*B) <= B"
    8.88 -apply (unfold range_def)
    8.89 -apply (subst converse_prod)
    8.90 -apply (rule domain_subset)
    8.91 -done
    8.92 -
    8.93 -
    8.94 -(*** field ***)
    8.95 -
    8.96 -lemma fieldI1: "<a,b>: r ==> a : field(r)"
    8.97 -by (unfold field_def, blast)
    8.98 -
    8.99 -lemma fieldI2: "<a,b>: r ==> b : field(r)"
   8.100 -by (unfold field_def, blast)
   8.101 -
   8.102 -lemma fieldCI [intro]: 
   8.103 -    "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
   8.104 -apply (unfold field_def, blast)
   8.105 -done
   8.106 -
   8.107 -lemma fieldE [elim!]: 
   8.108 -     "[| a : field(r);   
   8.109 -         !!x. <a,x>: r ==> P;   
   8.110 -         !!x. <x,a>: r ==> P        |] ==> P"
   8.111 -by (unfold field_def, blast)
   8.112 -
   8.113 -lemma field_subset: "field(A*B) <= A Un B"
   8.114 -by blast
   8.115 -
   8.116 -lemma domain_subset_field: "domain(r) <= field(r)"
   8.117 -apply (unfold field_def)
   8.118 -apply (rule Un_upper1)
   8.119 -done
   8.120 -
   8.121 -lemma range_subset_field: "range(r) <= field(r)"
   8.122 -apply (unfold field_def)
   8.123 -apply (rule Un_upper2)
   8.124 -done
   8.125 -
   8.126 -lemma domain_times_range: "r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
   8.127 +lemma subset_consI: "B <= cons(a,B)"
   8.128  by blast
   8.129  
   8.130 -lemma field_times_field: "r <= Sigma(A,B) ==> r <= field(r)*field(r)"
   8.131 -by blast
   8.132 -
   8.133 -lemma relation_field_times_field: "relation(r) ==> r <= field(r)*field(r)"
   8.134 -by (simp add: relation_def, blast) 
   8.135 -
   8.136 -
   8.137 -(*** Image of a set under a function/relation ***)
   8.138 -
   8.139 -lemma image_iff: "b : r``A <-> (EX x:A. <x,b>:r)"
   8.140 -by (unfold image_def, blast)
   8.141 -
   8.142 -lemma image_singleton_iff: "b : r``{a} <-> <a,b>:r"
   8.143 -by (rule image_iff [THEN iff_trans], blast)
   8.144 -
   8.145 -lemma imageI [intro]: "[| <a,b>: r;  a:A |] ==> b : r``A"
   8.146 -by (unfold image_def, blast)
   8.147 -
   8.148 -lemma imageE [elim!]: 
   8.149 -    "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
   8.150 -apply (unfold image_def, blast)
   8.151 -done
   8.152 -
   8.153 -lemma image_subset: "r <= A*B ==> r``C <= B"
   8.154 +lemma cons_subset_iff [iff]: "cons(a,B)<=C <-> a:C & B<=C"
   8.155  by blast
   8.156  
   8.157 -
   8.158 -(*** Inverse image of a set under a function/relation ***)
   8.159 -
   8.160 -lemma vimage_iff: 
   8.161 -    "a : r-``B <-> (EX y:B. <a,y>:r)"
   8.162 -apply (unfold vimage_def image_def converse_def, blast)
   8.163 -done
   8.164 -
   8.165 -lemma vimage_singleton_iff: "a : r-``{b} <-> <a,b>:r"
   8.166 -by (rule vimage_iff [THEN iff_trans], blast)
   8.167 -
   8.168 -lemma vimageI [intro]: "[| <a,b>: r;  b:B |] ==> a : r-``B"
   8.169 -by (unfold vimage_def, blast)
   8.170 +(*A safe special case of subset elimination, adding no new variables 
   8.171 +  [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
   8.172 +lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE, standard]
   8.173  
   8.174 -lemma vimageE [elim!]: 
   8.175 -    "[| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P"
   8.176 -apply (unfold vimage_def, blast)
   8.177 -done
   8.178 -
   8.179 -lemma vimage_subset: "r <= A*B ==> r-``C <= A"
   8.180 -apply (unfold vimage_def)
   8.181 -apply (erule converse_type [THEN image_subset])
   8.182 -done
   8.183 -
   8.184 -
   8.185 -(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
   8.186 -lemma rel_Union: "(ALL x:S. EX A B. x <= A*B) ==>   
   8.187 -                  Union(S) <= domain(Union(S)) * range(Union(S))"
   8.188 +lemma subset_empty_iff: "A<=0 <-> A=0"
   8.189  by blast
   8.190  
   8.191 -(** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
   8.192 -lemma rel_Un: "[| r <= A*B;  s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
   8.193 -by blast
   8.194 -
   8.195 -lemma domain_Diff_eq: "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"
   8.196 +lemma subset_cons_iff: "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
   8.197  by blast
   8.198  
   8.199 -lemma range_Diff_eq: "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)"
   8.200 -by blast
   8.201 -
   8.202 -
   8.203 -
   8.204 -(** Finite Sets **)
   8.205 -
   8.206  (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
   8.207  lemma cons_eq: "{a} Un B = cons(a,B)"
   8.208  by blast
   8.209 @@ -233,9 +145,50 @@
   8.210  lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
   8.211  by blast
   8.212  
   8.213 -(** Binary Intersection **)
   8.214 +(** singletons **)
   8.215 +
   8.216 +lemma singleton_subsetI: "a:C ==> {a} <= C"
   8.217 +by blast
   8.218 +
   8.219 +lemma singleton_subsetD: "{a} <= C  ==>  a:C"
   8.220 +by blast
   8.221 +
   8.222 +
   8.223 +(*** succ ***)
   8.224 +
   8.225 +lemma subset_succI: "i <= succ(i)"
   8.226 +by blast
   8.227 +
   8.228 +(*But if j is an ordinal or is transitive, then i:j implies i<=j! 
   8.229 +  See ordinal/Ord_succ_subsetI*)
   8.230 +lemma succ_subsetI: "[| i:j;  i<=j |] ==> succ(i)<=j"
   8.231 +by (unfold succ_def, blast)
   8.232  
   8.233 -(*NOT an equality, but it seems to belong here...*)
   8.234 +lemma succ_subsetE:
   8.235 +    "[| succ(i) <= j;  [| i:j;  i<=j |] ==> P |] ==> P"
   8.236 +apply (unfold succ_def, blast) 
   8.237 +done
   8.238 +
   8.239 +lemma succ_subset_iff: "succ(a) <= B <-> (a <= B & a : B)"
   8.240 +by (unfold succ_def, blast)
   8.241 +
   8.242 +
   8.243 +(*** Binary Intersection ***)
   8.244 +
   8.245 +(** Intersection is the greatest lower bound of two sets **)
   8.246 +
   8.247 +lemma Int_subset_iff: "C <= A Int B <-> C <= A & C <= B"
   8.248 +by blast
   8.249 +
   8.250 +lemma Int_lower1: "A Int B <= A"
   8.251 +by blast
   8.252 +
   8.253 +lemma Int_lower2: "A Int B <= B"
   8.254 +by blast
   8.255 +
   8.256 +lemma Int_greatest: "[| C<=A;  C<=B |] ==> C <= A Int B"
   8.257 +by blast
   8.258 +
   8.259  lemma Int_cons: "cons(a,B) Int C <= cons(a, B Int C)"
   8.260  by blast
   8.261  
   8.262 @@ -272,7 +225,21 @@
   8.263  lemma Int_Diff_eq: "C<=A ==> (A-B) Int C = C-B"
   8.264  by blast
   8.265  
   8.266 -(** Binary Union **)
   8.267 +(*** Binary Union ***)
   8.268 +
   8.269 +(** Union is the least upper bound of two sets *)
   8.270 +
   8.271 +lemma Un_subset_iff: "A Un B <= C <-> A <= C & B <= C"
   8.272 +by blast
   8.273 +
   8.274 +lemma Un_upper1: "A <= A Un B"
   8.275 +by blast
   8.276 +
   8.277 +lemma Un_upper2: "B <= A Un B"
   8.278 +by blast
   8.279 +
   8.280 +lemma Un_least: "[| A<=C;  B<=C |] ==> A Un B <= C"
   8.281 +by blast
   8.282  
   8.283  lemma Un_cons: "cons(a,B) Un C = cons(a, B Un C)"
   8.284  by blast
   8.285 @@ -310,7 +277,16 @@
   8.286  lemma Un_eq_Union: "A Un B = Union({A, B})"
   8.287  by blast
   8.288  
   8.289 -(** Simple properties of Diff -- set difference **)
   8.290 +(*** Set difference ***)
   8.291 +
   8.292 +lemma Diff_subset: "A-B <= A"
   8.293 +by blast
   8.294 +
   8.295 +lemma Diff_contains: "[| C<=A;  C Int B = 0 |] ==> C <= A-B"
   8.296 +by blast
   8.297 +
   8.298 +lemma subset_Diff_cons_iff: "B <= A - cons(c,C)  <->  B<=A-C & c ~: B"
   8.299 +by blast
   8.300  
   8.301  lemma Diff_cancel: "A - A = 0"
   8.302  by blast
   8.303 @@ -378,7 +354,18 @@
   8.304  by (blast elim!: equalityE)
   8.305  
   8.306  
   8.307 -(** Big Union and Intersection **)
   8.308 +(*** Big Union and Intersection ***)
   8.309 +
   8.310 +(** Big Union is the least upper bound of a set  **)
   8.311 +
   8.312 +lemma Union_subset_iff: "Union(A) <= C <-> (ALL x:A. x <= C)"
   8.313 +by blast
   8.314 +
   8.315 +lemma Union_upper: "B:A ==> B <= Union(A)"
   8.316 +by blast
   8.317 +
   8.318 +lemma Union_least: "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C"
   8.319 +by blast
   8.320  
   8.321  lemma Union_cons [simp]: "Union(cons(a,B)) = a Un Union(B)"
   8.322  by blast
   8.323 @@ -395,10 +382,31 @@
   8.324  lemma Union_empty_iff: "Union(A) = 0 <-> (ALL B:A. B=0)"
   8.325  by blast
   8.326  
   8.327 +(** Big Intersection is the greatest lower bound of a nonempty set **)
   8.328 +
   8.329 +lemma Inter_subset_iff: "a: A  ==>  C <= Inter(A) <-> (ALL x:A. C <= x)"
   8.330 +by blast
   8.331 +
   8.332 +lemma Inter_lower: "B:A ==> Inter(A) <= B"
   8.333 +by blast
   8.334 +
   8.335 +lemma Inter_greatest: "[| a:A;  !!x. x:A ==> C<=x |] ==> C <= Inter(A)"
   8.336 +by blast
   8.337 +
   8.338 +(** Intersection of a family of sets  **)
   8.339 +
   8.340 +lemma INT_lower: "x:A ==> (INT x:A. B(x)) <= B(x)"
   8.341 +by blast
   8.342 +
   8.343 +lemma INT_greatest: 
   8.344 +    "[| a:A;  !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"
   8.345 +by blast 
   8.346 +
   8.347  lemma Inter_0: "Inter(0) = 0"
   8.348  by (unfold Inter_def, blast)
   8.349  
   8.350 -lemma Inter_Un_subset: "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)"
   8.351 +lemma Inter_Un_subset:
   8.352 +     "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)"
   8.353  by blast
   8.354  
   8.355  (* A good challenge: Inter is ill-behaved on the empty set *)
   8.356 @@ -416,7 +424,19 @@
   8.357       "Inter(cons(a,B)) = (if B=0 then a else a Int Inter(B))"
   8.358  by force
   8.359  
   8.360 -(** Unions and Intersections of Families **)
   8.361 +(*** Unions and Intersections of Families ***)
   8.362 +
   8.363 +lemma subset_UN_iff_eq: "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))"
   8.364 +by (blast elim!: equalityE)
   8.365 +
   8.366 +lemma UN_subset_iff: "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"
   8.367 +by blast
   8.368 +
   8.369 +lemma UN_upper: "x:A ==> B(x) <= (UN x:A. B(x))"
   8.370 +by (erule RepFunI [THEN Union_upper])
   8.371 +
   8.372 +lemma UN_least: "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"
   8.373 +by blast
   8.374  
   8.375  lemma Union_eq_UN: "Union(A) = (UN x:A. x)"
   8.376  by blast
   8.377 @@ -436,7 +456,7 @@
   8.378  lemma INT_Un: "(INT i:I Un J. A(i)) = (if I=0 then INT j:J. A(j)  
   8.379                                else if J=0 then INT i:I. A(i)  
   8.380                                else ((INT i:I. A(i)) Int  (INT j:J. A(j))))"
   8.381 -apply auto
   8.382 +apply simp
   8.383  apply (blast intro!: equalityI)
   8.384  done
   8.385  
   8.386 @@ -562,6 +582,19 @@
   8.387  
   8.388  (** Domain **)
   8.389  
   8.390 +lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>: r)"
   8.391 +by (unfold domain_def, blast)
   8.392 +
   8.393 +lemma domainI [intro]: "<a,b>: r ==> a: domain(r)"
   8.394 +by (unfold domain_def, blast)
   8.395 +
   8.396 +lemma domainE [elim!]:
   8.397 +    "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P"
   8.398 +by (unfold domain_def, blast)
   8.399 +
   8.400 +lemma domain_subset: "domain(Sigma(A,B)) <= A"
   8.401 +by blast
   8.402 +
   8.403  lemma domain_of_prod: "b:B ==> domain(A*B) = A"
   8.404  by blast
   8.405  
   8.406 @@ -580,9 +613,6 @@
   8.407  lemma domain_Diff_subset: "domain(A) - domain(B) <= domain(A - B)"
   8.408  by blast
   8.409  
   8.410 -lemma domain_converse [simp]: "domain(converse(r)) = range(r)"
   8.411 -by blast
   8.412 -
   8.413  lemma domain_UN: "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))"
   8.414  by blast
   8.415  
   8.416 @@ -592,6 +622,20 @@
   8.417  
   8.418  (** Range **)
   8.419  
   8.420 +lemma rangeI [intro]: "<a,b>: r ==> b : range(r)"
   8.421 +apply (unfold range_def)
   8.422 +apply (erule converseI [THEN domainI])
   8.423 +done
   8.424 +
   8.425 +lemma rangeE [elim!]: "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P"
   8.426 +by (unfold range_def, blast)
   8.427 +
   8.428 +lemma range_subset: "range(A*B) <= B"
   8.429 +apply (unfold range_def)
   8.430 +apply (subst converse_prod)
   8.431 +apply (rule domain_subset)
   8.432 +done
   8.433 +
   8.434  lemma range_of_prod: "a:A ==> range(A*B) = B"
   8.435  by blast
   8.436  
   8.437 @@ -610,12 +654,54 @@
   8.438  lemma range_Diff_subset: "range(A) - range(B) <= range(A - B)"
   8.439  by blast
   8.440  
   8.441 +lemma domain_converse [simp]: "domain(converse(r)) = range(r)"
   8.442 +by blast
   8.443 +
   8.444  lemma range_converse [simp]: "range(converse(r)) = domain(r)"
   8.445  by blast
   8.446  
   8.447  
   8.448  (** Field **)
   8.449  
   8.450 +lemma fieldI1: "<a,b>: r ==> a : field(r)"
   8.451 +by (unfold field_def, blast)
   8.452 +
   8.453 +lemma fieldI2: "<a,b>: r ==> b : field(r)"
   8.454 +by (unfold field_def, blast)
   8.455 +
   8.456 +lemma fieldCI [intro]: 
   8.457 +    "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
   8.458 +apply (unfold field_def, blast)
   8.459 +done
   8.460 +
   8.461 +lemma fieldE [elim!]: 
   8.462 +     "[| a : field(r);   
   8.463 +         !!x. <a,x>: r ==> P;   
   8.464 +         !!x. <x,a>: r ==> P        |] ==> P"
   8.465 +by (unfold field_def, blast)
   8.466 +
   8.467 +lemma field_subset: "field(A*B) <= A Un B"
   8.468 +by blast
   8.469 +
   8.470 +lemma domain_subset_field: "domain(r) <= field(r)"
   8.471 +apply (unfold field_def)
   8.472 +apply (rule Un_upper1)
   8.473 +done
   8.474 +
   8.475 +lemma range_subset_field: "range(r) <= field(r)"
   8.476 +apply (unfold field_def)
   8.477 +apply (rule Un_upper2)
   8.478 +done
   8.479 +
   8.480 +lemma domain_times_range: "r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
   8.481 +by blast
   8.482 +
   8.483 +lemma field_times_field: "r <= Sigma(A,B) ==> r <= field(r)*field(r)"
   8.484 +by blast
   8.485 +
   8.486 +lemma relation_field_times_field: "relation(r) ==> r <= field(r)*field(r)"
   8.487 +by (simp add: relation_def, blast) 
   8.488 +
   8.489  lemma field_of_prod: "field(A*A) = A"
   8.490  by blast
   8.491  
   8.492 @@ -637,8 +723,39 @@
   8.493  lemma field_converse [simp]: "field(converse(r)) = field(r)"
   8.494  by blast
   8.495  
   8.496 +(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
   8.497 +lemma rel_Union: "(ALL x:S. EX A B. x <= A*B) ==>   
   8.498 +                  Union(S) <= domain(Union(S)) * range(Union(S))"
   8.499 +by blast
   8.500  
   8.501 -(** Image **)
   8.502 +(** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
   8.503 +lemma rel_Un: "[| r <= A*B;  s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
   8.504 +by blast
   8.505 +
   8.506 +lemma domain_Diff_eq: "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"
   8.507 +by blast
   8.508 +
   8.509 +lemma range_Diff_eq: "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)"
   8.510 +by blast
   8.511 +
   8.512 +
   8.513 +(*** Image of a set under a function/relation ***)
   8.514 +
   8.515 +lemma image_iff: "b : r``A <-> (EX x:A. <x,b>:r)"
   8.516 +by (unfold image_def, blast)
   8.517 +
   8.518 +lemma image_singleton_iff: "b : r``{a} <-> <a,b>:r"
   8.519 +by (rule image_iff [THEN iff_trans], blast)
   8.520 +
   8.521 +lemma imageI [intro]: "[| <a,b>: r;  a:A |] ==> b : r``A"
   8.522 +by (unfold image_def, blast)
   8.523 +
   8.524 +lemma imageE [elim!]: 
   8.525 +    "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
   8.526 +by (unfold image_def, blast)
   8.527 +
   8.528 +lemma image_subset: "r <= A*B ==> r``C <= B"
   8.529 +by blast
   8.530  
   8.531  lemma image_0 [simp]: "r``0 = 0"
   8.532  by blast
   8.533 @@ -667,7 +784,27 @@
   8.534  by blast
   8.535  
   8.536  
   8.537 -(** Inverse Image **)
   8.538 +(*** Inverse image of a set under a function/relation ***)
   8.539 +
   8.540 +lemma vimage_iff: 
   8.541 +    "a : r-``B <-> (EX y:B. <a,y>:r)"
   8.542 +by (unfold vimage_def image_def converse_def, blast)
   8.543 +
   8.544 +lemma vimage_singleton_iff: "a : r-``{b} <-> <a,b>:r"
   8.545 +by (rule vimage_iff [THEN iff_trans], blast)
   8.546 +
   8.547 +lemma vimageI [intro]: "[| <a,b>: r;  b:B |] ==> a : r-``B"
   8.548 +by (unfold vimage_def, blast)
   8.549 +
   8.550 +lemma vimageE [elim!]: 
   8.551 +    "[| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P"
   8.552 +apply (unfold vimage_def, blast)
   8.553 +done
   8.554 +
   8.555 +lemma vimage_subset: "r <= A*B ==> r-``C <= A"
   8.556 +apply (unfold vimage_def)
   8.557 +apply (erule converse_type [THEN image_subset])
   8.558 +done
   8.559  
   8.560  lemma vimage_0 [simp]: "r-``0 = 0"
   8.561  by blast
   8.562 @@ -760,7 +897,10 @@
   8.563  lemma Pow_INT_eq: "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))"
   8.564  by blast
   8.565  
   8.566 -(** RepFun **)
   8.567 +(*** RepFun ***)
   8.568 +
   8.569 +lemma RepFun_subset: "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B"
   8.570 +by blast
   8.571  
   8.572  lemma RepFun_eq_0_iff [simp]: "{f(x).x:A}=0 <-> A=0"
   8.573  by blast
   8.574 @@ -770,7 +910,10 @@
   8.575  apply blast
   8.576  done
   8.577  
   8.578 -(** Collect **)
   8.579 +(*** Collect ***)
   8.580 +
   8.581 +lemma Collect_subset: "Collect(A,P) <= A"
   8.582 +by blast
   8.583  
   8.584  lemma Collect_Un: "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)"
   8.585  by blast
   8.586 @@ -800,10 +943,74 @@
   8.587       "Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
   8.588  by blast
   8.589  
   8.590 +lemmas subset_SIs = subset_refl cons_subsetI subset_consI 
   8.591 +                    Union_least UN_least Un_least 
   8.592 +                    Inter_greatest Int_greatest RepFun_subset
   8.593 +                    Un_upper1 Un_upper2 Int_lower1 Int_lower2
   8.594 +
   8.595 +(*First, ML bindings from the old file subset.ML*)
   8.596 +ML
   8.597 +{*
   8.598 +val cons_subsetI = thm "cons_subsetI";
   8.599 +val subset_consI = thm "subset_consI";
   8.600 +val cons_subset_iff = thm "cons_subset_iff";
   8.601 +val cons_subsetE = thm "cons_subsetE";
   8.602 +val subset_empty_iff = thm "subset_empty_iff";
   8.603 +val subset_cons_iff = thm "subset_cons_iff";
   8.604 +val subset_succI = thm "subset_succI";
   8.605 +val succ_subsetI = thm "succ_subsetI";
   8.606 +val succ_subsetE = thm "succ_subsetE";
   8.607 +val succ_subset_iff = thm "succ_subset_iff";
   8.608 +val singleton_subsetI = thm "singleton_subsetI";
   8.609 +val singleton_subsetD = thm "singleton_subsetD";
   8.610 +val Union_subset_iff = thm "Union_subset_iff";
   8.611 +val Union_upper = thm "Union_upper";
   8.612 +val Union_least = thm "Union_least";
   8.613 +val subset_UN_iff_eq = thm "subset_UN_iff_eq";
   8.614 +val UN_subset_iff = thm "UN_subset_iff";
   8.615 +val UN_upper = thm "UN_upper";
   8.616 +val UN_least = thm "UN_least";
   8.617 +val Inter_subset_iff = thm "Inter_subset_iff";
   8.618 +val Inter_lower = thm "Inter_lower";
   8.619 +val Inter_greatest = thm "Inter_greatest";
   8.620 +val INT_lower = thm "INT_lower";
   8.621 +val INT_greatest = thm "INT_greatest";
   8.622 +val Un_subset_iff = thm "Un_subset_iff";
   8.623 +val Un_upper1 = thm "Un_upper1";
   8.624 +val Un_upper2 = thm "Un_upper2";
   8.625 +val Un_least = thm "Un_least";
   8.626 +val Int_subset_iff = thm "Int_subset_iff";
   8.627 +val Int_lower1 = thm "Int_lower1";
   8.628 +val Int_lower2 = thm "Int_lower2";
   8.629 +val Int_greatest = thm "Int_greatest";
   8.630 +val Diff_subset = thm "Diff_subset";
   8.631 +val Diff_contains = thm "Diff_contains";
   8.632 +val subset_Diff_cons_iff = thm "subset_Diff_cons_iff";
   8.633 +val Collect_subset = thm "Collect_subset";
   8.634 +val RepFun_subset = thm "RepFun_subset";
   8.635 +
   8.636 +val subset_SIs = thms "subset_SIs";
   8.637 +
   8.638 +val subset_cs = claset() 
   8.639 +    delrules [subsetI, subsetCE]
   8.640 +    addSIs subset_SIs
   8.641 +    addIs  [Union_upper, Inter_lower]
   8.642 +    addSEs [cons_subsetE];
   8.643 +*}
   8.644 +(*subset_cs is a claset for subset reasoning*)
   8.645 +
   8.646  ML
   8.647  {*
   8.648  val ZF_cs = claset() delrules [equalityI];
   8.649  
   8.650 +val in_mono = thm "in_mono";
   8.651 +val conj_mono = thm "conj_mono";
   8.652 +val disj_mono = thm "disj_mono";
   8.653 +val imp_mono = thm "imp_mono";
   8.654 +val imp_refl = thm "imp_refl";
   8.655 +val ex_mono = thm "ex_mono";
   8.656 +val all_mono = thm "all_mono";
   8.657 +
   8.658  val converse_iff = thm "converse_iff";
   8.659  val converseI = thm "converseI";
   8.660  val converseD = thm "converseD";
     9.1 --- a/src/ZF/ex/Primes.thy	Fri Jun 28 20:01:09 2002 +0200
     9.2 +++ b/src/ZF/ex/Primes.thy	Sat Jun 29 21:33:06 2002 +0200
     9.3 @@ -137,14 +137,15 @@
     9.4  
     9.5  lemma dvd_mod_imp_dvd_raw:
     9.6       "[| a \<in> nat; b \<in> nat; k dvd b; k dvd (a mod b) |] ==> k dvd a"
     9.7 -apply (tactic "div_undefined_case_tac \"b=0\" 1")
     9.8 +apply (case_tac "b=0")
     9.9 + apply (simp add: DIVISION_BY_ZERO_MOD)
    9.10  apply (blast intro: mod_div_equality [THEN subst]
    9.11               elim: dvdE 
    9.12               intro!: dvd_add dvd_mult mult_type mod_type div_type)
    9.13  done
    9.14  
    9.15  lemma dvd_mod_imp_dvd: "[| k dvd (a mod b); k dvd b; a \<in> nat |] ==> k dvd a"
    9.16 -apply (cut_tac b = "natify (b) " in dvd_mod_imp_dvd_raw)
    9.17 +apply (cut_tac b = "natify (b)" in dvd_mod_imp_dvd_raw)
    9.18  apply auto
    9.19  apply (simp add: divides_def)
    9.20  done
    9.21 @@ -176,7 +177,7 @@
    9.22  lemma gcd_type [simp,TC]: "gcd(m, n) \<in> nat"
    9.23  apply (subgoal_tac "gcd (natify (m) , natify (n)) \<in> nat")
    9.24  apply simp
    9.25 -apply (rule_tac m = "natify (m) " and n = "natify (n) " in gcd_induct)
    9.26 +apply (rule_tac m = "natify (m)" and n = "natify (n)" in gcd_induct)
    9.27  apply auto
    9.28  apply (simp add: gcd_non_0)
    9.29  done
    9.30 @@ -192,12 +193,12 @@
    9.31  done
    9.32  
    9.33  lemma gcd_dvd1 [simp]: "m \<in> nat ==> gcd(m,n) dvd m"
    9.34 -apply (cut_tac m = "natify (m) " and n = "natify (n) " in gcd_dvd_both)
    9.35 +apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both)
    9.36  apply auto
    9.37  done
    9.38  
    9.39  lemma gcd_dvd2 [simp]: "n \<in> nat ==> gcd(m,n) dvd n"
    9.40 -apply (cut_tac m = "natify (m) " and n = "natify (n) " in gcd_dvd_both)
    9.41 +apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both)
    9.42  apply auto
    9.43  done
    9.44  
    9.45 @@ -205,7 +206,8 @@
    9.46  
    9.47  lemma dvd_mod: "[| f dvd a; f dvd b |] ==> f dvd (a mod b)"
    9.48  apply (unfold divides_def)
    9.49 -apply (tactic "div_undefined_case_tac \"b=0\" 1")
    9.50 +apply (case_tac "b=0")
    9.51 + apply (simp add: DIVISION_BY_ZERO_MOD)
    9.52  apply auto
    9.53  apply (blast intro: mod_mult_distrib2 [symmetric])
    9.54  done
    9.55 @@ -254,7 +256,7 @@
    9.56  done
    9.57  
    9.58  lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
    9.59 -apply (cut_tac m = "natify (m) " and n = "natify (n) " in gcd_commute_raw)
    9.60 +apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_commute_raw)
    9.61  apply auto
    9.62  done
    9.63  
    9.64 @@ -267,7 +269,7 @@
    9.65  done
    9.66  
    9.67  lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
    9.68 -apply (cut_tac k = "natify (k) " and m = "natify (m) " and n = "natify (n) " 
    9.69 +apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) " 
    9.70         in gcd_assoc_raw)
    9.71  apply auto
    9.72  done
    9.73 @@ -293,7 +295,7 @@
    9.74  done
    9.75  
    9.76  lemma gcd_mult_distrib2: "k #* gcd (m, n) = gcd (k #* m, k #* n)"
    9.77 -apply (cut_tac k = "natify (k) " and m = "natify (m) " and n = "natify (n) " 
    9.78 +apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) " 
    9.79         in gcd_mult_distrib2_raw)
    9.80  apply auto
    9.81  done
    9.82 @@ -324,7 +326,7 @@
    9.83       "[| p \<in> prime;  ~ (p dvd n);  n \<in> nat |] ==> gcd (p, n) = 1"
    9.84  apply (unfold prime_def)
    9.85  apply clarify
    9.86 -apply (drule_tac x = "gcd (p,n) " in bspec)
    9.87 +apply (drule_tac x = "gcd (p,n)" in bspec)
    9.88  apply auto
    9.89  apply (cut_tac m = "p" and n = "n" in gcd_dvd2)
    9.90  apply auto
    9.91 @@ -371,7 +373,7 @@
    9.92  done
    9.93  
    9.94  lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)"
    9.95 -apply (cut_tac k = "natify (k) " in gcd_add_mult_raw)
    9.96 +apply (cut_tac k = "natify (k)" in gcd_add_mult_raw)
    9.97  apply auto
    9.98  done
    9.99  
   9.100 @@ -390,7 +392,7 @@
   9.101  done
   9.102  
   9.103  lemma gcd_mult_cancel: "gcd (k,n) = 1 ==> gcd (k #* m, n) = gcd (m, n)"
   9.104 -apply (cut_tac m = "natify (m) " and n = "natify (n) " in gcd_mult_cancel_raw)
   9.105 +apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_mult_cancel_raw)
   9.106  apply auto
   9.107  done
   9.108  
    10.1 --- a/src/ZF/mono.ML	Fri Jun 28 20:01:09 2002 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,191 +0,0 @@
    10.4 -(*  Title:      ZF/mono
    10.5 -    ID:         $Id$
    10.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7 -    Copyright   1993  University of Cambridge
    10.8 -
    10.9 -Monotonicity of various operations (for lattice properties see subset.ML)
   10.10 -*)
   10.11 -
   10.12 -(** Replacement, in its various formulations **)
   10.13 -
   10.14 -(*Not easy to express monotonicity in P, since any "bigger" predicate
   10.15 -  would have to be single-valued*)
   10.16 -Goal "A<=B ==> Replace(A,P) <= Replace(B,P)";
   10.17 -by (blast_tac (claset() addSEs [ReplaceE]) 1);
   10.18 -qed "Replace_mono";
   10.19 -
   10.20 -Goal "A<=B ==> {f(x). x:A} <= {f(x). x:B}";
   10.21 -by (Blast_tac 1);
   10.22 -qed "RepFun_mono";
   10.23 -
   10.24 -Goal "A<=B ==> Pow(A) <= Pow(B)";
   10.25 -by (Blast_tac 1);
   10.26 -qed "Pow_mono";
   10.27 -
   10.28 -Goal "A<=B ==> Union(A) <= Union(B)";
   10.29 -by (Blast_tac 1);
   10.30 -qed "Union_mono";
   10.31 -
   10.32 -val prems = Goal
   10.33 -    "[| A<=C;  !!x. x:A ==> B(x)<=D(x) \
   10.34 -\    |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))";
   10.35 -by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
   10.36 -qed "UN_mono";
   10.37 -
   10.38 -(*Intersection is ANTI-monotonic.  There are TWO premises! *)
   10.39 -Goal "[| A<=B;  a:A |] ==> Inter(B) <= Inter(A)";
   10.40 -by (Blast_tac 1);
   10.41 -qed "Inter_anti_mono";
   10.42 -
   10.43 -Goal "C<=D ==> cons(a,C) <= cons(a,D)";
   10.44 -by (Blast_tac 1);
   10.45 -qed "cons_mono";
   10.46 -
   10.47 -Goal "[| A<=C;  B<=D |] ==> A Un B <= C Un D";
   10.48 -by (Blast_tac 1);
   10.49 -qed "Un_mono";
   10.50 -
   10.51 -Goal "[| A<=C;  B<=D |] ==> A Int B <= C Int D";
   10.52 -by (Blast_tac 1);
   10.53 -qed "Int_mono";
   10.54 -
   10.55 -Goal "[| A<=C;  D<=B |] ==> A-B <= C-D";
   10.56 -by (Blast_tac 1);
   10.57 -qed "Diff_mono";
   10.58 -
   10.59 -(** Standard products, sums and function spaces **)
   10.60 -
   10.61 -Goal "[| A<=C;  ALL x:A. B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)";
   10.62 -by (Blast_tac 1);
   10.63 -qed "Sigma_mono_lemma";
   10.64 -bind_thm ("Sigma_mono", ballI RSN (2,Sigma_mono_lemma));
   10.65 -
   10.66 -Goalw sum_defs "[| A<=C;  B<=D |] ==> A+B <= C+D";
   10.67 -by (REPEAT (ares_tac [subset_refl,Un_mono,Sigma_mono] 1));
   10.68 -qed "sum_mono";
   10.69 -
   10.70 -(*Note that B->A and C->A are typically disjoint!*)
   10.71 -Goal "B<=C ==> A->B <= A->C";
   10.72 -by (blast_tac (claset() addIs [lam_type] addEs [Pi_lamE]) 1);
   10.73 -qed "Pi_mono";
   10.74 -
   10.75 -Goalw [lam_def] "A<=B ==> Lambda(A,c) <= Lambda(B,c)";
   10.76 -by (etac RepFun_mono 1);
   10.77 -qed "lam_mono";
   10.78 -
   10.79 -(** Quine-inspired ordered pairs, products, injections and sums **)
   10.80 -
   10.81 -Goalw [QPair_def] "[| a<=c;  b<=d |] ==> <a;b> <= <c;d>";
   10.82 -by (REPEAT (ares_tac [sum_mono] 1));
   10.83 -qed "QPair_mono";
   10.84 -
   10.85 -Goal "[| A<=C;  ALL x:A. B(x) <= D(x) |] ==>  \
   10.86 -\                          QSigma(A,B) <= QSigma(C,D)";
   10.87 -by (Blast_tac 1);
   10.88 -qed "QSigma_mono_lemma";
   10.89 -bind_thm ("QSigma_mono", ballI RSN (2,QSigma_mono_lemma));
   10.90 -
   10.91 -Goalw [QInl_def] "a<=b ==> QInl(a) <= QInl(b)";
   10.92 -by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1));
   10.93 -qed "QInl_mono";
   10.94 -
   10.95 -Goalw [QInr_def] "a<=b ==> QInr(a) <= QInr(b)";
   10.96 -by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1));
   10.97 -qed "QInr_mono";
   10.98 -
   10.99 -Goal "[| A<=C;  B<=D |] ==> A <+> B <= C <+> D";
  10.100 -by (Blast_tac 1);
  10.101 -qed "qsum_mono";
  10.102 -
  10.103 -
  10.104 -(** Converse, domain, range, field **)
  10.105 -
  10.106 -Goal "r<=s ==> converse(r) <= converse(s)";
  10.107 -by (Blast_tac 1);
  10.108 -qed "converse_mono";
  10.109 -
  10.110 -Goal "r<=s ==> domain(r)<=domain(s)";
  10.111 -by (Blast_tac 1);
  10.112 -qed "domain_mono";
  10.113 -
  10.114 -bind_thm ("domain_rel_subset", [domain_mono, domain_subset] MRS subset_trans);
  10.115 -
  10.116 -Goal "r<=s ==> range(r)<=range(s)";
  10.117 -by (Blast_tac 1);
  10.118 -qed "range_mono";
  10.119 -
  10.120 -bind_thm ("range_rel_subset", [range_mono, range_subset] MRS subset_trans);
  10.121 -
  10.122 -Goal "r<=s ==> field(r)<=field(s)";
  10.123 -by (Blast_tac 1);
  10.124 -qed "field_mono";
  10.125 -
  10.126 -Goal "r <= A*A ==> field(r) <= A";
  10.127 -by (etac (field_mono RS subset_trans) 1);
  10.128 -by (Blast_tac 1);
  10.129 -qed "field_rel_subset";
  10.130 -
  10.131 -
  10.132 -(** Images **)
  10.133 -
  10.134 -val [prem1,prem2] = Goal
  10.135 -    "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r``A <= s``B";
  10.136 -by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1);
  10.137 -qed "image_pair_mono";
  10.138 -
  10.139 -val [prem1,prem2] = Goal
  10.140 -    "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r-``A <= s-``B";
  10.141 -by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1);
  10.142 -qed "vimage_pair_mono";
  10.143 -
  10.144 -Goal "[| r<=s;  A<=B |] ==> r``A <= s``B";
  10.145 -by (Blast_tac 1);
  10.146 -qed "image_mono";
  10.147 -
  10.148 -Goal "[| r<=s;  A<=B |] ==> r-``A <= s-``B";
  10.149 -by (Blast_tac 1);
  10.150 -qed "vimage_mono";
  10.151 -
  10.152 -val [sub,PQimp] = Goal
  10.153 -    "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)";
  10.154 -by (blast_tac (claset() addIs [sub RS subsetD, PQimp RS mp]) 1);
  10.155 -qed "Collect_mono";
  10.156 -
  10.157 -(** Monotonicity of implications -- some could go to FOL **)
  10.158 -
  10.159 -Goal "A<=B ==> x:A --> x:B";
  10.160 -by (Blast_tac 1);
  10.161 -qed "in_mono";
  10.162 -
  10.163 -goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
  10.164 -by (IntPr.fast_tac 1);
  10.165 -qed "conj_mono";
  10.166 -
  10.167 -goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
  10.168 -by (IntPr.fast_tac 1);
  10.169 -qed "disj_mono";
  10.170 -
  10.171 -goal IFOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
  10.172 -by (IntPr.fast_tac 1);
  10.173 -qed "imp_mono";
  10.174 -
  10.175 -goal IFOL.thy "P-->P";
  10.176 -by (rtac impI 1);
  10.177 -by (assume_tac 1);
  10.178 -qed "imp_refl";
  10.179 -
  10.180 -val [PQimp] = goal IFOL.thy
  10.181 -    "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))";
  10.182 -by IntPr.safe_tac;
  10.183 -by (etac (PQimp RS mp RS exI) 1);
  10.184 -qed "ex_mono";
  10.185 -
  10.186 -val [PQimp] = goal IFOL.thy
  10.187 -    "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))";
  10.188 -by IntPr.safe_tac;
  10.189 -by (etac (spec RS (PQimp RS mp)) 1);
  10.190 -qed "all_mono";
  10.191 -
  10.192 -(*Used in intr_elim.ML and in individual datatype definitions*)
  10.193 -bind_thms ("basic_monos",
  10.194 -  [subset_refl, imp_refl, disj_mono, conj_mono, ex_mono, Collect_mono, Part_mono, in_mono]);
    11.1 --- a/src/ZF/mono.thy	Fri Jun 28 20:01:09 2002 +0200
    11.2 +++ b/src/ZF/mono.thy	Sat Jun 29 21:33:06 2002 +0200
    11.3 @@ -1,2 +1,143 @@
    11.4 -mono = QPair + Sum + func
    11.5 +(*  Title:      ZF/mono
    11.6 +    ID:         $Id$
    11.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.8 +    Copyright   1993  University of Cambridge
    11.9 +
   11.10 +Monotonicity of various operations
   11.11 +*)
   11.12 +
   11.13 +theory mono = Sum + func:
   11.14 +
   11.15 +(** Replacement, in its various formulations **)
   11.16 +
   11.17 +(*Not easy to express monotonicity in P, since any "bigger" predicate
   11.18 +  would have to be single-valued*)
   11.19 +lemma Replace_mono: "A<=B ==> Replace(A,P) <= Replace(B,P)"
   11.20 +by (blast elim!: ReplaceE)
   11.21 +
   11.22 +lemma RepFun_mono: "A<=B ==> {f(x). x:A} <= {f(x). x:B}"
   11.23 +by blast
   11.24 +
   11.25 +lemma Pow_mono: "A<=B ==> Pow(A) <= Pow(B)"
   11.26 +by blast
   11.27 +
   11.28 +lemma Union_mono: "A<=B ==> Union(A) <= Union(B)"
   11.29 +by blast
   11.30 +
   11.31 +lemma UN_mono:
   11.32 +    "[| A<=C;  !!x. x:A ==> B(x)<=D(x) |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))"
   11.33 +by blast  
   11.34 +
   11.35 +(*Intersection is ANTI-monotonic.  There are TWO premises! *)
   11.36 +lemma Inter_anti_mono: "[| A<=B;  a:A |] ==> Inter(B) <= Inter(A)"
   11.37 +by blast
   11.38 +
   11.39 +lemma cons_mono: "C<=D ==> cons(a,C) <= cons(a,D)"
   11.40 +by blast
   11.41 +
   11.42 +lemma Un_mono: "[| A<=C;  B<=D |] ==> A Un B <= C Un D"
   11.43 +by blast
   11.44 +
   11.45 +lemma Int_mono: "[| A<=C;  B<=D |] ==> A Int B <= C Int D"
   11.46 +by blast
   11.47 +
   11.48 +lemma Diff_mono: "[| A<=C;  D<=B |] ==> A-B <= C-D"
   11.49 +by blast
   11.50 +
   11.51 +(** Standard products, sums and function spaces **)
   11.52 +
   11.53 +lemma Sigma_mono [rule_format]:
   11.54 +     "[| A<=C;  !!x. x:A --> B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)"
   11.55 +by blast
   11.56 +
   11.57 +lemma sum_mono: "[| A<=C;  B<=D |] ==> A+B <= C+D"
   11.58 +by (unfold sum_def, blast)
   11.59 +
   11.60 +(*Note that B->A and C->A are typically disjoint!*)
   11.61 +lemma Pi_mono: "B<=C ==> A->B <= A->C"
   11.62 +by (blast intro: lam_type elim: Pi_lamE)
   11.63 +
   11.64 +lemma lam_mono: "A<=B ==> Lambda(A,c) <= Lambda(B,c)"
   11.65 +apply (unfold lam_def)
   11.66 +apply (erule RepFun_mono)
   11.67 +done
   11.68 +
   11.69 +(** Converse, domain, range, field **)
   11.70 +
   11.71 +lemma converse_mono: "r<=s ==> converse(r) <= converse(s)"
   11.72 +by blast
   11.73 +
   11.74 +lemma domain_mono: "r<=s ==> domain(r)<=domain(s)"
   11.75 +by blast
   11.76  
   11.77 +lemmas domain_rel_subset = subset_trans [OF domain_mono domain_subset]
   11.78 +
   11.79 +lemma range_mono: "r<=s ==> range(r)<=range(s)"
   11.80 +by blast
   11.81 +
   11.82 +lemmas range_rel_subset = subset_trans [OF range_mono range_subset]
   11.83 +
   11.84 +lemma field_mono: "r<=s ==> field(r)<=field(s)"
   11.85 +by blast
   11.86 +
   11.87 +lemma field_rel_subset: "r <= A*A ==> field(r) <= A"
   11.88 +by (erule field_mono [THEN subset_trans], blast)
   11.89 +
   11.90 +
   11.91 +(** Images **)
   11.92 +
   11.93 +lemma image_pair_mono:
   11.94 +    "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r``A <= s``B"
   11.95 +by blast 
   11.96 +
   11.97 +lemma vimage_pair_mono:
   11.98 +    "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r-``A <= s-``B"
   11.99 +by blast 
  11.100 +
  11.101 +lemma image_mono: "[| r<=s;  A<=B |] ==> r``A <= s``B"
  11.102 +by blast
  11.103 +
  11.104 +lemma vimage_mono: "[| r<=s;  A<=B |] ==> r-``A <= s-``B"
  11.105 +by blast
  11.106 +
  11.107 +lemma Collect_mono:
  11.108 +    "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)"
  11.109 +by blast
  11.110 +
  11.111 +(*Used in intr_elim.ML and in individual datatype definitions*)
  11.112 +lemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono 
  11.113 +                     Collect_mono Part_mono in_mono
  11.114 +
  11.115 +ML
  11.116 +{*
  11.117 +val Replace_mono = thm "Replace_mono";
  11.118 +val RepFun_mono = thm "RepFun_mono";
  11.119 +val Pow_mono = thm "Pow_mono";
  11.120 +val Union_mono = thm "Union_mono";
  11.121 +val UN_mono = thm "UN_mono";
  11.122 +val Inter_anti_mono = thm "Inter_anti_mono";
  11.123 +val cons_mono = thm "cons_mono";
  11.124 +val Un_mono = thm "Un_mono";
  11.125 +val Int_mono = thm "Int_mono";
  11.126 +val Diff_mono = thm "Diff_mono";
  11.127 +val Sigma_mono = thm "Sigma_mono";
  11.128 +val sum_mono = thm "sum_mono";
  11.129 +val Pi_mono = thm "Pi_mono";
  11.130 +val lam_mono = thm "lam_mono";
  11.131 +val converse_mono = thm "converse_mono";
  11.132 +val domain_mono = thm "domain_mono";
  11.133 +val domain_rel_subset = thm "domain_rel_subset";
  11.134 +val range_mono = thm "range_mono";
  11.135 +val range_rel_subset = thm "range_rel_subset";
  11.136 +val field_mono = thm "field_mono";
  11.137 +val field_rel_subset = thm "field_rel_subset";
  11.138 +val image_pair_mono = thm "image_pair_mono";
  11.139 +val vimage_pair_mono = thm "vimage_pair_mono";
  11.140 +val image_mono = thm "image_mono";
  11.141 +val vimage_mono = thm "vimage_mono";
  11.142 +val Collect_mono = thm "Collect_mono";
  11.143 +
  11.144 +val basic_monos = thms "basic_monos";
  11.145 +*}
  11.146 +
  11.147 +end
    12.1 --- a/src/ZF/subset.ML	Fri Jun 28 20:01:09 2002 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,216 +0,0 @@
    12.4 -(*  Title:      ZF/subset
    12.5 -    ID:         $Id$
    12.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7 -    Copyright   1991  University of Cambridge
    12.8 -
    12.9 -Derived rules involving subsets
   12.10 -Union and Intersection as lattice operations
   12.11 -*)
   12.12 -
   12.13 -(*** cons ***)
   12.14 -
   12.15 -Goal "[| a:C; B<=C |] ==> cons(a,B) <= C";
   12.16 -by (Blast_tac 1);
   12.17 -qed "cons_subsetI";
   12.18 -
   12.19 -Goal "B <= cons(a,B)";
   12.20 -by (Blast_tac 1);
   12.21 -qed "subset_consI";
   12.22 -
   12.23 -Goal "cons(a,B)<=C <-> a:C & B<=C";
   12.24 -by (Blast_tac 1);
   12.25 -qed "cons_subset_iff";
   12.26 -AddIffs [cons_subset_iff];
   12.27 -
   12.28 -(*A safe special case of subset elimination, adding no new variables 
   12.29 -  [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)
   12.30 -bind_thm ("cons_subsetE", cons_subset_iff RS iffD1 RS conjE);
   12.31 -
   12.32 -Goal "A<=0 <-> A=0";
   12.33 -by (Blast_tac 1) ;
   12.34 -qed "subset_empty_iff";
   12.35 -
   12.36 -Goal "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)";
   12.37 -by (Blast_tac 1) ;
   12.38 -qed "subset_cons_iff";
   12.39 -
   12.40 -(*** succ ***)
   12.41 -
   12.42 -Goal "i <= succ(i)";
   12.43 -by (Blast_tac 1) ;
   12.44 -qed "subset_succI";
   12.45 -
   12.46 -(*But if j is an ordinal or is transitive, then i:j implies i<=j! 
   12.47 -  See ordinal/Ord_succ_subsetI*)
   12.48 -Goalw [succ_def] "[| i:j;  i<=j |] ==> succ(i)<=j";
   12.49 -by (Blast_tac 1) ;
   12.50 -qed "succ_subsetI";
   12.51 -
   12.52 -val major::prems= Goalw [succ_def]  
   12.53 -    "[| succ(i) <= j;  [| i:j;  i<=j |] ==> P \
   12.54 -\    |] ==> P";
   12.55 -by (rtac (major RS cons_subsetE) 1);
   12.56 -by (REPEAT (ares_tac prems 1)) ;
   12.57 -qed "succ_subsetE";
   12.58 -
   12.59 -Goalw [succ_def] "succ(a) <= B <-> (a <= B & a : B)";
   12.60 -by (Blast_tac 1) ;
   12.61 -qed "succ_subset_iff";
   12.62 -
   12.63 -(*** singletons ***)
   12.64 -
   12.65 -Goal "a:C ==> {a} <= C";
   12.66 -by (Blast_tac 1) ;
   12.67 -qed "singleton_subsetI";
   12.68 -
   12.69 -Goal "{a} <= C  ==>  a:C";
   12.70 -by (Blast_tac 1) ;
   12.71 -qed "singleton_subsetD";
   12.72 -
   12.73 -(*** Big Union -- least upper bound of a set  ***)
   12.74 -
   12.75 -Goal "Union(A) <= C <-> (ALL x:A. x <= C)";
   12.76 -by (Blast_tac 1);
   12.77 -qed "Union_subset_iff";
   12.78 -
   12.79 -Goal "B:A ==> B <= Union(A)";
   12.80 -by (Blast_tac 1);
   12.81 -qed "Union_upper";
   12.82 -
   12.83 -val [prem]= Goal
   12.84 -    "[| !!x. x:A ==> x<=C |] ==> Union(A) <= C";
   12.85 -by (rtac (ballI RS (Union_subset_iff RS iffD2)) 1);
   12.86 -by (etac prem 1) ;
   12.87 -qed "Union_least";
   12.88 -
   12.89 -(*** Union of a family of sets  ***)
   12.90 -
   12.91 -Goal "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
   12.92 -by (blast_tac (claset() addSEs [equalityE]) 1);
   12.93 -qed "subset_UN_iff_eq";
   12.94 -
   12.95 -Goal "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)";
   12.96 -by (Blast_tac 1);
   12.97 -qed "UN_subset_iff";
   12.98 -
   12.99 -Goal "x:A ==> B(x) <= (UN x:A. B(x))";
  12.100 -by (etac (RepFunI RS Union_upper) 1);
  12.101 -qed "UN_upper";
  12.102 -
  12.103 -val [prem]= Goal
  12.104 -    "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
  12.105 -by (rtac (ballI RS (UN_subset_iff RS iffD2)) 1);
  12.106 -by (etac prem 1) ;
  12.107 -qed "UN_least";
  12.108 -
  12.109 -
  12.110 -(*** Big Intersection -- greatest lower bound of a nonempty set ***)
  12.111 -
  12.112 -Goal "a: A  ==>  C <= Inter(A) <-> (ALL x:A. C <= x)";
  12.113 -by (Blast_tac 1);
  12.114 -qed "Inter_subset_iff";
  12.115 -
  12.116 -Goal "B:A ==> Inter(A) <= B";
  12.117 -by (Blast_tac 1);
  12.118 -qed "Inter_lower";
  12.119 -
  12.120 -val [prem1,prem2]= Goal
  12.121 -    "[| a:A;  !!x. x:A ==> C<=x |] ==> C <= Inter(A)";
  12.122 -by (rtac ([prem1, ballI] MRS (Inter_subset_iff RS iffD2)) 1);
  12.123 -by (etac prem2 1) ;
  12.124 -qed "Inter_greatest";
  12.125 -
  12.126 -(*** Intersection of a family of sets  ***)
  12.127 -
  12.128 -Goal "x:A ==> (INT x:A. B(x)) <= B(x)";
  12.129 -by (Blast_tac 1);
  12.130 -qed "INT_lower";
  12.131 -
  12.132 -val [nonempty,prem] = Goal
  12.133 -    "[| a:A;  !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
  12.134 -by (rtac (nonempty RS RepFunI RS Inter_greatest) 1);
  12.135 -by (REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1));
  12.136 -qed "INT_greatest";
  12.137 -
  12.138 -
  12.139 -(*** Finite Union -- the least upper bound of 2 sets ***)
  12.140 -
  12.141 -Goal "A Un B <= C <-> A <= C & B <= C";
  12.142 -by (Blast_tac 1);
  12.143 -qed "Un_subset_iff";
  12.144 -
  12.145 -Goal "A <= A Un B";
  12.146 -by (Blast_tac 1);
  12.147 -qed "Un_upper1";
  12.148 -
  12.149 -Goal "B <= A Un B";
  12.150 -by (Blast_tac 1);
  12.151 -qed "Un_upper2";
  12.152 -
  12.153 -Goal "[| A<=C;  B<=C |] ==> A Un B <= C";
  12.154 -by (Blast_tac 1);
  12.155 -qed "Un_least";
  12.156 -
  12.157 -
  12.158 -(*** Finite Intersection -- the greatest lower bound of 2 sets *)
  12.159 -
  12.160 -Goal "C <= A Int B <-> C <= A & C <= B";
  12.161 -by (Blast_tac 1);
  12.162 -qed "Int_subset_iff";
  12.163 -
  12.164 -Goal "A Int B <= A";
  12.165 -by (Blast_tac 1);
  12.166 -qed "Int_lower1";
  12.167 -
  12.168 -Goal "A Int B <= B";
  12.169 -by (Blast_tac 1);
  12.170 -qed "Int_lower2";
  12.171 -
  12.172 -Goal "[| C<=A;  C<=B |] ==> C <= A Int B";
  12.173 -by (Blast_tac 1);
  12.174 -qed "Int_greatest";
  12.175 -
  12.176 -
  12.177 -(*** Set difference *)
  12.178 -
  12.179 -Goal "A-B <= A";
  12.180 -by (Blast_tac 1);
  12.181 -qed "Diff_subset";
  12.182 -
  12.183 -Goal "[| C<=A;  C Int B = 0 |] ==> C <= A-B";
  12.184 -by (Blast_tac 1);
  12.185 -qed "Diff_contains";
  12.186 -
  12.187 -Goal "B <= A - cons(c,C)  <->  B<=A-C & c ~: B";
  12.188 -by (Blast_tac 1);
  12.189 -qed "subset_Diff_cons_iff";
  12.190 -
  12.191 -
  12.192 -
  12.193 -(** Collect **)
  12.194 -
  12.195 -Goal "Collect(A,P) <= A";
  12.196 -by (Blast_tac 1);
  12.197 -qed "Collect_subset";
  12.198 -
  12.199 -
  12.200 -(** RepFun **)
  12.201 -
  12.202 -val prems = Goal "[| !!x. x:A ==> f(x): B |] ==> {f(x). x:A} <= B";
  12.203 -by (blast_tac (claset() addIs prems) 1);
  12.204 -qed "RepFun_subset";
  12.205 -
  12.206 -bind_thms ("subset_SIs",
  12.207 -    [subset_refl, cons_subsetI, subset_consI, 
  12.208 -     Union_least, UN_least, Un_least, 
  12.209 -     Inter_greatest, Int_greatest, RepFun_subset,
  12.210 -     Un_upper1, Un_upper2, Int_lower1, Int_lower2]);
  12.211 -
  12.212 -
  12.213 -(*A claset for subset reasoning*)
  12.214 -val subset_cs = claset() 
  12.215 -    delrules [subsetI, subsetCE]
  12.216 -    addSIs subset_SIs
  12.217 -    addIs  [Union_upper, Inter_lower]
  12.218 -    addSEs [cons_subsetE];
  12.219 -
    13.1 --- a/src/ZF/subset.thy	Fri Jun 28 20:01:09 2002 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,3 +0,0 @@
    13.4 -(*Dummy theory to document dependencies *)
    13.5 -
    13.6 -subset = pair
    14.1 --- a/src/ZF/upair.ML	Fri Jun 28 20:01:09 2002 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,404 +0,0 @@
    14.4 -(*  Title:      ZF/upair
    14.5 -    ID:         $Id$
    14.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.7 -    Copyright   1991  University of Cambridge
    14.8 -
    14.9 -UNORDERED pairs in Zermelo-Fraenkel Set Theory 
   14.10 -
   14.11 -Observe the order of dependence:
   14.12 -    Upair is defined in terms of Replace
   14.13 -    Un is defined in terms of Upair and Union (similarly for Int)
   14.14 -    cons is defined in terms of Upair and Un
   14.15 -    Ordered pairs and descriptions are defined using cons ("set notation")
   14.16 -*)
   14.17 -
   14.18 -(*** Lemmas about power sets  ***)
   14.19 -
   14.20 -bind_thm ("Pow_bottom", empty_subsetI RS PowI);         (* 0 : Pow(B) *)
   14.21 -bind_thm ("Pow_top", subset_refl RS PowI);              (* A : Pow(A) *)
   14.22 -
   14.23 -
   14.24 -(*** Unordered pairs - Upair ***)
   14.25 -
   14.26 -Goalw [Upair_def] "c : Upair(a,b) <-> (c=a | c=b)";
   14.27 -by (Blast_tac 1) ;
   14.28 -qed "Upair_iff";
   14.29 -
   14.30 -Addsimps [Upair_iff];
   14.31 -
   14.32 -Goal "a : Upair(a,b)";
   14.33 -by (Simp_tac 1);
   14.34 -qed "UpairI1";
   14.35 -
   14.36 -Goal "b : Upair(a,b)";
   14.37 -by (Simp_tac 1);
   14.38 -qed "UpairI2";
   14.39 -
   14.40 -val major::prems= Goal
   14.41 -    "[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P";
   14.42 -by (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1);
   14.43 -by (REPEAT (eresolve_tac prems 1)) ;
   14.44 -qed "UpairE";
   14.45 -
   14.46 -AddSIs [UpairI1,UpairI2];
   14.47 -AddSEs [UpairE];
   14.48 -
   14.49 -(*** Rules for binary union -- Un -- defined via Upair ***)
   14.50 -
   14.51 -Goalw [Un_def]  "c : A Un B <-> (c:A | c:B)";
   14.52 -by (Blast_tac 1);
   14.53 -qed "Un_iff";
   14.54 -
   14.55 -Addsimps [Un_iff];
   14.56 -
   14.57 -Goal "c : A ==> c : A Un B";
   14.58 -by (Asm_simp_tac 1);
   14.59 -qed "UnI1";
   14.60 -
   14.61 -Goal "c : B ==> c : A Un B";
   14.62 -by (Asm_simp_tac 1);
   14.63 -qed "UnI2";
   14.64 -
   14.65 -val major::prems= Goal 
   14.66 -    "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P";
   14.67 -by (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1);
   14.68 -by (REPEAT (eresolve_tac prems 1)) ;
   14.69 -qed "UnE";
   14.70 -
   14.71 -(*Stronger version of the rule above*)
   14.72 -val major::prems = Goal
   14.73 -    "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P";
   14.74 -by (rtac (major RS UnE) 1);
   14.75 -by (eresolve_tac prems 1);
   14.76 -by (rtac classical 1);
   14.77 -by (eresolve_tac prems 1);
   14.78 -by (swap_res_tac prems 1);
   14.79 -by (etac notnotD 1);
   14.80 -qed "UnE'";
   14.81 -
   14.82 -(*Classical introduction rule: no commitment to A vs B*)
   14.83 -val prems = Goal "(c ~: B ==> c : A) ==> c : A Un B";
   14.84 -by (Simp_tac 1);
   14.85 -by (blast_tac (claset() addSIs prems) 1);
   14.86 -qed "UnCI";
   14.87 -
   14.88 -AddSIs [UnCI];
   14.89 -AddSEs [UnE];
   14.90 -
   14.91 -
   14.92 -(*** Rules for small intersection -- Int -- defined via Upair ***)
   14.93 -
   14.94 -Goalw [Int_def]  "c : A Int B <-> (c:A & c:B)";
   14.95 -by (Blast_tac 1);
   14.96 -qed "Int_iff";
   14.97 -
   14.98 -Addsimps [Int_iff];
   14.99 -
  14.100 -Goal "[| c : A;  c : B |] ==> c : A Int B";
  14.101 -by (Asm_simp_tac 1);
  14.102 -qed "IntI";
  14.103 -
  14.104 -Goal "c : A Int B ==> c : A";
  14.105 -by (Asm_full_simp_tac 1);
  14.106 -qed "IntD1";
  14.107 -
  14.108 -Goal "c : A Int B ==> c : B";
  14.109 -by (Asm_full_simp_tac 1);
  14.110 -qed "IntD2";
  14.111 -
  14.112 -val prems = Goal "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P";
  14.113 -by (resolve_tac prems 1);
  14.114 -by (REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ;
  14.115 -qed "IntE";
  14.116 -
  14.117 -AddSIs [IntI];
  14.118 -AddSEs [IntE];
  14.119 -
  14.120 -(*** Rules for set difference -- defined via Upair ***)
  14.121 -
  14.122 -Goalw [Diff_def]  "c : A-B <-> (c:A & c~:B)";
  14.123 -by (Blast_tac 1);
  14.124 -qed "Diff_iff";
  14.125 -
  14.126 -Addsimps [Diff_iff];
  14.127 -
  14.128 -Goal "[| c : A;  c ~: B |] ==> c : A - B";
  14.129 -by (Asm_simp_tac 1);
  14.130 -qed "DiffI";
  14.131 -
  14.132 -Goal "c : A - B ==> c : A";
  14.133 -by (Asm_full_simp_tac 1);
  14.134 -qed "DiffD1";
  14.135 -
  14.136 -Goal "c : A - B ==> c ~: B";
  14.137 -by (Asm_full_simp_tac 1);
  14.138 -qed "DiffD2";
  14.139 -
  14.140 -val prems = Goal "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P";
  14.141 -by (resolve_tac prems 1);
  14.142 -by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ;
  14.143 -qed "DiffE";
  14.144 -
  14.145 -AddSIs [DiffI];
  14.146 -AddSEs [DiffE];
  14.147 -
  14.148 -(*** Rules for cons -- defined via Un and Upair ***)
  14.149 -
  14.150 -Goalw [cons_def]  "a : cons(b,A) <-> (a=b | a:A)";
  14.151 -by (Blast_tac 1);
  14.152 -qed "cons_iff";
  14.153 -
  14.154 -Addsimps [cons_iff];
  14.155 -
  14.156 -Goal "a : cons(a,B)";
  14.157 -by (Simp_tac 1);
  14.158 -qed "consI1";
  14.159 -
  14.160 -Addsimps [consI1];
  14.161 -AddTCs   [consI1];   (*risky as a typechecking rule, but solves otherwise
  14.162 -		       unconstrained goals of the form  x : ?A*)
  14.163 -
  14.164 -Goal "a : B ==> a : cons(b,B)";
  14.165 -by (Asm_simp_tac 1);
  14.166 -qed "consI2";
  14.167 -
  14.168 -val major::prems= Goal
  14.169 -    "[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P";
  14.170 -by (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1);
  14.171 -by (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ;
  14.172 -qed "consE";
  14.173 -
  14.174 -(*Stronger version of the rule above*)
  14.175 -val major::prems = Goal
  14.176 -    "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P";
  14.177 -by (rtac (major RS consE) 1);
  14.178 -by (eresolve_tac prems 1);
  14.179 -by (rtac classical 1);
  14.180 -by (eresolve_tac prems 1);
  14.181 -by (swap_res_tac prems 1);
  14.182 -by (etac notnotD 1);
  14.183 -qed "consE'";
  14.184 -
  14.185 -(*Classical introduction rule*)
  14.186 -val prems = Goal "(a~:B ==> a=b) ==> a: cons(b,B)";
  14.187 -by (Simp_tac 1);
  14.188 -by (blast_tac (claset() addSIs prems) 1);
  14.189 -qed "consCI";
  14.190 -
  14.191 -AddSIs [consCI];
  14.192 -AddSEs [consE];
  14.193 -
  14.194 -Goal "cons(a,B) ~= 0";
  14.195 -by (blast_tac (claset() addEs [equalityE]) 1) ;
  14.196 -qed "cons_not_0";
  14.197 -
  14.198 -bind_thm ("cons_neq_0", cons_not_0 RS notE);
  14.199 -
  14.200 -Addsimps [cons_not_0, cons_not_0 RS not_sym];
  14.201 -
  14.202 -
  14.203 -(*** Singletons - using cons ***)
  14.204 -
  14.205 -Goal "a : {b} <-> a=b";
  14.206 -by (Simp_tac 1);
  14.207 -qed "singleton_iff";
  14.208 -
  14.209 -Goal "a : {a}";
  14.210 -by (rtac consI1 1) ;
  14.211 -qed "singletonI";
  14.212 -
  14.213 -bind_thm ("singletonE", make_elim (singleton_iff RS iffD1));
  14.214 -
  14.215 -AddSIs [singletonI];
  14.216 -AddSEs [singletonE];
  14.217 -
  14.218 -(*** Rules for Descriptions ***)
  14.219 -
  14.220 -val [pa,eq] = Goalw [the_def] 
  14.221 -    "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a";
  14.222 -by (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ;
  14.223 -qed "the_equality";
  14.224 -
  14.225 -AddIs [the_equality];
  14.226 -
  14.227 -(* Only use this if you already know EX!x. P(x) *)
  14.228 -Goal "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a";
  14.229 -by (Blast_tac 1);
  14.230 -qed "the_equality2";
  14.231 -
  14.232 -Goal "EX! x. P(x) ==> P(THE x. P(x))";
  14.233 -by (etac ex1E 1);
  14.234 -by (stac the_equality 1);
  14.235 -by (REPEAT (Blast_tac 1));
  14.236 -qed "theI";
  14.237 -
  14.238 -(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then 
  14.239 -  (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
  14.240 -
  14.241 -(*If it's "undefined", it's zero!*)
  14.242 -Goalw  [the_def] "~ (EX! x. P(x)) ==> (THE x. P(x))=0";
  14.243 -by (blast_tac (claset() addSEs [ReplaceE]) 1);
  14.244 -qed "the_0";
  14.245 -
  14.246 -(*Easier to apply than theI: conclusion has only one occurrence of P*)
  14.247 -val prems = 
  14.248 -Goal "[| ~ Q(0) ==> EX! x. P(x);  !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))";
  14.249 -by (rtac classical 1);
  14.250 -by (resolve_tac prems 1);
  14.251 -by (rtac theI 1);
  14.252 -by (rtac classical 1);
  14.253 -by (resolve_tac prems 1);
  14.254 -by (etac (the_0 RS subst) 1);
  14.255 -by (assume_tac 1);
  14.256 -qed "theI2";
  14.257 -
  14.258 -(*** if -- a conditional expression for formulae ***)
  14.259 -
  14.260 -Goalw [if_def] "(if True then a else b) = a";
  14.261 -by (Blast_tac 1);
  14.262 -qed "if_true";
  14.263 -
  14.264 -Goalw [if_def] "(if False then a else b) = b";
  14.265 -by (Blast_tac 1);
  14.266 -qed "if_false";
  14.267 -
  14.268 -(*Never use with case splitting, or if P is known to be true or false*)
  14.269 -val prems = Goalw [if_def]
  14.270 -    "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |] \
  14.271 -\    ==> (if P then a else b) = (if Q then c else d)";
  14.272 -by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1);
  14.273 -qed "if_cong";
  14.274 -
  14.275 -(*Prevents simplification of x and y: faster and allows the execution
  14.276 -  of functional programs. NOW THE DEFAULT.*)
  14.277 -Goal "P<->Q ==> (if P then x else y) = (if Q then x else y)";
  14.278 -by (Asm_simp_tac 1);
  14.279 -qed "if_weak_cong";
  14.280 -
  14.281 -(*Not needed for rewriting, since P would rewrite to True anyway*)
  14.282 -Goalw [if_def] "P ==> (if P then a else b) = a";
  14.283 -by (Blast_tac 1);
  14.284 -qed "if_P";
  14.285 -
  14.286 -(*Not needed for rewriting, since P would rewrite to False anyway*)
  14.287 -Goalw [if_def] "~P ==> (if P then a else b) = b";
  14.288 -by (Blast_tac 1);
  14.289 -qed "if_not_P";
  14.290 -
  14.291 -Addsimps [if_true, if_false];
  14.292 -
  14.293 -Goal "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))";
  14.294 -by (case_tac "Q" 1);
  14.295 -by (Asm_simp_tac 1);
  14.296 -by (Asm_simp_tac 1) ;
  14.297 -qed "split_if";
  14.298 -
  14.299 -(** Rewrite rules for boolean case-splitting: faster than 
  14.300 -	addsplits[split_if]
  14.301 -**)
  14.302 -
  14.303 -bind_thm ("split_if_eq1", inst "P" "%x. x = ?b" split_if);
  14.304 -bind_thm ("split_if_eq2", inst "P" "%x. ?a = x" split_if);
  14.305 -
  14.306 -bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if);
  14.307 -bind_thm ("split_if_mem2", inst "P" "%x. ?a : x" split_if);
  14.308 -
  14.309 -bind_thms ("split_ifs", [split_if_eq1, split_if_eq2, split_if_mem1, split_if_mem2]);
  14.310 -
  14.311 -(*Logically equivalent to split_if_mem2*)
  14.312 -Goal "a: (if P then x else y) <-> P & a:x | ~P & a:y";
  14.313 -by (simp_tac (simpset() addsplits [split_if]) 1) ;
  14.314 -qed "if_iff";
  14.315 -
  14.316 -val prems = Goal
  14.317 -    "[| P ==> a: A;  ~P ==> b: A |] ==> (if P then a else b): A";
  14.318 -by (simp_tac (simpset() addsimps prems addsplits [split_if]) 1) ;
  14.319 -qed "if_type";
  14.320 -
  14.321 -AddTCs [if_type];
  14.322 -
  14.323 -(*** Foundation lemmas ***)
  14.324 -
  14.325 -(*was called mem_anti_sym*)
  14.326 -val prems = Goal "[| a:b;  ~P ==> b:a |] ==> P";
  14.327 -by (rtac classical 1);
  14.328 -by (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1);
  14.329 -by (REPEAT (blast_tac (claset() addIs prems addSEs [equalityE]) 1));
  14.330 -qed "mem_asym";
  14.331 -
  14.332 -(*was called mem_anti_refl*)
  14.333 -Goal "a:a ==> P";
  14.334 -by (blast_tac (claset() addIs [mem_asym]) 1);
  14.335 -qed "mem_irrefl";
  14.336 -
  14.337 -(*mem_irrefl should NOT be added to default databases:
  14.338 -      it would be tried on most goals, making proofs slower!*)
  14.339 -
  14.340 -Goal "a ~: a";
  14.341 -by (rtac notI 1);
  14.342 -by (etac mem_irrefl 1);
  14.343 -qed "mem_not_refl";
  14.344 -
  14.345 -(*Good for proving inequalities by rewriting*)
  14.346 -Goal "a:A ==> a ~= A";
  14.347 -by (blast_tac (claset() addSEs [mem_irrefl]) 1);
  14.348 -qed "mem_imp_not_eq";
  14.349 -
  14.350 -(*** Rules for succ ***)
  14.351 -
  14.352 -Goalw [succ_def]  "i : succ(j) <-> i=j | i:j";
  14.353 -by (Blast_tac 1);
  14.354 -qed "succ_iff";
  14.355 -
  14.356 -Goalw [succ_def]  "i : succ(i)";
  14.357 -by (rtac consI1 1) ;
  14.358 -qed "succI1";
  14.359 -
  14.360 -Addsimps [succI1];
  14.361 -
  14.362 -Goalw [succ_def] "i : j ==> i : succ(j)";
  14.363 -by (etac consI2 1) ;
  14.364 -qed "succI2";
  14.365 -
  14.366 -val major::prems= Goalw [succ_def] 
  14.367 -    "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P";
  14.368 -by (rtac (major RS consE) 1);
  14.369 -by (REPEAT (eresolve_tac prems 1)) ;
  14.370 -qed "succE";
  14.371 -
  14.372 -(*Classical introduction rule*)
  14.373 -val [prem]= Goal "(i~:j ==> i=j) ==> i: succ(j)";
  14.374 -by (rtac (disjCI RS (succ_iff RS iffD2)) 1);
  14.375 -by (etac prem 1) ;
  14.376 -qed "succCI";
  14.377 -
  14.378 -AddSIs [succCI];
  14.379 -AddSEs [succE];
  14.380 -
  14.381 -Goal "succ(n) ~= 0";
  14.382 -by (blast_tac (claset() addSEs [equalityE]) 1) ;
  14.383 -qed "succ_not_0";
  14.384 -
  14.385 -bind_thm ("succ_neq_0", succ_not_0 RS notE);
  14.386 -
  14.387 -Addsimps [succ_not_0, succ_not_0 RS not_sym];
  14.388 -AddSEs [succ_neq_0, sym RS succ_neq_0];
  14.389 -
  14.390 -
  14.391 -(* succ(c) <= B ==> c : B *)
  14.392 -bind_thm ("succ_subsetD", succI1 RSN (2,subsetD));
  14.393 -
  14.394 -(* succ(b) ~= b *)
  14.395 -bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);
  14.396 -
  14.397 -Goal "succ(m) = succ(n) <-> m=n";
  14.398 -by (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ;
  14.399 -qed "succ_inject_iff";
  14.400 -
  14.401 -bind_thm ("succ_inject", succ_inject_iff RS iffD1);
  14.402 -
  14.403 -Addsimps [succ_inject_iff];
  14.404 -AddSDs [succ_inject];
  14.405 -
  14.406 -(*Not needed now that cons is available.  Deletion reduces the search space.*)
  14.407 -Delrules [UpairI1,UpairI2,UpairE];
    15.1 --- a/src/ZF/upair.thy	Fri Jun 28 20:01:09 2002 +0200
    15.2 +++ b/src/ZF/upair.thy	Sat Jun 29 21:33:06 2002 +0200
    15.3 @@ -2,6 +2,14 @@
    15.4      ID:         $Id$
    15.5      Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
    15.6      Copyright   1993  University of Cambridge
    15.7 +
    15.8 +UNORDERED pairs in Zermelo-Fraenkel Set Theory 
    15.9 +
   15.10 +Observe the order of dependence:
   15.11 +    Upair is defined in terms of Replace
   15.12 +    Un is defined in terms of Upair and Union (similarly for Int)
   15.13 +    cons is defined in terms of Upair and Un
   15.14 +    Ordered pairs and descriptions are defined using cons ("set notation")
   15.15  *)
   15.16  
   15.17  theory upair = ZF
   15.18 @@ -10,4 +18,379 @@
   15.19  setup TypeCheck.setup
   15.20  declare atomize_ball [symmetric, rulify]
   15.21  
   15.22 +(*** Lemmas about power sets  ***)
   15.23 +
   15.24 +lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 : Pow(B) *)
   15.25 +lemmas Pow_top = subset_refl [THEN PowI] (* A : Pow(A) *)
   15.26 +
   15.27 +
   15.28 +(*** Unordered pairs - Upair ***)
   15.29 +
   15.30 +lemma Upair_iff [simp]: "c : Upair(a,b) <-> (c=a | c=b)"
   15.31 +by (unfold Upair_def, blast)
   15.32 +
   15.33 +lemma UpairI1: "a : Upair(a,b)"
   15.34 +by simp
   15.35 +
   15.36 +lemma UpairI2: "b : Upair(a,b)"
   15.37 +by simp
   15.38 +
   15.39 +lemma UpairE:
   15.40 +    "[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
   15.41 +apply simp
   15.42 +apply blast 
   15.43 +done
   15.44 +
   15.45 +(*** Rules for binary union -- Un -- defined via Upair ***)
   15.46 +
   15.47 +lemma Un_iff [simp]: "c : A Un B <-> (c:A | c:B)"
   15.48 +apply (simp add: Un_def)
   15.49 +apply (blast intro: UpairI1 UpairI2 elim: UpairE)
   15.50 +done
   15.51 +
   15.52 +lemma UnI1: "c : A ==> c : A Un B"
   15.53 +by simp
   15.54 +
   15.55 +lemma UnI2: "c : B ==> c : A Un B"
   15.56 +by simp
   15.57 +
   15.58 +lemma UnE [elim!]: "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
   15.59 +apply simp 
   15.60 +apply blast 
   15.61 +done
   15.62 +
   15.63 +(*Stronger version of the rule above*)
   15.64 +lemma UnE': "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P"
   15.65 +apply simp 
   15.66 +apply blast 
   15.67 +done
   15.68 +
   15.69 +(*Classical introduction rule: no commitment to A vs B*)
   15.70 +lemma UnCI [intro!]: "(c ~: B ==> c : A) ==> c : A Un B"
   15.71 +apply simp
   15.72 +apply blast
   15.73 +done
   15.74 +
   15.75 +
   15.76 +(*** Rules for small intersection -- Int -- defined via Upair ***)
   15.77 +
   15.78 +lemma Int_iff [simp]: "c : A Int B <-> (c:A & c:B)"
   15.79 +apply (unfold Int_def)
   15.80 +apply (blast intro: UpairI1 UpairI2 elim: UpairE)
   15.81 +done
   15.82 +
   15.83 +lemma IntI [intro!]: "[| c : A;  c : B |] ==> c : A Int B"
   15.84 +by simp
   15.85 +
   15.86 +lemma IntD1: "c : A Int B ==> c : A"
   15.87 +by simp
   15.88 +
   15.89 +lemma IntD2: "c : A Int B ==> c : B"
   15.90 +by simp
   15.91 +
   15.92 +lemma IntE [elim!]: "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
   15.93 +by simp
   15.94 +
   15.95 +
   15.96 +(*** Rules for set difference -- defined via Upair ***)
   15.97 +
   15.98 +lemma Diff_iff [simp]: "c : A-B <-> (c:A & c~:B)"
   15.99 +by (unfold Diff_def, blast)
  15.100 +
  15.101 +lemma DiffI [intro!]: "[| c : A;  c ~: B |] ==> c : A - B"
  15.102 +by simp
  15.103 +
  15.104 +lemma DiffD1: "c : A - B ==> c : A"
  15.105 +by simp
  15.106 +
  15.107 +lemma DiffD2: "c : A - B ==> c ~: B"
  15.108 +by simp
  15.109 +
  15.110 +lemma DiffE [elim!]: "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
  15.111 +by simp
  15.112 +
  15.113 +
  15.114 +(*** Rules for cons -- defined via Un and Upair ***)
  15.115 +
  15.116 +lemma cons_iff [simp]: "a : cons(b,A) <-> (a=b | a:A)"
  15.117 +apply (unfold cons_def)
  15.118 +apply (blast intro: UpairI1 UpairI2 elim: UpairE)
  15.119 +done
  15.120 +
  15.121 +(*risky as a typechecking rule, but solves otherwise unconstrained goals of
  15.122 +the form x : ?A*)
  15.123 +lemma consI1 [simp,TC]: "a : cons(a,B)"
  15.124 +by simp
  15.125 +
  15.126 +
  15.127 +lemma consI2: "a : B ==> a : cons(b,B)"
  15.128 +by simp
  15.129 +
  15.130 +lemma consE [elim!]:
  15.131 +    "[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P"
  15.132 +apply simp 
  15.133 +apply blast 
  15.134 +done
  15.135 +
  15.136 +(*Stronger version of the rule above*)
  15.137 +lemma consE':
  15.138 +    "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P"
  15.139 +apply simp 
  15.140 +apply blast 
  15.141 +done
  15.142 +
  15.143 +(*Classical introduction rule*)
  15.144 +lemma consCI [intro!]: "(a~:B ==> a=b) ==> a: cons(b,B)"
  15.145 +apply simp
  15.146 +apply blast
  15.147 +done
  15.148 +
  15.149 +lemma cons_not_0 [simp]: "cons(a,B) ~= 0"
  15.150 +by (blast elim: equalityE)
  15.151 +
  15.152 +lemmas cons_neq_0 = cons_not_0 [THEN notE, standard]
  15.153 +
  15.154 +declare cons_not_0 [THEN not_sym, simp]
  15.155 +
  15.156 +
  15.157 +(*** Singletons - using cons ***)
  15.158 +
  15.159 +lemma singleton_iff: "a : {b} <-> a=b"
  15.160 +by simp
  15.161 +
  15.162 +lemma singletonI [intro!]: "a : {a}"
  15.163 +by (rule consI1)
  15.164 +
  15.165 +lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!]
  15.166 +
  15.167 +
  15.168 +(*** Rules for Descriptions ***)
  15.169 +
  15.170 +lemma the_equality [intro]:
  15.171 +    "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
  15.172 +apply (unfold the_def) 
  15.173 +apply (fast dest: subst)
  15.174 +done
  15.175 +
  15.176 +(* Only use this if you already know EX!x. P(x) *)
  15.177 +lemma the_equality2: "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
  15.178 +by blast
  15.179 +
  15.180 +lemma theI: "EX! x. P(x) ==> P(THE x. P(x))"
  15.181 +apply (erule ex1E)
  15.182 +apply (subst the_equality)
  15.183 +apply (blast+)
  15.184 +done
  15.185 +
  15.186 +(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then 
  15.187 +  (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
  15.188 +
  15.189 +(*If it's "undefined", it's zero!*)
  15.190 +lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0"
  15.191 +apply (unfold the_def)
  15.192 +apply (blast elim!: ReplaceE)
  15.193 +done
  15.194 +
  15.195 +(*Easier to apply than theI: conclusion has only one occurrence of P*)
  15.196 +lemma theI2:
  15.197 +    assumes p1: "~ Q(0) ==> EX! x. P(x)"
  15.198 +        and p2: "!!x. P(x) ==> Q(x)"
  15.199 +    shows "Q(THE x. P(x))"
  15.200 +apply (rule classical)
  15.201 +apply (rule p2)
  15.202 +apply (rule theI)
  15.203 +apply (rule classical)
  15.204 +apply (rule p1)
  15.205 +apply (erule the_0 [THEN subst], assumption)
  15.206 +done
  15.207 +
  15.208 +(*** if -- a conditional expression for formulae ***)
  15.209 +
  15.210 +lemma if_true [simp]: "(if True then a else b) = a"
  15.211 +by (unfold if_def, blast)
  15.212 +
  15.213 +lemma if_false [simp]: "(if False then a else b) = b"
  15.214 +by (unfold if_def, blast)
  15.215 +
  15.216 +(*Never use with case splitting, or if P is known to be true or false*)
  15.217 +lemma if_cong:
  15.218 +    "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |]  
  15.219 +     ==> (if P then a else b) = (if Q then c else d)"
  15.220 +by (simp add: if_def cong add: conj_cong)
  15.221 +
  15.222 +(*Prevents simplification of x and y: faster and allows the execution
  15.223 +  of functional programs. NOW THE DEFAULT.*)
  15.224 +lemma if_weak_cong: "P<->Q ==> (if P then x else y) = (if Q then x else y)"
  15.225 +by simp
  15.226 +
  15.227 +(*Not needed for rewriting, since P would rewrite to True anyway*)
  15.228 +lemma if_P: "P ==> (if P then a else b) = a"
  15.229 +by (unfold if_def, blast)
  15.230 +
  15.231 +(*Not needed for rewriting, since P would rewrite to False anyway*)
  15.232 +lemma if_not_P: "~P ==> (if P then a else b) = b"
  15.233 +by (unfold if_def, blast)
  15.234 +
  15.235 +lemma split_if: "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
  15.236 +(*no case_tac yet!*)
  15.237 +apply (rule_tac P=Q in case_split_thm, simp_all)
  15.238 +done
  15.239 +
  15.240 +(** Rewrite rules for boolean case-splitting: faster than 
  15.241 +	addsplits[split_if]
  15.242 +**)
  15.243 +
  15.244 +lemmas split_if_eq1 = split_if [of "%x. x = b", standard]
  15.245 +lemmas split_if_eq2 = split_if [of "%x. a = x", standard]
  15.246 +
  15.247 +lemmas split_if_mem1 = split_if [of "%x. x : b", standard]
  15.248 +lemmas split_if_mem2 = split_if [of "%x. a : x", standard]
  15.249 +
  15.250 +lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
  15.251 +
  15.252 +(*Logically equivalent to split_if_mem2*)
  15.253 +lemma if_iff: "a: (if P then x else y) <-> P & a:x | ~P & a:y"
  15.254 +by (simp split add: split_if)
  15.255 +
  15.256 +lemma if_type [TC]:
  15.257 +    "[| P ==> a: A;  ~P ==> b: A |] ==> (if P then a else b): A"
  15.258 +by (simp split add: split_if)
  15.259 +
  15.260 +
  15.261 +(*** Foundation lemmas ***)
  15.262 +
  15.263 +(*was called mem_anti_sym*)
  15.264 +lemma mem_asym: "[| a:b;  ~P ==> b:a |] ==> P"
  15.265 +apply (rule classical)
  15.266 +apply (rule_tac A1 = "{a,b}" in foundation [THEN disjE])
  15.267 +apply (blast elim!: equalityE)+
  15.268 +done
  15.269 +
  15.270 +(*was called mem_anti_refl*)
  15.271 +lemma mem_irrefl: "a:a ==> P"
  15.272 +by (blast intro: mem_asym)
  15.273 +
  15.274 +(*mem_irrefl should NOT be added to default databases:
  15.275 +      it would be tried on most goals, making proofs slower!*)
  15.276 +
  15.277 +lemma mem_not_refl: "a ~: a"
  15.278 +apply (rule notI)
  15.279 +apply (erule mem_irrefl)
  15.280 +done
  15.281 +
  15.282 +(*Good for proving inequalities by rewriting*)
  15.283 +lemma mem_imp_not_eq: "a:A ==> a ~= A"
  15.284 +by (blast elim!: mem_irrefl)
  15.285 +
  15.286 +(*** Rules for succ ***)
  15.287 +
  15.288 +lemma succ_iff: "i : succ(j) <-> i=j | i:j"
  15.289 +by (unfold succ_def, blast)
  15.290 +
  15.291 +lemma succI1 [simp]: "i : succ(i)"
  15.292 +by (simp add: succ_iff)
  15.293 +
  15.294 +lemma succI2: "i : j ==> i : succ(j)"
  15.295 +by (simp add: succ_iff)
  15.296 +
  15.297 +lemma succE [elim!]: 
  15.298 +    "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"
  15.299 +apply (simp add: succ_iff, blast) 
  15.300 +done
  15.301 +
  15.302 +(*Classical introduction rule*)
  15.303 +lemma succCI [intro!]: "(i~:j ==> i=j) ==> i: succ(j)"
  15.304 +by (simp add: succ_iff, blast)
  15.305 +
  15.306 +lemma succ_not_0 [simp]: "succ(n) ~= 0"
  15.307 +by (blast elim!: equalityE)
  15.308 +
  15.309 +lemmas succ_neq_0 = succ_not_0 [THEN notE, standard, elim!]
  15.310 +
  15.311 +declare succ_not_0 [THEN not_sym, simp]
  15.312 +declare sym [THEN succ_neq_0, elim!]
  15.313 +
  15.314 +(* succ(c) <= B ==> c : B *)
  15.315 +lemmas succ_subsetD = succI1 [THEN [2] subsetD]
  15.316 +
  15.317 +(* succ(b) ~= b *)
  15.318 +lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym, standard]
  15.319 +
  15.320 +lemma succ_inject_iff [simp]: "succ(m) = succ(n) <-> m=n"
  15.321 +by (blast elim: mem_asym elim!: equalityE)
  15.322 +
  15.323 +lemmas succ_inject = succ_inject_iff [THEN iffD1, standard, dest!]
  15.324 +
  15.325 +ML
  15.326 +{*
  15.327 +val Pow_bottom = thm "Pow_bottom";
  15.328 +val Pow_top = thm "Pow_top";
  15.329 +val Upair_iff = thm "Upair_iff";
  15.330 +val UpairI1 = thm "UpairI1";
  15.331 +val UpairI2 = thm "UpairI2";
  15.332 +val UpairE = thm "UpairE";
  15.333 +val Un_iff = thm "Un_iff";
  15.334 +val UnI1 = thm "UnI1";
  15.335 +val UnI2 = thm "UnI2";
  15.336 +val UnE = thm "UnE";
  15.337 +val UnE' = thm "UnE'";
  15.338 +val UnCI = thm "UnCI";
  15.339 +val Int_iff = thm "Int_iff";
  15.340 +val IntI = thm "IntI";
  15.341 +val IntD1 = thm "IntD1";
  15.342 +val IntD2 = thm "IntD2";
  15.343 +val IntE = thm "IntE";
  15.344 +val Diff_iff = thm "Diff_iff";
  15.345 +val DiffI = thm "DiffI";
  15.346 +val DiffD1 = thm "DiffD1";
  15.347 +val DiffD2 = thm "DiffD2";
  15.348 +val DiffE = thm "DiffE";
  15.349 +val cons_iff = thm "cons_iff";
  15.350 +val consI1 = thm "consI1";
  15.351 +val consI2 = thm "consI2";
  15.352 +val consE = thm "consE";
  15.353 +val consE' = thm "consE'";
  15.354 +val consCI = thm "consCI";
  15.355 +val cons_not_0 = thm "cons_not_0";
  15.356 +val cons_neq_0 = thm "cons_neq_0";
  15.357 +val singleton_iff = thm "singleton_iff";
  15.358 +val singletonI = thm "singletonI";
  15.359 +val singletonE = thm "singletonE";
  15.360 +val the_equality = thm "the_equality";
  15.361 +val the_equality2 = thm "the_equality2";
  15.362 +val theI = thm "theI";
  15.363 +val the_0 = thm "the_0";
  15.364 +val theI2 = thm "theI2";
  15.365 +val if_true = thm "if_true";
  15.366 +val if_false = thm "if_false";
  15.367 +val if_cong = thm "if_cong";
  15.368 +val if_weak_cong = thm "if_weak_cong";
  15.369 +val if_P = thm "if_P";
  15.370 +val if_not_P = thm "if_not_P";
  15.371 +val split_if = thm "split_if";
  15.372 +val split_if_eq1 = thm "split_if_eq1";
  15.373 +val split_if_eq2 = thm "split_if_eq2";
  15.374 +val split_if_mem1 = thm "split_if_mem1";
  15.375 +val split_if_mem2 = thm "split_if_mem2";
  15.376 +val if_iff = thm "if_iff";
  15.377 +val if_type = thm "if_type";
  15.378 +val mem_asym = thm "mem_asym";
  15.379 +val mem_irrefl = thm "mem_irrefl";
  15.380 +val mem_not_refl = thm "mem_not_refl";
  15.381 +val mem_imp_not_eq = thm "mem_imp_not_eq";
  15.382 +val succ_iff = thm "succ_iff";
  15.383 +val succI1 = thm "succI1";
  15.384 +val succI2 = thm "succI2";
  15.385 +val succE = thm "succE";
  15.386 +val succCI = thm "succCI";
  15.387 +val succ_not_0 = thm "succ_not_0";
  15.388 +val succ_neq_0 = thm "succ_neq_0";
  15.389 +val succ_subsetD = thm "succ_subsetD";
  15.390 +val succ_neq_self = thm "succ_neq_self";
  15.391 +val succ_inject_iff = thm "succ_inject_iff";
  15.392 +val succ_inject = thm "succ_inject";
  15.393 +
  15.394 +val split_ifs = thms "split_ifs";
  15.395 +*}
  15.396 +
  15.397  end