# HG changeset patch
# User nipkow
# Date 955614628 -7200
# Node ID 8812dad6ef12e14d32e23a0b20c2d867f1124109
# Parent  88dafea5955c43e13e48b17805bee41a78fe4bf9
made mod_less_divisor a simplification rule.

diff -r 88dafea5955c -r 8812dad6ef12 src/HOL/Divides.ML
--- 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];
 
diff -r 88dafea5955c -r 8812dad6ef12 src/HOL/Integ/NatBin.ML
--- 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";
diff -r 88dafea5955c -r 8812dad6ef12 src/HOL/ex/Primes.ML
--- 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*)
diff -r 88dafea5955c -r 8812dad6ef12 src/HOL/ex/Primes.thy
--- 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 +