src/HOL/Library/Abstract_Rat.thy
changeset 31706 1db0c8f235fb
parent 30663 0b6aff7451b2
child 31952 40501bb2d57c
child 31963 663a725dc339
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Tue Jun 16 22:07:39 2009 -0700
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Wed Jun 17 16:55:01 2009 -0700
     1.3 @@ -21,17 +21,17 @@
     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> zgcd a b = 1))"
     1.8 +  "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> gcd 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 = zgcd a b 
    1.15 +  (let g = gcd 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 -declare zgcd_zdvd1[presburger] 
    1.19 -declare zgcd_zdvd2[presburger]
    1.20 +declare int_gcd_dvd1[presburger]
    1.21 +declare int_gcd_dvd2[presburger]
    1.22  lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
    1.23  proof -
    1.24    have " \<exists> a b. x = (a,b)" by auto
    1.25 @@ -39,19 +39,19 @@
    1.26    {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}  
    1.27    moreover
    1.28    {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0" 
    1.29 -    let ?g = "zgcd a b"
    1.30 +    let ?g = "gcd a b"
    1.31      let ?a' = "a div ?g"
    1.32      let ?b' = "b div ?g"
    1.33 -    let ?g' = "zgcd ?a' ?b'"
    1.34 -    from anz bnz have "?g \<noteq> 0" by simp  with zgcd_pos[of a b] 
    1.35 +    let ?g' = "gcd ?a' ?b'"
    1.36 +    from anz bnz have "?g \<noteq> 0" by simp  with int_gcd_ge_0[of a b] 
    1.37      have gpos: "?g > 0"  by arith
    1.38      have gdvd: "?g dvd a" "?g dvd b" by arith+ 
    1.39      from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
    1.40      anz bnz
    1.41 -    have nz':"?a' \<noteq> 0" "?b' \<noteq> 0" 
    1.42 -      by - (rule notI,simp add:zgcd_def)+
    1.43 +    have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
    1.44 +      by - (rule notI, simp)+
    1.45      from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith 
    1.46 -    from div_zgcd_relprime[OF stupid] have gp1: "?g' = 1" .
    1.47 +    from int_div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
    1.48      from bnz have "b < 0 \<or> b > 0" by arith
    1.49      moreover
    1.50      {assume b: "b > 0"
    1.51 @@ -67,7 +67,7 @@
    1.52  	have False using b by arith }
    1.53        hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric]) 
    1.54        from anz bnz nz' b b' gp1 have ?thesis 
    1.55 -	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    1.56 +	by (simp add: isnormNum_def normNum_def Let_def split_def)}
    1.57      ultimately have ?thesis by blast
    1.58    }
    1.59    ultimately show ?thesis by blast
    1.60 @@ -85,7 +85,7 @@
    1.61  definition
    1.62    Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
    1.63  where
    1.64 -  "Nmul = (\<lambda>(a,b) (a',b'). let g = zgcd (a*a') (b*b') 
    1.65 +  "Nmul = (\<lambda>(a,b) (a',b'). let g = gcd (a*a') (b*b') 
    1.66      in (a*a' div g, b*b' div g))"
    1.67  
    1.68  definition
    1.69 @@ -121,11 +121,11 @@
    1.70    then obtain a b a' b' where ab: "x = (a,b)"  and ab': "y = (a',b')" by blast 
    1.71    {assume "a = 0"
    1.72      hence ?thesis using xn ab ab'
    1.73 -      by (simp add: zgcd_def isnormNum_def Let_def Nmul_def split_def)}
    1.74 +      by (simp add: isnormNum_def Let_def Nmul_def split_def)}
    1.75    moreover
    1.76    {assume "a' = 0"
    1.77      hence ?thesis using yn ab ab' 
    1.78 -      by (simp add: zgcd_def isnormNum_def Let_def Nmul_def split_def)}
    1.79 +      by (simp add: isnormNum_def Let_def Nmul_def split_def)}
    1.80    moreover
    1.81    {assume a: "a \<noteq>0" and a': "a'\<noteq>0"
    1.82      hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def)
    1.83 @@ -137,11 +137,11 @@
    1.84  
    1.85  lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
    1.86    by (simp add: Ninv_def isnormNum_def split_def)
    1.87 -    (cases "fst x = 0", auto simp add: zgcd_commute)
    1.88 +    (cases "fst x = 0", auto simp add: int_gcd_commute)
    1.89  
    1.90  lemma isnormNum_int[simp]: 
    1.91    "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
    1.92 -  by (simp_all add: isnormNum_def zgcd_def)
    1.93 +  by (simp_all add: isnormNum_def)
    1.94  
    1.95  
    1.96  text {* Relations over Num *}
    1.97 @@ -202,8 +202,8 @@
    1.98      from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
    1.99      from prems have eq:"a * b' = a'*b" 
   1.100        by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
   1.101 -    from prems have gcd1: "zgcd a b = 1" "zgcd b a = 1" "zgcd a' b' = 1" "zgcd b' a' = 1"       
   1.102 -      by (simp_all add: isnormNum_def add: zgcd_commute)
   1.103 +    from prems have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"       
   1.104 +      by (simp_all add: isnormNum_def add: int_gcd_commute)
   1.105      from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
   1.106        apply - 
   1.107        apply algebra
   1.108 @@ -211,8 +211,8 @@
   1.109        apply simp
   1.110        apply algebra
   1.111        done
   1.112 -    from zdvd_dvd_eq[OF bz zrelprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
   1.113 -      zrelprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
   1.114 +    from zdvd_dvd_eq[OF bz int_coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
   1.115 +      int_coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
   1.116        have eq1: "b = b'" using pos by arith  
   1.117        with eq have "a = a'" using pos by simp
   1.118        with eq1 have ?rhs by simp}
   1.119 @@ -258,7 +258,7 @@
   1.120        by (simp add: INum_def normNum_def split_def Let_def)}
   1.121    moreover 
   1.122    {assume a: "a\<noteq>0" and b: "b\<noteq>0"
   1.123 -    let ?g = "zgcd a b"
   1.124 +    let ?g = "gcd a b"
   1.125      from a b have g: "?g \<noteq> 0"by simp
   1.126      from of_int_div[OF g, where ?'a = 'a]
   1.127      have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)}
   1.128 @@ -294,11 +294,11 @@
   1.129        from z aa' bb' have ?thesis 
   1.130  	by (simp add: th Nadd_def normNum_def INum_def split_def)}
   1.131      moreover {assume z: "a * b' + b * a' \<noteq> 0"
   1.132 -      let ?g = "zgcd (a * b' + b * a') (b*b')"
   1.133 +      let ?g = "gcd (a * b' + b * a') (b*b')"
   1.134        have gz: "?g \<noteq> 0" using z by simp
   1.135        have ?thesis using aa' bb' z gz
   1.136 -	of_int_div[where ?'a = 'a, OF gz zgcd_zdvd1[where i="a * b' + b * a'" and j="b*b'"]]	of_int_div[where ?'a = 'a,
   1.137 -	OF gz zgcd_zdvd2[where i="a * b' + b * a'" and j="b*b'"]]
   1.138 +	of_int_div[where ?'a = 'a, OF gz int_gcd_dvd1[where x="a * b' + b * a'" and y="b*b'"]]	of_int_div[where ?'a = 'a,
   1.139 +	OF gz int_gcd_dvd2[where x="a * b' + b * a'" and y="b*b'"]]
   1.140  	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
   1.141      ultimately have ?thesis using aa' bb' 
   1.142        by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
   1.143 @@ -317,10 +317,10 @@
   1.144        done }
   1.145    moreover
   1.146    {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
   1.147 -    let ?g="zgcd (a*a') (b*b')"
   1.148 +    let ?g="gcd (a*a') (b*b')"
   1.149      have gz: "?g \<noteq> 0" using z by simp
   1.150 -    from z of_int_div[where ?'a = 'a, OF gz zgcd_zdvd1[where i="a*a'" and j="b*b'"]] 
   1.151 -      of_int_div[where ?'a = 'a , OF gz zgcd_zdvd2[where i="a*a'" and j="b*b'"]] 
   1.152 +    from z of_int_div[where ?'a = 'a, OF gz int_gcd_dvd1[where x="a*a'" and y="b*b'"]] 
   1.153 +      of_int_div[where ?'a = 'a , OF gz int_gcd_dvd2[where x="a*a'" and y="b*b'"]] 
   1.154      have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
   1.155    ultimately show ?thesis by blast
   1.156  qed
   1.157 @@ -478,7 +478,7 @@
   1.158  qed
   1.159  
   1.160  lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
   1.161 -  by (simp add: Nmul_def split_def Let_def zgcd_commute mult_commute)
   1.162 +  by (simp add: Nmul_def split_def Let_def int_gcd_commute mult_commute)
   1.163  
   1.164  lemma Nmul_assoc:
   1.165    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"