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.87 -      by (simp_all add: isnormNum_def add: igcd_commute)
    1.88 +    from prems have gcd1: "zgcd a b = 1" "zgcd b a = 1" "zgcd a' b' = 1" "zgcd b' a' = 1"       
    1.89 +      by (simp_all add: isnormNum_def add: zgcd_commute)
    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.104  	by (simp add: th Nadd_def normNum_def INum_def split_def)}
   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.116  	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
   1.117      ultimately have ?thesis using aa' bb' 
   1.118        by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
   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)"