# HG changeset patch
# User paulson
# Date 968055895 -7200
# Node ID c6eee0626d285769abb64d3aa881755a915c4649
# Parent  5873fc4ea3f9af1cc1b6db0b3aa50768480178bb
Converting HOL/ex/Primes.thy to new style, removing Primes.ML

diff -r 5873fc4ea3f9 -r c6eee0626d28 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Sep 04 09:40:28 2000 +0200
+++ b/src/HOL/IsaMakefile	Mon Sep 04 10:24:55 2000 +0200
@@ -432,7 +432,7 @@
 
 $(LOG)/HOL-ex.gz: $(OUT)/HOL  ex/AVL.ML ex/AVL.thy ex/BT.ML ex/BT.thy \
   ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML ex/NatSum.thy \
-  ex/Fib.ML ex/Fib.thy ex/Primes.ML ex/Primes.thy \
+  ex/Fib.ML ex/Fib.thy ex/Primes.thy \
   ex/Factorization.ML ex/Factorization.thy \
   ex/Primrec.ML ex/Primrec.thy \
   ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \
diff -r 5873fc4ea3f9 -r c6eee0626d28 src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Mon Sep 04 09:40:28 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,197 +0,0 @@
-(*  Title:      HOL/ex/Primes.ML
-    ID:         $Id$
-    Author:     Christophe Tabacznyj and Lawrence C Paulson
-    Copyright   1996  University of Cambridge
-
-The "divides" relation, the greatest common divisor and Euclid's algorithm
-
-See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992)
-*)
-
-eta_contract:=false;
-
-(************************************************)
-(** Greatest Common Divisor                    **)
-(************************************************)
-
-(*** Euclid's Algorithm ***)
-
-
-val [gcd_eq] = gcd.simps;
-
-
-val prems = goal thy
-     "[| !!m. P m 0;     \
-\        !!m n. [| 0<n;  P n (m mod n) |] ==> P m n  \
-\     |] ==> P (m::nat) (n::nat)";
-by (induct_thm_tac gcd.induct "m n" 1);
-by (case_tac "n=0" 1);
-by (asm_simp_tac (simpset() addsimps prems) 1);
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps prems) 1);
-qed "gcd_induct";
-
-
-Goal "gcd(m,0) = m";
-by (Simp_tac 1);
-qed "gcd_0";
-Addsimps [gcd_0];
-
-Goal "0<n ==> gcd(m,n) = gcd (n, m mod n)";
-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";
-Addsimps [gcd_1];
-
-(*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 (induct_thm_tac gcd_induct "m n" 1);
-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";
-
-bind_thm ("gcd_dvd1", gcd_dvd_both RS conjunct1);
-bind_thm ("gcd_dvd2", gcd_dvd_both RS conjunct2);
-
-
-(*Maximality: for all m,n,f naturals, 
-                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 (induct_thm_tac gcd_induct "m n" 1);
-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*)
-Goalw [is_gcd_def] "is_gcd (gcd(m,n)) m n";
-by (asm_simp_tac (simpset() addsimps [gcd_greatest, gcd_dvd_both]) 1);
-qed "is_gcd";
-
-(*uniqueness of GCDs*)
-Goalw [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";
-
-(*USED??*)
-Goalw [is_gcd_def]
-    "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m";
-by (Blast_tac 1);
-qed "is_gcd_dvd";
-
-(** Commutativity **)
-
-Goalw [is_gcd_def] "is_gcd k m n = is_gcd k n m";
-by (Blast_tac 1);
-qed "is_gcd_commute";
-
-Goal "gcd(m,n) = gcd(n,m)";
-by (rtac is_gcd_unique 1);
-by (rtac is_gcd 2);
-by (asm_simp_tac (simpset() addsimps [is_gcd, is_gcd_commute]) 1);
-qed "gcd_commute";
-
-Goal "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))";
-by (rtac is_gcd_unique 1);
-by (rtac is_gcd 2);
-by (rewtac is_gcd_def);
-by (blast_tac (claset() addSIs [gcd_dvd1, gcd_dvd2]
-   	                addIs  [gcd_greatest, dvd_trans]) 1);
-qed "gcd_assoc";
-
-Goal "gcd(0,m) = m";
-by (stac gcd_commute 1);
-by (rtac gcd_0 1);
-qed "gcd_0_left";
-
-Goal "gcd(1,m) = 1";
-by (stac gcd_commute 1);
-by (rtac gcd_1 1);
-qed "gcd_1_left";
-Addsimps [gcd_0_left, gcd_1_left];
-
-
-(** Multiplication laws **)
-
-(*Davenport, page 27*)
-Goal "k * gcd(m,n) = gcd(k*m, k*n)";
-by (induct_thm_tac gcd_induct "m n" 1);
-by (Asm_full_simp_tac 1);
-by (case_tac "k=0" 1);
- by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac
-    (simpset() addsimps [mod_geq, gcd_non_0, mod_mult_distrib2]) 1);
-qed "gcd_mult_distrib2";
-
-Goal "gcd(m,m) = m";
-by (cut_inst_tac [("k","m"),("m","1"),("n","1")] gcd_mult_distrib2 1);
-by (Asm_full_simp_tac 1);
-qed "gcd_self";
-Addsimps [gcd_self];
-
-Goal "gcd(k, k*n) = k";
-by (cut_inst_tac [("k","k"),("m","1"),("n","n")] gcd_mult_distrib2 1);
-by (Asm_full_simp_tac 1);
-qed "gcd_mult";
-Addsimps [gcd_mult];
-
-Goal "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
-by (subgoal_tac "m = gcd(m*k, m*n)" 1);
-by (etac ssubst 1 THEN rtac gcd_greatest 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym])));
-qed "relprime_dvd_mult";
-
-Goalw [prime_def] "[| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1";
-by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1);
-by Auto_tac;
-qed "prime_imp_relprime";
-
-(*This theorem leads immediately to a proof of the uniqueness of factorization.
-  If p divides a product of primes then it is one of those primes.*)
-Goal "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
-by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime]) 1);
-qed "prime_dvd_mult";
-
-
-(** Addition laws **)
-
-Goal "gcd(m, m+n) = gcd(m,n)";
-by (res_inst_tac [("n1", "m+n")] (gcd_commute RS ssubst) 1);
-by (rtac (gcd_eq RS trans) 1);
-by Auto_tac;
-by (asm_simp_tac (simpset() addsimps [mod_add_self1]) 1);
-by (stac gcd_commute 1);
-by (stac gcd_non_0 1);
-by Safe_tac;
-qed "gcd_add";
-
-Goal "gcd(m, n+m) = gcd(m,n)";
-by (asm_simp_tac (simpset() addsimps [add_commute, gcd_add]) 1);
-qed "gcd_add2";
-
-Goal "gcd(m, k*m+n) = gcd(m,n)";
-by (induct_tac "k" 1);
-by (asm_simp_tac (simpset() addsimps [gcd_add, add_assoc]) 2); 
-by (Simp_tac 1);
-qed "gcd_add_mult";
-
-
-(** More multiplication laws **)
-
-Goal "gcd(m,n) dvd gcd(k*m, n)";
-by (blast_tac (claset() addIs [gcd_greatest, dvd_trans, 
-                               gcd_dvd1, gcd_dvd2]) 1);
-qed "gcd_dvd_gcd_mult";
-
-Goal "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)";
-by (rtac dvd_anti_sym 1);
-by (rtac gcd_dvd_gcd_mult 2);
-by (rtac ([relprime_dvd_mult, gcd_dvd2] MRS gcd_greatest) 1);
-by (stac mult_commute 2);
-by (rtac gcd_dvd1 2);
-by (stac gcd_commute 1);
-by (asm_simp_tac (simpset() addsimps [gcd_assoc RS sym]) 1);
-qed "gcd_mult_cancel";
diff -r 5873fc4ea3f9 -r c6eee0626d28 src/HOL/ex/Primes.thy
--- a/src/HOL/ex/Primes.thy	Mon Sep 04 09:40:28 2000 +0200
+++ b/src/HOL/ex/Primes.thy	Mon Sep 04 10:24:55 2000 +0200
@@ -5,27 +5,209 @@
 
 The Greatest Common Divisor and Euclid's algorithm
 
