proper implementation of rational numbers
authorhaftmann
Thu Aug 09 15:52:49 2007 +0200 (2007-08-09)
changeset 24197c9e3cb5e5681
parent 24196 f1dbfd7e3223
child 24198 4031da6d8ba3
proper implementation of rational numbers
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/Executable_Rat.thy
src/HOL/Library/Executable_Real.thy
src/HOL/Library/Library.thy
src/HOL/ex/ExecutableContent.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Thu Aug 09 15:52:49 2007 +0200
     1.3 @@ -0,0 +1,502 @@
     1.4 +(*  Title:      HOL/Library/Abstract_Rat.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Amine Chaieb
     1.7 +*)
     1.8 +
     1.9 +header {* Abstract rational numbers *}
    1.10 +
    1.11 +theory Abstract_Rat
    1.12 +imports GCD
    1.13 +begin
    1.14 +
    1.15 +types Num = "int \<times> int"
    1.16 +syntax "_Num0" :: "Num" ("0\<^sub>N")
    1.17 +translations "0\<^sub>N" \<rightleftharpoons> "(0, 0)"
    1.18 +syntax "_Numi" :: "int \<Rightarrow> Num" ("_\<^sub>N")
    1.19 +translations "i\<^sub>N" \<rightleftharpoons> "(i, 1) \<Colon> Num"
    1.20 +
    1.21 +definition
    1.22 +  isnormNum :: "Num \<Rightarrow> bool"
    1.23 +where
    1.24 +  "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> igcd a b = 1))"
    1.25 +
    1.26 +definition
    1.27 +  normNum :: "Num \<Rightarrow> Num"
    1.28 +where
    1.29 +  "normNum = (\<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else 
    1.30 +  (let g = igcd a b 
    1.31 +   in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
    1.32 +
    1.33 +lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
    1.34 +proof -
    1.35 +  have " \<exists> a b. x = (a,b)" by auto
    1.36 +  then obtain a b where x[simp]: "x = (a,b)" by blast
    1.37 +  {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}  
    1.38 +  moreover
    1.39 +  {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0" 
    1.40 +    let ?g = "igcd a b"
    1.41 +    let ?a' = "a div ?g"
    1.42 +    let ?b' = "b div ?g"
    1.43 +    let ?g' = "igcd ?a' ?b'"
    1.44 +    from anz bnz have "?g \<noteq> 0" by simp  with igcd_pos[of a b] 
    1.45 +    have gpos: "?g > 0"  by arith
    1.46 +    have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2)
    1.47 +    from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
    1.48 +    anz bnz
    1.49 +    have nz':"?a' \<noteq> 0" "?b' \<noteq> 0" 
    1.50 +      by - (rule notI,simp add:igcd_def)+
    1.51 +    from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by blast
    1.52 +    from div_igcd_relprime[OF stupid] have gp1: "?g' = 1" .
    1.53 +    from bnz have "b < 0 \<or> b > 0" by arith
    1.54 +    moreover
    1.55 +    {assume b: "b > 0"
    1.56 +      from pos_imp_zdiv_nonneg_iff[OF gpos] b
    1.57 +      have "?b' \<ge> 0" by simp
    1.58 +      with nz' have b': "?b' > 0" by simp
    1.59 +      from b b' anz bnz nz' gp1 have ?thesis 
    1.60 +	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    1.61 +    moreover {assume b: "b < 0"
    1.62 +      {assume b': "?b' \<ge> 0" 
    1.63 +	from gpos have th: "?g \<ge> 0" by arith
    1.64 +	from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
    1.65 +	have False using b by simp }
    1.66 +      hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric]) 
    1.67 +      from anz bnz nz' b b' gp1 have ?thesis 
    1.68 +	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    1.69 +    ultimately have ?thesis by blast
    1.70 +  }
    1.71 +  ultimately show ?thesis by blast
    1.72 +qed
    1.73 +
    1.74 +text {* Arithmetic over Num *}
    1.75 +
    1.76 +definition
    1.77 +  Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "+\<^sub>N" 60)
    1.78 +where
    1.79 +  "Nadd = (\<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b') 
    1.80 +    else if a'=0 \<or> b' = 0 then normNum(a,b) 
    1.81 +    else normNum(a*b' + b*a', b*b'))"
    1.82 +
    1.83 +definition
    1.84 +  Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
    1.85 +where
    1.86 +  "Nmul = (\<lambda>(a,b) (a',b'). let g = igcd (a*a') (b*b') 
    1.87 +    in (a*a' div g, b*b' div g))"
    1.88 +
    1.89 +definition
    1.90 +  Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N")
    1.91 +where
    1.92 +  "Nneg \<equiv> (\<lambda>(a,b). (-a,b))"
    1.93 +
    1.94 +definition
    1.95 +  Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "-\<^sub>N" 60)
    1.96 +where
    1.97 +  "Nsub = (\<lambda>a b. a +\<^sub>N ~\<^sub>N b)"
    1.98 +
    1.99 +definition
   1.100 +  Ninv :: "Num \<Rightarrow> Num" 
   1.101 +where
   1.102 +  "Ninv \<equiv> \<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a)"
   1.103 +
   1.104 +definition
   1.105 +  Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "\<div>\<^sub>N" 60)
   1.106 +where
   1.107 +  "Ndiv \<equiv> \<lambda>a b. a *\<^sub>N Ninv b"
   1.108 +
   1.109 +lemma Nneg_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (~\<^sub>N x)"
   1.110 +  by(simp add: isnormNum_def Nneg_def split_def)
   1.111 +lemma Nadd_normN[simp]: "isnormNum (x +\<^sub>N y)"
   1.112 +  by (simp add: Nadd_def split_def)
   1.113 +lemma Nsub_normN[simp]: "\<lbrakk> isnormNum y\<rbrakk> \<Longrightarrow> isnormNum (x -\<^sub>N y)"
   1.114 +  by (simp add: Nsub_def split_def)
   1.115 +lemma Nmul_normN[simp]: assumes xn:"isnormNum x" and yn: "isnormNum y"
   1.116 +  shows "isnormNum (x *\<^sub>N y)"
   1.117 +proof-
   1.118 +  have "\<exists>a b. x = (a,b)" and "\<exists> a' b'. y = (a',b')" by auto
   1.119 +  then obtain a b a' b' where ab: "x = (a,b)"  and ab': "y = (a',b')" by blast 
   1.120 +  {assume "a = 0"
   1.121 +    hence ?thesis using xn ab ab'
   1.122 +      by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
   1.123 +  moreover
   1.124 +  {assume "a' = 0"
   1.125 +    hence ?thesis using yn ab ab' 
   1.126 +      by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
   1.127 +  moreover
   1.128 +  {assume a: "a \<noteq>0" and a': "a'\<noteq>0"
   1.129 +    hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def)
   1.130 +    from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a*a', b*b')" 
   1.131 +      using ab ab' a a' bp by (simp add: Nmul_def Let_def split_def normNum_def)
   1.132 +    hence ?thesis by simp}
   1.133 +  ultimately show ?thesis by blast
   1.134 +qed
   1.135 +
   1.136 +lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
   1.137 +by (simp add: Ninv_def isnormNum_def split_def)
   1.138 +(cases "fst x = 0",auto simp add: igcd_commute)
   1.139 +
   1.140 +lemma isnormNum_int[simp]: 
   1.141 +  "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
   1.142 +  by (simp_all add: isnormNum_def igcd_def)
   1.143 +
   1.144 +
   1.145 +text {* Relations over Num *}
   1.146 +
   1.147 +definition
   1.148 +  Nlt0:: "Num \<Rightarrow> bool" ("0>\<^sub>N")
   1.149 +where
   1.150 +  "Nlt0 = (\<lambda>(a,b). a < 0)"
   1.151 +
   1.152 +definition
   1.153 +  Nle0:: "Num \<Rightarrow> bool" ("0\<ge>\<^sub>N")
   1.154 +where
   1.155 +  "Nle0 = (\<lambda>(a,b). a \<le> 0)"
   1.156 +
   1.157 +definition
   1.158 +  Ngt0:: "Num \<Rightarrow> bool" ("0<\<^sub>N")
   1.159 +where
   1.160 +  "Ngt0 = (\<lambda>(a,b). a > 0)"
   1.161 +
   1.162 +definition
   1.163 +  Nge0:: "Num \<Rightarrow> bool" ("0\<le>\<^sub>N")
   1.164 +where
   1.165 +  "Nge0 = (\<lambda>(a,b). a \<ge> 0)"
   1.166 +
   1.167 +definition
   1.168 +  Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "<\<^sub>N" 55)
   1.169 +where
   1.170 +  "Nlt = (\<lambda>a b. 0>\<^sub>N (a -\<^sub>N b))"
   1.171 +
   1.172 +definition
   1.173 +  Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "\<le>\<^sub>N" 55)
   1.174 +where
   1.175 +  "Nle = (\<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b))"
   1.176 +
   1.177 +definition
   1.178 +  "INum = (\<lambda>(a,b). of_int a / of_int b)"
   1.179 +
   1.180 +lemma INum_int [simp]: "INum i\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
   1.181 +  by (simp_all add: INum_def)
   1.182 +
   1.183 +lemma isnormNum_unique[simp]: 
   1.184 +  assumes na: "isnormNum x" and nb: "isnormNum y" 
   1.185 +  shows "((INum x ::'a::{ring_char_0,field, division_by_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
   1.186 +proof
   1.187 +  have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
   1.188 +  then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
   1.189 +  assume H: ?lhs 
   1.190 +  {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" hence ?rhs
   1.191 +      using na nb H
   1.192 +      apply (simp add: INum_def split_def isnormNum_def)
   1.193 +      apply (cases "a = 0", simp_all)
   1.194 +      apply (cases "b = 0", simp_all)
   1.195 +      apply (cases "a' = 0", simp_all)
   1.196 +      apply (cases "a' = 0", simp_all add: of_int_eq_0_iff)
   1.197 +      done}
   1.198 +  moreover
   1.199 +  { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
   1.200 +    from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
   1.201 +    from prems have eq:"a * b' = a'*b" 
   1.202 +      by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
   1.203 +    from prems have gcd1: "igcd a b = 1" "igcd b a = 1" "igcd a' b' = 1" "igcd b' a' = 1"       
   1.204 +      by (simp_all add: isnormNum_def add: igcd_commute)
   1.205 +    from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'" 
   1.206 +      apply(unfold dvd_def)
   1.207 +      apply (rule_tac x="b'" in exI, simp add: mult_ac)
   1.208 +      apply (rule_tac x="a'" in exI, simp add: mult_ac)
   1.209 +      apply (rule_tac x="b" in exI, simp add: mult_ac)
   1.210 +      apply (rule_tac x="a" in exI, simp add: mult_ac)
   1.211 +      done
   1.212 +    from zdvd_dvd_eq[OF bz zrelprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
   1.213 +      zrelprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
   1.214 +      have eq1: "b = b'" using pos by simp_all
   1.215 +      with eq have "a = a'" using pos by simp
   1.216 +      with eq1 have ?rhs by simp}
   1.217 +  ultimately show ?rhs by blast
   1.218 +next
   1.219 +  assume ?rhs thus ?lhs by simp
   1.220 +qed
   1.221 +
   1.222 +
   1.223 +lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{ring_char_0, field,division_by_zero})) = (x = 0\<^sub>N)"
   1.224 +  unfolding INum_int(2)[symmetric]
   1.225 +  by (rule isnormNum_unique, simp_all)
   1.226 +
   1.227 +lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::{field, ring_char_0}) / (of_int d) = 
   1.228 +    of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)"
   1.229 +proof -
   1.230 +  assume "d ~= 0"
   1.231 +  hence dz: "of_int d \<noteq> (0::'a)" by (simp add: of_int_eq_0_iff)
   1.232 +  let ?t = "of_int (x div d) * ((of_int d)::'a) + of_int(x mod d)"
   1.233 +  let ?f = "\<lambda>x. x / of_int d"
   1.234 +  have "x = (x div d) * d + x mod d"
   1.235 +    by auto
   1.236 +  then have eq: "of_int x = ?t"
   1.237 +    by (simp only: of_int_mult[symmetric] of_int_add [symmetric])
   1.238 +  then have "of_int x / of_int d = ?t / of_int d" 
   1.239 +    using cong[OF refl[of ?f] eq] by simp
   1.240 +  then show ?thesis by (simp add: add_divide_distrib ring_simps prems)
   1.241 +qed
   1.242 +
   1.243 +lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
   1.244 +    (of_int(n div d)::'a::{field, ring_char_0}) = of_int n / of_int d"
   1.245 +  apply (frule of_int_div_aux [of d n, where ?'a = 'a])
   1.246 +  apply simp
   1.247 +  apply (simp add: zdvd_iff_zmod_eq_0)
   1.248 +done
   1.249 +
   1.250 +
   1.251 +lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{ring_char_0,field, division_by_zero})"
   1.252 +proof-
   1.253 +  have "\<exists> a b. x = (a,b)" by auto
   1.254 +  then obtain a b where x[simp]: "x = (a,b)" by blast
   1.255 +  {assume "a=0 \<or> b = 0" hence ?thesis
   1.256 +      by (simp add: INum_def normNum_def split_def Let_def)}
   1.257 +  moreover 
   1.258 +  {assume a: "a\<noteq>0" and b: "b\<noteq>0"
   1.259 +    let ?g = "igcd a b"
   1.260 +    from a b have g: "?g \<noteq> 0"by simp
   1.261 +    from of_int_div[OF g, where ?'a = 'a]
   1.262 +    have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)}
   1.263 +  ultimately show ?thesis by blast
   1.264 +qed
   1.265 +
   1.266 +lemma INum_normNum_iff [code]: "(INum x ::'a::{field, division_by_zero, ring_char_0}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
   1.267 +proof -
   1.268 +  have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
   1.269 +    by (simp del: normNum)
   1.270 +  also have "\<dots> = ?lhs" by simp
   1.271 +  finally show ?thesis by simp
   1.272 +qed
   1.273 +
   1.274 +lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {ring_char_0,division_by_zero,field})"
   1.275 +proof-
   1.276 +let ?z = "0:: 'a"
   1.277 +  have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
   1.278 +  then obtain a b a' b' where x[simp]: "x = (a,b)" 
   1.279 +    and y[simp]: "y = (a',b')" by blast
   1.280 +  {assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0" hence ?thesis 
   1.281 +      apply (cases "a=0",simp_all add: Nadd_def)
   1.282 +      apply (cases "b= 0",simp_all add: INum_def)
   1.283 +       apply (cases "a'= 0",simp_all)
   1.284 +       apply (cases "b'= 0",simp_all)
   1.285 +       done }
   1.286 +  moreover 
   1.287 +  {assume aa':"a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0" 
   1.288 +    {assume z: "a * b' + b * a' = 0"
   1.289 +      hence "of_int (a*b' + b*a') / (of_int b* of_int b') = ?z" by simp
   1.290 +      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.291 +      hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa' by simp 
   1.292 +      from z aa' bb' have ?thesis 
   1.293 +	by (simp add: th Nadd_def normNum_def INum_def split_def)}
   1.294 +    moreover {assume z: "a * b' + b * a' \<noteq> 0"
   1.295 +      let ?g = "igcd (a * b' + b * a') (b*b')"
   1.296 +      have gz: "?g \<noteq> 0" using z by simp
   1.297 +      have ?thesis using aa' bb' z gz
   1.298 +	of_int_div[where ?'a = 'a, 
   1.299 +	OF gz igcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
   1.300 +	of_int_div[where ?'a = 'a,
   1.301 +	OF gz igcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
   1.302 +	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
   1.303 +    ultimately have ?thesis using aa' bb' 
   1.304 +      by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
   1.305 +  ultimately show ?thesis by blast
   1.306 +qed
   1.307 +
   1.308 +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {ring_char_0,division_by_zero,field}) "
   1.309 +proof-
   1.310 +  let ?z = "0::'a"
   1.311 +  have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
   1.312 +  then obtain a b a' b' where x: "x = (a,b)" and y: "y = (a',b')" by blast
   1.313 +  {assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0" hence ?thesis 
   1.314 +      apply (cases "a=0",simp_all add: x y Nmul_def INum_def Let_def)
   1.315 +      apply (cases "b=0",simp_all)
   1.316 +      apply (cases "a'=0",simp_all) 
   1.317 +      done }
   1.318 +  moreover
   1.319 +  {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
   1.320 +    let ?g="igcd (a*a') (b*b')"
   1.321 +    have gz: "?g \<noteq> 0" using z by simp
   1.322 +    from z of_int_div[where ?'a = 'a, OF gz igcd_dvd1[where i="a*a'" and j="b*b'"]] 
   1.323 +      of_int_div[where ?'a = 'a , OF gz igcd_dvd2[where i="a*a'" and j="b*b'"]] 
   1.324 +    have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
   1.325 +  ultimately show ?thesis by blast
   1.326 +qed
   1.327 +
   1.328 +lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
   1.329 +  by (simp add: Nneg_def split_def INum_def)
   1.330 +
   1.331 +lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {ring_char_0,division_by_zero,field})"
   1.332 +by (simp add: Nsub_def split_def)
   1.333 +
   1.334 +lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: {division_by_zero,field}) / (INum x)"
   1.335 +  by (simp add: Ninv_def INum_def split_def)
   1.336 +
   1.337 +lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {ring_char_0, division_by_zero,field})" by (simp add: Ndiv_def)
   1.338 +
   1.339 +lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" 
   1.340 +  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field})< 0) = 0>\<^sub>N x "
   1.341 +proof-
   1.342 +  have " \<exists> a b. x = (a,b)" by simp
   1.343 +  then obtain a b where x[simp]:"x = (a,b)" by blast
   1.344 +  {assume "a = 0" hence ?thesis by (simp add: Nlt0_def INum_def) }
   1.345 +  moreover
   1.346 +  {assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
   1.347 +    from pos_divide_less_eq[OF b, where b="of_int a" and a="0::'a"]
   1.348 +    have ?thesis by (simp add: Nlt0_def INum_def)}
   1.349 +  ultimately show ?thesis by blast
   1.350 +qed
   1.351 +
   1.352 +lemma Nle0_iff[simp]:assumes nx: "isnormNum x" 
   1.353 +  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field}) \<le> 0) = 0\<ge>\<^sub>N x"
   1.354 +proof-
   1.355 +  have " \<exists> a b. x = (a,b)" by simp
   1.356 +  then obtain a b where x[simp]:"x = (a,b)" by blast
   1.357 +  {assume "a = 0" hence ?thesis by (simp add: Nle0_def INum_def) }
   1.358 +  moreover
   1.359 +  {assume a: "a\<noteq>0" hence b: "(of_int b :: 'a) > 0" using nx by (simp add: isnormNum_def)
   1.360 +    from pos_divide_le_eq[OF b, where b="of_int a" and a="0::'a"]
   1.361 +    have ?thesis by (simp add: Nle0_def INum_def)}
   1.362 +  ultimately show ?thesis by blast
   1.363 +qed
   1.364 +
   1.365 +lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field})> 0) = 0<\<^sub>N x"
   1.366 +proof-
   1.367 +  have " \<exists> a b. x = (a,b)" by simp
   1.368 +  then obtain a b where x[simp]:"x = (a,b)" by blast
   1.369 +  {assume "a = 0" hence ?thesis by (simp add: Ngt0_def INum_def) }
   1.370 +  moreover
   1.371 +  {assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
   1.372 +    from pos_less_divide_eq[OF b, where b="of_int a" and a="0::'a"]
   1.373 +    have ?thesis by (simp add: Ngt0_def INum_def)}
   1.374 +  ultimately show ?thesis by blast
   1.375 +qed
   1.376 +lemma Nge0_iff[simp]:assumes nx: "isnormNum x" 
   1.377 +  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field}) \<ge> 0) = 0\<le>\<^sub>N x"
   1.378 +proof-
   1.379 +  have " \<exists> a b. x = (a,b)" by simp
   1.380 +  then obtain a b where x[simp]:"x = (a,b)" by blast
   1.381 +  {assume "a = 0" hence ?thesis by (simp add: Nge0_def INum_def) }
   1.382 +  moreover
   1.383 +  {assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
   1.384 +    from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"]
   1.385 +    have ?thesis by (simp add: Nge0_def INum_def)}
   1.386 +  ultimately show ?thesis by blast
   1.387 +qed
   1.388 +
   1.389 +lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
   1.390 +  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field}) < INum y) = (x <\<^sub>N y)"
   1.391 +proof-
   1.392 +  let ?z = "0::'a"
   1.393 +  have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp
   1.394 +  also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))" using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
   1.395 +  finally show ?thesis by (simp add: Nlt_def)
   1.396 +qed
   1.397 +
   1.398 +lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
   1.399 +  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field})\<le> INum y) = (x \<le>\<^sub>N y)"
   1.400 +proof-
   1.401 +  have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" using nx ny by simp
   1.402 +  also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp
   1.403 +  finally show ?thesis by (simp add: Nle_def)
   1.404 +qed
   1.405 +
   1.406 +lemma Nadd_commute: "x +\<^sub>N y = y +\<^sub>N x"
   1.407 +proof-
   1.408 +  have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
   1.409 +  have "(INum (x +\<^sub>N y)::'a :: {ring_char_0,division_by_zero,field}) = INum (y +\<^sub>N x)" by simp
   1.410 +  with isnormNum_unique[OF n] show ?thesis by simp
   1.411 +qed
   1.412 +
   1.413 +lemma[simp]: "(0, b) +\<^sub>N y = normNum y" "(a, 0) +\<^sub>N y = normNum y" 
   1.414 +  "x +\<^sub>N (0, b) = normNum x" "x +\<^sub>N (a, 0) = normNum x"
   1.415 +  apply (simp add: Nadd_def split_def, simp add: Nadd_def split_def)
   1.416 +  apply (subst Nadd_commute,simp add: Nadd_def split_def)
   1.417 +  apply (subst Nadd_commute,simp add: Nadd_def split_def)
   1.418 +  done
   1.419 +
   1.420 +lemma normNum_nilpotent_aux[simp]: assumes nx: "isnormNum x" 
   1.421 +  shows "normNum x = x"
   1.422 +proof-
   1.423 +  let ?a = "normNum x"
   1.424 +  have n: "isnormNum ?a" by simp
   1.425 +  have th:"INum ?a = (INum x ::'a :: {ring_char_0, division_by_zero,field})" by simp
   1.426 +  with isnormNum_unique[OF n nx]  
   1.427 +  show ?thesis by simp
   1.428 +qed
   1.429 +
   1.430 +lemma normNum_nilpotent[simp]: "normNum (normNum x) = normNum x"
   1.431 +  by simp
   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 +lemma normNum_Nadd: "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
   1.435 +lemma Nadd_normNum1[simp]: "normNum x +\<^sub>N y = x +\<^sub>N y"
   1.436 +proof-
   1.437 +  have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
   1.438 +  have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a :: {ring_char_0, division_by_zero,field})" by simp
   1.439 +  also have "\<dots> = INum (x +\<^sub>N y)" by simp
   1.440 +  finally show ?thesis using isnormNum_unique[OF n] by simp
   1.441 +qed
   1.442 +lemma Nadd_normNum2[simp]: "x +\<^sub>N normNum y = x +\<^sub>N y"
   1.443 +proof-
   1.444 +  have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
   1.445 +  have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a :: {ring_char_0, division_by_zero,field})" by simp
   1.446 +  also have "\<dots> = INum (x +\<^sub>N y)" by simp
   1.447 +  finally show ?thesis using isnormNum_unique[OF n] by simp
   1.448 +qed
   1.449 +
   1.450 +lemma Nadd_assoc: "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
   1.451 +proof-
   1.452 +  have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
   1.453 +  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a :: {ring_char_0, division_by_zero,field})" by simp
   1.454 +  with isnormNum_unique[OF n] show ?thesis by simp
   1.455 +qed
   1.456 +
   1.457 +lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
   1.458 +  by (simp add: Nmul_def split_def Let_def igcd_commute mult_commute)
   1.459 +
   1.460 +lemma Nmul_assoc: assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
   1.461 +  shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
   1.462 +proof-
   1.463 +  from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" 
   1.464 +    by simp_all
   1.465 +  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a :: {ring_char_0, division_by_zero,field})" by simp
   1.466 +  with isnormNum_unique[OF n] show ?thesis by simp
   1.467 +qed
   1.468 +
   1.469 +lemma Nsub0: assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
   1.470 +proof-
   1.471 +  {fix h :: "'a :: {ring_char_0,division_by_zero,ordered_field}"
   1.472 +    from isnormNum_unique[where ?'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] 
   1.473 +    have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp
   1.474 +    also have "\<dots> = (INum x = (INum y:: 'a))" by simp
   1.475 +    also have "\<dots> = (x = y)" using x y by simp
   1.476 +    finally show ?thesis .}
   1.477 +qed
   1.478 +
   1.479 +lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N"
   1.480 +  by (simp_all add: Nmul_def Let_def split_def)
   1.481 +
   1.482 +lemma Nmul_eq0[simp]: assumes nx:"isnormNum x" and ny: "isnormNum y"
   1.483 +  shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)"
   1.484 +proof-
   1.485 +  {fix h :: "'a :: {ring_char_0,division_by_zero,ordered_field}"
   1.486 +  have " \<exists> a b a' b'. x = (a,b) \<and> y= (a',b')" by auto
   1.487 +  then obtain a b a' b' where xy[simp]: "x = (a,b)" "y = (a',b')" by blast
   1.488 +  have n0: "isnormNum 0\<^sub>N" by simp
   1.489 +  show ?thesis using nx ny 
   1.490 +    apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
   1.491 +    apply (simp add: INum_def split_def isnormNum_def fst_conv snd_conv)
   1.492 +    apply (cases "a=0",simp_all)
   1.493 +    apply (cases "a'=0",simp_all)
   1.494 +    done }
   1.495 +qed
   1.496 +lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
   1.497 +  by (simp add: Nneg_def split_def)
   1.498 +
   1.499 +lemma Nmul1[simp]: 
   1.500 +  "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c" 
   1.501 +  "isnormNum c \<Longrightarrow> c *\<^sub>N 1\<^sub>N  = c" 
   1.502 +  apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
   1.503 +  by (cases "fst c = 0", simp_all,cases c, simp_all)+
   1.504 +
   1.505 +end
   1.506 \ No newline at end of file
     2.1 --- a/src/HOL/Library/Executable_Rat.thy	Thu Aug 09 15:52:47 2007 +0200
     2.2 +++ b/src/HOL/Library/Executable_Rat.thy	Thu Aug 09 15:52:49 2007 +0200
     2.3 @@ -3,107 +3,95 @@
     2.4      Author:     Florian Haftmann, TU Muenchen
     2.5  *)
     2.6  
     2.7 -header {* Executable implementation of rational numbers in HOL *}
     2.8 +header {* Implementation of rational numbers as pairs of integers *}
     2.9  
    2.10  theory Executable_Rat
    2.11 -imports "~~/src/HOL/Real/Rational" "~~/src/HOL/NumberTheory/IntPrimes"
    2.12 +imports Abstract_Rat "~~/src/HOL/Real/Rational"
    2.13  begin
    2.14  
    2.15 -text {*
    2.16 -  Actually \emph{nothing} is proved about this implementation.
    2.17 -*}
    2.18 -
    2.19 -subsection {* Representation and operations of executable rationals *}
    2.20 -
    2.21 -datatype erat = Rat bool nat nat
    2.22 -
    2.23 -axiomatization
    2.24 -  div_zero :: erat
    2.25 -
    2.26 -fun
    2.27 -  common :: "(nat * nat) \<Rightarrow> (nat * nat) \<Rightarrow> (nat * nat) * nat" where
    2.28 -  "common (p1, q1) (p2, q2) = (
    2.29 -     let
    2.30 -       q' = q1 * q2 div gcd (q1, q2)
    2.31 -     in ((p1 * (q' div q1), p2 * (q' div q2)), q'))"
    2.32 -
    2.33 -definition
    2.34 -  minus_sign :: "nat \<Rightarrow> nat \<Rightarrow> bool * nat" where
    2.35 -  "minus_sign n m = (if n < m then (False, m - n) else (True, n - m))"
    2.36 -
    2.37 -fun
    2.38 -  add_sign :: "bool * nat \<Rightarrow> bool * nat \<Rightarrow> bool * nat" where
    2.39 -  "add_sign (True, n) (True, m) = (True, n + m)"
    2.40 -| "add_sign (False, n) (False, m) = (False, n + m)"
    2.41 -| "add_sign (True, n) (False, m) = minus_sign n m"
    2.42 -| "add_sign (False, n) (True, m) = minus_sign m n"
    2.43 +hide (open) const Rat
    2.44  
    2.45  definition
    2.46 -  erat_of_quotient :: "int \<Rightarrow> int \<Rightarrow> erat" where
    2.47 -  "erat_of_quotient k1 k2 = (
    2.48 -    let
    2.49 -      l1 = nat (abs k1);
    2.50 -      l2 = nat (abs k2);
    2.51 -      m = gcd (l1, l2)
    2.52 -    in Rat (k1 \<le> 0 \<longleftrightarrow> k2 \<le> 0) (l1 div m) (l2 div m))"
    2.53 +  Rat :: "int \<times> int \<Rightarrow> rat"
    2.54 +where
    2.55 +  "Rat = INum"
    2.56 +
    2.57 +code_datatype Rat
    2.58  
    2.59 -instance erat :: zero
    2.60 -  zero_rat_def: "0 \<equiv> Rat True 0 1" ..
    2.61 -
    2.62 -instance erat :: one
    2.63 -  one_rat_def: "1 \<equiv> Rat True 1 1" ..
    2.64 +lemma Rat_simp:
    2.65 +  "Rat (k, l) = rat_of_int k / rat_of_int l"
    2.66 +  unfolding Rat_def INum_def by simp
    2.67  
    2.68 -instance erat :: plus
    2.69 -  add_rat_def: "r + s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
    2.70 -        let
    2.71 -          ((r1, r2), den) = common (p1, q1) (p2, q2);
    2.72 -          (sign, num) = add_sign (a1, r1) (a2, r2)
    2.73 -        in Rat sign num den" ..
    2.74 +lemma Rat_zero [simp]: "Rat 0\<^sub>N = 0"
    2.75 +  by (simp add: Rat_simp)
    2.76 +
    2.77 +lemma Rat_lit [simp]: "Rat i\<^sub>N = rat_of_int i"
    2.78 +  by (simp add: Rat_simp)
    2.79 +
    2.80 +lemma zero_rat_code [code]:
    2.81 +  "0 = Rat 0\<^sub>N" by simp
    2.82  
    2.83 -instance erat :: minus
    2.84 -  uminus_rat_def: "- r \<equiv> case r of Rat a p q \<Rightarrow>
    2.85 -        if p = 0 then Rat True 0 1
    2.86 -        else Rat (\<not> a) p q" ..
    2.87 -  
    2.88 -instance erat :: times
    2.89 -  times_rat_def: "r * s \<equiv> case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
    2.90 -        let
    2.91 -          p = p1 * p2;
    2.92 -          q = q1 * q2;
    2.93 -          m = gcd (p, q)
    2.94 -        in Rat (a1 = a2) (p div m) (q div m)" ..
    2.95 +lemma zero_rat_code [code]:
    2.96 +  "1 = Rat 1\<^sub>N" by simp
    2.97  
    2.98 -instance erat :: inverse
    2.99 -  inverse_rat_def: "inverse r \<equiv> case r of Rat a p q \<Rightarrow>
   2.100 -        if p = 0 then div_zero
   2.101 -        else Rat a q p" ..
   2.102 +lemma [code, code unfold]:
   2.103 +  "number_of k = rat_of_int (number_of k)"
   2.104 +  by (simp add: number_of_is_id rat_number_of_def)
   2.105 +
   2.106 +definition
   2.107 +  [code func del]: "Fract' (b\<Colon>bool) k l = Fract k l"
   2.108  
   2.109 -instance erat :: ord
   2.110 -  le_rat_def: "r1 \<le> r2 \<equiv> case r1 of Rat a1 p1 q1 \<Rightarrow> case r2 of Rat a2 p2 q2 \<Rightarrow>
   2.111 -        (\<not> a1 \<and> a2) \<or>
   2.112 -        (\<not> (a1 \<and> \<not> a2) \<and>
   2.113 -          (let
   2.114 -            ((r1, r2), dummy) = common (p1, q1) (p2, q2)
   2.115 -          in if a1 then r1 \<le> r2 else r2 \<le> r1))" ..
   2.116 -
   2.117 -
   2.118 -subsection {* Code generator setup *}
   2.119 +lemma [code]:
   2.120 +  "Fract k l = Fract' (l \<noteq> 0) k l"
   2.121 +  unfolding Fract'_def ..
   2.122  
   2.123 -subsubsection {* code lemmas *}
   2.124 -
   2.125 -lemma number_of_rat [code unfold]:
   2.126 -  "(number_of k \<Colon> rat) = Fract k 1"
   2.127 -  unfolding Fract_of_int_eq rat_number_of_def by simp
   2.128 +lemma [code]:
   2.129 +  "Fract' True k l = (if l \<noteq> 0 then Rat (k, l) else Fract 1 0)"
   2.130 +  by (simp add: Fract'_def Rat_simp Fract_of_int_quotient [of k l])
   2.131  
   2.132 -lemma rat_minus [code func]:
   2.133 -  "(a\<Colon>rat) - b = a + (- b)" unfolding diff_minus ..
   2.134 -
   2.135 -lemma rat_divide [code func]:
   2.136 -  "(a\<Colon>rat) / b = a * inverse b" unfolding divide_inverse ..
   2.137 +lemma [code]:
   2.138 +  "of_rat (Rat (k, l)) = (if l \<noteq> 0 then of_int k / of_int l else 0)"
   2.139 +  by (cases "l = 0")
   2.140 +    (auto simp add: Rat_simp of_rat_rat [simplified Fract_of_int_quotient [of k l], symmetric])
   2.141  
   2.142  instance rat :: eq ..
   2.143  
   2.144 -subsubsection {* names *}
   2.145 +lemma rat_eq_code [code]: "Rat x = Rat y \<longleftrightarrow> normNum x = normNum y"
   2.146 +  unfolding Rat_def INum_normNum_iff ..
   2.147 +
   2.148 +lemma rat_less_eq_code [code]: "Rat x \<le> Rat y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
   2.149 +proof -
   2.150 +  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> Rat (normNum x) \<le> Rat (normNum y)" 
   2.151 +    by (simp add: Rat_def del: normNum)
   2.152 +  also have "\<dots> = (Rat x \<le> Rat y)" by (simp add: Rat_def)
   2.153 +  finally show ?thesis by simp
   2.154 +qed
   2.155 +
   2.156 +lemma rat_less_code [code]: "Rat x < Rat y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
   2.157 +proof -
   2.158 +  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> Rat (normNum x) < Rat (normNum y)" 
   2.159 +    by (simp add: Rat_def del: normNum)
   2.160 +  also have "\<dots> = (Rat x < Rat y)" by (simp add: Rat_def)
   2.161 +  finally show ?thesis by simp
   2.162 +qed
   2.163 +
   2.164 +lemma rat_add_code [code]: "Rat x + Rat y = Rat (x +\<^sub>N y)"
   2.165 +  unfolding Rat_def by simp
   2.166 +
   2.167 +lemma rat_mul_code [code]: "Rat x * Rat y = Rat (x *\<^sub>N y)"
   2.168 +  unfolding Rat_def by simp
   2.169 +
   2.170 +lemma rat_neg_code [code]: "- Rat x = Rat (~\<^sub>N x)"
   2.171 +  unfolding Rat_def by simp
   2.172 +
   2.173 +lemma rat_sub_code [code]: "Rat x - Rat y = Rat (x -\<^sub>N y)"
   2.174 +  unfolding Rat_def by simp
   2.175 +
   2.176 +lemma rat_inv_code [code]: "inverse (Rat x) = Rat (Ninv x)"
   2.177 +  unfolding Rat_def Ninv divide_rat_def by simp
   2.178 +
   2.179 +lemma rat_div_code [code]: "Rat x / Rat y = Rat (x \<div>\<^sub>N y)"
   2.180 +  unfolding Rat_def by simp
   2.181  
   2.182  code_modulename SML
   2.183    Executable_Rat Rational
   2.184 @@ -114,37 +102,4 @@
   2.185  code_modulename Haskell
   2.186    Executable_Rat Rational
   2.187  
   2.188 -subsubsection {* rat as abstype *}
   2.189 -
   2.190 -code_const div_zero
   2.191 -  (SML "raise/ Fail/ \"Division by zero\"")
   2.192 -  (OCaml "failwith \"Division by zero\"")
   2.193 -  (Haskell "error/ \"Division by zero\"")
   2.194 -
   2.195 -code_abstype rat erat where
   2.196 -  Fract \<equiv> erat_of_quotient
   2.197 -  "0 \<Colon> rat" \<equiv> "0 \<Colon> erat"
   2.198 -  "1 \<Colon> rat" \<equiv> "1 \<Colon> erat"
   2.199 -  "op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
   2.200 -  "uminus \<Colon> rat \<Rightarrow> rat" \<equiv> "uminus \<Colon> erat \<Rightarrow> erat"
   2.201 -  "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
   2.202 -  "inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"
   2.203 -  "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv>  "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
   2.204 -  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
   2.205 -
   2.206 -types_code
   2.207 -  rat ("{*erat*}")
   2.208 -
   2.209 -consts_code
   2.210 -  div_zero ("(raise/ (Fail/ \"Division by zero\"))")
   2.211 -  Fract ("({*erat_of_quotient*} (_) (_))")
   2.212 -  "0 \<Colon> rat" ("({*Rat True 0 1*})")
   2.213 -  "1 \<Colon> rat" ("({*Rat True 1 1*})")
   2.214 -  "plus \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
   2.215 -  "uminus \<Colon> rat \<Rightarrow> rat" ("({*uminus \<Colon> erat \<Rightarrow> erat*} (_))")
   2.216 -  "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" ("({*op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat*} (_) (_))")
   2.217 -  "inverse \<Colon> rat \<Rightarrow> rat" ("({*inverse \<Colon> erat \<Rightarrow> erat*} (_))")
   2.218 -  "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
   2.219 -  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" ("({*op = \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool*} (_) (_))")
   2.220 -
   2.221  end
     3.1 --- a/src/HOL/Library/Executable_Real.thy	Thu Aug 09 15:52:47 2007 +0200
     3.2 +++ b/src/HOL/Library/Executable_Real.thy	Thu Aug 09 15:52:49 2007 +0200
     3.3 @@ -1,472 +1,81 @@
     3.4  (*  Title:      HOL/Library/Executable_Real.thy
     3.5      ID:         $Id$
     3.6 -    Author:     Amine Chaieb, TU Muenchen
     3.7 +    Author:     Florian Haftmann, TU Muenchen
     3.8  *)
     3.9  
    3.10  header {* Implementation of rational real numbers as pairs of integers *}
    3.11  
    3.12  theory Executable_Real
    3.13 -imports GCD "~~/src/HOL/Real/Real"
    3.14 +imports Abstract_Rat "~~/src/HOL/Real/Real"
    3.15  begin
    3.16  
    3.17 -subsection {* Implementation of operations on pair of integers *}
    3.18 -
    3.19 -types Num = "int * int"
    3.20 -syntax "_Num0" :: "Num" ("0\<^sub>N")
    3.21 -translations "0\<^sub>N" \<rightleftharpoons> "(0,0)"
    3.22 -syntax "_Numi" :: "int \<Rightarrow> Num" ("_\<^sub>N")
    3.23 -translations "i\<^sub>N" \<rightleftharpoons> "(i,1)::Num"
    3.24 -
    3.25 -constdefs isnormNum :: "Num \<Rightarrow> bool"
    3.26 -  "isnormNum \<equiv> \<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> igcd a b = 1)"
    3.27 -
    3.28 -constdefs normNum :: "Num \<Rightarrow> Num"
    3.29 -  "normNum \<equiv> \<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else 
    3.30 -  (let g = igcd a b 
    3.31 -   in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g))))"
    3.32 -
    3.33 -lemma normNum_isnormNum[simp]: "isnormNum (normNum x)"
    3.34 -proof-
    3.35 -  have " \<exists> a b. x = (a,b)" by auto
    3.36 -  then obtain a b where x[simp]: "x = (a,b)" by blast
    3.37 -  {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}  
    3.38 -  moreover
    3.39 -  {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0" 
    3.40 -    let ?g = "igcd a b"
    3.41 -    let ?a' = "a div ?g"
    3.42 -    let ?b' = "b div ?g"
    3.43 -    let ?g' = "igcd ?a' ?b'"
    3.44 -    from anz bnz have "?g \<noteq> 0" by simp  with igcd_pos[of a b] 
    3.45 -    have gpos: "?g > 0"  by arith
    3.46 -    have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2)
    3.47 -    from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
    3.48 -    anz bnz
    3.49 -    have nz':"?a' \<noteq> 0" "?b' \<noteq> 0" 
    3.50 -      by - (rule notI,simp add:igcd_def)+
    3.51 -    from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by blast
    3.52 -    from div_igcd_relprime[OF stupid] have gp1: "?g' = 1" .
    3.53 -    from bnz have "b < 0 \<or> b > 0" by arith
    3.54 -    moreover
    3.55 -    {assume b: "b > 0"
    3.56 -      from pos_imp_zdiv_nonneg_iff[OF gpos] b
    3.57 -      have "?b' \<ge> 0" by simp
    3.58 -      with nz' have b': "?b' > 0" by simp
    3.59 -      from b b' anz bnz nz' gp1 have ?thesis 
    3.60 -	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    3.61 -    moreover {assume b: "b < 0"
    3.62 -      {assume b': "?b' \<ge> 0" 
    3.63 -	from gpos have th: "?g \<ge> 0" by arith
    3.64 -	from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
    3.65 -	have False using b by simp }
    3.66 -      hence b': "?b' < 0" by (auto simp add: linorder_not_le[symmetric])
    3.67 -      from anz bnz nz' b b' gp1 have ?thesis 
    3.68 -	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    3.69 -    ultimately have ?thesis by blast
    3.70 -  }
    3.71 -  ultimately show ?thesis by blast
    3.72 -qed
    3.73 -    (* Arithmetic over Num *)
    3.74 -constdefs Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "+\<^sub>N" 60)
    3.75 -  "Nadd \<equiv> \<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 -constdefs Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
    3.79 -  "Nmul \<equiv> \<lambda>(a,b) (a',b'). let g = igcd (a*a') (b*b') 
    3.80 -  in (a*a' div g, b*b' div g)"
    3.81 -constdefs Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N")
    3.82 -  "Nneg \<equiv> \<lambda>(a,b). (-a,b)"
    3.83 -constdefs  Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "-\<^sub>N" 60)
    3.84 -  "Nsub \<equiv> \<lambda>a b. a +\<^sub>N ~\<^sub>N b"
    3.85 -constdefs Ninv :: "Num \<Rightarrow> Num" 
    3.86 -"Ninv \<equiv> \<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a)"
    3.87 -constdefs Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "\<div>\<^sub>N" 60)
    3.88 -  "Ndiv \<equiv> \<lambda>a b. a *\<^sub>N Ninv b"
    3.89 -
    3.90 -lemma Nneg_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (~\<^sub>N x)"
    3.91 -  by(simp add: isnormNum_def Nneg_def split_def)
    3.92 -lemma Nadd_normN[simp]: "isnormNum (x +\<^sub>N y)"
    3.93 -  by (simp add: Nadd_def split_def)
    3.94 -lemma Nsub_normN[simp]: "\<lbrakk> isnormNum y\<rbrakk> \<Longrightarrow> isnormNum (x -\<^sub>N y)"
    3.95 -  by (simp add: Nsub_def split_def)
    3.96 -lemma Nmul_normN[simp]: assumes xn:"isnormNum x" and yn: "isnormNum y"
    3.97 -  shows "isnormNum (x *\<^sub>N y)"
    3.98 -proof-
    3.99 -  have "\<exists>a b. x = (a,b)" and "\<exists> a' b'. y = (a',b')" by auto
   3.100 -  then obtain a b a' b' where ab: "x = (a,b)"  and ab': "y = (a',b')" by blast 
   3.101 -  {assume "a = 0"
   3.102 -    hence ?thesis using xn ab ab'
   3.103 -      by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
   3.104 -  moreover
   3.105 -  {assume "a' = 0"
   3.106 -    hence ?thesis using yn ab ab' 
   3.107 -      by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
   3.108 -  moreover
   3.109 -  {assume a: "a \<noteq>0" and a': "a'\<noteq>0"
   3.110 -    hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def)
   3.111 -    from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a*a', b*b')" 
   3.112 -      using ab ab' a a' bp by (simp add: Nmul_def Let_def split_def normNum_def)
   3.113 -    hence ?thesis by simp}
   3.114 -  ultimately show ?thesis by blast
   3.115 -qed
   3.116 -
   3.117 -lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
   3.118 -by (simp add: Ninv_def isnormNum_def split_def)
   3.119 -(cases "fst x = 0",auto simp add: igcd_commute)
   3.120 -
   3.121 -lemma isnormNum_int[simp]: 
   3.122 -  "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
   3.123 - by (simp_all add: isnormNum_def igcd_def)
   3.124 -
   3.125 -    (* Relations over Num *)
   3.126 -constdefs Nlt0:: "Num \<Rightarrow> bool" ("0>\<^sub>N")
   3.127 -  "Nlt0 \<equiv> \<lambda>(a,b). a < 0"
   3.128 -constdefs Nle0:: "Num \<Rightarrow> bool" ("0\<ge>\<^sub>N")
   3.129 -  "Nle0 \<equiv> \<lambda>(a,b). a \<le> 0"
   3.130 -constdefs Ngt0:: "Num \<Rightarrow> bool" ("0<\<^sub>N")
   3.131 -  "Ngt0 \<equiv> \<lambda>(a,b). a > 0"
   3.132 -constdefs Nge0:: "Num \<Rightarrow> bool" ("0\<le>\<^sub>N")
   3.133 -  "Nge0 \<equiv> \<lambda>(a,b). a \<ge> 0"
   3.134 -constdefs Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "<\<^sub>N" 55)
   3.135 -  "Nlt \<equiv> \<lambda>a b. 0>\<^sub>N (a -\<^sub>N b)"
   3.136 -constdefs Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "\<le>\<^sub>N" 55)
   3.137 -  "Nle \<equiv> \<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b)"
   3.138 -
   3.139 -
   3.140 -subsection {* Interpretation of the normalized rats in reals *}
   3.141 +hide (open) const Real
   3.142  
   3.143  definition
   3.144 -  INum:: "Num \<Rightarrow> real"
   3.145 +  Real :: "int \<times> int \<Rightarrow> real"
   3.146  where
   3.147 -  INum_def: "INum \<equiv> \<lambda>(a,b). real a / real b"
   3.148 +  "Real = INum"
   3.149 +
   3.150 +code_datatype Real
   3.151 +
   3.152 +lemma Real_simp:
   3.153 +  "Real (k, l) = real_of_int k / real_of_int l"
   3.154 +  unfolding Real_def INum_def by simp
   3.155 +
   3.156 +lemma Real_zero [simp]: "Real 0\<^sub>N = 0"
   3.157 +  by (simp add: Real_simp)
   3.158  
   3.159 -code_datatype INum
   3.160 +lemma Real_lit [simp]: "Real i\<^sub>N = real_of_int i"
   3.161 +  by (simp add: Real_simp)
   3.162 +
   3.163 +lemma zero_real_code [code]:
   3.164 +  "0 = Real 0\<^sub>N" by simp
   3.165 +
   3.166 +lemma zero_real_code [code]:
   3.167 +  "1 = Real 1\<^sub>N" by simp
   3.168 +
   3.169 +lemma [code, code unfold]:
   3.170 +  "number_of k = real_of_int (number_of k)"
   3.171 +  by (simp add: number_of_is_id real_number_of_def)
   3.172 +
   3.173  instance real :: eq ..
   3.174  
   3.175 -definition
   3.176 -  real_int :: "int \<Rightarrow> real"
   3.177 -where
   3.178 -  "real_int = real"
   3.179 -lemmas [code unfold] = real_int_def [symmetric]
   3.180 -
   3.181 -lemma [code unfold]:
   3.182 -  "real = real_int o int"
   3.183 -  by (auto simp add: real_int_def expand_fun_eq)
   3.184 -
   3.185 -lemma INum_int [simp]: "INum i\<^sub>N = real i" "INum 0\<^sub>N = 0"
   3.186 -  by (simp_all add: INum_def)
   3.187 -lemmas [code, code unfold] = INum_int [unfolded real_int_def [symmetric], symmetric]
   3.188 -
   3.189 -lemma [code, code unfold]: "1 = INum 1\<^sub>N" by simp
   3.190 +lemma real_eq_code [code]: "Real x = Real y \<longleftrightarrow> normNum x = normNum y"
   3.191 +  unfolding Real_def INum_normNum_iff ..
   3.192  
   3.193 -lemma isnormNum_unique[simp]: 
   3.194 -  assumes na: "isnormNum x" and nb: "isnormNum y" 
   3.195 -  shows "(INum x = INum y) = (x = y)" (is "?lhs = ?rhs")
   3.196 -proof
   3.197 -  have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
   3.198 -  then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
   3.199 -  assume H: ?lhs 
   3.200 -  {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" hence ?rhs
   3.201 -      using na nb H
   3.202 -      by (simp add: INum_def split_def isnormNum_def)
   3.203 -       (cases "a = 0", simp_all,cases "b = 0", simp_all,
   3.204 -      cases "a' = 0", simp_all,cases "a' = 0", simp_all)}
   3.205 -  moreover
   3.206 -  { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
   3.207 -    from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
   3.208 -    from prems have eq:"a * b' = a'*b" 
   3.209 -      by (simp add: INum_def  eq_divide_eq divide_eq_eq real_of_int_mult[symmetric] del: real_of_int_mult)
   3.210 -    from prems have gcd1: "igcd a b = 1" "igcd b a = 1" "igcd a' b' = 1" "igcd b' a' = 1"       
   3.211 -      by (simp_all add: isnormNum_def add: igcd_commute)
   3.212 -    from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'" 
   3.213 -      apply(unfold dvd_def)
   3.214 -      apply (rule_tac x="b'" in exI, simp add: mult_ac)
   3.215 -      apply (rule_tac x="a'" in exI, simp add: mult_ac)
   3.216 -      apply (rule_tac x="b" in exI, simp add: mult_ac)
   3.217 -      apply (rule_tac x="a" in exI, simp add: mult_ac)
   3.218 -      done
   3.219 -    from zdvd_dvd_eq[OF bz zrelprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
   3.220 -      zrelprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
   3.221 -      have eq1: "b = b'" using pos by simp_all
   3.222 -      with eq have "a = a'" using pos by simp
   3.223 -      with eq1 have ?rhs by simp}
   3.224 -  ultimately show ?rhs by blast
   3.225 -next
   3.226 -  assume ?rhs thus ?lhs by simp
   3.227 -qed
   3.228 -
   3.229 -
   3.230 -lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = 0) = (x = 0\<^sub>N)"
   3.231 -  unfolding INum_int(2)[symmetric]
   3.232 -  by (rule isnormNum_unique, simp_all)
   3.233 -
   3.234 -lemma normNum[simp]: "INum (normNum x) = INum x"
   3.235 -proof-
   3.236 -  have "\<exists> a b. x = (a,b)" by auto
   3.237 -  then obtain a b where x[simp]: "x = (a,b)" by blast
   3.238 -  {assume "a=0 \<or> b = 0" hence ?thesis
   3.239 -      by (simp add: INum_def normNum_def split_def Let_def)}
   3.240 -  moreover 
   3.241 -  {assume a: "a\<noteq>0" and b: "b\<noteq>0"
   3.242 -    let ?g = "igcd a b"
   3.243 -    from a b have g: "?g \<noteq> 0"by simp
   3.244 -    from real_of_int_div[OF g]
   3.245 -    have ?thesis by (simp add: INum_def normNum_def split_def Let_def)}
   3.246 -  ultimately show ?thesis by blast
   3.247 -qed
   3.248 -
   3.249 -lemma INum_normNum_iff [code]: "INum x = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
   3.250 +lemma real_less_eq_code [code]: "Real x \<le> Real y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
   3.251  proof -
   3.252 -  have "normNum x = normNum y \<longleftrightarrow> INum (normNum x) = INum (normNum y)"
   3.253 -    by (simp del: normNum)
   3.254 -  also have "\<dots> = ?lhs" by simp
   3.255 +  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> Real (normNum x) \<le> Real (normNum y)" 
   3.256 +    by (simp add: Real_def del: normNum)
   3.257 +  also have "\<dots> = (Real x \<le> Real y)" by (simp add: Real_def)
   3.258    finally show ?thesis by simp
   3.259  qed
   3.260  
   3.261 -lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + INum y"
   3.262 -proof-
   3.263 -  have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
   3.264 -  then obtain a b a' b' where x[simp]: "x = (a,b)" 
   3.265 -    and y[simp]: "y = (a',b')" by blast
   3.266 -  {assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0" hence ?thesis 
   3.267 -      apply (cases "a=0",simp_all add: Nadd_def)
   3.268 -      apply (cases "b= 0",simp_all add: INum_def)
   3.269 -       apply (cases "a'= 0",simp_all)
   3.270 -       apply (cases "b'= 0",simp_all)
   3.271 -       done }
   3.272 -  moreover 
   3.273 -  {assume aa':"a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0" 
   3.274 -    {assume z: "a * b' + b * a' = 0"
   3.275 -      hence "real (a*b' + b*a') / (real b* real b') = 0" by simp
   3.276 -      hence "real b' * real a / (real b * real b') + real b * real a' / (real b * real b') = 0"  by (simp add:add_divide_distrib) 
   3.277 -      hence th: "real a / real b + real a' / real b' = 0" using bb' aa' by simp 
   3.278 -      from z aa' bb' have ?thesis 
   3.279 -	by (simp add: th Nadd_def normNum_def INum_def split_def)}
   3.280 -    moreover {assume z: "a * b' + b * a' \<noteq> 0"
   3.281 -      let ?g = "igcd (a * b' + b * a') (b*b')"
   3.282 -      have gz: "?g \<noteq> 0" using z by simp
   3.283 -      have ?thesis using aa' bb' z gz
   3.284 -	real_of_int_div[OF gz igcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
   3.285 -	real_of_int_div[OF gz igcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
   3.286 -	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
   3.287 -    ultimately have ?thesis using aa' bb' 
   3.288 -      by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
   3.289 -  ultimately show ?thesis by blast
   3.290 -qed
   3.291 -lemmas [code] = Nadd [symmetric]
   3.292 -
   3.293 -lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * INum y"
   3.294 -proof-
   3.295 -  have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
   3.296 -  then obtain a b a' b' where x: "x = (a,b)" and y: "y = (a',b')" by blast
   3.297 -  {assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0" hence ?thesis 
   3.298 -      apply (cases "a=0",simp_all add: x y Nmul_def INum_def Let_def)
   3.299 -      apply (cases "b=0",simp_all)
   3.300 -      apply (cases "a'=0",simp_all) 
   3.301 -      done }
   3.302 -  moreover
   3.303 -  {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
   3.304 -    let ?g="igcd (a*a') (b*b')"
   3.305 -    have gz: "?g \<noteq> 0" using z by simp
   3.306 -    from z real_of_int_div[OF gz igcd_dvd1[where i="a*a'" and j="b*b'"]] 
   3.307 -      real_of_int_div[OF gz igcd_dvd2[where i="a*a'" and j="b*b'"]] 
   3.308 -    have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
   3.309 -  ultimately show ?thesis by blast
   3.310 -qed
   3.311 -lemmas [code] = Nmul [symmetric]
   3.312 -
   3.313 -lemma Nneg[simp]: "INum (~\<^sub>N x) = - INum x"
   3.314 -  by (simp add: Nneg_def split_def INum_def)
   3.315 -lemmas [code] = Nneg [symmetric]
   3.316 -
   3.317 -lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - INum y"
   3.318 -  by (simp add: Nsub_def split_def)
   3.319 -lemmas [code] = Nsub [symmetric]
   3.320 -
   3.321 -lemma Ninv[simp]: "INum (Ninv x) = 1 / (INum x)"
   3.322 -  by (simp add: Ninv_def INum_def split_def)
   3.323 -lemmas [code] = Ninv [symmetric]
   3.324 -
   3.325 -lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / INum y" by (simp add: Ndiv_def)
   3.326 -lemmas [code] = Ndiv [symmetric]
   3.327 -
   3.328 -lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" shows "(INum x < 0) = 0>\<^sub>N x "
   3.329 -proof-
   3.330 -  have " \<exists> a b. x = (a,b)" by simp
   3.331 -  then obtain a b where x[simp]:"x = (a,b)" by blast
   3.332 -  {assume "a = 0" hence ?thesis by (simp add: Nlt0_def INum_def) }
   3.333 -  moreover
   3.334 -  {assume a: "a\<noteq>0" hence b: "real b > 0" using nx by (simp add: isnormNum_def)
   3.335 -    from pos_divide_less_eq[OF b, where b="real a" and a="0"]
   3.336 -    have ?thesis by (simp add: Nlt0_def INum_def)}
   3.337 -  ultimately show ?thesis by blast
   3.338 -qed
   3.339 -
   3.340 -lemma   Nle0_iff[simp]:assumes nx: "isnormNum x" shows "(INum x \<le> 0) = 0\<ge>\<^sub>N x"
   3.341 -proof-
   3.342 -  have " \<exists> a b. x = (a,b)" by simp
   3.343 -  then obtain a b where x[simp]:"x = (a,b)" by blast
   3.344 -  {assume "a = 0" hence ?thesis by (simp add: Nle0_def INum_def) }
   3.345 -  moreover
   3.346 -  {assume a: "a\<noteq>0" hence b: "real b > 0" using nx by (simp add: isnormNum_def)
   3.347 -    from pos_divide_le_eq[OF b, where b="real a" and a="0"]
   3.348 -    have ?thesis by (simp add: Nle0_def INum_def)}
   3.349 -  ultimately show ?thesis by blast
   3.350 -qed
   3.351 -
   3.352 -lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "(INum x > 0) = 0<\<^sub>N x"
   3.353 -proof-
   3.354 -  have " \<exists> a b. x = (a,b)" by simp
   3.355 -  then obtain a b where x[simp]:"x = (a,b)" by blast
   3.356 -  {assume "a = 0" hence ?thesis by (simp add: Ngt0_def INum_def) }
   3.357 -  moreover
   3.358 -  {assume a: "a\<noteq>0" hence b: "real b > 0" using nx by (simp add: isnormNum_def)
   3.359 -    from pos_less_divide_eq[OF b, where b="real a" and a="0"]
   3.360 -    have ?thesis by (simp add: Ngt0_def INum_def)}
   3.361 -  ultimately show ?thesis by blast
   3.362 -qed
   3.363 -lemma Nge0_iff[simp]:assumes nx: "isnormNum x" shows "(INum x \<ge> 0) = 0\<le>\<^sub>N x"
   3.364 -proof-
   3.365 -  have " \<exists> a b. x = (a,b)" by simp
   3.366 -  then obtain a b where x[simp]:"x = (a,b)" by blast
   3.367 -  {assume "a = 0" hence ?thesis by (simp add: Nge0_def INum_def) }
   3.368 -  moreover
   3.369 -  {assume a: "a\<noteq>0" hence b: "real b > 0" using nx by (simp add: isnormNum_def)
   3.370 -    from pos_le_divide_eq[OF b, where b="real a" and a="0"]
   3.371 -    have ?thesis by (simp add: Nge0_def INum_def)}
   3.372 -  ultimately show ?thesis by blast
   3.373 -qed
   3.374 -
   3.375 -lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
   3.376 -  shows "(INum x < INum y) = (x <\<^sub>N y)"
   3.377 -proof-
   3.378 -  have "(INum x < INum y) = (INum (x -\<^sub>N y) < 0)" using nx ny by simp
   3.379 -  also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))" using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
   3.380 -  finally show ?thesis by (simp add: Nlt_def)
   3.381 -qed
   3.382 -
   3.383 -lemma [code]: "INum x < INum y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
   3.384 +lemma real_less_code [code]: "Real x < Real y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
   3.385  proof -
   3.386 -  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> INum (normNum x) < INum (normNum y)" 
   3.387 -    by (simp del: normNum)
   3.388 -  also have "\<dots> = (INum x < INum y)" by simp 
   3.389 +  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> Real (normNum x) < Real (normNum y)" 
   3.390 +    by (simp add: Real_def del: normNum)
   3.391 +  also have "\<dots> = (Real x < Real y)" by (simp add: Real_def)
   3.392    finally show ?thesis by simp
   3.393  qed
   3.394  
   3.395 -lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
   3.396 -  shows "(INum x \<le> INum y) = (x \<le>\<^sub>N y)"
   3.397 -proof-
   3.398 -  have "(INum x \<le> INum y) = (INum (x -\<^sub>N y) \<le> 0)" using nx ny by simp
   3.399 -  also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp
   3.400 -  finally show ?thesis by (simp add: Nle_def)
   3.401 -qed
   3.402 -
   3.403 -lemma [code]: "INum x \<le> INum y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
   3.404 -proof -
   3.405 -  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> INum (normNum x) \<le> INum (normNum y)" 
   3.406 -    by (simp del: normNum)
   3.407 -  also have "\<dots> = (INum x \<le> INum y)" by simp 
   3.408 -  finally show ?thesis by simp
   3.409 -qed
   3.410 +lemma real_add_code [code]: "Real x + Real y = Real (x +\<^sub>N y)"
   3.411 +  unfolding Real_def by simp
   3.412  
   3.413 -lemma Nadd_commute: "x +\<^sub>N y = y +\<^sub>N x"
   3.414 -proof-
   3.415 -  have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
   3.416 -  have "INum (x +\<^sub>N y) = INum (y +\<^sub>N x)" by simp
   3.417 -  with isnormNum_unique[OF n] show ?thesis by simp
   3.418 -qed
   3.419 +lemma real_mul_code [code]: "Real x * Real y = Real (x *\<^sub>N y)"
   3.420 +  unfolding Real_def by simp
   3.421  
   3.422 -lemma[simp]: "(0, b) +\<^sub>N y = normNum y" "(a, 0) +\<^sub>N y = normNum y" 
   3.423 -  "x +\<^sub>N (0, b) = normNum x" "x +\<^sub>N (a, 0) = normNum x"
   3.424 -  apply (simp add: Nadd_def split_def, simp add: Nadd_def split_def)
   3.425 -  apply (subst Nadd_commute,simp add: Nadd_def split_def)
   3.426 -  apply (subst Nadd_commute,simp add: Nadd_def split_def)
   3.427 -  done
   3.428 -
   3.429 -lemma normNum_nilpotent_aux[simp]: assumes nx: "isnormNum x" 
   3.430 -  shows "normNum x = x"
   3.431 -proof-
   3.432 -  let ?a = "normNum x"
   3.433 -  have n: "isnormNum ?a" by simp
   3.434 -  have th:"INum ?a = INum x" by simp
   3.435 -  with isnormNum_unique[OF n nx]  
   3.436 -  show ?thesis by simp
   3.437 -qed
   3.438 +lemma real_neg_code [code]: "- Real x = Real (~\<^sub>N x)"
   3.439 +  unfolding Real_def by simp
   3.440  
   3.441 -lemma normNum_nilpotent[simp]: "normNum (normNum x) = normNum x"
   3.442 -  by simp
   3.443 -lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N"
   3.444 -  by (simp_all add: normNum_def)
   3.445 -lemma normNum_Nadd: "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
   3.446 -lemma Nadd_normNum1[simp]: "normNum x +\<^sub>N y = x +\<^sub>N y"
   3.447 -proof-
   3.448 -  have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
   3.449 -  have "INum (normNum x +\<^sub>N y) = INum x + INum y" by simp
   3.450 -  also have "\<dots> = INum (x +\<^sub>N y)" by simp
   3.451 -  finally show ?thesis using isnormNum_unique[OF n] by simp
   3.452 -qed
   3.453 -lemma Nadd_normNum2[simp]: "x +\<^sub>N normNum y = x +\<^sub>N y"
   3.454 -proof-
   3.455 -  have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
   3.456 -  have "INum (x +\<^sub>N normNum y) = INum x + INum y" by simp
   3.457 -  also have "\<dots> = INum (x +\<^sub>N y)" by simp
   3.458 -  finally show ?thesis using isnormNum_unique[OF n] by simp
   3.459 -qed
   3.460 -
   3.461 -lemma Nadd_assoc: "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))" 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 igcd_commute mult_commute)
   3.470 +lemma real_sub_code [code]: "Real x - Real y = Real (x -\<^sub>N y)"
   3.471 +  unfolding Real_def by simp
   3.472  
   3.473 -lemma Nmul_assoc: 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))" by simp
   3.479 -  with isnormNum_unique[OF n] show ?thesis by simp
   3.480 -qed
   3.481 -
   3.482 -lemma Nsub0: assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
   3.483 -proof-
   3.484 -  from isnormNum_unique[OF Nsub_normN[OF y], where y="0\<^sub>N"] 
   3.485 -  have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = INum 0\<^sub>N)" by simp
   3.486 -  also have "\<dots> = (INum x = INum y)" by simp
   3.487 -  also have "\<dots> = (x = y)" using x y by simp
   3.488 -  finally show ?thesis .
   3.489 -qed
   3.490 -lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N"
   3.491 -  by (simp_all add: Nmul_def Let_def split_def)
   3.492 +lemma real_inv_code [code]: "inverse (Real x) = Real (Ninv x)"
   3.493 +  unfolding Real_def Ninv real_divide_def by simp
   3.494  
   3.495 -lemma Nmul_eq0[simp]: assumes nx:"isnormNum x" and ny: "isnormNum y"
   3.496 -  shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)"
   3.497 -proof-
   3.498 -  have " \<exists> a b a' b'. x = (a,b) \<and> y= (a',b')" by auto
   3.499 -  then obtain a b a' b' where xy[simp]: "x = (a,b)" "y = (a',b')" by blast
   3.500 -  have n0: "isnormNum 0\<^sub>N" by simp
   3.501 -  show ?thesis using nx ny 
   3.502 -    apply (simp only: isnormNum_unique[OF  Nmul_normN[OF nx ny] n0, symmetric] Nmul)
   3.503 -    apply (simp add: INum_def split_def isnormNum_def fst_conv snd_conv)
   3.504 -    apply (cases "a=0",simp_all)
   3.505 -    apply (cases "a'=0",simp_all)
   3.506 -    done 
   3.507 -qed
   3.508 -lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
   3.509 -  by (simp add: Nneg_def split_def)
   3.510 -
   3.511 -lemma Nmul1[simp]: 
   3.512 -  "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c" 
   3.513 -  "isnormNum c \<Longrightarrow> c *\<^sub>N 1\<^sub>N  = c" 
   3.514 -  apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
   3.515 -  by (cases "fst c = 0", simp_all,cases c, simp_all)+
   3.516 -
   3.517 -lemma [code, code unfold]:
   3.518 -  "number_of k = real_int (number_of k)"
   3.519 -  by (simp add: real_int_def)
   3.520 +lemma real_div_code [code]: "Real x / Real y = Real (x \<div>\<^sub>N y)"
   3.521 +  unfolding Real_def by simp
   3.522  
   3.523  code_modulename SML
   3.524    RealDef Real
   3.525 @@ -480,19 +89,4 @@
   3.526    RealDef Real
   3.527    Executable_Real Real
   3.528  
   3.529 -(* There is already an implementation in RealDef
   3.530 -types_code real ("{* int * int *}")
   3.531 -attach (term_of) {*
   3.532 -fun term_of_real (p, q) =
   3.533 -  let 
   3.534 -    val rT = HOLogic.realT;
   3.535 -in if q = 1
   3.536 -  then HOLogic.mk_number rT p
   3.537 -  else @{term "op / \<Colon> real \<Rightarrow> real \<Rightarrow> real"} $
   3.538 -    HOLogic.mk_number rT p $ HOLogic.mk_number rT q
   3.539 -end;
   3.540 -*}
   3.541 -
   3.542 -consts_code INum ("")
   3.543 -*)
   3.544  end
     4.1 --- a/src/HOL/Library/Library.thy	Thu Aug 09 15:52:47 2007 +0200
     4.2 +++ b/src/HOL/Library/Library.thy	Thu Aug 09 15:52:49 2007 +0200
     4.3 @@ -2,6 +2,7 @@
     4.4  (*<*)
     4.5  theory Library
     4.6  imports
     4.7 +  Abstract_Rat
     4.8    AssocList
     4.9    BigO
    4.10    Binomial
     5.1 --- a/src/HOL/ex/ExecutableContent.thy	Thu Aug 09 15:52:47 2007 +0200
     5.2 +++ b/src/HOL/ex/ExecutableContent.thy	Thu Aug 09 15:52:49 2007 +0200
     5.3 @@ -1,4 +1,3 @@
     5.4 -
     5.5  (*  ID:         $Id$
     5.6      Author:     Florian Haftmann, TU Muenchen
     5.7  *)
     5.8 @@ -14,6 +13,7 @@
     5.9    Binomial
    5.10    Commutative_Ring
    5.11    "~~/src/HOL/ex/Commutative_Ring_Complete"
    5.12 +  Executable_Rat
    5.13    Executable_Real
    5.14    GCD
    5.15    List_Prefix
    5.16 @@ -79,4 +79,44 @@
    5.17  definition
    5.18    "shadow keywords = keywords @ [ExecutableContent.keywords 0 0 0 0 0 0]"
    5.19  
    5.20 +definition
    5.21 +  foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where
    5.22 +  "foo r s t = (t + s) / t"
    5.23 +
    5.24 +definition
    5.25 +  bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where
    5.26 +  "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
    5.27 +
    5.28 +definition
    5.29 +  "R1 = Fract 3 7"
    5.30 +
    5.31 +definition
    5.32 +  "R2 = Fract (-7) 5"
    5.33 +
    5.34 +definition
    5.35 +  "R3 = Fract 11 (-9)"
    5.36 +
    5.37 +definition
    5.38 +  "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
    5.39 +
    5.40 +definition
    5.41 +  foo' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
    5.42 +  "foo' r s t = (t + s) / t"
    5.43 +
    5.44 +definition
    5.45 +  bar' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" where
    5.46 +  "bar' r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
    5.47 +
    5.48 +definition
    5.49 +  "R1' = real_of_rat (Fract 3 7)"
    5.50 +
    5.51 +definition
    5.52 +  "R2' = real_of_rat (Fract (-7) 5)"
    5.53 +
    5.54 +definition
    5.55 +  "R3' = real_of_rat (Fract 11 (-9))"
    5.56 +
    5.57 +definition
    5.58 +  "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
    5.59 +
    5.60  end