# HG changeset patch
# User paulson
# Date 864121442 -7200
# Node ID 406ae5ced4e9989a7201160eb18b5a5038bd2b38
# Parent  91b543ab091ba3a2f771939a292f501183739dbe
Renamed egcd and gcd; defined the gcd function using TFL

diff -r 91b543ab091b -r 406ae5ced4e9 src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Tue May 20 11:42:59 1997 +0200
+++ b/src/HOL/ex/Primes.ML	Tue May 20 11:44:02 1997 +0200
@@ -42,111 +42,95 @@
 (** Greatest Common Divisor                    **)
 (************************************************)
 
-(* GCD by Euclid's Algorithm *)
+(* Euclid's Algorithm *)
+
 
-val [rew] = goal HOL.thy "x==y ==> x=y";
-by (rewtac rew);
-by (rtac refl 1);
-qed "equals_reflection";
+Tfl.tgoalw thy [] gcd.rules;
+by (simp_tac (!simpset addsimps [mod_less_divisor,zero_less_eq]) 1);
+val tc = result();
 
-goal thy "(%n m. egcd m n) = wfrec (pred_nat^+)   \
-\                                  (%f n m. if n=0 then m else f (m mod n) n)";
-by (simp_tac (HOL_ss addsimps [egcd_def]) 1);
-val egcd_def1 = result() RS eq_reflection;
+val gcd_eq = tc RS hd gcd.rules;
+val gcd_induct = tc RS gcd.induct 
+                  |> read_instantiate [("P","split Q")]
+                  |> rewrite_rule [split RS eq_reflection]
+                  |> standard;
 
-goalw thy [egcd_def] "egcd m 0 = m";
-by (simp_tac (!simpset addsimps [wf_pred_nat RS wf_trancl RS wfrec]) 1);
-qed "egcd_0";
+goal thy "gcd(m,0) = m";
+by (rtac (gcd_eq RS trans) 1);
+by (Simp_tac 1);
+qed "gcd_0";
 
-goal thy "!!m. 0<n ==> egcd m n = egcd n (m mod n)";
-by (rtac (egcd_def1 RS wf_less_trans RS fun_cong) 1);
-by (asm_simp_tac (!simpset addsimps [mod_less_divisor, cut_apply, less_eq]) 1);
-qed "egcd_less_0";
-Addsimps [egcd_0, egcd_less_0];
+goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
+by (rtac (gcd_eq RS trans) 1);
+by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+qed "gcd_less_0";
+Addsimps [gcd_0, gcd_less_0];
 
-goal thy "(egcd m 0) dvd m";
+goal thy "gcd(m,0) dvd m";
 by (Simp_tac 1);
-qed "egcd_0_dvd_m";
+qed "gcd_0_dvd_m";
 
-goal thy "(egcd m 0) dvd 0";
+goal thy "gcd(m,0) dvd 0";
 by (Simp_tac 1);
-qed "egcd_0_dvd_0";
+qed "gcd_0_dvd_0";
 
 goalw thy [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m + n)";
-by (fast_tac (!claset addIs [add_mult_distrib2 RS sym]) 1);
+by (blast_tac (!claset addIs [add_mult_distrib2 RS sym]) 1);
 qed "dvd_add";
 
 goalw thy [dvd_def] "!!k. k dvd m ==> k dvd (q * m)";
-by (fast_tac (!claset addIs [mult_left_commute]) 1);
+by (blast_tac (!claset addIs [mult_left_commute]) 1);
 qed "dvd_mult";
 
-goal thy "!!k. [| k dvd n; k dvd (m mod n); 0 < n |] ==> k dvd m";
-by (deepen_tac 
-    (!claset addIs [mod_div_equality RS subst]
-             addSIs [dvd_add, dvd_mult]) 0 1);
-qed "gcd_ind";
+goal thy "!!k. [| k dvd (m mod n); k dvd n; n~=0 |] ==> k dvd m";
+by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
+by (asm_simp_tac (!simpset addsimps [dvd_add, dvd_mult]) 2);
+by (asm_full_simp_tac (!simpset addsimps [mod_div_equality, zero_less_eq]) 1);
+qed "gcd_recursion";
 
 
-(* Property 1: egcd m n divides m and n *)
-
-goal thy "ALL m. (egcd m n dvd m) & (egcd m n dvd n)";
-by (res_inst_tac [("n","n")] less_induct 1);
-by (rtac allI 1);
+(*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
+goal thy "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)";
+by (res_inst_tac [("v","m"),("v1.0","n")] gcd_induct 1);
 by (case_tac "n=0" 1);
-(* case n = 0 *)
-by (Asm_simp_tac 1);
-(* case n > 0 *)
-by (asm_full_simp_tac (!simpset addsimps [zero_less_eq RS sym]) 1);
-by (eres_inst_tac [("x","m mod n")] allE 1);
-by (asm_full_simp_tac (!simpset addsimps [mod_less_divisor]) 1);
-by (fast_tac (!claset addIs [gcd_ind]) 1);
-qed "egcd_prop1";
+by (ALLGOALS 
+    (asm_simp_tac (!simpset addsimps [mod_less_divisor,zero_less_eq])));
+by (blast_tac (!claset addDs [gcd_recursion]) 1);
+qed "gcd_divides_both";
 
 
-(* if f divides m and n then f divides egcd m n *)
-
-Delsimps [add_mult_distrib,add_mult_distrib2];
-
+(* if f divides m and n then f divides gcd(m,n) *)
 
 goalw thy [dvd_def] "!!m. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
 by (Step_tac 1);
-by (rtac (zero_less_mult_iff RS iffD1 RS conjE) 1);
-by (REPEAT_SOME assume_tac);
+by (full_simp_tac (!simpset addsimps [zero_less_mult_iff]) 1);
 by (res_inst_tac 
     [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] 
     exI 1);
-by (asm_simp_tac (!simpset addsimps [diff_mult_distrib2, div_cancel,
-                                     mult_mod_distrib, add_mult_distrib2,
-                                     diff_add_inverse]) 1);
+by (asm_simp_tac (!simpset addsimps [diff_mult_distrib2, 
+                                     mult_mod_distrib, add_mult_distrib2]) 1);
 qed "dvd_mod";
 
 
-(* Property 2: for all m,n,f naturals, 
-               if f divides m and f divides n then f divides egcd m n*)
-goal thy "!!k. ALL m. (f dvd m) & (f dvd k) --> f dvd egcd m k";
-by (res_inst_tac [("n","k")] less_induct 1);
-by (rtac allI 1);
+(*Maximality: for all m,n,f naturals, 
+                if f divides m and f divides n then f divides gcd(m,n)*)
+goal thy "!!k. (f dvd m) & (f dvd n) --> f dvd gcd(m,n)";
+by (res_inst_tac [("v","m"),("v1.0","n")] gcd_induct 1);
 by (case_tac "n=0" 1);
-(* case n = 0 *)
-by (Asm_simp_tac 1);
-(* case n > 0 *)
-by (Step_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [zero_less_eq RS sym]) 1);
-by (eres_inst_tac [("x","m mod n")] allE 1);
-by (asm_full_simp_tac (!simpset addsimps [mod_less_divisor]) 1);
-by (fast_tac (!claset addSIs [dvd_mod]) 1);
-qed "egcd_prop2";
+by (ALLGOALS 
+    (asm_simp_tac (!simpset addsimps [dvd_mod, mod_less_divisor,
+				      zero_less_eq])));
+qed_spec_mp "gcd_greatest";
 
-(* GCD PROOF : GCD exists and egcd fits the definition *)
+(* GCD PROOF : GCD exists and gcd fits the definition *)
 
-goalw thy [gcd_def] "gcd (egcd m n) m n";
-by (asm_simp_tac (!simpset addsimps [egcd_prop1]) 1);
-by (fast_tac (!claset addIs [egcd_prop2 RS spec RS mp]) 1);
-qed "gcd";
+goalw thy [is_gcd_def] "is_gcd (gcd(m,n)) m n";
+by (asm_simp_tac (!simpset addsimps [gcd_greatest, gcd_divides_both]) 1);
+qed "is_gcd";
 
 (* GCD is unique *)
 
-goalw thy [gcd_def] "gcd m a b & gcd n a b --> m=n";
-by (fast_tac (!claset addIs [dvd_anti_sym]) 1);
-qed "gcd_unique";
+goalw thy [is_gcd_def] "is_gcd m a b & is_gcd n a b --> m=n";
+by (blast_tac (!claset addIs [dvd_anti_sym]) 1);
+qed "is_gcd_unique";
 
diff -r 91b543ab091b -r 406ae5ced4e9 src/HOL/ex/Primes.thy
--- a/src/HOL/ex/Primes.thy	Tue May 20 11:42:59 1997 +0200
+++ b/src/HOL/ex/Primes.thy	Tue May 20 11:44:02 1997 +0200
@@ -3,28 +3,27 @@
     Author:     Christophe Tabacznyj and Lawrence C Paulson
     Copyright   1996  University of Cambridge
 
-The "divides" relation, the greatest common divisor and Euclid's algorithm
+The "divides" relation, the Greatest Common Divisor and Euclid's algorithm
 *)
 
-Primes = Arith +
+Primes = Arith + WF_Rel +
 consts
   dvd     :: [nat,nat]=>bool              (infixl 70) 
-  gcd     :: [nat,nat,nat]=>bool          (* great common divisor *)
-  egcd    :: [nat,nat]=>nat               (* gcd by Euclid's algorithm *)
-  coprime :: [nat,nat]=>bool              (* coprime definition *)
-  prime   :: nat=>bool                    (* prime definition *)
+  is_gcd  :: [nat,nat,nat]=>bool          (*gcd as a relation*)
+  gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
+  coprime :: [nat,nat]=>bool
+  prime   :: nat=>bool
   
+recdef gcd "measure ((%(x,y).y) ::nat*nat=>nat)"
+    "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
+
 defs
   dvd_def     "m dvd n == EX k. n = m*k"
 
-  gcd_def     "gcd p m n == ((p dvd m) & (p dvd n))   &
-               (ALL d. (d dvd m) & (d dvd n) --> d dvd p)"
+  is_gcd_def  "is_gcd p m n == p dvd m  &  p dvd n  &
+                               (ALL d. d dvd m & d dvd n --> d dvd p)"
 
-  egcd_def    "egcd m n ==   
-               wfrec (pred_nat^+)
-                     (%f n m. if n=0 then m else f (m mod n) n) n m"
-
-  coprime_def "coprime m n == egcd m n = 1"
+  coprime_def "coprime m n == gcd(m,n) = 1"
 
   prime_def   "prime(n) == (1<n) & (ALL m. 1<m & m<n --> ~(m dvd n))"