more convenient place for a theory in solitariness
authorhaftmann
Thu Oct 31 11:44:20 2013 +0100 (2013-10-31)
changeset 542200e6645622f22
parent 54219 63fe59f64578
child 54221 56587960e444
more convenient place for a theory in solitariness
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/Library.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -0,0 +1,521 @@
     1.4 +(*  Title:      HOL/Decision_Procs/Rat_Pair.thy
     1.5 +    Author:     Amine Chaieb
     1.6 +*)
     1.7 +
     1.8 +header {* Rational numbers as pairs *}
     1.9 +
    1.10 +theory Rat_Pair
    1.11 +imports Complex_Main
    1.12 +begin
    1.13 +
    1.14 +type_synonym Num = "int \<times> int"
    1.15 +
    1.16 +abbreviation Num0_syn :: Num  ("0\<^sub>N")
    1.17 +  where "0\<^sub>N \<equiv> (0, 0)"
    1.18 +
    1.19 +abbreviation Numi_syn :: "int \<Rightarrow> Num"  ("'((_)')\<^sub>N")
    1.20 +  where "(i)\<^sub>N \<equiv> (i, 1)"
    1.21 +
    1.22 +definition isnormNum :: "Num \<Rightarrow> bool" where
    1.23 +  "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> gcd a b = 1))"
    1.24 +
    1.25 +definition normNum :: "Num \<Rightarrow> Num" where
    1.26 +  "normNum = (\<lambda>(a,b).
    1.27 +    (if a=0 \<or> b = 0 then (0,0) else
    1.28 +      (let g = gcd a b
    1.29 +       in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
    1.30 +
    1.31 +declare gcd_dvd1_int[presburger] gcd_dvd2_int[presburger]
    1.32 +
    1.33 +lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
    1.34 +proof -
    1.35 +  obtain a b where x: "x = (a, b)" by (cases x)
    1.36 +  { assume "a=0 \<or> b = 0" hence ?thesis by (simp add: x normNum_def isnormNum_def) }
    1.37 +  moreover
    1.38 +  { assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0"
    1.39 +    let ?g = "gcd a b"
    1.40 +    let ?a' = "a div ?g"
    1.41 +    let ?b' = "b div ?g"
    1.42 +    let ?g' = "gcd ?a' ?b'"
    1.43 +    from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b]
    1.44 +    have gpos: "?g > 0" by arith
    1.45 +    have gdvd: "?g dvd a" "?g dvd b" by arith+
    1.46 +    from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] anz bnz
    1.47 +    have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
    1.48 +    from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
    1.49 +    from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
    1.50 +    from bnz have "b < 0 \<or> b > 0" by arith
    1.51 +    moreover
    1.52 +    { assume b: "b > 0"
    1.53 +      from b have "?b' \<ge> 0"
    1.54 +        by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])
    1.55 +      with nz' have b': "?b' > 0" by arith
    1.56 +      from b b' anz bnz nz' gp1 have ?thesis
    1.57 +        by (simp add: x isnormNum_def normNum_def Let_def split_def) }
    1.58 +    moreover {
    1.59 +      assume b: "b < 0"
    1.60 +      { assume b': "?b' \<ge> 0"
    1.61 +        from gpos have th: "?g \<ge> 0" by arith
    1.62 +        from mult_nonneg_nonneg[OF th b'] dvd_mult_div_cancel[OF gdvd(2)]
    1.63 +        have False using b by arith }
    1.64 +      hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
    1.65 +      from anz bnz nz' b b' gp1 have ?thesis
    1.66 +        by (simp add: x isnormNum_def normNum_def Let_def split_def) }
    1.67 +    ultimately have ?thesis by blast
    1.68 +  }
    1.69 +  ultimately show ?thesis by blast
    1.70 +qed
    1.71 +
    1.72 +text {* Arithmetic over Num *}
    1.73 +
    1.74 +definition Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "+\<^sub>N" 60) where
    1.75 +  "Nadd = (\<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b')
    1.76 +    else if a'=0 \<or> b' = 0 then normNum(a,b)
    1.77 +    else normNum(a*b' + b*a', b*b'))"
    1.78 +
    1.79 +definition Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "*\<^sub>N" 60) where
    1.80 +  "Nmul = (\<lambda>(a,b) (a',b'). let g = gcd (a*a') (b*b')
    1.81 +    in (a*a' div g, b*b' div g))"
    1.82 +
    1.83 +definition Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N")
    1.84 +  where "Nneg \<equiv> (\<lambda>(a,b). (-a,b))"
    1.85 +
    1.86 +definition Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "-\<^sub>N" 60)
    1.87 +  where "Nsub = (\<lambda>a b. a +\<^sub>N ~\<^sub>N b)"
    1.88 +
    1.89 +definition Ninv :: "Num \<Rightarrow> Num"
    1.90 +  where "Ninv = (\<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a))"
    1.91 +
    1.92 +definition Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "\<div>\<^sub>N" 60)
    1.93 +  where "Ndiv = (\<lambda>a b. a *\<^sub>N Ninv b)"
    1.94 +
    1.95 +lemma Nneg_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (~\<^sub>N x)"
    1.96 +  by (simp add: isnormNum_def Nneg_def split_def)
    1.97 +
    1.98 +lemma Nadd_normN[simp]: "isnormNum (x +\<^sub>N y)"
    1.99 +  by (simp add: Nadd_def split_def)
   1.100 +
   1.101 +lemma Nsub_normN[simp]: "\<lbrakk> isnormNum y\<rbrakk> \<Longrightarrow> isnormNum (x -\<^sub>N y)"
   1.102 +  by (simp add: Nsub_def split_def)
   1.103 +
   1.104 +lemma Nmul_normN[simp]:
   1.105 +  assumes xn: "isnormNum x" and yn: "isnormNum y"
   1.106 +  shows "isnormNum (x *\<^sub>N y)"
   1.107 +proof -
   1.108 +  obtain a b where x: "x = (a, b)" by (cases x)
   1.109 +  obtain a' b' where y: "y = (a', b')" by (cases y)
   1.110 +  { assume "a = 0"
   1.111 +    hence ?thesis using xn x y
   1.112 +      by (simp add: isnormNum_def Let_def Nmul_def split_def) }
   1.113 +  moreover
   1.114 +  { assume "a' = 0"
   1.115 +    hence ?thesis using yn x y
   1.116 +      by (simp add: isnormNum_def Let_def Nmul_def split_def) }
   1.117 +  moreover
   1.118 +  { assume a: "a \<noteq>0" and a': "a'\<noteq>0"
   1.119 +    hence bp: "b > 0" "b' > 0" using xn yn x y by (simp_all add: isnormNum_def)
   1.120 +    from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a * a', b * b')"
   1.121 +      using x y a a' bp by (simp add: Nmul_def Let_def split_def normNum_def)
   1.122 +    hence ?thesis by simp }
   1.123 +  ultimately show ?thesis by blast
   1.124 +qed
   1.125 +
   1.126 +lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
   1.127 +  by (simp add: Ninv_def isnormNum_def split_def)
   1.128 +    (cases "fst x = 0", auto simp add: gcd_commute_int)
   1.129 +
   1.130 +lemma isnormNum_int[simp]:
   1.131 +  "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i)\<^sub>N"
   1.132 +  by (simp_all add: isnormNum_def)
   1.133 +
   1.134 +
   1.135 +text {* Relations over Num *}
   1.136 +
   1.137 +definition Nlt0:: "Num \<Rightarrow> bool"  ("0>\<^sub>N")
   1.138 +  where "Nlt0 = (\<lambda>(a,b). a < 0)"
   1.139 +
   1.140 +definition Nle0:: "Num \<Rightarrow> bool"  ("0\<ge>\<^sub>N")
   1.141 +  where "Nle0 = (\<lambda>(a,b). a \<le> 0)"
   1.142 +
   1.143 +definition Ngt0:: "Num \<Rightarrow> bool"  ("0<\<^sub>N")
   1.144 +  where "Ngt0 = (\<lambda>(a,b). a > 0)"
   1.145 +
   1.146 +definition Nge0:: "Num \<Rightarrow> bool"  ("0\<le>\<^sub>N")
   1.147 +  where "Nge0 = (\<lambda>(a,b). a \<ge> 0)"
   1.148 +
   1.149 +definition Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool"  (infix "<\<^sub>N" 55)
   1.150 +  where "Nlt = (\<lambda>a b. 0>\<^sub>N (a -\<^sub>N b))"
   1.151 +
   1.152 +definition Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool"  (infix "\<le>\<^sub>N" 55)
   1.153 +  where "Nle = (\<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b))"
   1.154 +
   1.155 +definition "INum = (\<lambda>(a,b). of_int a / of_int b)"
   1.156 +
   1.157 +lemma INum_int [simp]: "INum (i)\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
   1.158 +  by (simp_all add: INum_def)
   1.159 +
   1.160 +lemma isnormNum_unique[simp]:
   1.161 +  assumes na: "isnormNum x" and nb: "isnormNum y"
   1.162 +  shows "((INum x ::'a::{field_char_0, field_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
   1.163 +proof
   1.164 +  obtain a b where x: "x = (a, b)" by (cases x)
   1.165 +  obtain a' b' where y: "y = (a', b')" by (cases y)
   1.166 +  assume H: ?lhs
   1.167 +  { assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0"
   1.168 +    hence ?rhs using na nb H
   1.169 +      by (simp add: x y INum_def split_def isnormNum_def split: split_if_asm) }
   1.170 +  moreover
   1.171 +  { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
   1.172 +    from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: x y isnormNum_def)
   1.173 +    from H bz b'z have eq: "a * b' = a'*b"
   1.174 +      by (simp add: x y INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
   1.175 +    from az a'z na nb have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
   1.176 +      by (simp_all add: x y isnormNum_def add: gcd_commute_int)
   1.177 +    from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
   1.178 +      apply -
   1.179 +      apply algebra
   1.180 +      apply algebra
   1.181 +      apply simp
   1.182 +      apply algebra
   1.183 +      done
   1.184 +    from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
   1.185 +        coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
   1.186 +      have eq1: "b = b'" using pos by arith
   1.187 +      with eq have "a = a'" using pos by simp
   1.188 +      with eq1 have ?rhs by (simp add: x y) }
   1.189 +  ultimately show ?rhs by blast
   1.190 +next
   1.191 +  assume ?rhs thus ?lhs by simp
   1.192 +qed
   1.193 +
   1.194 +
   1.195 +lemma isnormNum0[simp]:
   1.196 +    "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
   1.197 +  unfolding INum_int(2)[symmetric]
   1.198 +  by (rule isnormNum_unique) simp_all
   1.199 +
   1.200 +lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) =
   1.201 +    of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)"
   1.202 +proof -
   1.203 +  assume "d ~= 0"
   1.204 +  let ?t = "of_int (x div d) * ((of_int d)::'a) + of_int(x mod d)"
   1.205 +  let ?f = "\<lambda>x. x / of_int d"
   1.206 +  have "x = (x div d) * d + x mod d"
   1.207 +    by auto
   1.208 +  then have eq: "of_int x = ?t"
   1.209 +    by (simp only: of_int_mult[symmetric] of_int_add [symmetric])
   1.210 +  then have "of_int x / of_int d = ?t / of_int d"
   1.211 +    using cong[OF refl[of ?f] eq] by simp
   1.212 +  then show ?thesis by (simp add: add_divide_distrib algebra_simps `d ~= 0`)
   1.213 +qed
   1.214 +
   1.215 +lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
   1.216 +    (of_int(n div d)::'a::field_char_0) = of_int n / of_int d"
   1.217 +  apply (frule of_int_div_aux [of d n, where ?'a = 'a])
   1.218 +  apply simp
   1.219 +  apply (simp add: dvd_eq_mod_eq_0)
   1.220 +  done
   1.221 +
   1.222 +
   1.223 +lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
   1.224 +proof -
   1.225 +  obtain a b where x: "x = (a, b)" by (cases x)
   1.226 +  { assume "a = 0 \<or> b = 0"
   1.227 +    hence ?thesis by (simp add: x INum_def normNum_def split_def Let_def) }
   1.228 +  moreover
   1.229 +  { assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
   1.230 +    let ?g = "gcd a b"
   1.231 +    from a b have g: "?g \<noteq> 0"by simp
   1.232 +    from of_int_div[OF g, where ?'a = 'a]
   1.233 +    have ?thesis by (auto simp add: x INum_def normNum_def split_def Let_def) }
   1.234 +  ultimately show ?thesis by blast
   1.235 +qed
   1.236 +
   1.237 +lemma INum_normNum_iff:
   1.238 +  "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y"
   1.239 +  (is "?lhs = ?rhs")
   1.240 +proof -
   1.241 +  have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
   1.242 +    by (simp del: normNum)
   1.243 +  also have "\<dots> = ?lhs" by simp
   1.244 +  finally show ?thesis by simp
   1.245 +qed
   1.246 +
   1.247 +lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})"
   1.248 +proof -
   1.249 +  let ?z = "0:: 'a"
   1.250 +  obtain a b where x: "x = (a, b)" by (cases x)
   1.251 +  obtain a' b' where y: "y = (a', b')" by (cases y)
   1.252 +  { assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0"
   1.253 +    hence ?thesis
   1.254 +      apply (cases "a=0", simp_all add: x y Nadd_def)
   1.255 +      apply (cases "b= 0", simp_all add: INum_def)
   1.256 +       apply (cases "a'= 0", simp_all)
   1.257 +       apply (cases "b'= 0", simp_all)
   1.258 +       done }
   1.259 +  moreover
   1.260 +  { assume aa': "a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0"
   1.261 +    { assume z: "a * b' + b * a' = 0"
   1.262 +      hence "of_int (a*b' + b*a') / (of_int b* of_int b') = ?z" by simp
   1.263 +      hence "of_int b' * of_int a / (of_int b * of_int b') +
   1.264 +          of_int b * of_int a' / (of_int b * of_int b') = ?z"
   1.265 +        by (simp add:add_divide_distrib)
   1.266 +      hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa'
   1.267 +        by simp
   1.268 +      from z aa' bb' have ?thesis
   1.269 +        by (simp add: x y th Nadd_def normNum_def INum_def split_def) }
   1.270 +    moreover {
   1.271 +      assume z: "a * b' + b * a' \<noteq> 0"
   1.272 +      let ?g = "gcd (a * b' + b * a') (b*b')"
   1.273 +      have gz: "?g \<noteq> 0" using z by simp
   1.274 +      have ?thesis using aa' bb' z gz
   1.275 +        of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]
   1.276 +        of_int_div[where ?'a = 'a, OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
   1.277 +        by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib) }
   1.278 +    ultimately have ?thesis using aa' bb'
   1.279 +      by (simp add: x y Nadd_def INum_def normNum_def Let_def) }
   1.280 +  ultimately show ?thesis by blast
   1.281 +qed
   1.282 +
   1.283 +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero})"
   1.284 +proof -
   1.285 +  let ?z = "0::'a"
   1.286 +  obtain a b where x: "x = (a, b)" by (cases x)
   1.287 +  obtain a' b' where y: "y = (a', b')" by (cases y)
   1.288 +  { assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0"
   1.289 +    hence ?thesis
   1.290 +      apply (cases "a=0", simp_all add: x y Nmul_def INum_def Let_def)
   1.291 +      apply (cases "b=0", simp_all)
   1.292 +      apply (cases "a'=0", simp_all)
   1.293 +      done }
   1.294 +  moreover
   1.295 +  { assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
   1.296 +    let ?g="gcd (a*a') (b*b')"
   1.297 +    have gz: "?g \<noteq> 0" using z by simp
   1.298 +    from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]]
   1.299 +      of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]]
   1.300 +    have ?thesis by (simp add: Nmul_def x y Let_def INum_def) }
   1.301 +  ultimately show ?thesis by blast
   1.302 +qed
   1.303 +
   1.304 +lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
   1.305 +  by (simp add: Nneg_def split_def INum_def)
   1.306 +
   1.307 +lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
   1.308 +  by (simp add: Nsub_def split_def)
   1.309 +
   1.310 +lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)"
   1.311 +  by (simp add: Ninv_def INum_def split_def)
   1.312 +
   1.313 +lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})"
   1.314 +  by (simp add: Ndiv_def)
   1.315 +
   1.316 +lemma Nlt0_iff[simp]:
   1.317 +  assumes nx: "isnormNum x"
   1.318 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x"
   1.319 +proof -
   1.320 +  obtain a b where x: "x = (a, b)" by (cases x)
   1.321 +  { assume "a = 0" hence ?thesis by (simp add: x Nlt0_def INum_def) }
   1.322 +  moreover
   1.323 +  { assume a: "a \<noteq> 0" hence b: "(of_int b::'a) > 0"
   1.324 +      using nx by (simp add: x isnormNum_def)
   1.325 +    from pos_divide_less_eq[OF b, where b="of_int a" and a="0::'a"]
   1.326 +    have ?thesis by (simp add: x Nlt0_def INum_def) }
   1.327 +  ultimately show ?thesis by blast
   1.328 +qed
   1.329 +
   1.330 +lemma Nle0_iff[simp]:
   1.331 +  assumes nx: "isnormNum x"
   1.332 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<le> 0) = 0\<ge>\<^sub>N x"
   1.333 +proof -
   1.334 +  obtain a b where x: "x = (a, b)" by (cases x)
   1.335 +  { assume "a = 0" hence ?thesis by (simp add: x Nle0_def INum_def) }
   1.336 +  moreover
   1.337 +  { assume a: "a \<noteq> 0" hence b: "(of_int b :: 'a) > 0"
   1.338 +      using nx by (simp add: x isnormNum_def)
   1.339 +    from pos_divide_le_eq[OF b, where b="of_int a" and a="0::'a"]
   1.340 +    have ?thesis by (simp add: x Nle0_def INum_def) }
   1.341 +  ultimately show ?thesis by blast
   1.342 +qed
   1.343 +
   1.344 +lemma Ngt0_iff[simp]:
   1.345 +  assumes nx: "isnormNum x"
   1.346 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
   1.347 +proof -
   1.348 +  obtain a b where x: "x = (a, b)" by (cases x)
   1.349 +  { assume "a = 0" hence ?thesis by (simp add: x Ngt0_def INum_def) }
   1.350 +  moreover
   1.351 +  { assume a: "a \<noteq> 0" hence b: "(of_int b::'a) > 0" using nx
   1.352 +      by (simp add: x isnormNum_def)
   1.353 +    from pos_less_divide_eq[OF b, where b="of_int a" and a="0::'a"]
   1.354 +    have ?thesis by (simp add: x Ngt0_def INum_def) }
   1.355 +  ultimately show ?thesis by blast
   1.356 +qed
   1.357 +
   1.358 +lemma Nge0_iff[simp]:
   1.359 +  assumes nx: "isnormNum x"
   1.360 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
   1.361 +proof -
   1.362 +  obtain a b where x: "x = (a, b)" by (cases x)
   1.363 +  { assume "a = 0" hence ?thesis by (simp add: x Nge0_def INum_def) }
   1.364 +  moreover
   1.365 +  { assume "a \<noteq> 0" hence b: "(of_int b::'a) > 0" using nx
   1.366 +      by (simp add: x isnormNum_def)
   1.367 +    from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"]
   1.368 +    have ?thesis by (simp add: x Nge0_def INum_def) }
   1.369 +  ultimately show ?thesis by blast
   1.370 +qed
   1.371 +
   1.372 +lemma Nlt_iff[simp]:
   1.373 +  assumes nx: "isnormNum x" and ny: "isnormNum y"
   1.374 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)"
   1.375 +proof -
   1.376 +  let ?z = "0::'a"
   1.377 +  have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)"
   1.378 +    using nx ny by simp
   1.379 +  also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))"
   1.380 +    using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
   1.381 +  finally show ?thesis by (simp add: Nlt_def)
   1.382 +qed
   1.383 +
   1.384 +lemma Nle_iff[simp]:
   1.385 +  assumes nx: "isnormNum x" and ny: "isnormNum y"
   1.386 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\<le> INum y) = (x \<le>\<^sub>N y)"
   1.387 +proof -
   1.388 +  have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))"
   1.389 +    using nx ny by simp
   1.390 +  also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))"
   1.391 +    using Nle0_iff[OF Nsub_normN[OF ny]] by simp
   1.392 +  finally show ?thesis by (simp add: Nle_def)
   1.393 +qed
   1.394 +
   1.395 +lemma Nadd_commute:
   1.396 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.397 +  shows "x +\<^sub>N y = y +\<^sub>N x"
   1.398 +proof -
   1.399 +  have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
   1.400 +  have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp
   1.401 +  with isnormNum_unique[OF n] show ?thesis by simp
   1.402 +qed
   1.403 +
   1.404 +lemma [simp]:
   1.405 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.406 +  shows "(0, b) +\<^sub>N y = normNum y"
   1.407 +    and "(a, 0) +\<^sub>N y = normNum y"
   1.408 +    and "x +\<^sub>N (0, b) = normNum x"
   1.409 +    and "x +\<^sub>N (a, 0) = normNum x"
   1.410 +  apply (simp add: Nadd_def split_def)
   1.411 +  apply (simp add: Nadd_def split_def)
   1.412 +  apply (subst Nadd_commute, simp add: Nadd_def split_def)
   1.413 +  apply (subst Nadd_commute, simp add: Nadd_def split_def)
   1.414 +  done
   1.415 +
   1.416 +lemma normNum_nilpotent_aux[simp]:
   1.417 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.418 +  assumes nx: "isnormNum x"
   1.419 +  shows "normNum x = x"
   1.420 +proof -
   1.421 +  let ?a = "normNum x"
   1.422 +  have n: "isnormNum ?a" by simp
   1.423 +  have th: "INum ?a = (INum x ::'a)" by simp
   1.424 +  with isnormNum_unique[OF n nx] show ?thesis by simp
   1.425 +qed
   1.426 +
   1.427 +lemma normNum_nilpotent[simp]:
   1.428 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.429 +  shows "normNum (normNum x) = normNum x"
   1.430 +  by simp
   1.431 +
   1.432 +lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N"
   1.433 +  by (simp_all add: normNum_def)
   1.434 +
   1.435 +lemma normNum_Nadd:
   1.436 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.437 +  shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
   1.438 +
   1.439 +lemma Nadd_normNum1[simp]:
   1.440 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.441 +  shows "normNum x +\<^sub>N y = x +\<^sub>N y"
   1.442 +proof -
   1.443 +  have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
   1.444 +  have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp
   1.445 +  also have "\<dots> = INum (x +\<^sub>N y)" by simp
   1.446 +  finally show ?thesis using isnormNum_unique[OF n] by simp
   1.447 +qed
   1.448 +
   1.449 +lemma Nadd_normNum2[simp]:
   1.450 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.451 +  shows "x +\<^sub>N normNum y = x +\<^sub>N y"
   1.452 +proof -
   1.453 +  have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
   1.454 +  have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp
   1.455 +  also have "\<dots> = INum (x +\<^sub>N y)" by simp
   1.456 +  finally show ?thesis using isnormNum_unique[OF n] by simp
   1.457 +qed
   1.458 +
   1.459 +lemma Nadd_assoc:
   1.460 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.461 +  shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
   1.462 +proof -
   1.463 +  have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
   1.464 +  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
   1.465 +  with isnormNum_unique[OF n] show ?thesis by simp
   1.466 +qed
   1.467 +
   1.468 +lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
   1.469 +  by (simp add: Nmul_def split_def Let_def gcd_commute_int mult_commute)
   1.470 +
   1.471 +lemma Nmul_assoc:
   1.472 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.473 +  assumes nx: "isnormNum x" and ny: "isnormNum y" and nz: "isnormNum z"
   1.474 +  shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
   1.475 +proof -
   1.476 +  from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))"
   1.477 +    by simp_all
   1.478 +  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
   1.479 +  with isnormNum_unique[OF n] show ?thesis by simp
   1.480 +qed
   1.481 +
   1.482 +lemma Nsub0:
   1.483 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.484 +  assumes x: "isnormNum x" and y: "isnormNum y"
   1.485 +  shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y"
   1.486 +proof -
   1.487 +  fix h :: 'a
   1.488 +  from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"]
   1.489 +  have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp
   1.490 +  also have "\<dots> = (INum x = (INum y :: 'a))" by simp
   1.491 +  also have "\<dots> = (x = y)" using x y by simp
   1.492 +  finally show ?thesis .
   1.493 +qed
   1.494 +
   1.495 +lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N"
   1.496 +  by (simp_all add: Nmul_def Let_def split_def)
   1.497 +
   1.498 +lemma Nmul_eq0[simp]:
   1.499 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.500 +  assumes nx: "isnormNum x" and ny: "isnormNum y"
   1.501 +  shows "x*\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = 0\<^sub>N \<or> y = 0\<^sub>N"
   1.502 +proof -
   1.503 +  fix h :: 'a
   1.504 +  obtain a b where x: "x = (a, b)" by (cases x)
   1.505 +  obtain a' b' where y: "y = (a', b')" by (cases y)
   1.506 +  have n0: "isnormNum 0\<^sub>N" by simp
   1.507 +  show ?thesis using nx ny
   1.508 +    apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric]
   1.509 +      Nmul[where ?'a = 'a])
   1.510 +    apply (simp add: x y INum_def split_def isnormNum_def split: split_if_asm)
   1.511 +    done
   1.512 +qed
   1.513 +
   1.514 +lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
   1.515 +  by (simp add: Nneg_def split_def)
   1.516 +
   1.517 +lemma Nmul1[simp]:
   1.518 +    "isnormNum c \<Longrightarrow> (1)\<^sub>N *\<^sub>N c = c"
   1.519 +    "isnormNum c \<Longrightarrow> c *\<^sub>N (1)\<^sub>N = c"
   1.520 +  apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
   1.521 +  apply (cases "fst c = 0", simp_all, cases c, simp_all)+
   1.522 +  done
   1.523 +
   1.524 +end
     2.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Oct 31 11:44:20 2013 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Oct 31 11:44:20 2013 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Implementation and verification of multivariate polynomials *}
     2.5  
     2.6  theory Reflected_Multivariate_Polynomial
     2.7 -imports Complex_Main "~~/src/HOL/Library/Abstract_Rat" Polynomial_List
     2.8 +imports Complex_Main Rat_Pair Polynomial_List
     2.9  begin
    2.10  
    2.11  subsection{* Datatype of polynomial expressions *}
     3.1 --- a/src/HOL/Library/Abstract_Rat.thy	Thu Oct 31 11:44:20 2013 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,521 +0,0 @@
     3.4 -(*  Title:      HOL/Library/Abstract_Rat.thy
     3.5 -    Author:     Amine Chaieb
     3.6 -*)
     3.7 -
     3.8 -header {* Abstract rational numbers *}
     3.9 -
    3.10 -theory Abstract_Rat
    3.11 -imports Complex_Main
    3.12 -begin
    3.13 -
    3.14 -type_synonym Num = "int \<times> int"
    3.15 -
    3.16 -abbreviation Num0_syn :: Num  ("0\<^sub>N")
    3.17 -  where "0\<^sub>N \<equiv> (0, 0)"
    3.18 -
    3.19 -abbreviation Numi_syn :: "int \<Rightarrow> Num"  ("'((_)')\<^sub>N")
    3.20 -  where "(i)\<^sub>N \<equiv> (i, 1)"
    3.21 -
    3.22 -definition isnormNum :: "Num \<Rightarrow> bool" where
    3.23 -  "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> gcd a b = 1))"
    3.24 -
    3.25 -definition normNum :: "Num \<Rightarrow> Num" where
    3.26 -  "normNum = (\<lambda>(a,b).
    3.27 -    (if a=0 \<or> b = 0 then (0,0) else
    3.28 -      (let g = gcd a b
    3.29 -       in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
    3.30 -
    3.31 -declare gcd_dvd1_int[presburger] gcd_dvd2_int[presburger]
    3.32 -
    3.33 -lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
    3.34 -proof -
    3.35 -  obtain a b where x: "x = (a, b)" by (cases x)
    3.36 -  { assume "a=0 \<or> b = 0" hence ?thesis by (simp add: x normNum_def isnormNum_def) }
    3.37 -  moreover
    3.38 -  { assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0"
    3.39 -    let ?g = "gcd a b"
    3.40 -    let ?a' = "a div ?g"
    3.41 -    let ?b' = "b div ?g"
    3.42 -    let ?g' = "gcd ?a' ?b'"
    3.43 -    from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b]
    3.44 -    have gpos: "?g > 0" by arith
    3.45 -    have gdvd: "?g dvd a" "?g dvd b" by arith+
    3.46 -    from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] anz bnz
    3.47 -    have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
    3.48 -    from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
    3.49 -    from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
    3.50 -    from bnz have "b < 0 \<or> b > 0" by arith
    3.51 -    moreover
    3.52 -    { assume b: "b > 0"
    3.53 -      from b have "?b' \<ge> 0"
    3.54 -        by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])
    3.55 -      with nz' have b': "?b' > 0" by arith
    3.56 -      from b b' anz bnz nz' gp1 have ?thesis
    3.57 -        by (simp add: x isnormNum_def normNum_def Let_def split_def) }
    3.58 -    moreover {
    3.59 -      assume b: "b < 0"
    3.60 -      { assume b': "?b' \<ge> 0"
    3.61 -        from gpos have th: "?g \<ge> 0" by arith
    3.62 -        from mult_nonneg_nonneg[OF th b'] dvd_mult_div_cancel[OF gdvd(2)]
    3.63 -        have False using b by arith }
    3.64 -      hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
    3.65 -      from anz bnz nz' b b' gp1 have ?thesis
    3.66 -        by (simp add: x isnormNum_def normNum_def Let_def split_def) }
    3.67 -    ultimately have ?thesis by blast
    3.68 -  }
    3.69 -  ultimately show ?thesis by blast
    3.70 -qed
    3.71 -
    3.72 -text {* Arithmetic over Num *}
    3.73 -
    3.74 -definition Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "+\<^sub>N" 60) where
    3.75 -  "Nadd = (\<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b')
    3.76 -    else if a'=0 \<or> b' = 0 then normNum(a,b)
    3.77 -    else normNum(a*b' + b*a', b*b'))"
    3.78 -
    3.79 -definition Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "*\<^sub>N" 60) where
    3.80 -  "Nmul = (\<lambda>(a,b) (a',b'). let g = gcd (a*a') (b*b')
    3.81 -    in (a*a' div g, b*b' div g))"
    3.82 -
    3.83 -definition Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N")
    3.84 -  where "Nneg \<equiv> (\<lambda>(a,b). (-a,b))"
    3.85 -
    3.86 -definition Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "-\<^sub>N" 60)
    3.87 -  where "Nsub = (\<lambda>a b. a +\<^sub>N ~\<^sub>N b)"
    3.88 -
    3.89 -definition Ninv :: "Num \<Rightarrow> Num"
    3.90 -  where "Ninv = (\<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a))"
    3.91 -
    3.92 -definition Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "\<div>\<^sub>N" 60)
    3.93 -  where "Ndiv = (\<lambda>a b. a *\<^sub>N Ninv b)"
    3.94 -
    3.95 -lemma Nneg_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (~\<^sub>N x)"
    3.96 -  by (simp add: isnormNum_def Nneg_def split_def)
    3.97 -
    3.98 -lemma Nadd_normN[simp]: "isnormNum (x +\<^sub>N y)"
    3.99 -  by (simp add: Nadd_def split_def)
   3.100 -
   3.101 -lemma Nsub_normN[simp]: "\<lbrakk> isnormNum y\<rbrakk> \<Longrightarrow> isnormNum (x -\<^sub>N y)"
   3.102 -  by (simp add: Nsub_def split_def)
   3.103 -
   3.104 -lemma Nmul_normN[simp]:
   3.105 -  assumes xn: "isnormNum x" and yn: "isnormNum y"
   3.106 -  shows "isnormNum (x *\<^sub>N y)"
   3.107 -proof -
   3.108 -  obtain a b where x: "x = (a, b)" by (cases x)
   3.109 -  obtain a' b' where y: "y = (a', b')" by (cases y)
   3.110 -  { assume "a = 0"
   3.111 -    hence ?thesis using xn x y
   3.112 -      by (simp add: isnormNum_def Let_def Nmul_def split_def) }
   3.113 -  moreover
   3.114 -  { assume "a' = 0"
   3.115 -    hence ?thesis using yn x y
   3.116 -      by (simp add: isnormNum_def Let_def Nmul_def split_def) }
   3.117 -  moreover
   3.118 -  { assume a: "a \<noteq>0" and a': "a'\<noteq>0"
   3.119 -    hence bp: "b > 0" "b' > 0" using xn yn x y by (simp_all add: isnormNum_def)
   3.120 -    from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a * a', b * b')"
   3.121 -      using x y a a' bp by (simp add: Nmul_def Let_def split_def normNum_def)
   3.122 -    hence ?thesis by simp }
   3.123 -  ultimately show ?thesis by blast
   3.124 -qed
   3.125 -
   3.126 -lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
   3.127 -  by (simp add: Ninv_def isnormNum_def split_def)
   3.128 -    (cases "fst x = 0", auto simp add: gcd_commute_int)
   3.129 -
   3.130 -lemma isnormNum_int[simp]:
   3.131 -  "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i)\<^sub>N"
   3.132 -  by (simp_all add: isnormNum_def)
   3.133 -
   3.134 -
   3.135 -text {* Relations over Num *}
   3.136 -
   3.137 -definition Nlt0:: "Num \<Rightarrow> bool"  ("0>\<^sub>N")
   3.138 -  where "Nlt0 = (\<lambda>(a,b). a < 0)"
   3.139 -
   3.140 -definition Nle0:: "Num \<Rightarrow> bool"  ("0\<ge>\<^sub>N")
   3.141 -  where "Nle0 = (\<lambda>(a,b). a \<le> 0)"
   3.142 -
   3.143 -definition Ngt0:: "Num \<Rightarrow> bool"  ("0<\<^sub>N")
   3.144 -  where "Ngt0 = (\<lambda>(a,b). a > 0)"
   3.145 -
   3.146 -definition Nge0:: "Num \<Rightarrow> bool"  ("0\<le>\<^sub>N")
   3.147 -  where "Nge0 = (\<lambda>(a,b). a \<ge> 0)"
   3.148 -
   3.149 -definition Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool"  (infix "<\<^sub>N" 55)
   3.150 -  where "Nlt = (\<lambda>a b. 0>\<^sub>N (a -\<^sub>N b))"
   3.151 -
   3.152 -definition Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool"  (infix "\<le>\<^sub>N" 55)
   3.153 -  where "Nle = (\<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b))"
   3.154 -
   3.155 -definition "INum = (\<lambda>(a,b). of_int a / of_int b)"
   3.156 -
   3.157 -lemma INum_int [simp]: "INum (i)\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
   3.158 -  by (simp_all add: INum_def)
   3.159 -
   3.160 -lemma isnormNum_unique[simp]:
   3.161 -  assumes na: "isnormNum x" and nb: "isnormNum y"
   3.162 -  shows "((INum x ::'a::{field_char_0, field_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
   3.163 -proof
   3.164 -  obtain a b where x: "x = (a, b)" by (cases x)
   3.165 -  obtain a' b' where y: "y = (a', b')" by (cases y)
   3.166 -  assume H: ?lhs
   3.167 -  { assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0"
   3.168 -    hence ?rhs using na nb H
   3.169 -      by (simp add: x y INum_def split_def isnormNum_def split: split_if_asm) }
   3.170 -  moreover
   3.171 -  { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
   3.172 -    from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: x y isnormNum_def)
   3.173 -    from H bz b'z have eq: "a * b' = a'*b"
   3.174 -      by (simp add: x y INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
   3.175 -    from az a'z na nb have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
   3.176 -      by (simp_all add: x y isnormNum_def add: gcd_commute_int)
   3.177 -    from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
   3.178 -      apply -
   3.179 -      apply algebra
   3.180 -      apply algebra
   3.181 -      apply simp
   3.182 -      apply algebra
   3.183 -      done
   3.184 -    from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
   3.185 -        coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
   3.186 -      have eq1: "b = b'" using pos by arith
   3.187 -      with eq have "a = a'" using pos by simp
   3.188 -      with eq1 have ?rhs by (simp add: x y) }
   3.189 -  ultimately show ?rhs by blast
   3.190 -next
   3.191 -  assume ?rhs thus ?lhs by simp
   3.192 -qed
   3.193 -
   3.194 -
   3.195 -lemma isnormNum0[simp]:
   3.196 -    "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
   3.197 -  unfolding INum_int(2)[symmetric]
   3.198 -  by (rule isnormNum_unique) simp_all
   3.199 -
   3.200 -lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) =
   3.201 -    of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)"
   3.202 -proof -
   3.203 -  assume "d ~= 0"
   3.204 -  let ?t = "of_int (x div d) * ((of_int d)::'a) + of_int(x mod d)"
   3.205 -  let ?f = "\<lambda>x. x / of_int d"
   3.206 -  have "x = (x div d) * d + x mod d"
   3.207 -    by auto
   3.208 -  then have eq: "of_int x = ?t"
   3.209 -    by (simp only: of_int_mult[symmetric] of_int_add [symmetric])
   3.210 -  then have "of_int x / of_int d = ?t / of_int d"
   3.211 -    using cong[OF refl[of ?f] eq] by simp
   3.212 -  then show ?thesis by (simp add: add_divide_distrib algebra_simps `d ~= 0`)
   3.213 -qed
   3.214 -
   3.215 -lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
   3.216 -    (of_int(n div d)::'a::field_char_0) = of_int n / of_int d"
   3.217 -  apply (frule of_int_div_aux [of d n, where ?'a = 'a])
   3.218 -  apply simp
   3.219 -  apply (simp add: dvd_eq_mod_eq_0)
   3.220 -  done
   3.221 -
   3.222 -
   3.223 -lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
   3.224 -proof -
   3.225 -  obtain a b where x: "x = (a, b)" by (cases x)
   3.226 -  { assume "a = 0 \<or> b = 0"
   3.227 -    hence ?thesis by (simp add: x INum_def normNum_def split_def Let_def) }
   3.228 -  moreover
   3.229 -  { assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
   3.230 -    let ?g = "gcd a b"
   3.231 -    from a b have g: "?g \<noteq> 0"by simp
   3.232 -    from of_int_div[OF g, where ?'a = 'a]
   3.233 -    have ?thesis by (auto simp add: x INum_def normNum_def split_def Let_def) }
   3.234 -  ultimately show ?thesis by blast
   3.235 -qed
   3.236 -
   3.237 -lemma INum_normNum_iff:
   3.238 -  "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y"
   3.239 -  (is "?lhs = ?rhs")
   3.240 -proof -
   3.241 -  have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
   3.242 -    by (simp del: normNum)
   3.243 -  also have "\<dots> = ?lhs" by simp
   3.244 -  finally show ?thesis by simp
   3.245 -qed
   3.246 -
   3.247 -lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})"
   3.248 -proof -
   3.249 -  let ?z = "0:: 'a"
   3.250 -  obtain a b where x: "x = (a, b)" by (cases x)
   3.251 -  obtain a' b' where y: "y = (a', b')" by (cases y)
   3.252 -  { assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0"
   3.253 -    hence ?thesis
   3.254 -      apply (cases "a=0", simp_all add: x y Nadd_def)
   3.255 -      apply (cases "b= 0", simp_all add: INum_def)
   3.256 -       apply (cases "a'= 0", simp_all)
   3.257 -       apply (cases "b'= 0", simp_all)
   3.258 -       done }
   3.259 -  moreover
   3.260 -  { assume aa': "a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0"
   3.261 -    { assume z: "a * b' + b * a' = 0"
   3.262 -      hence "of_int (a*b' + b*a') / (of_int b* of_int b') = ?z" by simp
   3.263 -      hence "of_int b' * of_int a / (of_int b * of_int b') +
   3.264 -          of_int b * of_int a' / (of_int b * of_int b') = ?z"
   3.265 -        by (simp add:add_divide_distrib)
   3.266 -      hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa'
   3.267 -        by simp
   3.268 -      from z aa' bb' have ?thesis
   3.269 -        by (simp add: x y th Nadd_def normNum_def INum_def split_def) }
   3.270 -    moreover {
   3.271 -      assume z: "a * b' + b * a' \<noteq> 0"
   3.272 -      let ?g = "gcd (a * b' + b * a') (b*b')"
   3.273 -      have gz: "?g \<noteq> 0" using z by simp
   3.274 -      have ?thesis using aa' bb' z gz
   3.275 -        of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]
   3.276 -        of_int_div[where ?'a = 'a, OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
   3.277 -        by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib) }
   3.278 -    ultimately have ?thesis using aa' bb'
   3.279 -      by (simp add: x y Nadd_def INum_def normNum_def Let_def) }
   3.280 -  ultimately show ?thesis by blast
   3.281 -qed
   3.282 -
   3.283 -lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero})"
   3.284 -proof -
   3.285 -  let ?z = "0::'a"
   3.286 -  obtain a b where x: "x = (a, b)" by (cases x)
   3.287 -  obtain a' b' where y: "y = (a', b')" by (cases y)
   3.288 -  { assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0"
   3.289 -    hence ?thesis
   3.290 -      apply (cases "a=0", simp_all add: x y Nmul_def INum_def Let_def)
   3.291 -      apply (cases "b=0", simp_all)
   3.292 -      apply (cases "a'=0", simp_all)
   3.293 -      done }
   3.294 -  moreover
   3.295 -  { assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
   3.296 -    let ?g="gcd (a*a') (b*b')"
   3.297 -    have gz: "?g \<noteq> 0" using z by simp
   3.298 -    from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]]
   3.299 -      of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]]
   3.300 -    have ?thesis by (simp add: Nmul_def x y Let_def INum_def) }
   3.301 -  ultimately show ?thesis by blast
   3.302 -qed
   3.303 -
   3.304 -lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
   3.305 -  by (simp add: Nneg_def split_def INum_def)
   3.306 -
   3.307 -lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
   3.308 -  by (simp add: Nsub_def split_def)
   3.309 -
   3.310 -lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)"
   3.311 -  by (simp add: Ninv_def INum_def split_def)
   3.312 -
   3.313 -lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})"
   3.314 -  by (simp add: Ndiv_def)
   3.315 -
   3.316 -lemma Nlt0_iff[simp]:
   3.317 -  assumes nx: "isnormNum x"
   3.318 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x"
   3.319 -proof -
   3.320 -  obtain a b where x: "x = (a, b)" by (cases x)
   3.321 -  { assume "a = 0" hence ?thesis by (simp add: x Nlt0_def INum_def) }
   3.322 -  moreover
   3.323 -  { assume a: "a \<noteq> 0" hence b: "(of_int b::'a) > 0"
   3.324 -      using nx by (simp add: x isnormNum_def)
   3.325 -    from pos_divide_less_eq[OF b, where b="of_int a" and a="0::'a"]
   3.326 -    have ?thesis by (simp add: x Nlt0_def INum_def) }
   3.327 -  ultimately show ?thesis by blast
   3.328 -qed
   3.329 -
   3.330 -lemma Nle0_iff[simp]:
   3.331 -  assumes nx: "isnormNum x"
   3.332 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<le> 0) = 0\<ge>\<^sub>N x"
   3.333 -proof -
   3.334 -  obtain a b where x: "x = (a, b)" by (cases x)
   3.335 -  { assume "a = 0" hence ?thesis by (simp add: x Nle0_def INum_def) }
   3.336 -  moreover
   3.337 -  { assume a: "a \<noteq> 0" hence b: "(of_int b :: 'a) > 0"
   3.338 -      using nx by (simp add: x isnormNum_def)
   3.339 -    from pos_divide_le_eq[OF b, where b="of_int a" and a="0::'a"]
   3.340 -    have ?thesis by (simp add: x Nle0_def INum_def) }
   3.341 -  ultimately show ?thesis by blast
   3.342 -qed
   3.343 -
   3.344 -lemma Ngt0_iff[simp]:
   3.345 -  assumes nx: "isnormNum x"
   3.346 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
   3.347 -proof -
   3.348 -  obtain a b where x: "x = (a, b)" by (cases x)
   3.349 -  { assume "a = 0" hence ?thesis by (simp add: x Ngt0_def INum_def) }
   3.350 -  moreover
   3.351 -  { assume a: "a \<noteq> 0" hence b: "(of_int b::'a) > 0" using nx
   3.352 -      by (simp add: x isnormNum_def)
   3.353 -    from pos_less_divide_eq[OF b, where b="of_int a" and a="0::'a"]
   3.354 -    have ?thesis by (simp add: x Ngt0_def INum_def) }
   3.355 -  ultimately show ?thesis by blast
   3.356 -qed
   3.357 -
   3.358 -lemma Nge0_iff[simp]:
   3.359 -  assumes nx: "isnormNum x"
   3.360 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
   3.361 -proof -
   3.362 -  obtain a b where x: "x = (a, b)" by (cases x)
   3.363 -  { assume "a = 0" hence ?thesis by (simp add: x Nge0_def INum_def) }
   3.364 -  moreover
   3.365 -  { assume "a \<noteq> 0" hence b: "(of_int b::'a) > 0" using nx
   3.366 -      by (simp add: x isnormNum_def)
   3.367 -    from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"]
   3.368 -    have ?thesis by (simp add: x Nge0_def INum_def) }
   3.369 -  ultimately show ?thesis by blast
   3.370 -qed
   3.371 -
   3.372 -lemma Nlt_iff[simp]:
   3.373 -  assumes nx: "isnormNum x" and ny: "isnormNum y"
   3.374 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)"
   3.375 -proof -
   3.376 -  let ?z = "0::'a"
   3.377 -  have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)"
   3.378 -    using nx ny by simp
   3.379 -  also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))"
   3.380 -    using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
   3.381 -  finally show ?thesis by (simp add: Nlt_def)
   3.382 -qed
   3.383 -
   3.384 -lemma Nle_iff[simp]:
   3.385 -  assumes nx: "isnormNum x" and ny: "isnormNum y"
   3.386 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\<le> INum y) = (x \<le>\<^sub>N y)"
   3.387 -proof -
   3.388 -  have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))"
   3.389 -    using nx ny by simp
   3.390 -  also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))"
   3.391 -    using Nle0_iff[OF Nsub_normN[OF ny]] by simp
   3.392 -  finally show ?thesis by (simp add: Nle_def)
   3.393 -qed
   3.394 -
   3.395 -lemma Nadd_commute:
   3.396 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.397 -  shows "x +\<^sub>N y = y +\<^sub>N x"
   3.398 -proof -
   3.399 -  have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
   3.400 -  have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp
   3.401 -  with isnormNum_unique[OF n] show ?thesis by simp
   3.402 -qed
   3.403 -
   3.404 -lemma [simp]:
   3.405 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.406 -  shows "(0, b) +\<^sub>N y = normNum y"
   3.407 -    and "(a, 0) +\<^sub>N y = normNum y"
   3.408 -    and "x +\<^sub>N (0, b) = normNum x"
   3.409 -    and "x +\<^sub>N (a, 0) = normNum x"
   3.410 -  apply (simp add: Nadd_def split_def)
   3.411 -  apply (simp add: Nadd_def split_def)
   3.412 -  apply (subst Nadd_commute, simp add: Nadd_def split_def)
   3.413 -  apply (subst Nadd_commute, simp add: Nadd_def split_def)
   3.414 -  done
   3.415 -
   3.416 -lemma normNum_nilpotent_aux[simp]:
   3.417 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.418 -  assumes nx: "isnormNum x"
   3.419 -  shows "normNum x = x"
   3.420 -proof -
   3.421 -  let ?a = "normNum x"
   3.422 -  have n: "isnormNum ?a" by simp
   3.423 -  have th: "INum ?a = (INum x ::'a)" by simp
   3.424 -  with isnormNum_unique[OF n nx] show ?thesis by simp
   3.425 -qed
   3.426 -
   3.427 -lemma normNum_nilpotent[simp]:
   3.428 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.429 -  shows "normNum (normNum x) = normNum x"
   3.430 -  by simp
   3.431 -
   3.432 -lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N"
   3.433 -  by (simp_all add: normNum_def)
   3.434 -
   3.435 -lemma normNum_Nadd:
   3.436 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.437 -  shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
   3.438 -
   3.439 -lemma Nadd_normNum1[simp]:
   3.440 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.441 -  shows "normNum x +\<^sub>N y = x +\<^sub>N y"
   3.442 -proof -
   3.443 -  have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
   3.444 -  have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp
   3.445 -  also have "\<dots> = INum (x +\<^sub>N y)" by simp
   3.446 -  finally show ?thesis using isnormNum_unique[OF n] by simp
   3.447 -qed
   3.448 -
   3.449 -lemma Nadd_normNum2[simp]:
   3.450 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.451 -  shows "x +\<^sub>N normNum y = x +\<^sub>N y"
   3.452 -proof -
   3.453 -  have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
   3.454 -  have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp
   3.455 -  also have "\<dots> = INum (x +\<^sub>N y)" by simp
   3.456 -  finally show ?thesis using isnormNum_unique[OF n] by simp
   3.457 -qed
   3.458 -
   3.459 -lemma Nadd_assoc:
   3.460 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.461 -  shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
   3.462 -proof -
   3.463 -  have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
   3.464 -  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
   3.465 -  with isnormNum_unique[OF n] show ?thesis by simp
   3.466 -qed
   3.467 -
   3.468 -lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
   3.469 -  by (simp add: Nmul_def split_def Let_def gcd_commute_int mult_commute)
   3.470 -
   3.471 -lemma Nmul_assoc:
   3.472 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.473 -  assumes nx: "isnormNum x" and ny: "isnormNum y" and nz: "isnormNum z"
   3.474 -  shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
   3.475 -proof -
   3.476 -  from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))"
   3.477 -    by simp_all
   3.478 -  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
   3.479 -  with isnormNum_unique[OF n] show ?thesis by simp
   3.480 -qed
   3.481 -
   3.482 -lemma Nsub0:
   3.483 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.484 -  assumes x: "isnormNum x" and y: "isnormNum y"
   3.485 -  shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y"
   3.486 -proof -
   3.487 -  fix h :: 'a
   3.488 -  from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"]
   3.489 -  have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp
   3.490 -  also have "\<dots> = (INum x = (INum y :: 'a))" by simp
   3.491 -  also have "\<dots> = (x = y)" using x y by simp
   3.492 -  finally show ?thesis .
   3.493 -qed
   3.494 -
   3.495 -lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N"
   3.496 -  by (simp_all add: Nmul_def Let_def split_def)
   3.497 -
   3.498 -lemma Nmul_eq0[simp]:
   3.499 -  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   3.500 -  assumes nx: "isnormNum x" and ny: "isnormNum y"
   3.501 -  shows "x*\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = 0\<^sub>N \<or> y = 0\<^sub>N"
   3.502 -proof -
   3.503 -  fix h :: 'a
   3.504 -  obtain a b where x: "x = (a, b)" by (cases x)
   3.505 -  obtain a' b' where y: "y = (a', b')" by (cases y)
   3.506 -  have n0: "isnormNum 0\<^sub>N" by simp
   3.507 -  show ?thesis using nx ny
   3.508 -    apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric]
   3.509 -      Nmul[where ?'a = 'a])
   3.510 -    apply (simp add: x y INum_def split_def isnormNum_def split: split_if_asm)
   3.511 -    done
   3.512 -qed
   3.513 -
   3.514 -lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
   3.515 -  by (simp add: Nneg_def split_def)
   3.516 -
   3.517 -lemma Nmul1[simp]:
   3.518 -    "isnormNum c \<Longrightarrow> (1)\<^sub>N *\<^sub>N c = c"
   3.519 -    "isnormNum c \<Longrightarrow> c *\<^sub>N (1)\<^sub>N = c"
   3.520 -  apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
   3.521 -  apply (cases "fst c = 0", simp_all, cases c, simp_all)+
   3.522 -  done
   3.523 -
   3.524 -end
     4.1 --- a/src/HOL/Library/Library.thy	Thu Oct 31 11:44:20 2013 +0100
     4.2 +++ b/src/HOL/Library/Library.thy	Thu Oct 31 11:44:20 2013 +0100
     4.3 @@ -1,7 +1,6 @@
     4.4  (*<*)
     4.5  theory Library
     4.6  imports
     4.7 -  Abstract_Rat
     4.8    AList
     4.9    BigO
    4.10    Binomial