--- a/src/ZF/ex/Integ.ML Tue Mar 26 12:01:13 1996 +0100
+++ b/src/ZF/ex/Integ.ML Tue Mar 26 16:16:24 1996 +0100
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-For integ.thy. The integers as equivalence classes over nat*nat.
+The integers as equivalence classes over nat*nat.
Could also prove...
"znegative(z) ==> $# zmagnitude(z) = $~ z"
@@ -93,7 +93,7 @@
(**** zminus: unary negation on integ ****)
goalw Integ.thy [congruent_def]
- "congruent(intrel, split(%x y. intrel``{<y,x>}))";
+ "congruent(intrel, %<x,y>. intrel``{<y,x>})";
by (safe_tac intrel_cs);
by (asm_full_simp_tac (intrel_ss addsimps add_ac) 1);
qed "zminus_congruent";
@@ -154,15 +154,15 @@
(**** zmagnitude: magnitide of an integer, as a natural number ****)
goalw Integ.thy [congruent_def]
- "congruent(intrel, split(%x y. (y#-x) #+ (x#-y)))";
+ "congruent(intrel, %<x,y>. (y#-x) #+ (x#-y))";
by (safe_tac intrel_cs);
by (ALLGOALS (asm_simp_tac intrel_ss));
by (etac rev_mp 1);
by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1 THEN
REPEAT (assume_tac 1));
-by (asm_simp_tac (intrel_ss addsimps [succ_inject_iff]) 3);
+by (asm_simp_tac intrel_ss 3);
by (asm_simp_tac (*this one's very sensitive to order of rewrites*)
- (arith_ss addsimps [diff_add_inverse,diff_add_0,add_0_right]) 2);
+ (arith_ss0 addsimps [diff_add_inverse,diff_add_0,add_0_right]) 2);
by (asm_simp_tac intrel_ss 1);
by (rtac impI 1);
by (etac subst 1);
--- a/src/ZF/ex/Limit.ML Tue Mar 26 12:01:13 1996 +0100
+++ b/src/ZF/ex/Limit.ML Tue Mar 26 16:16:24 1996 +0100
@@ -1705,9 +1705,10 @@
(* ARITH_CONV proves the following in HOL. Would like something similar
in Isabelle/ZF. *)
-val prems = goalw Arith.thy [] (* lemma_succ_sub *)
+goalw Arith.thy [] (* lemma_succ_sub *)
"!!z. [|n:nat; m:nat|] ==> succ(m#+n)#-m = succ(n)";
-by(asm_simp_tac(arith_ss addsimps [add_succ_right RS sym,diff_add_inverse])1);
+(*Uses add_succ_right the wrong way round!*)
+by(asm_simp_tac(nat_ss addsimps [add_succ_right RS sym, diff_add_inverse])1);
val lemma_succ_sub = result();
val prems = goalw Limit.thy [e_less_def] (* e_less_add *)
@@ -1755,7 +1756,7 @@
by(asm_full_simp_tac arith_ss 1);
(* Great, by luck I found lt_cs. Such cs's and ss's should be documented. *)
by(fast_tac lt_cs 1);
-by(asm_simp_tac (arith_ss addsimps[add_succ_right RS sym]) 1);
+by(asm_simp_tac (nat_ss addsimps[add_succ, add_succ_right RS sym]) 1);
by (rtac bexI 1);
br(succ_sub1 RS mp RS ssubst)1;
(* Instantiation. *)