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.103 +    from prems have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
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.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.141      ultimately have ?thesis using aa' bb'
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})"
```