--- a/NEWS Fri Jul 11 23:17:25 2008 +0200
+++ b/NEWS Mon Jul 14 11:04:42 2008 +0200
@@ -41,7 +41,20 @@
*** HOL ***
-* HOL-Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY.
+* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, zlcm (for int);
+carried together from various gcd/lcm developements in the HOL Distribution.
+zgcd and zlcm replace former igcd and ilcm; corresponding theorems renamed
+accordingly. INCOMPATIBILY. To recover tupled syntax, use syntax declarations like:
+
+ hide (open) const gcd
+ abbreviation gcd where
+ "gcd == (%(a, b). GCD.gcd a b)"
+ notation (output)
+ GCD.gcd ("gcd '(_, _')")
+
+(analogously for lcm, zgcd, zlcm).
+
+* HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY.
* Integrated image HOL-Complex with HOL. Entry points Main.thy and
Complex_Main.thy remain as they are.
--- a/src/HOL/Complex/ex/MIR.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Mon Jul 14 11:04:42 2008 +0200
@@ -642,9 +642,9 @@
done
recdef numgcdh "measure size"
- "numgcdh (C i) = (\<lambda>g. igcd i g)"
- "numgcdh (CN n c t) = (\<lambda>g. igcd c (numgcdh t g))"
- "numgcdh (CF c s t) = (\<lambda>g. igcd c (numgcdh t g))"
+ "numgcdh (C i) = (\<lambda>g. zgcd i g)"
+ "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"
+ "numgcdh (CF c s t) = (\<lambda>g. zgcd c (numgcdh t g))"
"numgcdh t = (\<lambda>g. 1)"
definition
@@ -687,13 +687,13 @@
shows "Inum bs t = 0"
proof-
have "\<And>x. numgcdh t x= 0 \<Longrightarrow> Inum bs t = 0"
- by (induct t rule: numgcdh.induct, auto simp add: igcd_def gcd_zero natabs0 max_def maxcoeff_pos)
+ by (induct t rule: numgcdh.induct, auto simp add: zgcd_def gcd_zero natabs0 max_def maxcoeff_pos)
thus ?thesis using g0[simplified numgcd_def] by blast
qed
lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
using gp
- by (induct t rule: numgcdh.induct, auto simp add: igcd_def)
+ by (induct t rule: numgcdh.induct, auto simp add: zgcd_def)
lemma numgcd_pos: "numgcd t \<ge>0"
by (simp add: numgcd_def numgcdh_pos maxcoeff_pos)
@@ -738,8 +738,8 @@
from ismaxcoeff_mono[OF H1 thh1] show ?case by (simp add: le_maxI1)
qed simp_all
-lemma igcd_gt1: "igcd i j > 1 \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"
- apply (unfold igcd_def)
+lemma zgcd_gt1: "zgcd i j > 1 \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"
+ apply (unfold zgcd_def)
apply (cases "i = 0", simp_all)
apply (cases "j = 0", simp_all)
apply (cases "abs i = 1", simp_all)
@@ -747,7 +747,7 @@
apply auto
done
lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow> m =0"
- by (induct t rule: numgcdh.induct, auto simp add:igcd0)
+ by (induct t rule: numgcdh.induct, auto simp add:zgcd0)
lemma dvdnumcoeff_aux:
assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"
@@ -756,17 +756,17 @@
proof(induct t rule: numgcdh.induct)
case (2 n c t)
let ?g = "numgcdh t m"
- from prems have th:"igcd c ?g > 1" by simp
- from igcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
+ from prems have th:"zgcd c ?g > 1" by simp
+ from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
moreover {assume "abs c > 1" and gp: "?g > 1" with prems
have th: "dvdnumcoeff t ?g" by simp
- have th': "igcd c ?g dvd ?g" by (simp add:igcd_dvd2)
- from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: igcd_dvd1)}
+ have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
+ from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
moreover {assume "abs c = 0 \<and> ?g > 1"
with prems have th: "dvdnumcoeff t ?g" by simp
- have th': "igcd c ?g dvd ?g" by (simp add:igcd_dvd2)
- from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: igcd_dvd1)
+ have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
+ from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
hence ?case by simp }
moreover {assume "abs c > 1" and g0:"?g = 0"
from numgcdh0[OF g0] have "m=0". with prems have ?case by simp }
@@ -774,22 +774,22 @@
next
case (3 c s t)
let ?g = "numgcdh t m"
- from prems have th:"igcd c ?g > 1" by simp
- from igcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
+ from prems have th:"zgcd c ?g > 1" by simp
+ from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
moreover {assume "abs c > 1" and gp: "?g > 1" with prems
have th: "dvdnumcoeff t ?g" by simp
- have th': "igcd c ?g dvd ?g" by (simp add:igcd_dvd2)
- from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: igcd_dvd1)}
+ have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
+ from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
moreover {assume "abs c = 0 \<and> ?g > 1"
with prems have th: "dvdnumcoeff t ?g" by simp
- have th': "igcd c ?g dvd ?g" by (simp add:igcd_dvd2)
- from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: igcd_dvd1)
+ have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
+ from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
hence ?case by simp }
moreover {assume "abs c > 1" and g0:"?g = 0"
from numgcdh0[OF g0] have "m=0". with prems have ?case by simp }
ultimately show ?case by blast
-qed(auto simp add: igcd_dvd1)
+qed(auto simp add: zgcd_dvd1)
lemma dvdnumcoeff_aux2:
assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
@@ -1041,7 +1041,7 @@
constdefs simp_num_pair:: "(num \<times> int) \<Rightarrow> num \<times> int"
"simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else
(let t' = simpnum t ; g = numgcd t' in
- if g > 1 then (let g' = igcd n g in
+ if g > 1 then (let g' = zgcd n g in
if g' = 1 then (t',n)
else (reducecoeffh t' g', n div g'))
else (t',n))))"
@@ -1052,23 +1052,23 @@
proof-
let ?t' = "simpnum t"
let ?g = "numgcd ?t'"
- let ?g' = "igcd n ?g"
+ let ?g' = "zgcd n ?g"
{assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
moreover
{ assume nnz: "n \<noteq> 0"
{assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
moreover
{assume g1:"?g>1" hence g0: "?g > 0" by simp
- from igcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
- hence g'p: "?g' > 0" using igcd_pos[where i="n" and j="numgcd ?t'"] by arith
+ from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
+ hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
hence "?g'= 1 \<or> ?g' > 1" by arith
moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
moreover {assume g'1:"?g'>1"
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
let ?tt = "reducecoeffh ?t' ?g'"
let ?t = "Inum bs ?tt"
- have gpdg: "?g' dvd ?g" by (simp add: igcd_dvd2)
- have gpdd: "?g' dvd n" by (simp add: igcd_dvd1)
+ have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
+ have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1)
have gpdgp: "?g' dvd ?g'" by simp
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
have th2:"real ?g' * ?t = Inum bs ?t'" by simp
@@ -1088,21 +1088,21 @@
proof-
let ?t' = "simpnum t"
let ?g = "numgcd ?t'"
- let ?g' = "igcd n ?g"
+ let ?g' = "zgcd n ?g"
{assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}
moreover
{ assume nnz: "n \<noteq> 0"
{assume "\<not> ?g > 1" hence ?thesis using prems by (auto simp add: Let_def simp_num_pair_def)}
moreover
{assume g1:"?g>1" hence g0: "?g > 0" by simp
- from igcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
- hence g'p: "?g' > 0" using igcd_pos[where i="n" and j="numgcd ?t'"] by arith
+ from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
+ hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
hence "?g'= 1 \<or> ?g' > 1" by arith
moreover {assume "?g'=1" hence ?thesis using prems
by (auto simp add: Let_def simp_num_pair_def)}
moreover {assume g'1:"?g'>1"
- have gpdg: "?g' dvd ?g" by (simp add: igcd_dvd2)
- have gpdd: "?g' dvd n" by (simp add: igcd_dvd1)
+ have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
+ have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1)
have gpdgp: "?g' dvd ?g'" by simp
from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
@@ -1219,7 +1219,7 @@
constdefs simpdvd:: "int \<Rightarrow> num \<Rightarrow> (int \<times> num)"
"simpdvd d t \<equiv>
(let g = numgcd t in
- if g > 1 then (let g' = igcd d g in
+ if g > 1 then (let g' = zgcd d g in
if g' = 1 then (d, t)
else (d div g',reducecoeffh t g'))
else (d, t))"
@@ -1228,20 +1228,20 @@
shows "Ifm bs (Dvd (fst (simpdvd d t)) (snd (simpdvd d t))) = Ifm bs (Dvd d t)"
proof-
let ?g = "numgcd t"
- let ?g' = "igcd d ?g"
+ let ?g' = "zgcd d ?g"
{assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simpdvd_def)}
moreover
{assume g1:"?g>1" hence g0: "?g > 0" by simp
- from igcd0 g1 dnz have gp0: "?g' \<noteq> 0" by simp
- hence g'p: "?g' > 0" using igcd_pos[where i="d" and j="numgcd t"] by arith
+ from zgcd0 g1 dnz have gp0: "?g' \<noteq> 0" by simp
+ hence g'p: "?g' > 0" using zgcd_pos[where i="d" and j="numgcd t"] by arith
hence "?g'= 1 \<or> ?g' > 1" by arith
moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simpdvd_def)}
moreover {assume g'1:"?g'>1"
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" ..
let ?tt = "reducecoeffh t ?g'"
let ?t = "Inum bs ?tt"
- have gpdg: "?g' dvd ?g" by (simp add: igcd_dvd2)
- have gpdd: "?g' dvd d" by (simp add: igcd_dvd1)
+ have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
+ have gpdd: "?g' dvd d" by (simp add: zgcd_dvd1)
have gpdgp: "?g' dvd ?g'" by simp
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
have th2:"real ?g' * ?t = Inum bs t" by simp
@@ -2093,8 +2093,8 @@
"plusinf p = p"
recdef \<delta> "measure size"
- "\<delta> (And p q) = ilcm (\<delta> p) (\<delta> q)"
- "\<delta> (Or p q) = ilcm (\<delta> p) (\<delta> q)"
+ "\<delta> (And p q) = zlcm (\<delta> p) (\<delta> q)"
+ "\<delta> (Or p q) = zlcm (\<delta> p) (\<delta> q)"
"\<delta> (Dvd i (CN 0 c e)) = i"
"\<delta> (NDvd i (CN 0 c e)) = i"
"\<delta> p = 1"
@@ -2126,20 +2126,20 @@
proof (induct p rule: iszlfm.induct)
case (1 p q)
let ?d = "\<delta> (And p q)"
- from prems ilcm_pos have dp: "?d >0" by simp
+ from prems zlcm_pos have dp: "?d >0" by simp
have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp
hence th: "d\<delta> p ?d"
- using delta_mono prems by (auto simp del: dvd_ilcm_self1)
+ using delta_mono prems by (auto simp del: dvd_zlcm_self1)
have "\<delta> q dvd \<delta> (And p q)" using prems by simp
- hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: dvd_ilcm_self2)
+ hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: dvd_zlcm_self2)
from th th' dp show ?case by simp
next
case (2 p q)
let ?d = "\<delta> (And p q)"
- from prems ilcm_pos have dp: "?d >0" by simp
+ from prems zlcm_pos have dp: "?d >0" by simp
have "\<delta> p dvd \<delta> (And p q)" using prems by simp hence th: "d\<delta> p ?d" using delta_mono prems
- by (auto simp del: dvd_ilcm_self1)
- have "\<delta> q dvd \<delta> (And p q)" using prems by simp hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: dvd_ilcm_self2)
+ by (auto simp del: dvd_zlcm_self1)
+ have "\<delta> q dvd \<delta> (And p q)" using prems by simp hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: dvd_zlcm_self2)
from th th' dp show ?case by simp
qed simp_all
@@ -2388,8 +2388,8 @@
"d\<beta> p = (\<lambda> k. True)"
recdef \<zeta> "measure size"
- "\<zeta> (And p q) = ilcm (\<zeta> p) (\<zeta> q)"
- "\<zeta> (Or p q) = ilcm (\<zeta> p) (\<zeta> q)"
+ "\<zeta> (And p q) = zlcm (\<zeta> p) (\<zeta> q)"
+ "\<zeta> (Or p q) = zlcm (\<zeta> p) (\<zeta> q)"
"\<zeta> (Eq (CN 0 c e)) = c"
"\<zeta> (NEq (CN 0 c e)) = c"
"\<zeta> (Lt (CN 0 c e)) = c"
@@ -2510,19 +2510,19 @@
using linp
proof(induct p rule: iszlfm.induct)
case (1 p q)
- from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
- from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
- from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"]
- d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"]
- dl1 dl2 show ?case by (auto simp add: ilcm_pos)
+ from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
+ from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
+ from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"]
+ d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"]
+ dl1 dl2 show ?case by (auto simp add: zlcm_pos)
next
case (2 p q)
- from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
- from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
- from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"]
- d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"]
- dl1 dl2 show ?case by (auto simp add: ilcm_pos)
-qed (auto simp add: ilcm_pos)
+ from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
+ from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
+ from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"]
+ d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"]
+ dl1 dl2 show ?case by (auto simp add: zlcm_pos)
+qed (auto simp add: zlcm_pos)
lemma a\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d\<beta> p l" and lp: "l > 0"
shows "iszlfm (a\<beta> p l) (a #bs) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm (real (l * x) #bs) (a\<beta> p l) = Ifm ((real x)#bs) p)"
@@ -4171,9 +4171,9 @@
lemma bound0at_l : "\<lbrakk>isatom p ; bound0 p\<rbrakk> \<Longrightarrow> isrlfm p"
by (induct p rule: isrlfm.induct, auto)
-lemma igcd_le1: assumes ip: "0 < i" shows "igcd i j \<le> i"
+lemma zgcd_le1: assumes ip: "0 < i" shows "zgcd i j \<le> i"
proof-
- from igcd_dvd1 have th: "igcd i j dvd i" by blast
+ from zgcd_dvd1 have th: "zgcd i j dvd i" by blast
from zdvd_imp_le[OF th ip] show ?thesis .
qed
@@ -4195,7 +4195,7 @@
with numgcd_pos[where t="CN 0 c (simpnum e)"]
have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
- by (simp add: numgcd_def igcd_le1)
+ by (simp add: numgcd_def zgcd_le1)
from prems have th': "c\<noteq>0" by auto
from prems have cp: "c \<ge> 0" by simp
from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
@@ -4220,7 +4220,7 @@
with numgcd_pos[where t="CN 0 c (simpnum e)"]
have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
- by (simp add: numgcd_def igcd_le1)
+ by (simp add: numgcd_def zgcd_le1)
from prems have th': "c\<noteq>0" by auto
from prems have cp: "c \<ge> 0" by simp
from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
@@ -4245,7 +4245,7 @@
with numgcd_pos[where t="CN 0 c (simpnum e)"]
have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
- by (simp add: numgcd_def igcd_le1)
+ by (simp add: numgcd_def zgcd_le1)
from prems have th': "c\<noteq>0" by auto
from prems have cp: "c \<ge> 0" by simp
from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
@@ -4270,7 +4270,7 @@
with numgcd_pos[where t="CN 0 c (simpnum e)"]
have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
- by (simp add: numgcd_def igcd_le1)
+ by (simp add: numgcd_def zgcd_le1)
from prems have th': "c\<noteq>0" by auto
from prems have cp: "c \<ge> 0" by simp
from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
@@ -4295,7 +4295,7 @@
with numgcd_pos[where t="CN 0 c (simpnum e)"]
have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
- by (simp add: numgcd_def igcd_le1)
+ by (simp add: numgcd_def zgcd_le1)
from prems have th': "c\<noteq>0" by auto
from prems have cp: "c \<ge> 0" by simp
from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
@@ -4320,7 +4320,7 @@
with numgcd_pos[where t="CN 0 c (simpnum e)"]
have th1:"numgcd (CN 0 c (simpnum e)) > 0" by simp
from prems have th:"numgcd (CN 0 c (simpnum e)) \<le> c"
- by (simp add: numgcd_def igcd_le1)
+ by (simp add: numgcd_def zgcd_le1)
from prems have th': "c\<noteq>0" by auto
from prems have cp: "c \<ge> 0" by simp
from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
@@ -5117,9 +5117,9 @@
let ?M = "?I x (minusinf ?rq)"
let ?P = "?I x (plusinf ?rq)"
have MF: "?M = False"
- apply (simp add: Let_def reducecoeff_def numgcd_def igcd_def rsplit_def ge_def lt_def conj_def disj_def)
+ apply (simp add: Let_def reducecoeff_def numgcd_def zgcd_def rsplit_def ge_def lt_def conj_def disj_def)
by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
- have PF: "?P = False" apply (simp add: Let_def reducecoeff_def numgcd_def igcd_def rsplit_def ge_def lt_def conj_def disj_def)
+ have PF: "?P = False" apply (simp add: Let_def reducecoeff_def numgcd_def zgcd_def rsplit_def ge_def lt_def conj_def disj_def)
by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
have "(\<exists> x. ?I x ?q ) =
((?I x (minusinf ?rq)) \<or> (?I x (plusinf ?rq )) \<or> (\<exists> (t,n) \<in> set (\<Upsilon> ?rq). \<exists> (s,m) \<in> set (\<Upsilon> ?rq ). ?I x (\<upsilon> ?rq (Add (Mul m t) (Mul n s), 2*n*m))))"
@@ -5284,7 +5284,7 @@
let ?F = "\<lambda> p. \<exists> a \<in> set (\<Upsilon> p). \<exists> b \<in> set (\<Upsilon> p). ?I x (\<upsilon> p (?g(a,b)))"
let ?ep = "evaldjf (\<upsilon> ?q) ?Y"
from rlfm_l[OF qf] have lq: "isrlfm ?q"
- by (simp add: rsplit_def lt_def ge_def conj_def disj_def Let_def reducecoeff_def numgcd_def igcd_def)
+ by (simp add: rsplit_def lt_def ge_def conj_def disj_def Let_def reducecoeff_def numgcd_def zgcd_def)
from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp
from \<Upsilon>_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
from U_l UpU
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Mon Jul 14 11:04:42 2008 +0200
@@ -478,8 +478,8 @@
by (induct t rule: maxcoeff.induct, auto)
recdef numgcdh "measure size"
- "numgcdh (C i) = (\<lambda>g. igcd i g)"
- "numgcdh (CN n c t) = (\<lambda>g. igcd c (numgcdh t g))"
+ "numgcdh (C i) = (\<lambda>g. zgcd i g)"
+ "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"
"numgcdh t = (\<lambda>g. 1)"
defs numgcd_def [code func]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
@@ -512,11 +512,11 @@
assumes g0: "numgcd t = 0"
shows "Inum bs t = 0"
using g0[simplified numgcd_def]
- by (induct t rule: numgcdh.induct, auto simp add: igcd_def gcd_zero natabs0 max_def maxcoeff_pos)
+ by (induct t rule: numgcdh.induct, auto simp add: zgcd_def gcd_zero natabs0 max_def maxcoeff_pos)
lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
using gp
- by (induct t rule: numgcdh.induct, auto simp add: igcd_def)
+ by (induct t rule: numgcdh.induct, auto simp add: zgcd_def)
lemma numgcd_pos: "numgcd t \<ge>0"
by (simp add: numgcd_def numgcdh_pos maxcoeff_pos)
@@ -551,15 +551,15 @@
from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1)
qed simp_all
-lemma igcd_gt1: "igcd i j > 1 \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"
- apply (cases "abs i = 0", simp_all add: igcd_def)
+lemma zgcd_gt1: "zgcd i j > 1 \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"
+ apply (cases "abs i = 0", simp_all add: zgcd_def)
apply (cases "abs j = 0", simp_all)
apply (cases "abs i = 1", simp_all)
apply (cases "abs j = 1", simp_all)
apply auto
done
lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow> m =0"
- by (induct t rule: numgcdh.induct, auto simp add:igcd0)
+ by (induct t rule: numgcdh.induct, auto simp add:zgcd0)
lemma dvdnumcoeff_aux:
assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"
@@ -568,22 +568,22 @@
proof(induct t rule: numgcdh.induct)
case (2 n c t)
let ?g = "numgcdh t m"
- from prems have th:"igcd c ?g > 1" by simp
- from igcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
+ from prems have th:"zgcd c ?g > 1" by simp
+ from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
moreover {assume "abs c > 1" and gp: "?g > 1" with prems
have th: "dvdnumcoeff t ?g" by simp
- have th': "igcd c ?g dvd ?g" by (simp add:igcd_dvd2)
- from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: igcd_dvd1)}
+ have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
+ from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
moreover {assume "abs c = 0 \<and> ?g > 1"
with prems have th: "dvdnumcoeff t ?g" by simp
- have th': "igcd c ?g dvd ?g" by (simp add:igcd_dvd2)
- from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: igcd_dvd1)
+ have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
+ from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
hence ?case by simp }
moreover {assume "abs c > 1" and g0:"?g = 0"
from numgcdh0[OF g0] have "m=0". with prems have ?case by simp }
ultimately show ?case by blast
-qed(auto simp add: igcd_dvd1)
+qed(auto simp add: zgcd_dvd1)
lemma dvdnumcoeff_aux2:
assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
@@ -727,7 +727,7 @@
constdefs simp_num_pair:: "(num \<times> int) \<Rightarrow> num \<times> int"
"simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else
(let t' = simpnum t ; g = numgcd t' in
- if g > 1 then (let g' = igcd n g in
+ if g > 1 then (let g' = zgcd n g in
if g' = 1 then (t',n)
else (reducecoeffh t' g', n div g'))
else (t',n))))"
@@ -738,23 +738,23 @@
proof-
let ?t' = "simpnum t"
let ?g = "numgcd ?t'"
- let ?g' = "igcd n ?g"
+ let ?g' = "zgcd n ?g"
{assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
moreover
{ assume nnz: "n \<noteq> 0"
{assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}
moreover
{assume g1:"?g>1" hence g0: "?g > 0" by simp
- from igcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
- hence g'p: "?g' > 0" using igcd_pos[where i="n" and j="numgcd ?t'"] by arith
+ from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
+ hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
hence "?g'= 1 \<or> ?g' > 1" by arith
moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}
moreover {assume g'1:"?g'>1"
from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
let ?tt = "reducecoeffh ?t' ?g'"
let ?t = "Inum bs ?tt"
- have gpdg: "?g' dvd ?g" by (simp add: igcd_dvd2)
- have gpdd: "?g' dvd n" by (simp add: igcd_dvd1)
+ have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
+ have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1)
have gpdgp: "?g' dvd ?g'" by simp
from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
have th2:"real ?g' * ?t = Inum bs ?t'" by simp
@@ -774,21 +774,21 @@
proof-
let ?t' = "simpnum t"
let ?g = "numgcd ?t'"
- let ?g' = "igcd n ?g"
+ let ?g' = "zgcd n ?g"
{assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}
moreover
{ assume nnz: "n \<noteq> 0"
{assume "\<not> ?g > 1" hence ?thesis using prems by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
moreover
{assume g1:"?g>1" hence g0: "?g > 0" by simp
- from igcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
- hence g'p: "?g' > 0" using igcd_pos[where i="n" and j="numgcd ?t'"] by arith
+ from zgcd0 g1 nnz have gp0: "?g' \<noteq> 0" by simp
+ hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
hence "?g'= 1 \<or> ?g' > 1" by arith
moreover {assume "?g'=1" hence ?thesis using prems
by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
moreover {assume g'1:"?g'>1"
- have gpdg: "?g' dvd ?g" by (simp add: igcd_dvd2)
- have gpdd: "?g' dvd n" by (simp add: igcd_dvd1)
+ have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
+ have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1)
have gpdgp: "?g' dvd ?g'" by simp
from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
--- a/src/HOL/Complex/ex/Sqrt.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/Complex/ex/Sqrt.thy Mon Jul 14 11:04:42 2008 +0200
@@ -23,16 +23,16 @@
theorem rationals_rep [elim?]:
assumes "x \<in> \<rat>"
- obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd (m, n) = 1"
+ obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
proof -
from `x \<in> \<rat>` obtain m n :: nat where
n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
unfolding rationals_def by blast
- let ?gcd = "gcd (m, n)"
+ let ?gcd = "gcd m n"
from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
let ?k = "m div ?gcd"
let ?l = "n div ?gcd"
- let ?gcd' = "gcd (?k, ?l)"
+ let ?gcd' = "gcd ?k ?l"
have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
by (rule dvd_mult_div_cancel)
have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
@@ -52,7 +52,7 @@
moreover
have "?gcd' = 1"
proof -
- have "?gcd * ?gcd' = gcd (?gcd * ?k, ?gcd * ?l)"
+ have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
by (rule gcd_mult_distrib2)
with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
with gcd show ?thesis by simp
@@ -76,7 +76,7 @@
assume "sqrt (real p) \<in> \<rat>"
then obtain m n where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
- and gcd: "gcd (m, n) = 1" ..
+ and gcd: "gcd m n = 1" ..
have eq: "m\<twosuperior> = p * n\<twosuperior>"
proof -
from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
@@ -96,7 +96,7 @@
then have "p dvd n\<twosuperior>" ..
with `prime p` show "p dvd n" by (rule prime_dvd_power_two)
qed
- then have "p dvd gcd (m, n)" ..
+ then have "p dvd gcd m n" ..
with gcd have "p dvd 1" by simp
then have "p \<le> 1" by (simp add: dvd_imp_le)
with p show False by simp
@@ -122,7 +122,7 @@
assume "sqrt (real p) \<in> \<rat>"
then obtain m n where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
- and gcd: "gcd (m, n) = 1" ..
+ and gcd: "gcd m n = 1" ..
from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
by (auto simp add: power2_eq_square)
@@ -136,7 +136,7 @@
with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
then have "p dvd n\<twosuperior>" ..
with `prime p` have "p dvd n" by (rule prime_dvd_power_two)
- with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest)
+ with dvd_m have "p dvd gcd m n" by (rule gcd_greatest)
with gcd have "p dvd 1" by simp
then have "p \<le> 1" by (simp add: dvd_imp_le)
with p show False by simp
--- a/src/HOL/Isar_examples/Fibonacci.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy Mon Jul 14 11:04:42 2008 +0200
@@ -70,55 +70,55 @@
finally show "?P (n + 2)" .
qed
-lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n")
+lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1" (is "?P n")
proof (induct n rule: fib_induct)
show "?P 0" by simp
show "?P 1" by simp
fix n
have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
by simp
- also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"
+ also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))"
by (simp only: gcd_add2')
- also have "... = gcd (fib (n + 1), fib (n + 1 + 1))"
+ also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))"
by (simp add: gcd_commute)
also assume "... = 1"
finally show "?P (n + 2)" .
qed
-lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)"
+lemma gcd_mult_add: "0 < n ==> gcd (n * k + m) n = gcd m n"
proof -
assume "0 < n"
- then have "gcd (n * k + m, n) = gcd (n, m mod n)"
+ then have "gcd (n * k + m) n = gcd n (m mod n)"
by (simp add: gcd_non_0 add_commute)
- also from `0 < n` have "... = gcd (m, n)" by (simp add: gcd_non_0)
+ also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0)
finally show ?thesis .
qed
-lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
+lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
proof (cases m)
case 0
then show ?thesis by simp
next
case (Suc k)
- then have "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))"
+ then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
by (simp add: gcd_commute)
also have "fib (n + k + 1)
= fib (k + 1) * fib (n + 1) + fib k * fib n"
by (rule fib_add)
- also have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))"
+ also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
by (simp add: gcd_mult_add)
- also have "... = gcd (fib n, fib (k + 1))"
+ also have "... = gcd (fib n) (fib (k + 1))"
by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
- also have "... = gcd (fib m, fib n)"
+ also have "... = gcd (fib m) (fib n)"
using Suc by (simp add: gcd_commute)
finally show ?thesis .
qed
lemma gcd_fib_diff:
assumes "m <= n"
- shows "gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
+ shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
proof -
- have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))"
+ have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
by (simp add: gcd_fib_add)
also from `m <= n` have "n - m + m = n" by simp
finally show ?thesis .
@@ -126,25 +126,25 @@
lemma gcd_fib_mod:
assumes "0 < m"
- shows "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
+ shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
proof (induct n rule: nat_less_induct)
case (1 n) note hyp = this
show ?case
proof -
have "n mod m = (if n < m then n else (n - m) mod m)"
by (rule mod_if)
- also have "gcd (fib m, fib ...) = gcd (fib m, fib n)"
+ also have "gcd (fib m) (fib ...) = gcd (fib m) (fib n)"
proof (cases "n < m")
case True then show ?thesis by simp
next
case False then have "m <= n" by simp
from `0 < m` and False have "n - m < n" by simp
- with hyp have "gcd (fib m, fib ((n - m) mod m))
- = gcd (fib m, fib (n - m))" by simp
- also have "... = gcd (fib m, fib n)"
+ with hyp have "gcd (fib m) (fib ((n - m) mod m))
+ = gcd (fib m) (fib (n - m))" by simp
+ also have "... = gcd (fib m) (fib n)"
using `m <= n` by (rule gcd_fib_diff)
- finally have "gcd (fib m, fib ((n - m) mod m)) =
- gcd (fib m, fib n)" .
+ finally have "gcd (fib m) (fib ((n - m) mod m)) =
+ gcd (fib m) (fib n)" .
with False show ?thesis by simp
qed
finally show ?thesis .
@@ -152,15 +152,15 @@
qed
-theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n")
+theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
proof (induct m n rule: gcd_induct)
- fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp
+ fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp
fix n :: nat assume n: "0 < n"
- then have "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0)
- also assume hyp: "fib ... = gcd (fib n, fib (m mod n))"
- also from n have "... = gcd (fib n, fib m)" by (rule gcd_fib_mod)
- also have "... = gcd (fib m, fib n)" by (rule gcd_commute)
- finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" .
+ then have "gcd m n = gcd n (m mod n)" by (rule gcd_non_0)
+ also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))"
+ also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod)
+ also have "... = gcd (fib m) (fib n)" by (rule gcd_commute)
+ finally show "fib (gcd m n) = gcd (fib m) (fib n)" .
qed
end
--- a/src/HOL/Library/Abstract_Rat.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy Mon Jul 14 11:04:42 2008 +0200
@@ -22,13 +22,13 @@
definition
isnormNum :: "Num \<Rightarrow> bool"
where
- "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> igcd a b = 1))"
+ "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> zgcd a b = 1))"
definition
normNum :: "Num \<Rightarrow> Num"
where
"normNum = (\<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else
- (let g = igcd a b
+ (let g = zgcd a b
in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
@@ -38,19 +38,19 @@
{assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}
moreover
{assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0"
- let ?g = "igcd a b"
+ let ?g = "zgcd a b"
let ?a' = "a div ?g"
let ?b' = "b div ?g"
- let ?g' = "igcd ?a' ?b'"
- from anz bnz have "?g \<noteq> 0" by simp with igcd_pos[of a b]
+ let ?g' = "zgcd ?a' ?b'"
+ from anz bnz have "?g \<noteq> 0" by simp with zgcd_pos[of a b]
have gpos: "?g > 0" by arith
- have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2)
+ have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_dvd1 zgcd_dvd2)
from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
anz bnz
have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
- by - (rule notI,simp add:igcd_def)+
+ by - (rule notI,simp add:zgcd_def)+
from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by blast
- from div_igcd_relprime[OF stupid] have gp1: "?g' = 1" .
+ from div_zgcd_relprime[OF stupid] have gp1: "?g' = 1" .
from bnz have "b < 0 \<or> b > 0" by arith
moreover
{assume b: "b > 0"
@@ -84,7 +84,7 @@
definition
Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
where
- "Nmul = (\<lambda>(a,b) (a',b'). let g = igcd (a*a') (b*b')
+ "Nmul = (\<lambda>(a,b) (a',b'). let g = zgcd (a*a') (b*b')
in (a*a' div g, b*b' div g))"
definition
@@ -120,11 +120,11 @@
then obtain a b a' b' where ab: "x = (a,b)" and ab': "y = (a',b')" by blast
{assume "a = 0"
hence ?thesis using xn ab ab'
- by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
+ by (simp add: zgcd_def isnormNum_def Let_def Nmul_def split_def)}
moreover
{assume "a' = 0"
hence ?thesis using yn ab ab'
- by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
+ by (simp add: zgcd_def isnormNum_def Let_def Nmul_def split_def)}
moreover
{assume a: "a \<noteq>0" and a': "a'\<noteq>0"
hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def)
@@ -136,11 +136,11 @@
lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
by (simp add: Ninv_def isnormNum_def split_def)
- (cases "fst x = 0", auto simp add: igcd_commute)
+ (cases "fst x = 0", auto simp add: zgcd_commute)
lemma isnormNum_int[simp]:
"isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
- by (simp_all add: isnormNum_def igcd_def)
+ by (simp_all add: isnormNum_def zgcd_def)
text {* Relations over Num *}
@@ -201,8 +201,8 @@
from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
from prems have eq:"a * b' = a'*b"
by (simp add: INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
- from prems have gcd1: "igcd a b = 1" "igcd b a = 1" "igcd a' b' = 1" "igcd b' a' = 1"
- by (simp_all add: isnormNum_def add: igcd_commute)
+ from prems have gcd1: "zgcd a b = 1" "zgcd b a = 1" "zgcd a' b' = 1" "zgcd b' a' = 1"
+ by (simp_all add: isnormNum_def add: zgcd_commute)
from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
apply(unfold dvd_def)
apply (rule_tac x="b'" in exI, simp add: mult_ac)
@@ -257,7 +257,7 @@
by (simp add: INum_def normNum_def split_def Let_def)}
moreover
{assume a: "a\<noteq>0" and b: "b\<noteq>0"
- let ?g = "igcd a b"
+ let ?g = "zgcd a b"
from a b have g: "?g \<noteq> 0"by simp
from of_int_div[OF g, where ?'a = 'a]
have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)}
@@ -293,13 +293,13 @@
from z aa' bb' have ?thesis
by (simp add: th Nadd_def normNum_def INum_def split_def)}
moreover {assume z: "a * b' + b * a' \<noteq> 0"
- let ?g = "igcd (a * b' + b * a') (b*b')"
+ let ?g = "zgcd (a * b' + b * a') (b*b')"
have gz: "?g \<noteq> 0" using z by simp
have ?thesis using aa' bb' z gz
of_int_div[where ?'a = 'a,
- OF gz igcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
+ OF gz zgcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
of_int_div[where ?'a = 'a,
- OF gz igcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
+ OF gz zgcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
ultimately have ?thesis using aa' bb'
by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
@@ -318,10 +318,10 @@
done }
moreover
{assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
- let ?g="igcd (a*a') (b*b')"
+ let ?g="zgcd (a*a') (b*b')"
have gz: "?g \<noteq> 0" using z by simp
- from z of_int_div[where ?'a = 'a, OF gz igcd_dvd1[where i="a*a'" and j="b*b'"]]
- of_int_div[where ?'a = 'a , OF gz igcd_dvd2[where i="a*a'" and j="b*b'"]]
+ from z of_int_div[where ?'a = 'a, OF gz zgcd_dvd1[where i="a*a'" and j="b*b'"]]
+ of_int_div[where ?'a = 'a , OF gz zgcd_dvd2[where i="a*a'" and j="b*b'"]]
have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
ultimately show ?thesis by blast
qed
@@ -456,7 +456,7 @@
qed
lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
- by (simp add: Nmul_def split_def Let_def igcd_commute mult_commute)
+ by (simp add: Nmul_def split_def Let_def zgcd_commute mult_commute)
lemma Nmul_assoc: assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
--- a/src/HOL/Library/GCD.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/Library/GCD.thy Mon Jul 14 11:04:42 2008 +0200
@@ -18,64 +18,62 @@
definition
is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
- [code func del]: "is_gcd p m n \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
+ [code func del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
(\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
text {* Uniqueness *}
-lemma is_gcd_unique: "is_gcd m a b \<Longrightarrow> is_gcd n a b \<Longrightarrow> m = n"
+lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
text {* Connection to divides relation *}
-lemma is_gcd_dvd: "is_gcd m a b \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
+lemma is_gcd_dvd: "is_gcd a b m \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
by (auto simp add: is_gcd_def)
text {* Commutativity *}
-lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
+lemma is_gcd_commute: "is_gcd m n k = is_gcd n m k"
by (auto simp add: is_gcd_def)
subsection {* GCD on nat by Euclid's algorithm *}
-fun
- gcd :: "nat \<times> nat => nat"
-where
- "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
+fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+ "gcd m n = (if n = 0 then m else gcd n (m mod n))"
-lemma gcd_induct:
+thm gcd.induct
+
+lemma gcd_induct [case_names "0" rec]:
fixes m n :: nat
assumes "\<And>m. P m 0"
and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
shows "P m n"
-apply (rule gcd.induct [of "split P" "(m, n)", unfolded Product_Type.split])
-apply (case_tac "n = 0")
-apply simp_all
-using assms apply simp_all
-done
+proof (induct m n rule: gcd.induct)
+ case (1 m n) with assms show ?case by (cases "n = 0") simp_all
+qed
-lemma gcd_0 [simp]: "gcd (m, 0) = m"
+lemma gcd_0 [simp]: "gcd m 0 = m"
by simp
-lemma gcd_0_left [simp]: "gcd (0, m) = m"
+lemma gcd_0_left [simp]: "gcd 0 m = m"
by simp
-lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd (m, n) = gcd (n, m mod n)"
+lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
by simp
-lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
+lemma gcd_1 [simp]: "gcd m (Suc 0) = 1"
by simp
declare gcd.simps [simp del]
text {*
- \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}. The
+ \medskip @{term "gcd m n"} divides @{text m} and @{text n}. The
conjunctions don't seem provable separately.
*}
-lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m"
- and gcd_dvd2 [iff]: "gcd (m, n) dvd n"
+lemma gcd_dvd1 [iff]: "gcd m n dvd m"
+ and gcd_dvd2 [iff]: "gcd m n dvd n"
apply (induct m n rule: gcd_induct)
apply (simp_all add: gcd_non_0)
apply (blast dest: dvd_mod_imp_dvd)
@@ -84,50 +82,50 @@
text {*
\medskip Maximality: for all @{term m}, @{term n}, @{term k}
naturals, if @{term k} divides @{term m} and @{term k} divides
- @{term n} then @{term k} divides @{term "gcd (m, n)"}.
+ @{term n} then @{term k} divides @{term "gcd m n"}.
*}
-lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd (m, n)"
+lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
text {*
\medskip Function gcd yields the Greatest Common Divisor.
*}
-lemma is_gcd: "is_gcd (gcd (m, n)) m n"
+lemma is_gcd: "is_gcd m n (gcd m n) "
by (simp add: is_gcd_def gcd_greatest)
subsection {* Derived laws for GCD *}
-lemma gcd_greatest_iff [iff]: "k dvd gcd (m, n) \<longleftrightarrow> k dvd m \<and> k dvd n"
+lemma gcd_greatest_iff [iff]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
by (blast intro!: gcd_greatest intro: dvd_trans)
-lemma gcd_zero: "gcd (m, n) = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
+lemma gcd_zero: "gcd m n = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
-lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
+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))"
+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: dvd_trans)
done
-lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
+lemma gcd_1_left [simp]: "gcd (Suc 0) m = 1"
by (simp add: gcd_commute)
text {*
\medskip Multiplication laws
*}
-lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
+lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
-- {* \cite[page 27]{davenport92} *}
apply (induct m n rule: gcd_induct)
apply simp
@@ -135,26 +133,26 @@
apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
done
-lemma gcd_mult [simp]: "gcd (k, k * n) = k"
+lemma gcd_mult [simp]: "gcd k (k * n) = k"
apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
done
-lemma gcd_self [simp]: "gcd (k, k) = k"
+lemma gcd_self [simp]: "gcd k k = k"
apply (rule gcd_mult [of k 1, simplified])
done
-lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m"
+lemma relprime_dvd_mult: "gcd k n = 1 ==> k dvd m * n ==> k dvd m"
apply (insert gcd_mult_distrib2 [of m k n])
apply simp
apply (erule_tac t = m in ssubst)
apply simp
done
-lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)"
+lemma relprime_dvd_mult_iff: "gcd k n = 1 ==> (k dvd m * n) = (k dvd m)"
apply (blast intro: relprime_dvd_mult dvd_trans)
done
-lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
+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)
@@ -167,29 +165,29 @@
text {* \medskip Addition laws *}
-lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)"
+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)"
+lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
proof -
- have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute)
- also have "... = gcd (n + m, m)" by (simp add: add_commute)
- also have "... = gcd (n, m)" by simp
- also have "... = gcd (m, n)" by (rule gcd_commute)
+ have "gcd m (m + n) = gcd (m + n) m" by (rule gcd_commute)
+ also have "... = gcd (n + m) m" by (simp add: add_commute)
+ also have "... = gcd n m" by simp
+ also have "... = gcd m n" by (rule gcd_commute)
finally show ?thesis .
qed
-lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
+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)"
+lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
by (induct k) (simp_all add: add_assoc)
-lemma gcd_dvd_prod: "gcd (m, n) dvd m * n"
+lemma gcd_dvd_prod: "gcd m n dvd m * n"
using mult_dvd_mono [of 1] by auto
text {*
@@ -198,12 +196,12 @@
lemma div_gcd_relprime:
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
- shows "gcd (a div gcd(a,b), b div gcd(a,b)) = 1"
+ shows "gcd (a div gcd a b) (b div gcd a b) = 1"
proof -
- let ?g = "gcd (a, b)"
+ let ?g = "gcd a b"
let ?a' = "a div ?g"
let ?b' = "b div ?g"
- let ?g' = "gcd (?a', ?b')"
+ let ?g' = "gcd ?a' ?b'"
have dvdg: "?g dvd a" "?g dvd b" by simp_all
have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
from dvdg dvdg' obtain ka kb ka' kb' where
@@ -222,28 +220,28 @@
subsection {* LCM defined by GCD *}
definition
- lcm :: "nat \<times> nat \<Rightarrow> nat"
+ lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
- lcm_prim_def: "lcm = (\<lambda>(m, n). m * n div gcd (m, n))"
+ lcm_prim_def: "lcm m n = m * n div gcd m n"
lemma lcm_def:
- "lcm (m, n) = m * n div gcd (m, n)"
+ "lcm m n = m * n div gcd m n"
unfolding lcm_prim_def by simp
lemma prod_gcd_lcm:
- "m * n = gcd (m, n) * lcm (m, n)"
+ "m * n = gcd m n * lcm m n"
unfolding lcm_def by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
-lemma lcm_0 [simp]: "lcm (m, 0) = 0"
+lemma lcm_0 [simp]: "lcm m 0 = 0"
unfolding lcm_def by simp
-lemma lcm_1 [simp]: "lcm (m, 1) = m"
+lemma lcm_1 [simp]: "lcm m 1 = m"
unfolding lcm_def by simp
-lemma lcm_0_left [simp]: "lcm (0, n) = 0"
+lemma lcm_0_left [simp]: "lcm 0 n = 0"
unfolding lcm_def by simp
-lemma lcm_1_left [simp]: "lcm (1, m) = m"
+lemma lcm_1_left [simp]: "lcm 1 m = m"
unfolding lcm_def by simp
lemma dvd_pos:
@@ -254,38 +252,38 @@
lemma lcm_least:
assumes "m dvd k" and "n dvd k"
- shows "lcm (m, n) dvd k"
+ shows "lcm m n dvd k"
proof (cases k)
case 0 then show ?thesis by auto
next
case (Suc _) then have pos_k: "k > 0" by auto
from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
- with gcd_zero [of m n] have pos_gcd: "gcd (m, n) > 0" by simp
+ with gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
from assms obtain p where k_m: "k = m * p" using dvd_def by blast
from assms obtain q where k_n: "k = n * q" using dvd_def by blast
from pos_k k_m have pos_p: "p > 0" by auto
from pos_k k_n have pos_q: "q > 0" by auto
- have "k * k * gcd (q, p) = k * gcd (k * q, k * p)"
+ have "k * k * gcd q p = k * gcd (k * q) (k * p)"
by (simp add: mult_ac gcd_mult_distrib2)
- also have "\<dots> = k * gcd (m * p * q, n * q * p)"
+ also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
by (simp add: k_m [symmetric] k_n [symmetric])
- also have "\<dots> = k * p * q * gcd (m, n)"
+ also have "\<dots> = k * p * q * gcd m n"
by (simp add: mult_ac gcd_mult_distrib2)
- finally have "(m * p) * (n * q) * gcd (q, p) = k * p * q * gcd (m, n)"
+ finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
by (simp only: k_m [symmetric] k_n [symmetric])
- then have "p * q * m * n * gcd (q, p) = p * q * k * gcd (m, n)"
+ then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
by (simp add: mult_ac)
- with pos_p pos_q have "m * n * gcd (q, p) = k * gcd (m, n)"
+ with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
by simp
with prod_gcd_lcm [of m n]
- have "lcm (m, n) * gcd (q, p) * gcd (m, n) = k * gcd (m, n)"
+ have "lcm m n * gcd q p * gcd m n = k * gcd m n"
by (simp add: mult_ac)
- with pos_gcd have "lcm (m, n) * gcd (q, p) = k" by simp
+ with pos_gcd have "lcm m n * gcd q p = k" by simp
then show ?thesis using dvd_def by auto
qed
lemma lcm_dvd1 [iff]:
- "m dvd lcm (m, n)"
+ "m dvd lcm m n"
proof (cases m)
case 0 then show ?thesis by simp
next
@@ -297,16 +295,16 @@
next
case (Suc _)
then have npos: "n > 0" by simp
- have "gcd (m, n) dvd n" by simp
- then obtain k where "n = gcd (m, n) * k" using dvd_def by auto
- then have "m * n div gcd (m, n) = m * (gcd (m, n) * k) div gcd (m, n)" by (simp add: mult_ac)
+ have "gcd m n dvd n" by simp
+ then obtain k where "n = gcd m n * k" using dvd_def by auto
+ then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac)
also have "\<dots> = m * k" using mpos npos gcd_zero by simp
finally show ?thesis by (simp add: lcm_def)
qed
qed
lemma lcm_dvd2 [iff]:
- "n dvd lcm (m, n)"
+ "n dvd lcm m n"
proof (cases n)
case 0 then show ?thesis by simp
next
@@ -318,9 +316,9 @@
next
case (Suc _)
then have mpos: "m > 0" by simp
- have "gcd (m, n) dvd m" by simp
- then obtain k where "m = gcd (m, n) * k" using dvd_def by auto
- then have "m * n div gcd (m, n) = (gcd (m, n) * k) * n div gcd (m, n)" by (simp add: mult_ac)
+ have "gcd m n dvd m" by simp
+ then obtain k where "m = gcd m n * k" using dvd_def by auto
+ then have "m * n div gcd m n = (gcd m n * k) * n div gcd m n" by (simp add: mult_ac)
also have "\<dots> = n * k" using mpos npos gcd_zero by simp
finally show ?thesis by (simp add: lcm_def)
qed
@@ -330,35 +328,35 @@
subsection {* GCD and LCM on integers *}
definition
- igcd :: "int \<Rightarrow> int \<Rightarrow> int" where
- "igcd i j = int (gcd (nat (abs i), nat (abs j)))"
+ zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
+ "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
-lemma igcd_dvd1 [simp]: "igcd i j dvd i"
- by (simp add: igcd_def int_dvd_iff)
+lemma zgcd_dvd1 [simp]: "zgcd i j dvd i"
+ by (simp add: zgcd_def int_dvd_iff)
-lemma igcd_dvd2 [simp]: "igcd i j dvd j"
- by (simp add: igcd_def int_dvd_iff)
+lemma zgcd_dvd2 [simp]: "zgcd i j dvd j"
+ by (simp add: zgcd_def int_dvd_iff)
-lemma igcd_pos: "igcd i j \<ge> 0"
- by (simp add: igcd_def)
+lemma zgcd_pos: "zgcd i j \<ge> 0"
+ by (simp add: zgcd_def)
-lemma igcd0 [simp]: "(igcd i j = 0) = (i = 0 \<and> j = 0)"
- by (simp add: igcd_def gcd_zero) arith
+lemma zgcd0 [simp]: "(zgcd i j = 0) = (i = 0 \<and> j = 0)"
+ by (simp add: zgcd_def gcd_zero) arith
-lemma igcd_commute: "igcd i j = igcd j i"
- unfolding igcd_def by (simp add: gcd_commute)
+lemma zgcd_commute: "zgcd i j = zgcd j i"
+ unfolding zgcd_def by (simp add: gcd_commute)
-lemma igcd_neg1 [simp]: "igcd (- i) j = igcd i j"
- unfolding igcd_def by simp
+lemma zgcd_neg1 [simp]: "zgcd (- i) j = zgcd i j"
+ unfolding zgcd_def by simp
-lemma igcd_neg2 [simp]: "igcd i (- j) = igcd i j"
- unfolding igcd_def by simp
+lemma zgcd_neg2 [simp]: "zgcd i (- j) = zgcd i j"
+ unfolding zgcd_def by simp
-lemma zrelprime_dvd_mult: "igcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
- unfolding igcd_def
+lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
+ unfolding zgcd_def
proof -
- assume "int (gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>)) = 1" "i dvd k * j"
- then have g: "gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>) = 1" by simp
+ assume "int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>)) = 1" "i dvd k * j"
+ then have g: "gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>) = 1" by simp
from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
unfolding dvd_def
@@ -375,34 +373,34 @@
done
qed
-lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith
+lemma int_nat_abs: "int (nat (abs x)) = abs x" by arith
-lemma igcd_greatest:
+lemma zgcd_greatest:
assumes "k dvd m" and "k dvd n"
- shows "k dvd igcd m n"
+ shows "k dvd zgcd m n"
proof -
let ?k' = "nat \<bar>k\<bar>"
let ?m' = "nat \<bar>m\<bar>"
let ?n' = "nat \<bar>n\<bar>"
from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2)
- from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd igcd m n"
- unfolding igcd_def by (simp only: zdvd_int)
- then have "\<bar>k\<bar> dvd igcd m n" by (simp only: int_nat_abs)
- then show "k dvd igcd m n" by (simp add: zdvd_abs1)
+ from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
+ unfolding zgcd_def by (simp only: zdvd_int)
+ then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
+ then show "k dvd zgcd m n" by (simp add: zdvd_abs1)
qed
-lemma div_igcd_relprime:
+lemma div_zgcd_relprime:
assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
- shows "igcd (a div (igcd a b)) (b div (igcd a b)) = 1"
+ shows "zgcd (a div (zgcd a b)) (b div (zgcd a b)) = 1"
proof -
from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by arith
- let ?g = "igcd a b"
+ let ?g = "zgcd a b"
let ?a' = "a div ?g"
let ?b' = "b div ?g"
- let ?g' = "igcd ?a' ?b'"
- have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2)
- have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: igcd_dvd1 igcd_dvd2)
+ let ?g' = "zgcd ?a' ?b'"
+ have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_dvd1 zgcd_dvd2)
+ have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: zgcd_dvd1 zgcd_dvd2)
from dvdg dvdg' obtain ka kb ka' kb' where
kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
unfolding dvd_def by blast
@@ -411,35 +409,36 @@
by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
have "?g \<noteq> 0" using nz by simp
- then have gp: "?g \<noteq> 0" using igcd_pos[where i="a" and j="b"] by arith
- from igcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
+ then have gp: "?g \<noteq> 0" using zgcd_pos[where i="a" and j="b"] by arith
+ from zgcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp
- with igcd_pos show "?g' = 1" by simp
+ with zgcd_pos show "?g' = 1" by simp
qed
-definition "ilcm = (\<lambda>i j. int (lcm(nat(abs i),nat(abs j))))"
+definition zlcm :: "int \<Rightarrow> int \<Rightarrow> int" where
+ "zlcm i j = int (lcm (nat (abs i)) (nat (abs j)))"
-lemma dvd_ilcm_self1[simp]: "i dvd ilcm i j"
-by(simp add:ilcm_def dvd_int_iff)
+lemma dvd_zlcm_self1[simp]: "i dvd zlcm i j"
+by(simp add:zlcm_def dvd_int_iff)
-lemma dvd_ilcm_self2[simp]: "j dvd ilcm i j"
-by(simp add:ilcm_def dvd_int_iff)
+lemma dvd_zlcm_self2[simp]: "j dvd zlcm i j"
+by(simp add:zlcm_def dvd_int_iff)
-lemma dvd_imp_dvd_ilcm1:
- assumes "k dvd i" shows "k dvd (ilcm i j)"
+lemma dvd_imp_dvd_zlcm1:
+ assumes "k dvd i" shows "k dvd (zlcm i j)"
proof -
have "nat(abs k) dvd nat(abs i)" using `k dvd i`
by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
- thus ?thesis by(simp add:ilcm_def dvd_int_iff)(blast intro: dvd_trans)
+ thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
qed
-lemma dvd_imp_dvd_ilcm2:
- assumes "k dvd j" shows "k dvd (ilcm i j)"
+lemma dvd_imp_dvd_zlcm2:
+ assumes "k dvd j" shows "k dvd (zlcm i j)"
proof -
have "nat(abs k) dvd nat(abs j)" using `k dvd j`
by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
- thus ?thesis by(simp add:ilcm_def dvd_int_iff)(blast intro: dvd_trans)
+ thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
qed
@@ -453,35 +452,35 @@
lemma lcm_pos:
assumes mpos: "m > 0"
- and npos: "n>0"
- shows "lcm (m,n) > 0"
+ and npos: "n > 0"
+ shows "lcm m n > 0"
proof(rule ccontr, simp add: lcm_def gcd_zero)
-assume h:"m*n div gcd(m,n) = 0"
-from mpos npos have "gcd (m,n) \<noteq> 0" using gcd_zero by simp
-hence gcdp: "gcd(m,n) > 0" by simp
+assume h:"m * n div gcd m n = 0"
+from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
+hence gcdp: "gcd m n > 0" by simp
with h
-have "m*n < gcd(m,n)"
- by (cases "m * n < gcd (m, n)") (auto simp add: div_if[OF gcdp, where m="m*n"])
+have "m*n < gcd m n"
+ by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
moreover
-have "gcd(m,n) dvd m" by simp
- with mpos dvd_imp_le have t1:"gcd(m,n) \<le> m" by simp
- with npos have t1:"gcd(m,n)*n \<le> m*n" by simp
- have "gcd(m,n) \<le> gcd(m,n)*n" using npos by simp
- with t1 have "gcd(m,n) \<le> m*n" by arith
+have "gcd m n dvd m" by simp
+ with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
+ with npos have t1:"gcd m n*n \<le> m*n" by simp
+ have "gcd m n \<le> gcd m n*n" using npos by simp
+ with t1 have "gcd m n \<le> m*n" by arith
ultimately show "False" by simp
qed
-lemma ilcm_pos:
+lemma zlcm_pos:
assumes anz: "a \<noteq> 0"
and bnz: "b \<noteq> 0"
- shows "0 < ilcm a b"
+ shows "0 < zlcm a b"
proof-
let ?na = "nat (abs a)"
let ?nb = "nat (abs b)"
have nap: "?na >0" using anz by simp
have nbp: "?nb >0" using bnz by simp
- have "0 < lcm (?na,?nb)" by (rule lcm_pos[OF nap nbp])
- thus ?thesis by (simp add: ilcm_def)
+ have "0 < lcm ?na ?nb" by (rule lcm_pos[OF nap nbp])
+ thus ?thesis by (simp add: zlcm_def)
qed
end
--- a/src/HOL/Library/Primes.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/Library/Primes.thy Mon Jul 14 11:04:42 2008 +0200
@@ -12,7 +12,7 @@
definition
coprime :: "nat => nat => bool" where
- "coprime m n \<longleftrightarrow> (gcd (m, n) = 1)"
+ "coprime m n \<longleftrightarrow> (gcd m n = 1)"
definition
prime :: "nat \<Rightarrow> bool" where
@@ -25,7 +25,7 @@
apply (auto dest!: dvd_imp_le)
done
-lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd (p, n) = 1"
+lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd p n = 1"
apply (auto simp add: prime_def)
apply (metis One_nat_def gcd_dvd1 gcd_dvd2)
done
@@ -309,24 +309,24 @@
qed
text {* Greatest common divisor. *}
-lemma gcd_unique: "d dvd a\<and>d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd(a,b)"
+lemma gcd_unique: "d dvd a\<and>d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
proof(auto)
assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b]
- have th: "gcd (a,b) dvd d" by blast
- from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]] show "d = gcd (a,b)" by blast
+ have th: "gcd a b dvd d" by blast
+ from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]] show "d =gcd a b" by blast
qed
lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
- shows "gcd (x,y) = gcd(u,v)"
+ shows "gcd x y = gcd u v"
proof-
- from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd (u,v)" by simp
- with gcd_unique[of "gcd(u,v)" x y] show ?thesis by auto
+ from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" by simp
+ with gcd_unique[of "gcd u v" x y] show ?thesis by auto
qed
-lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd(a,b) \<or> b * x - a * y = gcd(a,b)"
+lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
proof-
- let ?g = "gcd (a,b)"
+ let ?g = "gcd a b"
from bezout[of a b] obtain d x y where d: "d dvd a" "d dvd b" "a * x - b * y = d \<or> b * x - a * y = d" by blast
from d(1,2) have "d dvd ?g" by simp
then obtain k where k: "?g = d*k" unfolding dvd_def by blast
@@ -339,9 +339,9 @@
qed
lemma bezout_gcd_strong: assumes a: "a \<noteq> 0"
- shows "\<exists>x y. a * x = b * y + gcd(a,b)"
+ shows "\<exists>x y. a * x = b * y + gcd a b"
proof-
- let ?g = "gcd (a,b)"
+ let ?g = "gcd a b"
from bezout_add_strong[OF a, of b]
obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
from d(1,2) have "d dvd ?g" by simp
@@ -351,13 +351,13 @@
thus ?thesis by blast
qed
-lemma gcd_mult_distrib: "gcd(a * c, b * c) = c * gcd(a,b)"
+lemma gcd_mult_distrib: "gcd (a * c) (b * c) = c * gcd a b"
by(simp add: gcd_mult_distrib2 mult_commute)
-lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd(a,b) dvd d"
+lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd a b dvd d"
(is "?lhs \<longleftrightarrow> ?rhs")
proof-
- let ?g = "gcd (a,b)"
+ let ?g = "gcd a b"
{assume H: ?rhs then obtain k where k: "d = ?g*k" unfolding dvd_def by blast
from bezout_gcd[of a b] obtain x y where xy: "a * x - b * y = ?g \<or> b * x - a * y = ?g"
by blast
@@ -376,34 +376,34 @@
ultimately show ?thesis by blast
qed
-lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd(a,b) dvd d"
+lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd a b dvd d"
proof-
- let ?g = "gcd (a,b)"
+ let ?g = "gcd a b"
have dv: "?g dvd a*x" "?g dvd b * y"
using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
from dvd_add[OF dv] H
show ?thesis by auto
qed
-lemma gcd_mult': "gcd(b,a * b) = b"
+lemma gcd_mult': "gcd b (a * b) = b"
by (simp add: gcd_mult mult_commute[of a b])
-lemma gcd_add: "gcd(a + b,b) = gcd(a,b)" "gcd(b + a,b) = gcd(a,b)" "gcd(a,a + b) = gcd(a,b)" "gcd(a,b + a) = gcd(a,b)"
+lemma gcd_add: "gcd (a + b) b = gcd a b" "gcd (b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
apply (simp_all add: gcd_add1)
by (simp add: gcd_commute gcd_add1)
-lemma gcd_sub: "b <= a ==> gcd(a - b,b) = gcd(a,b)" "a <= b ==> gcd(a,b - a) = gcd(a,b)"
+lemma gcd_sub: "b <= a ==> gcd (a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
proof-
{fix a b assume H: "b \<le> (a::nat)"
hence th: "a - b + b = a" by arith
- from gcd_add(1)[of "a - b" b] th have "gcd(a - b,b) = gcd(a,b)" by simp}
+ from gcd_add(1)[of "a - b" b] th have "gcd (a - b) b = gcd a b" by simp}
note th = this
{
assume ab: "b \<le> a"
- from th[OF ab] show "gcd (a - b, b) = gcd (a, b)" by blast
+ from th[OF ab] show "gcd (a - b) b = gcd a b" by blast
next
assume ab: "a \<le> b"
- from th[OF ab] show "gcd (a,b - a) = gcd (a, b)"
+ from th[OF ab] show "gcd a (b - a) = gcd a b"
by (simp add: gcd_commute)}
qed
@@ -425,10 +425,10 @@
lemma coprime_Suc0'[simp]: "coprime (Suc 0) a" by (simp add: coprime_def)
lemma gcd_coprime:
- assumes z: "gcd(a,b) \<noteq> 0" and a: "a = a' * gcd(a,b)" and b: "b = b' * gcd(a,b)"
+ assumes z: "gcd a b \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b"
shows "coprime a' b'"
proof-
- let ?g = "gcd(a,b)"
+ let ?g = "gcd a b"
{assume bz: "a = 0" from b bz z a have ?thesis by (simp add: gcd_zero coprime_def)}
moreover
{assume az: "a\<noteq> 0"
@@ -447,8 +447,8 @@
lemma coprime_mul: assumes da: "coprime d a" and db: "coprime d b"
shows "coprime d (a * b)"
proof-
- from da have th: "gcd(a, d) = 1" by (simp add: coprime_def gcd_commute)
- from gcd_mult_cancel[of a d b, OF th] db[unfolded coprime_def] have "gcd (d, a*b) = 1"
+ from da have th: "gcd a d = 1" by (simp add: coprime_def gcd_commute)
+ from gcd_mult_cancel[of a d b, OF th] db[unfolded coprime_def] have "gcd d (a * b) = 1"
by (simp add: gcd_commute)
thus ?thesis unfolding coprime_def .
qed
@@ -480,10 +480,10 @@
by blast
lemma gcd_coprime_exists:
- assumes nz: "gcd(a,b) \<noteq> 0"
- shows "\<exists>a' b'. a = a' * gcd(a,b) \<and> b = b' * gcd(a,b) \<and> coprime a' b'"
+ assumes nz: "gcd a b \<noteq> 0"
+ shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
proof-
- let ?g = "gcd (a,b)"
+ let ?g = "gcd a b"
from gcd_dvd1[of a b] gcd_dvd2[of a b]
obtain a' b' where "a = ?g*a'" "b = ?g*b'" unfolding dvd_def by blast
hence ab': "a = a'*?g" "b = b'*?g" by algebra+
@@ -505,9 +505,9 @@
lemma coprime_minus1: "n \<noteq> 0 ==> coprime (n - 1) n"
using coprime_plus1[of "n - 1"] coprime_commute[of "n - 1" n] by auto
-lemma bezout_gcd_pow: "\<exists>x y. a ^n * x - b ^ n * y = gcd(a,b) ^ n \<or> b ^ n * x - a ^ n * y = gcd(a,b) ^ n"
+lemma bezout_gcd_pow: "\<exists>x y. a ^n * x - b ^ n * y = gcd a b ^ n \<or> b ^ n * x - a ^ n * y = gcd a b ^ n"
proof-
- let ?g = "gcd (a,b)"
+ let ?g = "gcd a b"
{assume z: "?g = 0" hence ?thesis
apply (cases n, simp)
apply arith
@@ -530,16 +530,16 @@
hence ?thesis by blast }
ultimately show ?thesis by blast
qed
-lemma gcd_exp: "gcd (a^n, b^n) = gcd(a,b)^n"
+lemma gcd_exp: "gcd (a^n) (b^n) = gcd a b ^ n"
proof-
- let ?g = "gcd(a^n,b^n)"
- let ?gn = "gcd(a,b)^n"
+ let ?g = "gcd (a^n) (b^n)"
+ let ?gn = "gcd a b ^ n"
{fix e assume H: "e dvd a^n" "e dvd b^n"
from bezout_gcd_pow[of a n b] obtain x y
where xy: "a ^ n * x - b ^ n * y = ?gn \<or> b ^ n * x - a ^ n * y = ?gn" by blast
from dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
- have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd (a, b) ^ n", simp_all)}
+ have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd a b ^ n", simp_all)}
hence th: "\<forall>e. e dvd a^n \<and> e dvd b^n \<longrightarrow> e dvd ?gn" by blast
from divides_exp[OF gcd_dvd1[of a b], of n] divides_exp[OF gcd_dvd2[of a b], of n] th
gcd_unique have "?gn = ?g" by blast thus ?thesis by simp
@@ -551,7 +551,7 @@
lemma division_decomp: assumes dc: "(a::nat) dvd b * c"
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
proof-
- let ?g = "gcd (a,b)"
+ let ?g = "gcd a b"
{assume "?g = 0" with dc have ?thesis apply (simp add: gcd_zero)
apply (rule exI[where x="0"])
by (rule exI[where x="c"], simp)}
@@ -575,7 +575,7 @@
lemma divides_rev: assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0" shows "a dvd b"
proof-
- let ?g = "gcd (a,b)"
+ let ?g = "gcd a b"
from n obtain m where m: "n = Suc m" by (cases n, simp_all)
{assume "?g = 0" with ab n have ?thesis by (simp add: gcd_zero)}
moreover
--- a/src/HOL/NumberTheory/Chinese.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy Mon Jul 14 11:04:42 2008 +0200
@@ -6,7 +6,9 @@
header {* The Chinese Remainder Theorem *}
-theory Chinese imports IntPrimes begin
+theory Chinese
+imports IntPrimes
+begin
text {*
The Chinese Remainder Theorem for an arbitrary finite number of
@@ -35,11 +37,11 @@
m_cond :: "nat => (nat => int) => bool" where
"m_cond n mf =
((\<forall>i. i \<le> n --> 0 < mf i) \<and>
- (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1))"
+ (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i) (mf j) = 1))"
definition
km_cond :: "nat => (nat => int) => (nat => int) => bool" where
- "km_cond n kf mf = (\<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1)"
+ "km_cond n kf mf = (\<forall>i. i \<le> n --> zgcd (kf i) (mf i) = 1)"
definition
lincong_sol ::
@@ -75,8 +77,8 @@
done
lemma funprod_zgcd [rule_format (no_asm)]:
- "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i, mf m) = 1) -->
- zgcd (funprod mf k l, mf m) = 1"
+ "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i) (mf m) = 1) -->
+ zgcd (funprod mf k l) (mf m) = 1"
apply (induct l)
apply simp_all
apply (rule impI)+
--- a/src/HOL/NumberTheory/EulerFermat.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy Mon Jul 14 11:04:42 2008 +0200
@@ -6,7 +6,9 @@
header {* Fermat's Little Theorem extended to Euler's Totient function *}
-theory EulerFermat imports BijectionRel IntFact begin
+theory EulerFermat
+imports BijectionRel IntFact
+begin
text {*
Fermat's Little Theorem extended to Euler's Totient function. More
@@ -22,7 +24,7 @@
for m :: int
where
empty [simp]: "{} \<in> RsetR m"
- | insert: "A \<in> RsetR m ==> zgcd (a, m) = 1 ==>
+ | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
\<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
consts
@@ -33,7 +35,7 @@
"BnorRset (a, m) =
(if 0 < a then
let na = BnorRset (a - 1, m)
- in (if zgcd (a, m) = 1 then insert a na else na)
+ in (if zgcd a m = 1 then insert a na else na)
else {})"
definition
@@ -103,7 +105,7 @@
done
lemma Bnor_mem_if [rule_format]:
- "zgcd (b, m) = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
+ "zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
apply (induct a m rule: BnorRset.induct, auto)
apply (subst BnorRset.simps)
defer
@@ -137,7 +139,7 @@
lemma norR_mem_unique:
"1 < m ==>
- zgcd (a, m) = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
+ zgcd a m = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
apply (unfold norRRset_def)
apply (cut_tac a = a and m = m in zcong_zless_unique, auto)
apply (rule_tac [2] m = m in zcong_zless_imp_eq)
@@ -149,7 +151,7 @@
apply (auto intro: order_less_le [THEN iffD2])
prefer 2
apply (simp only: zcong_def)
- apply (subgoal_tac "zgcd (a, m) = m")
+ apply (subgoal_tac "zgcd a m = m")
prefer 2
apply (subst zdvd_iff_zgcd [symmetric])
apply (rule_tac [4] zgcd_zcong_zgcd)
@@ -160,14 +162,14 @@
text {* \medskip @{term noXRRset} *}
lemma RRset_gcd [rule_format]:
- "is_RRset A m ==> a \<in> A --> zgcd (a, m) = 1"
+ "is_RRset A m ==> a \<in> A --> zgcd a m = 1"
apply (unfold is_RRset_def)
- apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd (a, m) = 1"], auto)
+ apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd a m = 1"], auto)
done
lemma RsetR_zmult_mono:
"A \<in> RsetR m ==>
- 0 < m ==> zgcd (x, m) = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
+ 0 < m ==> zgcd x m = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
apply (erule RsetR.induct, simp_all)
apply (rule RsetR.insert, auto)
apply (blast intro: zgcd_zgcd_zmult)
@@ -176,7 +178,7 @@
lemma card_nor_eq_noX:
"0 < m ==>
- zgcd (x, m) = 1 ==> card (noXRRset m x) = card (norRRset m)"
+ zgcd x m = 1 ==> card (noXRRset m x) = card (norRRset m)"
apply (unfold norRRset_def noXRRset_def)
apply (rule card_image)
apply (auto simp add: inj_on_def Bnor_fin)
@@ -184,7 +186,7 @@
done
lemma noX_is_RRset:
- "0 < m ==> zgcd (x, m) = 1 ==> is_RRset (noXRRset m x) m"
+ "0 < m ==> zgcd x m = 1 ==> is_RRset (noXRRset m x) m"
apply (unfold is_RRset_def phi_def)
apply (auto simp add: card_nor_eq_noX)
apply (unfold noXRRset_def norRRset_def)
@@ -284,7 +286,7 @@
done
lemma Bnor_prod_zgcd [rule_format]:
- "a < m --> zgcd (\<Prod>(BnorRset(a, m)), m) = 1"
+ "a < m --> zgcd (\<Prod>(BnorRset(a, m))) m = 1"
apply (induct a m rule: BnorRset_induct)
prefer 2
apply (subst BnorRset.simps)
@@ -294,7 +296,7 @@
done
theorem Euler_Fermat:
- "0 < m ==> zgcd (x, m) = 1 ==> [x^(phi m) = 1] (mod m)"
+ "0 < m ==> zgcd x m = 1 ==> [x^(phi m) = 1] (mod m)"
apply (unfold norRRset_def phi_def)
apply (case_tac "x = 0")
apply (case_tac [2] "m = 1")
--- a/src/HOL/NumberTheory/Fib.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/NumberTheory/Fib.thy Mon Jul 14 11:04:42 2008 +0200
@@ -5,7 +5,9 @@
header {* The Fibonacci function *}
-theory Fib imports Primes begin
+theory Fib
+imports Primes
+begin
text {*
Fibonacci numbers: proofs of laws taken from:
@@ -92,14 +94,14 @@
text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
-lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = Suc 0"
+lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (Suc n)) = Suc 0"
apply (induct n rule: fib.induct)
prefer 3
apply (simp add: gcd_commute fib_Suc3)
apply (simp_all add: fib_2)
done
-lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"
+lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
apply (simp add: gcd_commute [of "fib m"])
apply (case_tac m)
apply simp
@@ -109,31 +111,31 @@
apply (simp add: gcd_fib_Suc_eq_1 gcd_mult_cancel)
done
-lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)"
+lemma gcd_fib_diff: "m \<le> n ==> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
-lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
+lemma gcd_fib_mod: "0 < m ==> gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
proof (induct n rule: less_induct)
case (less n)
from less.prems have pos_m: "0 < m" .
- show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
+ show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
proof (cases "m < n")
case True note m_n = True
then have m_n': "m \<le> n" by auto
with pos_m have pos_n: "0 < n" by auto
with pos_m m_n have diff: "n - m < n" by auto
- have "gcd (fib m, fib (n mod m)) = gcd (fib m, fib ((n - m) mod m))"
+ have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
by (simp add: mod_if [of n]) (insert m_n, auto)
- also have "\<dots> = gcd (fib m, fib (n - m))" by (simp add: less.hyps diff pos_m)
- also have "\<dots> = gcd (fib m, fib n)" by (simp add: gcd_fib_diff m_n')
- finally show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" .
+ also have "\<dots> = gcd (fib m) (fib (n - m))" by (simp add: less.hyps diff pos_m)
+ also have "\<dots> = gcd (fib m) (fib n)" by (simp add: gcd_fib_diff m_n')
+ finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
next
- case False then show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
+ case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
by (cases "m = n") auto
qed
qed
-lemma fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" -- {* Law 6.111 *}
+lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" -- {* Law 6.111 *}
apply (induct m n rule: gcd_induct)
apply (simp_all add: gcd_non_0 gcd_commute gcd_fib_mod)
done
--- a/src/HOL/NumberTheory/Gauss.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy Mon Jul 14 11:04:42 2008 +0200
@@ -5,7 +5,9 @@
header {* Gauss' Lemma *}
-theory Gauss imports Euler begin
+theory Gauss
+imports Euler
+begin
locale GAUSS =
fixes p :: "int"
@@ -284,10 +286,10 @@
using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
qed
-lemma all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
+lemma all_A_relprime: "\<forall>x \<in> A. zgcd x p = 1"
using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
-lemma A_prod_relprime: "zgcd((setprod id A),p) = 1"
+lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime)
--- a/src/HOL/NumberTheory/Int2.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/NumberTheory/Int2.thy Mon Jul 14 11:04:42 2008 +0200
@@ -5,7 +5,9 @@
header {*Integers: Divisibility and Congruences*}
-theory Int2 imports Finite2 WilsonRuss begin
+theory Int2
+imports Finite2 WilsonRuss
+begin
definition
MultInv :: "int => int => int" where
@@ -167,8 +169,8 @@
apply auto
done
-lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
- ==> zgcd (setprod id A,y) = 1"
+lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. zgcd x y = 1 |]
+ ==> zgcd (setprod id A) y = 1"
by (induct set: finite) (auto simp add: zgcd_zgcd_zmult)
--- a/src/HOL/NumberTheory/IntPrimes.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Mon Jul 14 11:04:42 2008 +0200
@@ -34,10 +34,6 @@
t, t' - (r' div r) * t))"
definition
- zgcd :: "int * int => int" where
- "zgcd = (\<lambda>(x,y). int (gcd (nat (abs x), nat (abs y))))"
-
-definition
zprime :: "int \<Rightarrow> bool" where
"zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
@@ -53,10 +49,10 @@
text {* \medskip @{term gcd} lemmas *}
-lemma gcd_add1_eq: "gcd (m + k, k) = gcd (m + k, m)"
+lemma gcd_add1_eq: "gcd (m + k) k = gcd (m + k) m"
by (simp add: gcd_commute)
-lemma gcd_diff2: "m \<le> n ==> gcd (n, n - m) = gcd (n, m)"
+lemma gcd_diff2: "m \<le> n ==> gcd n (n - m) = gcd n m"
apply (subgoal_tac "n = m + (n - m)")
apply (erule ssubst, rule gcd_add1_eq, simp)
done
@@ -64,19 +60,19 @@
subsection {* Euclid's Algorithm and GCD *}
-lemma zgcd_0 [simp]: "zgcd (m, 0) = abs m"
+lemma zgcd_0 [simp]: "zgcd m 0 = abs m"
by (simp add: zgcd_def abs_if)
-lemma zgcd_0_left [simp]: "zgcd (0, m) = abs m"
+lemma zgcd_0_left [simp]: "zgcd 0 m = abs m"
by (simp add: zgcd_def abs_if)
-lemma zgcd_zminus [simp]: "zgcd (-m, n) = zgcd (m, n)"
+lemma zgcd_zminus [simp]: "zgcd (-m) n = zgcd m n"
by (simp add: zgcd_def)
-lemma zgcd_zminus2 [simp]: "zgcd (m, -n) = zgcd (m, n)"
+lemma zgcd_zminus2 [simp]: "zgcd m (-n) = zgcd m n"
by (simp add: zgcd_def)
-lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)"
+lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)"
apply (frule_tac b = n and a = m in pos_mod_sign)
apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
@@ -84,37 +80,37 @@
apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
done
-lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)"
+lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO)
apply (auto simp add: linorder_neq_iff zgcd_non_0)
apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
done
-lemma zgcd_1 [simp]: "zgcd (m, 1) = 1"
+lemma zgcd_1 [simp]: "zgcd m 1 = 1"
by (simp add: zgcd_def abs_if)
-lemma zgcd_0_1_iff [simp]: "(zgcd (0, m) = 1) = (abs m = 1)"
+lemma zgcd_0_1_iff [simp]: "zgcd 0 m = 1 \<longleftrightarrow> abs m = 1"
by (simp add: zgcd_def abs_if)
-lemma zgcd_zdvd1 [iff]: "zgcd (m, n) dvd m"
+lemma zgcd_zdvd1 [iff]: "zgcd m n dvd m"
by (simp add: zgcd_def abs_if int_dvd_iff)
-lemma zgcd_zdvd2 [iff]: "zgcd (m, n) dvd n"
+lemma zgcd_zdvd2 [iff]: "zgcd m n dvd n"
by (simp add: zgcd_def abs_if int_dvd_iff)
-lemma zgcd_greatest_iff: "k dvd zgcd (m, n) = (k dvd m \<and> k dvd n)"
+lemma zgcd_greatest_iff: "k dvd zgcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
-lemma zgcd_commute: "zgcd (m, n) = zgcd (n, m)"
+lemma zgcd_commute: "zgcd m n = zgcd n m"
by (simp add: zgcd_def gcd_commute)
-lemma zgcd_1_left [simp]: "zgcd (1, m) = 1"
+lemma zgcd_1_left [simp]: "zgcd 1 m = 1"
by (simp add: zgcd_def gcd_1_left)
-lemma zgcd_assoc: "zgcd (zgcd (k, m), n) = zgcd (k, zgcd (m, n))"
+lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)"
by (simp add: zgcd_def gcd_assoc)
-lemma zgcd_left_commute: "zgcd (k, zgcd (m, n)) = zgcd (m, zgcd (k, n))"
+lemma zgcd_left_commute: "zgcd k (zgcd m n) = zgcd m (zgcd k n)"
apply (rule zgcd_commute [THEN trans])
apply (rule zgcd_assoc [THEN trans])
apply (rule zgcd_commute [THEN arg_cong])
@@ -123,35 +119,35 @@
lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
-- {* addition is an AC-operator *}
-lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)"
+lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
by (simp del: minus_mult_right [symmetric]
add: minus_mult_right nat_mult_distrib zgcd_def abs_if
mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
-lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)"
+lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
by (simp add: abs_if zgcd_zmult_distrib2)
-lemma zgcd_self [simp]: "0 \<le> m ==> zgcd (m, m) = m"
+lemma zgcd_self [simp]: "0 \<le> m ==> zgcd m m = m"
by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all)
-lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd (k, k * n) = k"
+lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd k (k * n) = k"
by (cut_tac k = k and m = 1 and n = n in zgcd_zmult_distrib2, simp_all)
-lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n, k) = k"
+lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n) k = k"
by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all)
lemma zrelprime_zdvd_zmult_aux:
- "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
+ "zgcd n k = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
by (metis abs_of_nonneg zdvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
-lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m"
+lemma zrelprime_zdvd_zmult: "zgcd n k = 1 ==> k dvd m * n ==> k dvd m"
apply (case_tac "0 \<le> m")
apply (blast intro: zrelprime_zdvd_zmult_aux)
apply (subgoal_tac "k dvd -m")
apply (rule_tac [2] zrelprime_zdvd_zmult_aux, auto)
done
-lemma zgcd_geq_zero: "0 <= zgcd(x,y)"
+lemma zgcd_geq_zero: "0 <= zgcd x y"
by (auto simp add: zgcd_def)
text{*This is merely a sanity check on zprime, since the previous version
@@ -163,34 +159,34 @@
done
lemma zprime_imp_zrelprime:
- "zprime p ==> \<not> p dvd n ==> zgcd (n, p) = 1"
+ "zprime p ==> \<not> p dvd n ==> zgcd n p = 1"
apply (auto simp add: zprime_def)
apply (metis zgcd_commute zgcd_geq_zero zgcd_zdvd1 zgcd_zdvd2)
done
lemma zless_zprime_imp_zrelprime:
- "zprime p ==> 0 < n ==> n < p ==> zgcd (n, p) = 1"
+ "zprime p ==> 0 < n ==> n < p ==> zgcd n p = 1"
apply (erule zprime_imp_zrelprime)
apply (erule zdvd_not_zless, assumption)
done
lemma zprime_zdvd_zmult:
"0 \<le> (m::int) ==> zprime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
- by (metis igcd_dvd1 igcd_dvd2 igcd_pos zprime_def zrelprime_dvd_mult)
+ by (metis zgcd_dvd1 zgcd_dvd2 zgcd_pos zprime_def zrelprime_dvd_mult)
-lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k, n) = zgcd (m, n)"
+lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n"
apply (rule zgcd_eq [THEN trans])
apply (simp add: zmod_zadd1_eq)
apply (rule zgcd_eq [symmetric])
done
-lemma zgcd_zdvd_zgcd_zmult: "zgcd (m, n) dvd zgcd (k * m, n)"
+lemma zgcd_zdvd_zgcd_zmult: "zgcd m n dvd zgcd (k * m) n"
apply (simp add: zgcd_greatest_iff)
apply (blast intro: zdvd_trans)
done
lemma zgcd_zmult_zdvd_zgcd:
- "zgcd (k, n) = 1 ==> zgcd (k * m, n) dvd zgcd (m, n)"
+ "zgcd k n = 1 ==> zgcd (k * m) n dvd zgcd m n"
apply (simp add: zgcd_greatest_iff)
apply (rule_tac n = k in zrelprime_zdvd_zmult)
prefer 2
@@ -198,14 +194,14 @@
apply (metis zgcd_1 zgcd_commute zgcd_left_commute)
done
-lemma zgcd_zmult_cancel: "zgcd (k, n) = 1 ==> zgcd (k * m, n) = zgcd (m, n)"
+lemma zgcd_zmult_cancel: "zgcd k n = 1 ==> zgcd (k * m) n = zgcd m n"
by (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel)
lemma zgcd_zgcd_zmult:
- "zgcd (k, m) = 1 ==> zgcd (n, m) = 1 ==> zgcd (k * n, m) = 1"
+ "zgcd k m = 1 ==> zgcd n m = 1 ==> zgcd (k * n) m = 1"
by (simp add: zgcd_zmult_cancel)
-lemma zdvd_iff_zgcd: "0 < m ==> (m dvd n) = (zgcd (n, m) = m)"
+lemma zdvd_iff_zgcd: "0 < m ==> m dvd n \<longleftrightarrow> zgcd n m = m"
by (metis abs_of_pos zdvd_mult_div_cancel zgcd_0 zgcd_commute zgcd_geq_zero zgcd_zdvd2 zgcd_zmult_eq_self)
@@ -276,7 +272,7 @@
lemma zcong_cancel:
"0 \<le> m ==>
- zgcd (k, m) = 1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)"
+ zgcd k m = 1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)"
apply safe
prefer 2
apply (blast intro: zcong_scalar)
@@ -293,11 +289,11 @@
lemma zcong_cancel2:
"0 \<le> m ==>
- zgcd (k, m) = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)"
+ zgcd k m = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)"
by (simp add: zmult_commute zcong_cancel)
lemma zcong_zgcd_zmult_zmod:
- "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd (m, n) = 1
+ "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd m n = 1
==> [a = b] (mod m * n)"
apply (unfold zcong_def dvd_def, auto)
apply (subgoal_tac "m dvd n * ka")
@@ -353,7 +349,7 @@
lemma zgcd_zcong_zgcd:
"0 < m ==>
- zgcd (a, m) = 1 ==> [a = b] (mod m) ==> zgcd (b, m) = 1"
+ zgcd a m = 1 ==> [a = b] (mod m) ==> zgcd b m = 1"
by (auto simp add: zcong_iff_lin)
lemma zcong_zmod_aux:
@@ -412,7 +408,7 @@
declare xzgcda.simps [simp del]
lemma xzgcd_correct_aux1:
- "zgcd (r', r) = k --> 0 < r -->
+ "zgcd r' r = k --> 0 < r -->
(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))"
apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
z = s and aa = t' and ab = t in xzgcda.induct)
@@ -428,7 +424,7 @@
lemma xzgcd_correct_aux2:
"(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r -->
- zgcd (r', r) = k"
+ zgcd r' r = k"
apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
z = s and aa = t' and ab = t in xzgcda.induct)
apply (subst zgcd_eq)
@@ -441,7 +437,7 @@
done
lemma xzgcd_correct:
- "0 < n ==> (zgcd (m, n) = k) = (\<exists>s t. xzgcd m n = (k, s, t))"
+ "0 < n ==> zgcd m n = k \<longleftrightarrow> (\<exists>s t. xzgcd m n = (k, s, t))"
apply (unfold xzgcd_def)
apply (rule iffI)
apply (rule_tac [2] xzgcd_correct_aux2 [THEN mp, THEN mp])
@@ -491,14 +487,14 @@
done
lemma zgcd_ex_linear:
- "0 < n ==> zgcd (m, n) = k ==> (\<exists>s t. k = s * m + t * n)"
+ "0 < n ==> zgcd m n = k ==> (\<exists>s t. k = s * m + t * n)"
apply (simp add: xzgcd_correct, safe)
apply (rule exI)+
apply (erule xzgcd_linear, auto)
done
lemma zcong_lineq_ex:
- "0 < n ==> zgcd (a, n) = 1 ==> \<exists>x. [a * x = 1] (mod n)"
+ "0 < n ==> zgcd a n = 1 ==> \<exists>x. [a * x = 1] (mod n)"
apply (cut_tac m = a and n = n and k = 1 in zgcd_ex_linear, safe)
apply (rule_tac x = s in exI)
apply (rule_tac b = "s * a + t * n" in zcong_trans)
@@ -510,7 +506,7 @@
lemma zcong_lineq_unique:
"0 < n ==>
- zgcd (a, n) = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
+ zgcd a n = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
apply auto
apply (rule_tac [2] zcong_zless_imp_eq)
apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *})
--- a/src/HOL/ex/LocaleTest2.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/ex/LocaleTest2.thy Mon Jul 14 11:04:42 2008 +0200
@@ -592,26 +592,26 @@
qed
interpretation nat_dvd: dlat ["op dvd :: [nat, nat] => bool"]
- where "dlat.meet (op dvd) (x::nat) y = gcd (x, y)"
- and "dlat.join (op dvd) (x::nat) y = lcm (x, y)"
+ where "dlat.meet (op dvd) (x::nat) y = gcd x y"
+ and "dlat.join (op dvd) (x::nat) y = lcm x y"
proof -
show "dlat (op dvd :: [nat, nat] => bool)"
apply unfold_locales
apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
- apply (rule_tac x = "gcd (x, y)" in exI)
+ apply (rule_tac x = "gcd x y" in exI)
apply auto [1]
- apply (rule_tac x = "lcm (x, y)" in exI)
+ apply (rule_tac x = "lcm x y" in exI)
apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
done
then interpret nat_dvd: dlat ["op dvd :: [nat, nat] => bool"] .
txt {* Interpretation to ease use of definitions, which are
conditional in general but unconditional after interpretation. *}
- show "dlat.meet (op dvd) (x::nat) y = gcd (x, y)"
+ show "dlat.meet (op dvd) (x::nat) y = gcd x y"
apply (unfold nat_dvd.meet_def)
apply (rule the_equality)
apply (unfold nat_dvd.is_inf_def)
by auto
- show "dlat.join (op dvd) (x::nat) y = lcm (x, y)"
+ show "dlat.join (op dvd) (x::nat) y = lcm x y"
apply (unfold nat_dvd.join_def)
apply (rule the_equality)
apply (unfold nat_dvd.is_sup_def)
@@ -624,7 +624,7 @@
lemma "((x::nat) dvd y & x ~= y) = (x dvd y & x ~= y)"
apply (rule nat_dvd.less_def) done
thm nat_dvd.meet_left text {* from dlat *}
-lemma "gcd (x, y) dvd x"
+lemma "gcd x y dvd x"
apply (rule nat_dvd.meet_left) done
print_interps dpo
--- a/src/HOL/ex/Reflected_Presburger.thy Fri Jul 11 23:17:25 2008 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Mon Jul 14 11:04:42 2008 +0200
@@ -1077,8 +1077,8 @@
"plusinf p = p"
recdef \<delta> "measure size"
- "\<delta> (And p q) = ilcm (\<delta> p) (\<delta> q)"
- "\<delta> (Or p q) = ilcm (\<delta> p) (\<delta> q)"
+ "\<delta> (And p q) = zlcm (\<delta> p) (\<delta> q)"
+ "\<delta> (Or p q) = zlcm (\<delta> p) (\<delta> q)"
"\<delta> (Dvd i (CN 0 c e)) = i"
"\<delta> (NDvd i (CN 0 c e)) = i"
"\<delta> p = 1"
@@ -1110,20 +1110,20 @@
proof (induct p rule: iszlfm.induct)
case (1 p q)
let ?d = "\<delta> (And p q)"
- from prems ilcm_pos have dp: "?d >0" by simp
+ from prems zlcm_pos have dp: "?d >0" by simp
have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp
- hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp del:dvd_ilcm_self1)
+ hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp del:dvd_zlcm_self1)
have "\<delta> q dvd \<delta> (And p q)" using prems by simp
- hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_ilcm_self2)
+ hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_zlcm_self2)
from th th' dp show ?case by simp
next
case (2 p q)
let ?d = "\<delta> (And p q)"
- from prems ilcm_pos have dp: "?d >0" by simp
+ from prems zlcm_pos have dp: "?d >0" by simp
have "\<delta> p dvd \<delta> (And p q)" using prems by simp
- hence th: "d\<delta> p ?d" using delta_mono prems by(simp del:dvd_ilcm_self1)
+ hence th: "d\<delta> p ?d" using delta_mono prems by(simp del:dvd_zlcm_self1)
have "\<delta> q dvd \<delta> (And p q)" using prems by simp
- hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_ilcm_self2)
+ hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:dvd_zlcm_self2)
from th th' dp show ?case by simp
qed simp_all
@@ -1162,8 +1162,8 @@
"d\<beta> p = (\<lambda> k. True)"
recdef \<zeta> "measure size"
- "\<zeta> (And p q) = ilcm (\<zeta> p) (\<zeta> q)"
- "\<zeta> (Or p q) = ilcm (\<zeta> p) (\<zeta> q)"
+ "\<zeta> (And p q) = zlcm (\<zeta> p) (\<zeta> q)"
+ "\<zeta> (Or p q) = zlcm (\<zeta> p) (\<zeta> q)"
"\<zeta> (Eq (CN 0 c e)) = c"
"\<zeta> (NEq (CN 0 c e)) = c"
"\<zeta> (Lt (CN 0 c e)) = c"
@@ -1412,19 +1412,19 @@
using linp
proof(induct p rule: iszlfm.induct)
case (1 p q)
- from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
- from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
- from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"]
- d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"]
- dl1 dl2 show ?case by (auto simp add: ilcm_pos)
+ from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
+ from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
+ from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"]
+ d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"]
+ dl1 dl2 show ?case by (auto simp add: zlcm_pos)
next
case (2 p q)
- from prems have dl1: "\<zeta> p dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
- from prems have dl2: "\<zeta> q dvd ilcm (\<zeta> p) (\<zeta> q)" by simp
- from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="ilcm (\<zeta> p) (\<zeta> q)"]
- d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="ilcm (\<zeta> p) (\<zeta> q)"]
- dl1 dl2 show ?case by (auto simp add: ilcm_pos)
-qed (auto simp add: ilcm_pos)
+ from prems have dl1: "\<zeta> p dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
+ from prems have dl2: "\<zeta> q dvd zlcm (\<zeta> p) (\<zeta> q)" by simp
+ from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="zlcm (\<zeta> p) (\<zeta> q)"]
+ d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="zlcm (\<zeta> p) (\<zeta> q)"]
+ dl1 dl2 show ?case by (auto simp add: zlcm_pos)
+qed (auto simp add: zlcm_pos)
lemma a\<beta>: assumes linp: "iszlfm p" and d: "d\<beta> p l" and lp: "l > 0"
shows "iszlfm (a\<beta> p l) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a\<beta> p l) = Ifm bbs (x#bs) p)"