--- a/src/ZF/Arith.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/Arith.ML Fri Sep 17 16:16:38 1993 +0200
@@ -29,10 +29,9 @@
goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
val rec_ss = ZF_ss
- addcongs (mk_typed_congs Arith.thy [("b", "[i,i]=>i")])
- addrews [nat_case_succ, nat_succI];
+ addsimps [nat_case_succ, nat_succI];
by (rtac rec_trans 1);
-by (SIMP_TAC rec_ss 1);
+by (simp_tac rec_ss 1);
val rec_succ = result();
val major::prems = goal Arith.thy
@@ -42,20 +41,12 @@
\ |] ==> rec(n,a,b) : C(n)";
by (rtac (major RS nat_induct) 1);
by (ALLGOALS
- (ASM_SIMP_TAC (ZF_ss addrews (prems@[rec_0,rec_succ]))));
+ (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
val rec_type = result();
-val prems = goalw Arith.thy [rec_def]
- "[| n=n'; a=a'; !!m z. b(m,z)=b'(m,z) \
-\ |] ==> rec(n,a,b)=rec(n',a',b')";
-by (SIMP_TAC (ZF_ss addcongs [transrec_cong,nat_case_cong]
- addrews (prems RL [sym])) 1);
-val rec_cong = result();
-
val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
-val nat_ss = ZF_ss addcongs [nat_case_cong,rec_cong]
- addrews ([rec_0,rec_succ] @ nat_typechecks);
+val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
(** Addition **)
@@ -101,16 +92,16 @@
"n:nat ==> 0 #- n = 0"
(fn [prem]=>
[ (rtac (prem RS nat_induct) 1),
- (ALLGOALS (ASM_SIMP_TAC nat_ss)) ]);
+ (ALLGOALS (asm_simp_tac nat_ss)) ]);
(*Must simplify BEFORE the induction!! (Else we get a critical pair)
succ(m) #- succ(n) rewrites to pred(succ(m) #- n) *)
val diff_succ_succ = prove_goalw Arith.thy [diff_def]
"[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n"
(fn prems=>
- [ (ASM_SIMP_TAC (nat_ss addrews prems) 1),
+ [ (asm_simp_tac (nat_ss addsimps prems) 1),
(nat_ind_tac "n" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
val prems = goal Arith.thy
"[| m:nat; n:nat |] ==> m #- n : succ(m)";
@@ -119,8 +110,8 @@
by (resolve_tac prems 1);
by (etac succE 3);
by (ALLGOALS
- (ASM_SIMP_TAC
- (nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
+ (asm_simp_tac
+ (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
val diff_leq = result();
(*** Simplification over add, mult, diff ***)
@@ -130,10 +121,7 @@
mult_0, mult_succ,
diff_0, diff_0_eq_0, diff_succ_succ];
-val arith_congs = mk_congs Arith.thy ["op #+", "op #-", "op #*"];
-
-val arith_ss = nat_ss addcongs arith_congs
- addrews (arith_rews@arith_typechecks);
+val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
(*** Addition ***)
@@ -142,7 +130,7 @@
"m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
(*The following two lemmas are used for add_commute and sometimes
elsewhere, since they are safe for rewriting.*)
@@ -150,13 +138,13 @@
"m:nat ==> m #+ 0 = m"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
val add_succ_right = prove_goal Arith.thy
"m:nat ==> m #+ succ(n) = succ(m #+ n)"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
(*Commutative law for addition*)
val add_commute = prove_goal Arith.thy
@@ -164,15 +152,15 @@
(fn prems=>
[ (nat_ind_tac "n" prems 1),
(ALLGOALS
- (ASM_SIMP_TAC
- (arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]);
+ (asm_simp_tac
+ (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
(*Cancellation law on the left*)
val [knat,eqn] = goal Arith.thy
"[| k:nat; k #+ m = k #+ n |] ==> m=n";
by (rtac (eqn RS rev_mp) 1);
by (nat_ind_tac "k" [knat] 1);
-by (ALLGOALS (SIMP_TAC arith_ss));
+by (ALLGOALS (simp_tac arith_ss));
by (fast_tac ZF_cs 1);
val add_left_cancel = result();
@@ -183,39 +171,40 @@
"m:nat ==> m #* 0 = 0"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
(*right successor law for multiplication*)
val mult_succ_right = prove_goal Arith.thy
- "[| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
- (fn prems=>
- [ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))),
+ "!!m n. [| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
+ (fn _=>
+ [ (nat_ind_tac "m" [] 1),
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
(*The final goal requires the commutative law for addition*)
- (REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1)) ]);
+ (rtac (add_commute RS subst_context) 1),
+ (REPEAT (assume_tac 1)) ]);
(*Commutative law for multiplication*)
val mult_commute = prove_goal Arith.thy
"[| m:nat; n:nat |] ==> m #* n = n #* m"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC
- (arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]);
+ (ALLGOALS (asm_simp_tac
+ (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
(*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 addrews ([add_assoc RS sym]@prems)))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
(*Distributive law on the left; requires an extra typing premise*)
val add_mult_distrib_left = prove_goal Arith.thy
"[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
(fn prems=>
let val mult_commute' = read_instantiate [("m","k")] mult_commute
- val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems)
- in [ (SIMP_TAC ss 1) ]
+ val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
+ in [ (simp_tac ss 1) ]
end);
(*Associative law for multiplication*)
@@ -223,7 +212,7 @@
"[| 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 addrews (prems@[add_mult_distrib])))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
(*** Difference ***)
@@ -232,7 +221,7 @@
"m:nat ==> m #- m = 0"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
val notless::prems = goal Arith.thy
@@ -241,8 +230,8 @@
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (resolve_tac prems 1);
by (resolve_tac prems 1);
-by (ALLGOALS (ASM_SIMP_TAC
- (arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
+by (ALLGOALS (asm_simp_tac
+ (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
naturals_are_ordinals]))));
val add_diff_inverse = result();
@@ -251,29 +240,24 @@
val [mnat,nnat] = goal Arith.thy
"[| m:nat; n:nat |] ==> (n#+m) #-n = m";
by (rtac (nnat RS nat_induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
val diff_add_inverse = result();
val [mnat,nnat] = goal Arith.thy
"[| m:nat; n:nat |] ==> n #- (n#+m) = 0";
by (rtac (nnat RS nat_induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
val diff_add_0 = result();
(*** Remainder ***)
(*In ordinary notation: if 0<n and n<=m then m-n < m *)
-val prems = goal Arith.thy
- "[| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m";
-by (cut_facts_tac prems 1);
+goal Arith.thy "!!m n. [| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m";
by (etac rev_mp 1);
by (etac rev_mp 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
-by (ALLGOALS (ASM_SIMP_TAC
- (nat_ss addrews (prems@[diff_leq,diff_succ_succ]))));
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
val div_termination = result();
val div_rls =
@@ -286,17 +270,17 @@
by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
val mod_type = result();
-val div_ss = ZF_ss addrews [naturals_are_ordinals,div_termination];
+val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
val prems = goal Arith.thy "[| 0:n; m:n; m:nat; n:nat |] ==> m mod n = m";
by (rtac (mod_def RS def_transrec RS trans) 1);
-by (SIMP_TAC (div_ss addrews prems) 1);
+by (simp_tac (div_ss addsimps prems) 1);
val mod_less = result();
val prems = goal Arith.thy
"[| 0:n; ~m:n; m:nat; n:nat |] ==> m mod n = (m#-n) mod n";
by (rtac (mod_def RS def_transrec RS trans) 1);
-by (SIMP_TAC (div_ss addrews prems) 1);
+by (simp_tac (div_ss addsimps prems) 1);
val mod_geq = result();
(*** Quotient ***)
@@ -310,13 +294,13 @@
val prems = goal Arith.thy
"[| 0:n; m:n; m:nat; n:nat |] ==> m div n = 0";
by (rtac (div_def RS def_transrec RS trans) 1);
-by (SIMP_TAC (div_ss addrews prems) 1);
+by (simp_tac (div_ss addsimps prems) 1);
val div_less = result();
val prems = goal Arith.thy
"[| 0:n; ~m:n; m:nat; n:nat |] ==> m div n = succ((m#-n) div n)";
by (rtac (div_def RS def_transrec RS trans) 1);
-by (SIMP_TAC (div_ss addrews prems) 1);
+by (simp_tac (div_ss addsimps prems) 1);
val div_geq = result();
(*Main Result.*)
@@ -326,8 +310,8 @@
by (resolve_tac prems 1);
by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
by (ALLGOALS
- (ASM_SIMP_TAC
- (arith_ss addrews ([mod_type,div_type] @ prems @
+ (asm_simp_tac
+ (arith_ss addsimps ([mod_type,div_type] @ prems @
[mod_less,mod_geq, div_less, div_geq,
add_assoc, add_diff_inverse, div_termination]))));
val mod_div_equality = result();
@@ -338,7 +322,7 @@
val [mnat,nnat] = goal Arith.thy
"[| m:nat; n:nat |] ==> ~ (m #+ n) : n";
by (rtac (mnat RS nat_induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl])));
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
by (rtac notI 1);
by (etac notE 1);
by (etac (succI1 RS Ord_trans) 1);