made mod_less_divisor a simplification rule.
--- a/src/HOL/Divides.ML Wed Apr 12 23:52:50 2000 +0200
+++ b/src/HOL/Divides.ML Thu Apr 13 10:30:28 2000 +0200
@@ -305,7 +305,7 @@
(*case na<n*)
by (Asm_simp_tac 1);
qed "mod_less_divisor";
-
+Addsimps [mod_less_divisor];
(** Evens and Odds **)
@@ -314,14 +314,14 @@
Goal "b<2 ==> (k mod 2 = b) | (k mod 2 = (if b=1 then 0 else 1))";
by (subgoal_tac "k mod 2 < 2" 1);
-by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
+by (Asm_simp_tac 2);
by (Asm_simp_tac 1);
by Safe_tac;
qed "mod2_cases";
Goal "Suc(Suc(m)) mod 2 = m mod 2";
by (subgoal_tac "m mod 2 < 2" 1);
-by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
+by (Asm_simp_tac 2);
by Safe_tac;
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc])));
qed "mod2_Suc_Suc";
@@ -329,8 +329,8 @@
Goal "(0 < m mod 2) = (m mod 2 = 1)";
by (subgoal_tac "m mod 2 < 2" 1);
-by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
-by Auto_tac;
+by (Asm_simp_tac 2);
+by (auto_tac (claset(), simpset() delsimps [mod_less_divisor]));
qed "mod2_gr_0";
Addsimps [mod2_gr_0];
--- a/src/HOL/Integ/NatBin.ML Wed Apr 12 23:52:50 2000 +0200
+++ b/src/HOL/Integ/NatBin.ML Thu Apr 13 10:30:28 2000 +0200
@@ -159,8 +159,7 @@
by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
by (Force_tac 2);
by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def,
- numeral_0_eq_0, zadd_int, zmult_int,
- mod_less_divisor]) 1);
+ numeral_0_eq_0, zadd_int, zmult_int]) 1);
by (rtac (mod_div_equality RS sym RS trans) 1);
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
qed "nat_div_distrib";
@@ -192,8 +191,7 @@
by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
by (Force_tac 2);
by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def,
- numeral_0_eq_0, zadd_int, zmult_int,
- mod_less_divisor]) 1);
+ numeral_0_eq_0, zadd_int, zmult_int]) 1);
by (rtac (mod_div_equality RS sym RS trans) 1);
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
qed "nat_mod_distrib";
--- a/src/HOL/ex/Primes.ML Wed Apr 12 23:52:50 2000 +0200
+++ b/src/HOL/ex/Primes.ML Thu Apr 13 10:30:28 2000 +0200
@@ -17,20 +17,14 @@
(*** Euclid's Algorithm ***)
-(** Prove the termination condition and remove it from the recursion equations
- and induction rule **)
+val [gcd_eq] = gcd.simps;
-Tfl.tgoalw thy [] gcd.simps;
-by (simp_tac (simpset() addsimps [mod_less_divisor]) 1);
-val tc = result();
-
-val gcd_eq = tc RS hd gcd.simps;
val prems = goal thy
"[| !!m. P m 0; \
\ !!m n. [| 0<n; P n (m mod n) |] ==> P m n \
\ |] ==> P m n";
-by (res_inst_tac [("u","m"),("v","n")] (tc RS gcd.induct) 1);
+by (res_inst_tac [("u","m"),("v","n")] gcd.induct 1);
by (case_tac "n=0" 1);
by (asm_simp_tac (simpset() addsimps prems) 1);
by Safe_tac;
@@ -39,16 +33,16 @@
Goal "gcd(m,0) = m";
-by (rtac (gcd_eq RS trans) 1);
by (Simp_tac 1);
qed "gcd_0";
Addsimps [gcd_0];
Goal "0<n ==> gcd(m,n) = gcd (n, m mod n)";
-by (rtac (gcd_eq RS trans) 1);
by (Asm_simp_tac 1);
qed "gcd_non_0";
+Delsimps gcd.simps;
+
Goal "gcd(m,1) = 1";
by (simp_tac (simpset() addsimps [gcd_non_0]) 1);
qed "gcd_1";
@@ -57,8 +51,7 @@
(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*)
Goal "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)";
by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
-by (ALLGOALS
- (asm_full_simp_tac (simpset() addsimps [gcd_non_0, mod_less_divisor])));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [gcd_non_0])));
by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1);
qed "gcd_dvd_both";
@@ -70,9 +63,7 @@
if f divides m and f divides n then f divides gcd(m,n)*)
Goal "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
-by (ALLGOALS
- (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod,
- mod_less_divisor])));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod])));
qed_spec_mp "gcd_greatest";
(*Function gcd yields the Greatest Common Divisor*)
--- a/src/HOL/ex/Primes.thy Wed Apr 12 23:52:50 2000 +0200
+++ b/src/HOL/ex/Primes.thy Thu Apr 13 10:30:28 2000 +0200
@@ -5,10 +5,8 @@
The Greatest Common Divisor and Euclid's algorithm
-The "simpset" clause in the recdef declaration is omitted on purpose:
- in order to demonstrate the treatment of definitions that have
- unproved termination conditions. Restoring the clause lets
- Isabelle prove those conditions.
+The "simpset" clause in the recdef declaration used to be necessary when the
+two lemmas where not part of the default simpset.
*)
Primes = Main +