--- a/src/ZF/AC/AC16_WO4.ML Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/AC/AC16_WO4.ML Tue Aug 01 15:28:21 2000 +0200
@@ -146,7 +146,7 @@
Goal "[| k:nat; m:nat |] ==> \
\ ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m";
by (induct_tac "k" 1);
-by (simp_tac (simpset() addsimps [add_0]) 1);
+by (asm_simp_tac (simpset() addsimps [add_0]) 1);
by (fast_tac (claset() addIs [eqpoll_imp_lepoll RS
(Diff_subset RS subset_imp_lepoll RS lepoll_trans)]) 1);
by (REPEAT (resolve_tac [allI,impI] 1));
--- a/src/ZF/AC/WO2_AC16.ML Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/AC/WO2_AC16.ML Tue Aug 01 15:28:21 2000 +0200
@@ -256,8 +256,8 @@
Goal "[| recfunAC16(f,g,y,a) <= {X: Pow(A). X eqpoll n}; \
-\ A eqpoll a; y<a; ~Finite(a); Card(a); n:nat |] \
-\ ==> Union(recfunAC16(f,g,y,a)) lesspoll a";
+\ A eqpoll a; y<a; ~Finite(a); Card(a); n:nat |] \
+\ ==> Union(recfunAC16(f,g,y,a)) lesspoll a";
by (eresolve_tac [eqpoll_def RS def_imp_iff RS iffD1 RS exE] 1);
by (rtac Union_lesspoll 1 THEN (TRYALL assume_tac));
by (eresolve_tac [lt_Ord RS recfunAC16_lepoll_index] 3);
@@ -270,12 +270,12 @@
Goal "[| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
\ Card(a); ~ Finite(a); A eqpoll a; \
-\ k : nat; m : nat; y<a; \
+\ k: nat; y<a; \
\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}) |] \
\ ==> A - Union(recfunAC16(f, fa, y, a)) - fa`y eqpoll a";
by (rtac dbl_Diff_eqpoll_Card 1 THEN (TRYALL assume_tac));
by (rtac Union_recfunAC16_lesspoll 1 THEN (REPEAT (assume_tac 1)));
-by (eresolve_tac [add_type RS nat_succI] 1 THEN (assume_tac 1));
+by (Simp_tac 1);
by (resolve_tac [nat_succI RSN
(2, bexI RS (Finite_def RS def_imp_iff RS iffD2)) RS
(Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord))] 1
--- a/src/ZF/Arith.ML Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/Arith.ML Tue Aug 01 15:28:21 2000 +0200
@@ -28,163 +28,317 @@
bind_thm ("zero_lt_natE", lemma RS bexE);
+(** natify: coercion to "nat" **)
+
+Goalw [pred_def] "pred(succ(y)) = y";
+by Auto_tac;
+qed "pred_succ_eq";
+Addsimps [pred_succ_eq];
+
+Goal "natify(succ(x)) = succ(natify(x))";
+by (rtac (natify_def RS def_Vrecursor RS trans) 1);
+by Auto_tac;
+qed "natify_succ";
+Addsimps [natify_succ];
+
+Goal "natify(0) = 0";
+by (rtac (natify_def RS def_Vrecursor RS trans) 1);
+by Auto_tac;
+qed "natify_0";
+Addsimps [natify_0];
+
+Goal "ALL z. x ~= succ(z) ==> natify(x) = 0";
+by (rtac (natify_def RS def_Vrecursor RS trans) 1);
+by Auto_tac;
+qed "natify_non_succ";
+
+Goal "natify(x) : nat";
+by (eps_ind_tac "x" 1);
+by (case_tac "EX z. x1 = succ(z)" 1);
+by (auto_tac (claset(), simpset() addsimps [natify_non_succ]));
+qed "natify_in_nat";
+AddIffs [natify_in_nat];
+AddTCs [natify_in_nat];
+
+Goal "n : nat ==> natify(n) = n";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "natify_ident";
+Addsimps [natify_ident];
+
+
+(*** Collapsing rules: to remove natify from arithmetic expressions ***)
+
+Goal "natify(natify(x)) = natify(x)";
+by (Simp_tac 1);
+qed "natify_idem";
+Addsimps [natify_idem];
+
(** Addition **)
-Goal "[| m:nat; n:nat |] ==> m #+ n : nat";
+Goal "natify(m) #+ n = m #+ n";
+by (simp_tac (simpset() addsimps [add_def]) 1);
+qed "add_natify1";
+
+Goal "m #+ natify(n) = m #+ n";
+by (simp_tac (simpset() addsimps [add_def]) 1);
+qed "add_natify2";
+Addsimps [add_natify1, add_natify2];
+
+(** Multiplication **)
+
+Goal "natify(m) #* n = m #* n";
+by (simp_tac (simpset() addsimps [mult_def]) 1);
+qed "mult_natify1";
+
+Goal "m #* natify(n) = m #* n";
+by (simp_tac (simpset() addsimps [mult_def]) 1);
+qed "mult_natify2";
+Addsimps [mult_natify1, mult_natify2];
+
+(** Difference **)
+
+Goal "natify(m) #- n = m #- n";
+by (simp_tac (simpset() addsimps [diff_def]) 1);
+qed "diff_natify1";
+
+Goal "m #- natify(n) = m #- n";
+by (simp_tac (simpset() addsimps [diff_def]) 1);
+qed "diff_natify2";
+Addsimps [diff_natify1, diff_natify2];
+
+
+(*** Typing rules ***)
+
+(** Addition **)
+
+Goal "[| m:nat; n:nat |] ==> m ##+ n : nat";
by (induct_tac "m" 1);
by Auto_tac;
+qed "raw_add_type";
+
+Goal "m #+ n : nat";
+by (simp_tac (simpset() addsimps [add_def, raw_add_type]) 1);
qed "add_type";
-Addsimps [add_type];
+AddIffs [add_type];
AddTCs [add_type];
(** Multiplication **)
-Goal "[| m:nat; n:nat |] ==> m #* n : nat";
+Goal "[| m:nat; n:nat |] ==> m ##* n : nat";
by (induct_tac "m" 1);
-by Auto_tac;
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [raw_add_type])));
+qed "raw_mult_type";
+
+Goal "m #* n : nat";
+by (simp_tac (simpset() addsimps [mult_def, raw_mult_type]) 1);
qed "mult_type";
-Addsimps [mult_type];
+AddIffs [mult_type];
AddTCs [mult_type];
(** Difference **)
-Goal "[| m:nat; n:nat |] ==> m #- n : nat";
+Goal "[| m:nat; n:nat |] ==> m ##- n : nat";
by (induct_tac "n" 1);
by Auto_tac;
by (fast_tac (claset() addIs [nat_case_type]) 1);
+qed "raw_diff_type";
+
+Goal "m #- n : nat";
+by (simp_tac (simpset() addsimps [diff_def, raw_diff_type]) 1);
qed "diff_type";
-Addsimps [diff_type];
+AddIffs [diff_type];
AddTCs [diff_type];
-Goal "n:nat ==> 0 #- n = 0";
-by (induct_tac "n" 1);
+Goalw [diff_def] "0 #- n = 0";
+by (rtac (natify_in_nat RS nat_induct) 1);
by Auto_tac;
qed "diff_0_eq_0";
(*Must simplify BEFORE the induction: else we get a critical pair*)
-Goal "[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n";
-by (Asm_simp_tac 1);
-by (induct_tac "n" 1);
+Goal "succ(m) #- succ(n) = m #- n";
+by (simp_tac (simpset() addsimps [diff_def]) 1);
+by (res_inst_tac [("x1","n")] (natify_in_nat RS nat_induct) 1);
by Auto_tac;
qed "diff_succ_succ";
-Addsimps [diff_0_eq_0, diff_succ_succ];
+(*This defining property is no longer wanted*)
+Delsimps [raw_diff_succ];
-(*This defining property is no longer wanted*)
-Delsimps [diff_SUCC];
+(*Natify has weakened this law, compared with the older approach*)
+Goal "m #- 0 = natify(m)";
+by (asm_simp_tac (simpset() addsimps [diff_def]) 1);
+qed "diff_0";
-val prems = goal Arith.thy
- "[| m:nat; n:nat |] ==> m #- n le m";
-by (rtac (prems MRS diff_induct) 1);
-by (etac leE 3);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps prems @ [le_iff])));
+Addsimps [diff_0, diff_0_eq_0, diff_succ_succ];
+
+Goal "m:nat ==> (m #- n) le m";
+by (subgoal_tac "(m #- natify(n)) le m" 1);
+by (res_inst_tac [("m","m"), ("n","natify(n)")] diff_induct 2);
+by (etac leE 6);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [le_iff])));
qed "diff_le_self";
-(*** Simplification over add, mult, diff ***)
-
-val arith_typechecks = [add_type, mult_type, diff_type];
-
(*** Addition ***)
+(*Natify has weakened this law, compared with the older approach*)
+Goal "0 #+ m = natify(m)";
+by (asm_simp_tac (simpset() addsimps [add_def]) 1);
+qed "add_0";
+
+Goal "succ(m) #+ n = succ(m #+ n)";
+by (asm_simp_tac (simpset() addsimps [add_def]) 1);
+qed "add_succ";
+
+Addsimps [add_0, add_succ];
+
(*Associative law for addition*)
-Goal "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)";
-by (induct_tac "m" 1);
+Goal "(m #+ n) #+ k = m #+ (n #+ k)";
+by (subgoal_tac "(natify(m) #+ natify(n)) #+ natify(k) = \
+\ natify(m) #+ (natify(n) #+ natify(k))" 1);
+by (res_inst_tac [("n","natify(m)")] nat_induct 2);
by Auto_tac;
qed "add_assoc";
(*The following two lemmas are used for add_commute and sometimes
elsewhere, since they are safe for rewriting.*)
-Goal "m:nat ==> m #+ 0 = m";
-by (induct_tac "m" 1);
+Goal "m #+ 0 = natify(m)";
+by (subgoal_tac "natify(m) #+ 0 = natify(m)" 1);
+by (res_inst_tac [("n","natify(m)")] nat_induct 2);
+by Auto_tac;
+qed "add_0_right_natify";
+
+Goalw [add_def] "m #+ succ(n) = succ(m #+ n)";
+by (res_inst_tac [("n","natify(m)")] nat_induct 1);
+by Auto_tac;
+qed "add_succ_right";
+
+Addsimps [add_0_right_natify, add_succ_right];
+
+Goal "m: nat ==> m #+ 0 = m";
by Auto_tac;
qed "add_0_right";
-Goal "m:nat ==> m #+ succ(n) = succ(m #+ n)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "add_succ_right";
-
-Addsimps [add_0_right, add_succ_right];
-
(*Commutative law for addition*)
-Goal "[| m:nat; n:nat |] ==> m #+ n = n #+ m";
-by (induct_tac "n" 1);
+Goal "m #+ n = n #+ m";
+by (subgoal_tac "natify(m) #+ natify(n) = natify(n) #+ natify(m)" 1);
+by (res_inst_tac [("n","natify(m)")] nat_induct 2);
by Auto_tac;
qed "add_commute";
(*for a/c rewriting*)
-Goal "[| m:nat; n:nat |] ==> m#+(n#+k)=n#+(m#+k)";
-by (asm_simp_tac (simpset() addsimps [add_assoc RS sym, add_commute]) 1);
+Goal "m#+(n#+k)=n#+(m#+k)";
+by (rtac (add_commute RS trans) 1);
+by (rtac (add_assoc RS trans) 1);
+by (rtac (add_commute RS subst_context) 1);
qed "add_left_commute";
(*Addition is an AC-operator*)
val add_ac = [add_assoc, add_commute, add_left_commute];
(*Cancellation law on the left*)
-Goal "[| k #+ m = k #+ n; k:nat |] ==> m=n";
+Goal "[| k ##+ m = k ##+ n; k:nat |] ==> m=n";
by (etac rev_mp 1);
by (induct_tac "k" 1);
by Auto_tac;
+qed "raw_add_left_cancel";
+
+Goalw [add_def] "k #+ m = k #+ n ==> natify(m) = natify(n)";
+by (dtac raw_add_left_cancel 1);
+by Auto_tac;
+qed "add_left_cancel_natify";
+
+Goal "[| k #+ m = k #+ n; m:nat; n:nat |] ==> m = n";
+by (dtac add_left_cancel_natify 1);
+by Auto_tac;
qed "add_left_cancel";
+
(*** Multiplication ***)
+Goal "0 #* m = 0";
+by (simp_tac (simpset() addsimps [mult_def]) 1);
+qed "mult_0";
+
+Goal "succ(m) #* n = n #+ (m #* n)";
+by (simp_tac (simpset() addsimps [add_def, mult_def, raw_mult_type]) 1);
+qed "mult_succ";
+
+Addsimps [mult_0, mult_succ];
+
(*right annihilation in product*)
-Goal "m:nat ==> m #* 0 = 0";
-by (induct_tac "m" 1);
+Goalw [mult_def] "m #* 0 = 0";
+by (res_inst_tac [("n","natify(m)")] nat_induct 1);
by Auto_tac;
qed "mult_0_right";
(*right successor law for multiplication*)
-Goal "[| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)";
-by (induct_tac "m" 1);
+Goal "m #* succ(n) = m #+ (m #* n)";
+by (subgoal_tac "natify(m) #* succ(natify(n)) = \
+\ natify(m) #+ (natify(m) #* natify(n))" 1);
+by (full_simp_tac (simpset() addsimps [add_def, mult_def]) 1);
+by (res_inst_tac [("n","natify(m)")] nat_induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
qed "mult_succ_right";
Addsimps [mult_0_right, mult_succ_right];
-Goal "n:nat ==> 1 #* n = n";
+Goal "1 #* n = natify(n)";
+by Auto_tac;
+qed "mult_1_natify";
+
+Goal "n #* 1 = natify(n)";
+by Auto_tac;
+qed "mult_1_right_natify";
+
+Addsimps [mult_1_natify, mult_1_right_natify];
+
+Goal "n : nat ==> 1 #* n = n";
by (Asm_simp_tac 1);
qed "mult_1";
-Goal "n:nat ==> n #* 1 = n";
+Goal "n : nat ==> n #* 1 = n";
by (Asm_simp_tac 1);
qed "mult_1_right";
-Addsimps [mult_1, mult_1_right];
-
(*Commutative law for multiplication*)
-Goal "[| m:nat; n:nat |] ==> m #* n = n #* m";
-by (induct_tac "m" 1);
+Goal "m #* n = n #* m";
+by (subgoal_tac "natify(m) #* natify(n) = natify(n) #* natify(m)" 1);
+by (res_inst_tac [("n","natify(m)")] nat_induct 2);
by Auto_tac;
qed "mult_commute";
(*addition distributes over multiplication*)
-Goal "[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)";
-by (induct_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
+Goal "(m #+ n) #* k = (m #* k) #+ (n #* k)";
+by (subgoal_tac "(natify(m) #+ natify(n)) #* natify(k) = \
+\ (natify(m) #* natify(k)) #+ (natify(n) #* natify(k))" 1);
+by (res_inst_tac [("n","natify(m)")] nat_induct 2);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_assoc RS sym])));
qed "add_mult_distrib";
-(*Distributive law on the left; requires an extra typing premise*)
-Goal "[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)";
-by (induct_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
+(*Distributive law on the left*)
+Goal "k #* (m #+ n) = (k #* m) #+ (k #* n)";
+by (subgoal_tac "natify(k) #* (natify(m) #+ natify(n)) = \
+\ (natify(k) #* natify(m)) #+ (natify(k) #* natify(n))" 1);
+by (res_inst_tac [("n","natify(m)")] nat_induct 2);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
qed "add_mult_distrib_left";
(*Associative law for multiplication*)
-Goal "[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)";
-by (induct_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
+Goal "(m #* n) #* k = m #* (n #* k)";
+by (subgoal_tac "(natify(m) #* natify(n)) #* natify(k) = \
+\ natify(m) #* (natify(n) #* natify(k))" 1);
+by (res_inst_tac [("n","natify(m)")] nat_induct 2);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_mult_distrib])));
qed "mult_assoc";
(*for a/c rewriting*)
-Goal "[| m:nat; n:nat; k:nat |] ==> m #* (n #* k) = n #* (m #* k)";
+Goal "m #* (n #* k) = n #* (m #* k)";
by (rtac (mult_commute RS trans) 1);
-by (rtac (mult_assoc RS trans) 3);
-by (rtac (mult_commute RS subst_context) 6);
-by (REPEAT (ares_tac [mult_type] 1));
+by (rtac (mult_assoc RS trans) 1);
+by (rtac (mult_commute RS subst_context) 1);
qed "mult_left_commute";
val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
@@ -192,18 +346,22 @@
(*** Difference ***)
-Goal "m:nat ==> m #- m = 0";
-by (induct_tac "m" 1);
+Goal "m #- m = 0";
+by (subgoal_tac "natify(m) #- natify(m) = 0" 1);
+by (rtac (natify_in_nat RS nat_induct) 2);
by Auto_tac;
qed "diff_self_eq_0";
-(*Addition is the inverse of subtraction*)
+(**Addition is the inverse of subtraction**)
+
+(*We need m:nat even if we replace the RHS by natify(m), for consider e.g.
+ n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 ~= 0 = natify(m).*)
Goal "[| n le m; m:nat |] ==> n #+ (m#-n) = m";
by (ftac lt_nat_in_nat 1);
by (etac nat_succI 1);
by (etac rev_mp 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
qed "add_diff_inverse";
Goal "[| n le m; m:nat |] ==> (m#-n) #+ n = m";
@@ -212,7 +370,7 @@
by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1);
qed "add_diff_inverse2";
-(*Proof is IDENTICAL to that above*)
+(*Proof is IDENTICAL to that of add_diff_inverse*)
Goal "[| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)";
by (ftac lt_nat_in_nat 1);
by (etac nat_succI 1);
@@ -221,7 +379,7 @@
by (ALLGOALS Asm_simp_tac);
qed "diff_succ";
-Goal "[| m: nat; n: nat |] ==> 0 < n #- m <-> m<n";
+Goal "[| m: nat; n: nat |] ==> 0 < (n #- m) <-> m<n";
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (ALLGOALS Asm_simp_tac);
qed "zero_less_diff";
@@ -230,45 +388,52 @@
(** Subtraction is the inverse of addition. **)
-Goal "[| m:nat; n:nat |] ==> (n#+m) #- n = m";
-by (induct_tac "n" 1);
+Goal "(n#+m) #- n = natify(m)";
+by (subgoal_tac "(natify(n) #+ m) #- natify(n) = natify(m)" 1);
+by (res_inst_tac [("n","natify(n)")] nat_induct 2);
by Auto_tac;
qed "diff_add_inverse";
-Goal "[| m:nat; n:nat |] ==> (m#+n) #- n = m";
-by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1);
-by (REPEAT (ares_tac [diff_add_inverse] 1));
+Goal "(m#+n) #- n = natify(m)";
+by (simp_tac (simpset() addsimps [inst "m" "m" add_commute,
+ diff_add_inverse]) 1);
qed "diff_add_inverse2";
-Goal "[| k:nat; m: nat; n: nat |] ==> (k#+m) #- (k#+n) = m #- n";
-by (induct_tac "k" 1);
-by (ALLGOALS Asm_simp_tac);
+Goal "(k#+m) #- (k#+n) = m #- n";
+by (subgoal_tac "(natify(k) #+ natify(m)) #- (natify(k) #+ natify(n)) = \
+\ natify(m) #- natify(n)" 1);
+by (res_inst_tac [("n","natify(k)")] nat_induct 2);
+by Auto_tac;
qed "diff_cancel";
-Goal "[| k:nat; m: nat; n: nat |] ==> (m#+k) #- (n#+k) = m #- n";
-by (asm_simp_tac
- (simpset() addsimps [inst "n" "k" add_commute, diff_cancel]) 1);
+Goal "(m#+k) #- (n#+k) = m #- n";
+by (simp_tac (simpset() addsimps [inst "n" "k" add_commute, diff_cancel]) 1);
qed "diff_cancel2";
-Goal "[| m:nat; n:nat |] ==> n #- (n#+m) = 0";
-by (induct_tac "n" 1);
+Goal "n #- (n#+m) = 0";
+by (subgoal_tac "natify(n) #- (natify(n) #+ natify(m)) = 0" 1);
+by (res_inst_tac [("n","natify(n)")] nat_induct 2);
by Auto_tac;
qed "diff_add_0";
(** Difference distributes over multiplication **)
-Goal "[| m:nat; n: nat; k:nat |] ==> (m #- n) #* k = (m #* k) #- (n #* k)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
+Goal "(m #- n) #* k = (m #* k) #- (n #* k)";
+by (subgoal_tac "(natify(m) #- natify(n)) #* natify(k) = \
+\ (natify(m) #* natify(k)) #- (natify(n) #* natify(k))" 1);
+by (res_inst_tac [("m","natify(m)"),("n","natify(n)")] diff_induct 2);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [diff_cancel])));
qed "diff_mult_distrib" ;
-Goal "[| m:nat; n: nat; k:nat |] ==> k #* (m #- n) = (k #* m) #- (k #* n)";
-by (asm_simp_tac
+Goal "k #* (m #- n) = (k #* m) #- (k #* n)";
+by (simp_tac
(simpset() addsimps [inst "m" "k" mult_commute, diff_mult_distrib]) 1);
-qed "diff_mult_distrib2" ;
+qed "diff_mult_distrib2";
+
(*** Remainder ***)
+(*We need m:nat even with natify*)
Goal "[| 0<n; n le m; m:nat |] ==> m #- n < m";
by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
by (etac rev_mp 1);
@@ -390,20 +555,22 @@
(**** Additional theorems about "le" ****)
-Goal "[| m:nat; n:nat |] ==> m le m #+ n";
+Goal "m:nat ==> m le (m #+ n)";
by (induct_tac "m" 1);
by (ALLGOALS Asm_simp_tac);
qed "add_le_self";
-Goal "[| m:nat; n:nat |] ==> m le n #+ m";
+Goal "m:nat ==> m le (n #+ m)";
by (stac add_commute 1);
-by (REPEAT (ares_tac [add_le_self] 1));
+by (etac add_le_self 1);
qed "add_le_self2";
(*** Monotonicity of Addition ***)
-(*strict, in 1st argument; proof is by rule induction on 'less than'*)
-Goal "[| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
+(*strict, in 1st argument; proof is by rule induction on 'less than'.
+ Still need j:nat, for consider j = omega. Then we can have i<omega,
+ which is the same as i:nat, but natify(j)=0, so the conclusion fails.*)
+Goal "[| i<j; j:nat |] ==> i#+k < j#+k";
by (ftac lt_nat_in_nat 1);
by (assume_tac 1);
by (etac succ_lt_induct 1);
@@ -413,11 +580,11 @@
(*strict, in both arguments*)
Goal "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
by (rtac (add_lt_mono1 RS lt_trans) 1);
-by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
+by (REPEAT (assume_tac 1));
by (EVERY [stac add_commute 1,
- stac add_commute 3,
- rtac add_lt_mono1 5]);
-by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
+ stac add_commute 1,
+ rtac add_lt_mono1 1]);
+by (REPEAT (assume_tac 1));
qed "add_lt_mono";
(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
@@ -431,7 +598,7 @@
qed "Ord_lt_mono_imp_le_mono";
(*le monotonicity, 1st argument*)
-Goal "[| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
+Goal "[| i le j; j: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 nat_into_Ord] 1));
qed "add_le_mono1";
@@ -439,32 +606,34 @@
(* le monotonicity, BOTH arguments*)
Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
by (rtac (add_le_mono1 RS le_trans) 1);
-by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
+by (REPEAT (assume_tac 1));
by (EVERY [stac add_commute 1,
- stac add_commute 3,
- rtac add_le_mono1 5]);
-by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
+ stac add_commute 1,
+ rtac add_le_mono1 1]);
+by (REPEAT (assume_tac 1));
qed "add_le_mono";
(*** Monotonicity of Multiplication ***)
-Goal "[| i le j; j:nat; k:nat |] ==> i#*k le j#*k";
-by (ftac lt_nat_in_nat 1);
-by (induct_tac "k" 2);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
+Goal "[| i le j; j:nat |] ==> (i#*k) le (j#*k)";
+by (subgoal_tac "natify(i)#*natify(k) le j#*natify(k)" 1);
+by (ftac lt_nat_in_nat 2);
+by (res_inst_tac [("n","natify(k)")] nat_induct 3);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_le_mono])));
qed "mult_le_mono1";
(* le monotonicity, BOTH arguments*)
Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l";
by (rtac (mult_le_mono1 RS le_trans) 1);
-by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
+by (REPEAT (assume_tac 1));
by (EVERY [stac mult_commute 1,
- stac mult_commute 3,
- rtac mult_le_mono1 5]);
-by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
+ stac mult_commute 1,
+ rtac mult_le_mono1 1]);
+by (REPEAT (assume_tac 1));
qed "mult_le_mono";
-(*strict, in 1st argument; proof is by induction on k>0*)
+(*strict, in 1st argument; proof is by induction on k>0.
+ I can't see how to relax the typing conditions.*)
Goal "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
by (etac zero_lt_natE 1);
by (ftac lt_nat_in_nat 2);
@@ -473,17 +642,35 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
qed "mult_lt_mono2";
-Goal "[| i<j; 0<c; i:nat; j:nat; c:nat |] ==> i#*c < j#*c";
-by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, mult_commute]) 1);
+Goal "[| i<j; 0<k; j:nat; k:nat |] ==> i#*k < j#*k";
+by (asm_simp_tac (simpset() addsimps [mult_lt_mono2,
+ inst "n" "k" mult_commute]) 1);
qed "mult_lt_mono1";
-Goal "[| m: nat; n: nat |] ==> 0 < m#*n <-> 0<m & 0<n";
-by (best_tac (claset() addEs [natE] addss (simpset())) 1);
+Goal "m#+n = 0 <-> natify(m)=0 & natify(n)=0";
+by (subgoal_tac "natify(m) #+ natify(n) = 0 <-> natify(m)=0 & natify(n)=0" 1);
+by (res_inst_tac [("n","natify(m)")] natE 2);
+ by (res_inst_tac [("n","natify(n)")] natE 4);
+by Auto_tac;
+qed "add_eq_0_iff";
+AddIffs [add_eq_0_iff];
+
+Goal "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)";
+by (subgoal_tac "0 < natify(m)#*natify(n) <-> \
+\ 0 < natify(m) & 0 < natify(n)" 1);
+by (res_inst_tac [("n","natify(m)")] natE 2);
+ by (res_inst_tac [("n","natify(n)")] natE 4);
+ by (res_inst_tac [("n","natify(n)")] natE 3);
+by Auto_tac;
qed "zero_lt_mult_iff";
-Goal "[| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1";
-by (best_tac (claset() addEs [natE] addss (simpset())) 1);
+Goal "m#*n = 1 <-> natify(m)=1 & natify(n)=1";
+by (subgoal_tac "natify(m) #* natify(n) = 1 <-> natify(m)=1 & natify(n)=1" 1);
+by (res_inst_tac [("n","natify(m)")] natE 2);
+ by (res_inst_tac [("n","natify(n)")] natE 4);
+by Auto_tac;
qed "mult_eq_1_iff";
+AddIffs [zero_lt_mult_iff, mult_eq_1_iff];
(*Cancellation law for division*)
Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n";
@@ -512,21 +699,24 @@
qed "mult_mod_distrib";
(*Lemma for gcd*)
-Goal "[| m = m#*n; m: nat; n: nat |] ==> n=1 | m=0";
+Goal "m = m#*n ==> natify(n)=1 | m=0";
+by (subgoal_tac "m: nat" 1);
+by (etac ssubst 2);
by (rtac disjCI 1);
by (dtac sym 1);
by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
-by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 2);
+by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 3);
by Auto_tac;
+by (subgoal_tac "m #* n = 0" 1);
+by (stac (mult_natify2 RS sym) 2);
+by (auto_tac (claset(), simpset() delsimps [mult_natify2]));
qed "mult_eq_self_implies_10";
(*Thanks to Sten Agerholm*)
-Goal "[|k#+m le k#+n; k:nat |] ==> m le n";
-by (etac rev_mp 1);
-by (induct_tac "k" 1);
-by (Asm_simp_tac 1);
-by Safe_tac;
-by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt]) 1);
+Goal "[| k#+m le k#+n; m: nat; n: nat |] ==> m le n";
+by (res_inst_tac [("P", "natify(k)#+m le natify(k)#+n")] rev_mp 1);
+by (res_inst_tac [("n","natify(k)")] nat_induct 2);
+by Auto_tac;
qed "add_le_elim1";
Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
--- a/src/ZF/Arith.thy Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/Arith.thy Tue Aug 01 15:28:21 2000 +0200
@@ -6,38 +6,47 @@
Arithmetic operators and their definitions
*)
-Arith = Epsilon +
-
-setup setup_datatypes
+Arith = Univ +
-(*The natural numbers as a datatype*)
-rep_datatype
- elim natE
- induct nat_induct
- case_eqns nat_case_0, nat_case_succ
- recursor_eqns recursor_0, recursor_succ
+constdefs
+ pred :: i=>i (*inverse of succ*)
+ "pred(y) == THE x. y = succ(x)"
+ natify :: i=>i (*coerces non-nats to nats*)
+ "natify == Vrecursor(%f a. if a = succ(pred(a)) then succ(f`pred(a))
+ else 0)"
consts
- "#*" :: [i,i]=>i (infixl 70)
- div :: [i,i]=>i (infixl 70)
- mod :: [i,i]=>i (infixl 70)
- "#+" :: [i,i]=>i (infixl 65)
- "#-" :: [i,i]=>i (infixl 65)
+ "##*" :: [i,i]=>i (infixl 70)
+ "##+" :: [i,i]=>i (infixl 65)
+ "##-" :: [i,i]=>i (infixl 65)
primrec
- add_0 "0 #+ n = n"
- add_succ "succ(m) #+ n = succ(m #+ n)"
+ raw_add_0 "0 ##+ n = n"
+ raw_add_succ "succ(m) ##+ n = succ(m ##+ n)"
+
+primrec
+ raw_diff_0 "m ##- 0 = m"
+ raw_diff_succ "m ##- succ(n) = nat_case(0, %x. x, m ##- n)"
primrec
- diff_0 "m #- 0 = m"
- diff_SUCC "m #- succ(n) = nat_case(0, %x. x, m #- n)"
+ raw_mult_0 "0 ##* n = 0"
+ raw_mult_succ "succ(m) ##* n = n ##+ (m ##* n)"
+
+constdefs
+ add :: [i,i]=>i (infixl "#+" 65)
+ "m #+ n == natify(m) ##+ natify(n)"
+
+ diff :: [i,i]=>i (infixl "#-" 65)
+ "m #- n == natify(m) ##- natify(n)"
-primrec
- mult_0 "0 #* n = 0"
- mult_succ "succ(m) #* n = n #+ (m #* n)"
-
-defs
- mod_def "m mod n == transrec(m, %j f. if j<n then j else f`(j#-n))"
- div_def "m div n == transrec(m, %j f. if j<n then 0 else succ(f`(j#-n)))"
+ mult :: [i,i]=>i (infixl "#*" 70)
+ "m #* n == natify(m) ##* natify(n)"
+
+ div :: [i,i]=>i (infixl "div" 70)
+ "m div n == transrec(m, %j f. if j<n then 0 else succ(f`(j#-n)))"
+
+ mod :: [i,i]=>i (infixl "mod" 70)
+ "m mod n == transrec(m, %j f. if j<n then j else f`(j#-n))"
+
end
--- a/src/ZF/CardinalArith.ML Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/CardinalArith.ML Tue Aug 01 15:28:21 2000 +0200
@@ -404,9 +404,9 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2])));
qed "csquareD";
-Goalw [pred_def]
+Goalw [Order.pred_def]
"z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)";
-by (safe_tac (claset() delrules [SigmaI,succCI])); (*avoids using succCI,...*)
+by (safe_tac (claset() delrules [SigmaI, succCI]));
by (etac (csquareD RS conjE) 1);
by (rewtac lt_def);
by (ALLGOALS Blast_tac);
--- a/src/ZF/Finite.thy Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/Finite.thy Tue Aug 01 15:28:21 2000 +0200
@@ -6,7 +6,18 @@
Finite powerset operator
*)
-Finite = Arith + Inductive +
+Finite = Inductive + Nat +
+
+setup setup_datatypes
+
+(*The natural numbers as a datatype*)
+rep_datatype
+ elim natE
+ induct nat_induct
+ case_eqns nat_case_0, nat_case_succ
+ recursor_eqns recursor_0, recursor_succ
+
+
consts
Fin :: i=>i
FiniteFun :: [i,i]=>i ("(_ -||>/ _)" [61, 60] 60)
--- a/src/ZF/Inductive.thy Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/Inductive.thy Tue Aug 01 15:28:21 2000 +0200
@@ -1,5 +1,5 @@
(*Dummy theory to document dependencies *)
-Inductive = Fixedpt + Sum + QPair +
+Inductive = Fixedpt + mono +
end
--- a/src/ZF/Integ/Int.ML Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/Integ/Int.ML Tue Aug 01 15:28:21 2000 +0200
@@ -16,20 +16,6 @@
(*** Proving that intrel is an equivalence relation ***)
-(*By luck, requires no typing premises for y1, y2,y3*)
-val eqa::eqb::prems = goal Arith.thy
- "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2; \
-\ x1: nat; x2: nat; x3: nat |] ==> x1 #+ y3 = x3 #+ y1";
-by (cut_facts_tac prems 1);
-by (res_inst_tac [("k","x2")] add_left_cancel 1);
-by (rtac (add_left_commute RS trans) 1);
-by Auto_tac;
-by (stac eqb 1);
-by (rtac (add_left_commute RS trans) 1);
-by (stac eqa 3);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_left_commute])));
-qed "int_trans_lemma";
-
(** Natural deduction for intrel **)
Goalw [intrel_def]
@@ -64,6 +50,16 @@
AddSIs [intrelI];
AddSEs [intrelE];
+val eqa::eqb::prems = goal Arith.thy
+ "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
+by (res_inst_tac [("k","x2")] add_left_cancel 1);
+by (rtac (add_left_commute RS trans) 1);
+by Auto_tac;
+by (stac eqb 1);
+by (rtac (add_left_commute RS trans) 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [eqa, add_left_commute])));
+qed "int_trans_lemma";
+
Goalw [equiv_def, refl_def, sym_def, trans_def]
"equiv(nat*nat, intrel)";
by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
@@ -239,8 +235,7 @@
(*The rest should be trivial, but rearranging terms is hard;
add_ac does not help rewriting with the assumptions.*)
by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
-by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
-by Auto_tac;
+by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 1);
by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
qed "zadd_congruent2";
--- a/src/ZF/List.ML Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/List.ML Tue Aug 01 15:28:21 2000 +0200
@@ -216,7 +216,8 @@
by (ALLGOALS Asm_simp_tac);
qed "length_map";
-Goal "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
+Goal "[| xs: list(A); ys: list(A) |] \
+\ ==> length(xs@ys) = length(xs) #+ length(ys)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "length_app";
--- a/src/ZF/List.thy Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/List.thy Tue Aug 01 15:28:21 2000 +0200
@@ -10,7 +10,7 @@
although complicating its derivation.
*)
-List = Datatype +
+List = Datatype + Arith +
consts
list :: i=>i
--- a/src/ZF/ex/Acc.ML Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/ex/Acc.ML Tue Aug 01 15:28:21 2000 +0200
@@ -9,8 +9,6 @@
Research Report 92-49, LIP, ENS Lyon. Dec 1992.
*)
-open Acc;
-
(*The introduction rule must require a:field(r)
Otherwise acc(r) would be a proper class! *)
--- a/src/ZF/ex/Limit.ML Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/ex/Limit.ML Tue Aug 01 15:28:21 2000 +0200
@@ -1345,69 +1345,38 @@
(* ARITH_CONV proves the following in HOL. Would like something similar
in Isabelle/ZF. *)
-Goal "[|n:nat; m:nat|] ==> succ(m#+n)#-m = succ(n)";
-(*Uses add_succ_right the wrong way round!*)
+Goal "succ(m#+n)#-m = succ(natify(n))";
by (asm_simp_tac
- (simpset_of Nat.thy addsimps [add_succ_right RS sym, diff_add_inverse]) 1);
+ (simpset() delsimps [add_succ_right]
+ addsimps [add_succ_right RS sym, diff_add_inverse]) 1);
val lemma_succ_sub = result();
-Goalw [e_less_def] (* e_less_add *)
- "[|m:nat; k:nat|] ==> \
-\ e_less(DD,ee,m,succ(m#+k)) = (ee`(m#+k))O(e_less(DD,ee,m,m#+k))";
+Goalw [e_less_def]
+ "e_less(DD,ee,m,succ(m#+k)) = (ee`(m#+k))O(e_less(DD,ee,m,m#+k))";
by (asm_simp_tac (simpset() addsimps [lemma_succ_sub,diff_add_inverse]) 1);
qed "e_less_add";
-(* Again, would like more theorems about arithmetic. *)
-
Goal "n:nat ==> succ(n) = n #+ 1";
by (Asm_simp_tac 1);
qed "add1";
-Goal "x:nat ==> 0 < x --> succ(x #- 1)=x";
-by (induct_tac "x" 1);
-by Auto_tac;
-qed "succ_sub1";
-
-Goal (* succ_le_pos *)
- "[|m:nat; k:nat|] ==> succ(m) le m #+ k --> 0 < k";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "succ_le_pos";
-
-Goal "[|n:nat; m:nat|] ==> m le n --> (EX k:nat. n = m #+ k)";
-by (induct_tac "m" 1);
-by Safe_tac;
-by (rtac bexI 1);
-by (rtac (add_0 RS sym) 1);
-by (assume_tac 1);
-by (Asm_full_simp_tac 1);
-(* Great, by luck I found le_cs. Such cs's and ss's should be documented. *)
-by (fast_tac le_cs 1);
-by (asm_simp_tac
- (simpset_of Nat.thy addsimps[add_succ, add_succ_right RS sym]) 1);
-by (rtac bexI 1);
-by (stac (succ_sub1 RS mp) 1);
-(* Instantiation. *)
-by (rtac refl 3);
-by (assume_tac 1);
-by (rtac (succ_le_pos RS mp) 1);
-by (assume_tac 3); (* Instantiation *)
-by (ALLGOALS Asm_simp_tac);
+Goal "[| m le n; n: nat |] ==> EX k: nat. n = m #+ k";
+by (dtac less_imp_Suc_add 1);
+by Auto_tac;
val lemma_le_exists = result();
-val prems = goal thy (* le_exists *)
- "[|m le n; !!x. [|n=m#+x; x:nat|] ==> Q; m:nat; n:nat|] ==> Q";
-by (rtac (lemma_le_exists RS mp RS bexE) 1);
+val prems = Goal
+ "[| m le n; !!x. [|n=m#+x; x:nat|] ==> Q; n:nat |] ==> Q";
+by (rtac (lemma_le_exists RS bexE) 1);
by (DEPTH_SOLVE (ares_tac prems 1));
qed "le_exists";
-Goal (* e_less_le *)
- "[|m le n; m:nat; n:nat|] ==> \
-\ e_less(DD,ee,m,succ(n)) = ee`n O e_less(DD,ee,m,n)";
+Goal "[| m le n; n:nat |] ==> \
+\ e_less(DD,ee,m,succ(n)) = ee`n O e_less(DD,ee,m,n)";
by (rtac le_exists 1);
by (assume_tac 1);
by (asm_simp_tac(simpset() addsimps[e_less_add]) 1);
-by (REPEAT (assume_tac 1));
+by (assume_tac 1);
qed "e_less_le";
(* All theorems assume variables m and n are natural numbers. *)
@@ -1416,7 +1385,7 @@
by (asm_simp_tac(simpset() addsimps[e_less_le, e_less_eq]) 1);
qed "e_less_succ";
-val prems = Goal (* e_less_succ_emb *)
+val prems = Goal
"[|!!n. n:nat ==> emb(DD`n,DD`succ(n),ee`n); m:nat|] ==> \
\ e_less(DD,ee,m,succ(m)) = ee`m";
by (asm_simp_tac(simpset() addsimps e_less_succ::prems) 1);
@@ -1427,23 +1396,26 @@
(* Compare this proof with the HOL one, here we do type checking. *)
(* In any case the one below was very easy to write. *)
-Goal "[|emb_chain(DD,ee); m:nat; k:nat|] ==> \
-\ emb(DD`m,DD`(m#+k),e_less(DD,ee,m,m#+k))";
-by (induct_tac "k" 1);
-by (asm_simp_tac(simpset() addsimps[e_less_eq]) 1);
+Goal "[| emb_chain(DD,ee); m:nat |] ==> \
+\ emb(DD`m, DD`(m#+k), e_less(DD,ee,m,m#+k))";
+by (subgoal_tac "emb(DD`m, DD`(m#+natify(k)), e_less(DD,ee,m,m#+natify(k)))" 1);
+by (res_inst_tac [("n","natify(k)")] nat_induct 2);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps[e_less_eq])));
brr[emb_id,emb_chain_cpo] 1;
by (asm_simp_tac(simpset() addsimps[e_less_add]) 1);
by (auto_tac (claset() addIs [emb_comp,emb_chain_emb,emb_chain_cpo,add_type],
simpset()));
qed "emb_e_less_add";
-Goal "[|m le n; emb_chain(DD,ee); m:nat; n:nat|] ==> \
-\ emb(DD`m,DD`n,e_less(DD,ee,m,n))";
+Goal "[| m le n; emb_chain(DD,ee); n:nat |] ==> \
+\ emb(DD`m, DD`n, e_less(DD,ee,m,n))";
+by (ftac lt_nat_in_nat 1);
+by (etac nat_succI 1);
(* same proof as e_less_le *)
by (rtac le_exists 1);
by (assume_tac 1);
by (asm_simp_tac(simpset() addsimps[emb_e_less_add]) 1);
-by (REPEAT (assume_tac 1));
+by (assume_tac 1);
qed "emb_e_less";
Goal "[|f=f'; g=g'|] ==> f O g = f' O g'";
@@ -1752,20 +1724,17 @@
(* Arithmetic, little support in Isabelle/ZF. *)
-val prems = Goal (* le_exists_lemma *)
- "[|n le k; k le m; \
-\ !!p q. [|p le q; k=n#+p; m=n#+q; p:nat; q:nat|] ==> R; \
-\ m:nat; n:nat; k:nat|]==>R";
-by (rtac (hd prems RS le_exists) 1);
-by (rtac (le_exists) 1);
-by (rtac le_trans 1);
-(* Careful *)
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
+val [prem1,prem2,prem3,prem4] = Goal
+ "[| n le k; k le m; \
+\ !!p q. [|p le q; k=n#+p; m=n#+q; p:nat; q:nat|] ==> R; \
+\ m:nat |]==>R";
+by (rtac (prem1 RS le_exists) 1);
+by (simp_tac (simpset() addsimps [prem2 RS lt_nat_in_nat, prem4]) 2);
+by (rtac ([prem1,prem2] MRS le_trans RS le_exists) 1);
+by (rtac prem3 1);
by (assume_tac 2);
by (assume_tac 2);
-by (cut_facts_tac[hd prems,hd(tl prems)]1);
+by (cut_facts_tac [prem1,prem2] 1);
by (Asm_full_simp_tac 1);
by (etac add_le_elim1 1);
by (REPEAT (ares_tac prems 1));
--- a/src/ZF/ex/ListN.ML Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/ex/ListN.ML Tue Aug 01 15:28:21 2000 +0200
@@ -35,7 +35,8 @@
Goal "[| <n,l> : listn(A); <n',l'> : listn(A) |] ==> <n#+n', l@l'> : listn(A)";
by (etac listn.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps listn.intrs)));
+by (ftac (impOfSubs listn.dom_subset) 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps listn.intrs)));
qed "listn_append";
val Nil_listn_case = listn.mk_cases "<i,Nil> : listn(A)"
--- a/src/ZF/ex/Primes.ML Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/ex/Primes.ML Tue Aug 01 15:28:21 2000 +0200
@@ -8,8 +8,6 @@
eta_contract:=false;
-open Primes;
-
(************************************************)
(** Divides Relation **)
(************************************************)
@@ -125,10 +123,9 @@
(* if f divides a and b then f divides egcd(a,b) *)
Goalw [dvd_def] "[| f dvd a; f dvd b; 0<b |] ==> f dvd (a mod b)";
-by (safe_tac (claset() addSIs [mult_type, mod_type]));
+by (safe_tac (claset() addSIs [mod_type]));
ren "m n" 1;
-by (rtac (zero_lt_mult_iff RS iffD1 RS conjE) 1);
-by (REPEAT_SOME assume_tac);
+by (Asm_full_simp_tac 1);
by (res_inst_tac
[("x", "(((m div n)#*n #+ m mod n) #- ((f#*m) div (f#*n)) #* n)")]
bexI 1);
--- a/src/ZF/ex/Primrec.ML Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/ex/Primrec.ML Tue Aug 01 15:28:21 2000 +0200
@@ -137,7 +137,7 @@
by (rtac (ack2_le_ack1 RSN (2,lt_trans2)) 1);
by (Asm_simp_tac 1);
by (rtac (add_le_self RS ack_le_mono1 RS lt_trans1) 1);
-by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 5);
+by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 4);
by Auto_tac;
qed "ack_nest_bound";
@@ -265,7 +265,7 @@
(*final part of the simplification*)
by (Asm_simp_tac 1);
by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1);
-by (etac ack_lt_mono2 5);
+by (etac ack_lt_mono2 4);
by Auto_tac;
qed "PREC_case_lemma";