--- 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)"