--- a/src/ZF/Cardinal.ML Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/Cardinal.ML Tue Jul 12 18:05:03 1994 +0200
@@ -181,7 +181,7 @@
by (rtac LeastI 1);
by (etac Ord_ordertype 2);
by (rtac exI 1);
-by (etac (ordertype_bij RS bij_converse_bij) 1);
+by (etac (ordermap_bij RS bij_converse_bij) 1);
val well_ord_cardinal_eqpoll = result();
val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll
--- a/src/ZF/CardinalArith.ML Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/CardinalArith.ML Tue Jul 12 18:05:03 1994 +0200
@@ -8,6 +8,27 @@
open CardinalArith;
+goalw CardinalArith.thy [jump_cardinal_def]
+ "Ord(jump_cardinal(K))";
+by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
+by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
+
+bw Transset_def;
+by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
+br (ordertype_subset RS exE) 1;
+ba 1;
+ba 1;
+by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
+fr UN_I;
+br ReplaceI 2;
+by (fast_tac ZF_cs 4);
+by (fast_tac ZF_cs 1);
+
+(****************************************************************)
+
+
+
+
(*Use AC to discharge first premise*)
goal CardinalArith.thy
"!!A B. [| well_ord(B,r); A lepoll B |] ==> |A| le |B|";
@@ -341,7 +362,7 @@
"!!A. [| well_ord(A,r); x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)";
by (rtac exI 1);
by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, well_ord_is_wf]) 1);
-by (etac (ordertype_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1);
+by (etac (ordermap_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1);
by (rtac pred_subset 1);
val ordermap_eqpoll_pred = result();
@@ -420,7 +441,7 @@
by (etac (InfCard_is_Card RS Card_is_Ord RS well_ord_csquare) 2);
by (fast_tac (ZF_cs addSIs [Un_least_lt, InfCard_is_Limit, Limit_has_succ]) 2);
by (rtac (OrdmemD RS subset_imp_lepoll) 1);
-by (res_inst_tac [("z1","z")] (csquare_ltI RS less_imp_ordermap_in) 1);
+by (res_inst_tac [("z1","z")] (csquare_ltI RS ordermap_mono) 1);
by (etac well_ord_is_wf 4);
by (ALLGOALS
(fast_tac (ZF_cs addSIs [Un_upper1_le, Un_upper2_le, Ord_ordermap]
@@ -487,7 +508,7 @@
by (rtac cardinal_cong 1);
by (rewtac eqpoll_def);
by (rtac exI 1);
-by (etac (well_ord_csquare RS ordertype_bij) 1);
+by (etac (well_ord_csquare RS ordermap_bij) 1);
val csquare_eq_ordertype = result();
(*Main result: Kunen's Theorem 10.12*)
--- a/src/ZF/CardinalArith.thy Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/CardinalArith.thy Tue Jul 12 18:05:03 1994 +0200
@@ -8,6 +8,8 @@
CardinalArith = Cardinal + OrderArith + Arith +
consts
+ jump_cardinal :: "i=>i"
+
InfCard :: "i=>o"
"|*|" :: "[i,i]=>i" (infixl 70)
"|+|" :: "[i,i]=>i" (infixl 65)
@@ -15,6 +17,11 @@
rules
+ jump_cardinal_def
+ "jump_cardinal(K) == \
+\ UN X:Pow(K). {z. r: Pow(X*X), well_ord(X,r) & z = ordertype(X,r)}"
+
+
InfCard_def "InfCard(i) == Card(i) & nat le i"
cadd_def "i |+| j == | i+j |"
--- a/src/ZF/Makefile Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/Makefile Tue Jul 12 18:05:03 1994 +0200
@@ -24,7 +24,7 @@
ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.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 \
+ OrderArith.thy OrderArith.ML OrderType.thy OrderType.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 \
--- a/src/ZF/Order.ML Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/Order.ML Tue Jul 12 18:05:03 1994 +0200
@@ -164,6 +164,11 @@
by (safe_tac ZF_cs);
val well_ord_is_wf = result();
+goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def]
+ "!!r. well_ord(A,r) ==> trans[A](r)";
+by (safe_tac ZF_cs);
+val well_ord_is_trans_on = result();
+
(*** Derived rules for pred(A,x,r) ***)
@@ -180,3 +185,12 @@
goalw Order.thy [pred_def] "pred(A,x,r) <= A";
by (fast_tac ZF_cs 1);
val pred_subset = result();
+
+goalw Order.thy [pred_def] "y : pred(A,x,r) <-> <y,x>:r & y:A";
+by (fast_tac ZF_cs 1);
+val pred_iff = result();
+
+goalw Order.thy [pred_def]
+ "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)";
+by (fast_tac eq_cs 1);
+val pred_pred_eq = result();
--- a/src/ZF/OrderType.ML Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/OrderType.ML Tue Jul 12 18:05:03 1994 +0200
@@ -7,15 +7,6 @@
*)
-(*Requires Ordinal.thy as parent; otherwise could be in Order.ML*)
-goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
-by (rtac well_ordI 1);
-by (rtac (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;
goalw OrderType.thy [ordermap_def,ordertype_def]
@@ -38,6 +29,7 @@
vimage_singleton_iff]) 1);
val ordermap_eq_image = result();
+(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
goal OrderType.thy
"!!r. [| wf[A](r); x:A |] ==> \
\ ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
@@ -87,7 +79,7 @@
by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
by (assume_tac 1);
by (fast_tac ZF_cs 1);
-val less_imp_ordermap_in = result();
+val ordermap_mono = result();
(*linearity of r is crucial here*)
goalw OrderType.thy [well_ord_def, tot_ord_def]
@@ -96,11 +88,11 @@
by (safe_tac ZF_cs);
by (linear_case_tac 1);
by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1);
-by (dtac less_imp_ordermap_in 1);
+by (dtac ordermap_mono 1);
by (REPEAT_SOME assume_tac);
by (etac mem_asym 1);
by (assume_tac 1);
-val ordermap_in_imp_less = result();
+val converse_ordermap_mono = result();
val ordermap_surj =
(ordermap_type RS surj_image) |>
@@ -114,20 +106,20 @@
by (rtac ordermap_surj 2);
by (linear_case_tac 1);
(*The two cases yield similar contradictions*)
-by (ALLGOALS (dtac less_imp_ordermap_in));
+by (ALLGOALS (dtac ordermap_mono));
by (REPEAT_SOME assume_tac);
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl])));
-val ordertype_bij = result();
+val ordermap_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);
-by (rtac ordertype_bij 1);
+by (rtac ordermap_bij 1);
by (assume_tac 1);
-by (fast_tac (ZF_cs addSEs [MemrelE, ordermap_in_imp_less]) 2);
+by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2);
by (rewtac well_ord_def);
-by (fast_tac (ZF_cs addSIs [MemrelI, less_imp_ordermap_in,
+by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono,
ordermap_type RS apply_type]) 1);
val ordertype_ord_iso = result();
@@ -138,3 +130,90 @@
"ordertype(A,r) = {ordermap(A,r)`y . y : A}";
by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);
val ordertype_unfold = result();
+
+
+(** Ordertype of Memrel **)
+
+(*Requires Ordinal.thy as parent; otherwise could be in Order.ML*)
+goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
+by (rtac well_ordI 1);
+by (rtac (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();
+
+goal OrderType.thy "!!i. [| Ord(i); j:i |] ==> ordermap(i,Memrel(i)) ` j = j";
+by (eresolve_tac [Ord_induct] 1);
+ba 1;
+by (asm_simp_tac (ZF_ss addsimps
+ [well_ord_Memrel RS well_ord_is_wf RS ordermap_pred_unfold]) 1);
+by (asm_simp_tac (ZF_ss addsimps [pred_def, Memrel_iff]) 1);
+by (dresolve_tac [OrdmemD] 1);
+by (assume_tac 1);
+by (fast_tac eq_cs 1);
+val ordermap_Memrel = result();
+
+goal OrderType.thy "!!i. Ord(i) ==> ordertype(i,Memrel(i)) = i";
+by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, ordermap_Memrel]) 1);
+val ordertype_Memrel = result();
+
+(** Ordertype of rvimage **)
+
+goal OrderType.thy
+ "!!f. [| f: bij(A,B); well_ord(B,r); x:A |] ==> \
+\ ordermap(A,rvimage(A,f,r)) ` x = ordermap(B,r) ` (f`x)";
+by (metacut_tac well_ord_rvimage 1 THEN
+ etac bij_is_inj 2 THEN assume_tac 2);
+by (res_inst_tac [("A","A"), ("a","x")] wf_on_induct 1 THEN
+ REPEAT (ares_tac [well_ord_is_wf] 1));
+by (asm_simp_tac
+ (bij_inverse_ss addsimps [ordermap_pred_unfold, well_ord_is_wf]) 1);
+by (asm_simp_tac (ZF_ss addsimps [pred_def, rvimage_iff]) 1);
+by (safe_tac eq_cs);
+by (fast_tac bij_apply_cs 1);
+by (res_inst_tac [("a", "converse(f)`xb")] RepFun_eqI 1);
+by (ALLGOALS (asm_simp_tac bij_inverse_ss));
+val bij_ordermap_vimage = result();
+
+goal OrderType.thy
+ "!!f. [| f: bij(A,B); well_ord(B,r) |] ==> \
+\ ordertype(A,rvimage(A,f,r)) = ordertype(B,r)";
+by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, bij_ordermap_vimage]) 1);
+by (safe_tac eq_cs);
+by (fast_tac bij_apply_cs 1);
+by (res_inst_tac [("a", "converse(f)`xa")] RepFun_eqI 1);
+by (ALLGOALS (asm_simp_tac bij_inverse_ss));
+val bij_ordertype_vimage = result();
+
+
+goal OrderType.thy
+ "!!r. [| well_ord(A,r); y:A; z: pred(A,y,r) |] ==> \
+\ ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
+by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1);
+by (wf_on_ind_tac "z" [] 1);
+by (safe_tac (ZF_cs addSEs [predE]));
+by (asm_simp_tac
+ (ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1);
+(*combining these two simplifications LOOPS! *)
+by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1);
+by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1);
+br (refl RSN (2,RepFun_cong)) 1;
+bd well_ord_is_trans_on 1;
+by (fast_tac (eq_cs addSEs [trans_onD]) 1);
+val ordermap_pred_eq_ordermap = result();
+
+
+goal OrderType.thy
+ "!!r. [| well_ord(A,r); i: ordertype(A,r) |] ==> \
+\ EX B. B<=A & i = ordertype(B,r)";
+by (dresolve_tac [ordertype_unfold RS equalityD1 RS subsetD] 1);
+by (res_inst_tac [("x", "pred(A, converse(ordermap(A,r))`i, r)")] exI 1);
+by (safe_tac (ZF_cs addSEs [predE]));
+by (asm_simp_tac (ZF_ss addsimps [ordermap_bij RS left_inverse_bij]) 1);
+by (asm_simp_tac (ZF_ss addsimps
+ [well_ord_is_wf RS ordermap_pred_unfold]) 1);
+by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold,
+ ordermap_pred_eq_ordermap]) 1);
+val ordertype_subset = result();
+
--- a/src/ZF/OrderType.thy Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/OrderType.thy Tue Jul 12 18:05:03 1994 +0200
@@ -8,7 +8,7 @@
The order type of a well-ordering is the least ordinal isomorphic to it.
*)
-OrderType = Order + Ordinal +
+OrderType = OrderArith + Ordinal +
consts
ordermap :: "[i,i]=>i"
ordertype :: "[i,i]=>i"
--- a/src/ZF/simpdata.ML Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/simpdata.ML Tue Jul 12 18:05:03 1994 +0200
@@ -19,6 +19,10 @@
"<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
"a : Collect(A,P) <-> a:A & P(a)" ];
+goal ZF.thy "{x.x:A} = A";
+by (fast_tac eq_cs 1);
+val triv_RepFun = result();
+
(*INCLUDED: should be??*)
val bquant_simps = map prove_fun
[ "(ALL x:0.P(x)) <-> True",
@@ -90,7 +94,8 @@
end;
val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false,
- beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff];
+ beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff,
+ triv_RepFun];
(*Sigma_cong, Pi_cong NOT included by default since they cause
flex-flex pairs and the "Check your prover" error -- because most