A verified theory for rational numbers representation and simple calculations;
authorchaieb
Tue May 15 18:28:02 2007 +0200 (2007-05-15)
changeset 22981cf071f3fc4ae
parent 22980 1226d861eefb
child 22982 bff3fcdeecd3
A verified theory for rational numbers representation and simple calculations;
verified with respect to the real numbers;
src/HOL/IsaMakefile
src/HOL/Library/Executable_Real.thy
src/HOL/Library/Library.thy
src/HOL/ex/ExecutableContent.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue May 15 18:20:07 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue May 15 18:28:02 2007 +0200
     1.3 @@ -196,6 +196,7 @@
     1.4  $(LOG)/HOL-Library.gz: $(OUT)/HOL \
     1.5    Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
     1.6    Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
     1.7 +  Library/Executable_Real.thy \
     1.8    Library/MLString.thy Library/Infinite_Set.thy \
     1.9    Library/FuncSet.thy Library/Library.thy \
    1.10    Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy Library/NatPair.thy \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Executable_Real.thy	Tue May 15 18:28:02 2007 +0200
     2.3 @@ -0,0 +1,484 @@
     2.4 +(*  Title:      HOL/Library/Executable_Real.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Amine Chaieb, TU Muenchen
     2.7 +*)
     2.8 +
     2.9 +header {* Implementation of rational real numbers as pairs of integers *}
    2.10 +
    2.11 +theory Executable_Real
    2.12 +imports GCD "~~/src/HOL/Real/Real"
    2.13 +begin
    2.14 +
    2.15 +subsection {* Implementation of operations on pair of integers *}
    2.16 +
    2.17 +types Num = "int * int"
    2.18 +syntax "_Num0" :: "Num" ("0\<^sub>N")
    2.19 +translations "0\<^sub>N" \<rightleftharpoons> "(0,0)"
    2.20 +syntax "_Numi" :: "int \<Rightarrow> Num" ("_\<^sub>N")
    2.21 +translations "i\<^sub>N" \<rightleftharpoons> "(i,1)::Num"
    2.22 +
    2.23 +constdefs isnormNum :: "Num \<Rightarrow> bool"
    2.24 +  "isnormNum \<equiv> \<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> igcd a b = 1)"
    2.25 +
    2.26 +constdefs normNum :: "Num \<Rightarrow> Num"
    2.27 +  "normNum \<equiv> \<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else 
    2.28 +  (let g = igcd a b 
    2.29 +   in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g))))"
    2.30 +lemma normNum_isnormNum[simp]: "isnormNum (normNum x)"
    2.31 +proof-
    2.32 +  have " \<exists> a b. x = (a,b)" by auto
    2.33 +  then obtain a b where x[simp]: "x = (a,b)" by blast
    2.34 +  {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}  
    2.35 +  moreover
    2.36 +  {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0" 
    2.37 +    let ?g = "igcd a b"
    2.38 +    let ?a' = "a div ?g"
    2.39 +    let ?b' = "b div ?g"
    2.40 +    let ?g' = "igcd ?a' ?b'"
    2.41 +    from anz bnz have "?g \<noteq> 0" by simp  with igcd_pos[of a b] 
    2.42 +    have gpos: "?g > 0"  by arith
    2.43 +    have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2)
    2.44 +    from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
    2.45 +    anz bnz
    2.46 +    have nz':"?a' \<noteq> 0" "?b' \<noteq> 0" 
    2.47 +      by - (rule notI,simp add:igcd_def)+
    2.48 +    from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by blast
    2.49 +    from div_igcd_relprime[OF stupid] have gp1: "?g' = 1" .
    2.50 +    from bnz have "b < 0 \<or> b > 0" by arith
    2.51 +    moreover
    2.52 +    {assume b: "b > 0"
    2.53 +      from pos_imp_zdiv_nonneg_iff[OF gpos] b
    2.54 +      have "?b' \<ge> 0" by simp
    2.55 +      with nz' have b': "?b' > 0" by simp
    2.56 +      from b b' anz bnz nz' gp1 have ?thesis 
    2.57 +	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    2.58 +    moreover {assume b: "b < 0"
    2.59 +      {assume b': "?b' \<ge> 0" 
    2.60 +	from gpos have th: "?g \<ge> 0" by arith
    2.61 +	from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
    2.62 +	have False using b by simp }
    2.63 +      hence b': "?b' < 0" by arith
    2.64 +      from anz bnz nz' b b' gp1 have ?thesis 
    2.65 +	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
    2.66 +    ultimately have ?thesis by blast
    2.67 +  }
    2.68 +  ultimately show ?thesis by blast
    2.69 +qed
    2.70 +    (* Arithmetic over Num *)
    2.71 +constdefs Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "+\<^sub>N" 60)
    2.72 +  "Nadd \<equiv> \<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b') 
    2.73 +  else if a'=0 \<or> b' = 0 then normNum(a,b) 
    2.74 +  else normNum(a*b' + b*a', b*b')"
    2.75 +constdefs Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
    2.76 +  "Nmul \<equiv> \<lambda>(a,b) (a',b'). let g = igcd (a*a') (b*b') 
    2.77 +  in (a*a' div g, b*b' div g)"
    2.78 +constdefs Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N")
    2.79 +  "Nneg \<equiv> \<lambda>(a,b). (-a,b)"
    2.80 +constdefs  Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "-\<^sub>N" 60)
    2.81 +  "Nsub \<equiv> \<lambda>a b. a +\<^sub>N ~\<^sub>N b"
    2.82 +constdefs Ninv :: "Num \<Rightarrow> Num" 
    2.83 +"Ninv \<equiv> \<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a)"
    2.84 +constdefs Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "\<div>\<^sub>N" 60)
    2.85 +  "Ndiv \<equiv> \<lambda>a b. a *\<^sub>N Ninv b"
    2.86 +
    2.87 +lemma Nneg_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (~\<^sub>N x)"
    2.88 +  by(simp add: isnormNum_def Nneg_def split_def)
    2.89 +lemma Nadd_normN[simp]: "isnormNum (x +\<^sub>N y)"
    2.90 +  by (simp add: Nadd_def split_def)
    2.91 +lemma Nsub_normN[simp]: "\<lbrakk> isnormNum y\<rbrakk> \<Longrightarrow> isnormNum (x -\<^sub>N y)"
    2.92 +  by (simp add: Nsub_def split_def)
    2.93 +lemma Nmul_normN[simp]: assumes xn:"isnormNum x" and yn: "isnormNum y"
    2.94 +  shows "isnormNum (x *\<^sub>N y)"
    2.95 +proof-
    2.96 +  have "\<exists>a b. x = (a,b)" and "\<exists> a' b'. y = (a',b')" by auto
    2.97 +  then obtain a b a' b' where ab: "x = (a,b)"  and ab': "y = (a',b')" by blast 
    2.98 +  {assume "a = 0"
    2.99 +    hence ?thesis using xn ab ab'
   2.100 +      by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
   2.101 +  moreover
   2.102 +  {assume "a' = 0"
   2.103 +    hence ?thesis using yn ab ab' 
   2.104 +      by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
   2.105 +  moreover
   2.106 +  {assume a: "a \<noteq>0" and a': "a'\<noteq>0"
   2.107 +    hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def)
   2.108 +    from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a*a', b*b')" 
   2.109 +      using ab ab' a a' bp by (simp add: Nmul_def Let_def split_def normNum_def)
   2.110 +    hence ?thesis by simp}
   2.111 +  ultimately show ?thesis by blast
   2.112 +qed
   2.113 +
   2.114 +lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
   2.115 +by (simp add: Ninv_def isnormNum_def split_def)
   2.116 +(cases "fst x = 0",auto simp add: igcd_commute)
   2.117 +
   2.118 +lemma isnormNum_int[simp]: 
   2.119 +  "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
   2.120 + by (simp_all add: isnormNum_def igcd_def)
   2.121 +
   2.122 +    (* Relations over Num *)
   2.123 +constdefs Nlt0:: "Num \<Rightarrow> bool" ("0>\<^sub>N")
   2.124 +  "Nlt0 \<equiv> \<lambda>(a,b). a < 0"
   2.125 +constdefs Nle0:: "Num \<Rightarrow> bool" ("0\<ge>\<^sub>N")
   2.126 +  "Nle0 \<equiv> \<lambda>(a,b). a \<le> 0"
   2.127 +constdefs Ngt0:: "Num \<Rightarrow> bool" ("0<\<^sub>N")
   2.128 +  "Ngt0 \<equiv> \<lambda>(a,b). a > 0"
   2.129 +constdefs Nge0:: "Num \<Rightarrow> bool" ("0\<le>\<^sub>N")
   2.130 +  "Nge0 \<equiv> \<lambda>(a,b). a \<ge> 0"
   2.131 +constdefs Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "<\<^sub>N" 55)
   2.132 +  "Nlt \<equiv> \<lambda>a b. 0>\<^sub>N (a -\<^sub>N b)"
   2.133 +constdefs Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "\<le>\<^sub>N" 55)
   2.134 +  "Nle \<equiv> \<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b)"
   2.135 +
   2.136 +
   2.137 +subsection {* Interpretation of the normalized rats in \<real> *}
   2.138 +
   2.139 +definition
   2.140 +  INum:: "Num \<Rightarrow> real"
   2.141 +where
   2.142 +  INum_def: "INum \<equiv> \<lambda>(a,b). real a / real b"
   2.143 +
   2.144 +code_datatype INum
   2.145 +instance real :: eq ..
   2.146 +
   2.147 +definition
   2.148 +  real_int :: "int \<Rightarrow> real"
   2.149 +where
   2.150 +  "real_int = real"
   2.151 +lemmas [code unfold] = real_int_def [symmetric]
   2.152 +
   2.153 +lemma [code unfold]:
   2.154 +  "real = real_int o int"
   2.155 +  by (auto simp add: real_int_def expand_fun_eq)
   2.156 +
   2.157 +lemma INum_int [simp]: "INum i\<^sub>N = real i" "INum 0\<^sub>N = 0"
   2.158 +  by (simp_all add: INum_def)
   2.159 +lemmas [code, code unfold] = INum_int [unfolded real_int_def [symmetric], symmetric]
   2.160 +
   2.161 +lemma [code, code unfold]: "1 = INum 1\<^sub>N" by simp
   2.162 +
   2.163 +lemma isnormNum_unique[simp]: 
   2.164 +  assumes na: "isnormNum x" and nb: "isnormNum y" 
   2.165 +  shows "(INum x = INum y) = (x = y)" (is "?lhs = ?rhs")
   2.166 +proof
   2.167 +  have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
   2.168 +  then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
   2.169 +  assume H: ?lhs 
   2.170 +  {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" hence ?rhs
   2.171 +      using na nb H
   2.172 +      by (simp add: INum_def split_def isnormNum_def)
   2.173 +       (cases "a = 0", simp_all,cases "b = 0", simp_all,
   2.174 +      cases "a' = 0", simp_all,cases "a' = 0", simp_all)}
   2.175 +  moreover
   2.176 +  { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
   2.177 +    from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
   2.178 +    from prems have eq:"a * b' = a'*b" 
   2.179 +      by (simp add: INum_def  eq_divide_eq divide_eq_eq real_of_int_mult[symmetric] del: real_of_int_mult)
   2.180 +    from prems have gcd1: "igcd a b = 1" "igcd b a = 1" "igcd a' b' = 1" "igcd b' a' = 1"       
   2.181 +      by (simp_all add: isnormNum_def add: igcd_commute)
   2.182 +    from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'" 
   2.183 +      apply(unfold dvd_def)
   2.184 +      apply (rule_tac x="b'" in exI, simp add: mult_ac)
   2.185 +      apply (rule_tac x="a'" in exI, simp add: mult_ac)
   2.186 +      apply (rule_tac x="b" in exI, simp add: mult_ac)
   2.187 +      apply (rule_tac x="a" in exI, simp add: mult_ac)
   2.188 +      done
   2.189 +    from zdvd_dvd_eq[OF bz zrelprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
   2.190 +      zrelprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
   2.191 +      have eq1: "b = b'" using pos by simp_all
   2.192 +      with eq have "a = a'" using pos by simp
   2.193 +      with eq1 have ?rhs by simp}
   2.194 +  ultimately show ?rhs by blast
   2.195 +next
   2.196 +  assume ?rhs thus ?lhs by simp
   2.197 +qed
   2.198 +
   2.199 +
   2.200 +lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = 0) = (x = 0\<^sub>N)"
   2.201 +  unfolding INum_int(2)[symmetric]
   2.202 +  by (rule isnormNum_unique, simp_all)
   2.203 +
   2.204 +lemma normNum[simp]: "INum (normNum x) = INum x"
   2.205 +proof-
   2.206 +  have "\<exists> a b. x = (a,b)" by auto
   2.207 +  then obtain a b where x[simp]: "x = (a,b)" by blast
   2.208 +  {assume "a=0 \<or> b = 0" hence ?thesis
   2.209 +      by (simp add: INum_def normNum_def split_def Let_def)}
   2.210 +  moreover 
   2.211 +  {assume a: "a\<noteq>0" and b: "b\<noteq>0"
   2.212 +    let ?g = "igcd a b"
   2.213 +    from a b have g: "?g \<noteq> 0"by simp
   2.214 +    from real_of_int_div[OF g]
   2.215 +    have ?thesis by (simp add: INum_def normNum_def split_def Let_def)}
   2.216 +  ultimately show ?thesis by blast
   2.217 +qed
   2.218 +
   2.219 +lemma INum_normNum_iff [code]: "INum x = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
   2.220 +proof -
   2.221 +  have "normNum x = normNum y \<longleftrightarrow> INum (normNum x) = INum (normNum y)"
   2.222 +    by (simp del: normNum)
   2.223 +  also have "\<dots> = ?lhs" by simp
   2.224 +  finally show ?thesis by simp
   2.225 +qed
   2.226 +
   2.227 +lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + INum y"
   2.228 +proof-
   2.229 +  have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
   2.230 +  then obtain a b a' b' where x[simp]: "x = (a,b)" 
   2.231 +    and y[simp]: "y = (a',b')" by blast
   2.232 +  {assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0" hence ?thesis 
   2.233 +      apply (cases "a=0",simp_all add: Nadd_def)
   2.234 +      apply (cases "b= 0",simp_all add: INum_def)
   2.235 +       apply (cases "a'= 0",simp_all)
   2.236 +       apply (cases "b'= 0",simp_all)
   2.237 +       done }
   2.238 +  moreover 
   2.239 +  {assume aa':"a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0" 
   2.240 +    {assume z: "a * b' + b * a' = 0"
   2.241 +      hence "real (a*b' + b*a') / (real b* real b') = 0" by simp
   2.242 +      hence "real b' * real a / (real b * real b') + real b * real a' / (real b * real b') = 0"  by (simp add:add_divide_distrib) 
   2.243 +      hence th: "real a / real b + real a' / real b' = 0" using bb' aa' by simp 
   2.244 +      from z aa' bb' have ?thesis 
   2.245 +	by (simp add: th Nadd_def normNum_def INum_def split_def)}
   2.246 +    moreover {assume z: "a * b' + b * a' \<noteq> 0"
   2.247 +      let ?g = "igcd (a * b' + b * a') (b*b')"
   2.248 +      have gz: "?g \<noteq> 0" using z by simp
   2.249 +      have ?thesis using aa' bb' z gz
   2.250 +	real_of_int_div[OF gz igcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
   2.251 +	real_of_int_div[OF gz igcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
   2.252 +	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
   2.253 +    ultimately have ?thesis using aa' bb' 
   2.254 +      by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
   2.255 +  ultimately show ?thesis by blast
   2.256 +qed
   2.257 +lemmas [code] = Nadd [symmetric]
   2.258 +
   2.259 +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * INum y"
   2.260 +proof-
   2.261 +  have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
   2.262 +  then obtain a b a' b' where x: "x = (a,b)" and y: "y = (a',b')" by blast
   2.263 +  {assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0" hence ?thesis 
   2.264 +      apply (cases "a=0",simp_all add: x y Nmul_def INum_def Let_def)
   2.265 +      apply (cases "b=0",simp_all)
   2.266 +      apply (cases "a'=0",simp_all) 
   2.267 +      done }
   2.268 +  moreover
   2.269 +  {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
   2.270 +    let ?g="igcd (a*a') (b*b')"
   2.271 +    have gz: "?g \<noteq> 0" using z by simp
   2.272 +    from z real_of_int_div[OF gz igcd_dvd1[where i="a*a'" and j="b*b'"]] 
   2.273 +      real_of_int_div[OF gz igcd_dvd2[where i="a*a'" and j="b*b'"]] 
   2.274 +    have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
   2.275 +  ultimately show ?thesis by blast
   2.276 +qed
   2.277 +lemmas [code] = Nmul [symmetric]
   2.278 +
   2.279 +lemma Nneg[simp]: "INum (~\<^sub>N x) = - INum x"
   2.280 +  by (simp add: Nneg_def split_def INum_def)
   2.281 +lemmas [code] = Nneg [symmetric]
   2.282 +
   2.283 +lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - INum y"
   2.284 +  by (simp add: Nsub_def split_def)
   2.285 +lemmas [code] = Nsub [symmetric]
   2.286 +
   2.287 +lemma Ninv[simp]: "INum (Ninv x) = 1 / (INum x)"
   2.288 +  by (simp add: Ninv_def INum_def split_def)
   2.289 +lemmas [code] = Ninv [symmetric]
   2.290 +
   2.291 +lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / INum y" by (simp add: Ndiv_def)
   2.292 +lemmas [code] = Ndiv [symmetric]
   2.293 +
   2.294 +lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" shows "(INum x < 0) = 0>\<^sub>N x "
   2.295 +proof-
   2.296 +  have " \<exists> a b. x = (a,b)" by simp
   2.297 +  then obtain a b where x[simp]:"x = (a,b)" by blast
   2.298 +  {assume "a = 0" hence ?thesis by (simp add: Nlt0_def INum_def) }
   2.299 +  moreover
   2.300 +  {assume a: "a\<noteq>0" hence b: "real b > 0" using nx by (simp add: isnormNum_def)
   2.301 +    from pos_divide_less_eq[OF b, where b="real a" and a="0"]
   2.302 +    have ?thesis by (simp add: Nlt0_def INum_def)}
   2.303 +  ultimately show ?thesis by blast
   2.304 +qed
   2.305 +
   2.306 +lemma   Nle0_iff[simp]:assumes nx: "isnormNum x" shows "(INum x \<le> 0) = 0\<ge>\<^sub>N x"
   2.307 +proof-
   2.308 +  have " \<exists> a b. x = (a,b)" by simp
   2.309 +  then obtain a b where x[simp]:"x = (a,b)" by blast
   2.310 +  {assume "a = 0" hence ?thesis by (simp add: Nle0_def INum_def) }
   2.311 +  moreover
   2.312 +  {assume a: "a\<noteq>0" hence b: "real b > 0" using nx by (simp add: isnormNum_def)
   2.313 +    from pos_divide_le_eq[OF b, where b="real a" and a="0"]
   2.314 +    have ?thesis by (simp add: Nle0_def INum_def)}
   2.315 +  ultimately show ?thesis by blast
   2.316 +qed
   2.317 +
   2.318 +lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "(INum x > 0) = 0<\<^sub>N x"
   2.319 +proof-
   2.320 +  have " \<exists> a b. x = (a,b)" by simp
   2.321 +  then obtain a b where x[simp]:"x = (a,b)" by blast
   2.322 +  {assume "a = 0" hence ?thesis by (simp add: Ngt0_def INum_def) }
   2.323 +  moreover
   2.324 +  {assume a: "a\<noteq>0" hence b: "real b > 0" using nx by (simp add: isnormNum_def)
   2.325 +    from pos_less_divide_eq[OF b, where b="real a" and a="0"]
   2.326 +    have ?thesis by (simp add: Ngt0_def INum_def)}
   2.327 +  ultimately show ?thesis by blast
   2.328 +qed
   2.329 +lemma Nge0_iff[simp]:assumes nx: "isnormNum x" shows "(INum x \<ge> 0) = 0\<le>\<^sub>N x"
   2.330 +proof-
   2.331 +  have " \<exists> a b. x = (a,b)" by simp
   2.332 +  then obtain a b where x[simp]:"x = (a,b)" by blast
   2.333 +  {assume "a = 0" hence ?thesis by (simp add: Nge0_def INum_def) }
   2.334 +  moreover
   2.335 +  {assume a: "a\<noteq>0" hence b: "real b > 0" using nx by (simp add: isnormNum_def)
   2.336 +    from pos_le_divide_eq[OF b, where b="real a" and a="0"]
   2.337 +    have ?thesis by (simp add: Nge0_def INum_def)}
   2.338 +  ultimately show ?thesis by blast
   2.339 +qed
   2.340 +
   2.341 +lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
   2.342 +  shows "(INum x < INum y) = (x <\<^sub>N y)"
   2.343 +proof-
   2.344 +  have "(INum x < INum y) = (INum (x -\<^sub>N y) < 0)" using nx ny by simp
   2.345 +  also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))" using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
   2.346 +  finally show ?thesis by (simp add: Nlt_def)
   2.347 +qed
   2.348 +
   2.349 +lemma [code]: "INum x < INum y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
   2.350 +proof -
   2.351 +  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> INum (normNum x) < INum (normNum y)" 
   2.352 +    by (simp del: normNum)
   2.353 +  also have "\<dots> = (INum x < INum y)" by simp 
   2.354 +  finally show ?thesis by simp
   2.355 +qed
   2.356 +
   2.357 +lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
   2.358 +  shows "(INum x \<le> INum y) = (x \<le>\<^sub>N y)"
   2.359 +proof-
   2.360 +  have "(INum x \<le> INum y) = (INum (x -\<^sub>N y) \<le> 0)" using nx ny by simp
   2.361 +  also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp
   2.362 +  finally show ?thesis by (simp add: Nle_def)
   2.363 +qed
   2.364 +
   2.365 +lemma [code]: "INum x \<le> INum y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
   2.366 +proof -
   2.367 +  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> INum (normNum x) \<le> INum (normNum y)" 
   2.368 +    by (simp del: normNum)
   2.369 +  also have "\<dots> = (INum x \<le> INum y)" by simp 
   2.370 +  finally show ?thesis by simp
   2.371 +qed
   2.372 +
   2.373 +lemma Nadd_commute: "x +\<^sub>N y = y +\<^sub>N x"
   2.374 +proof-
   2.375 +  have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
   2.376 +  have "INum (x +\<^sub>N y) = INum (y +\<^sub>N x)" by simp
   2.377 +  with isnormNum_unique[OF n] show ?thesis by simp
   2.378 +qed
   2.379 +
   2.380 +lemma[simp]: "(0, b) +\<^sub>N y = normNum y" "(a, 0) +\<^sub>N y = normNum y" 
   2.381 +  "x +\<^sub>N (0, b) = normNum x" "x +\<^sub>N (a, 0) = normNum x"
   2.382 +  apply (simp add: Nadd_def split_def, simp add: Nadd_def split_def)
   2.383 +  apply (subst Nadd_commute,simp add: Nadd_def split_def)
   2.384 +  apply (subst Nadd_commute,simp add: Nadd_def split_def)
   2.385 +  done
   2.386 +
   2.387 +lemma normNum_nilpotent_aux[simp]: assumes nx: "isnormNum x" 
   2.388 +  shows "normNum x = x"
   2.389 +proof-
   2.390 +  let ?a = "normNum x"
   2.391 +  have n: "isnormNum ?a" by simp
   2.392 +  have th:"INum ?a = INum x" by simp
   2.393 +  with isnormNum_unique[OF n nx]  
   2.394 +  show ?thesis by simp
   2.395 +qed
   2.396 +
   2.397 +lemma normNum_nilpotent[simp]: "normNum (normNum x) = normNum x"
   2.398 +  by simp
   2.399 +lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N"
   2.400 +  by (simp_all add: normNum_def)
   2.401 +lemma normNum_Nadd: "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
   2.402 +lemma Nadd_normNum1[simp]: "normNum x +\<^sub>N y = x +\<^sub>N y"
   2.403 +proof-
   2.404 +  have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
   2.405 +  have "INum (normNum x +\<^sub>N y) = INum x + INum y" by simp
   2.406 +  also have "\<dots> = INum (x +\<^sub>N y)" by simp
   2.407 +  finally show ?thesis using isnormNum_unique[OF n] by simp
   2.408 +qed
   2.409 +lemma Nadd_normNum2[simp]: "x +\<^sub>N normNum y = x +\<^sub>N y"
   2.410 +proof-
   2.411 +  have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
   2.412 +  have "INum (x +\<^sub>N normNum y) = INum x + INum y" by simp
   2.413 +  also have "\<dots> = INum (x +\<^sub>N y)" by simp
   2.414 +  finally show ?thesis using isnormNum_unique[OF n] by simp
   2.415 +qed
   2.416 +
   2.417 +lemma Nadd_assoc: "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
   2.418 +proof-
   2.419 +  have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
   2.420 +  have "INum (x +\<^sub>N y +\<^sub>N z) = INum (x +\<^sub>N (y +\<^sub>N z))" by simp
   2.421 +  with isnormNum_unique[OF n] show ?thesis by simp
   2.422 +qed
   2.423 +
   2.424 +lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
   2.425 +  by (simp add: Nmul_def split_def Let_def igcd_commute mult_commute)
   2.426 +
   2.427 +lemma Nmul_assoc: assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
   2.428 +  shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
   2.429 +proof-
   2.430 +  from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" 
   2.431 +    by simp_all
   2.432 +  have "INum (x +\<^sub>N y +\<^sub>N z) = INum (x +\<^sub>N (y +\<^sub>N z))" by simp
   2.433 +  with isnormNum_unique[OF n] show ?thesis by simp
   2.434 +qed
   2.435 +
   2.436 +lemma Nsub0: assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
   2.437 +proof-
   2.438 +  from isnormNum_unique[OF Nsub_normN[OF y], where y="0\<^sub>N"] 
   2.439 +  have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = INum 0\<^sub>N)" by simp
   2.440 +  also have "\<dots> = (INum x = INum y)" by simp
   2.441 +  also have "\<dots> = (x = y)" using x y by simp
   2.442 +  finally show ?thesis .
   2.443 +qed
   2.444 +lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N"
   2.445 +  by (simp_all add: Nmul_def Let_def split_def)
   2.446 +
   2.447 +lemma Nmul_eq0[simp]: assumes nx:"isnormNum x" and ny: "isnormNum y"
   2.448 +  shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)"
   2.449 +proof-
   2.450 +  have " \<exists> a b a' b'. x = (a,b) \<and> y= (a',b')" by auto
   2.451 +  then obtain a b a' b' where xy[simp]: "x = (a,b)" "y = (a',b')" by blast
   2.452 +  have n0: "isnormNum 0\<^sub>N" by simp
   2.453 +  show ?thesis using nx ny 
   2.454 +    apply (simp only: isnormNum_unique[OF  Nmul_normN[OF nx ny] n0, symmetric] Nmul)
   2.455 +    apply (simp add: INum_def split_def isnormNum_def fst_conv snd_conv)
   2.456 +    apply (cases "a=0",simp_all)
   2.457 +    apply (cases "a'=0",simp_all)
   2.458 +    done 
   2.459 +qed
   2.460 +lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
   2.461 +  by (simp add: Nneg_def split_def)
   2.462 +
   2.463 +lemma Nmul1[simp]: 
   2.464 +  "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c" 
   2.465 +  "isnormNum c \<Longrightarrow> c *\<^sub>N 1\<^sub>N  = c" 
   2.466 +  apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
   2.467 +  by (cases "fst c = 0", simp_all,cases c, simp_all)+
   2.468 +
   2.469 +lemma [code, code unfold]:
   2.470 +  "number_of k = real_int (number_of k)"
   2.471 +  by (simp add: real_int_def)
   2.472 +
   2.473 +types_code real ("{* int * int *}")
   2.474 +attach (term_of) {*
   2.475 +fun term_of_real (p, q) =
   2.476 +  let 
   2.477 +    val rT = HOLogic.realT;
   2.478 +in if q = 1
   2.479 +  then HOLogic.mk_number rT p
   2.480 +  else Const ("HOL.divide", rT --> rT --> rT) $
   2.481 +    HOLogic.mk_number rT p $ HOLogic.mk_number rT q
   2.482 +end;
   2.483 +*}
   2.484 +
   2.485 +consts_code INum ("")
   2.486 +
   2.487 +end
   2.488 \ No newline at end of file
     3.1 --- a/src/HOL/Library/Library.thy	Tue May 15 18:20:07 2007 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Tue May 15 18:28:02 2007 +0200
     3.3 @@ -12,6 +12,7 @@
     3.4    EfficientNat
     3.5    Eval
     3.6    ExecutableRat
     3.7 +  Executable_Real
     3.8    ExecutableSet
     3.9    FuncSet
    3.10    GCD
     4.1 --- a/src/HOL/ex/ExecutableContent.thy	Tue May 15 18:20:07 2007 +0200
     4.2 +++ b/src/HOL/ex/ExecutableContent.thy	Tue May 15 18:28:02 2007 +0200
     4.3 @@ -14,6 +14,7 @@
     4.4    Binomial
     4.5    Commutative_Ring
     4.6    "~~/src/HOL/ex/Commutative_Ring_Complete"
     4.7 +(*  Executable_Real *)
     4.8    GCD
     4.9    List_Prefix
    4.10    Nat_Infinity