# HG changeset patch # User haftmann # Date 1216026282 -7200 # Node ID 292098f2efdf59807aaa556ae5a99d1e28ec006f # Parent dfda3192dec29c8ef2456e73289b41e5fde15c20 unified curried gcd, lcm, zgcd, zlcm diff -r dfda3192dec2 -r 292098f2efdf NEWS --- 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. diff -r dfda3192dec2 -r 292098f2efdf src/HOL/Complex/ex/MIR.thy --- 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) = (\g. igcd i g)" - "numgcdh (CN n c t) = (\g. igcd c (numgcdh t g))" - "numgcdh (CF c s t) = (\g. igcd c (numgcdh t g))" + "numgcdh (C i) = (\g. zgcd i g)" + "numgcdh (CN n c t) = (\g. zgcd c (numgcdh t g))" + "numgcdh (CF c s t) = (\g. zgcd c (numgcdh t g))" "numgcdh t = (\g. 1)" definition @@ -687,13 +687,13 @@ shows "Inum bs t = 0" proof- have "\x. numgcdh t x= 0 \ 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 \ 0" shows "numgcdh t g \ 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 \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 \ ((abs i > 1 \ abs j > 1) \ (abs i = 0 \ abs j > 1) \ (abs i > 1 \ abs j = 0))" - apply (unfold igcd_def) +lemma zgcd_gt1: "zgcd i j > 1 \ ((abs i > 1 \ abs j > 1) \ (abs i = 0 \ abs j > 1) \ (abs i > 1 \ 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 \ 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 \ 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 \ ?g > 1) \ (abs c = 0 \ ?g > 1) \ (abs c > 1 \ ?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 \ ?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 \ ?g > 1) \ (abs c = 0 \ ?g > 1) \ (abs c > 1 \ ?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 \ ?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) \ numgcd t > 0" @@ -1041,7 +1041,7 @@ constdefs simp_num_pair:: "(num \ int) \ num \ int" "simp_num_pair \ (\ (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 \ 0" {assume "\ ?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' \ 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' \ 0" by simp + hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith hence "?g'= 1 \ ?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 \ 0" {assume "\ ?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' \ 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' \ 0" by simp + hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith hence "?g'= 1 \ ?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' \ n" . from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]] @@ -1219,7 +1219,7 @@ constdefs simpdvd:: "int \ num \ (int \ num)" "simpdvd d t \ (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 "\ ?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' \ 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' \ 0" by simp + hence g'p: "?g' > 0" using zgcd_pos[where i="d" and j="numgcd t"] by arith hence "?g'= 1 \ ?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 \ "measure size" - "\ (And p q) = ilcm (\ p) (\ q)" - "\ (Or p q) = ilcm (\ p) (\ q)" + "\ (And p q) = zlcm (\ p) (\ q)" + "\ (Or p q) = zlcm (\ p) (\ q)" "\ (Dvd i (CN 0 c e)) = i" "\ (NDvd i (CN 0 c e)) = i" "\ p = 1" @@ -2126,20 +2126,20 @@ proof (induct p rule: iszlfm.induct) case (1 p q) let ?d = "\ (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: "\ p dvd \ (And p q)" using prems by simp hence th: "d\ 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 "\ q dvd \ (And p q)" using prems by simp - hence th': "d\ q ?d" using delta_mono prems by (auto simp del: dvd_ilcm_self2) + hence th': "d\ 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 = "\ (And p q)" - from prems ilcm_pos have dp: "?d >0" by simp + from prems zlcm_pos have dp: "?d >0" by simp have "\ p dvd \ (And p q)" using prems by simp hence th: "d\ p ?d" using delta_mono prems - by (auto simp del: dvd_ilcm_self1) - have "\ q dvd \ (And p q)" using prems by simp hence th': "d\ q ?d" using delta_mono prems by (auto simp del: dvd_ilcm_self2) + by (auto simp del: dvd_zlcm_self1) + have "\ q dvd \ (And p q)" using prems by simp hence th': "d\ 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\ p = (\ k. True)" recdef \ "measure size" - "\ (And p q) = ilcm (\ p) (\ q)" - "\ (Or p q) = ilcm (\ p) (\ q)" + "\ (And p q) = zlcm (\ p) (\ q)" + "\ (Or p q) = zlcm (\ p) (\ q)" "\ (Eq (CN 0 c e)) = c" "\ (NEq (CN 0 c e)) = c" "\ (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: "\ p dvd ilcm (\ p) (\ q)" by simp - from prems have dl2: "\ q dvd ilcm (\ p) (\ q)" by simp - from prems d\_mono[where p = "p" and l="\ p" and l'="ilcm (\ p) (\ q)"] - d\_mono[where p = "q" and l="\ q" and l'="ilcm (\ p) (\ q)"] - dl1 dl2 show ?case by (auto simp add: ilcm_pos) + from prems have dl1: "\ p dvd zlcm (\ p) (\ q)" by simp + from prems have dl2: "\ q dvd zlcm (\ p) (\ q)" by simp + from prems d\_mono[where p = "p" and l="\ p" and l'="zlcm (\ p) (\ q)"] + d\_mono[where p = "q" and l="\ q" and l'="zlcm (\ p) (\ q)"] + dl1 dl2 show ?case by (auto simp add: zlcm_pos) next case (2 p q) - from prems have dl1: "\ p dvd ilcm (\ p) (\ q)" by simp - from prems have dl2: "\ q dvd ilcm (\ p) (\ q)" by simp - from prems d\_mono[where p = "p" and l="\ p" and l'="ilcm (\ p) (\ q)"] - d\_mono[where p = "q" and l="\ q" and l'="ilcm (\ p) (\ q)"] - dl1 dl2 show ?case by (auto simp add: ilcm_pos) -qed (auto simp add: ilcm_pos) + from prems have dl1: "\ p dvd zlcm (\ p) (\ q)" by simp + from prems have dl2: "\ q dvd zlcm (\ p) (\ q)" by simp + from prems d\_mono[where p = "p" and l="\ p" and l'="zlcm (\ p) (\ q)"] + d\_mono[where p = "q" and l="\ q" and l'="zlcm (\ p) (\ q)"] + dl1 dl2 show ?case by (auto simp add: zlcm_pos) +qed (auto simp add: zlcm_pos) lemma a\: assumes linp: "iszlfm p (a #bs)" and d: "d\ p l" and lp: "l > 0" shows "iszlfm (a\ p l) (a #bs) \ d\ (a\ p l) 1 \ (Ifm (real (l * x) #bs) (a\ p l) = Ifm ((real x)#bs) p)" @@ -4171,9 +4171,9 @@ lemma bound0at_l : "\isatom p ; bound0 p\ \ isrlfm p" by (induct p rule: isrlfm.induct, auto) -lemma igcd_le1: assumes ip: "0 < i" shows "igcd i j \ i" +lemma zgcd_le1: assumes ip: "0 < i" shows "zgcd i j \ 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)) \ c" - by (simp add: numgcd_def igcd_le1) + by (simp add: numgcd_def zgcd_le1) from prems have th': "c\0" by auto from prems have cp: "c \ 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)) \ c" - by (simp add: numgcd_def igcd_le1) + by (simp add: numgcd_def zgcd_le1) from prems have th': "c\0" by auto from prems have cp: "c \ 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)) \ c" - by (simp add: numgcd_def igcd_le1) + by (simp add: numgcd_def zgcd_le1) from prems have th': "c\0" by auto from prems have cp: "c \ 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)) \ c" - by (simp add: numgcd_def igcd_le1) + by (simp add: numgcd_def zgcd_le1) from prems have th': "c\0" by auto from prems have cp: "c \ 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)) \ c" - by (simp add: numgcd_def igcd_le1) + by (simp add: numgcd_def zgcd_le1) from prems have th': "c\0" by auto from prems have cp: "c \ 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)) \ c" - by (simp add: numgcd_def igcd_le1) + by (simp add: numgcd_def zgcd_le1) from prems have th': "c\0" by auto from prems have cp: "c \ 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 "(\ x. ?I x ?q ) = ((?I x (minusinf ?rq)) \ (?I x (plusinf ?rq )) \ (\ (t,n) \ set (\ ?rq). \ (s,m) \ set (\ ?rq ). ?I x (\ ?rq (Add (Mul m t) (Mul n s), 2*n*m))))" @@ -5284,7 +5284,7 @@ let ?F = "\ p. \ a \ set (\ p). \ b \ set (\ p). ?I x (\ p (?g(a,b)))" let ?ep = "evaldjf (\ ?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 \ (set ?U \ set ?U)" by simp from \_l[OF lq] have U_l: "\ (t,n) \ set ?U. numbound0 t \ n > 0" . from U_l UpU diff -r dfda3192dec2 -r 292098f2efdf src/HOL/Complex/ex/ReflectedFerrack.thy --- 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) = (\g. igcd i g)" - "numgcdh (CN n c t) = (\g. igcd c (numgcdh t g))" + "numgcdh (C i) = (\g. zgcd i g)" + "numgcdh (CN n c t) = (\g. zgcd c (numgcdh t g))" "numgcdh t = (\g. 1)" defs numgcd_def [code func]: "numgcd t \ 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 \ 0" shows "numgcdh t g \ 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 \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 \ ((abs i > 1 \ abs j > 1) \ (abs i = 0 \ abs j > 1) \ (abs i > 1 \ abs j = 0))" - apply (cases "abs i = 0", simp_all add: igcd_def) +lemma zgcd_gt1: "zgcd i j > 1 \ ((abs i > 1 \ abs j > 1) \ (abs i = 0 \ abs j > 1) \ (abs i > 1 \ 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 \ 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 \ 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 \ ?g > 1) \ (abs c = 0 \ ?g > 1) \ (abs c > 1 \ ?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 \ ?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) \ numgcd t > 0" @@ -727,7 +727,7 @@ constdefs simp_num_pair:: "(num \ int) \ num \ int" "simp_num_pair \ (\ (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 \ 0" {assume "\ ?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' \ 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' \ 0" by simp + hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith hence "?g'= 1 \ ?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 \ 0" {assume "\ ?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' \ 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' \ 0" by simp + hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith hence "?g'= 1 \ ?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' \ n" . from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]] diff -r dfda3192dec2 -r 292098f2efdf src/HOL/Complex/ex/Sqrt.thy --- 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 \ \" - obtains m n where "n \ 0" and "\x\ = real m / real n" and "gcd (m, n) = 1" + obtains m n where "n \ 0" and "\x\ = real m / real n" and "gcd m n = 1" proof - from `x \ \` obtain m n :: nat where n: "n \ 0" and x_rat: "\x\ = real m / real n" unfolding rationals_def by blast - let ?gcd = "gcd (m, n)" + let ?gcd = "gcd m n" from n have gcd: "?gcd \ 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) \ \" then obtain m n where n: "n \ 0" and sqrt_rat: "\sqrt (real p)\ = real m / real n" - and gcd: "gcd (m, n) = 1" .. + and gcd: "gcd m n = 1" .. have eq: "m\ = p * n\" proof - from n and sqrt_rat have "real m = \sqrt (real p)\ * real n" by simp @@ -96,7 +96,7 @@ then have "p dvd n\" .. 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 \ 1" by (simp add: dvd_imp_le) with p show False by simp @@ -122,7 +122,7 @@ assume "sqrt (real p) \ \" then obtain m n where n: "n \ 0" and sqrt_rat: "\sqrt (real p)\ = real m / real n" - and gcd: "gcd (m, n) = 1" .. + and gcd: "gcd m n = 1" .. from n and sqrt_rat have "real m = \sqrt (real p)\ * real n" by simp then have "real (m\) = (sqrt (real p))\ * real (n\)" by (auto simp add: power2_eq_square) @@ -136,7 +136,7 @@ with p have "n\ = p * k\" by (simp add: power2_eq_square) then have "p dvd n\" .. 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 \ 1" by (simp add: dvd_imp_le) with p show False by simp diff -r dfda3192dec2 -r 292098f2efdf src/HOL/Isar_examples/Fibonacci.thy --- 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 diff -r dfda3192dec2 -r 292098f2efdf src/HOL/Library/Abstract_Rat.thy --- 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 \ bool" where - "isnormNum = (\(a,b). (if a = 0 then b = 0 else b > 0 \ igcd a b = 1))" + "isnormNum = (\(a,b). (if a = 0 then b = 0 else b > 0 \ zgcd a b = 1))" definition normNum :: "Num \ Num" where "normNum = (\(a,b). (if a=0 \ 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 \ b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)} moreover {assume anz: "a \ 0" and bnz: "b \ 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 \ 0" by simp with igcd_pos[of a b] + let ?g' = "zgcd ?a' ?b'" + from anz bnz have "?g \ 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' \ 0" "?b' \ 0" - by - (rule notI,simp add:igcd_def)+ + by - (rule notI,simp add:zgcd_def)+ from anz bnz have stupid: "a \ 0 \ b \ 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 \ b > 0" by arith moreover {assume b: "b > 0" @@ -84,7 +84,7 @@ definition Nmul :: "Num \ Num \ Num" (infixl "*\<^sub>N" 60) where - "Nmul = (\(a,b) (a',b'). let g = igcd (a*a') (b*b') + "Nmul = (\(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 \0" and a': "a'\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 \ 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 \ 0 \ 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\0" and b: "b\0" - let ?g = "igcd a b" + let ?g = "zgcd a b" from a b have g: "?g \ 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' \ 0" - let ?g = "igcd (a * b' + b * a') (b*b')" + let ?g = "zgcd (a * b' + b * a') (b*b')" have gz: "?g \ 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 \ 0" "a' \ 0" "b \ 0" "b' \ 0" - let ?g="igcd (a*a') (b*b')" + let ?g="zgcd (a*a') (b*b')" have gz: "?g \ 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 \ isnormNum y \ 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)" diff -r dfda3192dec2 -r 292098f2efdf src/HOL/Library/GCD.thy --- 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 \ nat \ nat \ bool" where -- {* @{term gcd} as a relation *} - [code func del]: "is_gcd p m n \ p dvd m \ p dvd n \ + [code func del]: "is_gcd m n p \ p dvd m \ p dvd n \ (\d. d dvd m \ d dvd n \ d dvd p)" text {* Uniqueness *} -lemma is_gcd_unique: "is_gcd m a b \ is_gcd n a b \ m = n" +lemma is_gcd_unique: "is_gcd a b m \ is_gcd a b n \ 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 \ k dvd a \ k dvd b \ k dvd m" +lemma is_gcd_dvd: "is_gcd a b m \ k dvd a \ k dvd b \ 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 \ nat => nat" -where - "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))" +fun gcd :: "nat \ nat \ 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 "\m. P m 0" and "\m n. 0 < n \ P n (m mod n) \ 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 \ gcd (m, n) = gcd (n, m mod n)" +lemma gcd_non_0: "n > 0 \ 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 \ k dvd n \ k dvd gcd (m, n)" +lemma gcd_greatest: "k dvd m \ k dvd n \ 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) \ k dvd m \ k dvd n" +lemma gcd_greatest_iff [iff]: "k dvd gcd m n \ k dvd m \ k dvd n" by (blast intro!: gcd_greatest intro: dvd_trans) -lemma gcd_zero: "gcd (m, n) = 0 \ m = 0 \ n = 0" +lemma gcd_zero: "gcd m n = 0 \ m = 0 \ 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 \ 0 \ b \ 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 \ nat \ nat" + lcm :: "nat \