--- a/src/ZF/Arith.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Arith.ML Tue Jun 21 17:20:34 1994 +0200
@@ -42,7 +42,7 @@
(asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
val rec_type = result();
-val nat_le_refl = naturals_are_ordinals RS le_refl;
+val nat_le_refl = nat_into_Ord RS le_refl;
val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
@@ -113,7 +113,7 @@
by (ALLGOALS
(asm_simp_tac
(nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0,
- diff_succ_succ, naturals_are_ordinals]))));
+ diff_succ_succ, nat_into_Ord]))));
val diff_le_self = result();
(*** Simplification over add, mult, diff ***)
@@ -150,12 +150,21 @@
(*Commutative law for addition*)
val add_commute = prove_goal Arith.thy
- "[| m:nat; n:nat |] ==> m #+ n = n #+ m"
- (fn prems=>
- [ (nat_ind_tac "n" prems 1),
+ "!!m n. [| m:nat; n:nat |] ==> m #+ n = n #+ m"
+ (fn _ =>
+ [ (nat_ind_tac "n" [] 1),
(ALLGOALS
- (asm_simp_tac
- (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
+ (asm_simp_tac (arith_ss addsimps [add_0_right, add_succ_right]))) ]);
+
+val add_left_commute = prove_goal Arith.thy
+ "!!m n k. [| m:nat; n:nat; k:nat |] ==> m#+(n#+k)=n#+(m#+k)"
+ (fn _ => [rtac (add_commute RS trans) 1,
+ rtac (add_assoc RS trans) 3,
+ rtac (add_commute RS subst_context) 4,
+ REPEAT (ares_tac [add_type] 1)]);
+
+(*Addition is an AC-operator*)
+val add_ac = [add_assoc, add_commute, add_left_commute];
(*Cancellation law on the left*)
val [knat,eqn] = goal Arith.thy
@@ -170,20 +179,17 @@
(*right annihilation in product*)
val mult_0_right = prove_goal Arith.thy
- "m:nat ==> m #* 0 = 0"
- (fn prems=>
- [ (nat_ind_tac "m" prems 1),
- (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
+ "!!m. m:nat ==> m #* 0 = 0"
+ (fn _=>
+ [ (nat_ind_tac "m" [] 1),
+ (ALLGOALS (asm_simp_tac arith_ss)) ]);
(*right successor law for multiplication*)
val mult_succ_right = prove_goal Arith.thy
"!!m n. [| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
- (fn _=>
+ (fn _ =>
[ (nat_ind_tac "m" [] 1),
- (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
- (*The final goal requires the commutative law for addition*)
- (rtac (add_commute RS subst_context) 1),
- (REPEAT (assume_tac 1)) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps add_ac))) ]);
(*Commutative law for multiplication*)
val mult_commute = prove_goal Arith.thy
@@ -202,12 +208,11 @@
(*Distributive law on the left; requires an extra typing premise*)
val add_mult_distrib_left = prove_goal Arith.thy
- "[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
+ "!!m. [| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
(fn prems=>
- let val mult_commute' = read_instantiate [("m","k")] mult_commute
- val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
- in [ (simp_tac ss 1) ]
- end);
+ [ (nat_ind_tac "m" [] 1),
+ (asm_simp_tac (arith_ss addsimps [mult_0_right]) 1),
+ (asm_simp_tac (arith_ss addsimps ([mult_succ_right] @ add_ac)) 1) ]);
(*Associative law for multiplication*)
val mult_assoc = prove_goal Arith.thy
@@ -261,9 +266,9 @@
val div_rls = (*for mod and div*)
nat_typechecks @
[Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
- naturals_are_ordinals, not_lt_iff_le RS iffD1];
+ nat_into_Ord, not_lt_iff_le RS iffD1];
-val div_ss = ZF_ss addsimps [naturals_are_ordinals, div_termination RS ltD,
+val div_ss = ZF_ss addsimps [nat_into_Ord, div_termination RS ltD,
not_lt_iff_le RS iffD2];
(*Type checking depends upon termination!*)
@@ -311,7 +316,7 @@
by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2);
(*case n le x*)
by (asm_full_simp_tac
- (arith_ss addsimps [not_lt_iff_le, naturals_are_ordinals,
+ (arith_ss addsimps [not_lt_iff_le, nat_into_Ord,
mod_geq, div_geq, add_assoc,
div_termination RS ltD, add_diff_inverse]) 1);
val mod_div_equality = result();
@@ -350,7 +355,7 @@
val add_lt_mono = result();
(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
-val lt_mono::ford::prems = goal Ord.thy
+val lt_mono::ford::prems = goal Ordinal.thy
"[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
\ !!i. i:k ==> Ord(f(i)); \
\ i le j; j:k \
@@ -363,7 +368,7 @@
goal Arith.thy
"!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1);
-by (REPEAT (ares_tac [add_lt_mono1, add_type RS naturals_are_ordinals] 1));
+by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1));
val add_le_mono1 = result();
(* le monotonicity, BOTH arguments*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Cardinal.ML Tue Jun 21 17:20:34 1994 +0200
@@ -0,0 +1,352 @@
+(* Title: ZF/Cardinal.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Cardinals in Zermelo-Fraenkel Set Theory
+
+This theory does NOT assume the Axiom of Choice
+*)
+
+open Cardinal;
+
+(*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***)
+
+(** Lemma: Banach's Decomposition Theorem **)
+
+goal Cardinal.thy "bnd_mono(X, %W. X - g``(Y - f``W))";
+by (rtac bnd_monoI 1);
+by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1));
+val decomp_bnd_mono = result();
+
+val [gfun] = goal Cardinal.thy
+ "g: Y->X ==> \
+\ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \
+\ X - lfp(X, %W. X - g``(Y - f``W)) ";
+by (res_inst_tac [("P", "%u. ?v = X-u")]
+ (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1);
+by (simp_tac (ZF_ss addsimps [subset_refl, double_complement,
+ gfun RS fun_is_rel RS image_subset]) 1);
+val Banach_last_equation = result();
+
+val prems = goal Cardinal.thy
+ "[| f: X->Y; g: Y->X |] ==> \
+\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \
+\ (YA Int YB = 0) & (YA Un YB = Y) & \
+\ f``XA=YA & g``YB=XB";
+by (REPEAT
+ (FIRSTGOAL
+ (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition])));
+by (rtac Banach_last_equation 3);
+by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1));
+val decomposition = result();
+
+val prems = goal Cardinal.thy
+ "[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)";
+by (cut_facts_tac prems 1);
+by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1);
+by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un]
+ addIs [bij_converse_bij]) 1);
+(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))"
+ is forced by the context!! *)
+val schroeder_bernstein = result();
+
+
+(** Equipollence is an equivalence relation **)
+
+goalw Cardinal.thy [eqpoll_def] "X eqpoll X";
+br exI 1;
+br id_bij 1;
+val eqpoll_refl = result();
+
+goalw Cardinal.thy [eqpoll_def] "!!X Y. X eqpoll Y ==> Y eqpoll X";
+by (fast_tac (ZF_cs addIs [bij_converse_bij]) 1);
+val eqpoll_sym = result();
+
+goalw Cardinal.thy [eqpoll_def]
+ "!!X Y. [| X eqpoll Y; Y eqpoll Z |] ==> X eqpoll Z";
+by (fast_tac (ZF_cs addIs [comp_bij]) 1);
+val eqpoll_trans = result();
+
+(** Le-pollence is a partial ordering **)
+
+goalw Cardinal.thy [lepoll_def] "!!X Y. X<=Y ==> X lepoll Y";
+br exI 1;
+be id_subset_inj 1;
+val subset_imp_lepoll = result();
+
+val lepoll_refl = subset_refl RS subset_imp_lepoll;
+
+goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def]
+ "!!X Y. X eqpoll Y ==> X lepoll Y";
+by (fast_tac ZF_cs 1);
+val eqpoll_imp_lepoll = result();
+
+goalw Cardinal.thy [lepoll_def]
+ "!!X Y. [| X lepoll Y; Y lepoll Z |] ==> X lepoll Z";
+by (fast_tac (ZF_cs addIs [comp_inj]) 1);
+val lepoll_trans = result();
+
+(*Asymmetry law*)
+goalw Cardinal.thy [lepoll_def,eqpoll_def]
+ "!!X Y. [| X lepoll Y; Y lepoll X |] ==> X eqpoll Y";
+by (REPEAT (etac exE 1));
+by (rtac schroeder_bernstein 1);
+by (REPEAT (assume_tac 1));
+val eqpollI = result();
+
+val [major,minor] = goal Cardinal.thy
+ "[| X eqpoll Y; [| X lepoll Y; Y lepoll X |] ==> P |] ==> P";
+br minor 1;
+by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1));
+val eqpollE = result();
+
+goal Cardinal.thy "X eqpoll Y <-> X lepoll Y & Y lepoll X";
+by (fast_tac (ZF_cs addIs [eqpollI] addSEs [eqpollE]) 1);
+val eqpoll_iff = result();
+
+
+(** LEAST -- the least number operator [from HOL/Univ.ML] **)
+
+val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def]
+ "[| P(i); Ord(i); !!x. x<i ==> ~P(x) |] ==> (LEAST x.P(x)) = i";
+by (rtac the_equality 1);
+by (fast_tac (ZF_cs addSIs [premP,premOrd,premNot]) 1);
+by (REPEAT (etac conjE 1));
+be (premOrd RS Ord_linear_lt) 1;
+by (ALLGOALS (fast_tac (ZF_cs addSIs [premP] addSDs [premNot])));
+val Least_equality = result();
+
+goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> P(LEAST x.P(x))";
+by (etac rev_mp 1);
+by (trans_ind_tac "i" [] 1);
+by (rtac impI 1);
+by (rtac classical 1);
+by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]);
+by (assume_tac 2);
+by (fast_tac (ZF_cs addSEs [ltE]) 1);
+val LeastI = result();
+
+(*Proof is almost identical to the one above!*)
+goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> (LEAST x.P(x)) le i";
+by (etac rev_mp 1);
+by (trans_ind_tac "i" [] 1);
+by (rtac impI 1);
+by (rtac classical 1);
+by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]);
+by (etac le_refl 2);
+by (fast_tac (ZF_cs addEs [ltE, lt_trans1] addIs [leI, ltI]) 1);
+val Least_le = result();
+
+(*LEAST really is the smallest*)
+goal Cardinal.thy "!!i. [| P(i); i < (LEAST x.P(x)) |] ==> Q";
+br (Least_le RSN (2,lt_trans2) RS lt_anti_refl) 1;
+by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
+val less_LeastE = result();
+
+goal Cardinal.thy "Ord(LEAST x.P(x))";
+by (res_inst_tac [("Q","EX i. Ord(i) & P(i)")] (excluded_middle RS disjE) 1);
+by (safe_tac ZF_cs);
+br (Least_le RS ltE) 2;
+by (REPEAT_SOME assume_tac);
+bw Least_def;
+by (rtac (the_0 RS ssubst) 1 THEN rtac Ord_0 2);
+by (fast_tac FOL_cs 1);
+val Ord_Least = result();
+
+
+(** Basic properties of cardinals **)
+
+(*Not needed for simplification, but helpful below*)
+val prems = goal Cardinal.thy
+ "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x.P(x)) = (LEAST x.Q(x))";
+by (simp_tac (FOL_ss addsimps prems) 1);
+val Least_cong = result();
+
+(*Need AC to prove X lepoll Y ==> |X| le |Y| ; see well_ord_lepoll_imp_le *)
+goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|";
+br Least_cong 1;
+by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1);
+val cardinal_cong = result();
+
+(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
+goalw Cardinal.thy [eqpoll_def, cardinal_def]
+ "!!A. well_ord(A,r) ==> |A| eqpoll A";
+br LeastI 1;
+be Ord_ordertype 2;
+br exI 1;
+be (ordertype_bij RS bij_converse_bij) 1;
+val well_ord_cardinal_eqpoll = result();
+
+val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll
+ |> standard;
+
+goal Cardinal.thy
+ "!!X Y. [| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X eqpoll Y";
+br (eqpoll_sym RS eqpoll_trans) 1;
+be well_ord_cardinal_eqpoll 1;
+by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1);
+val well_ord_cardinal_eqE = result();
+
+
+(** Observations from Kunen, page 28 **)
+
+goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> |i| le i";
+be (eqpoll_refl RS Least_le) 1;
+val Ord_cardinal_le = result();
+
+goalw Cardinal.thy [Card_def] "!!i. Card(i) ==> |i| = i";
+be sym 1;
+val Card_cardinal_eq = result();
+
+val prems = goalw Cardinal.thy [Card_def,cardinal_def]
+ "[| Ord(i); !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)";
+br (Least_equality RS ssubst) 1;
+by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1));
+val CardI = result();
+
+goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)";
+be ssubst 1;
+br Ord_Least 1;
+val Card_is_Ord = result();
+
+goalw Cardinal.thy [cardinal_def] "Ord( |i| )";
+br Ord_Least 1;
+val Ord_cardinal = result();
+
+(*Kunen's Lemma 10.5*)
+goal Cardinal.thy "!!i j. [| |i| le j; j le i |] ==> |j| = |i|";
+br (eqpollI RS cardinal_cong) 1;
+be (le_imp_subset RS subset_imp_lepoll) 1;
+br lepoll_trans 1;
+be (le_imp_subset RS subset_imp_lepoll) 2;
+br (eqpoll_sym RS eqpoll_imp_lepoll) 1;
+br Ord_cardinal_eqpoll 1;
+by (REPEAT (eresolve_tac [ltE, Ord_succD] 1));
+val cardinal_eq_lemma = result();
+
+goal Cardinal.thy "!!i j. i le j ==> |i| le |j|";
+by (res_inst_tac [("i","|i|"),("j","|j|")] Ord_linear_le 1);
+by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));
+br cardinal_eq_lemma 1;
+ba 2;
+be le_trans 1;
+be ltE 1;
+be Ord_cardinal_le 1;
+val cardinal_mono = result();
+
+(*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*)
+goal Cardinal.thy "!!i j. [| |i| < |j|; Ord(i); Ord(j) |] ==> i < j";
+br Ord_linear2 1;
+by (REPEAT_SOME assume_tac);
+be (lt_trans2 RS lt_anti_refl) 1;
+be cardinal_mono 1;
+val cardinal_lt_imp_lt = result();
+
+goal Cardinal.thy "!!i j. [| |i| < k; Ord(i); Card(k) |] ==> i < k";
+by (asm_simp_tac (ZF_ss addsimps
+ [cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1);
+val Card_lt_imp_lt = result();
+
+
+(** The swap operator [NOT USED] **)
+
+goalw Cardinal.thy [swap_def]
+ "!!A. [| x:A; y:A |] ==> swap(A,x,y) : A->A";
+by (REPEAT (ares_tac [lam_type,if_type] 1));
+val swap_type = result();
+
+goalw Cardinal.thy [swap_def]
+ "!!A. [| x:A; y:A; z:A |] ==> swap(A,x,y)`(swap(A,x,y)`z) = z";
+by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
+val swap_swap_identity = result();
+
+goal Cardinal.thy "!!A. [| x:A; y:A |] ==> swap(A,x,y) : bij(A,A)";
+br nilpotent_imp_bijective 1;
+by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2,
+ ballI, swap_swap_identity] 1));
+val swap_bij = result();
+
+(*** The finite cardinals ***)
+
+(*Lemma suggested by Mike Fourman*)
+val [prem] = goalw Cardinal.thy [inj_def]
+ "f: inj(succ(m), succ(n)) ==> (lam x:m. if(f`x=n, f`m, f`x)) : inj(m,n)";
+br CollectI 1;
+(*Proving it's in the function space m->n*)
+by (cut_facts_tac [prem] 1);
+br (if_type RS lam_type) 1;
+by (fast_tac (ZF_cs addSEs [mem_anti_refl] addEs [apply_funtype RS succE]) 1);
+by (fast_tac (ZF_cs addSEs [mem_anti_refl] addEs [apply_funtype RS succE]) 1);
+(*Proving it's injective*)
+by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
+(*Adding prem earlier would cause the simplifier to loop*)
+by (cut_facts_tac [prem] 1);
+by (fast_tac (ZF_cs addSEs [mem_anti_refl]) 1);
+val inj_succ_succD = result();
+
+val [prem] = goalw Cardinal.thy [lepoll_def]
+ "m:nat ==> ALL n: nat. m lepoll n --> m le n";
+by (nat_ind_tac "m" [prem] 1);
+by (fast_tac (ZF_cs addSIs [nat_0_le]) 1);
+br ballI 1;
+by (eres_inst_tac [("n","n")] natE 1);
+by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1);
+by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [inj_succ_succD]) 1);
+val nat_lepoll_imp_le_lemma = result();
+val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp |> standard;
+
+goal Cardinal.thy
+ "!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
+br iffI 1;
+by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2);
+by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_asym] addSEs [eqpollE]) 1);
+val nat_eqpoll_iff = result();
+
+goalw Cardinal.thy [Card_def,cardinal_def]
+ "!!n. n: nat ==> Card(n)";
+br (Least_equality RS ssubst) 1;
+by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl]));
+by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1);
+by (fast_tac (ZF_cs addSEs [lt_anti_refl]) 1);
+val nat_into_Card = result();
+
+val Card_0 = nat_0I RS nat_into_Card;
+
+(*Part of Kunen's Lemma 10.6*)
+goal Cardinal.thy "!!n. [| succ(n) lepoll n; n:nat |] ==> P";
+br (nat_lepoll_imp_le RS lt_anti_refl) 1;
+by (REPEAT (ares_tac [nat_succI] 1));
+val succ_lepoll_natE = result();
+
+
+(*** The first infinite cardinal: Omega, or nat ***)
+
+(*This implies Kunen's Lemma 10.6*)
+goal Cardinal.thy "!!n. [| n<i; n:nat |] ==> ~ i lepoll n";
+br notI 1;
+by (rtac succ_lepoll_natE 1 THEN assume_tac 2);
+by (rtac lepoll_trans 1 THEN assume_tac 2);
+be ltE 1;
+by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1));
+val lt_not_lepoll = result();
+
+goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)";
+br (Least_equality RS ssubst) 1;
+by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl]));
+be ltE 1;
+by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1);
+val Card_nat = result();
+
+goal Cardinal.thy "!!i n. [| Ord(i); n:nat |] ==> i eqpoll n <-> i=n";
+br iffI 1;
+by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2);
+by (rtac Ord_linear_lt 1);
+by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord]));
+by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN
+ REPEAT (assume_tac 1));
+by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1)));
+be eqpoll_imp_lepoll 1;
+val Ord_nat_eqpoll_iff = result();
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Cardinal.thy Tue Jun 21 17:20:34 1994 +0200
@@ -0,0 +1,33 @@
+(* Title: ZF/Cardinal.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Cardinals in Zermelo-Fraenkel Set Theory
+*)
+
+Cardinal = OrderType + Fixedpt + Nat + Sum +
+consts
+ Least :: "(i=>o) => i" (binder "LEAST " 10)
+ eqpoll, lepoll :: "[i,i] => o" (infixl 50)
+ "cardinal" :: "i=>i" ("|_|")
+ Card :: "i=>o"
+
+ swap :: "[i,i,i]=>i" (*not used; useful??*)
+
+rules
+
+ (*least ordinal operator*)
+ Least_def "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
+
+ eqpoll_def "A eqpoll B == EX f. f: bij(A,B)"
+
+ lepoll_def "A lepoll B == EX f. f: inj(A,B)"
+
+ cardinal_def "|A| == LEAST i. i eqpoll A"
+
+ Card_def "Card(i) == ( i = |i| )"
+
+ swap_def "swap(A,x,y) == (lam z:A. if(z=x, y, if(z=y, x, z)))"
+
+end
--- a/src/ZF/Fin.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Fin.ML Tue Jun 21 17:20:34 1994 +0200
@@ -1,12 +1,10 @@
-(* Title: ZF/ex/fin.ML
+(* Title: ZF/ex/Fin.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Finite powerset operator
-could define cardinality?
-
prove X:Fin(A) ==> EX n:nat. EX f. f:bij(X,n)
card(0)=0
[| a~:b; b: Fin(A) |] ==> card(cons(a,b)) = succ(card(b))
--- a/src/ZF/Fin.thy Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Fin.thy Tue Jun 21 17:20:34 1994 +0200
@@ -1,3 +1,3 @@
(*Dummy theory to document dependencies *)
-fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities"
+Fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities"
--- a/src/ZF/List.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/List.ML Tue Jun 21 17:20:34 1994 +0200
@@ -1,4 +1,4 @@
-(* Title: ZF/list.ML
+(* Title: ZF/List.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -36,6 +36,14 @@
rename_last_tac a ["1"] (i+2),
ares_tac prems i];
+goal List.thy "list(A) = {0} + (A * list(A))";
+by (rtac (List.unfold RS trans) 1);
+bws List.con_defs;
+by (fast_tac (sum_cs addIs ([equalityI] @ datatype_intrs)
+ addDs [List.dom_subset RS subsetD]
+ addEs [A_into_univ]) 1);
+val list_unfold = result();
+
(** Lemmas to justify using "list" in other recursive type definitions **)
goalw List.thy List.defs "!!A B. A<=B ==> list(A) <= list(B)";
@@ -54,6 +62,10 @@
val list_subset_univ = standard ([list_mono, list_univ] MRS subset_trans);
+goal List.thy "!!l A B. [| l: list(A); A <= univ(B) |] ==> l: univ(B)";
+by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
+val list_into_univ = result();
+
val major::prems = goal List.thy
"[| l: list(A); \
\ c: C(Nil); \
--- a/src/ZF/List.thy Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/List.thy Tue Jun 21 17:20:34 1994 +0200
@@ -1,3 +1,3 @@
(*Dummy theory to document dependencies *)
-list = Univ + "Datatype" + "intr_elim"
+List = Univ + "Datatype" + "intr_elim"
--- a/src/ZF/Makefile Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Makefile Tue Jun 21 17:20:34 1994 +0200
@@ -22,8 +22,11 @@
func.ML simpdata.ML Bool.thy Bool.ML \
Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \
ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \
- equalities.ML Perm.thy Perm.ML Trancl.thy Trancl.ML \
- WF.thy WF.ML Ord.thy Ord.ML Nat.thy Nat.ML \
+ equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \
+ WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \
+ OrderType.thy OrderType.ML OrderArith.thy OrderArith.ML \
+ Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \
+ Nat.thy Nat.ML \
Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
QUniv.thy QUniv.ML constructor.ML Datatype.ML \
Fin.ML List.ML ListFn.thy ListFn.ML
@@ -44,7 +47,8 @@
poly*) cp $(BIN)/FOL $(BIN)/ZF;\
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\
- *) echo Bad value for ISABELLECOMP;;\
+ *) echo Bad value for ISABELLECOMP: \
+ $(COMP) is not poly or sml;;\
esac
$(BIN)/FOL:
@@ -54,7 +58,8 @@
case "$(COMP)" in \
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/ZF ;;\
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/ZF;;\
- *) echo Bad value for ISABELLECOMP;;\
+ *) echo Bad value for ISABELLECOMP: \
+ $(COMP) is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/FOL $(BIN)/ZF
--- a/src/ZF/Nat.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Nat.ML Tue Jun 21 17:20:34 1994 +0200
@@ -68,10 +68,12 @@
val prems = goal Nat.thy "n: nat ==> Ord(n)";
by (nat_ind_tac "n" prems 1);
by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));
-val naturals_are_ordinals = result();
+val nat_into_Ord = result();
(* i: nat ==> 0 le i *)
-val nat_0_le = naturals_are_ordinals RS Ord_0_le;
+val nat_0_le = nat_into_Ord RS Ord_0_le;
+
+val nat_le_refl = nat_into_Ord RS le_refl;
goal Nat.thy "!!n. n: nat ==> n=0 | 0:n";
by (etac nat_induct 1);
@@ -81,18 +83,23 @@
goal Nat.thy "Ord(nat)";
by (rtac OrdI 1);
-by (etac (naturals_are_ordinals RS Ord_is_Transset) 2);
+by (etac (nat_into_Ord RS Ord_is_Transset) 2);
by (rewtac Transset_def);
by (rtac ballI 1);
by (etac nat_induct 1);
by (REPEAT (ares_tac [empty_subsetI,succ_subsetI] 1));
val Ord_nat = result();
+goalw Nat.thy [Limit_def] "Limit(nat)";
+by (safe_tac (ZF_cs addSIs [ltI, nat_0I, nat_1I, nat_succI, Ord_nat]));
+by (etac ltD 1);
+val Limit_nat = result();
+
(* succ(i): nat ==> i: nat *)
val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans;
(* [| succ(i): k; k: nat |] ==> i: k *)
-val succ_in_naturalD = [succI1, asm_rl, naturals_are_ordinals] MRS Ord_trans;
+val succ_in_naturalD = [succI1, asm_rl, nat_into_Ord] MRS Ord_trans;
goal Nat.thy "!!m n. [| m<n; n: nat |] ==> m: nat";
by (etac ltE 1);
--- a/src/ZF/Nat.thy Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Nat.thy Tue Jun 21 17:20:34 1994 +0200
@@ -1,12 +1,12 @@
-(* Title: ZF/nat.thy
+(* Title: ZF/Nat.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
+ Copyright 1994 University of Cambridge
Natural numbers in Zermelo-Fraenkel Set Theory
*)
-Nat = Ord + Bool + "mono" +
+Nat = Ordinal + Bool + "mono" +
consts
nat :: "i"
nat_case :: "[i, i=>i, i]=>i"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Order.ML Tue Jun 21 17:20:34 1994 +0200
@@ -0,0 +1,185 @@
+(* Title: ZF/Order.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+For Order.thy. Orders in Zermelo-Fraenkel Set Theory
+*)
+
+(*TO PURE/TACTIC.ML*)
+fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
+
+
+open Order;
+
+val bij_apply_cs = ZF_cs addSEs [bij_converse_bij]
+ addIs [bij_is_fun, apply_type];
+
+val bij_inverse_ss =
+ ZF_ss addsimps [bij_is_fun RS apply_type,
+ bij_converse_bij RS bij_is_fun RS apply_type,
+ left_inverse_bij, right_inverse_bij];
+
+(** Basic properties of the definitions **)
+
+(*needed????*)
+goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, asym_def]
+ "!!r. part_ord(A,r) ==> asym(r Int A*A)";
+by (fast_tac ZF_cs 1);
+val part_ord_Imp_asym = result();
+
+(** Order-isomorphisms **)
+
+goalw Order.thy [ord_iso_def]
+ "!!f. f: ord_iso(A,r,B,s) ==> f: bij(A,B)";
+by (etac CollectD1 1);
+val ord_iso_is_bij = result();
+
+goalw Order.thy [ord_iso_def]
+ "!!f. [| f: ord_iso(A,r,B,s); <x,y>: r; x:A; y:A |] ==> \
+\ <f`x, f`y> : s";
+by (fast_tac ZF_cs 1);
+val ord_iso_apply = result();
+
+goalw Order.thy [ord_iso_def]
+ "!!f. [| f: ord_iso(A,r,B,s); <x,y>: s; x:B; y:B |] ==> \
+\ <converse(f) ` x, converse(f) ` y> : r";
+be CollectE 1;
+be (bspec RS bspec RS iffD2) 1;
+by (REPEAT (eresolve_tac [asm_rl,
+ bij_converse_bij RS bij_is_fun RS apply_type] 1));
+by (asm_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1);
+val ord_iso_converse = result();
+
+val major::premx::premy::prems = goalw Order.thy [linear_def]
+ "[| linear(A,r); x:A; y:A; \
+\ <x,y>:r ==> P; x=y ==> P; <y,x>:r ==> P |] ==> P";
+by (cut_facts_tac [major,premx,premy] 1);
+by (REPEAT_FIRST (eresolve_tac [ballE,disjE]));
+by (EVERY1 (map etac prems));
+by (ALLGOALS contr_tac);
+val linearE = result();
+
+(*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*)
+val linear_case_tac =
+ SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1,
+ REPEAT_SOME assume_tac]);
+
+(*Inductive argument for proving Kunen's Lemma 6.1*)
+goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def, pred_def]
+ "!!r. [| well_ord(A,r); x: A; f: ord_iso(A, r, pred(A,x,r), r); y: A |] \
+\ ==> f`y = y";
+by (safe_tac ZF_cs);
+by (wf_on_ind_tac "y" [] 1);
+by (forward_tac [ord_iso_is_bij] 1);
+by (subgoal_tac "f`y1 : {y: A . <y, x> : r}" 1);
+by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type]) 2);
+(*Now we know f`y1 : A and <f`y1, x> : r *)
+by (etac CollectE 1);
+by (linear_case_tac 1);
+(*Case <f`y1, y1> : r *) (*use induction hyp*)
+by (dtac bspec 1 THEN mp_tac 2 THEN assume_tac 1);
+by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1);
+by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1);
+(*The case <y1, f`y1> : r *)
+by (subgoal_tac "<y1,x> : r" 1);
+by (fast_tac (ZF_cs addSEs [trans_onD]) 2);
+by (dtac ord_iso_converse 1 THEN assume_tac 1 THEN fast_tac ZF_cs 2);
+by (fast_tac ZF_cs 1);
+by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1);
+(*now use induction hyp*)
+by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1);
+by (dres_inst_tac [("t", "op `(f)")] subst_context 1);
+by (asm_full_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1);
+val not_well_ord_iso_pred_lemma = result();
+
+
+(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
+ of a well-ordering*)
+goal Order.thy
+ "!!r. [| well_ord(A,r); x:A |] ==> \
+\ ALL f. f ~: ord_iso(A, r, pred(A,x,r), r)";
+by (safe_tac ZF_cs);
+by (metacut_tac not_well_ord_iso_pred_lemma 1);
+by (REPEAT_SOME assume_tac);
+(*Now we know f`x = x*)
+by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type),
+ assume_tac]);
+(*Now we know f`x : pred(A,x,r) *)
+by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, pred_def]) 1);
+by (fast_tac (ZF_cs addSEs [wf_on_not_refl RS notE]) 1);
+val not_well_ord_iso_pred = result();
+
+
+(*Inductive argument for proving Kunen's Lemma 6.2*)
+goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def]
+ "!!r. [| well_ord(A,r); well_ord(B,s); \
+\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s); y: A |] \
+\ ==> f`y = g`y";
+by (safe_tac ZF_cs);
+by (wf_on_ind_tac "y" [] 1);
+by (subgoals_tac ["f: bij(A,B)", "g: bij(A,B)", "f`y1 : B", "g`y1 : B"] 1);
+by (REPEAT (fast_tac (bij_apply_cs addSEs [ord_iso_is_bij]) 2));
+by (linear_case_tac 1);
+(*The case <f`y1, g`y1> : s *)
+by (forw_inst_tac [("f","g")] ord_iso_converse 1 THEN REPEAT (assume_tac 1));
+by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1);
+by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1);
+by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1);
+by (dres_inst_tac [("t", "op `(g)")] subst_context 1);
+by (asm_full_simp_tac bij_inverse_ss 1);
+(*The case <g`y1, f`y1> : s *)
+by (forw_inst_tac [("f","f")] ord_iso_converse 1 THEN REPEAT (assume_tac 1));
+by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1);
+by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1);
+by (dres_inst_tac [("t", "op `(converse(g))")] subst_context 1);
+by (dres_inst_tac [("t", "op `(f)")] subst_context 1);
+by (asm_full_simp_tac bij_inverse_ss 1);
+val well_ord_iso_unique_lemma = result();
+
+
+(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
+goal Order.thy
+ "!!r. [| well_ord(A,r); well_ord(B,s); \
+\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s) |] ==> f = g";
+br fun_extension 1;
+be (ord_iso_is_bij RS bij_is_fun) 1;
+be (ord_iso_is_bij RS bij_is_fun) 1;
+br well_ord_iso_unique_lemma 1;
+by (REPEAT_SOME assume_tac);
+val well_ord_iso_unique = result();
+
+
+goalw Order.thy [irrefl_def, part_ord_def, tot_ord_def,
+ trans_on_def, well_ord_def]
+ "!!r. [| wf[A](r); linear(A,r) |] ==> well_ord(A,r)";
+by (asm_simp_tac (ZF_ss addsimps [wf_on_not_refl]) 1);
+by (safe_tac ZF_cs);
+by (linear_case_tac 1);
+(*case x=xb*)
+by (fast_tac (ZF_cs addSEs [wf_on_anti_sym]) 1);
+(*case x<xb*)
+by (fast_tac (ZF_cs addSEs [wf_on_chain3]) 1);
+val well_ordI = result();
+
+goalw Order.thy [well_ord_def]
+ "!!r. well_ord(A,r) ==> wf[A](r)";
+by (safe_tac ZF_cs);
+val well_ord_is_wf = result();
+
+
+(*** Derived rules for pred(A,x,r) ***)
+
+val [major,minor] = goalw Order.thy [pred_def]
+ "[| y: pred(A,x,r); [| y:A; <y,x>:r |] ==> P |] ==> P";
+br (major RS CollectE) 1;
+by (REPEAT (ares_tac [minor] 1));
+val predE = result();
+
+goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}";
+by (fast_tac ZF_cs 1);
+val pred_subset_under = result();
+
+goalw Order.thy [pred_def] "pred(A,x,r) <= A";
+by (fast_tac ZF_cs 1);
+val pred_subset = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Order.thy Tue Jun 21 17:20:34 1994 +0200
@@ -0,0 +1,31 @@
+(* Title: ZF/Order.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Orders in Zermelo-Fraenkel Set Theory
+*)
+
+Order = WF + Perm +
+consts
+ part_ord :: "[i,i]=>o" (*Strict partial ordering*)
+ linear, tot_ord :: "[i,i]=>o" (*Strict total ordering*)
+ well_ord :: "[i,i]=>o" (*Well-ordering*)
+ ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*)
+ pred :: "[i,i,i]=>i" (*Set of predecessors*)
+
+rules
+ part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
+
+ linear_def "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
+
+ tot_ord_def "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
+
+ well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
+
+ ord_iso_def "ord_iso(A,r,B,s) == \
+\ {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
+
+ pred_def "pred(A,x,r) == {y:A. <y,x>:r}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/OrderType.ML Tue Jun 21 17:20:34 1994 +0200
@@ -0,0 +1,132 @@
+(* Title: ZF/OrderType.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+For OrderType.thy. Order types in Zermelo-Fraenkel Set Theory
+*)
+
+
+(*Requires Ordinal.thy as parent; otherwise could be in Order.ML*)
+goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
+br well_ordI 1;
+br (wf_Memrel RS wf_imp_wf_on) 1;
+by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1);
+by (REPEAT (resolve_tac [ballI, Ord_linear] 1));;
+by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));;
+val well_ord_Memrel = result();
+
+open OrderType;
+
+(** Unfolding of ordermap **)
+
+goalw OrderType.thy [ordermap_def, pred_def]
+ "!!r. [| wf[A](r); x:A |] ==> \
+\ ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
+by (asm_simp_tac ZF_ss 1);
+be (wfrec_on RS trans) 1;
+ba 1;
+by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam,
+ vimage_singleton_iff]) 1);
+val ordermap_pred_unfold = result();
+
+(*pred-unfolded version. NOT suitable for rewriting -- loops!*)
+val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold;
+
+goalw OrderType.thy [ordermap_def,ordertype_def]
+ "ordermap(A,r) : A -> ordertype(A,r)";
+br lam_type 1;
+by (rtac (lamI RS imageI) 1);
+by (REPEAT (assume_tac 1));
+val ordermap_type = result();
+
+(** Showing that ordermap, ordertype yield ordinals **)
+
+fun ordermap_elim_tac i =
+ EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i,
+ assume_tac (i+1),
+ assume_tac i];
+
+goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def]
+ "!!r. [| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)";
+by (safe_tac ZF_cs);
+by (wf_on_ind_tac "x" [] 1);
+by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1);
+by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
+bws [pred_def,Transset_def];
+by (fast_tac ZF_cs 2);
+by (safe_tac ZF_cs);
+by (ordermap_elim_tac 1);
+by (fast_tac (ZF_cs addSEs [trans_onD]) 1);
+val Ord_ordermap = result();
+
+goalw OrderType.thy [ordertype_def]
+ "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
+by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1);
+by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
+by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2);
+bws [Transset_def,well_ord_def];
+by (safe_tac ZF_cs);
+by (ordermap_elim_tac 1);
+by (fast_tac ZF_cs 1);
+val Ord_ordertype = result();
+
+(** ordermap preserves the orderings in both directions **)
+
+goal OrderType.thy
+ "!!r. [| <w,x>: r; wf[A](r); w: A; x: A |] ==> \
+\ ordermap(A,r)`w : ordermap(A,r)`x";
+by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
+ba 1;
+by (fast_tac ZF_cs 1);
+val less_imp_ordermap_in = result();
+
+(*linearity of r is crucial here*)
+goalw OrderType.thy [well_ord_def, tot_ord_def]
+ "!!r. [| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \
+\ w: A; x: A |] ==> <w,x>: r";
+by (safe_tac ZF_cs);
+by (linear_case_tac 1);
+by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1);
+bd less_imp_ordermap_in 1;
+by (REPEAT_SOME assume_tac);
+be mem_anti_sym 1;
+ba 1;
+val ordermap_in_imp_less = result();
+
+val ordermap_surj =
+ (ordermap_type RS surj_image) |>
+ rewrite_rule [symmetric ordertype_def] |>
+ standard;
+
+goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
+ "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
+by (safe_tac ZF_cs);
+br ordermap_type 1;
+br ordermap_surj 2;
+by (linear_case_tac 1);
+(*The two cases yield similar contradictions*)
+by (ALLGOALS (dtac less_imp_ordermap_in));
+by (REPEAT_SOME assume_tac);
+by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl])));
+val ordertype_bij = result();
+
+goalw OrderType.thy [ord_iso_def]
+ "!!r. well_ord(A,r) ==> \
+\ ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
+by (safe_tac ZF_cs);
+br ordertype_bij 1;
+ba 1;
+by (fast_tac (ZF_cs addSEs [MemrelE, ordermap_in_imp_less]) 2);
+bw well_ord_def;
+by (fast_tac (ZF_cs addSIs [MemrelI, less_imp_ordermap_in,
+ ordermap_type RS apply_type]) 1);
+val ordertype_ord_iso = result();
+
+
+(** Unfolding of ordertype **)
+
+goalw OrderType.thy [ordertype_def]
+ "ordertype(A,r) = {ordermap(A,r)`y . y : A}";
+by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);
+val ordertype_unfold = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/OrderType.thy Tue Jun 21 17:20:34 1994 +0200
@@ -0,0 +1,22 @@
+(* Title: ZF/OrderType.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Order types.
+
+The order type of a well-ordering is the least ordinal isomorphic to it.
+*)
+
+OrderType = Order + Ordinal +
+consts
+ ordermap :: "[i,i]=>i"
+ ordertype :: "[i,i]=>i"
+
+rules
+ ordermap_def
+ "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
+
+ ordertype_def "ordertype(A,r) == ordermap(A,r)``A"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Ordinal.ML Tue Jun 21 17:20:34 1994 +0200
@@ -0,0 +1,619 @@
+(* Title: ZF/Ordinal.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+For Ordinal.thy. Ordinals in Zermelo-Fraenkel Set Theory
+*)
+
+open Ordinal;
+
+(*** Rules for Transset ***)
+
+(** Two neat characterisations of Transset **)
+
+goalw Ordinal.thy [Transset_def] "Transset(A) <-> A<=Pow(A)";
+by (fast_tac ZF_cs 1);
+val Transset_iff_Pow = result();
+
+goalw Ordinal.thy [Transset_def] "Transset(A) <-> Union(succ(A)) = A";
+by (fast_tac (eq_cs addSEs [equalityE]) 1);
+val Transset_iff_Union_succ = result();
+
+(** Consequences of downwards closure **)
+
+goalw Ordinal.thy [Transset_def]
+ "!!C a b. [| Transset(C); {a,b}: C |] ==> a:C & b: C";
+by (fast_tac ZF_cs 1);
+val Transset_doubleton_D = result();
+
+val [prem1,prem2] = goalw Ordinal.thy [Pair_def]
+ "[| Transset(C); <a,b>: C |] ==> a:C & b: C";
+by (cut_facts_tac [prem2] 1);
+by (fast_tac (ZF_cs addSDs [prem1 RS Transset_doubleton_D]) 1);
+val Transset_Pair_D = result();
+
+val prem1::prems = goal Ordinal.thy
+ "[| Transset(C); A*B <= C; b: B |] ==> A <= C";
+by (cut_facts_tac prems 1);
+by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1);
+val Transset_includes_domain = result();
+
+val prem1::prems = goal Ordinal.thy
+ "[| Transset(C); A*B <= C; a: A |] ==> B <= C";
+by (cut_facts_tac prems 1);
+by (fast_tac (ZF_cs addSDs [prem1 RS Transset_Pair_D]) 1);
+val Transset_includes_range = result();
+
+val [prem1,prem2] = goalw (merge_theories(Ordinal.thy,Sum.thy)) [sum_def]
+ "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
+by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1);
+by (REPEAT (etac (prem1 RS Transset_includes_range) 1
+ ORELSE resolve_tac [conjI, singletonI] 1));
+val Transset_includes_summands = result();
+
+val [prem] = goalw (merge_theories(Ordinal.thy,Sum.thy)) [sum_def]
+ "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
+by (rtac (Int_Un_distrib RS ssubst) 1);
+by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);
+val Transset_sum_Int_subset = result();
+
+(** Closure properties **)
+
+goalw Ordinal.thy [Transset_def] "Transset(0)";
+by (fast_tac ZF_cs 1);
+val Transset_0 = result();
+
+goalw Ordinal.thy [Transset_def]
+ "!!i j. [| Transset(i); Transset(j) |] ==> Transset(i Un j)";
+by (fast_tac ZF_cs 1);
+val Transset_Un = result();
+
+goalw Ordinal.thy [Transset_def]
+ "!!i j. [| Transset(i); Transset(j) |] ==> Transset(i Int j)";
+by (fast_tac ZF_cs 1);
+val Transset_Int = result();
+
+goalw Ordinal.thy [Transset_def] "!!i. Transset(i) ==> Transset(succ(i))";
+by (fast_tac ZF_cs 1);
+val Transset_succ = result();
+
+goalw Ordinal.thy [Transset_def] "!!i. Transset(i) ==> Transset(Pow(i))";
+by (fast_tac ZF_cs 1);
+val Transset_Pow = result();
+
+goalw Ordinal.thy [Transset_def] "!!A. Transset(A) ==> Transset(Union(A))";
+by (fast_tac ZF_cs 1);
+val Transset_Union = result();
+
+val [Transprem] = goalw Ordinal.thy [Transset_def]
+ "[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))";
+by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1);
+val Transset_Union_family = result();
+
+val [prem,Transprem] = goalw Ordinal.thy [Transset_def]
+ "[| j:A; !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))";
+by (cut_facts_tac [prem] 1);
+by (fast_tac (ZF_cs addEs [Transprem RS bspec RS subsetD]) 1);
+val Transset_Inter_family = result();
+
+(*** Natural Deduction rules for Ord ***)
+
+val prems = goalw Ordinal.thy [Ord_def]
+ "[| Transset(i); !!x. x:i ==> Transset(x) |] ==> Ord(i) ";
+by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
+val OrdI = result();
+
+val [major] = goalw Ordinal.thy [Ord_def]
+ "Ord(i) ==> Transset(i)";
+by (rtac (major RS conjunct1) 1);
+val Ord_is_Transset = result();
+
+val [major,minor] = goalw Ordinal.thy [Ord_def]
+ "[| Ord(i); j:i |] ==> Transset(j) ";
+by (rtac (minor RS (major RS conjunct2 RS bspec)) 1);
+val Ord_contains_Transset = result();
+
+(*** Lemmas for ordinals ***)
+
+goalw Ordinal.thy [Ord_def,Transset_def] "!!i j.[| Ord(i); j:i |] ==> Ord(j)";
+by (fast_tac ZF_cs 1);
+val Ord_in_Ord = result();
+
+(* Ord(succ(j)) ==> Ord(j) *)
+val Ord_succD = succI1 RSN (2, Ord_in_Ord);
+
+goal Ordinal.thy "!!i j. [| Ord(i); Transset(j); j<=i |] ==> Ord(j)";
+by (REPEAT (ares_tac [OrdI] 1
+ ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1));
+val Ord_subset_Ord = result();
+
+goalw Ordinal.thy [Ord_def,Transset_def] "!!i j. [| j:i; Ord(i) |] ==> j<=i";
+by (fast_tac ZF_cs 1);
+val OrdmemD = result();
+
+goal Ordinal.thy "!!i j k. [| i:j; j:k; Ord(k) |] ==> i:k";
+by (REPEAT (ares_tac [OrdmemD RS subsetD] 1));
+val Ord_trans = result();
+
+goal Ordinal.thy "!!i j. [| i:j; Ord(j) |] ==> succ(i) <= j";
+by (REPEAT (ares_tac [OrdmemD RSN (2,succ_subsetI)] 1));
+val Ord_succ_subsetI = result();
+
+
+(*** The construction of ordinals: 0, succ, Union ***)
+
+goal Ordinal.thy "Ord(0)";
+by (REPEAT (ares_tac [OrdI,Transset_0] 1 ORELSE etac emptyE 1));
+val Ord_0 = result();
+
+goal Ordinal.thy "!!i. Ord(i) ==> Ord(succ(i))";
+by (REPEAT (ares_tac [OrdI,Transset_succ] 1
+ ORELSE eresolve_tac [succE,ssubst,Ord_is_Transset,
+ Ord_contains_Transset] 1));
+val Ord_succ = result();
+
+goal Ordinal.thy "Ord(succ(i)) <-> Ord(i)";
+by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1);
+val Ord_succ_iff = result();
+
+goalw Ordinal.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Un j)";
+by (fast_tac (ZF_cs addSIs [Transset_Un]) 1);
+val Ord_Un = result();
+
+goalw Ordinal.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Int j)";
+by (fast_tac (ZF_cs addSIs [Transset_Int]) 1);
+val Ord_Int = result();
+
+val nonempty::prems = goal Ordinal.thy
+ "[| j:A; !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
+by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);
+by (rtac Ord_is_Transset 1);
+by (REPEAT (ares_tac ([Ord_contains_Transset,nonempty]@prems) 1
+ ORELSE etac InterD 1));
+val Ord_Inter = result();
+
+val jmemA::prems = goal Ordinal.thy
+ "[| j:A; !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))";
+by (rtac (jmemA RS RepFunI RS Ord_Inter) 1);
+by (etac RepFunE 1);
+by (etac ssubst 1);
+by (eresolve_tac prems 1);
+val Ord_INT = result();
+
+(*There is no set of all ordinals, for then it would contain itself*)
+goal Ordinal.thy "~ (ALL i. i:X <-> Ord(i))";
+by (rtac notI 1);
+by (forw_inst_tac [("x", "X")] spec 1);
+by (safe_tac (ZF_cs addSEs [mem_anti_refl]));
+by (swap_res_tac [Ord_is_Transset RSN (2,OrdI)] 1);
+by (fast_tac ZF_cs 2);
+bw Transset_def;
+by (safe_tac ZF_cs);
+by (asm_full_simp_tac ZF_ss 1);
+by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
+val ON_class = result();
+
+(*** < is 'less than' for ordinals ***)
+
+goalw Ordinal.thy [lt_def] "!!i j. [| i:j; Ord(j) |] ==> i<j";
+by (REPEAT (ares_tac [conjI] 1));
+val ltI = result();
+
+val major::prems = goalw Ordinal.thy [lt_def]
+ "[| i<j; [| i:j; Ord(i); Ord(j) |] ==> P |] ==> P";
+by (rtac (major RS conjE) 1);
+by (REPEAT (ares_tac (prems@[Ord_in_Ord]) 1));
+val ltE = result();
+
+goal Ordinal.thy "!!i j. i<j ==> i:j";
+by (etac ltE 1);
+by (assume_tac 1);
+val ltD = result();
+
+goalw Ordinal.thy [lt_def] "~ i<0";
+by (fast_tac ZF_cs 1);
+val not_lt0 = result();
+
+(* i<0 ==> R *)
+val lt0E = standard (not_lt0 RS notE);
+
+goal Ordinal.thy "!!i j k. [| i<j; j<k |] ==> i<k";
+by (fast_tac (ZF_cs addSIs [ltI] addSEs [ltE, Ord_trans]) 1);
+val lt_trans = result();
+
+goalw Ordinal.thy [lt_def] "!!i j. [| i<j; j<i |] ==> P";
+by (REPEAT (eresolve_tac [asm_rl, conjE, mem_anti_sym] 1));
+val lt_anti_sym = result();
+
+val lt_anti_refl = prove_goal Ordinal.thy "i<i ==> P"
+ (fn [major]=> [ (rtac (major RS (major RS lt_anti_sym)) 1) ]);
+
+val lt_not_refl = prove_goal Ordinal.thy "~ i<i"
+ (fn _=> [ (rtac notI 1), (etac lt_anti_refl 1) ]);
+
+(** le is less than or equals; recall i le j abbrevs i<succ(j) !! **)
+
+goalw Ordinal.thy [lt_def] "i le j <-> i<j | (i=j & Ord(j))";
+by (fast_tac (ZF_cs addSIs [Ord_succ] addSDs [Ord_succD]) 1);
+val le_iff = result();
+
+goal Ordinal.thy "!!i j. i<j ==> i le j";
+by (asm_simp_tac (ZF_ss addsimps [le_iff]) 1);
+val leI = result();
+
+goal Ordinal.thy "!!i. [| i=j; Ord(j) |] ==> i le j";
+by (asm_simp_tac (ZF_ss addsimps [le_iff]) 1);
+val le_eqI = result();
+
+val le_refl = refl RS le_eqI;
+
+val [prem] = goal Ordinal.thy "(~ (i=j & Ord(j)) ==> i<j) ==> i le j";
+by (rtac (disjCI RS (le_iff RS iffD2)) 1);
+by (etac prem 1);
+val leCI = result();
+
+val major::prems = goal Ordinal.thy
+ "[| i le j; i<j ==> P; [| i=j; Ord(j) |] ==> P |] ==> P";
+by (rtac (major RS (le_iff RS iffD1 RS disjE)) 1);
+by (DEPTH_SOLVE (ares_tac prems 1 ORELSE etac conjE 1));
+val leE = result();
+
+goal Ordinal.thy "!!i j. [| i le j; j le i |] ==> i=j";
+by (asm_full_simp_tac (ZF_ss addsimps [le_iff]) 1);
+by (fast_tac (ZF_cs addEs [lt_anti_sym]) 1);
+val le_asym = result();
+
+goal Ordinal.thy "i le 0 <-> i=0";
+by (fast_tac (ZF_cs addSIs [Ord_0 RS le_refl] addSEs [leE, lt0E]) 1);
+val le0_iff = result();
+
+val le0D = standard (le0_iff RS iffD1);
+
+val lt_cs =
+ ZF_cs addSIs [le_refl, leCI]
+ addSDs [le0D]
+ addSEs [lt_anti_refl, lt0E, leE];
+
+
+(*** Natural Deduction rules for Memrel ***)
+
+goalw Ordinal.thy [Memrel_def] "<a,b> : Memrel(A) <-> a:b & a:A & b:A";
+by (fast_tac ZF_cs 1);
+val Memrel_iff = result();
+
+val prems = goal Ordinal.thy "[| a: b; a: A; b: A |] ==> <a,b> : Memrel(A)";
+by (REPEAT (resolve_tac (prems@[conjI, Memrel_iff RS iffD2]) 1));
+val MemrelI = result();
+
+val [major,minor] = goal Ordinal.thy
+ "[| <a,b> : Memrel(A); \
+\ [| a: A; b: A; a:b |] ==> P \
+\ |] ==> P";
+by (rtac (major RS (Memrel_iff RS iffD1) RS conjE) 1);
+by (etac conjE 1);
+by (rtac minor 1);
+by (REPEAT (assume_tac 1));
+val MemrelE = result();
+
+(*The membership relation (as a set) is well-founded.
+ Proof idea: show A<=B by applying the foundation axiom to A-B *)
+goalw Ordinal.thy [wf_def] "wf(Memrel(A))";
+by (EVERY1 [rtac (foundation RS disjE RS allI),
+ etac disjI1,
+ etac bexE,
+ rtac (impI RS allI RS bexI RS disjI2),
+ etac MemrelE,
+ etac bspec,
+ REPEAT o assume_tac]);
+val wf_Memrel = result();
+
+(*Transset(i) does not suffice, though ALL j:i.Transset(j) does*)
+goalw Ordinal.thy [Ord_def, Transset_def, trans_def]
+ "!!i. Ord(i) ==> trans(Memrel(i))";
+by (fast_tac (ZF_cs addSIs [MemrelI] addSEs [MemrelE]) 1);
+val trans_Memrel = result();
+
+(*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
+goalw Ordinal.thy [Transset_def]
+ "!!A. Transset(A) ==> <a,b> : Memrel(A) <-> a:b & b:A";
+by (fast_tac (ZF_cs addSIs [MemrelI] addSEs [MemrelE]) 1);
+val Transset_Memrel_iff = result();
+
+
+(*** Transfinite induction ***)
+
+(*Epsilon induction over a transitive set*)
+val major::prems = goalw Ordinal.thy [Transset_def]
+ "[| i: k; Transset(k); \
+\ !!x.[| x: k; ALL y:x. P(y) |] ==> P(x) \
+\ |] ==> P(i)";
+by (rtac (major RS (wf_Memrel RS wf_induct2)) 1);
+by (fast_tac (ZF_cs addEs [MemrelE]) 1);
+by (resolve_tac prems 1);
+by (assume_tac 1);
+by (cut_facts_tac prems 1);
+by (fast_tac (ZF_cs addIs [MemrelI]) 1);
+val Transset_induct = result();
+
+(*Induction over an ordinal*)
+val Ord_induct = Ord_is_Transset RSN (2, Transset_induct);
+
+(*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
+val [major,indhyp] = goal Ordinal.thy
+ "[| Ord(i); \
+\ !!x.[| Ord(x); ALL y:x. P(y) |] ==> P(x) \
+\ |] ==> P(i)";
+by (rtac (major RS Ord_succ RS (succI1 RS Ord_induct)) 1);
+by (rtac indhyp 1);
+by (rtac (major RS Ord_succ RS Ord_in_Ord) 1);
+by (REPEAT (assume_tac 1));
+val trans_induct = result();
+
+(*Perform induction on i, then prove the Ord(i) subgoal using prems. *)
+fun trans_ind_tac a prems i =
+ EVERY [res_inst_tac [("i",a)] trans_induct i,
+ rename_last_tac a ["1"] (i+1),
+ ares_tac prems i];
+
+
+(*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
+
+(*Finds contradictions for the following proof*)
+val Ord_trans_tac = EVERY' [etac notE, etac Ord_trans, REPEAT o atac];
+
+(** Proving that < is a linear ordering on the ordinals **)
+
+val prems = goal Ordinal.thy
+ "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)";
+by (trans_ind_tac "i" prems 1);
+by (rtac (impI RS allI) 1);
+by (trans_ind_tac "j" [] 1);
+by (DEPTH_SOLVE (step_tac eq_cs 1 ORELSE Ord_trans_tac 1));
+val Ord_linear_lemma = result();
+val Ord_linear = standard (Ord_linear_lemma RS spec RS mp);
+
+(*The trichotomy law for ordinals!*)
+val ordi::ordj::prems = goalw Ordinal.thy [lt_def]
+ "[| Ord(i); Ord(j); i<j ==> P; i=j ==> P; j<i ==> P |] ==> P";
+by (rtac ([ordi,ordj] MRS Ord_linear RS disjE) 1);
+by (etac disjE 2);
+by (DEPTH_SOLVE (ares_tac ([ordi,ordj,conjI] @ prems) 1));
+val Ord_linear_lt = result();
+
+val prems = goal Ordinal.thy
+ "[| Ord(i); Ord(j); i<j ==> P; j le i ==> P |] ==> P";
+by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
+by (DEPTH_SOLVE (ares_tac ([leI, sym RS le_eqI] @ prems) 1));
+val Ord_linear2 = result();
+
+val prems = goal Ordinal.thy
+ "[| Ord(i); Ord(j); i le j ==> P; j le i ==> P |] ==> P";
+by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
+by (DEPTH_SOLVE (ares_tac ([leI,le_eqI] @ prems) 1));
+val Ord_linear_le = result();
+
+goal Ordinal.thy "!!i j. j le i ==> ~ i<j";
+by (fast_tac (lt_cs addEs [lt_anti_sym]) 1);
+val le_imp_not_lt = result();
+
+goal Ordinal.thy "!!i j. [| ~ i<j; Ord(i); Ord(j) |] ==> j le i";
+by (res_inst_tac [("i","i"),("j","j")] Ord_linear2 1);
+by (REPEAT (SOMEGOAL assume_tac));
+by (fast_tac (lt_cs addEs [lt_anti_sym]) 1);
+val not_lt_imp_le = result();
+
+goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> ~ i<j <-> j le i";
+by (REPEAT (ares_tac [iffI, le_imp_not_lt, not_lt_imp_le] 1));
+val not_lt_iff_le = result();
+
+goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> ~ i le j <-> j<i";
+by (asm_simp_tac (ZF_ss addsimps [not_lt_iff_le RS iff_sym]) 1);
+val not_le_iff_lt = result();
+
+goal Ordinal.thy "!!i. Ord(i) ==> 0 le i";
+by (etac (not_lt_iff_le RS iffD1) 1);
+by (REPEAT (resolve_tac [Ord_0, not_lt0] 1));
+val Ord_0_le = result();
+
+goal Ordinal.thy "!!i. [| Ord(i); i~=0 |] ==> 0<i";
+by (etac (not_le_iff_lt RS iffD1) 1);
+by (rtac Ord_0 1);
+by (fast_tac lt_cs 1);
+val Ord_0_lt = result();
+
+(*** Results about less-than or equals ***)
+
+(** For ordinals, j<=i (subset) implies j le i (less-than or equals) **)
+
+goal Ordinal.thy "!!i j. [| j<=i; Ord(i); Ord(j) |] ==> j le i";
+by (rtac (not_lt_iff_le RS iffD1) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (fast_tac (ZF_cs addEs [ltE, mem_anti_refl]) 1);
+val subset_imp_le = result();
+
+goal Ordinal.thy "!!i j. i le j ==> i<=j";
+by (etac leE 1);
+by (fast_tac ZF_cs 2);
+by (fast_tac (subset_cs addIs [OrdmemD] addEs [ltE]) 1);
+val le_imp_subset = result();
+
+goal Ordinal.thy "j le i <-> j<=i & Ord(i) & Ord(j)";
+by (fast_tac (ZF_cs addSEs [subset_imp_le, le_imp_subset]
+ addEs [ltE, make_elim Ord_succD]) 1);
+val le_subset_iff = result();
+
+goal Ordinal.thy "i le succ(j) <-> i le j | i=succ(j) & Ord(i)";
+by (simp_tac (ZF_ss addsimps [le_iff]) 1);
+by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1);
+val le_succ_iff = result();
+
+(*Just a variant of subset_imp_le*)
+val [ordi,ordj,minor] = goal Ordinal.thy
+ "[| Ord(i); Ord(j); !!x. x<j ==> x<i |] ==> j le i";
+by (REPEAT_FIRST (ares_tac [notI RS not_lt_imp_le, ordi, ordj]));
+be (minor RS lt_anti_refl) 1;
+val all_lt_imp_le = result();
+
+(** Transitive laws **)
+
+goal Ordinal.thy "!!i j. [| i le j; j<k |] ==> i<k";
+by (fast_tac (ZF_cs addEs [leE, lt_trans]) 1);
+val lt_trans1 = result();
+
+goal Ordinal.thy "!!i j. [| i<j; j le k |] ==> i<k";
+by (fast_tac (ZF_cs addEs [leE, lt_trans]) 1);
+val lt_trans2 = result();
+
+goal Ordinal.thy "!!i j. [| i le j; j le k |] ==> i le k";
+by (REPEAT (ares_tac [lt_trans1] 1));
+val le_trans = result();
+
+goal Ordinal.thy "!!i j. i<j ==> succ(i) le j";
+by (rtac (not_lt_iff_le RS iffD1) 1);
+by (fast_tac (lt_cs addEs [lt_anti_sym]) 3);
+by (ALLGOALS (fast_tac (ZF_cs addEs [ltE] addIs [Ord_succ])));
+val succ_leI = result();
+
+goal Ordinal.thy "!!i j. succ(i) le j ==> i<j";
+by (rtac (not_le_iff_lt RS iffD1) 1);
+by (fast_tac (lt_cs addEs [lt_anti_sym]) 3);
+by (ALLGOALS (fast_tac (ZF_cs addEs [ltE, make_elim Ord_succD])));
+val succ_leE = result();
+
+goal Ordinal.thy "succ(i) le j <-> i<j";
+by (REPEAT (ares_tac [iffI,succ_leI,succ_leE] 1));
+val succ_le_iff = result();
+
+(** Union and Intersection **)
+
+goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> i le i Un j";
+by (rtac (Un_upper1 RS subset_imp_le) 1);
+by (REPEAT (ares_tac [Ord_Un] 1));
+val Un_upper1_le = result();
+
+goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> j le i Un j";
+by (rtac (Un_upper2 RS subset_imp_le) 1);
+by (REPEAT (ares_tac [Ord_Un] 1));
+val Un_upper2_le = result();
+
+(*Replacing k by succ(k') yields the similar rule for le!*)
+goal Ordinal.thy "!!i j k. [| i<k; j<k |] ==> i Un j < k";
+by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);
+by (rtac (Un_commute RS ssubst) 4);
+by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 4);
+by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 3);
+by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
+val Un_least_lt = result();
+
+goal Ordinal.thy "!!i j. [| Ord(i); Ord(j) |] ==> i Un j < k <-> i<k & j<k";
+by (safe_tac (ZF_cs addSIs [Un_least_lt]));
+br (Un_upper2_le RS lt_trans1) 2;
+br (Un_upper1_le RS lt_trans1) 1;
+by (REPEAT_SOME assume_tac);
+val Un_least_lt_iff = result();
+
+val [ordi,ordj,ordk] = goal Ordinal.thy
+ "[| Ord(i); Ord(j); Ord(k) |] ==> i Un j : k <-> i:k & j:k";
+by (cut_facts_tac [[ordi,ordj] MRS
+ read_instantiate [("k","k")] Un_least_lt_iff] 1);
+by (asm_full_simp_tac (ZF_ss addsimps [lt_def,ordi,ordj,ordk]) 1);
+val Un_least_mem_iff = result();
+
+(*Replacing k by succ(k') yields the similar rule for le!*)
+goal Ordinal.thy "!!i j k. [| i<k; j<k |] ==> i Int j < k";
+by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);
+by (rtac (Int_commute RS ssubst) 4);
+by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 4);
+by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 3);
+by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
+val Int_greatest_lt = result();
+
+(*FIXME: the Intersection duals are missing!*)
+
+
+(*** Results about limits ***)
+
+val prems = goal Ordinal.thy "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))";
+by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1);
+by (REPEAT (etac UnionE 1 ORELSE ares_tac ([Ord_contains_Transset]@prems) 1));
+val Ord_Union = result();
+
+val prems = goal Ordinal.thy
+ "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))";
+by (rtac Ord_Union 1);
+by (etac RepFunE 1);
+by (etac ssubst 1);
+by (eresolve_tac prems 1);
+val Ord_UN = result();
+
+(* No < version; consider (UN i:nat.i)=nat *)
+val [ordi,limit] = goal Ordinal.thy
+ "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i";
+by (rtac (le_imp_subset RS UN_least RS subset_imp_le) 1);
+by (REPEAT (ares_tac [ordi, Ord_UN, limit] 1 ORELSE etac (limit RS ltE) 1));
+val UN_least_le = result();
+
+val [jlti,limit] = goal Ordinal.thy
+ "[| j<i; !!x. x:A ==> b(x)<j |] ==> (UN x:A. succ(b(x))) < i";
+by (rtac (jlti RS ltE) 1);
+by (rtac (UN_least_le RS lt_trans2) 1);
+by (REPEAT (ares_tac [jlti, succ_leI, limit] 1));
+val UN_succ_least_lt = result();
+
+val prems = goal Ordinal.thy
+ "[| a: A; i le b(a); !!x. x:A ==> Ord(b(x)) |] ==> i le (UN x:A. b(x))";
+by (resolve_tac (prems RL [ltE]) 1);
+by (rtac (le_imp_subset RS subset_trans RS subset_imp_le) 1);
+by (REPEAT (ares_tac (prems @ [UN_upper, Ord_UN]) 1));
+val UN_upper_le = result();
+
+goal Ordinal.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";
+by (fast_tac (eq_cs addEs [Ord_trans]) 1);
+val Ord_equality = result();
+
+(*Holds for all transitive sets, not just ordinals*)
+goal Ordinal.thy "!!i. Ord(i) ==> Union(i) <= i";
+by (fast_tac (ZF_cs addSEs [Ord_trans]) 1);
+val Ord_Union_subset = result();
+
+
+(*** Limit ordinals -- general properties ***)
+
+goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i";
+by (fast_tac (eq_cs addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1);
+val Limit_Union_eq = result();
+
+goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)";
+by (etac conjunct1 1);
+val Limit_is_Ord = result();
+
+goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> 0 < i";
+by (etac (conjunct2 RS conjunct1) 1);
+val Limit_has_0 = result();
+
+goalw Ordinal.thy [Limit_def] "!!i. [| Limit(i); j<i |] ==> succ(j) < i";
+by (fast_tac ZF_cs 1);
+val Limit_has_succ = result();
+
+goalw Ordinal.thy [Limit_def]
+ "!!i. [| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)";
+by (safe_tac subset_cs);
+by (rtac (not_le_iff_lt RS iffD1) 2);
+by (fast_tac (lt_cs addEs [lt_anti_sym]) 4);
+by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1));
+val non_succ_LimitI = result();
+
+goal Ordinal.thy "!!i. Limit(succ(i)) ==> P";
+br lt_anti_refl 1;
+br Limit_has_succ 1;
+ba 1;
+be (Limit_is_Ord RS Ord_succD RS le_refl) 1;
+val succ_LimitE = result();
+
+goal Ordinal.thy "!!i. [| Limit(i); i le succ(j) |] ==> i le j";
+by (safe_tac (ZF_cs addSEs [succ_LimitE, leE]));
+val Limit_le_succD = result();
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Ordinal.thy Tue Jun 21 17:20:34 1994 +0200
@@ -0,0 +1,28 @@
+(* Title: ZF/Ordinal.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Ordinals in Zermelo-Fraenkel Set Theory
+*)
+
+Ordinal = WF + "simpdata" + "equalities" +
+consts
+ Memrel :: "i=>i"
+ Transset,Ord :: "i=>o"
+ "<" :: "[i,i] => o" (infixl 50) (*less than on ordinals*)
+ "le" :: "[i,i] => o" (infixl 50) (*less than or equals*)
+ Limit :: "i=>o"
+
+translations
+ "x le y" == "x < succ(y)"
+
+rules
+ Memrel_def "Memrel(A) == {z: A*A . EX x y. z=<x,y> & x:y }"
+ Transset_def "Transset(i) == ALL x:i. x<=i"
+ Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))"
+ lt_def "i<j == i:j & Ord(j)"
+ Limit_def "Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
+
+
+end
--- a/src/ZF/Perm.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Perm.ML Tue Jun 21 17:20:34 1994 +0200
@@ -75,10 +75,13 @@
by (rtac (prem RS lam_mono) 1);
val id_mono = result();
-goalw Perm.thy [inj_def,id_def] "id(A): inj(A,A)";
+goalw Perm.thy [inj_def,id_def] "!!A B. A<=B ==> id(A): inj(A,B)";
by (REPEAT (ares_tac [CollectI,lam_type] 1));
+by (etac subsetD 1 THEN assume_tac 1);
by (simp_tac ZF_ss 1);
-val id_inj = result();
+val id_subset_inj = result();
+
+val id_inj = subset_refl RS id_subset_inj;
goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";
by (fast_tac (ZF_cs addIs [lam_type,beta]) 1);
@@ -111,24 +114,32 @@
by (fast_tac (ZF_cs addIs (prems@[apply_Pair,apply_equality,converseI])) 1);
val left_inverse_lemma = result();
-val prems = goal Perm.thy
- "[| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a";
-by (fast_tac (ZF_cs addIs (prems@
- [left_inverse_lemma,inj_converse_fun,inj_is_fun])) 1);
+goal Perm.thy
+ "!!f. [| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a";
+by (fast_tac (ZF_cs addIs [left_inverse_lemma,inj_converse_fun,inj_is_fun]) 1);
val left_inverse = result();
+val left_inverse_bij = bij_is_inj RS left_inverse;
+
val prems = goal Perm.thy
"[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b";
by (rtac (apply_Pair RS (converseD RS apply_equality)) 1);
by (REPEAT (resolve_tac prems 1));
val right_inverse_lemma = result();
-val prems = goal Perm.thy
- "[| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b";
+goal Perm.thy
+ "!!f. [| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b";
by (rtac right_inverse_lemma 1);
-by (REPEAT (resolve_tac (prems@ [inj_converse_fun,inj_is_fun]) 1));
+by (REPEAT (ares_tac [inj_converse_fun,inj_is_fun] 1));
val right_inverse = result();
+goalw Perm.thy [bij_def]
+ "!!f. [| f: bij(A,B); b: B |] ==> f`(converse(f)`b) = b";
+by (EVERY1 [etac IntE, etac right_inverse,
+ etac (surj_range RS ssubst),
+ assume_tac]);
+val right_inverse_bij = result();
+
val prems = goal Perm.thy
"f: inj(A,B) ==> converse(f): inj(range(f), A)";
bw inj_def; (*rewrite subgoal but not prems!!*)
@@ -236,22 +247,22 @@
by (REPEAT (ares_tac [PiI,comp_rel,ex1I,compI] 1
ORELSE eresolve_tac [fun_is_rel,apply_Pair,apply_type] 1));
by (fast_tac (comp_cs addDs [apply_equality]) 1);
-val comp_func = result();
+val comp_fun = result();
goal Perm.thy "!!f g. [| g: A->B; f: B->C; a:A |] ==> (f O g)`a = f`(g`a)";
-by (REPEAT (ares_tac [comp_func,apply_equality,compI,
+by (REPEAT (ares_tac [comp_fun,apply_equality,compI,
apply_Pair,apply_type] 1));
-val comp_func_apply = result();
+val comp_fun_apply = result();
goalw Perm.thy [inj_def]
"!!f g. [| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C)";
by (REPEAT (eresolve_tac [bspec RS bspec RS mp, box_equals] 1
- ORELSE step_tac (ZF_cs addSIs [comp_func,apply_type,comp_func_apply]) 1));
+ ORELSE step_tac (ZF_cs addSIs [comp_fun,apply_type,comp_fun_apply]) 1));
val comp_inj = result();
goalw Perm.thy [surj_def]
"!!f g. [| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C)";
-by (best_tac (ZF_cs addSIs [comp_func,comp_func_apply]) 1);
+by (best_tac (ZF_cs addSIs [comp_fun,comp_fun_apply]) 1);
val comp_surj = result();
goalw Perm.thy [bij_def]
@@ -268,7 +279,7 @@
"!!f g. [| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)";
by (safe_tac comp_cs);
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
-by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
+by (asm_simp_tac (FOL_ss addsimps [comp_fun_apply]) 1);
val comp_mem_injD1 = result();
goalw Perm.thy [inj_def,surj_def]
@@ -280,24 +291,24 @@
by (safe_tac comp_cs);
by (res_inst_tac [("t", "op `(g)")] subst_context 1);
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
-by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
+by (asm_simp_tac (FOL_ss addsimps [comp_fun_apply]) 1);
val comp_mem_injD2 = result();
goalw Perm.thy [surj_def]
"!!f g. [| (f O g): surj(A,C); g: A->B; f: B->C |] ==> f: surj(B,C)";
-by (fast_tac (comp_cs addSIs [comp_func_apply RS sym, apply_type]) 1);
+by (fast_tac (comp_cs addSIs [comp_fun_apply RS sym, apply_type]) 1);
val comp_mem_surjD1 = result();
goal Perm.thy
"!!f g. [| (f O g)`a = c; g: A->B; f: B->C; a:A |] ==> f`(g`a) = c";
-by (REPEAT (ares_tac [comp_func_apply RS sym RS trans] 1));
-val comp_func_applyD = result();
+by (REPEAT (ares_tac [comp_fun_apply RS sym RS trans] 1));
+val comp_fun_applyD = result();
goalw Perm.thy [inj_def,surj_def]
"!!f g. [| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)";
by (safe_tac comp_cs);
by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);
-by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_func_applyD 1));
+by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1));
by (best_tac (comp_cs addSIs [apply_type]) 1);
val comp_mem_surjD2 = result();
@@ -325,6 +336,49 @@
by (best_tac (comp_cs addIs [apply_Pair]) 1);
val right_comp_inverse = result();
+(** Proving that a function is a bijection **)
+
+val prems =
+goalw Perm.thy [bij_def, inj_def, surj_def]
+ "[| !!x. x:A ==> c(x): B; \
+\ !!y. y:B ==> d(y): A; \
+\ !!x. x:A ==> d(c(x)) = x; \
+\ !!y. y:B ==> c(d(y)) = y \
+\ |] ==> (lam x:A.c(x)) : bij(A,B)";
+by (simp_tac (ZF_ss addsimps ([lam_type]@prems)) 1);
+by (safe_tac ZF_cs);
+(*Apply d to both sides then simplify (type constraint is essential) *)
+by (dres_inst_tac [("t", "d::i=>i")] subst_context 1);
+by (asm_full_simp_tac (ZF_ss addsimps prems) 1);
+by (fast_tac (ZF_cs addIs prems) 1);
+val lam_bijective = result();
+
+goalw Perm.thy [id_def]
+ "!!f A B. [| f: A->B; g: B->A |] ==> \
+\ f O g = id(B) <-> (ALL y:B. f`(g`y)=y)";
+by (safe_tac ZF_cs);
+by (dres_inst_tac [("t", "%h.h`y ")] subst_context 1);
+by (asm_full_simp_tac (ZF_ss addsimps [comp_fun_apply]) 1);
+br fun_extension 1;
+by (REPEAT (ares_tac [comp_fun, lam_type] 1));
+by (asm_simp_tac (ZF_ss addsimps [comp_fun_apply]) 1);
+val comp_eq_id_iff = result();
+
+goalw Perm.thy [bij_def, inj_def, surj_def]
+ "!!f A B. [| f: A->B; g: B->A; f O g = id(B); g O f = id(A) \
+\ |] ==> f : bij(A,B)";
+by (asm_full_simp_tac (ZF_ss addsimps [comp_eq_id_iff]) 1);
+by (safe_tac ZF_cs);
+(*Apply g to both sides then simplify*)
+by (dres_inst_tac [("t", "op `(g)"), ("a", "f`x")] subst_context 1);
+by (asm_full_simp_tac ZF_ss 1);
+by (fast_tac (ZF_cs addIs [apply_type]) 1);
+val fg_imp_bijective = result();
+
+goal Perm.thy "!!f A. [| f: A->A; f O f = id(A) |] ==> f : bij(A,A)";
+by (REPEAT (ares_tac [fg_imp_bijective] 1));
+val nilpotent_imp_bijective = result();
+
(*Injective case applies converse(f) to both sides then simplifies
using left_inverse_lemma*)
goalw Perm.thy [bij_def,inj_def,surj_def]
--- a/src/ZF/QPair.thy Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/QPair.thy Tue Jun 21 17:20:34 1994 +0200
@@ -18,7 +18,7 @@
qfsplit :: "[[i,i] => o, i] => o"
qconverse :: "i => i"
"@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10)
- " <*>" :: "[i, i] => i" ("(_ <*>/ _)" [81, 80] 80)
+ "<*>" :: "[i, i] => i" ("(_ <*>/ _)" [81, 80] 80)
QSigma :: "[i, i => i] => i"
"<+>" :: "[i,i]=>i" (infixr 65)
--- a/src/ZF/ROOT.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/ROOT.ML Tue Jun 21 17:20:34 1994 +0200
@@ -28,6 +28,7 @@
print_depth 1;
+use_thy "CardinalArith";
use_thy "Fin";
use_thy "ListFn";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Rel.ML Tue Jun 21 17:20:34 1994 +0200
@@ -0,0 +1,60 @@
+(* Title: ZF/Rel.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+For Rel.thy. Relations in Zermelo-Fraenkel Set Theory
+*)
+
+open Rel;
+
+(*** Some properties of relations -- useful? ***)
+
+(* irreflexivity *)
+
+val prems = goalw Rel.thy [irrefl_def]
+ "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)";
+by (REPEAT (ares_tac (prems @ [ballI]) 1));
+val irreflI = result();
+
+val prems = goalw Rel.thy [irrefl_def]
+ "[| irrefl(A,r); x:A |] ==> <x,x> ~: r";
+by (rtac (prems MRS bspec) 1);
+val irreflE = result();
+
+(* symmetry *)
+
+val prems = goalw Rel.thy [sym_def]
+ "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)";
+by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
+val symI = result();
+
+goalw Rel.thy [sym_def] "!!r. [| sym(r); <x,y>: r |] ==> <y,x>: r";
+by (fast_tac ZF_cs 1);
+val symE = result();
+
+(* antisymmetry *)
+
+val prems = goalw Rel.thy [antisym_def]
+ "[| !!x y.[| <x,y>: r; <y,x>: r |] ==> x=y |] ==> \
+\ antisym(r)";
+by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
+val antisymI = result();
+
+val prems = goalw Rel.thy [antisym_def]
+ "!!r. [| antisym(r); <x,y>: r; <y,x>: r |] ==> x=y";
+by (fast_tac ZF_cs 1);
+val antisymE = result();
+
+(* transitivity *)
+
+goalw Rel.thy [trans_def]
+ "!!r. [| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
+by (fast_tac ZF_cs 1);
+val transD = result();
+
+goalw Rel.thy [trans_on_def]
+ "!!r. [| trans[A](r); <a,b>:r; <b,c>:r; a:A; b:A; c:A |] ==> <a,c>:r";
+by (fast_tac ZF_cs 1);
+val trans_onD = result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Rel.thy Tue Jun 21 17:20:34 1994 +0200
@@ -0,0 +1,33 @@
+(* Title: ZF/Rel.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Relations in Zermelo-Fraenkel Set Theory
+*)
+
+Rel = ZF +
+consts
+ refl,irrefl,equiv :: "[i,i]=>o"
+ sym,asym,antisym,trans :: "i=>o"
+ trans_on :: "[i,i]=>o" ("trans[_]'(_')")
+
+rules
+ refl_def "refl(A,r) == (ALL x: A. <x,x> : r)"
+
+ irrefl_def "irrefl(A,r) == ALL x: A. <x,x> ~: r"
+
+ sym_def "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
+
+ asym_def "asym(r) == ALL x y. <x,y>:r --> ~ <y,x>:r"
+
+ antisym_def "antisym(r) == ALL x y.<x,y>:r --> <y,x>:r --> x=y"
+
+ trans_def "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
+
+ trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A. \
+\ <x,y>: r --> <y,z>: r --> <x,z>: r"
+
+ equiv_def "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
+
+end
--- a/src/ZF/Sum.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Sum.ML Tue Jun 21 17:20:34 1994 +0200
@@ -35,19 +35,19 @@
(** Injection and freeness equivalences, for rewriting **)
goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b";
-by (simp_tac (ZF_ss addsimps [Pair_iff]) 1);
+by (simp_tac ZF_ss 1);
val Inl_iff = result();
goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b";
-by (simp_tac (ZF_ss addsimps [Pair_iff]) 1);
+by (simp_tac ZF_ss 1);
val Inr_iff = result();
goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False";
-by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0 RS not_sym]) 1);
+by (simp_tac (ZF_ss addsimps [one_not_0 RS not_sym]) 1);
val Inl_Inr_iff = result();
goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False";
-by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0]) 1);
+by (simp_tac (ZF_ss addsimps [one_not_0]) 1);
val Inr_Inl_iff = result();
(*Injection and freeness rules*)
@@ -60,6 +60,9 @@
val sum_cs = ZF_cs addSIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl]
addSDs [Inl_inject,Inr_inject];
+val sum_ss = ZF_ss addsimps [InlI, InrI, Inl_iff, Inr_iff,
+ Inl_Inr_iff, Inr_Inl_iff];
+
goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
by (fast_tac sum_cs 1);
val InlD = result();
@@ -104,6 +107,19 @@
(prems@[case_Inl,case_Inr]))));
val case_type = result();
+goal Sum.thy
+ "!!u. u: A+B ==> \
+\ R(case(c,d,u)) <-> \
+\ ((ALL x:A. u = Inl(x) --> R(c(x))) & \
+\ (ALL y:B. u = Inr(y) --> R(d(y))))";
+by (etac sumE 1);
+by (asm_simp_tac (ZF_ss addsimps [case_Inl]) 1);
+by (fast_tac sum_cs 1);
+by (asm_simp_tac (ZF_ss addsimps [case_Inr]) 1);
+by (fast_tac sum_cs 1);
+val expand_case = result();
+
+
(** Rules for the Part primitive **)
goalw Sum.thy [Part_def]
--- a/src/ZF/Trancl.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Trancl.ML Tue Jun 21 17:20:34 1994 +0200
@@ -8,12 +8,6 @@
open Trancl;
-val major::prems = goalw Trancl.thy [trans_def]
- "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
-by (rtac (major RS spec RS spec RS spec RS mp RS mp) 1);
-by (REPEAT (resolve_tac prems 1));
-val transD = result();
-
goal Trancl.thy "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))";
by (rtac bnd_monoI 1);
by (REPEAT (ares_tac [subset_refl, Un_mono, comp_mono] 2));
--- a/src/ZF/Trancl.thy Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Trancl.thy Tue Jun 21 17:20:34 1994 +0200
@@ -6,16 +6,12 @@
Transitive closure of a relation
*)
-Trancl = Fixedpt + Perm + "mono" +
+Trancl = Fixedpt + Perm + "mono" + Rel +
consts
- "rtrancl" :: "i=>i" ("(_^*)" [100] 100) (*refl/transitive closure*)
- "trancl" :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*)
- "trans" :: "i=>o" (*transitivity predicate*)
+ rtrancl :: "i=>i" ("(_^*)" [100] 100) (*refl/transitive closure*)
+ trancl :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*)
rules
- trans_def "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
-
rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
-
trancl_def "r^+ == r O r^*"
end
--- a/src/ZF/Univ.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Univ.ML Tue Jun 21 17:20:34 1994 +0200
@@ -1,7 +1,7 @@
-(* Title: ZF/univ
+(* Title: ZF/Univ
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
+ Copyright 1994 University of Cambridge
The cumulative hierarchy and a small universe for recursive types
*)
@@ -161,37 +161,6 @@
by (fast_tac ZF_cs 1);
val Vfrom_Union = result();
-(*** Limit ordinals -- general properties ***)
-
-goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i";
-by (fast_tac (eq_cs addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1);
-val Limit_Union_eq = result();
-
-goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)";
-by (etac conjunct1 1);
-val Limit_is_Ord = result();
-
-goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> 0 < i";
-by (etac (conjunct2 RS conjunct1) 1);
-val Limit_has_0 = result();
-
-goalw Univ.thy [Limit_def] "!!i. [| Limit(i); j<i |] ==> succ(j) < i";
-by (fast_tac ZF_cs 1);
-val Limit_has_succ = result();
-
-goalw Univ.thy [Limit_def] "Limit(nat)";
-by (safe_tac (ZF_cs addSIs (ltI::nat_typechecks)));
-by (etac ltD 1);
-val Limit_nat = result();
-
-goalw Univ.thy [Limit_def]
- "!!i. [| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)";
-by (safe_tac subset_cs);
-by (rtac (not_le_iff_lt RS iffD1) 2);
-by (fast_tac (lt_cs addEs [lt_anti_sym]) 4);
-by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1));
-val non_succ_LimitI = result();
-
goal Univ.thy "!!i. Ord(i) ==> i=0 | (EX j. i=succ(j)) | Limit(i)";
by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_lt]) 1);
val Ord_cases_lemma = result();
@@ -284,7 +253,7 @@
by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
val Transset_Vfrom_succ = result();
-goalw Ord.thy [Pair_def,Transset_def]
+goalw Ordinal.thy [Pair_def,Transset_def]
"!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
by (fast_tac ZF_cs 1);
val Transset_Pair_subset = result();
--- a/src/ZF/Univ.thy Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/Univ.thy Tue Jun 21 17:20:34 1994 +0200
@@ -10,18 +10,15 @@
Univ = Arith + Sum + "mono" +
consts
- Limit :: "i=>o"
- Vfrom :: "[i,i]=>i"
- Vset :: "i=>i"
- Vrec :: "[i, [i,i]=>i] =>i"
- univ :: "i=>i"
+ Vfrom :: "[i,i]=>i"
+ Vset :: "i=>i"
+ Vrec :: "[i, [i,i]=>i] =>i"
+ univ :: "i=>i"
translations
"Vset(x)" == "Vfrom(0,x)"
rules
- Limit_def "Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
-
Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
Vrec_def
--- a/src/ZF/WF.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/WF.ML Tue Jun 21 17:20:34 1994 +0200
@@ -22,33 +22,52 @@
(*** Well-founded relations ***)
-(*Are these two theorems at all useful??*)
+(** Equivalences between wf and wf_on **)
+
+goalw WF.thy [wf_def, wf_on_def] "!!A r. wf(r) ==> wf[A](r)";
+by (fast_tac ZF_cs 1);
+val wf_imp_wf_on = result();
+
+goalw WF.thy [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)";
+by (fast_tac ZF_cs 1);
+val wf_on_field_imp_wf = result();
+
+goal WF.thy "wf(r) <-> wf[field(r)](r)";
+by (fast_tac (ZF_cs addSEs [wf_imp_wf_on, wf_on_field_imp_wf]) 1);
+val wf_iff_wf_on_field = result();
-(*If every subset of field(r) possesses an r-minimal element then wf(r).
- Seems impossible to prove this for domain(r) or range(r) instead...
- Consider in particular finite wf relations!*)
-val [prem1,prem2] = goalw WF.thy [wf_def]
- "[| field(r)<=A; \
-\ !!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \
-\ ==> wf(r)";
+goalw WF.thy [wf_on_def, wf_def] "!!A B r. [| wf[A](r); B<=A |] ==> wf[B](r)";
+by (fast_tac ZF_cs 1);
+val wf_on_subset_A = result();
+
+goalw WF.thy [wf_on_def, wf_def] "!!A r s. [| wf[A](r); s<=r |] ==> wf[A](s)";
+by (fast_tac ZF_cs 1);
+val wf_on_subset_r = result();
+
+(** Introduction rules for wf_on **)
+
+(*If every non-empty subset of A has an r-minimal element then wf[A](r).*)
+val [prem] = goalw WF.thy [wf_on_def, wf_def]
+ "[| !!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \
+\ ==> wf[A](r)";
by (rtac (equals0I RS disjCI RS allI) 1);
-by (rtac prem2 1);
-by (res_inst_tac [ ("B1", "Z") ] (prem1 RS (Int_lower1 RS subset_trans)) 1);
-by (fast_tac ZF_cs 1);
-by (fast_tac ZF_cs 1);
-val wfI = result();
+by (res_inst_tac [ ("Z", "Z") ] prem 1);
+by (ALLGOALS (fast_tac ZF_cs));
+val wf_onI = result();
-(*If r allows well-founded induction then wf(r)*)
-val [prem1,prem2] = goal WF.thy
- "[| field(r)<=A; \
-\ !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B |] \
-\ ==> wf(r)";
-by (rtac (prem1 RS wfI) 1);
-by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);
-by (fast_tac ZF_cs 3);
+(*If r allows well-founded induction over A then wf[A](r)
+ Premise is equivalent to
+ !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B *)
+val [prem] = goal WF.thy
+ "[| !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A \
+\ |] ==> y:B |] \
+\ ==> wf[A](r)";
+br wf_onI 1;
+by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1);
+by (contr_tac 3);
by (fast_tac ZF_cs 2);
by (fast_tac ZF_cs 1);
-val wfI2 = result();
+val wf_onI2 = result();
(** Well-founded Induction **)
@@ -88,29 +107,100 @@
by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1);
val wf_induct2 = result();
-val prems = goal WF.thy "[| wf(r); <a,x>:r; <x,a>:r |] ==> False";
-by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> False" 1);
-by (wf_ind_tac "a" prems 2);
+goal ZF.thy "!!r A. field(r Int A*A) <= A";
+by (fast_tac ZF_cs 1);
+val field_Int_square = result();
+
+val wfr::amem::prems = goalw WF.thy [wf_on_def]
+ "[| wf[A](r); a:A; \
+\ !!x.[| x: A; ALL y:A. <y,x>: r --> P(y) |] ==> P(x) \
+\ |] ==> P(a)";
+by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1);
+by (REPEAT (ares_tac prems 1));
+by (fast_tac ZF_cs 1);
+val wf_on_induct = result();
+
+fun wf_on_ind_tac a prems i =
+ EVERY [res_inst_tac [("a",a)] wf_on_induct i,
+ rename_last_tac a ["1"] (i+2),
+ REPEAT (ares_tac prems i)];
+
+(*If r allows well-founded induction then wf(r)*)
+val [subs,indhyp] = goal WF.thy
+ "[| field(r)<=A; \
+\ !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A \
+\ |] ==> y:B |] \
+\ ==> wf(r)";
+br ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1;
+by (REPEAT (ares_tac [indhyp] 1));
+val wfI2 = result();
+
+
+(*** Properties of well-founded relations ***)
+
+goal WF.thy "!!r. wf(r) ==> <a,a> ~: r";
+by (wf_ind_tac "a" [] 1);
+by (fast_tac ZF_cs 1);
+val wf_not_refl = result();
+
+goal WF.thy "!!r. [| wf(r); <a,x>:r; <x,a>:r |] ==> P";
+by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
+by (wf_ind_tac "a" [] 2);
by (fast_tac ZF_cs 2);
-by (fast_tac (FOL_cs addIs prems) 1);
+by (fast_tac FOL_cs 1);
val wf_anti_sym = result();
-(*transitive closure of a WF relation is WF!*)
-val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
-by (rtac (trancl_type RS field_rel_subset RS wfI2) 1);
-by (rtac subsetI 1);
-(*must retain the universal formula for later use!*)
-by (rtac (bspec RS mp) 1 THEN assume_tac 1 THEN assume_tac 1);
-by (eres_inst_tac [("a","x")] (prem RS wf_induct2) 1);
-by (rtac subset_refl 1);
-by (rtac (impI RS allI) 1);
+goal WF.thy "!!r. [| wf[A](r); a: A |] ==> <a,a> ~: r";
+by (wf_on_ind_tac "a" [] 1);
+by (fast_tac ZF_cs 1);
+val wf_on_not_refl = result();
+
+goal WF.thy "!!r. [| wf[A](r); <a,b>:r; <b,a>:r; a:A; b:A |] ==> P";
+by (subgoal_tac "ALL y:A. <a,y>:r --> <y,a>:r --> P" 1);
+by (wf_on_ind_tac "a" [] 2);
+by (fast_tac ZF_cs 2);
+by (fast_tac ZF_cs 1);
+val wf_on_anti_sym = result();
+
+(*Needed to prove well_ordI. Could also reason that wf[A](r) means
+ wf(r Int A*A); thus wf( (r Int A*A)^+ ) and use wf_not_refl *)
+goal WF.thy
+ "!!r. [| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P";
+by (subgoal_tac
+ "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P" 1);
+by (wf_on_ind_tac "a" [] 2);
+by (fast_tac ZF_cs 2);
+by (fast_tac ZF_cs 1);
+val wf_on_chain3 = result();
+
+
+(*retains the universal formula for later use!*)
+val bchain_tac = EVERY' [rtac (bspec RS mp), assume_tac, assume_tac ];
+
+(*transitive closure of a WF relation is WF provided A is downwards closed*)
+val [wfr,subs] = goal WF.thy
+ "[| wf[A](r); r-``A <= A |] ==> wf[A](r^+)";
+br wf_onI2 1;
+by (bchain_tac 1);
+by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1);
+by (rtac (impI RS ballI) 1);
by (etac tranclE 1);
-by (etac (bspec RS mp) 1);
-by (etac fieldI1 1);
+by (etac (bspec RS mp) 1 THEN assume_tac 1);
by (fast_tac ZF_cs 1);
+by (cut_facts_tac [subs] 1);
+(*astar_tac is slightly faster*)
+by (best_tac ZF_cs 1);
+val wf_on_trancl = result();
+
+goal WF.thy "!!r. wf(r) ==> wf(r^+)";
+by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1);
+br (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1;
+be wf_on_trancl 1;
by (fast_tac ZF_cs 1);
val wf_trancl = result();
+
+
(** r-``{a} is the set of everything under a in r **)
val underI = standard (vimage_singleton_iff RS iffD2);
@@ -247,3 +337,12 @@
by (REPEAT (ares_tac (prems@[lam_type]) 1
ORELSE eresolve_tac [spec RS mp, underD] 1));
val wfrec_type = result();
+
+
+goalw WF.thy [wf_on_def, wfrec_on_def]
+ "!!A r. [| wf[A](r); a: A |] ==> \
+\ wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))";
+be (wfrec RS trans) 1;
+by (asm_simp_tac (ZF_ss addsimps [vimage_Int_square, cons_subset_iff]) 1);
+val wfrec_on = result();
+
--- a/src/ZF/WF.thy Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/WF.thy Tue Jun 21 17:20:34 1994 +0200
@@ -1,22 +1,28 @@
(* Title: ZF/wf.thy
ID: $Id$
Author: Tobias Nipkow and Lawrence C Paulson
- Copyright 1992 University of Cambridge
+ Copyright 1994 University of Cambridge
Well-founded Recursion
*)
-WF = Trancl + "mono" +
+WF = Trancl + "mono" + "equalities" +
consts
- wf :: "i=>o"
- wftrec,wfrec :: "[i, i, [i,i]=>i] =>i"
- is_recfun :: "[i, i, [i,i]=>i, i] =>o"
- the_recfun :: "[i, i, [i,i]=>i] =>i"
+ wf :: "i=>o"
+ wf_on :: "[i,i]=>o" ("wf[_]'(_')")
+
+ wftrec,wfrec :: "[i, i, [i,i]=>i] =>i"
+ wfrec_on :: "[i, i, i, [i,i]=>i] =>i" ("wfrec[_]'(_,_,_')")
+ is_recfun :: "[i, i, [i,i]=>i, i] =>o"
+ the_recfun :: "[i, i, [i,i]=>i] =>i"
rules
(*r is a well-founded relation*)
wf_def "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
+ (*r is well-founded relation over A*)
+ wf_on_def "wf_on(A,r) == wf(r Int A*A)"
+
is_recfun_def "is_recfun(r,a,H,f) == \
\ (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
@@ -27,4 +33,6 @@
(*public version. Does not require r to be transitive*)
wfrec_def "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
+ wfrec_on_def "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)"
+
end
--- a/src/ZF/ZF.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/ZF.ML Tue Jun 21 17:20:34 1994 +0200
@@ -1,7 +1,7 @@
(* Title: ZF/zf.ML
ID: $Id$
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
- Copyright 1992 University of Cambridge
+ Copyright 1994 University of Cambridge
Basic introduction and elimination rules for Zermelo-Fraenkel Set Theory
*)
@@ -10,63 +10,66 @@
signature ZF_LEMMAS =
sig
- val ballE : thm
- val ballI : thm
- val ball_cong : thm
- val ball_simp : thm
- val ball_tac : int -> tactic
- val bexCI : thm
- val bexE : thm
- val bexI : thm
- val bex_cong : thm
- val bspec : thm
- val CollectD1 : thm
- val CollectD2 : thm
- val CollectE : thm
- val CollectI : thm
- val Collect_cong : thm
- val emptyE : thm
- val empty_subsetI : thm
- val equalityCE : thm
- val equalityD1 : thm
- val equalityD2 : thm
- val equalityE : thm
- val equalityI : thm
- val equality_iffI : thm
- val equals0D : thm
- val equals0I : thm
- val ex1_functional : thm
- val InterD : thm
- val InterE : thm
- val InterI : thm
- val INT_E : thm
- val INT_I : thm
- val lemmas_cs : claset
- val PowD : thm
- val PowI : thm
- val RepFunE : thm
- val RepFunI : thm
- val RepFun_eqI : thm
- val RepFun_cong : thm
- val ReplaceE : thm
- val ReplaceI : thm
- val Replace_iff : thm
- val Replace_cong : thm
- val rev_ballE : thm
- val rev_bspec : thm
- val rev_subsetD : thm
- val separation : thm
- val setup_induction : thm
- val set_mp_tac : int -> tactic
- val subsetCE : thm
- val subsetD : thm
- val subsetI : thm
- val subset_refl : thm
- val subset_trans : thm
- val UnionE : thm
- val UnionI : thm
- val UN_E : thm
- val UN_I : thm
+ val ballE : thm
+ val ballI : thm
+ val ball_cong : thm
+ val ball_simp : thm
+ val ball_tac : int -> tactic
+ val bexCI : thm
+ val bexE : thm
+ val bexI : thm
+ val bex_cong : thm
+ val bspec : thm
+ val CollectD1 : thm
+ val CollectD2 : thm
+ val CollectE : thm
+ val CollectI : thm
+ val Collect_cong : thm
+ val emptyE : thm
+ val empty_subsetI : thm
+ val equalityCE : thm
+ val equalityD1 : thm
+ val equalityD2 : thm
+ val equalityE : thm
+ val equalityI : thm
+ val equality_iffI : thm
+ val equals0D : thm
+ val equals0I : thm
+ val ex1_functional : thm
+ val InterD : thm
+ val InterE : thm
+ val InterI : thm
+ val INT_E : thm
+ val INT_I : thm
+ val INT_cong : thm
+ val lemmas_cs : claset
+ val PowD : thm
+ val PowI : thm
+ val RepFunE : thm
+ val RepFunI : thm
+ val RepFun_eqI : thm
+ val RepFun_cong : thm
+ val ReplaceE : thm
+ val ReplaceI : thm
+ val Replace_iff : thm
+ val Replace_cong : thm
+ val rev_ballE : thm
+ val rev_bspec : thm
+ val rev_subsetD : thm
+ val separation : thm
+ val setup_induction : thm
+ val set_mp_tac : int -> tactic
+ val subsetCE : thm
+ val subsetD : thm
+ val subsetI : thm
+ val subset_iff : thm
+ val subset_refl : thm
+ val subset_trans : thm
+ val UnionE : thm
+ val UnionI : thm
+ val UN_E : thm
+ val UN_I : thm
+ val UN_cong : thm
end;
@@ -175,6 +178,11 @@
val subset_trans = prove_goal ZF.thy "[| A<=B; B<=C |] ==> A<=C"
(fn prems=> [ (REPEAT (ares_tac ([subsetI]@(prems RL [subsetD])) 1)) ]);
+(*Useful for proving A<=B by rewriting in some cases*)
+val subset_iff = prove_goalw ZF.thy [subset_def,Ball_def]
+ "A<=B <-> (ALL x. x:A --> x:B)"
+ (fn _=> [ (rtac iff_refl 1) ]);
+
(*** Rules for equality ***)
@@ -379,6 +387,10 @@
[ (rtac (major RS UnionE) 1),
(REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]);
+val UN_cong = prove_goal ZF.thy
+ "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A.C(x)) = (UN x:B.D(x))"
+ (fn prems=> [ (simp_tac (FOL_ss addcongs [RepFun_cong] addsimps prems) 1) ]);
+
(*** Rules for Intersections of families ***)
(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
@@ -395,6 +407,10 @@
[ (rtac (major RS InterD) 1),
(rtac (minor RS RepFunI) 1) ]);
+val INT_cong = prove_goal ZF.thy
+ "[| A=B; !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A.C(x)) = (INT x:B.D(x))"
+ (fn prems=> [ (simp_tac (FOL_ss addcongs [RepFun_cong] addsimps prems) 1) ]);
+
(*** Rules for Powersets ***)
--- a/src/ZF/equalities.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/equalities.ML Tue Jun 21 17:20:34 1994 +0200
@@ -58,6 +58,10 @@
by (fast_tac (eq_cs addSEs [equalityE]) 1);
val subset_Int_iff = result();
+goal ZF.thy "A<=B <-> B Int A = A";
+by (fast_tac (eq_cs addSEs [equalityE]) 1);
+val subset_Int_iff2 = result();
+
(** Binary Union **)
goal ZF.thy "0 Un A = A";
@@ -88,6 +92,10 @@
by (fast_tac (eq_cs addSEs [equalityE]) 1);
val subset_Un_iff = result();
+goal ZF.thy "A<=B <-> B Un A = B";
+by (fast_tac (eq_cs addSEs [equalityE]) 1);
+val subset_Un_iff2 = result();
+
(** Simple properties of Diff -- set difference **)
goal ZF.thy "A-A = 0";
@@ -161,6 +169,10 @@
by (fast_tac eq_cs 1);
val Union_Un_distrib = result();
+goal ZF.thy "Union(A Int B) <= Union(A) Int Union(B)";
+by (fast_tac ZF_cs 1);
+val Union_Int_subset = result();
+
goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
by (fast_tac (eq_cs addSEs [equalityE]) 1);
val Union_disjoint = result();
@@ -208,15 +220,13 @@
by (fast_tac eq_cs 1);
val Un_INT_distrib2 = result();
-goal ZF.thy "!!A. [| a: A; ALL y:A. b(y)=b(a) |] ==> (UN y:A. b(y)) = b(a)";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
-val UN_singleton_lemma = result();
-val UN_singleton = ballI RSN (2,UN_singleton_lemma);
+goal ZF.thy "!!A. a: A ==> (UN y:A. c) = c";
+by (fast_tac eq_cs 1);
+val UN_constant = result();
-goal ZF.thy "!!A. [| a: A; ALL y:A. b(y)=b(a) |] ==> (INT y:A. b(y)) = b(a)";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
-val INT_singleton_lemma = result();
-val INT_singleton = ballI RSN (2,INT_singleton_lemma);
+goal ZF.thy "!!A. a: A ==> (INT y:A. c) = c";
+by (fast_tac eq_cs 1);
+val INT_constant = result();
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
Union of a family of unions **)
@@ -292,7 +302,7 @@
val range_Un_eq = result();
goal ZF.thy "range(A Int B) <= range(A) Int range(B)";
-by (fast_tac eq_cs 1);
+by (fast_tac ZF_cs 1);
val range_Int_subset = result();
goal ZF.thy "range(A) - range(B) <= range(A - B)";
@@ -312,6 +322,52 @@
val field_diff_subset = result();
+(** Image **)
+
+goal ZF.thy "r``0 = 0";
+by (fast_tac eq_cs 1);
+val image_empty = result();
+
+goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)";
+by (fast_tac eq_cs 1);
+val image_Un = result();
+
+goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)";
+by (fast_tac ZF_cs 1);
+val image_Int_subset = result();
+
+goal ZF.thy "(r Int A*A)``B <= (r``B) Int A";
+by (fast_tac ZF_cs 1);
+val image_Int_square_subset = result();
+
+goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A";
+by (fast_tac eq_cs 1);
+val image_Int_square = result();
+
+
+(** Inverse Image **)
+
+goal ZF.thy "r-``0 = 0";
+by (fast_tac eq_cs 1);
+val vimage_empty = result();
+
+goal ZF.thy "r-``(A Un B) = (r-``A) Un (r-``B)";
+by (fast_tac eq_cs 1);
+val vimage_Un = result();
+
+goal ZF.thy "r-``(A Int B) <= (r-``A) Int (r-``B)";
+by (fast_tac ZF_cs 1);
+val vimage_Int_subset = result();
+
+goal ZF.thy "(r Int A*A)-``B <= (r-``B) Int A";
+by (fast_tac ZF_cs 1);
+val vimage_Int_square_subset = result();
+
+goal ZF.thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
+by (fast_tac eq_cs 1);
+val vimage_Int_square = result();
+
+
(** Converse **)
goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)";
@@ -351,3 +407,4 @@
goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
by (fast_tac eq_cs 1);
val INT_Pow_subset = result();
+
--- a/src/ZF/func.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/func.ML Tue Jun 21 17:20:34 1994 +0200
@@ -223,6 +223,19 @@
val Pi_lamE = result();
+(** Images of functions **)
+
+goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}";
+by (fast_tac eq_cs 1);
+val image_lam = result();
+
+goal ZF.thy "!!C A. [| f : Pi(A,B); C <= A |] ==> f``C = {f`x. x:C}";
+be (eta RS subst) 1;
+by (asm_full_simp_tac (FOL_ss addsimps [beta, image_lam, subset_iff]
+ addcongs [RepFun_cong]) 1);
+val image_fun = result();
+
+
(*** properties of "restrict" ***)
goalw ZF.thy [restrict_def,lam_def]
--- a/src/ZF/ind_syntax.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/ind_syntax.ML Tue Jun 21 17:20:34 1994 +0200
@@ -89,7 +89,6 @@
val Trueprop = Const("Trueprop",oT-->propT);
fun mk_tprop P = Trueprop $ P;
-fun dest_tprop (Const("Trueprop",_) $ P) = P;
(*Prove a goal stated as a term, with exception handling*)
fun prove_term sign defs (P,tacsf) =
@@ -113,9 +112,14 @@
(*Return the conclusion of a rule, of the form t:X*)
fun rule_concl rl =
- case dest_tprop (Logic.strip_imp_concl rl) of
- Const("op :",_) $ t $ X => (t,X)
- | _ => error "Conclusion of rule should be a set membership";
+ let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) =
+ Logic.strip_imp_concl rl
+ in (t,X) end;
+
+(*As above, but return error message if bad*)
+fun rule_concl_msg sign rl = rule_concl rl
+ handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
+ Sign.string_of_term sign rl);
(*For deriving cases rules. CollectD2 discards the domain, which is redundant;
read_instantiate replaces a propositional variable by a formula variable*)
--- a/src/ZF/intr_elim.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/intr_elim.ML Tue Jun 21 17:20:34 1994 +0200
@@ -119,7 +119,7 @@
val intr_tms = map (term_of o rd propT) sintrs;
local (*Checking the introduction rules*)
- val intr_sets = map (#2 o rule_concl) intr_tms;
+ val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
fun intr_ok set =
case head_of set of Const(a,recT) => a mem rec_names | _ => false;
@@ -154,6 +154,10 @@
| chk_prem rec_hd t =
deny (rec_hd occs t) "Recursion term in side formula";
+fun dest_tprop (Const("Trueprop",_) $ P) = P
+ | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
+ Sign.string_of_term sign Q);
+
(*Makes a disjunct from an introduction rule*)
fun lfp_part intr = (*quantify over rule's free vars except parameters*)
let val prems = map dest_tprop (strip_imp_prems intr)
@@ -213,7 +217,7 @@
val prove = prove_term (sign_of thy);
(********)
-val dummy = writeln "Proving monotonocity...";
+val dummy = writeln "Proving monotonicity...";
val bnd_mono =
prove [] (mk_tprop (Fp.bnd_mono $ dom_sum $ lfp_abs),
--- a/src/ZF/pair.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/pair.ML Tue Jun 21 17:20:34 1994 +0200
@@ -103,7 +103,7 @@
val split = prove_goalw ZF.thy [split_def]
"split(%x y.c(x,y), <a,b>) = c(a,b)"
(fn _ =>
- [ (fast_tac (upair_cs addIs [the_equality] addEs [Pair_inject]) 1) ]);
+ [ (fast_tac (upair_cs addIs [the_equality] addSEs [Pair_inject]) 1) ]);
val split_type = prove_goal ZF.thy
"[| p:Sigma(A,B); \
@@ -114,6 +114,16 @@
(etac ssubst 1),
(REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
+
+goal ZF.thy
+ "!!u. u: A*B ==> \
+\ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
+by (etac SigmaE 1);
+by (asm_simp_tac (FOL_ss addsimps [split]) 1);
+by (fast_tac (upair_cs addSEs [Pair_inject]) 1);
+val expand_split = result();
+
+
(*** conversions for fst and snd ***)
val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"
--- a/src/ZF/simpdata.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/simpdata.ML Tue Jun 21 17:20:34 1994 +0200
@@ -79,15 +79,18 @@
Some rls => flat (map atomize ([th] RL rls))
| None => [th])
| _ => [th]
- in case concl_of th of (*The operator below is Trueprop*)
- _ $ (Const("op :",_) $ a $ b) => tryrules atomize_mem_pairs b
- | _ $ (Const("True",_)) => [] (*True is DELETED*)
- | _ $ (Const("False",_)) => [] (*should False do something??*)
- | _ $ A => tryrules atomize_pairs A
+ in case concl_of th of
+ Const("Trueprop",_) $ P =>
+ (case P of
+ Const("op :",_) $ a $ b => tryrules atomize_mem_pairs b
+ | Const("True",_) => []
+ | Const("False",_) => []
+ | A => tryrules atomize_pairs A)
+ | _ => [th]
end;
val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false,
- beta, eta, restrict, fst_conv, snd_conv, split];
+ beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff];
(*Sigma_cong, Pi_cong NOT included by default since they cause
flex-flex pairs and the "Check your prover" error -- because most
--- a/src/ZF/upair.ML Tue Jun 21 16:26:34 1994 +0200
+++ b/src/ZF/upair.ML Tue Jun 21 17:20:34 1994 +0200
@@ -167,6 +167,15 @@
(resolve_tac [major RS the_equality2 RS ssubst] 1),
(REPEAT (assume_tac 1)) ]);
+(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then
+ (THE x.P(x)) rewrites to (THE x. Q(x)) *)
+
+(*If it's "undefined", it's zero!*)
+val the_0 = prove_goalw ZF.thy [the_def]
+ "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
+ (fn _ =>
+ [ (fast_tac (lemmas_cs addIs [equalityI]) 1) ]);
+
(*** if -- a conditional expression for formulae ***)
@@ -226,6 +235,10 @@
val mem_not_refl = prove_goal ZF.thy "a~:a"
(K [ (rtac notI 1), (etac mem_anti_refl 1) ]);
+(*Good for proving inequalities by rewriting*)
+val mem_imp_not_eq = prove_goal ZF.thy "!!a A. a:A ==> a ~= A"
+ (fn _=> [ fast_tac (lemmas_cs addSEs [mem_anti_refl]) 1 ]);
+
(*** Rules for succ ***)
val succI1 = prove_goalw ZF.thy [succ_def] "i : succ(i)"