-The "simpset" clause in the recdef declaration used to be necessary when the
-two lemmas where not part of the default simpset.
+See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992)
 *)
 
-Primes = Main +
+theory Primes = Main:
 consts
-  is_gcd  :: [nat,nat,nat]=>bool          (*gcd as a relation*)
   gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
-  coprime :: [nat,nat]=>bool
-  prime   :: nat set
-  
+
 recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
-(*  simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" *)
     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
 
-defs
-  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)"
+constdefs
+  is_gcd  :: "[nat,nat,nat]=>bool"        (*gcd as a relation*)
+    "is_gcd p m n == p dvd m  &  p dvd n  &
+                     (ALL d. d dvd m & d dvd n --> d dvd p)"
+
+  coprime :: "[nat,nat]=>bool"
+    "coprime m n == gcd(m,n) = 1"
+
+  prime   :: "nat set"
+    "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
+
+
+(************************************************)
+(** Greatest Common Divisor                    **)
+(************************************************)
+
+(*** Euclid's Algorithm ***)
+
+
+lemma gcd_induct:
+     "[| !!m. P m 0;     
+         !!m n. [| 0<n;  P n (m mod n) |] ==> P m n  
+      |] ==> P (m::nat) (n::nat)"
+  apply (rule_tac u="m" and v="n" in gcd.induct)
+  apply (case_tac "n=0")
+  apply (simp_all)
+  done
+
+
+lemma gcd_0 [simp]: "gcd(m,0) = m"
+  apply (simp);
+  done
+
+lemma gcd_non_0: "0<n ==> gcd(m,n) = gcd (n, m mod n)"
+  apply (simp)
+  done;
+
+declare gcd.simps [simp del];
+
+lemma gcd_1 [simp]: "gcd(m,1) = 1"
+  apply (simp add: gcd_non_0)
+  done
+
+(*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
+lemma gcd_dvd_both: "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"
+  apply (rule_tac m="m" and n="n" in gcd_induct)
+  apply (simp_all add: gcd_non_0)
+  apply (blast dest: dvd_mod_imp_dvd)
+  done
+
+lemmas gcd_dvd1 = gcd_dvd_both [THEN conjunct1];
+lemmas gcd_dvd2 = gcd_dvd_both [THEN conjunct2];
+
+
+(*Maximality: for all m,n,f naturals, 
+                if f divides m and f divides n then f divides gcd(m,n)*)
+lemma gcd_greatest [rulify]: "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"
+  apply (rule_tac m="m" and n="n" in gcd_induct)
+  apply (simp_all add: gcd_non_0 dvd_mod);
+  done;
+
+(*Function gcd yields the Greatest Common Divisor*)
+lemma is_gcd: "is_gcd (gcd(m,n)) m n"
+  apply (simp add: is_gcd_def gcd_greatest gcd_dvd_both);
+  done
+
+(*uniqueness of GCDs*)
+lemma is_gcd_unique: "[| is_gcd m a b; is_gcd n a b |] ==> m=n"
+  apply (simp add: is_gcd_def);
+  apply (blast intro: dvd_anti_sym)
+  done
+
+lemma is_gcd_dvd: "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"
+  apply (auto simp add: is_gcd_def);
+  done
+
+(** Commutativity **)
+
+lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
+  apply (auto simp add: is_gcd_def);
+  done
+
+lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
+  apply (rule is_gcd_unique)
+  apply (rule is_gcd)
+  apply (subst is_gcd_commute)
+  apply (simp add: is_gcd)
+  done
+
+lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"
+  apply (rule is_gcd_unique)
+  apply (rule is_gcd)
+  apply (simp add: is_gcd_def);
+  apply (blast intro!: gcd_dvd1 gcd_dvd2 intro: dvd_trans gcd_greatest);
+  done 
 
-  coprime_def "coprime m n == gcd(m,n) = 1"
+lemma gcd_0_left [simp]: "gcd(0,m) = m"
+  apply (simp add: gcd_commute [of 0])
+  done
+
+lemma gcd_1_left [simp]: "gcd(1,m) = 1"
+  apply (simp add: gcd_commute [of 1])
+  done
+
+
+(** Multiplication laws **)
+
+(*Davenport, page 27*)
+lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)"
+  apply (rule_tac m="m" and n="n" in gcd_induct)
+  apply (simp)
+  apply (case_tac "k=0")
+  apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
+  done
+
+lemma gcd_self [simp]: "gcd(m,m) = m"
+  apply (cut_tac k="m" and m="1" and n="1" in gcd_mult_distrib2)
+  apply (simp)
+(*alternative:
+proof -;
+  note gcd_mult_distrib2 [of m 1 1, simplify, THEN sym];
+      thus ?thesis; by assumption; qed; *)
+done
+
+lemma gcd_mult [simp]: "gcd(k, k*n) = k"
+  apply (cut_tac k="k" and m="1" and n="n" in gcd_mult_distrib2)
+  apply (simp)
+(*alternative:
+proof -;
+  note gcd_mult_distrib2 [of k 1 n, simplify, THEN sym];
+      thus ?thesis; by assumption; qed; *)
+done
+
+lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
+  apply (subgoal_tac "k dvd gcd(m*k, m*n)")
+   apply (subgoal_tac "gcd(m*k, m*n) = m")
+    apply (simp)
+   apply (simp add: gcd_mult_distrib2 [THEN sym]);
+  apply (rule gcd_greatest)
+   apply (simp_all)
+  done
 
