ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
domrange/image_subset,vimage_subset: deleted needless premise!
misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem
ind-syntax/rule_concl: recoded to avoid exceptions
intr-elim: now checks conclusions of introduction rules
func/fun_disjoint_Un: now uses ex_ex1I
list-fn/hd,tl,drop: new
simpdata/bquant_simps: new
list/list_case_type: restored!
bool.thy: changed 1 from a "def" to a translation
Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML
nat/succ_less_induct: new induction principle
arith/add_mono: new results about monotonicity
simpdata/mem_simps: removed the ones for succ and cons; added succI1,
consI2 to ZF_ss
upair/succ_iff: new, for use with simp_tac (cons_iff already existed)
ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ
nat/nat_0_in_succ: new
ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
--- a/src/ZF/Arith.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/Arith.ML Thu Sep 30 10:10:21 1993 +0100
@@ -28,10 +28,8 @@
val rec_0 = result();
goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
-val rec_ss = ZF_ss
- addsimps [nat_case_succ, nat_succI];
by (rtac rec_trans 1);
-by (simp_tac rec_ss 1);
+by (simp_tac (ZF_ss addsimps [nat_case_succ, nat_succI]) 1);
val rec_succ = result();
val major::prems = goal Arith.thy
@@ -103,6 +101,7 @@
(nat_ind_tac "n" prems 1),
(ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
+(*The conclusion is equivalent to m#-n <= m *)
val prems = goal Arith.thy
"[| m:nat; n:nat |] ==> m #- n : succ(m)";
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
@@ -111,8 +110,9 @@
by (etac succE 3);
by (ALLGOALS
(asm_simp_tac
- (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
-val diff_leq = result();
+ (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0,
+ diff_succ_succ]))));
+val diff_less_succ = result();
(*** Simplification over add, mult, diff ***)
@@ -193,10 +193,10 @@
(*addition distributes over multiplication*)
val add_mult_distrib = prove_goal Arith.thy
- "[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
- (fn prems=>
- [ (nat_ind_tac "m" prems 1),
- (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
+ "!!m n. [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
+ (fn _=>
+ [ (etac nat_induct 1),
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]);
(*Distributive law on the left; requires an extra typing premise*)
val add_mult_distrib_left = prove_goal Arith.thy
@@ -209,10 +209,10 @@
(*Associative law for multiplication*)
val mult_assoc = prove_goal Arith.thy
- "[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
- (fn prems=>
- [ (nat_ind_tac "m" prems 1),
- (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
+ "!!m n k. [| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
+ (fn _=>
+ [ (etac nat_induct 1),
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]);
(*** Difference ***)
@@ -231,8 +231,8 @@
by (resolve_tac prems 1);
by (resolve_tac prems 1);
by (ALLGOALS (asm_simp_tac
- (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
- naturals_are_ordinals]))));
+ (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ,
+ naturals_are_ordinals]))));
val add_diff_inverse = result();
@@ -257,7 +257,7 @@
by (etac rev_mp 1);
by (etac rev_mp 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ])));
val div_termination = result();
val div_rls =
@@ -335,6 +335,65 @@
(*May not simplify even with ZF_ss because it would expand m:succ(...) *)
by (rtac (add_0 RS ssubst) 1);
by (rtac (add_succ RS ssubst) 2);
-by (REPEAT (ares_tac [nnat, Ord_0_mem_succ, succ_mem_succI,
+by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI,
naturals_are_ordinals, nat_succI, add_type] 1));
val add_less_succ_self = result();
+
+goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m <= m #+ n";
+by (rtac (add_less_succ_self RS member_succD) 1);
+by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1));
+val add_leq_self = result();
+
+goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m <= n #+ m";
+by (rtac (add_commute RS ssubst) 1);
+by (REPEAT (ares_tac [add_leq_self] 1));
+val add_leq_self2 = result();
+
+(** Monotonicity of addition **)
+
+(*strict, in 1st argument*)
+goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k";
+by (etac succ_less_induct 1);
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff])));
+val add_less_mono1 = result();
+
+(*strict, in both arguments*)
+goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l";
+by (rtac (add_less_mono1 RS Ord_trans) 1);
+by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals]));
+by (EVERY [rtac (add_commute RS ssubst) 1,
+ rtac (add_commute RS ssubst) 3,
+ rtac add_less_mono1 5]);
+by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1));
+val add_less_mono = result();
+
+(*A [clumsy] way of lifting < monotonictity to <= monotonicity *)
+val less_mono::ford::prems = goal Ord.thy
+ "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j); \
+\ !!i. i:k ==> f(i):k; \
+\ i<=j; i:k; j:k; Ord(k) \
+\ |] ==> f(i) <= f(j)";
+by (cut_facts_tac prems 1);
+by (rtac member_succD 1);
+by (dtac member_succI 1);
+by (fast_tac (ZF_cs addSIs [less_mono]) 3);
+by (REPEAT (ares_tac [ford,Ord_in_Ord] 1));
+val Ord_less_mono_imp_mono = result();
+
+(*<=, in 1st argument*)
+goal Arith.thy
+ "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k";
+by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1);
+by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1));
+val add_mono1 = result();
+
+(*<=, in both arguments*)
+goal Arith.thy
+ "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l";
+by (rtac (add_mono1 RS subset_trans) 1);
+by (REPEAT (assume_tac 1));
+by (EVERY [rtac (add_commute RS ssubst) 1,
+ rtac (add_commute RS ssubst) 3,
+ rtac add_mono1 5]);
+by (REPEAT (assume_tac 1));
+val add_mono = result();
--- a/src/ZF/Bool.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/Bool.ML Thu Sep 30 10:10:21 1993 +0100
@@ -8,7 +8,7 @@
open Bool;
-val bool_defs = [bool_def,one_def,cond_def];
+val bool_defs = [bool_def,cond_def];
(* Introduction rules *)
--- a/src/ZF/Bool.thy Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/Bool.thy Thu Sep 30 10:10:21 1993 +0100
@@ -16,8 +16,10 @@
or :: "[i,i]=>i" (infixl 65)
xor :: "[i,i]=>i" (infixl 65)
+translations
+ "1" == "succ(0)"
+
rules
- one_def "1 == succ(0)"
bool_def "bool == {0,1}"
cond_def "cond(b,c,d) == if(b=1,c,d)"
not_def "not(b) == cond(b,0,1)"
--- a/src/ZF/Epsilon.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/Epsilon.ML Thu Sep 30 10:10:21 1993 +0100
@@ -12,7 +12,7 @@
goalw Epsilon.thy [eclose_def] "A <= eclose(A)";
by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1);
-br (nat_0I RS UN_upper) 1;
+by (rtac (nat_0I RS UN_upper) 1);
val arg_subset_eclose = result();
val arg_into_eclose = arg_subset_eclose RS subsetD;
@@ -71,7 +71,7 @@
goalw Epsilon.thy [eclose_def]
"!!X A. [| Transset(X); A<=X |] ==> eclose(A) <= X";
-br (eclose_least_lemma RS UN_least) 1;
+by (rtac (eclose_least_lemma RS UN_least) 1);
by (REPEAT (assume_tac 1));
val eclose_least = result();
@@ -90,8 +90,8 @@
val eclose_induct_down = result();
goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X";
-be ([eclose_least, arg_subset_eclose] MRS equalityI) 1;
-br subset_refl 1;
+by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1);
+by (rtac subset_refl 1);
val Transset_eclose_eq_arg = result();
@@ -233,8 +233,8 @@
goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
by (rtac (rank RS trans) 1);
-br ([UN_least, succI1 RS UN_upper] MRS equalityI) 1;
-be succE 1;
+by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
+by (etac succE 1);
by (fast_tac ZF_cs 1);
by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1));
val rank_succ = result();
--- a/src/ZF/Fixedpt.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/Fixedpt.ML Thu Sep 30 10:10:21 1993 +0100
@@ -88,7 +88,7 @@
val prems = goalw Fixedpt.thy [lfp_def]
"[| h(D) <= D; !!X. [| h(X) <= X; X<=D |] ==> A<=X |] ==> \
\ A <= lfp(D,h)";
-br (Pow_top RS CollectI RS Inter_greatest) 1;
+by (rtac (Pow_top RS CollectI RS Inter_greatest) 1);
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1));
val lfp_greatest = result();
@@ -174,8 +174,8 @@
val [hmono,imono,subhi] = goal Fixedpt.thy
"[| bnd_mono(D,h); bnd_mono(E,i); \
\ !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(E,i)";
-br (bnd_monoD1 RS lfp_greatest) 1;
-br imono 1;
+by (rtac (bnd_monoD1 RS lfp_greatest) 1);
+by (rtac imono 1);
by (rtac (hmono RSN (2, lfp_Int_lowerbound)) 1);
by (rtac (Int_lower1 RS subhi RS subset_trans) 1);
by (rtac (imono RS bnd_monoD2 RS subset_trans) 1);
@@ -186,10 +186,10 @@
but both lfp's must be over the SAME set D; Inter is anti-monotonic!*)
val [isubD,subhi] = goal Fixedpt.thy
"[| i(D) <= D; !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(D,i)";
-br lfp_greatest 1;
-br isubD 1;
+by (rtac lfp_greatest 1);
+by (rtac isubD 1);
by (rtac lfp_lowerbound 1);
-be (subhi RS subset_trans) 1;
+by (etac (subhi RS subset_trans) 1);
by (REPEAT (assume_tac 1));
val lfp_mono2 = result();
--- a/src/ZF/ROOT.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/ROOT.ML Thu Sep 30 10:10:21 1993 +0100
@@ -11,20 +11,7 @@
val banner = "ZF Set Theory (in FOL)";
writeln banner;
-(*For Pure/drule?? Multiple resolution infixes*)
-infix 0 MRS MRL;
-
-(*Resolve a list of rules against bottom_rl from right to left*)
-fun rls MRS bottom_rl =
- let fun rs_aux i [] = bottom_rl
- | rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
- in rs_aux 1 rls end;
-
-fun rlss MRL bottom_rls =
- let fun rs_aux i [] = bottom_rls
- | rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
- in rs_aux 1 rlss end;
-
+(*For Pure/tactic?? A crude way of adding structure to rules*)
fun CHECK_SOLVED (Tactic tf) =
Tactic (fn state =>
case Sequence.pull (tf state) of
--- a/src/ZF/arith.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/arith.ML Thu Sep 30 10:10:21 1993 +0100
@@ -28,10 +28,8 @@
val rec_0 = result();
goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
-val rec_ss = ZF_ss
- addsimps [nat_case_succ, nat_succI];
by (rtac rec_trans 1);
-by (simp_tac rec_ss 1);
+by (simp_tac (ZF_ss addsimps [nat_case_succ, nat_succI]) 1);
val rec_succ = result();
val major::prems = goal Arith.thy
@@ -103,6 +101,7 @@
(nat_ind_tac "n" prems 1),
(ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
+(*The conclusion is equivalent to m#-n <= m *)
val prems = goal Arith.thy
"[| m:nat; n:nat |] ==> m #- n : succ(m)";
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
@@ -111,8 +110,9 @@
by (etac succE 3);
by (ALLGOALS
(asm_simp_tac
- (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
-val diff_leq = result();
+ (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0,
+ diff_succ_succ]))));
+val diff_less_succ = result();
(*** Simplification over add, mult, diff ***)
@@ -193,10 +193,10 @@
(*addition distributes over multiplication*)
val add_mult_distrib = prove_goal Arith.thy
- "[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
- (fn prems=>
- [ (nat_ind_tac "m" prems 1),
- (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
+ "!!m n. [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
+ (fn _=>
+ [ (etac nat_induct 1),
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]);
(*Distributive law on the left; requires an extra typing premise*)
val add_mult_distrib_left = prove_goal Arith.thy
@@ -209,10 +209,10 @@
(*Associative law for multiplication*)
val mult_assoc = prove_goal Arith.thy
- "[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
- (fn prems=>
- [ (nat_ind_tac "m" prems 1),
- (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
+ "!!m n k. [| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
+ (fn _=>
+ [ (etac nat_induct 1),
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]);
(*** Difference ***)
@@ -231,8 +231,8 @@
by (resolve_tac prems 1);
by (resolve_tac prems 1);
by (ALLGOALS (asm_simp_tac
- (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
- naturals_are_ordinals]))));
+ (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ,
+ naturals_are_ordinals]))));
val add_diff_inverse = result();
@@ -257,7 +257,7 @@
by (etac rev_mp 1);
by (etac rev_mp 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ])));
val div_termination = result();
val div_rls =
@@ -335,6 +335,65 @@
(*May not simplify even with ZF_ss because it would expand m:succ(...) *)
by (rtac (add_0 RS ssubst) 1);
by (rtac (add_succ RS ssubst) 2);
-by (REPEAT (ares_tac [nnat, Ord_0_mem_succ, succ_mem_succI,
+by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI,
naturals_are_ordinals, nat_succI, add_type] 1));
val add_less_succ_self = result();
+
+goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m <= m #+ n";
+by (rtac (add_less_succ_self RS member_succD) 1);
+by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1));
+val add_leq_self = result();
+
+goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m <= n #+ m";
+by (rtac (add_commute RS ssubst) 1);
+by (REPEAT (ares_tac [add_leq_self] 1));
+val add_leq_self2 = result();
+
+(** Monotonicity of addition **)
+
+(*strict, in 1st argument*)
+goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k";
+by (etac succ_less_induct 1);
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff])));
+val add_less_mono1 = result();
+
+(*strict, in both arguments*)
+goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l";
+by (rtac (add_less_mono1 RS Ord_trans) 1);
+by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals]));
+by (EVERY [rtac (add_commute RS ssubst) 1,
+ rtac (add_commute RS ssubst) 3,
+ rtac add_less_mono1 5]);
+by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1));
+val add_less_mono = result();
+
+(*A [clumsy] way of lifting < monotonictity to <= monotonicity *)
+val less_mono::ford::prems = goal Ord.thy
+ "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j); \
+\ !!i. i:k ==> f(i):k; \
+\ i<=j; i:k; j:k; Ord(k) \
+\ |] ==> f(i) <= f(j)";
+by (cut_facts_tac prems 1);
+by (rtac member_succD 1);
+by (dtac member_succI 1);
+by (fast_tac (ZF_cs addSIs [less_mono]) 3);
+by (REPEAT (ares_tac [ford,Ord_in_Ord] 1));
+val Ord_less_mono_imp_mono = result();
+
+(*<=, in 1st argument*)
+goal Arith.thy
+ "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k";
+by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1);
+by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1));
+val add_mono1 = result();
+
+(*<=, in both arguments*)
+goal Arith.thy
+ "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l";
+by (rtac (add_mono1 RS subset_trans) 1);
+by (REPEAT (assume_tac 1));
+by (EVERY [rtac (add_commute RS ssubst) 1,
+ rtac (add_commute RS ssubst) 3,
+ rtac add_mono1 5]);
+by (REPEAT (assume_tac 1));
+val add_mono = result();
--- a/src/ZF/bool.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/bool.ML Thu Sep 30 10:10:21 1993 +0100
@@ -8,7 +8,7 @@
open Bool;
-val bool_defs = [bool_def,one_def,cond_def];
+val bool_defs = [bool_def,cond_def];
(* Introduction rules *)
--- a/src/ZF/bool.thy Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/bool.thy Thu Sep 30 10:10:21 1993 +0100
@@ -16,8 +16,10 @@
or :: "[i,i]=>i" (infixl 65)
xor :: "[i,i]=>i" (infixl 65)
+translations
+ "1" == "succ(0)"
+
rules
- one_def "1 == succ(0)"
bool_def "bool == {0,1}"
cond_def "cond(b,c,d) == if(b=1,c,d)"
not_def "not(b) == cond(b,0,1)"
--- a/src/ZF/domrange.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/domrange.ML Thu Sep 30 10:10:21 1993 +0100
@@ -174,7 +174,7 @@
(REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
val image_subset = prove_goal ZF.thy
- "!!A B r. [| r <= A*B; C<=A |] ==> r``C <= B"
+ "!!A B r. r <= A*B ==> r``C <= B"
(fn _ =>
[ (rtac subsetI 1),
(REPEAT (eresolve_tac [asm_rl, imageE, subsetD RS SigmaD2] 1)) ]);
@@ -202,8 +202,8 @@
(REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]);
val vimage_subset = prove_goalw ZF.thy [vimage_def]
- "!!A B r. [| r <= A*B; C<=B |] ==> r-``C <= A"
- (fn _ => [ (REPEAT (ares_tac [converse_type RS image_subset] 1)) ]);
+ "!!A B r. r <= A*B ==> r-``C <= A"
+ (fn _ => [ (etac (converse_type RS image_subset) 1) ]);
(** Theorem-proving for ZF set theory **)
--- a/src/ZF/epsilon.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/epsilon.ML Thu Sep 30 10:10:21 1993 +0100
@@ -12,7 +12,7 @@
goalw Epsilon.thy [eclose_def] "A <= eclose(A)";
by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1);
-br (nat_0I RS UN_upper) 1;
+by (rtac (nat_0I RS UN_upper) 1);
val arg_subset_eclose = result();
val arg_into_eclose = arg_subset_eclose RS subsetD;
@@ -71,7 +71,7 @@
goalw Epsilon.thy [eclose_def]
"!!X A. [| Transset(X); A<=X |] ==> eclose(A) <= X";
-br (eclose_least_lemma RS UN_least) 1;
+by (rtac (eclose_least_lemma RS UN_least) 1);
by (REPEAT (assume_tac 1));
val eclose_least = result();
@@ -90,8 +90,8 @@
val eclose_induct_down = result();
goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X";
-be ([eclose_least, arg_subset_eclose] MRS equalityI) 1;
-br subset_refl 1;
+by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1);
+by (rtac subset_refl 1);
val Transset_eclose_eq_arg = result();
@@ -233,8 +233,8 @@
goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
by (rtac (rank RS trans) 1);
-br ([UN_least, succI1 RS UN_upper] MRS equalityI) 1;
-be succE 1;
+by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
+by (etac succE 1);
by (fast_tac ZF_cs 1);
by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1));
val rank_succ = result();
--- a/src/ZF/fixedpt.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/fixedpt.ML Thu Sep 30 10:10:21 1993 +0100
@@ -88,7 +88,7 @@
val prems = goalw Fixedpt.thy [lfp_def]
"[| h(D) <= D; !!X. [| h(X) <= X; X<=D |] ==> A<=X |] ==> \
\ A <= lfp(D,h)";
-br (Pow_top RS CollectI RS Inter_greatest) 1;
+by (rtac (Pow_top RS CollectI RS Inter_greatest) 1);
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1));
val lfp_greatest = result();
@@ -174,8 +174,8 @@
val [hmono,imono,subhi] = goal Fixedpt.thy
"[| bnd_mono(D,h); bnd_mono(E,i); \
\ !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(E,i)";
-br (bnd_monoD1 RS lfp_greatest) 1;
-br imono 1;
+by (rtac (bnd_monoD1 RS lfp_greatest) 1);
+by (rtac imono 1);
by (rtac (hmono RSN (2, lfp_Int_lowerbound)) 1);
by (rtac (Int_lower1 RS subhi RS subset_trans) 1);
by (rtac (imono RS bnd_monoD2 RS subset_trans) 1);
@@ -186,10 +186,10 @@
but both lfp's must be over the SAME set D; Inter is anti-monotonic!*)
val [isubD,subhi] = goal Fixedpt.thy
"[| i(D) <= D; !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(D,i)";
-br lfp_greatest 1;
-br isubD 1;
+by (rtac lfp_greatest 1);
+by (rtac isubD 1);
by (rtac lfp_lowerbound 1);
-be (subhi RS subset_trans) 1;
+by (etac (subhi RS subset_trans) 1);
by (REPEAT (assume_tac 1));
val lfp_mono2 = result();
--- a/src/ZF/func.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/func.ML Thu Sep 30 10:10:21 1993 +0100
@@ -293,12 +293,14 @@
\ (f Un g) : (A Un C) -> (B Un D)";
(*Contradiction if A Int C = 0, a:A, a:B*)
val [disjoint] = prems RL ([IntI] RLN (2, [equals0D]));
+val Pair_UnE = read_instantiate [("c","<?a,?b>")] UnE; (* ignores x: A Un C *)
by (cut_facts_tac prems 1);
by (rtac PiI 1);
-(*solve subgoal 2 first!!*)
-by (DEPTH_SOLVE_1 (eresolve_tac [UnE, Pair_mem_PiE, sym, disjoint] 2
- INTLEAVE ares_tac [ex1I, apply_Pair RS UnI1, apply_Pair RS UnI2] 2));
-by (REPEAT (eresolve_tac [asm_rl,UnE,rel_Un,PiE] 1));
+by (REPEAT (ares_tac [rel_Un, fun_is_rel] 1));
+by (rtac ex_ex1I 1);
+by (fast_tac (ZF_cs addDs [apply_Pair]) 1);
+by (REPEAT_FIRST (eresolve_tac [asm_rl, Pair_UnE, sym RS trans]
+ ORELSE' eresolve_tac [Pair_mem_PiE,disjoint] THEN' atac));
val fun_disjoint_Un = result();
goal ZF.thy
--- a/src/ZF/ind-syntax.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/ind-syntax.ML Thu Sep 30 10:10:21 1993 +0100
@@ -127,10 +127,11 @@
val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono,
ex_mono, Collect_mono, Part_mono, in_mono];
+(*Return the conclusion of a rule, of the form t:X*)
fun rule_concl rl =
- let val Const("op :",_) $ t $ X = dest_tprop (Logic.strip_imp_concl rl)
- in (t,X) end
- handle _ => error "Conclusion of rule should be a set membership";
+ case dest_tprop (Logic.strip_imp_concl rl) of
+ Const("op :",_) $ t $ X => (t,X)
+ | _ => error "Conclusion of rule should be a set membership";
(*For deriving cases rules. CollectD2 discards the domain, which is redundant;
read_instantiate replaces a propositional variable by a formula variable*)
--- a/src/ZF/ind_syntax.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/ind_syntax.ML Thu Sep 30 10:10:21 1993 +0100
@@ -127,10 +127,11 @@
val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono,
ex_mono, Collect_mono, Part_mono, in_mono];
+(*Return the conclusion of a rule, of the form t:X*)
fun rule_concl rl =
- let val Const("op :",_) $ t $ X = dest_tprop (Logic.strip_imp_concl rl)
- in (t,X) end
- handle _ => error "Conclusion of rule should be a set membership";
+ case dest_tprop (Logic.strip_imp_concl rl) of
+ Const("op :",_) $ t $ X => (t,X)
+ | _ => error "Conclusion of rule should be a set membership";
(*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 Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/intr-elim.ML Thu Sep 30 10:10:21 1993 +0100
@@ -117,7 +117,20 @@
(fn a => "Name of recursive set not declared as constant: " ^ a);
val intr_tms = map (Sign.term_of o rd propT) sintrs;
-val (Const(_,recT),rec_params) = strip_comb (#2 (rule_concl(hd intr_tms)))
+
+local (*Checking the introduction rules*)
+ val intr_sets = map (#2 o rule_concl) intr_tms;
+
+ fun intr_ok set =
+ case head_of set of Const(a,recT) => a mem rec_names | _ => false;
+
+ val dummy = assert_all intr_ok intr_sets
+ (fn t => "Conclusion of rule does not name a recursive set: " ^
+ Sign.string_of_term sign t);
+in
+val (Const(_,recT),rec_params) = strip_comb (hd intr_sets)
+end;
+
val rec_hds = map (fn a=> Const(a,recT)) rec_names;
val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;
@@ -262,8 +275,9 @@
val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
-(*Applies freeness of the given constructors.
- NB for datatypes, defs=con_defs; for inference systems, con_defs=[]! *)
+(*Applies freeness of the given constructors, which *must* be unfolded by
+ the given defs. Cannot simply use the local con_defs because con_defs=[]
+ for inference systems. *)
fun con_elim_tac defs =
rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;
--- a/src/ZF/intr_elim.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/intr_elim.ML Thu Sep 30 10:10:21 1993 +0100
@@ -117,7 +117,20 @@
(fn a => "Name of recursive set not declared as constant: " ^ a);
val intr_tms = map (Sign.term_of o rd propT) sintrs;
-val (Const(_,recT),rec_params) = strip_comb (#2 (rule_concl(hd intr_tms)))
+
+local (*Checking the introduction rules*)
+ val intr_sets = map (#2 o rule_concl) intr_tms;
+
+ fun intr_ok set =
+ case head_of set of Const(a,recT) => a mem rec_names | _ => false;
+
+ val dummy = assert_all intr_ok intr_sets
+ (fn t => "Conclusion of rule does not name a recursive set: " ^
+ Sign.string_of_term sign t);
+in
+val (Const(_,recT),rec_params) = strip_comb (hd intr_sets)
+end;
+
val rec_hds = map (fn a=> Const(a,recT)) rec_names;
val rec_tms = map (fn rec_hd=> list_comb(rec_hd,rec_params)) rec_hds;
@@ -262,8 +275,9 @@
val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD);
-(*Applies freeness of the given constructors.
- NB for datatypes, defs=con_defs; for inference systems, con_defs=[]! *)
+(*Applies freeness of the given constructors, which *must* be unfolded by
+ the given defs. Cannot simply use the local con_defs because con_defs=[]
+ for inference systems. *)
fun con_elim_tac defs =
rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;
--- a/src/ZF/list.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/list.ML Thu Sep 30 10:10:21 1993 +0100
@@ -55,17 +55,14 @@
val list_subset_univ = standard
(list_mono RS (list_univ RSN (2,subset_trans)));
-(*****
val major::prems = goal List.thy
"[| l: list(A); \
-\ c: C(0); \
-\ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(<x,y>) \
-\ |] ==> list_case(l,c,h) : C(l)";
-by (rtac (major RS list_induct) 1);
-by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
- ([list_case_0,list_case_Pair]@prems))));
+\ c: C(Nil); \
+\ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) \
+\ |] ==> list_case(c,h,l) : C(l)";
+by (rtac (major RS List.induct) 1);
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.case_eqns @ prems))));
val list_case_type = result();
-****)
(** For recursion **)
--- a/src/ZF/listfn.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/listfn.ML Thu Sep 30 10:10:21 1993 +0100
@@ -8,6 +8,47 @@
open ListFn;
+(** hd and tl **)
+
+goalw ListFn.thy [hd_def] "hd(Cons(a,l)) = a";
+by (resolve_tac List.case_eqns 1);
+val hd_Cons = result();
+
+goalw ListFn.thy [tl_def] "tl(Nil) = Nil";
+by (resolve_tac List.case_eqns 1);
+val tl_Nil = result();
+
+goalw ListFn.thy [tl_def] "tl(Cons(a,l)) = l";
+by (resolve_tac List.case_eqns 1);
+val tl_Cons = result();
+
+goal ListFn.thy "!!l. l: list(A) ==> tl(l) : list(A)";
+by (etac List.elim 1);
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.intrs @ [tl_Nil,tl_Cons]))));
+val tl_type = result();
+
+(** drop **)
+
+goalw ListFn.thy [drop_def] "drop(0, l) = l";
+by (rtac rec_0 1);
+val drop_0 = result();
+
+goalw ListFn.thy [drop_def] "!!i. i:nat ==> drop(i, Nil) = Nil";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Nil])));
+val drop_Nil = result();
+
+goalw ListFn.thy [drop_def]
+ "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Cons])));
+val drop_succ_Cons = result();
+
+goalw ListFn.thy [drop_def]
+ "!!i l. [| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_type])));
+val drop_type = result();
(** list_rec -- by Vset recursion **)
@@ -67,18 +108,18 @@
val [length_Nil,length_Cons] = list_recs length_def;
-val prems = goalw ListFn.thy [length_def]
- "l: list(A) ==> length(l) : nat";
-by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, nat_succI]) 1));
+goalw ListFn.thy [length_def]
+ "!!l. l: list(A) ==> length(l) : nat";
+by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
val length_type = result();
(** app **)
val [app_Nil,app_Cons] = list_recs app_def;
-val prems = goalw ListFn.thy [app_def]
- "[| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)";
-by (REPEAT (ares_tac (prems @ [list_rec_type, ConsI]) 1));
+goalw ListFn.thy [app_def]
+ "!!xs ys. [| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)";
+by (REPEAT (ares_tac [list_rec_type, ConsI] 1));
val app_type = result();
(** rev **)
@@ -204,6 +245,38 @@
by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
val length_flat = result();
+(** Length and drop **)
+
+(*Lemma for the inductive step of drop_length*)
+goal ListFn.thy
+ "!!xs. xs: list(A) ==> \
+\ ALL x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
+by (etac List.induct 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [drop_0,drop_succ_Cons])));
+by (fast_tac ZF_cs 1);
+val drop_length_Cons_lemma = result();
+val drop_length_Cons = standard (drop_length_Cons_lemma RS spec);
+
+goal ListFn.thy
+ "!!l. l: list(A) ==> ALL i: length(l). EX z zs. drop(i,l) = Cons(z,zs)";
+by (etac List.induct 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps bquant_simps)));
+by (rtac conjI 1);
+by (etac drop_length_Cons 1);
+by (rtac ballI 1);
+by (rtac natE 1);
+by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
+by (assume_tac 1);
+by (asm_simp_tac (list_ss addsimps [drop_0]) 1);
+by (fast_tac ZF_cs 1);
+by (asm_simp_tac (list_ss addsimps [drop_succ_Cons]) 1);
+by (dtac bspec 1);
+by (fast_tac ZF_cs 2);
+by (fast_tac (ZF_cs addEs [succ_in_naturalD,length_type]) 1);
+val drop_length_lemma = result();
+val drop_length = standard (drop_length_lemma RS bspec);
+
+
(*** theorems about app ***)
val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";
--- a/src/ZF/listfn.thy Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/listfn.thy Thu Sep 30 10:10:21 1993 +0100
@@ -18,6 +18,8 @@
length,rev :: "i=>i"
flat :: "i=>i"
list_add :: "i=>i"
+ hd,tl :: "i=>i"
+ drop :: "[i,i]=>i"
(* List Enumeration *)
"[]" :: "i" ("[]")
@@ -31,6 +33,11 @@
rules
+
+ hd_def "hd(l) == list_case(0, %x xs.x, l)"
+ tl_def "tl(l) == list_case(Nil, %x xs.xs, l)"
+ drop_def "drop(i,l) == rec(i, l, %j r. tl(r))"
+
list_rec_def
"list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
@@ -40,5 +47,4 @@
rev_def "rev(l) == list_rec(l, Nil, %x xs r. r @ [x])"
flat_def "flat(ls) == list_rec(ls, Nil, %l ls r. l @ r)"
list_add_def "list_add(l) == list_rec(l, 0, %x xs r. x#+r)"
-
end
--- a/src/ZF/nat.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/nat.ML Thu Sep 30 10:10:21 1993 +0100
@@ -31,7 +31,7 @@
by (resolve_tac prems 1);
val nat_succI = result();
-goalw Nat.thy [one_def] "1 : nat";
+goal Nat.thy "1 : nat";
by (rtac (nat_0I RS nat_succI) 1);
val nat_1I = result();
@@ -59,7 +59,7 @@
val major::prems = goal Nat.thy
"[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P";
-br (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1;
+by (rtac (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1);
by (DEPTH_SOLVE (eresolve_tac [singletonE,RepFunE] 1
ORELSE ares_tac prems 1));
val natE = result();
@@ -69,10 +69,13 @@
by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));
val naturals_are_ordinals = result();
+(* i: nat ==> 0: succ(i) *)
+val nat_0_in_succ = naturals_are_ordinals RS Ord_0_in_succ;
+
goal Nat.thy "!!n. n: nat ==> n=0 | 0:n";
by (etac nat_induct 1);
by (fast_tac ZF_cs 1);
-by (fast_tac (ZF_cs addIs [naturals_are_ordinals RS Ord_0_mem_succ]) 1);
+by (fast_tac (ZF_cs addIs [nat_0_in_succ]) 1);
val natE0 = result();
goal Nat.thy "Ord(nat)";
@@ -84,6 +87,12 @@
by (REPEAT (ares_tac [empty_subsetI,succ_subsetI] 1));
val Ord_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;
+
(** Variations on mathematical induction **)
(*complete induction*)
@@ -97,7 +106,7 @@
by (ALLGOALS
(asm_simp_tac
(ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff,
- Ord_nat RS Ord_in_Ord]))));
+ naturals_are_ordinals]))));
val nat_induct_from_lemma = result();
(*Induction starting from m rather than 0*)
@@ -125,6 +134,28 @@
by (REPEAT (ares_tac (prems@[ballI]) 1 ORELSE etac bspec 1));
val diff_induct = result();
+(** Induction principle analogous to trancl_induct **)
+
+goal Nat.thy
+ "!!m. m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \
+\ (ALL n:nat. m:n --> P(m,n))";
+by (etac nat_induct 1);
+by (ALLGOALS
+ (EVERY' [rtac (impI RS impI), rtac (nat_induct RS ballI), assume_tac,
+ fast_tac ZF_cs, fast_tac ZF_cs]));
+val succ_less_induct_lemma = result();
+
+val prems = goal Nat.thy
+ "[| m: n; n: nat; \
+\ P(m,succ(m)); \
+\ !!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) \
+\ |] ==> P(m,n)";
+by (res_inst_tac [("P4","P")]
+ (succ_less_induct_lemma RS mp RS mp RS bspec RS mp) 1);
+by (rtac (Ord_nat RSN (3,Ord_trans)) 1);
+by (REPEAT (ares_tac (prems @ [ballI,impI]) 1));
+val succ_less_induct = result();
+
(** nat_case **)
goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a";
@@ -157,18 +188,16 @@
val [prem] = goal Nat.thy
"m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
-val nat_rec_ss = ZF_ss
- addsimps [prem, nat_case_succ, nat_succI, Memrel_iff,
- vimage_singleton_iff];
by (rtac nat_rec_trans 1);
-by (simp_tac nat_rec_ss 1);
+by (simp_tac (ZF_ss addsimps [prem, nat_case_succ, nat_succI, Memrel_iff,
+ vimage_singleton_iff]) 1);
val nat_rec_succ = result();
(** The union of two natural numbers is a natural number -- their maximum **)
-(* [| ?i : nat; ?j : nat |] ==> ?i Un ?j : nat *)
+(* [| i : nat; j : nat |] ==> i Un j : nat *)
val Un_nat_type = standard (Ord_nat RSN (3,Ord_member_UnI));
-(* [| ?i : nat; ?j : nat |] ==> ?i Int ?j : nat *)
+(* [| i : nat; j : nat |] ==> i Int j : nat *)
val Int_nat_type = standard (Ord_nat RSN (3,Ord_member_IntI));
--- a/src/ZF/ord.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/ord.ML Thu Sep 30 10:10:21 1993 +0100
@@ -47,14 +47,14 @@
val [prem1,prem2] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def]
"[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
-br (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1;
+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(Ord.thy,Sum.thy)) [sum_def]
"Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
-br (Int_Un_distrib RS ssubst) 1;
+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();
@@ -281,7 +281,7 @@
by (fast_tac ZF_cs 1);
by (rtac (prem RS Ord_succ) 1);
by (rtac Ord_0 1);
-val Ord_0_mem_succ = result();
+val Ord_0_in_succ = result();
goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> j:i <-> j<=i & ~(i<=j)";
by (rtac iffI 1);
@@ -293,7 +293,7 @@
val Ord_member_iff = result();
goal Ord.thy "!!i. Ord(i) ==> 0:i <-> ~ i=0";
-be (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1;
+by (etac (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1);
by (fast_tac eq_cs 1);
val Ord_0_member_iff = result();
@@ -307,6 +307,7 @@
by (ALLGOALS (fast_tac ZF_cs));
val member_succI = result();
+(*Recall Ord_succ_subsetI, namely [| i:j; Ord(j) |] ==> succ(i) <= j *)
goalw Ord.thy [Transset_def,Ord_def]
"!!i j. [| i : succ(j); Ord(j) |] ==> i<=j";
by (fast_tac ZF_cs 1);
@@ -353,6 +354,8 @@
by (REPEAT (ares_tac [Ord_succ] 1));
val Ord_succ_mono = result();
+(** Union and Intersection **)
+
goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Un j : k";
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
--- a/src/ZF/quniv.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/quniv.ML Thu Sep 30 10:10:21 1993 +0100
@@ -12,12 +12,12 @@
goalw QUniv.thy [quniv_def]
"!!X A. X <= univ(eclose(A)) ==> X : quniv(A)";
-be PowI 1;
+by (etac PowI 1);
val qunivI = result();
goalw QUniv.thy [quniv_def]
"!!X A. X : quniv(A) ==> X <= univ(eclose(A))";
-be PowD 1;
+by (etac PowD 1);
val qunivD = result();
goalw QUniv.thy [quniv_def] "!!A B. A<=B ==> quniv(A) <= quniv(B)";
@@ -152,8 +152,8 @@
goal Univ.thy
"!!X. [| {a,b} : Vfrom(X,succ(i)); Transset(X) |] ==> \
\ a: Vfrom(X,i) & b: Vfrom(X,i)";
-bd (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1;
-ba 1;
+by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
+by (assume_tac 1);
by (fast_tac ZF_cs 1);
val doubleton_in_Vfrom_D = result();
@@ -185,8 +185,8 @@
goalw QUniv.thy [QPair_def,sum_def]
"!!X. Transset(X) ==> \
\ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>";
-br (Int_Un_distrib RS ssubst) 1;
-br Un_mono 1;
+by (rtac (Int_Un_distrib RS ssubst) 1);
+by (rtac Un_mono 1);
by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans,
[Int_lower1, subset_refl] MRS Sigma_mono] 1));
val QPair_Int_Vfrom_succ_subset = result();
@@ -194,12 +194,12 @@
(** Pairs in quniv -- for handling the base case **)
goal QUniv.thy "!!X. <a,b> : quniv(X) ==> <a,b> : univ(eclose(X))";
-be ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1;
+by (etac ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1);
val Pair_in_quniv_D = result();
goal QUniv.thy "a*b Int quniv(A) = a*b Int univ(eclose(A))";
-br equalityI 1;
-br ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2;
+by (rtac equalityI 1);
+by (rtac ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2);
by (fast_tac (ZF_cs addSEs [Pair_in_quniv_D]) 1);
val product_Int_quniv_eq = result();
@@ -211,33 +211,33 @@
(**** "Take-lemma" rules for proving c: quniv(A) ****)
goalw QUniv.thy [quniv_def] "Transset(quniv(A))";
-br (Transset_eclose RS Transset_univ RS Transset_Pow) 1;
+by (rtac (Transset_eclose RS Transset_univ RS Transset_Pow) 1);
val Transset_quniv = result();
val [aprem, iprem] = goal QUniv.thy
"[| a: quniv(quniv(X)); \
\ !!i. i:nat ==> a Int Vfrom(quniv(X),i) : quniv(A) \
\ |] ==> a : quniv(A)";
-br (univ_Int_Vfrom_subset RS qunivI) 1;
-br (aprem RS qunivD) 1;
+by (rtac (univ_Int_Vfrom_subset RS qunivI) 1);
+by (rtac (aprem RS qunivD) 1);
by (rtac (Transset_quniv RS Transset_eclose_eq_arg RS ssubst) 1);
-be (iprem RS qunivD) 1;
+by (etac (iprem RS qunivD) 1);
val quniv_Int_Vfrom = result();
(** Rules for level 0 **)
goal QUniv.thy "<a;b> Int quniv(A) : quniv(A)";
-br (QPair_Int_quniv_eq RS ssubst) 1;
-br (Int_lower2 RS qunivI) 1;
+by (rtac (QPair_Int_quniv_eq RS ssubst) 1);
+by (rtac (Int_lower2 RS qunivI) 1);
val QPair_Int_quniv_in_quniv = result();
(*Unused; kept as an example. QInr rule is similar*)
goalw QUniv.thy [QInl_def] "QInl(a) Int quniv(A) : quniv(A)";
-br QPair_Int_quniv_in_quniv 1;
+by (rtac QPair_Int_quniv_in_quniv 1);
val QInl_Int_quniv_in_quniv = result();
goal QUniv.thy "!!a A X. a : quniv(A) ==> a Int X : quniv(A)";
-be ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1;
+by (etac ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1);
val Int_quniv_in_quniv = result();
goal QUniv.thy
@@ -252,8 +252,8 @@
\ b Int Vfrom(X,i) : quniv(A); \
\ Transset(X) \
\ |] ==> <a;b> Int Vfrom(X, succ(i)) : quniv(A)";
-br (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1;
-br (QPair_in_quniv RS qunivD) 2;
+by (rtac (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1);
+by (rtac (QPair_in_quniv RS qunivD) 2);
by (REPEAT (assume_tac 1));
val QPair_Int_Vfrom_succ_in_quniv = result();
@@ -267,7 +267,7 @@
goalw QUniv.thy [QInl_def]
"!!X. [| a Int Vfrom(X,i) : quniv(A); Transset(X) \
\ |] ==> QInl(a) Int Vfrom(X, succ(i)) : quniv(A)";
-br QPair_Int_Vfrom_succ_in_quniv 1;
+by (rtac QPair_Int_Vfrom_succ_in_quniv 1);
by (REPEAT (ares_tac [zero_Int_in_quniv] 1));
val QInl_Int_Vfrom_succ_in_quniv = result();
@@ -276,7 +276,7 @@
goalw QUniv.thy [QPair_def]
"!!X. Transset(X) ==> \
\ <a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>";
-be (Transset_Vfrom RS Transset_sum_Int_subset) 1;
+by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1);
val QPair_Int_Vfrom_subset = result();
goal QUniv.thy
@@ -284,8 +284,8 @@
\ b Int Vfrom(X,i) : quniv(A); \
\ Transset(X) \
\ |] ==> <a;b> Int Vfrom(X,i) : quniv(A)";
-br (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1;
-br (QPair_in_quniv RS qunivD) 2;
+by (rtac (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1);
+by (rtac (QPair_in_quniv RS qunivD) 2);
by (REPEAT (assume_tac 1));
val QPair_Int_Vfrom_in_quniv = result();
@@ -309,15 +309,15 @@
"!!i. [| a Int Vset(i) <= c; \
\ b Int Vset(i) <= d \
\ |] ==> <a;b> Int Vset(succ(i)) <= <c;d>";
-br ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono]
- MRS subset_trans) 1;
+by (rtac ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono]
+ MRS subset_trans) 1);
by (REPEAT (assume_tac 1));
val QPair_Int_Vset_succ_subset_trans = result();
(*Unused; kept as an example. QInr rule is similar*)
goalw QUniv.thy [QInl_def]
"!!i. a Int Vset(i) <= b ==> QInl(a) Int Vset(succ(i)) <= QInl(b)";
-be (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1;
+by (etac (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1);
val QInl_Int_Vset_succ_subset_trans = result();
(*Rule for level i -- preserving the level, not decreasing it*)
@@ -325,8 +325,8 @@
"!!i. [| a Int Vset(i) <= c; \
\ b Int Vset(i) <= d \
\ |] ==> <a;b> Int Vset(i) <= <c;d>";
-br ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono]
- MRS subset_trans) 1;
+by (rtac ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono]
+ MRS subset_trans) 1);
by (REPEAT (assume_tac 1));
val QPair_Int_Vset_subset_trans = result();
--- a/src/ZF/simpdata.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/simpdata.ML Thu Sep 30 10:10:21 1993 +0100
@@ -10,15 +10,21 @@
(writeln s; prove_goal ZF.thy s
(fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));
+(*INCLUDED IN ZF_ss*)
val mem_simps = map prove_fun
- [ "a:0 <-> False",
- "a : A Un B <-> a:A | a:B",
- "a : A Int B <-> a:A & a:B",
- "a : A-B <-> a:A & ~a:B",
- "a : cons(b,B) <-> a=b | a:B",
- "i : succ(j) <-> i=j | i:j",
+ [ "a : 0 <-> False",
+ "a : A Un B <-> a:A | a:B",
+ "a : A Int B <-> a:A & a:B",
+ "a : A-B <-> a:A & ~a:B",
"<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
- "a : Collect(A,P) <-> a:A & P(a)" ];
+ "a : Collect(A,P) <-> a:A & P(a)" ];
+
+(*INCLUDED: should be??*)
+val bquant_simps = map prove_fun
+ [ "(ALL x:0.P(x)) <-> True",
+ "(EX x:0.P(x)) <-> False",
+ "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
+ "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))" ];
(** Tactics for type checking -- from CTT **)
@@ -83,7 +89,7 @@
fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
-val ZF_simps = [empty_subsetI, ball_simp, if_true, if_false,
+val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false,
beta, eta, restrict, fst_conv, snd_conv, split];
(*Sigma_cong, Pi_cong NOT included by default since they cause
@@ -94,5 +100,5 @@
val ZF_ss = FOL_ss
setmksimps ZF_mk_rew_rules
- addsimps (ZF_simps@mem_simps)
+ addsimps (ZF_simps @ mem_simps @ bquant_simps)
addcongs ZF_congs;
--- a/src/ZF/univ.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/univ.ML Thu Sep 30 10:10:21 1993 +0100
@@ -47,11 +47,11 @@
by (eps_ind_tac "x" 1);
by (rtac (Vfrom RS ssubst) 1);
by (rtac (Vfrom RS ssubst) 1);
-br (subset_refl RS Un_mono) 1;
-br UN_least 1;
+by (rtac (subset_refl RS Un_mono) 1);
+by (rtac UN_least 1);
by (etac (rank_implies_mem RS bexE) 1);
-br subset_trans 1;
-be UN_upper 2;
+by (rtac subset_trans 1);
+by (etac UN_upper 2);
by (etac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1);
by (etac bspec 1);
by (assume_tac 1);
@@ -144,16 +144,16 @@
by (rtac equalityI 1);
(*first inclusion*)
by (rtac Un_least 1);
-br (A_subset_Vfrom RS subset_trans) 1;
-br (prem RS UN_upper) 1;
-br UN_least 1;
-be UnionE 1;
-br subset_trans 1;
-be UN_upper 2;
+by (rtac (A_subset_Vfrom RS subset_trans) 1);
+by (rtac (prem RS UN_upper) 1);
+by (rtac UN_least 1);
+by (etac UnionE 1);
+by (rtac subset_trans 1);
+by (etac UN_upper 2);
by (rtac (Vfrom RS ssubst) 1);
-be ([UN_upper, Un_upper2] MRS subset_trans) 1;
+by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
(*opposite inclusion*)
-br UN_least 1;
+by (rtac UN_least 1);
by (rtac (Vfrom RS ssubst) 1);
by (fast_tac ZF_cs 1);
val Vfrom_Union = result();
@@ -183,9 +183,9 @@
goalw Univ.thy [Limit_def]
"!!i. [| Ord(i); 0:i; ALL y. ~ succ(y)=i |] ==> Limit(i)";
by (safe_tac subset_cs);
-br Ord_member 1;
+by (rtac Ord_member 1);
by (REPEAT_FIRST (eresolve_tac [asm_rl, Ord_in_Ord RS Ord_succ]
- ORELSE' dresolve_tac [Ord_succ_subsetI]));
+ ORELSE' dtac Ord_succ_subsetI ));
by (fast_tac (subset_cs addSIs [equalityI]) 1);
val non_succ_LimitI = result();
@@ -271,10 +271,10 @@
goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))";
by (rtac (Vfrom_succ RS trans) 1);
-br (Un_upper2 RSN (2,equalityI)) 1;;
-br (subset_refl RSN (2,Un_least)) 1;;
-br (A_subset_Vfrom RS subset_trans) 1;
-be (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1;
+by (rtac (Un_upper2 RSN (2,equalityI)) 1);
+by (rtac (subset_refl RSN (2,Un_least)) 1);
+by (rtac (A_subset_Vfrom RS subset_trans) 1);
+by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
val Transset_Vfrom_succ = result();
goalw Ord.thy [Pair_def,Transset_def]
@@ -285,8 +285,8 @@
goal Univ.thy
"!!a b.[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \
\ <a,b> : Vfrom(A,i)";
-be (Transset_Pair_subset RS conjE) 1;
-be Transset_Vfrom 1;
+by (etac (Transset_Pair_subset RS conjE) 1);
+by (etac Transset_Vfrom 1);
by (REPEAT (ares_tac [Pair_in_Vfrom_limit] 1));
val Transset_Pair_subset_Vfrom_limit = result();
@@ -346,7 +346,7 @@
by (rtac (bprem RS (limiti RS Limit_VfromE)) 1);
by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1);
by (rtac UN_I 1);
-by (rtac (rewrite_rule [one_def] sum_in_Vfrom) 2);
+by (rtac sum_in_Vfrom 2);
by (rtac (succI1 RS UnI1) 5);
(*Infer that succ(succ(succ(x Un xa))) < i *)
by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2);
@@ -456,14 +456,14 @@
val Vset_rankI = Ord_rank RS VsetI;
goal Univ.thy "a <= Vset(rank(a))";
-br subsetI 1;
-be (rank_lt RS Vset_rankI) 1;
+by (rtac subsetI 1);
+by (etac (rank_lt RS Vset_rankI) 1);
val arg_subset_Vset_rank = result();
val [iprem] = goal Univ.thy
"[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
-br ([subset_refl, arg_subset_Vset_rank] MRS Int_greatest RS subset_trans) 1;
-br (Ord_rank RS iprem) 1;
+by (rtac ([subset_refl, arg_subset_Vset_rank] MRS Int_greatest RS subset_trans) 1);
+by (rtac (Ord_rank RS iprem) 1);
val Int_Vset_subset = result();
(** Set up an environment for simplification **)
@@ -507,28 +507,28 @@
(** univ(A) as a limit **)
goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))";
-br (Limit_nat RS Limit_Vfrom_eq) 1;
+by (rtac (Limit_nat RS Limit_Vfrom_eq) 1);
val univ_eq_UN = result();
goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))";
-br (subset_UN_iff_eq RS iffD1) 1;
-be (univ_eq_UN RS subst) 1;
+by (rtac (subset_UN_iff_eq RS iffD1) 1);
+by (etac (univ_eq_UN RS subst) 1);
val subset_univ_eq_Int = result();
val [aprem, iprem] = goal Univ.thy
"[| a <= univ(X); \
\ !!i. i:nat ==> a Int Vfrom(X,i) <= b \
\ |] ==> a <= b";
-br (aprem RS subset_univ_eq_Int RS ssubst) 1;
-br UN_least 1;
-be iprem 1;
+by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1);
+by (rtac UN_least 1);
+by (etac iprem 1);
val univ_Int_Vfrom_subset = result();
val prems = goal Univ.thy
"[| a <= univ(X); b <= univ(X); \
\ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
\ |] ==> a = b";
-br equalityI 1;
+by (rtac equalityI 1);
by (ALLGOALS
(resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN'
eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN'
@@ -576,7 +576,7 @@
goalw Univ.thy [univ_def]
"!!a b.[| <a,b> <= univ(A); Transset(A) |] ==> <a,b> : univ(A)";
-be Transset_Pair_subset_Vfrom_limit 1;
+by (etac Transset_Pair_subset_Vfrom_limit 1);
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1));
val Transset_Pair_subset_univ = result();
@@ -592,7 +592,7 @@
(** instances for 1 and 2 **)
-goalw Univ.thy [one_def] "1 : univ(A)";
+goal Univ.thy "1 : univ(A)";
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1));
val one_in_univ = result();
--- a/src/ZF/upair.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/upair.ML Thu Sep 30 10:10:21 1993 +0100
@@ -235,17 +235,21 @@
"i : j ==> i : succ(j)"
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
-(*Classical introduction rule*)
-val succCI = prove_goalw ZF.thy [succ_def]
- "(~ i:j ==> i=j) ==> i: succ(j)"
- (fn prems=> [ (rtac consCI 1), (eresolve_tac prems 1) ]);
-
val succE = prove_goalw ZF.thy [succ_def]
"[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS consE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
+val succ_iff = prove_goal ZF.thy "i : succ(j) <-> i=j | i:j"
+ (fn _ => [ (fast_tac (lemmas_cs addIs [succI1,succI2] addSEs [succE]) 1) ]);
+
+(*Classical introduction rule*)
+val succCI = prove_goal ZF.thy "(~ i:j ==> i=j) ==> i: succ(j)"
+ (fn [prem]=>
+ [ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
+ (etac prem 1) ]);
+
val succ_neq_0 = prove_goal ZF.thy "succ(n)=0 ==> P"
(fn [major]=>
[ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),