src/HOL/Library/Abstract_Rat.thy
 changeset 27556 292098f2efdf parent 27368 9f90ac19e32b child 27567 e3fe9a327c63
```     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Fri Jul 11 23:17:25 2008 +0200
1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Mon Jul 14 11:04:42 2008 +0200
1.3 @@ -22,13 +22,13 @@
1.4  definition
1.5    isnormNum :: "Num \<Rightarrow> bool"
1.6  where
1.7 -  "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> igcd a b = 1))"
1.8 +  "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> zgcd a b = 1))"
1.9
1.10  definition
1.11    normNum :: "Num \<Rightarrow> Num"
1.12  where
1.13    "normNum = (\<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else
1.14 -  (let g = igcd a b
1.15 +  (let g = zgcd a b
1.16     in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
1.17
1.18  lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
1.19 @@ -38,19 +38,19 @@
1.20    {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}
1.21    moreover
1.22    {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0"
1.23 -    let ?g = "igcd a b"
1.24 +    let ?g = "zgcd a b"
1.25      let ?a' = "a div ?g"
1.26      let ?b' = "b div ?g"
1.27 -    let ?g' = "igcd ?a' ?b'"
1.28 -    from anz bnz have "?g \<noteq> 0" by simp  with igcd_pos[of a b]
1.29 +    let ?g' = "zgcd ?a' ?b'"
1.30 +    from anz bnz have "?g \<noteq> 0" by simp  with zgcd_pos[of a b]
1.31      have gpos: "?g > 0"  by arith
1.32 -    have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2)
1.33 +    have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_dvd1 zgcd_dvd2)
1.34      from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
1.35      anz bnz
1.36      have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
1.37 -      by - (rule notI,simp add:igcd_def)+
1.38 +      by - (rule notI,simp add:zgcd_def)+
1.39      from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by blast
1.40 -    from div_igcd_relprime[OF stupid] have gp1: "?g' = 1" .
1.41 +    from div_zgcd_relprime[OF stupid] have gp1: "?g' = 1" .
1.42      from bnz have "b < 0 \<or> b > 0" by arith
1.43      moreover
1.44      {assume b: "b > 0"
1.45 @@ -84,7 +84,7 @@
1.46  definition
1.47    Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
1.48  where
1.49 -  "Nmul = (\<lambda>(a,b) (a',b'). let g = igcd (a*a') (b*b')
1.50 +  "Nmul = (\<lambda>(a,b) (a',b'). let g = zgcd (a*a') (b*b')
1.51      in (a*a' div g, b*b' div g))"
1.52
1.53  definition
1.54 @@ -120,11 +120,11 @@
1.55    then obtain a b a' b' where ab: "x = (a,b)"  and ab': "y = (a',b')" by blast
1.56    {assume "a = 0"
1.57      hence ?thesis using xn ab ab'
1.58 -      by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
1.59 +      by (simp add: zgcd_def isnormNum_def Let_def Nmul_def split_def)}
1.60    moreover
1.61    {assume "a' = 0"
1.62      hence ?thesis using yn ab ab'
1.63 -      by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
1.64 +      by (simp add: zgcd_def isnormNum_def Let_def Nmul_def split_def)}
1.65    moreover
1.66    {assume a: "a \<noteq>0" and a': "a'\<noteq>0"
1.67      hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def)
1.68 @@ -136,11 +136,11 @@
1.69
1.70  lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
1.71    by (simp add: Ninv_def isnormNum_def split_def)
1.72 -    (cases "fst x = 0", auto simp add: igcd_commute)
1.73 +    (cases "fst x = 0", auto simp add: zgcd_commute)
1.74
1.75  lemma isnormNum_int[simp]:
1.76    "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
1.77 -  by (simp_all add: isnormNum_def igcd_def)
1.78 +  by (simp_all add: isnormNum_def zgcd_def)
1.79
1.80
1.81  text {* Relations over Num *}
1.82 @@ -201,8 +201,8 @@
1.83      from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
1.84      from prems have eq:"a * b' = a'*b"
1.85        by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
1.86 -    from prems have gcd1: "igcd a b = 1" "igcd b a = 1" "igcd a' b' = 1" "igcd b' a' = 1"
1.88 +    from prems have gcd1: "zgcd a b = 1" "zgcd b a = 1" "zgcd a' b' = 1" "zgcd b' a' = 1"
1.90      from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
1.91        apply(unfold dvd_def)
1.92        apply (rule_tac x="b'" in exI, simp add: mult_ac)
1.93 @@ -257,7 +257,7 @@
1.94        by (simp add: INum_def normNum_def split_def Let_def)}
1.95    moreover
1.96    {assume a: "a\<noteq>0" and b: "b\<noteq>0"
1.97 -    let ?g = "igcd a b"
1.98 +    let ?g = "zgcd a b"
1.99      from a b have g: "?g \<noteq> 0"by simp
1.100      from of_int_div[OF g, where ?'a = 'a]
1.101      have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)}
1.102 @@ -293,13 +293,13 @@
1.103        from z aa' bb' have ?thesis
1.105      moreover {assume z: "a * b' + b * a' \<noteq> 0"
1.106 -      let ?g = "igcd (a * b' + b * a') (b*b')"
1.107 +      let ?g = "zgcd (a * b' + b * a') (b*b')"
1.108        have gz: "?g \<noteq> 0" using z by simp
1.109        have ?thesis using aa' bb' z gz
1.110  	of_int_div[where ?'a = 'a,
1.111 -	OF gz igcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
1.112 +	OF gz zgcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
1.113  	of_int_div[where ?'a = 'a,
1.114 -	OF gz igcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
1.115 +	OF gz zgcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
1.117      ultimately have ?thesis using aa' bb'
1.119 @@ -318,10 +318,10 @@
1.120        done }
1.121    moreover
1.122    {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
1.123 -    let ?g="igcd (a*a') (b*b')"
1.124 +    let ?g="zgcd (a*a') (b*b')"
1.125      have gz: "?g \<noteq> 0" using z by simp
1.126 -    from z of_int_div[where ?'a = 'a, OF gz igcd_dvd1[where i="a*a'" and j="b*b'"]]
1.127 -      of_int_div[where ?'a = 'a , OF gz igcd_dvd2[where i="a*a'" and j="b*b'"]]
1.128 +    from z of_int_div[where ?'a = 'a, OF gz zgcd_dvd1[where i="a*a'" and j="b*b'"]]
1.129 +      of_int_div[where ?'a = 'a , OF gz zgcd_dvd2[where i="a*a'" and j="b*b'"]]
1.130      have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
1.131    ultimately show ?thesis by blast
1.132  qed
1.133 @@ -456,7 +456,7 @@
1.134  qed
1.135
1.136  lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
1.137 -  by (simp add: Nmul_def split_def Let_def igcd_commute mult_commute)
1.138 +  by (simp add: Nmul_def split_def Let_def zgcd_commute mult_commute)
1.139
1.140  lemma Nmul_assoc: assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
1.141    shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
```