-  prime_def   "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
+lemma prime_imp_relprime: "[| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1"
+  apply (simp add: prime_def);
+  apply (cut_tac m="p" and n="n" in gcd_dvd_both)
+  apply auto
+  done
+
+(*This theorem leads immediately to a proof of the uniqueness of factorization.
+  If p divides a product of primes then it is one of those primes.*)
+lemma prime_dvd_mult: "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"
+  apply (blast intro: relprime_dvd_mult prime_imp_relprime)
+  done
+
+
+(** Addition laws **)
+
+lemma gcd_add1 [simp]: "gcd(m+n, n) = gcd(m,n)"
+  apply (case_tac "n=0")
+  apply (simp_all add: gcd_non_0)
+  done
+
+lemma gcd_add2 [simp]: "gcd(m, m+n) = gcd(m,n)"
+  apply (rule gcd_commute [THEN trans])
+  apply (subst add_commute)
+  apply (simp add: gcd_add1)
+  apply (rule gcd_commute)
+  done
+
+lemma gcd_add2' [simp]: "gcd(m, n+m) = gcd(m,n)"
+  apply (subst add_commute)
+  apply (rule gcd_add2)
+  done
+
+lemma gcd_add_mult: "gcd(m, k*m+n) = gcd(m,n)"
+  apply (induct_tac "k")
+  apply (simp_all add: gcd_add2 add_assoc)
+  done
+
+
+(** More multiplication laws **)
+
+lemma gcd_dvd_gcd_mult: "gcd(m,n) dvd gcd(k*m, n)"
+  apply (blast intro: gcd_dvd2 gcd_dvd1 dvd_trans gcd_greatest);
+  done
+
+lemma gcd_mult_cancel: "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"
+  apply (rule dvd_anti_sym)
+   apply (rule gcd_greatest)
+    apply (rule_tac n="k" in relprime_dvd_mult)
+     apply (simp add: gcd_assoc)
+     apply (simp add: gcd_commute)
+    apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2 gcd_dvd_gcd_mult)
+  done
 
 end