src/HOL/Library/Abstract_Rat.thy
changeset 44779 98d597c4193d
parent 42463 f270e3e18be5
child 44780 a13cdb1e9e08
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Wed Sep 07 11:36:39 2011 +0200
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Wed Sep 07 16:37:50 2011 +0200
     1.3 @@ -10,64 +10,58 @@
     1.4  
     1.5  type_synonym Num = "int \<times> int"
     1.6  
     1.7 -abbreviation
     1.8 -  Num0_syn :: Num ("0\<^sub>N")
     1.9 -where "0\<^sub>N \<equiv> (0, 0)"
    1.10 +abbreviation Num0_syn :: Num ("0\<^sub>N")
    1.11 +  where "0\<^sub>N \<equiv> (0, 0)"
    1.12  
    1.13 -abbreviation
    1.14 -  Numi_syn :: "int \<Rightarrow> Num" ("_\<^sub>N")
    1.15 -where "i\<^sub>N \<equiv> (i, 1)"
    1.16 +abbreviation Numi_syn :: "int \<Rightarrow> Num" ("_\<^sub>N")
    1.17 +  where "i\<^sub>N \<equiv> (i, 1)"
    1.18  
    1.19 -definition
    1.20 -  isnormNum :: "Num \<Rightarrow> bool"
    1.21 -where
    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
    1.26 -  normNum :: "Num \<Rightarrow> Num"
    1.27 -where
    1.28 -  "normNum = (\<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else 
    1.29 -  (let g = gcd a b 
    1.30 -   in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
    1.31 +definition normNum :: "Num \<Rightarrow> Num" where
    1.32 +  "normNum = (\<lambda>(a,b).
    1.33 +    (if a=0 \<or> b = 0 then (0,0) else
    1.34 +      (let g = gcd a b 
    1.35 +       in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
    1.36  
    1.37 -declare gcd_dvd1_int[presburger]
    1.38 -declare gcd_dvd2_int[presburger]
    1.39 +declare gcd_dvd1_int[presburger] gcd_dvd2_int[presburger]
    1.40 +
    1.41  lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
    1.42  proof -
    1.43    have " \<exists> a b. x = (a,b)" by auto
    1.44    then obtain a b where x[simp]: "x = (a,b)" by blast
    1.45 -  {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}  
    1.46 +  { assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def) }
    1.47    moreover
    1.48 -  {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0" 
    1.49 +  { assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0"
    1.50      let ?g = "gcd a b"
    1.51      let ?a' = "a div ?g"
    1.52      let ?b' = "b div ?g"
    1.53      let ?g' = "gcd ?a' ?b'"
    1.54 -    from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b] 
    1.55 +    from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b]
    1.56      have gpos: "?g > 0" by arith
    1.57 -    have gdvd: "?g dvd a" "?g dvd b" by arith+ 
    1.58 -    from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
    1.59 -    anz bnz
    1.60 -    have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
    1.61 -      by - (rule notI, simp)+
    1.62 -    from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith 
    1.63 +    have gdvd: "?g dvd a" "?g dvd b" by arith+
    1.64 +    from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)] anz bnz
    1.65 +    have nz':"?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
    1.66 +    from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
    1.67      from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
    1.68      from bnz have "b < 0 \<or> b > 0" by arith
    1.69      moreover
    1.70 -    {assume b: "b > 0"
    1.71 -      from b have "?b' \<ge> 0" 
    1.72 -        by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])  
    1.73 +    { assume b: "b > 0"
    1.74 +      from b have "?b' \<ge> 0"
    1.75 +        by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])
    1.76        with nz' have b': "?b' > 0" by arith 
    1.77        from b b' anz bnz nz' gp1 have ?thesis 
    1.78 -        by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    1.79 -    moreover {assume b: "b < 0"
    1.80 -      {assume b': "?b' \<ge> 0" 
    1.81 +        by (simp add: isnormNum_def normNum_def Let_def split_def)}
    1.82 +    moreover {
    1.83 +      assume b: "b < 0"
    1.84 +      { assume b': "?b' \<ge> 0" 
    1.85          from gpos have th: "?g \<ge> 0" by arith
    1.86          from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
    1.87          have False using b by arith }
    1.88 -      hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric]) 
    1.89 +      hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
    1.90        from anz bnz nz' b b' gp1 have ?thesis 
    1.91 -        by (simp add: isnormNum_def normNum_def Let_def split_def)}
    1.92 +        by (simp add: isnormNum_def normNum_def Let_def split_def) }
    1.93      ultimately have ?thesis by blast
    1.94    }
    1.95    ultimately show ?thesis by blast
    1.96 @@ -75,50 +69,42 @@
    1.97  
    1.98  text {* Arithmetic over Num *}
    1.99  
   1.100 -definition
   1.101 -  Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "+\<^sub>N" 60)
   1.102 -where
   1.103 -  "Nadd = (\<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b') 
   1.104 +definition Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "+\<^sub>N" 60) where
   1.105 +  "Nadd = (\<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b')
   1.106      else if a'=0 \<or> b' = 0 then normNum(a,b) 
   1.107      else normNum(a*b' + b*a', b*b'))"
   1.108  
   1.109 -definition
   1.110 -  Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
   1.111 -where
   1.112 +definition Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60) where
   1.113    "Nmul = (\<lambda>(a,b) (a',b'). let g = gcd (a*a') (b*b') 
   1.114      in (a*a' div g, b*b' div g))"
   1.115  
   1.116 -definition
   1.117 -  Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N")
   1.118 -where
   1.119 -  "Nneg \<equiv> (\<lambda>(a,b). (-a,b))"
   1.120 +definition Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N")
   1.121 +  where "Nneg \<equiv> (\<lambda>(a,b). (-a,b))"
   1.122  
   1.123 -definition
   1.124 -  Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "-\<^sub>N" 60)
   1.125 -where
   1.126 -  "Nsub = (\<lambda>a b. a +\<^sub>N ~\<^sub>N b)"
   1.127 +definition Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "-\<^sub>N" 60)
   1.128 +  where "Nsub = (\<lambda>a b. a +\<^sub>N ~\<^sub>N b)"
   1.129  
   1.130 -definition
   1.131 -  Ninv :: "Num \<Rightarrow> Num" 
   1.132 -where
   1.133 -  "Ninv \<equiv> \<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a)"
   1.134 +definition Ninv :: "Num \<Rightarrow> Num"
   1.135 +  where "Ninv = (\<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a))"
   1.136  
   1.137 -definition
   1.138 -  Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "\<div>\<^sub>N" 60)
   1.139 -where
   1.140 -  "Ndiv \<equiv> \<lambda>a b. a *\<^sub>N Ninv b"
   1.141 +definition Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "\<div>\<^sub>N" 60)
   1.142 +  where "Ndiv = (\<lambda>a b. a *\<^sub>N Ninv b)"
   1.143  
   1.144  lemma Nneg_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (~\<^sub>N x)"
   1.145 -  by(simp add: isnormNum_def Nneg_def split_def)
   1.146 +  by (simp add: isnormNum_def Nneg_def split_def)
   1.147 +
   1.148  lemma Nadd_normN[simp]: "isnormNum (x +\<^sub>N y)"
   1.149    by (simp add: Nadd_def split_def)
   1.150 +
   1.151  lemma Nsub_normN[simp]: "\<lbrakk> isnormNum y\<rbrakk> \<Longrightarrow> isnormNum (x -\<^sub>N y)"
   1.152    by (simp add: Nsub_def split_def)
   1.153 -lemma Nmul_normN[simp]: assumes xn:"isnormNum x" and yn: "isnormNum y"
   1.154 +
   1.155 +lemma Nmul_normN[simp]:
   1.156 +  assumes xn:"isnormNum x" and yn: "isnormNum y"
   1.157    shows "isnormNum (x *\<^sub>N y)"
   1.158 -proof-
   1.159 +proof -
   1.160    have "\<exists>a b. x = (a,b)" and "\<exists> a' b'. y = (a',b')" by auto
   1.161 -  then obtain a b a' b' where ab: "x = (a,b)"  and ab': "y = (a',b')" by blast 
   1.162 +  then obtain a b a' b' where ab: "x = (a,b)"  and ab': "y = (a',b')" by blast
   1.163    {assume "a = 0"
   1.164      hence ?thesis using xn ab ab'
   1.165        by (simp add: isnormNum_def Let_def Nmul_def split_def)}
   1.166 @@ -146,38 +132,25 @@
   1.167  
   1.168  text {* Relations over Num *}
   1.169  
   1.170 -definition
   1.171 -  Nlt0:: "Num \<Rightarrow> bool" ("0>\<^sub>N")
   1.172 -where
   1.173 -  "Nlt0 = (\<lambda>(a,b). a < 0)"
   1.174 +definition Nlt0:: "Num \<Rightarrow> bool" ("0>\<^sub>N")
   1.175 +  where "Nlt0 = (\<lambda>(a,b). a < 0)"
   1.176  
   1.177 -definition
   1.178 -  Nle0:: "Num \<Rightarrow> bool" ("0\<ge>\<^sub>N")
   1.179 -where
   1.180 -  "Nle0 = (\<lambda>(a,b). a \<le> 0)"
   1.181 +definition Nle0:: "Num \<Rightarrow> bool" ("0\<ge>\<^sub>N")
   1.182 +  where "Nle0 = (\<lambda>(a,b). a \<le> 0)"
   1.183  
   1.184 -definition
   1.185 -  Ngt0:: "Num \<Rightarrow> bool" ("0<\<^sub>N")
   1.186 -where
   1.187 -  "Ngt0 = (\<lambda>(a,b). a > 0)"
   1.188 +definition Ngt0:: "Num \<Rightarrow> bool" ("0<\<^sub>N")
   1.189 +  where "Ngt0 = (\<lambda>(a,b). a > 0)"
   1.190  
   1.191 -definition
   1.192 -  Nge0:: "Num \<Rightarrow> bool" ("0\<le>\<^sub>N")
   1.193 -where
   1.194 -  "Nge0 = (\<lambda>(a,b). a \<ge> 0)"
   1.195 +definition Nge0:: "Num \<Rightarrow> bool" ("0\<le>\<^sub>N")
   1.196 +  where "Nge0 = (\<lambda>(a,b). a \<ge> 0)"
   1.197  
   1.198 -definition
   1.199 -  Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "<\<^sub>N" 55)
   1.200 -where
   1.201 -  "Nlt = (\<lambda>a b. 0>\<^sub>N (a -\<^sub>N b))"
   1.202 +definition Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "<\<^sub>N" 55)
   1.203 +  where "Nlt = (\<lambda>a b. 0>\<^sub>N (a -\<^sub>N b))"
   1.204  
   1.205 -definition
   1.206 -  Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "\<le>\<^sub>N" 55)
   1.207 -where
   1.208 -  "Nle = (\<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b))"
   1.209 +definition Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool"  (infix "\<le>\<^sub>N" 55)
   1.210 +  where "Nle = (\<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b))"
   1.211  
   1.212 -definition
   1.213 -  "INum = (\<lambda>(a,b). of_int a / of_int b)"
   1.214 +definition "INum = (\<lambda>(a,b). of_int a / of_int b)"
   1.215  
   1.216  lemma INum_int [simp]: "INum (i\<^sub>N) = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
   1.217    by (simp_all add: INum_def)
   1.218 @@ -189,9 +162,9 @@
   1.219    have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
   1.220    then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
   1.221    assume H: ?lhs 
   1.222 -  {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0"
   1.223 +  { assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0"
   1.224      hence ?rhs using na nb H
   1.225 -      by (simp add: INum_def split_def isnormNum_def split: split_if_asm)}
   1.226 +      by (simp add: INum_def split_def isnormNum_def split: split_if_asm) }
   1.227    moreover
   1.228    { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
   1.229      from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
   1.230 @@ -217,9 +190,10 @@
   1.231  qed
   1.232  
   1.233  
   1.234 -lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
   1.235 +lemma isnormNum0[simp]:
   1.236 +    "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
   1.237    unfolding INum_int(2)[symmetric]
   1.238 -  by (rule isnormNum_unique, simp_all)
   1.239 +  by (rule isnormNum_unique) simp_all
   1.240  
   1.241  lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) = 
   1.242      of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)"
   1.243 @@ -241,25 +215,27 @@
   1.244    apply (frule of_int_div_aux [of d n, where ?'a = 'a])
   1.245    apply simp
   1.246    apply (simp add: dvd_eq_mod_eq_0)
   1.247 -done
   1.248 +  done
   1.249  
   1.250  
   1.251  lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
   1.252 -proof-
   1.253 +proof -
   1.254    have "\<exists> a b. x = (a,b)" by auto
   1.255 -  then obtain a b where x[simp]: "x = (a,b)" by blast
   1.256 -  {assume "a=0 \<or> b = 0" hence ?thesis
   1.257 -      by (simp add: INum_def normNum_def split_def Let_def)}
   1.258 +  then obtain a b where x: "x = (a,b)" by blast
   1.259 +  { assume "a=0 \<or> b = 0" hence ?thesis
   1.260 +      by (simp add: x INum_def normNum_def split_def Let_def)}
   1.261    moreover 
   1.262 -  {assume a: "a\<noteq>0" and b: "b\<noteq>0"
   1.263 +  { assume a: "a\<noteq>0" and b: "b\<noteq>0"
   1.264      let ?g = "gcd a b"
   1.265      from a b have g: "?g \<noteq> 0"by simp
   1.266      from of_int_div[OF g, where ?'a = 'a]
   1.267 -    have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)}
   1.268 +    have ?thesis by (auto simp add: x INum_def normNum_def split_def Let_def) }
   1.269    ultimately show ?thesis by blast
   1.270  qed
   1.271  
   1.272 -lemma INum_normNum_iff: "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
   1.273 +lemma INum_normNum_iff:
   1.274 +  "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y"
   1.275 +  (is "?lhs = ?rhs")
   1.276  proof -
   1.277    have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
   1.278      by (simp del: normNum)
   1.279 @@ -268,139 +244,159 @@
   1.280  qed
   1.281  
   1.282  lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})"
   1.283 -proof-
   1.284 -let ?z = "0:: 'a"
   1.285 -  have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
   1.286 -  then obtain a b a' b' where x[simp]: "x = (a,b)" 
   1.287 +proof -
   1.288 +  let ?z = "0:: 'a"
   1.289 +  have "\<exists>a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
   1.290 +  then obtain a b a' b' where x: "x = (a,b)" 
   1.291      and y[simp]: "y = (a',b')" by blast
   1.292 -  {assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0" hence ?thesis 
   1.293 -      apply (cases "a=0",simp_all add: Nadd_def)
   1.294 -      apply (cases "b= 0",simp_all add: INum_def)
   1.295 -       apply (cases "a'= 0",simp_all)
   1.296 -       apply (cases "b'= 0",simp_all)
   1.297 +  { assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0"
   1.298 +    hence ?thesis 
   1.299 +      apply (cases "a=0", simp_all add: x Nadd_def)
   1.300 +      apply (cases "b= 0", simp_all add: INum_def)
   1.301 +       apply (cases "a'= 0", simp_all)
   1.302 +       apply (cases "b'= 0", simp_all)
   1.303         done }
   1.304    moreover 
   1.305 -  {assume aa':"a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0" 
   1.306 -    {assume z: "a * b' + b * a' = 0"
   1.307 +  { assume aa':"a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0" 
   1.308 +    { assume z: "a * b' + b * a' = 0"
   1.309        hence "of_int (a*b' + b*a') / (of_int b* of_int b') = ?z" by simp
   1.310 -      hence "of_int b' * of_int a / (of_int b * of_int b') + of_int b * of_int a' / (of_int b * of_int b') = ?z"  by (simp add:add_divide_distrib) 
   1.311 -      hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa' by simp 
   1.312 +      hence "of_int b' * of_int a / (of_int b * of_int b') + of_int b * of_int a' / (of_int b * of_int b') = ?z"
   1.313 +        by (simp add:add_divide_distrib) 
   1.314 +      hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa'
   1.315 +        by simp 
   1.316        from z aa' bb' have ?thesis 
   1.317 -        by (simp add: th Nadd_def normNum_def INum_def split_def)}
   1.318 -    moreover {assume z: "a * b' + b * a' \<noteq> 0"
   1.319 +        by (simp add: x th Nadd_def normNum_def INum_def split_def) }
   1.320 +    moreover {
   1.321 +      assume z: "a * b' + b * a' \<noteq> 0"
   1.322        let ?g = "gcd (a * b' + b * a') (b*b')"
   1.323        have gz: "?g \<noteq> 0" using z by simp
   1.324        have ?thesis using aa' bb' z gz
   1.325 -        of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]  of_int_div[where ?'a = 'a,
   1.326 -        OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
   1.327 -        by (simp add: Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
   1.328 -    ultimately have ?thesis using aa' bb' 
   1.329 -      by (simp add: Nadd_def INum_def normNum_def Let_def) }
   1.330 +        of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]
   1.331 +        of_int_div[where ?'a = 'a, OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
   1.332 +        by (simp add: x Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
   1.333 +    ultimately have ?thesis using aa' bb'
   1.334 +      by (simp add: x Nadd_def INum_def normNum_def Let_def) }
   1.335    ultimately show ?thesis by blast
   1.336  qed
   1.337  
   1.338 -lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero}) "
   1.339 -proof-
   1.340 +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero})"
   1.341 +proof -
   1.342    let ?z = "0::'a"
   1.343 -  have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
   1.344 +  have "\<exists>a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
   1.345    then obtain a b a' b' where x: "x = (a,b)" and y: "y = (a',b')" by blast
   1.346 -  {assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0" hence ?thesis 
   1.347 -      apply (cases "a=0",simp_all add: x y Nmul_def INum_def Let_def)
   1.348 -      apply (cases "b=0",simp_all)
   1.349 -      apply (cases "a'=0",simp_all) 
   1.350 +  { assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0"
   1.351 +    hence ?thesis 
   1.352 +      apply (cases "a=0", simp_all add: x y Nmul_def INum_def Let_def)
   1.353 +      apply (cases "b=0", simp_all)
   1.354 +      apply (cases "a'=0", simp_all) 
   1.355        done }
   1.356    moreover
   1.357 -  {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
   1.358 +  { assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
   1.359      let ?g="gcd (a*a') (b*b')"
   1.360      have gz: "?g \<noteq> 0" using z by simp
   1.361 -    from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]] 
   1.362 +    from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]]
   1.363        of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]] 
   1.364 -    have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
   1.365 +    have ?thesis by (simp add: Nmul_def x y Let_def INum_def) }
   1.366    ultimately show ?thesis by blast
   1.367  qed
   1.368  
   1.369  lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
   1.370    by (simp add: Nneg_def split_def INum_def)
   1.371  
   1.372 -lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
   1.373 -by (simp add: Nsub_def split_def)
   1.374 +lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
   1.375 +  by (simp add: Nsub_def split_def)
   1.376  
   1.377  lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)"
   1.378    by (simp add: Ninv_def INum_def split_def)
   1.379  
   1.380 -lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})" by (simp add: Ndiv_def)
   1.381 +lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})"
   1.382 +  by (simp add: Ndiv_def)
   1.383  
   1.384 -lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" 
   1.385 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x "
   1.386 -proof-
   1.387 -  have " \<exists> a b. x = (a,b)" by simp
   1.388 +lemma Nlt0_iff[simp]:
   1.389 +  assumes nx: "isnormNum x" 
   1.390 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x"
   1.391 +proof -
   1.392 +  have "\<exists> a b. x = (a,b)" by simp
   1.393    then obtain a b where x[simp]:"x = (a,b)" by blast
   1.394    {assume "a = 0" hence ?thesis by (simp add: Nlt0_def INum_def) }
   1.395    moreover
   1.396 -  {assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
   1.397 +  { assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
   1.398      from pos_divide_less_eq[OF b, where b="of_int a" and a="0::'a"]
   1.399 -    have ?thesis by (simp add: Nlt0_def INum_def)}
   1.400 +    have ?thesis by (simp add: Nlt0_def INum_def) }
   1.401    ultimately show ?thesis by blast
   1.402  qed
   1.403  
   1.404 -lemma Nle0_iff[simp]:assumes nx: "isnormNum x" 
   1.405 +lemma Nle0_iff[simp]:
   1.406 +  assumes nx: "isnormNum x"
   1.407    shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<le> 0) = 0\<ge>\<^sub>N x"
   1.408 -proof-
   1.409 -  have " \<exists> a b. x = (a,b)" by simp
   1.410 +proof -
   1.411 +  have "\<exists>a b. x = (a,b)" by simp
   1.412    then obtain a b where x[simp]:"x = (a,b)" by blast
   1.413 -  {assume "a = 0" hence ?thesis by (simp add: Nle0_def INum_def) }
   1.414 +  { assume "a = 0" hence ?thesis by (simp add: Nle0_def INum_def) }
   1.415    moreover
   1.416 -  {assume a: "a\<noteq>0" hence b: "(of_int b :: 'a) > 0" using nx by (simp add: isnormNum_def)
   1.417 +  { assume a: "a\<noteq>0" hence b: "(of_int b :: 'a) > 0" using nx by (simp add: isnormNum_def)
   1.418      from pos_divide_le_eq[OF b, where b="of_int a" and a="0::'a"]
   1.419      have ?thesis by (simp add: Nle0_def INum_def)}
   1.420    ultimately show ?thesis by blast
   1.421  qed
   1.422  
   1.423 -lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
   1.424 -proof-
   1.425 -  have " \<exists> a b. x = (a,b)" by simp
   1.426 +lemma Ngt0_iff[simp]:
   1.427 +  assumes nx: "isnormNum x"
   1.428 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
   1.429 +proof -
   1.430 +  have "\<exists> a b. x = (a,b)" by simp
   1.431    then obtain a b where x[simp]:"x = (a,b)" by blast
   1.432 -  {assume "a = 0" hence ?thesis by (simp add: Ngt0_def INum_def) }
   1.433 +  { assume "a = 0" hence ?thesis by (simp add: Ngt0_def INum_def) }
   1.434    moreover
   1.435 -  {assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
   1.436 +  { assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx
   1.437 +      by (simp add: isnormNum_def)
   1.438      from pos_less_divide_eq[OF b, where b="of_int a" and a="0::'a"]
   1.439 -    have ?thesis by (simp add: Ngt0_def INum_def)}
   1.440 -  ultimately show ?thesis by blast
   1.441 -qed
   1.442 -lemma Nge0_iff[simp]:assumes nx: "isnormNum x" 
   1.443 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
   1.444 -proof-
   1.445 -  have " \<exists> a b. x = (a,b)" by simp
   1.446 -  then obtain a b where x[simp]:"x = (a,b)" by blast
   1.447 -  {assume "a = 0" hence ?thesis by (simp add: Nge0_def INum_def) }
   1.448 -  moreover
   1.449 -  {assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
   1.450 -    from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"]
   1.451 -    have ?thesis by (simp add: Nge0_def INum_def)}
   1.452 +    have ?thesis by (simp add: Ngt0_def INum_def) }
   1.453    ultimately show ?thesis by blast
   1.454  qed
   1.455  
   1.456 -lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
   1.457 +lemma Nge0_iff[simp]:
   1.458 +  assumes nx: "isnormNum x"
   1.459 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
   1.460 +proof -
   1.461 +  have "\<exists> a b. x = (a,b)" by simp
   1.462 +  then obtain a b where x[simp]:"x = (a,b)" by blast
   1.463 +  { assume "a = 0" hence ?thesis by (simp add: Nge0_def INum_def) }
   1.464 +  moreover
   1.465 +  { assume "a \<noteq> 0" hence b: "(of_int b::'a) > 0" using nx
   1.466 +      by (simp add: isnormNum_def)
   1.467 +    from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"]
   1.468 +    have ?thesis by (simp add: Nge0_def INum_def) }
   1.469 +  ultimately show ?thesis by blast
   1.470 +qed
   1.471 +
   1.472 +lemma Nlt_iff[simp]:
   1.473 +  assumes nx: "isnormNum x" and ny: "isnormNum y"
   1.474    shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)"
   1.475 -proof-
   1.476 +proof -
   1.477    let ?z = "0::'a"
   1.478 -  have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp
   1.479 -  also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))" using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
   1.480 +  have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)"
   1.481 +    using nx ny by simp
   1.482 +  also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))"
   1.483 +    using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
   1.484    finally show ?thesis by (simp add: Nlt_def)
   1.485  qed
   1.486  
   1.487 -lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
   1.488 +lemma Nle_iff[simp]:
   1.489 +  assumes nx: "isnormNum x" and ny: "isnormNum y"
   1.490    shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\<le> INum y) = (x \<le>\<^sub>N y)"
   1.491 -proof-
   1.492 -  have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" using nx ny by simp
   1.493 -  also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp
   1.494 +proof -
   1.495 +  have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))"
   1.496 +    using nx ny by simp
   1.497 +  also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))"
   1.498 +    using Nle0_iff[OF Nsub_normN[OF ny]] by simp
   1.499    finally show ?thesis by (simp add: Nle_def)
   1.500  qed
   1.501  
   1.502  lemma Nadd_commute:
   1.503    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.504    shows "x +\<^sub>N y = y +\<^sub>N x"
   1.505 -proof-
   1.506 +proof -
   1.507    have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
   1.508    have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp
   1.509    with isnormNum_unique[OF n] show ?thesis by simp
   1.510 @@ -422,12 +418,11 @@
   1.511    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.512    assumes nx: "isnormNum x" 
   1.513    shows "normNum x = x"
   1.514 -proof-
   1.515 +proof -
   1.516    let ?a = "normNum x"
   1.517    have n: "isnormNum ?a" by simp
   1.518 -  have th:"INum ?a = (INum x ::'a)" by simp
   1.519 -  with isnormNum_unique[OF n nx]  
   1.520 -  show ?thesis by simp
   1.521 +  have th: "INum ?a = (INum x ::'a)" by simp
   1.522 +  with isnormNum_unique[OF n nx] show ?thesis by simp
   1.523  qed
   1.524  
   1.525  lemma normNum_nilpotent[simp]:
   1.526 @@ -445,7 +440,7 @@
   1.527  lemma Nadd_normNum1[simp]:
   1.528    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.529    shows "normNum x +\<^sub>N y = x +\<^sub>N y"
   1.530 -proof-
   1.531 +proof -
   1.532    have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
   1.533    have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp
   1.534    also have "\<dots> = INum (x +\<^sub>N y)" by simp
   1.535 @@ -455,7 +450,7 @@
   1.536  lemma Nadd_normNum2[simp]:
   1.537    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.538    shows "x +\<^sub>N normNum y = x +\<^sub>N y"
   1.539 -proof-
   1.540 +proof -
   1.541    have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
   1.542    have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp
   1.543    also have "\<dots> = INum (x +\<^sub>N y)" by simp
   1.544 @@ -465,7 +460,7 @@
   1.545  lemma Nadd_assoc:
   1.546    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.547    shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
   1.548 -proof-
   1.549 +proof -
   1.550    have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
   1.551    have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
   1.552    with isnormNum_unique[OF n] show ?thesis by simp
   1.553 @@ -478,7 +473,7 @@
   1.554    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.555    assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
   1.556    shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
   1.557 -proof-
   1.558 +proof -
   1.559    from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" 
   1.560      by simp_all
   1.561    have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
   1.562 @@ -488,13 +483,13 @@
   1.563  lemma Nsub0:
   1.564    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.565    assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
   1.566 -proof-
   1.567 -  { fix h :: 'a
   1.568 -    from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] 
   1.569 -    have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp
   1.570 -    also have "\<dots> = (INum x = (INum y :: 'a))" by simp
   1.571 -    also have "\<dots> = (x = y)" using x y by simp
   1.572 -    finally show ?thesis . }
   1.573 +proof -
   1.574 +  fix h :: 'a
   1.575 +  from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] 
   1.576 +  have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp
   1.577 +  also have "\<dots> = (INum x = (INum y :: 'a))" by simp
   1.578 +  also have "\<dots> = (x = y)" using x y by simp
   1.579 +  finally show ?thesis .
   1.580  qed
   1.581  
   1.582  lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N"
   1.583 @@ -504,16 +499,18 @@
   1.584    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.585    assumes nx:"isnormNum x" and ny: "isnormNum y"
   1.586    shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)"
   1.587 -proof-
   1.588 -  { fix h :: 'a
   1.589 -    have " \<exists> a b a' b'. x = (a,b) \<and> y= (a',b')" by auto
   1.590 -    then obtain a b a' b' where xy[simp]: "x = (a,b)" "y = (a',b')" by blast
   1.591 -    have n0: "isnormNum 0\<^sub>N" by simp
   1.592 -    show ?thesis using nx ny 
   1.593 -      apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
   1.594 -      by (simp add: INum_def split_def isnormNum_def split: split_if_asm)
   1.595 -  }
   1.596 +proof -
   1.597 +  fix h :: 'a
   1.598 +  have " \<exists> a b a' b'. x = (a,b) \<and> y= (a',b')" by auto
   1.599 +  then obtain a b a' b' where xy[simp]: "x = (a,b)" "y = (a',b')" by blast
   1.600 +  have n0: "isnormNum 0\<^sub>N" by simp
   1.601 +  show ?thesis using nx ny 
   1.602 +    apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric]
   1.603 +      Nmul[where ?'a = 'a])
   1.604 +    apply (simp add: INum_def split_def isnormNum_def split: split_if_asm)
   1.605 +    done
   1.606  qed
   1.607 +
   1.608  lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
   1.609    by (simp add: Nneg_def split_def)
   1.610