src/HOL/Library/Executable_Real.thy
changeset 22981 cf071f3fc4ae
child 22982 bff3fcdeecd3
equal deleted inserted replaced
22980:1226d861eefb 22981:cf071f3fc4ae
       
     1 (*  Title:      HOL/Library/Executable_Real.thy
       
     2     ID:         $Id$
       
     3     Author:     Amine Chaieb, TU Muenchen
       
     4 *)
       
     5 
       
     6 header {* Implementation of rational real numbers as pairs of integers *}
       
     7 
       
     8 theory Executable_Real
       
     9 imports GCD "~~/src/HOL/Real/Real"
       
    10 begin
       
    11 
       
    12 subsection {* Implementation of operations on pair of integers *}
       
    13 
       
    14 types Num = "int * int"
       
    15 syntax "_Num0" :: "Num" ("0\<^sub>N")
       
    16 translations "0\<^sub>N" \<rightleftharpoons> "(0,0)"
       
    17 syntax "_Numi" :: "int \<Rightarrow> Num" ("_\<^sub>N")
       
    18 translations "i\<^sub>N" \<rightleftharpoons> "(i,1)::Num"
       
    19 
       
    20 constdefs isnormNum :: "Num \<Rightarrow> bool"
       
    21   "isnormNum \<equiv> \<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> igcd a b = 1)"
       
    22 
       
    23 constdefs normNum :: "Num \<Rightarrow> Num"
       
    24   "normNum \<equiv> \<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else 
       
    25   (let g = igcd a b 
       
    26    in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g))))"
       
    27 lemma normNum_isnormNum[simp]: "isnormNum (normNum x)"
       
    28 proof-
       
    29   have " \<exists> a b. x = (a,b)" by auto
       
    30   then obtain a b where x[simp]: "x = (a,b)" by blast
       
    31   {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}  
       
    32   moreover
       
    33   {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0" 
       
    34     let ?g = "igcd a b"
       
    35     let ?a' = "a div ?g"
       
    36     let ?b' = "b div ?g"
       
    37     let ?g' = "igcd ?a' ?b'"
       
    38     from anz bnz have "?g \<noteq> 0" by simp  with igcd_pos[of a b] 
       
    39     have gpos: "?g > 0"  by arith
       
    40     have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2)
       
    41     from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
       
    42     anz bnz
       
    43     have nz':"?a' \<noteq> 0" "?b' \<noteq> 0" 
       
    44       by - (rule notI,simp add:igcd_def)+
       
    45     from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by blast
       
    46     from div_igcd_relprime[OF stupid] have gp1: "?g' = 1" .
       
    47     from bnz have "b < 0 \<or> b > 0" by arith
       
    48     moreover
       
    49     {assume b: "b > 0"
       
    50       from pos_imp_zdiv_nonneg_iff[OF gpos] b
       
    51       have "?b' \<ge> 0" by simp
       
    52       with nz' have b': "?b' > 0" by simp
       
    53       from b b' anz bnz nz' gp1 have ?thesis 
       
    54 	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
       
    55     moreover {assume b: "b < 0"
       
    56       {assume b': "?b' \<ge> 0" 
       
    57 	from gpos have th: "?g \<ge> 0" by arith
       
    58 	from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
       
    59 	have False using b by simp }
       
    60       hence b': "?b' < 0" by arith
       
    61       from anz bnz nz' b b' gp1 have ?thesis 
       
    62 	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
       
    63     ultimately have ?thesis by blast
       
    64   }
       
    65   ultimately show ?thesis by blast
       
    66 qed
       
    67     (* Arithmetic over Num *)
       
    68 constdefs Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "+\<^sub>N" 60)
       
    69   "Nadd \<equiv> \<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b') 
       
    70   else if a'=0 \<or> b' = 0 then normNum(a,b) 
       
    71   else normNum(a*b' + b*a', b*b')"
       
    72 constdefs Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
       
    73   "Nmul \<equiv> \<lambda>(a,b) (a',b'). let g = igcd (a*a') (b*b') 
       
    74   in (a*a' div g, b*b' div g)"
       
    75 constdefs Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N")
       
    76   "Nneg \<equiv> \<lambda>(a,b). (-a,b)"
       
    77 constdefs  Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "-\<^sub>N" 60)
       
    78   "Nsub \<equiv> \<lambda>a b. a +\<^sub>N ~\<^sub>N b"
       
    79 constdefs Ninv :: "Num \<Rightarrow> Num" 
       
    80 "Ninv \<equiv> \<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a)"
       
    81 constdefs Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "\<div>\<^sub>N" 60)
       
    82   "Ndiv \<equiv> \<lambda>a b. a *\<^sub>N Ninv b"
       
    83 
       
    84 lemma Nneg_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (~\<^sub>N x)"
       
    85   by(simp add: isnormNum_def Nneg_def split_def)
       
    86 lemma Nadd_normN[simp]: "isnormNum (x +\<^sub>N y)"
       
    87   by (simp add: Nadd_def split_def)
       
    88 lemma Nsub_normN[simp]: "\<lbrakk> isnormNum y\<rbrakk> \<Longrightarrow> isnormNum (x -\<^sub>N y)"
       
    89   by (simp add: Nsub_def split_def)
       
    90 lemma Nmul_normN[simp]: assumes xn:"isnormNum x" and yn: "isnormNum y"
       
    91   shows "isnormNum (x *\<^sub>N y)"
       
    92 proof-
       
    93   have "\<exists>a b. x = (a,b)" and "\<exists> a' b'. y = (a',b')" by auto
       
    94   then obtain a b a' b' where ab: "x = (a,b)"  and ab': "y = (a',b')" by blast 
       
    95   {assume "a = 0"
       
    96     hence ?thesis using xn ab ab'
       
    97       by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
       
    98   moreover
       
    99   {assume "a' = 0"
       
   100     hence ?thesis using yn ab ab' 
       
   101       by (simp add: igcd_def isnormNum_def Let_def Nmul_def split_def)}
       
   102   moreover
       
   103   {assume a: "a \<noteq>0" and a': "a'\<noteq>0"
       
   104     hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def)
       
   105     from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a*a', b*b')" 
       
   106       using ab ab' a a' bp by (simp add: Nmul_def Let_def split_def normNum_def)
       
   107     hence ?thesis by simp}
       
   108   ultimately show ?thesis by blast
       
   109 qed
       
   110 
       
   111 lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
       
   112 by (simp add: Ninv_def isnormNum_def split_def)
       
   113 (cases "fst x = 0",auto simp add: igcd_commute)
       
   114 
       
   115 lemma isnormNum_int[simp]: 
       
   116   "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
       
   117  by (simp_all add: isnormNum_def igcd_def)
       
   118 
       
   119     (* Relations over Num *)
       
   120 constdefs Nlt0:: "Num \<Rightarrow> bool" ("0>\<^sub>N")
       
   121   "Nlt0 \<equiv> \<lambda>(a,b). a < 0"
       
   122 constdefs Nle0:: "Num \<Rightarrow> bool" ("0\<ge>\<^sub>N")
       
   123   "Nle0 \<equiv> \<lambda>(a,b). a \<le> 0"
       
   124 constdefs Ngt0:: "Num \<Rightarrow> bool" ("0<\<^sub>N")
       
   125   "Ngt0 \<equiv> \<lambda>(a,b). a > 0"
       
   126 constdefs Nge0:: "Num \<Rightarrow> bool" ("0\<le>\<^sub>N")
       
   127   "Nge0 \<equiv> \<lambda>(a,b). a \<ge> 0"
       
   128 constdefs Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "<\<^sub>N" 55)
       
   129   "Nlt \<equiv> \<lambda>a b. 0>\<^sub>N (a -\<^sub>N b)"
       
   130 constdefs Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "\<le>\<^sub>N" 55)
       
   131   "Nle \<equiv> \<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b)"
       
   132 
       
   133 
       
   134 subsection {* Interpretation of the normalized rats in \<real> *}
       
   135 
       
   136 definition
       
   137   INum:: "Num \<Rightarrow> real"
       
   138 where
       
   139   INum_def: "INum \<equiv> \<lambda>(a,b). real a / real b"
       
   140 
       
   141 code_datatype INum
       
   142 instance real :: eq ..
       
   143 
       
   144 definition
       
   145   real_int :: "int \<Rightarrow> real"
       
   146 where
       
   147   "real_int = real"
       
   148 lemmas [code unfold] = real_int_def [symmetric]
       
   149 
       
   150 lemma [code unfold]:
       
   151   "real = real_int o int"
       
   152   by (auto simp add: real_int_def expand_fun_eq)
       
   153 
       
   154 lemma INum_int [simp]: "INum i\<^sub>N = real i" "INum 0\<^sub>N = 0"
       
   155   by (simp_all add: INum_def)
       
   156 lemmas [code, code unfold] = INum_int [unfolded real_int_def [symmetric], symmetric]
       
   157 
       
   158 lemma [code, code unfold]: "1 = INum 1\<^sub>N" by simp
       
   159 
       
   160 lemma isnormNum_unique[simp]: 
       
   161   assumes na: "isnormNum x" and nb: "isnormNum y" 
       
   162   shows "(INum x = INum y) = (x = y)" (is "?lhs = ?rhs")
       
   163 proof
       
   164   have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
       
   165   then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
       
   166   assume H: ?lhs 
       
   167   {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" hence ?rhs
       
   168       using na nb H
       
   169       by (simp add: INum_def split_def isnormNum_def)
       
   170        (cases "a = 0", simp_all,cases "b = 0", simp_all,
       
   171       cases "a' = 0", simp_all,cases "a' = 0", simp_all)}
       
   172   moreover
       
   173   { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
       
   174     from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
       
   175     from prems have eq:"a * b' = a'*b" 
       
   176       by (simp add: INum_def  eq_divide_eq divide_eq_eq real_of_int_mult[symmetric] del: real_of_int_mult)
       
   177     from prems have gcd1: "igcd a b = 1" "igcd b a = 1" "igcd a' b' = 1" "igcd b' a' = 1"       
       
   178       by (simp_all add: isnormNum_def add: igcd_commute)
       
   179     from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'" 
       
   180       apply(unfold dvd_def)
       
   181       apply (rule_tac x="b'" in exI, simp add: mult_ac)
       
   182       apply (rule_tac x="a'" in exI, simp add: mult_ac)
       
   183       apply (rule_tac x="b" in exI, simp add: mult_ac)
       
   184       apply (rule_tac x="a" in exI, simp add: mult_ac)
       
   185       done
       
   186     from zdvd_dvd_eq[OF bz zrelprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
       
   187       zrelprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
       
   188       have eq1: "b = b'" using pos by simp_all
       
   189       with eq have "a = a'" using pos by simp
       
   190       with eq1 have ?rhs by simp}
       
   191   ultimately show ?rhs by blast
       
   192 next
       
   193   assume ?rhs thus ?lhs by simp
       
   194 qed
       
   195 
       
   196 
       
   197 lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = 0) = (x = 0\<^sub>N)"
       
   198   unfolding INum_int(2)[symmetric]
       
   199   by (rule isnormNum_unique, simp_all)
       
   200 
       
   201 lemma normNum[simp]: "INum (normNum x) = INum x"
       
   202 proof-
       
   203   have "\<exists> a b. x = (a,b)" by auto
       
   204   then obtain a b where x[simp]: "x = (a,b)" by blast
       
   205   {assume "a=0 \<or> b = 0" hence ?thesis
       
   206       by (simp add: INum_def normNum_def split_def Let_def)}
       
   207   moreover 
       
   208   {assume a: "a\<noteq>0" and b: "b\<noteq>0"
       
   209     let ?g = "igcd a b"
       
   210     from a b have g: "?g \<noteq> 0"by simp
       
   211     from real_of_int_div[OF g]
       
   212     have ?thesis by (simp add: INum_def normNum_def split_def Let_def)}
       
   213   ultimately show ?thesis by blast
       
   214 qed
       
   215 
       
   216 lemma INum_normNum_iff [code]: "INum x = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
       
   217 proof -
       
   218   have "normNum x = normNum y \<longleftrightarrow> INum (normNum x) = INum (normNum y)"
       
   219     by (simp del: normNum)
       
   220   also have "\<dots> = ?lhs" by simp
       
   221   finally show ?thesis by simp
       
   222 qed
       
   223 
       
   224 lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + INum y"
       
   225 proof-
       
   226   have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
       
   227   then obtain a b a' b' where x[simp]: "x = (a,b)" 
       
   228     and y[simp]: "y = (a',b')" by blast
       
   229   {assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0" hence ?thesis 
       
   230       apply (cases "a=0",simp_all add: Nadd_def)
       
   231       apply (cases "b= 0",simp_all add: INum_def)
       
   232        apply (cases "a'= 0",simp_all)
       
   233        apply (cases "b'= 0",simp_all)
       
   234        done }
       
   235   moreover 
       
   236   {assume aa':"a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0" 
       
   237     {assume z: "a * b' + b * a' = 0"
       
   238       hence "real (a*b' + b*a') / (real b* real b') = 0" by simp
       
   239       hence "real b' * real a / (real b * real b') + real b * real a' / (real b * real b') = 0"  by (simp add:add_divide_distrib) 
       
   240       hence th: "real a / real b + real a' / real b' = 0" using bb' aa' by simp 
       
   241       from z aa' bb' have ?thesis 
       
   242 	by (simp add: th Nadd_def normNum_def INum_def split_def)}
       
   243     moreover {assume z: "a * b' + b * a' \<noteq> 0"
       
   244       let ?g = "igcd (a * b' + b * a') (b*b')"
       
   245       have gz: "?g \<noteq> 0" using z by simp
       
   246       have ?thesis using aa' bb' z gz
       
   247 	real_of_int_div[OF gz igcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
       
   248 	real_of_int_div[OF gz igcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
       
   249 	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
       
   250     ultimately have ?thesis using aa' bb' 
       
   251       by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
       
   252   ultimately show ?thesis by blast
       
   253 qed
       
   254 lemmas [code] = Nadd [symmetric]
       
   255 
       
   256 lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * INum y"
       
   257 proof-
       
   258   have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
       
   259   then obtain a b a' b' where x: "x = (a,b)" and y: "y = (a',b')" by blast
       
   260   {assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0" hence ?thesis 
       
   261       apply (cases "a=0",simp_all add: x y Nmul_def INum_def Let_def)
       
   262       apply (cases "b=0",simp_all)
       
   263       apply (cases "a'=0",simp_all) 
       
   264       done }
       
   265   moreover
       
   266   {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
       
   267     let ?g="igcd (a*a') (b*b')"
       
   268     have gz: "?g \<noteq> 0" using z by simp
       
   269     from z real_of_int_div[OF gz igcd_dvd1[where i="a*a'" and j="b*b'"]] 
       
   270       real_of_int_div[OF gz igcd_dvd2[where i="a*a'" and j="b*b'"]] 
       
   271     have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
       
   272   ultimately show ?thesis by blast
       
   273 qed
       
   274 lemmas [code] = Nmul [symmetric]
       
   275 
       
   276 lemma Nneg[simp]: "INum (~\<^sub>N x) = - INum x"
       
   277   by (simp add: Nneg_def split_def INum_def)
       
   278 lemmas [code] = Nneg [symmetric]
       
   279 
       
   280 lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - INum y"
       
   281   by (simp add: Nsub_def split_def)
       
   282 lemmas [code] = Nsub [symmetric]
       
   283 
       
   284 lemma Ninv[simp]: "INum (Ninv x) = 1 / (INum x)"
       
   285   by (simp add: Ninv_def INum_def split_def)
       
   286 lemmas [code] = Ninv [symmetric]
       
   287 
       
   288 lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / INum y" by (simp add: Ndiv_def)
       
   289 lemmas [code] = Ndiv [symmetric]
       
   290 
       
   291 lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" shows "(INum x < 0) = 0>\<^sub>N x "
       
   292 proof-
       
   293   have " \<exists> a b. x = (a,b)" by simp
       
   294   then obtain a b where x[simp]:"x = (a,b)" by blast
       
   295   {assume "a = 0" hence ?thesis by (simp add: Nlt0_def INum_def) }
       
   296   moreover
       
   297   {assume a: "a\<noteq>0" hence b: "real b > 0" using nx by (simp add: isnormNum_def)
       
   298     from pos_divide_less_eq[OF b, where b="real a" and a="0"]
       
   299     have ?thesis by (simp add: Nlt0_def INum_def)}
       
   300   ultimately show ?thesis by blast
       
   301 qed
       
   302 
       
   303 lemma   Nle0_iff[simp]:assumes nx: "isnormNum x" shows "(INum x \<le> 0) = 0\<ge>\<^sub>N x"
       
   304 proof-
       
   305   have " \<exists> a b. x = (a,b)" by simp
       
   306   then obtain a b where x[simp]:"x = (a,b)" by blast
       
   307   {assume "a = 0" hence ?thesis by (simp add: Nle0_def INum_def) }
       
   308   moreover
       
   309   {assume a: "a\<noteq>0" hence b: "real b > 0" using nx by (simp add: isnormNum_def)
       
   310     from pos_divide_le_eq[OF b, where b="real a" and a="0"]
       
   311     have ?thesis by (simp add: Nle0_def INum_def)}
       
   312   ultimately show ?thesis by blast
       
   313 qed
       
   314 
       
   315 lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "(INum x > 0) = 0<\<^sub>N x"
       
   316 proof-
       
   317   have " \<exists> a b. x = (a,b)" by simp
       
   318   then obtain a b where x[simp]:"x = (a,b)" by blast
       
   319   {assume "a = 0" hence ?thesis by (simp add: Ngt0_def INum_def) }
       
   320   moreover
       
   321   {assume a: "a\<noteq>0" hence b: "real b > 0" using nx by (simp add: isnormNum_def)
       
   322     from pos_less_divide_eq[OF b, where b="real a" and a="0"]
       
   323     have ?thesis by (simp add: Ngt0_def INum_def)}
       
   324   ultimately show ?thesis by blast
       
   325 qed
       
   326 lemma Nge0_iff[simp]:assumes nx: "isnormNum x" shows "(INum x \<ge> 0) = 0\<le>\<^sub>N x"
       
   327 proof-
       
   328   have " \<exists> a b. x = (a,b)" by simp
       
   329   then obtain a b where x[simp]:"x = (a,b)" by blast
       
   330   {assume "a = 0" hence ?thesis by (simp add: Nge0_def INum_def) }
       
   331   moreover
       
   332   {assume a: "a\<noteq>0" hence b: "real b > 0" using nx by (simp add: isnormNum_def)
       
   333     from pos_le_divide_eq[OF b, where b="real a" and a="0"]
       
   334     have ?thesis by (simp add: Nge0_def INum_def)}
       
   335   ultimately show ?thesis by blast
       
   336 qed
       
   337 
       
   338 lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
       
   339   shows "(INum x < INum y) = (x <\<^sub>N y)"
       
   340 proof-
       
   341   have "(INum x < INum y) = (INum (x -\<^sub>N y) < 0)" using nx ny by simp
       
   342   also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))" using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
       
   343   finally show ?thesis by (simp add: Nlt_def)
       
   344 qed
       
   345 
       
   346 lemma [code]: "INum x < INum y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
       
   347 proof -
       
   348   have "normNum x <\<^sub>N normNum y \<longleftrightarrow> INum (normNum x) < INum (normNum y)" 
       
   349     by (simp del: normNum)
       
   350   also have "\<dots> = (INum x < INum y)" by simp 
       
   351   finally show ?thesis by simp
       
   352 qed
       
   353 
       
   354 lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
       
   355   shows "(INum x \<le> INum y) = (x \<le>\<^sub>N y)"
       
   356 proof-
       
   357   have "(INum x \<le> INum y) = (INum (x -\<^sub>N y) \<le> 0)" using nx ny by simp
       
   358   also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp
       
   359   finally show ?thesis by (simp add: Nle_def)
       
   360 qed
       
   361 
       
   362 lemma [code]: "INum x \<le> INum y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
       
   363 proof -
       
   364   have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> INum (normNum x) \<le> INum (normNum y)" 
       
   365     by (simp del: normNum)
       
   366   also have "\<dots> = (INum x \<le> INum y)" by simp 
       
   367   finally show ?thesis by simp
       
   368 qed
       
   369 
       
   370 lemma Nadd_commute: "x +\<^sub>N y = y +\<^sub>N x"
       
   371 proof-
       
   372   have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
       
   373   have "INum (x +\<^sub>N y) = INum (y +\<^sub>N x)" by simp
       
   374   with isnormNum_unique[OF n] show ?thesis by simp
       
   375 qed
       
   376 
       
   377 lemma[simp]: "(0, b) +\<^sub>N y = normNum y" "(a, 0) +\<^sub>N y = normNum y" 
       
   378   "x +\<^sub>N (0, b) = normNum x" "x +\<^sub>N (a, 0) = normNum x"
       
   379   apply (simp add: Nadd_def split_def, simp add: Nadd_def split_def)
       
   380   apply (subst Nadd_commute,simp add: Nadd_def split_def)
       
   381   apply (subst Nadd_commute,simp add: Nadd_def split_def)
       
   382   done
       
   383 
       
   384 lemma normNum_nilpotent_aux[simp]: assumes nx: "isnormNum x" 
       
   385   shows "normNum x = x"
       
   386 proof-
       
   387   let ?a = "normNum x"
       
   388   have n: "isnormNum ?a" by simp
       
   389   have th:"INum ?a = INum x" by simp
       
   390   with isnormNum_unique[OF n nx]  
       
   391   show ?thesis by simp
       
   392 qed
       
   393 
       
   394 lemma normNum_nilpotent[simp]: "normNum (normNum x) = normNum x"
       
   395   by simp
       
   396 lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N"
       
   397   by (simp_all add: normNum_def)
       
   398 lemma normNum_Nadd: "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
       
   399 lemma Nadd_normNum1[simp]: "normNum x +\<^sub>N y = x +\<^sub>N y"
       
   400 proof-
       
   401   have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
       
   402   have "INum (normNum x +\<^sub>N y) = INum x + INum y" by simp
       
   403   also have "\<dots> = INum (x +\<^sub>N y)" by simp
       
   404   finally show ?thesis using isnormNum_unique[OF n] by simp
       
   405 qed
       
   406 lemma Nadd_normNum2[simp]: "x +\<^sub>N normNum y = x +\<^sub>N y"
       
   407 proof-
       
   408   have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
       
   409   have "INum (x +\<^sub>N normNum y) = INum x + INum y" by simp
       
   410   also have "\<dots> = INum (x +\<^sub>N y)" by simp
       
   411   finally show ?thesis using isnormNum_unique[OF n] by simp
       
   412 qed
       
   413 
       
   414 lemma Nadd_assoc: "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
       
   415 proof-
       
   416   have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
       
   417   have "INum (x +\<^sub>N y +\<^sub>N z) = INum (x +\<^sub>N (y +\<^sub>N z))" by simp
       
   418   with isnormNum_unique[OF n] show ?thesis by simp
       
   419 qed
       
   420 
       
   421 lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
       
   422   by (simp add: Nmul_def split_def Let_def igcd_commute mult_commute)
       
   423 
       
   424 lemma Nmul_assoc: assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
       
   425   shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
       
   426 proof-
       
   427   from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" 
       
   428     by simp_all
       
   429   have "INum (x +\<^sub>N y +\<^sub>N z) = INum (x +\<^sub>N (y +\<^sub>N z))" by simp
       
   430   with isnormNum_unique[OF n] show ?thesis by simp
       
   431 qed
       
   432 
       
   433 lemma Nsub0: assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
       
   434 proof-
       
   435   from isnormNum_unique[OF Nsub_normN[OF y], where y="0\<^sub>N"] 
       
   436   have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = INum 0\<^sub>N)" by simp
       
   437   also have "\<dots> = (INum x = INum y)" by simp
       
   438   also have "\<dots> = (x = y)" using x y by simp
       
   439   finally show ?thesis .
       
   440 qed
       
   441 lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N"
       
   442   by (simp_all add: Nmul_def Let_def split_def)
       
   443 
       
   444 lemma Nmul_eq0[simp]: assumes nx:"isnormNum x" and ny: "isnormNum y"
       
   445   shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)"
       
   446 proof-
       
   447   have " \<exists> a b a' b'. x = (a,b) \<and> y= (a',b')" by auto
       
   448   then obtain a b a' b' where xy[simp]: "x = (a,b)" "y = (a',b')" by blast
       
   449   have n0: "isnormNum 0\<^sub>N" by simp
       
   450   show ?thesis using nx ny 
       
   451     apply (simp only: isnormNum_unique[OF  Nmul_normN[OF nx ny] n0, symmetric] Nmul)
       
   452     apply (simp add: INum_def split_def isnormNum_def fst_conv snd_conv)
       
   453     apply (cases "a=0",simp_all)
       
   454     apply (cases "a'=0",simp_all)
       
   455     done 
       
   456 qed
       
   457 lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
       
   458   by (simp add: Nneg_def split_def)
       
   459 
       
   460 lemma Nmul1[simp]: 
       
   461   "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c" 
       
   462   "isnormNum c \<Longrightarrow> c *\<^sub>N 1\<^sub>N  = c" 
       
   463   apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
       
   464   by (cases "fst c = 0", simp_all,cases c, simp_all)+
       
   465 
       
   466 lemma [code, code unfold]:
       
   467   "number_of k = real_int (number_of k)"
       
   468   by (simp add: real_int_def)
       
   469 
       
   470 types_code real ("{* int * int *}")
       
   471 attach (term_of) {*
       
   472 fun term_of_real (p, q) =
       
   473   let 
       
   474     val rT = HOLogic.realT;
       
   475 in if q = 1
       
   476   then HOLogic.mk_number rT p
       
   477   else Const ("HOL.divide", rT --> rT --> rT) $
       
   478     HOLogic.mk_number rT p $ HOLogic.mk_number rT q
       
   479 end;
       
   480 *}
       
   481 
       
   482 consts_code INum ("")
       
   483 
       
   484 end