1.1 --- a/doc-src/TutorialI/Rules/Primes.thy	Fri Nov 02 08:26:01 2007 +0100
     1.2 +++ b/doc-src/TutorialI/Rules/Primes.thy	Fri Nov 02 08:59:15 2007 +0100
     1.3 @@ -4,11 +4,9 @@
     1.4  (*Euclid's algorithm 
     1.5    This material now appears AFTER that of Forward.thy *)
     1.6  theory Primes imports Main begin
     1.7 -consts
     1.8 -  gcd     :: "nat*nat \<Rightarrow> nat"
     1.9  
    1.10 -recdef gcd "measure snd"
    1.11 -    "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
    1.12 +fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    1.13 +  "gcd m n = (if n=0 then m else gcd n (m mod n))"
    1.14  
    1.15  
    1.16  ML "Pretty.setmargin 64"
    1.17 @@ -23,18 +21,18 @@
    1.18  
    1.19  (*** Euclid's Algorithm ***)
    1.20  
    1.21 -lemma gcd_0 [simp]: "gcd(m,0) = m"
    1.22 +lemma gcd_0 [simp]: "gcd m 0 = m"
    1.23  apply (simp);
    1.24  done
    1.25  
    1.26 -lemma gcd_non_0 [simp]: "0<n \<Longrightarrow> gcd(m,n) = gcd (n, m mod n)"
    1.27 +lemma gcd_non_0 [simp]: "0<n \<Longrightarrow> gcd m n = gcd n (m mod n)"
    1.28  apply (simp)
    1.29  done;
    1.30  
    1.31  declare gcd.simps [simp del];
    1.32  
    1.33  (*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
    1.34 -lemma gcd_dvd_both: "(gcd(m,n) dvd m) \<and> (gcd(m,n) dvd n)"
    1.35 +lemma gcd_dvd_both: "(gcd m n dvd m) \<and> (gcd m n dvd n)"
    1.36  apply (induct_tac m n rule: gcd.induct)
    1.37    --{* @{subgoals[display,indent=0,margin=65]} *}
    1.38  apply (case_tac "n=0")
    1.39 @@ -72,7 +70,7 @@
    1.40  (*Maximality: for all m,n,k naturals, 
    1.41                  if k divides m and k divides n then k divides gcd(m,n)*)
    1.42  lemma gcd_greatest [rule_format]:
    1.43 -      "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd(m,n)"
    1.44 +      "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd m n"
    1.45  apply (induct_tac m n rule: gcd.induct)
    1.46  apply (case_tac "n=0")
    1.47  txt{*subgoals after the case tac
    1.48 @@ -87,7 +85,7 @@
    1.49  *}
    1.50  
    1.51  (*just checking the claim that case_tac "n" works too*)
    1.52 -lemma "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd(m,n)"
    1.53 +lemma "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd m n"
    1.54  apply (induct_tac m n rule: gcd.induct)
    1.55  apply (case_tac "n")
    1.56  apply (simp_all add: dvd_mod)
    1.57 @@ -95,7 +93,7 @@
    1.58  
    1.59  
    1.60  theorem gcd_greatest_iff [iff]: 
    1.61 -        "(k dvd gcd(m,n)) = (k dvd m \<and> k dvd n)"
    1.62 +        "(k dvd gcd m n) = (k dvd m \<and> k dvd n)"
    1.63  by (blast intro!: gcd_greatest intro: dvd_trans)
    1.64  
    1.65  
    1.66 @@ -107,7 +105,7 @@
    1.67                       (ALL d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)"
    1.68  
    1.69  (*Function gcd yields the Greatest Common Divisor*)
    1.70 -lemma is_gcd: "is_gcd (gcd(m,n)) m n"
    1.71 +lemma is_gcd: "is_gcd (gcd m n) m n"
    1.72  apply (simp add: is_gcd_def gcd_greatest);
    1.73  done
    1.74  
    1.75 @@ -133,12 +131,12 @@
    1.76  \end{isabelle}
    1.77  *};
    1.78  
    1.79 -lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"
    1.80 +lemma gcd_assoc: "gcd (gcd k m) n = gcd k (gcd m n)"
    1.81    apply (rule is_gcd_unique)
    1.82    apply (rule is_gcd)
    1.83    apply (simp add: is_gcd_def);
    1.84    apply (blast intro: dvd_trans);
    1.85 -  done 
    1.86 +  done
    1.87  
    1.88  text{*
    1.89  \begin{isabelle}
    1.90 @@ -152,12 +150,12 @@
    1.91  *}
    1.92  
    1.93  
    1.94 -lemma gcd_dvd_gcd_mult: "gcd(m,n) dvd gcd(k*m, n)"
    1.95 +lemma gcd_dvd_gcd_mult: "gcd m n dvd gcd (k*m) n"
    1.96    apply (blast intro: dvd_trans);
    1.97    done
    1.98  
    1.99  (*This is half of the proof (by dvd_anti_sym) of*)
   1.100 -lemma gcd_mult_cancel: "gcd(k,n) = 1 \<Longrightarrow> gcd(k*m, n) = gcd(m,n)"
   1.101 +lemma gcd_mult_cancel: "gcd k n = 1 \<Longrightarrow> gcd (k*m) n = gcd m n"
   1.102    oops
   1.103  
   1.104  end