reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
authorwenzelm
Wed Sep 02 16:25:44 2009 +0200 (2009-09-02)
changeset 32491d5d8bea0cd94
parent 32490 6a48db3e627c
child 32492 9d49a280f3f9
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
src/HOL/IsaMakefile
src/HOL/Matrix/ComputeFloat.thy
src/HOL/Matrix/ComputeHOL.thy
src/HOL/Matrix/ComputeNumeral.thy
src/HOL/Matrix/LP.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/ROOT.ML
src/HOL/Matrix/SparseMatrix.thy
src/HOL/Matrix/cplex/Cplex.thy
src/HOL/Matrix/cplex/CplexMatrixConverter.ML
src/HOL/Matrix/cplex/Cplex_tools.ML
src/HOL/Tools/ComputeFloat.thy
src/HOL/Tools/ComputeHOL.thy
src/HOL/Tools/ComputeNumeral.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Sep 02 14:11:45 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Sep 02 16:25:44 2009 +0200
     1.3 @@ -940,7 +940,7 @@
     1.4  
     1.5  HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
     1.6  
     1.7 -$(LOG)/HOL-Matrix.gz: $(OUT)/HOL				\
     1.8 +$(LOG)/HOL-Matrix.gz: $(OUT)/HOL					\
     1.9    $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy			\
    1.10    $(SRC)/Tools/Compute_Oracle/am_compiler.ML				\
    1.11    $(SRC)/Tools/Compute_Oracle/am_interpreter.ML				\
    1.12 @@ -948,8 +948,8 @@
    1.13    $(SRC)/Tools/Compute_Oracle/linker.ML					\
    1.14    $(SRC)/Tools/Compute_Oracle/am_ghc.ML					\
    1.15    $(SRC)/Tools/Compute_Oracle/am_sml.ML					\
    1.16 -  $(SRC)/Tools/Compute_Oracle/compute.ML	\
    1.17 -  Tools/ComputeFloat.thy Tools/float_arith.ML \
    1.18 +  $(SRC)/Tools/Compute_Oracle/compute.ML Matrix/ComputeFloat.thy	\
    1.19 +  Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy Tools/float_arith.ML	\
    1.20    Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy		\
    1.21    Matrix/document/root.tex Matrix/ROOT.ML Matrix/cplex/Cplex.thy	\
    1.22    Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML	\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Matrix/ComputeFloat.thy	Wed Sep 02 16:25:44 2009 +0200
     2.3 @@ -0,0 +1,568 @@
     2.4 +(*  Title:  HOL/Tools/ComputeFloat.thy
     2.5 +    Author: Steven Obua
     2.6 +*)
     2.7 +
     2.8 +header {* Floating Point Representation of the Reals *}
     2.9 +
    2.10 +theory ComputeFloat
    2.11 +imports Complex_Main
    2.12 +uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
    2.13 +begin
    2.14 +
    2.15 +definition
    2.16 +  pow2 :: "int \<Rightarrow> real" where
    2.17 +  "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
    2.18 +
    2.19 +definition
    2.20 +  float :: "int * int \<Rightarrow> real" where
    2.21 +  "float x = real (fst x) * pow2 (snd x)"
    2.22 +
    2.23 +lemma pow2_0[simp]: "pow2 0 = 1"
    2.24 +by (simp add: pow2_def)
    2.25 +
    2.26 +lemma pow2_1[simp]: "pow2 1 = 2"
    2.27 +by (simp add: pow2_def)
    2.28 +
    2.29 +lemma pow2_neg: "pow2 x = inverse (pow2 (-x))"
    2.30 +by (simp add: pow2_def)
    2.31 +
    2.32 +lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
    2.33 +proof -
    2.34 +  have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith
    2.35 +  have g: "! a b. a - -1 = a + (1::int)" by arith
    2.36 +  have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)"
    2.37 +    apply (auto, induct_tac n)
    2.38 +    apply (simp_all add: pow2_def)
    2.39 +    apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
    2.40 +    by (auto simp add: h)
    2.41 +  show ?thesis
    2.42 +  proof (induct a)
    2.43 +    case (1 n)
    2.44 +    from pos show ?case by (simp add: algebra_simps)
    2.45 +  next
    2.46 +    case (2 n)
    2.47 +    show ?case
    2.48 +      apply (auto)
    2.49 +      apply (subst pow2_neg[of "- int n"])
    2.50 +      apply (subst pow2_neg[of "-1 - int n"])
    2.51 +      apply (auto simp add: g pos)
    2.52 +      done
    2.53 +  qed
    2.54 +qed
    2.55 +
    2.56 +lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
    2.57 +proof (induct b)
    2.58 +  case (1 n)
    2.59 +  show ?case
    2.60 +  proof (induct n)
    2.61 +    case 0
    2.62 +    show ?case by simp
    2.63 +  next
    2.64 +    case (Suc m)
    2.65 +    show ?case by (auto simp add: algebra_simps pow2_add1 prems)
    2.66 +  qed
    2.67 +next
    2.68 +  case (2 n)
    2.69 +  show ?case
    2.70 +  proof (induct n)
    2.71 +    case 0
    2.72 +    show ?case
    2.73 +      apply (auto)
    2.74 +      apply (subst pow2_neg[of "a + -1"])
    2.75 +      apply (subst pow2_neg[of "-1"])
    2.76 +      apply (simp)
    2.77 +      apply (insert pow2_add1[of "-a"])
    2.78 +      apply (simp add: algebra_simps)
    2.79 +      apply (subst pow2_neg[of "-a"])
    2.80 +      apply (simp)
    2.81 +      done
    2.82 +    case (Suc m)
    2.83 +    have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith
    2.84 +    have b: "int m - -2 = 1 + (int m + 1)" by arith
    2.85 +    show ?case
    2.86 +      apply (auto)
    2.87 +      apply (subst pow2_neg[of "a + (-2 - int m)"])
    2.88 +      apply (subst pow2_neg[of "-2 - int m"])
    2.89 +      apply (auto simp add: algebra_simps)
    2.90 +      apply (subst a)
    2.91 +      apply (subst b)
    2.92 +      apply (simp only: pow2_add1)
    2.93 +      apply (subst pow2_neg[of "int m - a + 1"])
    2.94 +      apply (subst pow2_neg[of "int m + 1"])
    2.95 +      apply auto
    2.96 +      apply (insert prems)
    2.97 +      apply (auto simp add: algebra_simps)
    2.98 +      done
    2.99 +  qed
   2.100 +qed
   2.101 +
   2.102 +lemma "float (a, e) + float (b, e) = float (a + b, e)"
   2.103 +by (simp add: float_def algebra_simps)
   2.104 +
   2.105 +definition
   2.106 +  int_of_real :: "real \<Rightarrow> int" where
   2.107 +  "int_of_real x = (SOME y. real y = x)"
   2.108 +
   2.109 +definition
   2.110 +  real_is_int :: "real \<Rightarrow> bool" where
   2.111 +  "real_is_int x = (EX (u::int). x = real u)"
   2.112 +
   2.113 +lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"
   2.114 +by (auto simp add: real_is_int_def int_of_real_def)
   2.115 +
   2.116 +lemma float_transfer: "real_is_int ((real a)*(pow2 c)) \<Longrightarrow> float (a, b) = float (int_of_real ((real a)*(pow2 c)), b - c)"
   2.117 +by (simp add: float_def real_is_int_def2 pow2_add[symmetric])
   2.118 +
   2.119 +lemma pow2_int: "pow2 (int c) = 2^c"
   2.120 +by (simp add: pow2_def)
   2.121 +
   2.122 +lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)"
   2.123 +by (simp add: float_def pow2_int[symmetric] pow2_add[symmetric])
   2.124 +
   2.125 +lemma real_is_int_real[simp]: "real_is_int (real (x::int))"
   2.126 +by (auto simp add: real_is_int_def int_of_real_def)
   2.127 +
   2.128 +lemma int_of_real_real[simp]: "int_of_real (real x) = x"
   2.129 +by (simp add: int_of_real_def)
   2.130 +
   2.131 +lemma real_int_of_real[simp]: "real_is_int x \<Longrightarrow> real (int_of_real x) = x"
   2.132 +by (auto simp add: int_of_real_def real_is_int_def)
   2.133 +
   2.134 +lemma real_is_int_add_int_of_real: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> (int_of_real (a+b)) = (int_of_real a) + (int_of_real b)"
   2.135 +by (auto simp add: int_of_real_def real_is_int_def)
   2.136 +
   2.137 +lemma real_is_int_add[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a+b)"
   2.138 +apply (subst real_is_int_def2)
   2.139 +apply (simp add: real_is_int_add_int_of_real real_int_of_real)
   2.140 +done
   2.141 +
   2.142 +lemma int_of_real_sub: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> (int_of_real (a-b)) = (int_of_real a) - (int_of_real b)"
   2.143 +by (auto simp add: int_of_real_def real_is_int_def)
   2.144 +
   2.145 +lemma real_is_int_sub[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a-b)"
   2.146 +apply (subst real_is_int_def2)
   2.147 +apply (simp add: int_of_real_sub real_int_of_real)
   2.148 +done
   2.149 +
   2.150 +lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real a = x"
   2.151 +by (auto simp add: real_is_int_def)
   2.152 +
   2.153 +lemma int_of_real_mult:
   2.154 +  assumes "real_is_int a" "real_is_int b"
   2.155 +  shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)"
   2.156 +proof -
   2.157 +  from prems have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto)
   2.158 +  from prems have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto)
   2.159 +  from a obtain a'::int where a':"a = real a'" by auto
   2.160 +  from b obtain b'::int where b':"b = real b'" by auto
   2.161 +  have r: "real a' * real b' = real (a' * b')" by auto
   2.162 +  show ?thesis
   2.163 +    apply (simp add: a' b')
   2.164 +    apply (subst r)
   2.165 +    apply (simp only: int_of_real_real)
   2.166 +    done
   2.167 +qed
   2.168 +
   2.169 +lemma real_is_int_mult[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a*b)"
   2.170 +apply (subst real_is_int_def2)
   2.171 +apply (simp add: int_of_real_mult)
   2.172 +done
   2.173 +
   2.174 +lemma real_is_int_0[simp]: "real_is_int (0::real)"
   2.175 +by (simp add: real_is_int_def int_of_real_def)
   2.176 +
   2.177 +lemma real_is_int_1[simp]: "real_is_int (1::real)"
   2.178 +proof -
   2.179 +  have "real_is_int (1::real) = real_is_int(real (1::int))" by auto
   2.180 +  also have "\<dots> = True" by (simp only: real_is_int_real)
   2.181 +  ultimately show ?thesis by auto
   2.182 +qed
   2.183 +
   2.184 +lemma real_is_int_n1: "real_is_int (-1::real)"
   2.185 +proof -
   2.186 +  have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto
   2.187 +  also have "\<dots> = True" by (simp only: real_is_int_real)
   2.188 +  ultimately show ?thesis by auto
   2.189 +qed
   2.190 +
   2.191 +lemma real_is_int_number_of[simp]: "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
   2.192 +proof -
   2.193 +  have neg1: "real_is_int (-1::real)"
   2.194 +  proof -
   2.195 +    have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto
   2.196 +    also have "\<dots> = True" by (simp only: real_is_int_real)
   2.197 +    ultimately show ?thesis by auto
   2.198 +  qed
   2.199 +
   2.200 +  {
   2.201 +    fix x :: int
   2.202 +    have "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
   2.203 +      unfolding number_of_eq
   2.204 +      apply (induct x)
   2.205 +      apply (induct_tac n)
   2.206 +      apply (simp)
   2.207 +      apply (simp)
   2.208 +      apply (induct_tac n)
   2.209 +      apply (simp add: neg1)
   2.210 +    proof -
   2.211 +      fix n :: nat
   2.212 +      assume rn: "(real_is_int (of_int (- (int (Suc n)))))"
   2.213 +      have s: "-(int (Suc (Suc n))) = -1 + - (int (Suc n))" by simp
   2.214 +      show "real_is_int (of_int (- (int (Suc (Suc n)))))"
   2.215 +        apply (simp only: s of_int_add)
   2.216 +        apply (rule real_is_int_add)
   2.217 +        apply (simp add: neg1)
   2.218 +        apply (simp only: rn)
   2.219 +        done
   2.220 +    qed
   2.221 +  }
   2.222 +  note Abs_Bin = this
   2.223 +  {
   2.224 +    fix x :: int
   2.225 +    have "? u. x = u"
   2.226 +      apply (rule exI[where x = "x"])
   2.227 +      apply (simp)
   2.228 +      done
   2.229 +  }
   2.230 +  then obtain u::int where "x = u" by auto
   2.231 +  with Abs_Bin show ?thesis by auto
   2.232 +qed
   2.233 +
   2.234 +lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)"
   2.235 +by (simp add: int_of_real_def)
   2.236 +
   2.237 +lemma int_of_real_1[simp]: "int_of_real (1::real) = (1::int)"
   2.238 +proof -
   2.239 +  have 1: "(1::real) = real (1::int)" by auto
   2.240 +  show ?thesis by (simp only: 1 int_of_real_real)
   2.241 +qed
   2.242 +
   2.243 +lemma int_of_real_number_of[simp]: "int_of_real (number_of b) = number_of b"
   2.244 +proof -
   2.245 +  have "real_is_int (number_of b)" by simp
   2.246 +  then have uu: "?! u::int. number_of b = real u" by (auto simp add: real_is_int_rep)
   2.247 +  then obtain u::int where u:"number_of b = real u" by auto
   2.248 +  have "number_of b = real ((number_of b)::int)"
   2.249 +    by (simp add: number_of_eq real_of_int_def)
   2.250 +  have ub: "number_of b = real ((number_of b)::int)"
   2.251 +    by (simp add: number_of_eq real_of_int_def)
   2.252 +  from uu u ub have unb: "u = number_of b"
   2.253 +    by blast
   2.254 +  have "int_of_real (number_of b) = u" by (simp add: u)
   2.255 +  with unb show ?thesis by simp
   2.256 +qed
   2.257 +
   2.258 +lemma float_transfer_even: "even a \<Longrightarrow> float (a, b) = float (a div 2, b+1)"
   2.259 +  apply (subst float_transfer[where a="a" and b="b" and c="-1", simplified])
   2.260 +  apply (simp_all add: pow2_def even_def real_is_int_def algebra_simps)
   2.261 +  apply (auto)
   2.262 +proof -
   2.263 +  fix q::int
   2.264 +  have a:"b - (-1\<Colon>int) = (1\<Colon>int) + b" by arith
   2.265 +  show "(float (q, (b - (-1\<Colon>int)))) = (float (q, ((1\<Colon>int) + b)))"
   2.266 +    by (simp add: a)
   2.267 +qed
   2.268 +
   2.269 +lemma int_div_zdiv: "int (a div b) = (int a) div (int b)"
   2.270 +by (rule zdiv_int)
   2.271 +
   2.272 +lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)"
   2.273 +by (rule zmod_int)
   2.274 +
   2.275 +lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
   2.276 +by arith
   2.277 +
   2.278 +function norm_float :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
   2.279 +  "norm_float a b = (if a \<noteq> 0 \<and> even a then norm_float (a div 2) (b + 1)
   2.280 +    else if a = 0 then (0, 0) else (a, b))"
   2.281 +by auto
   2.282 +
   2.283 +termination by (relation "measure (nat o abs o fst)")
   2.284 +  (auto intro: abs_div_2_less)
   2.285 +
   2.286 +lemma norm_float: "float x = float (split norm_float x)"
   2.287 +proof -
   2.288 +  {
   2.289 +    fix a b :: int
   2.290 +    have norm_float_pair: "float (a, b) = float (norm_float a b)"
   2.291 +    proof (induct a b rule: norm_float.induct)
   2.292 +      case (1 u v)
   2.293 +      show ?case
   2.294 +      proof cases
   2.295 +        assume u: "u \<noteq> 0 \<and> even u"
   2.296 +        with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto
   2.297 +        with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
   2.298 +        then show ?thesis
   2.299 +          apply (subst norm_float.simps)
   2.300 +          apply (simp add: ind)
   2.301 +          done
   2.302 +      next
   2.303 +        assume "~(u \<noteq> 0 \<and> even u)"
   2.304 +        then show ?thesis
   2.305 +          by (simp add: prems float_def)
   2.306 +      qed
   2.307 +    qed
   2.308 +  }
   2.309 +  note helper = this
   2.310 +  have "? a b. x = (a,b)" by auto
   2.311 +  then obtain a b where "x = (a, b)" by blast
   2.312 +  then show ?thesis by (simp add: helper)
   2.313 +qed
   2.314 +
   2.315 +lemma float_add_l0: "float (0, e) + x = x"
   2.316 +  by (simp add: float_def)
   2.317 +
   2.318 +lemma float_add_r0: "x + float (0, e) = x"
   2.319 +  by (simp add: float_def)
   2.320 +
   2.321 +lemma float_add:
   2.322 +  "float (a1, e1) + float (a2, e2) =
   2.323 +  (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
   2.324 +  else float (a1*2^(nat (e1-e2))+a2, e2))"
   2.325 +  apply (simp add: float_def algebra_simps)
   2.326 +  apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric])
   2.327 +  done
   2.328 +
   2.329 +lemma float_add_assoc1:
   2.330 +  "(x + float (y1, e1)) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x"
   2.331 +  by simp
   2.332 +
   2.333 +lemma float_add_assoc2:
   2.334 +  "(float (y1, e1) + x) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x"
   2.335 +  by simp
   2.336 +
   2.337 +lemma float_add_assoc3:
   2.338 +  "float (y1, e1) + (x + float (y2, e2)) = (float (y1, e1) + float (y2, e2)) + x"
   2.339 +  by simp
   2.340 +
   2.341 +lemma float_add_assoc4:
   2.342 +  "float (y1, e1) + (float (y2, e2) + x) = (float (y1, e1) + float (y2, e2)) + x"
   2.343 +  by simp
   2.344 +
   2.345 +lemma float_mult_l0: "float (0, e) * x = float (0, 0)"
   2.346 +  by (simp add: float_def)
   2.347 +
   2.348 +lemma float_mult_r0: "x * float (0, e) = float (0, 0)"
   2.349 +  by (simp add: float_def)
   2.350 +
   2.351 +definition 
   2.352 +  lbound :: "real \<Rightarrow> real"
   2.353 +where
   2.354 +  "lbound x = min 0 x"
   2.355 +
   2.356 +definition
   2.357 +  ubound :: "real \<Rightarrow> real"
   2.358 +where
   2.359 +  "ubound x = max 0 x"
   2.360 +
   2.361 +lemma lbound: "lbound x \<le> x"   
   2.362 +  by (simp add: lbound_def)
   2.363 +
   2.364 +lemma ubound: "x \<le> ubound x"
   2.365 +  by (simp add: ubound_def)
   2.366 +
   2.367 +lemma float_mult:
   2.368 +  "float (a1, e1) * float (a2, e2) =
   2.369 +  (float (a1 * a2, e1 + e2))"
   2.370 +  by (simp add: float_def pow2_add)
   2.371 +
   2.372 +lemma float_minus:
   2.373 +  "- (float (a,b)) = float (-a, b)"
   2.374 +  by (simp add: float_def)
   2.375 +
   2.376 +lemma zero_less_pow2:
   2.377 +  "0 < pow2 x"
   2.378 +proof -
   2.379 +  {
   2.380 +    fix y
   2.381 +    have "0 <= y \<Longrightarrow> 0 < pow2 y"
   2.382 +      by (induct y, induct_tac n, simp_all add: pow2_add)
   2.383 +  }
   2.384 +  note helper=this
   2.385 +  show ?thesis
   2.386 +    apply (case_tac "0 <= x")
   2.387 +    apply (simp add: helper)
   2.388 +    apply (subst pow2_neg)
   2.389 +    apply (simp add: helper)
   2.390 +    done
   2.391 +qed
   2.392 +
   2.393 +lemma zero_le_float:
   2.394 +  "(0 <= float (a,b)) = (0 <= a)"
   2.395 +  apply (auto simp add: float_def)
   2.396 +  apply (auto simp add: zero_le_mult_iff zero_less_pow2)
   2.397 +  apply (insert zero_less_pow2[of b])
   2.398 +  apply (simp_all)
   2.399 +  done
   2.400 +
   2.401 +lemma float_le_zero:
   2.402 +  "(float (a,b) <= 0) = (a <= 0)"
   2.403 +  apply (auto simp add: float_def)
   2.404 +  apply (auto simp add: mult_le_0_iff)
   2.405 +  apply (insert zero_less_pow2[of b])
   2.406 +  apply auto
   2.407 +  done
   2.408 +
   2.409 +lemma float_abs:
   2.410 +  "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
   2.411 +  apply (auto simp add: abs_if)
   2.412 +  apply (simp_all add: zero_le_float[symmetric, of a b] float_minus)
   2.413 +  done
   2.414 +
   2.415 +lemma float_zero:
   2.416 +  "float (0, b) = 0"
   2.417 +  by (simp add: float_def)
   2.418 +
   2.419 +lemma float_pprt:
   2.420 +  "pprt (float (a, b)) = (if 0 <= a then (float (a,b)) else (float (0, b)))"
   2.421 +  by (auto simp add: zero_le_float float_le_zero float_zero)
   2.422 +
   2.423 +lemma pprt_lbound: "pprt (lbound x) = float (0, 0)"
   2.424 +  apply (simp add: float_def)
   2.425 +  apply (rule pprt_eq_0)
   2.426 +  apply (simp add: lbound_def)
   2.427 +  done
   2.428 +
   2.429 +lemma nprt_ubound: "nprt (ubound x) = float (0, 0)"
   2.430 +  apply (simp add: float_def)
   2.431 +  apply (rule nprt_eq_0)
   2.432 +  apply (simp add: ubound_def)
   2.433 +  done
   2.434 +
   2.435 +lemma float_nprt:
   2.436 +  "nprt (float (a, b)) = (if 0 <= a then (float (0,b)) else (float (a, b)))"
   2.437 +  by (auto simp add: zero_le_float float_le_zero float_zero)
   2.438 +
   2.439 +lemma norm_0_1: "(0::_::number_ring) = Numeral0 & (1::_::number_ring) = Numeral1"
   2.440 +  by auto
   2.441 +
   2.442 +lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
   2.443 +  by simp
   2.444 +
   2.445 +lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)"
   2.446 +  by simp
   2.447 +
   2.448 +lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
   2.449 +  by simp
   2.450 +
   2.451 +lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
   2.452 +  by simp
   2.453 +
   2.454 +lemma int_pow_0: "(a::int)^(Numeral0) = 1"
   2.455 +  by simp
   2.456 +
   2.457 +lemma int_pow_1: "(a::int)^(Numeral1) = a"
   2.458 +  by simp
   2.459 +
   2.460 +lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0"
   2.461 +  by simp
   2.462 +
   2.463 +lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1"
   2.464 +  by simp
   2.465 +
   2.466 +lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0"
   2.467 +  by simp
   2.468 +
   2.469 +lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
   2.470 +  by simp
   2.471 +
   2.472 +lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1"
   2.473 +  by simp
   2.474 +
   2.475 +lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1"
   2.476 +proof -
   2.477 +  have 1:"((-1)::nat) = 0"
   2.478 +    by simp
   2.479 +  show ?thesis by (simp add: 1)
   2.480 +qed
   2.481 +
   2.482 +lemma fst_cong: "a=a' \<Longrightarrow> fst (a,b) = fst (a',b)"
   2.483 +  by simp
   2.484 +
   2.485 +lemma snd_cong: "b=b' \<Longrightarrow> snd (a,b) = snd (a,b')"
   2.486 +  by simp
   2.487 +
   2.488 +lemma lift_bool: "x \<Longrightarrow> x=True"
   2.489 +  by simp
   2.490 +
   2.491 +lemma nlift_bool: "~x \<Longrightarrow> x=False"
   2.492 +  by simp
   2.493 +
   2.494 +lemma not_false_eq_true: "(~ False) = True" by simp
   2.495 +
   2.496 +lemma not_true_eq_false: "(~ True) = False" by simp
   2.497 +
   2.498 +lemmas binarith =
   2.499 +  normalize_bin_simps
   2.500 +  pred_bin_simps succ_bin_simps
   2.501 +  add_bin_simps minus_bin_simps mult_bin_simps
   2.502 +
   2.503 +lemma int_eq_number_of_eq:
   2.504 +  "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)"
   2.505 +  by (rule eq_number_of_eq)
   2.506 +
   2.507 +lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
   2.508 +  by (simp only: iszero_number_of_Pls)
   2.509 +
   2.510 +lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
   2.511 +  by simp
   2.512 +
   2.513 +lemma int_iszero_number_of_Bit0: "iszero ((number_of (Int.Bit0 w))::int) = iszero ((number_of w)::int)"
   2.514 +  by simp
   2.515 +
   2.516 +lemma int_iszero_number_of_Bit1: "\<not> iszero ((number_of (Int.Bit1 w))::int)"
   2.517 +  by simp
   2.518 +
   2.519 +lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
   2.520 +  unfolding neg_def number_of_is_id by simp
   2.521 +
   2.522 +lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
   2.523 +  by simp
   2.524 +
   2.525 +lemma int_neg_number_of_Min: "neg (-1::int)"
   2.526 +  by simp
   2.527 +
   2.528 +lemma int_neg_number_of_Bit0: "neg ((number_of (Int.Bit0 w))::int) = neg ((number_of w)::int)"
   2.529 +  by simp
   2.530 +
   2.531 +lemma int_neg_number_of_Bit1: "neg ((number_of (Int.Bit1 w))::int) = neg ((number_of w)::int)"
   2.532 +  by simp
   2.533 +
   2.534 +lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
   2.535 +  unfolding neg_def number_of_is_id by (simp add: not_less)
   2.536 +
   2.537 +lemmas intarithrel =
   2.538 +  int_eq_number_of_eq
   2.539 +  lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_Bit0
   2.540 +  lift_bool[OF int_iszero_number_of_Bit1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
   2.541 +  int_neg_number_of_Bit0 int_neg_number_of_Bit1 int_le_number_of_eq
   2.542 +
   2.543 +lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
   2.544 +  by simp
   2.545 +
   2.546 +lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
   2.547 +  by simp
   2.548 +
   2.549 +lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (v * w)"
   2.550 +  by simp
   2.551 +
   2.552 +lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
   2.553 +  by simp
   2.554 +
   2.555 +lemmas intarith = int_number_of_add_sym int_number_of_minus_sym int_number_of_diff_sym int_number_of_mult_sym
   2.556 +
   2.557 +lemmas natarith = add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
   2.558 +
   2.559 +lemmas powerarith = nat_number_of zpower_number_of_even
   2.560 +  zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
   2.561 +  zpower_Pls zpower_Min
   2.562 +
   2.563 +lemmas floatarith[simplified norm_0_1] = float_add float_add_l0 float_add_r0 float_mult float_mult_l0 float_mult_r0 
   2.564 +          float_minus float_abs zero_le_float float_pprt float_nprt pprt_lbound nprt_ubound
   2.565 +
   2.566 +(* for use with the compute oracle *)
   2.567 +lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false
   2.568 +
   2.569 +use "~~/src/HOL/Tools/float_arith.ML"
   2.570 +
   2.571 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Matrix/ComputeHOL.thy	Wed Sep 02 16:25:44 2009 +0200
     3.3 @@ -0,0 +1,191 @@
     3.4 +theory ComputeHOL
     3.5 +imports Complex_Main "~~/src/Tools/Compute_Oracle/Compute_Oracle"
     3.6 +begin
     3.7 +
     3.8 +lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq)
     3.9 +lemma meta_eq_trivial: "x == y \<Longrightarrow> x == y" by simp
    3.10 +lemma meta_eq_imp_eq: "x == y \<Longrightarrow> x = y" by auto
    3.11 +lemma eq_trivial: "x = y \<Longrightarrow> x = y" by auto
    3.12 +lemma bool_to_true: "x :: bool \<Longrightarrow> x == True"  by simp
    3.13 +lemma transmeta_1: "x = y \<Longrightarrow> y == z \<Longrightarrow> x = z" by simp
    3.14 +lemma transmeta_2: "x == y \<Longrightarrow> y = z \<Longrightarrow> x = z" by simp
    3.15 +lemma transmeta_3: "x == y \<Longrightarrow> y == z \<Longrightarrow> x = z" by simp
    3.16 +
    3.17 +
    3.18 +(**** compute_if ****)
    3.19 +
    3.20 +lemma If_True: "If True = (\<lambda> x y. x)" by ((rule ext)+,auto)
    3.21 +lemma If_False: "If False = (\<lambda> x y. y)" by ((rule ext)+, auto)
    3.22 +
    3.23 +lemmas compute_if = If_True If_False
    3.24 +
    3.25 +(**** compute_bool ****)
    3.26 +
    3.27 +lemma bool1: "(\<not> True) = False"  by blast
    3.28 +lemma bool2: "(\<not> False) = True"  by blast
    3.29 +lemma bool3: "(P \<and> True) = P" by blast
    3.30 +lemma bool4: "(True \<and> P) = P" by blast
    3.31 +lemma bool5: "(P \<and> False) = False" by blast
    3.32 +lemma bool6: "(False \<and> P) = False" by blast
    3.33 +lemma bool7: "(P \<or> True) = True" by blast
    3.34 +lemma bool8: "(True \<or> P) = True" by blast
    3.35 +lemma bool9: "(P \<or> False) = P" by blast
    3.36 +lemma bool10: "(False \<or> P) = P" by blast
    3.37 +lemma bool11: "(True \<longrightarrow> P) = P" by blast
    3.38 +lemma bool12: "(P \<longrightarrow> True) = True" by blast
    3.39 +lemma bool13: "(True \<longrightarrow> P) = P" by blast
    3.40 +lemma bool14: "(P \<longrightarrow> False) = (\<not> P)" by blast
    3.41 +lemma bool15: "(False \<longrightarrow> P) = True" by blast
    3.42 +lemma bool16: "(False = False) = True" by blast
    3.43 +lemma bool17: "(True = True) = True" by blast
    3.44 +lemma bool18: "(False = True) = False" by blast
    3.45 +lemma bool19: "(True = False) = False" by blast
    3.46 +
    3.47 +lemmas compute_bool = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10 bool11 bool12 bool13 bool14 bool15 bool16 bool17 bool18 bool19
    3.48 +
    3.49 +
    3.50 +(*** compute_pair ***)
    3.51 +
    3.52 +lemma compute_fst: "fst (x,y) = x" by simp
    3.53 +lemma compute_snd: "snd (x,y) = y" by simp
    3.54 +lemma compute_pair_eq: "((a, b) = (c, d)) = (a = c \<and> b = d)" by auto
    3.55 +
    3.56 +lemma prod_case_simp: "prod_case f (x,y) = f x y" by simp
    3.57 +
    3.58 +lemmas compute_pair = compute_fst compute_snd compute_pair_eq prod_case_simp
    3.59 +
    3.60 +(*** compute_option ***)
    3.61 +
    3.62 +lemma compute_the: "the (Some x) = x" by simp
    3.63 +lemma compute_None_Some_eq: "(None = Some x) = False" by auto
    3.64 +lemma compute_Some_None_eq: "(Some x = None) = False" by auto
    3.65 +lemma compute_None_None_eq: "(None = None) = True" by auto
    3.66 +lemma compute_Some_Some_eq: "(Some x = Some y) = (x = y)" by auto
    3.67 +
    3.68 +definition
    3.69 +   option_case_compute :: "'b option \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    3.70 +where
    3.71 +   "option_case_compute opt a f = option_case a f opt"
    3.72 +
    3.73 +lemma option_case_compute: "option_case = (\<lambda> a f opt. option_case_compute opt a f)"
    3.74 +  by (simp add: option_case_compute_def)
    3.75 +
    3.76 +lemma option_case_compute_None: "option_case_compute None = (\<lambda> a f. a)"
    3.77 +  apply (rule ext)+
    3.78 +  apply (simp add: option_case_compute_def)
    3.79 +  done
    3.80 +
    3.81 +lemma option_case_compute_Some: "option_case_compute (Some x) = (\<lambda> a f. f x)"
    3.82 +  apply (rule ext)+
    3.83 +  apply (simp add: option_case_compute_def)
    3.84 +  done
    3.85 +
    3.86 +lemmas compute_option_case = option_case_compute option_case_compute_None option_case_compute_Some
    3.87 +
    3.88 +lemmas compute_option = compute_the compute_None_Some_eq compute_Some_None_eq compute_None_None_eq compute_Some_Some_eq compute_option_case
    3.89 +
    3.90 +(**** compute_list_length ****)
    3.91 +
    3.92 +lemma length_cons:"length (x#xs) = 1 + (length xs)"
    3.93 +  by simp
    3.94 +
    3.95 +lemma length_nil: "length [] = 0"
    3.96 +  by simp
    3.97 +
    3.98 +lemmas compute_list_length = length_nil length_cons
    3.99 +
   3.100 +(*** compute_list_case ***)
   3.101 +
   3.102 +definition
   3.103 +  list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
   3.104 +where
   3.105 +  "list_case_compute l a f = list_case a f l"
   3.106 +
   3.107 +lemma list_case_compute: "list_case = (\<lambda> (a::'a) f (l::'b list). list_case_compute l a f)"
   3.108 +  apply (rule ext)+
   3.109 +  apply (simp add: list_case_compute_def)
   3.110 +  done
   3.111 +
   3.112 +lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\<lambda> (a::'a) f. a)"
   3.113 +  apply (rule ext)+
   3.114 +  apply (simp add: list_case_compute_def)
   3.115 +  done
   3.116 +
   3.117 +lemma list_case_compute_cons: "list_case_compute (u#v) = (\<lambda> (a::'a) f. (f (u::'b) v))"
   3.118 +  apply (rule ext)+
   3.119 +  apply (simp add: list_case_compute_def)
   3.120 +  done
   3.121 +
   3.122 +lemmas compute_list_case = list_case_compute list_case_compute_empty list_case_compute_cons
   3.123 +
   3.124 +(*** compute_list_nth ***)
   3.125 +(* Of course, you will need computation with nats for this to work \<dots> *)
   3.126 +
   3.127 +lemma compute_list_nth: "((x#xs) ! n) = (if n = 0 then x else (xs ! (n - 1)))"
   3.128 +  by (cases n, auto)
   3.129 +  
   3.130 +(*** compute_list ***)
   3.131 +
   3.132 +lemmas compute_list = compute_list_case compute_list_length compute_list_nth
   3.133 +
   3.134 +(*** compute_let ***)
   3.135 +
   3.136 +lemmas compute_let = Let_def
   3.137 +
   3.138 +(***********************)
   3.139 +(* Everything together *)
   3.140 +(***********************)
   3.141 +
   3.142 +lemmas compute_hol = compute_if compute_bool compute_pair compute_option compute_list compute_let
   3.143 +
   3.144 +ML {*
   3.145 +signature ComputeHOL =
   3.146 +sig
   3.147 +  val prep_thms : thm list -> thm list
   3.148 +  val to_meta_eq : thm -> thm
   3.149 +  val to_hol_eq : thm -> thm
   3.150 +  val symmetric : thm -> thm 
   3.151 +  val trans : thm -> thm -> thm
   3.152 +end
   3.153 +
   3.154 +structure ComputeHOL : ComputeHOL =
   3.155 +struct
   3.156 +
   3.157 +local
   3.158 +fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq));
   3.159 +in
   3.160 +fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [])
   3.161 +  | rewrite_conv (eq :: eqs) ct =
   3.162 +      Thm.instantiate (Thm.match (lhs_of eq, ct)) eq
   3.163 +      handle Pattern.MATCH => rewrite_conv eqs ct;
   3.164 +end
   3.165 +
   3.166 +val convert_conditions = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.try_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}])))
   3.167 +
   3.168 +val eq_th = @{thm "HOL.eq_reflection"}
   3.169 +val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"}
   3.170 +val bool_to_true = @{thm "ComputeHOL.bool_to_true"}
   3.171 +
   3.172 +fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th]
   3.173 +
   3.174 +fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] 
   3.175 +
   3.176 +fun prep_thms ths = map (convert_conditions o to_meta_eq) ths
   3.177 +
   3.178 +fun symmetric th = @{thm "HOL.sym"} OF [th] handle THM _ => @{thm "Pure.symmetric"} OF [th]
   3.179 +
   3.180 +local
   3.181 +    val trans_HOL = @{thm "HOL.trans"}
   3.182 +    val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"}
   3.183 +    val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"}
   3.184 +    val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"}
   3.185 +    fun tr [] th1 th2 = trans_HOL OF [th1, th2]
   3.186 +      | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) 
   3.187 +in
   3.188 +  fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2
   3.189 +end
   3.190 +
   3.191 +end
   3.192 +*}
   3.193 +
   3.194 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Matrix/ComputeNumeral.thy	Wed Sep 02 16:25:44 2009 +0200
     4.3 @@ -0,0 +1,195 @@
     4.4 +theory ComputeNumeral
     4.5 +imports ComputeHOL ComputeFloat
     4.6 +begin
     4.7 +
     4.8 +(* normalization of bit strings *)
     4.9 +lemmas bitnorm = normalize_bin_simps
    4.10 +
    4.11 +(* neg for bit strings *)
    4.12 +lemma neg1: "neg Int.Pls = False" by (simp add: Int.Pls_def)
    4.13 +lemma neg2: "neg Int.Min = True" apply (subst Int.Min_def) by auto
    4.14 +lemma neg3: "neg (Int.Bit0 x) = neg x" apply (simp add: neg_def) apply (subst Bit0_def) by auto
    4.15 +lemma neg4: "neg (Int.Bit1 x) = neg x" apply (simp add: neg_def) apply (subst Bit1_def) by auto  
    4.16 +lemmas bitneg = neg1 neg2 neg3 neg4
    4.17 +
    4.18 +(* iszero for bit strings *)
    4.19 +lemma iszero1: "iszero Int.Pls = True" by (simp add: Int.Pls_def iszero_def)
    4.20 +lemma iszero2: "iszero Int.Min = False" apply (subst Int.Min_def) apply (subst iszero_def) by simp
    4.21 +lemma iszero3: "iszero (Int.Bit0 x) = iszero x" apply (subst Int.Bit0_def) apply (subst iszero_def)+ by auto
    4.22 +lemma iszero4: "iszero (Int.Bit1 x) = False" apply (subst Int.Bit1_def) apply (subst iszero_def)+  apply simp by arith
    4.23 +lemmas bitiszero = iszero1 iszero2 iszero3 iszero4
    4.24 +
    4.25 +(* lezero for bit strings *)
    4.26 +constdefs
    4.27 +  "lezero x == (x \<le> 0)"
    4.28 +lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto
    4.29 +lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto
    4.30 +lemma lezero3: "lezero (Int.Bit0 x) = lezero x" unfolding Int.Bit0_def lezero_def by auto
    4.31 +lemma lezero4: "lezero (Int.Bit1 x) = neg x" unfolding Int.Bit1_def lezero_def neg_def by auto
    4.32 +lemmas bitlezero = lezero1 lezero2 lezero3 lezero4
    4.33 +
    4.34 +(* equality for bit strings *)
    4.35 +lemmas biteq = eq_bin_simps
    4.36 +
    4.37 +(* x < y for bit strings *)
    4.38 +lemmas bitless = less_bin_simps
    4.39 +
    4.40 +(* x \<le> y for bit strings *)
    4.41 +lemmas bitle = le_bin_simps
    4.42 +
    4.43 +(* succ for bit strings *)
    4.44 +lemmas bitsucc = succ_bin_simps
    4.45 +
    4.46 +(* pred for bit strings *)
    4.47 +lemmas bitpred = pred_bin_simps
    4.48 +
    4.49 +(* unary minus for bit strings *)
    4.50 +lemmas bituminus = minus_bin_simps
    4.51 +
    4.52 +(* addition for bit strings *)
    4.53 +lemmas bitadd = add_bin_simps
    4.54 +
    4.55 +(* multiplication for bit strings *) 
    4.56 +lemma mult_Pls_right: "x * Int.Pls = Int.Pls" by (simp add: Pls_def)
    4.57 +lemma mult_Min_right: "x * Int.Min = - x" by (subst mult_commute, simp add: mult_Min)
    4.58 +lemma multb0x: "(Int.Bit0 x) * y = Int.Bit0 (x * y)" by (rule mult_Bit0)
    4.59 +lemma multxb0: "x * (Int.Bit0 y) = Int.Bit0 (x * y)" unfolding Bit0_def by simp
    4.60 +lemma multb1: "(Int.Bit1 x) * (Int.Bit1 y) = Int.Bit1 (Int.Bit0 (x * y) + x + y)"
    4.61 +  unfolding Bit0_def Bit1_def by (simp add: algebra_simps)
    4.62 +lemmas bitmul = mult_Pls mult_Min mult_Pls_right mult_Min_right multb0x multxb0 multb1
    4.63 +
    4.64 +lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul 
    4.65 +
    4.66 +constdefs 
    4.67 +  "nat_norm_number_of (x::nat) == x"
    4.68 +
    4.69 +lemma nat_norm_number_of: "nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)"
    4.70 +  apply (simp add: nat_norm_number_of_def)
    4.71 +  unfolding lezero_def iszero_def neg_def
    4.72 +  apply (simp add: numeral_simps)
    4.73 +  done
    4.74 +
    4.75 +(* Normalization of nat literals *)
    4.76 +lemma natnorm0: "(0::nat) = number_of (Int.Pls)" by auto
    4.77 +lemma natnorm1: "(1 :: nat) = number_of (Int.Bit1 Int.Pls)"  by auto 
    4.78 +lemmas natnorm = natnorm0 natnorm1 nat_norm_number_of
    4.79 +
    4.80 +(* Suc *)
    4.81 +lemma natsuc: "Suc (number_of x) = (if neg x then 1 else number_of (Int.succ x))" by (auto simp add: number_of_is_id)
    4.82 +
    4.83 +(* Addition for nat *)
    4.84 +lemma natadd: "number_of x + ((number_of y)::nat) = (if neg x then (number_of y) else (if neg y then number_of x else (number_of (x + y))))"
    4.85 +  unfolding nat_number_of_def number_of_is_id neg_def
    4.86 +  by auto
    4.87 +
    4.88 +(* Subtraction for nat *)
    4.89 +lemma natsub: "(number_of x) - ((number_of y)::nat) = 
    4.90 +  (if neg x then 0 else (if neg y then number_of x else (nat_norm_number_of (number_of (x + (- y))))))"
    4.91 +  unfolding nat_norm_number_of
    4.92 +  by (auto simp add: number_of_is_id neg_def lezero_def iszero_def Let_def nat_number_of_def)
    4.93 +
    4.94 +(* Multiplication for nat *)
    4.95 +lemma natmul: "(number_of x) * ((number_of y)::nat) = 
    4.96 +  (if neg x then 0 else (if neg y then 0 else number_of (x * y)))"
    4.97 +  unfolding nat_number_of_def number_of_is_id neg_def
    4.98 +  by (simp add: nat_mult_distrib)
    4.99 +
   4.100 +lemma nateq: "(((number_of x)::nat) = (number_of y)) = ((lezero x \<and> lezero y) \<or> (x = y))"
   4.101 +  by (auto simp add: iszero_def lezero_def neg_def number_of_is_id)
   4.102 +
   4.103 +lemma natless: "(((number_of x)::nat) < (number_of y)) = ((x < y) \<and> (\<not> (lezero y)))"
   4.104 +  by (simp add: lezero_def numeral_simps not_le)
   4.105 +
   4.106 +lemma natle: "(((number_of x)::nat) \<le> (number_of y)) = (y < x \<longrightarrow> lezero x)"
   4.107 +  by (auto simp add: number_of_is_id lezero_def nat_number_of_def)
   4.108 +
   4.109 +fun natfac :: "nat \<Rightarrow> nat"
   4.110 +where
   4.111 +   "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))"
   4.112 +
   4.113 +lemmas compute_natarith = bitarith natnorm natsuc natadd natsub natmul nateq natless natle natfac.simps
   4.114 +
   4.115 +lemma number_eq: "(((number_of x)::'a::{number_ring, ordered_idom}) = (number_of y)) = (x = y)"
   4.116 +  unfolding number_of_eq
   4.117 +  apply simp
   4.118 +  done
   4.119 +
   4.120 +lemma number_le: "(((number_of x)::'a::{number_ring, ordered_idom}) \<le>  (number_of y)) = (x \<le> y)"
   4.121 +  unfolding number_of_eq
   4.122 +  apply simp
   4.123 +  done
   4.124 +
   4.125 +lemma number_less: "(((number_of x)::'a::{number_ring, ordered_idom}) <  (number_of y)) = (x < y)"
   4.126 +  unfolding number_of_eq 
   4.127 +  apply simp
   4.128 +  done
   4.129 +
   4.130 +lemma number_diff: "((number_of x)::'a::{number_ring, ordered_idom}) - number_of y = number_of (x + (- y))"
   4.131 +  apply (subst diff_number_of_eq)
   4.132 +  apply simp
   4.133 +  done
   4.134 +
   4.135 +lemmas number_norm = number_of_Pls[symmetric] numeral_1_eq_1[symmetric]
   4.136 +
   4.137 +lemmas compute_numberarith = number_of_minus[symmetric] number_of_add[symmetric] number_diff number_of_mult[symmetric] number_norm number_eq number_le number_less
   4.138 +
   4.139 +lemma compute_real_of_nat_number_of: "real ((number_of v)::nat) = (if neg v then 0 else number_of v)"
   4.140 +  by (simp only: real_of_nat_number_of number_of_is_id)
   4.141 +
   4.142 +lemma compute_nat_of_int_number_of: "nat ((number_of v)::int) = (number_of v)"
   4.143 +  by simp
   4.144 +
   4.145 +lemmas compute_num_conversions = compute_real_of_nat_number_of compute_nat_of_int_number_of real_number_of
   4.146 +
   4.147 +lemmas zpowerarith = zpower_number_of_even
   4.148 +  zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
   4.149 +  zpower_Pls zpower_Min
   4.150 +
   4.151 +(* div, mod *)
   4.152 +
   4.153 +lemma adjust: "adjust b (q, r) = (if 0 \<le> r - b then (2 * q + 1, r - b) else (2 * q, r))"
   4.154 +  by (auto simp only: adjust_def)
   4.155 +
   4.156 +lemma negateSnd: "negateSnd (q, r) = (q, -r)" 
   4.157 +  by (simp add: negateSnd_def)
   4.158 +
   4.159 +lemma divmod: "IntDiv.divmod a b = (if 0\<le>a then
   4.160 +                  if 0\<le>b then posDivAlg a b
   4.161 +                  else if a=0 then (0, 0)
   4.162 +                       else negateSnd (negDivAlg (-a) (-b))
   4.163 +               else 
   4.164 +                  if 0<b then negDivAlg a b
   4.165 +                  else negateSnd (posDivAlg (-a) (-b)))"
   4.166 +  by (auto simp only: IntDiv.divmod_def)
   4.167 +
   4.168 +lemmas compute_div_mod = div_def mod_def divmod adjust negateSnd posDivAlg.simps negDivAlg.simps
   4.169 +
   4.170 +
   4.171 +
   4.172 +(* collecting all the theorems *)
   4.173 +
   4.174 +lemma even_Pls: "even (Int.Pls) = True"
   4.175 +  apply (unfold Pls_def even_def)
   4.176 +  by simp
   4.177 +
   4.178 +lemma even_Min: "even (Int.Min) = False"
   4.179 +  apply (unfold Min_def even_def)
   4.180 +  by simp
   4.181 +
   4.182 +lemma even_B0: "even (Int.Bit0 x) = True"
   4.183 +  apply (unfold Bit0_def)
   4.184 +  by simp
   4.185 +
   4.186 +lemma even_B1: "even (Int.Bit1 x) = False"
   4.187 +  apply (unfold Bit1_def)
   4.188 +  by simp
   4.189 +
   4.190 +lemma even_number_of: "even ((number_of w)::int) = even w"
   4.191 +  by (simp only: number_of_is_id)
   4.192 +
   4.193 +lemmas compute_even = even_Pls even_Min even_B0 even_B1 even_number_of
   4.194 +
   4.195 +lemmas compute_numeral = compute_if compute_let compute_pair compute_bool 
   4.196 +                         compute_natarith compute_numberarith max_def min_def compute_num_conversions zpowerarith compute_div_mod compute_even
   4.197 +
   4.198 +end
     5.1 --- a/src/HOL/Matrix/LP.thy	Wed Sep 02 14:11:45 2009 +0200
     5.2 +++ b/src/HOL/Matrix/LP.thy	Wed Sep 02 16:25:44 2009 +0200
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/Matrix/LP.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Steven Obua
     5.7  *)
     5.8  
     6.1 --- a/src/HOL/Matrix/Matrix.thy	Wed Sep 02 14:11:45 2009 +0200
     6.2 +++ b/src/HOL/Matrix/Matrix.thy	Wed Sep 02 16:25:44 2009 +0200
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      HOL/Matrix/Matrix.thy
     6.5 -    ID:         $Id$
     6.6      Author:     Steven Obua
     6.7  *)
     6.8  
     7.1 --- a/src/HOL/Matrix/ROOT.ML	Wed Sep 02 14:11:45 2009 +0200
     7.2 +++ b/src/HOL/Matrix/ROOT.ML	Wed Sep 02 16:25:44 2009 +0200
     7.3 @@ -1,5 +1,1 @@
     7.4 -(*  Title:      HOL/Matrix/ROOT.ML
     7.5 -    ID:         $Id$
     7.6 -*)
     7.7 -
     7.8  use_thys ["SparseMatrix", "cplex/Cplex"];
     8.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Wed Sep 02 14:11:45 2009 +0200
     8.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Wed Sep 02 16:25:44 2009 +0200
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      HOL/Matrix/SparseMatrix.thy
     8.5 -    ID:         $Id$
     8.6      Author:     Steven Obua
     8.7  *)
     8.8  
     9.1 --- a/src/HOL/Matrix/cplex/Cplex.thy	Wed Sep 02 14:11:45 2009 +0200
     9.2 +++ b/src/HOL/Matrix/cplex/Cplex.thy	Wed Sep 02 16:25:44 2009 +0200
     9.3 @@ -1,10 +1,9 @@
     9.4  (*  Title:      HOL/Matrix/cplex/Cplex.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Steven Obua
     9.7  *)
     9.8  
     9.9  theory Cplex 
    9.10 -imports SparseMatrix LP "~~/src/HOL/Tools/ComputeFloat" "~~/src/HOL/Tools/ComputeNumeral"
    9.11 +imports SparseMatrix LP ComputeFloat ComputeNumeral
    9.12  uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML"
    9.13    "fspmlp.ML" ("matrixlp.ML")
    9.14  begin
    10.1 --- a/src/HOL/Matrix/cplex/CplexMatrixConverter.ML	Wed Sep 02 14:11:45 2009 +0200
    10.2 +++ b/src/HOL/Matrix/cplex/CplexMatrixConverter.ML	Wed Sep 02 16:25:44 2009 +0200
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOL/Matrix/cplex/CplexMatrixConverter.ML
    10.5 -    ID:         $Id$
    10.6      Author:     Steven Obua
    10.7  *)
    10.8  
    11.1 --- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Wed Sep 02 14:11:45 2009 +0200
    11.2 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Wed Sep 02 16:25:44 2009 +0200
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      HOL/Matrix/cplex/Cplex_tools.ML
    11.5 -    ID:         $Id$
    11.6      Author:     Steven Obua
    11.7  *)
    11.8  
    12.1 --- a/src/HOL/Tools/ComputeFloat.thy	Wed Sep 02 14:11:45 2009 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,568 +0,0 @@
    12.4 -(*  Title:  HOL/Tools/ComputeFloat.thy
    12.5 -    Author: Steven Obua
    12.6 -*)
    12.7 -
    12.8 -header {* Floating Point Representation of the Reals *}
    12.9 -
   12.10 -theory ComputeFloat
   12.11 -imports Complex_Main
   12.12 -uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
   12.13 -begin
   12.14 -
   12.15 -definition
   12.16 -  pow2 :: "int \<Rightarrow> real" where
   12.17 -  "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
   12.18 -
   12.19 -definition
   12.20 -  float :: "int * int \<Rightarrow> real" where
   12.21 -  "float x = real (fst x) * pow2 (snd x)"
   12.22 -
   12.23 -lemma pow2_0[simp]: "pow2 0 = 1"
   12.24 -by (simp add: pow2_def)
   12.25 -
   12.26 -lemma pow2_1[simp]: "pow2 1 = 2"
   12.27 -by (simp add: pow2_def)
   12.28 -
   12.29 -lemma pow2_neg: "pow2 x = inverse (pow2 (-x))"
   12.30 -by (simp add: pow2_def)
   12.31 -
   12.32 -lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
   12.33 -proof -
   12.34 -  have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith
   12.35 -  have g: "! a b. a - -1 = a + (1::int)" by arith
   12.36 -  have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)"
   12.37 -    apply (auto, induct_tac n)
   12.38 -    apply (simp_all add: pow2_def)
   12.39 -    apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
   12.40 -    by (auto simp add: h)
   12.41 -  show ?thesis
   12.42 -  proof (induct a)
   12.43 -    case (1 n)
   12.44 -    from pos show ?case by (simp add: algebra_simps)
   12.45 -  next
   12.46 -    case (2 n)
   12.47 -    show ?case
   12.48 -      apply (auto)
   12.49 -      apply (subst pow2_neg[of "- int n"])
   12.50 -      apply (subst pow2_neg[of "-1 - int n"])
   12.51 -      apply (auto simp add: g pos)
   12.52 -      done
   12.53 -  qed
   12.54 -qed
   12.55 -
   12.56 -lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
   12.57 -proof (induct b)
   12.58 -  case (1 n)
   12.59 -  show ?case
   12.60 -  proof (induct n)
   12.61 -    case 0
   12.62 -    show ?case by simp
   12.63 -  next
   12.64 -    case (Suc m)
   12.65 -    show ?case by (auto simp add: algebra_simps pow2_add1 prems)
   12.66 -  qed
   12.67 -next
   12.68 -  case (2 n)
   12.69 -  show ?case
   12.70 -  proof (induct n)
   12.71 -    case 0
   12.72 -    show ?case
   12.73 -      apply (auto)
   12.74 -      apply (subst pow2_neg[of "a + -1"])
   12.75 -      apply (subst pow2_neg[of "-1"])
   12.76 -      apply (simp)
   12.77 -      apply (insert pow2_add1[of "-a"])
   12.78 -      apply (simp add: algebra_simps)
   12.79 -      apply (subst pow2_neg[of "-a"])
   12.80 -      apply (simp)
   12.81 -      done
   12.82 -    case (Suc m)
   12.83 -    have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith
   12.84 -    have b: "int m - -2 = 1 + (int m + 1)" by arith
   12.85 -    show ?case
   12.86 -      apply (auto)
   12.87 -      apply (subst pow2_neg[of "a + (-2 - int m)"])
   12.88 -      apply (subst pow2_neg[of "-2 - int m"])
   12.89 -      apply (auto simp add: algebra_simps)
   12.90 -      apply (subst a)
   12.91 -      apply (subst b)
   12.92 -      apply (simp only: pow2_add1)
   12.93 -      apply (subst pow2_neg[of "int m - a + 1"])
   12.94 -      apply (subst pow2_neg[of "int m + 1"])
   12.95 -      apply auto
   12.96 -      apply (insert prems)
   12.97 -      apply (auto simp add: algebra_simps)
   12.98 -      done
   12.99 -  qed
  12.100 -qed
  12.101 -
  12.102 -lemma "float (a, e) + float (b, e) = float (a + b, e)"
  12.103 -by (simp add: float_def algebra_simps)
  12.104 -
  12.105 -definition
  12.106 -  int_of_real :: "real \<Rightarrow> int" where
  12.107 -  "int_of_real x = (SOME y. real y = x)"
  12.108 -
  12.109 -definition
  12.110 -  real_is_int :: "real \<Rightarrow> bool" where
  12.111 -  "real_is_int x = (EX (u::int). x = real u)"
  12.112 -
  12.113 -lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"
  12.114 -by (auto simp add: real_is_int_def int_of_real_def)
  12.115 -
  12.116 -lemma float_transfer: "real_is_int ((real a)*(pow2 c)) \<Longrightarrow> float (a, b) = float (int_of_real ((real a)*(pow2 c)), b - c)"
  12.117 -by (simp add: float_def real_is_int_def2 pow2_add[symmetric])
  12.118 -
  12.119 -lemma pow2_int: "pow2 (int c) = 2^c"
  12.120 -by (simp add: pow2_def)
  12.121 -
  12.122 -lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)"
  12.123 -by (simp add: float_def pow2_int[symmetric] pow2_add[symmetric])
  12.124 -
  12.125 -lemma real_is_int_real[simp]: "real_is_int (real (x::int))"
  12.126 -by (auto simp add: real_is_int_def int_of_real_def)
  12.127 -
  12.128 -lemma int_of_real_real[simp]: "int_of_real (real x) = x"
  12.129 -by (simp add: int_of_real_def)
  12.130 -
  12.131 -lemma real_int_of_real[simp]: "real_is_int x \<Longrightarrow> real (int_of_real x) = x"
  12.132 -by (auto simp add: int_of_real_def real_is_int_def)
  12.133 -
  12.134 -lemma real_is_int_add_int_of_real: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> (int_of_real (a+b)) = (int_of_real a) + (int_of_real b)"
  12.135 -by (auto simp add: int_of_real_def real_is_int_def)
  12.136 -
  12.137 -lemma real_is_int_add[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a+b)"
  12.138 -apply (subst real_is_int_def2)
  12.139 -apply (simp add: real_is_int_add_int_of_real real_int_of_real)
  12.140 -done
  12.141 -
  12.142 -lemma int_of_real_sub: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> (int_of_real (a-b)) = (int_of_real a) - (int_of_real b)"
  12.143 -by (auto simp add: int_of_real_def real_is_int_def)
  12.144 -
  12.145 -lemma real_is_int_sub[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a-b)"
  12.146 -apply (subst real_is_int_def2)
  12.147 -apply (simp add: int_of_real_sub real_int_of_real)
  12.148 -done
  12.149 -
  12.150 -lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real a = x"
  12.151 -by (auto simp add: real_is_int_def)
  12.152 -
  12.153 -lemma int_of_real_mult:
  12.154 -  assumes "real_is_int a" "real_is_int b"
  12.155 -  shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)"
  12.156 -proof -
  12.157 -  from prems have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto)
  12.158 -  from prems have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto)
  12.159 -  from a obtain a'::int where a':"a = real a'" by auto
  12.160 -  from b obtain b'::int where b':"b = real b'" by auto
  12.161 -  have r: "real a' * real b' = real (a' * b')" by auto
  12.162 -  show ?thesis
  12.163 -    apply (simp add: a' b')
  12.164 -    apply (subst r)
  12.165 -    apply (simp only: int_of_real_real)
  12.166 -    done
  12.167 -qed
  12.168 -
  12.169 -lemma real_is_int_mult[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a*b)"
  12.170 -apply (subst real_is_int_def2)
  12.171 -apply (simp add: int_of_real_mult)
  12.172 -done
  12.173 -
  12.174 -lemma real_is_int_0[simp]: "real_is_int (0::real)"
  12.175 -by (simp add: real_is_int_def int_of_real_def)
  12.176 -
  12.177 -lemma real_is_int_1[simp]: "real_is_int (1::real)"
  12.178 -proof -
  12.179 -  have "real_is_int (1::real) = real_is_int(real (1::int))" by auto
  12.180 -  also have "\<dots> = True" by (simp only: real_is_int_real)
  12.181 -  ultimately show ?thesis by auto
  12.182 -qed
  12.183 -
  12.184 -lemma real_is_int_n1: "real_is_int (-1::real)"
  12.185 -proof -
  12.186 -  have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto
  12.187 -  also have "\<dots> = True" by (simp only: real_is_int_real)
  12.188 -  ultimately show ?thesis by auto
  12.189 -qed
  12.190 -
  12.191 -lemma real_is_int_number_of[simp]: "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
  12.192 -proof -
  12.193 -  have neg1: "real_is_int (-1::real)"
  12.194 -  proof -
  12.195 -    have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto
  12.196 -    also have "\<dots> = True" by (simp only: real_is_int_real)
  12.197 -    ultimately show ?thesis by auto
  12.198 -  qed
  12.199 -
  12.200 -  {
  12.201 -    fix x :: int
  12.202 -    have "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
  12.203 -      unfolding number_of_eq
  12.204 -      apply (induct x)
  12.205 -      apply (induct_tac n)
  12.206 -      apply (simp)
  12.207 -      apply (simp)
  12.208 -      apply (induct_tac n)
  12.209 -      apply (simp add: neg1)
  12.210 -    proof -
  12.211 -      fix n :: nat
  12.212 -      assume rn: "(real_is_int (of_int (- (int (Suc n)))))"
  12.213 -      have s: "-(int (Suc (Suc n))) = -1 + - (int (Suc n))" by simp
  12.214 -      show "real_is_int (of_int (- (int (Suc (Suc n)))))"
  12.215 -        apply (simp only: s of_int_add)
  12.216 -        apply (rule real_is_int_add)
  12.217 -        apply (simp add: neg1)
  12.218 -        apply (simp only: rn)
  12.219 -        done
  12.220 -    qed
  12.221 -  }
  12.222 -  note Abs_Bin = this
  12.223 -  {
  12.224 -    fix x :: int
  12.225 -    have "? u. x = u"
  12.226 -      apply (rule exI[where x = "x"])
  12.227 -      apply (simp)
  12.228 -      done
  12.229 -  }
  12.230 -  then obtain u::int where "x = u" by auto
  12.231 -  with Abs_Bin show ?thesis by auto
  12.232 -qed
  12.233 -
  12.234 -lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)"
  12.235 -by (simp add: int_of_real_def)
  12.236 -
  12.237 -lemma int_of_real_1[simp]: "int_of_real (1::real) = (1::int)"
  12.238 -proof -
  12.239 -  have 1: "(1::real) = real (1::int)" by auto
  12.240 -  show ?thesis by (simp only: 1 int_of_real_real)
  12.241 -qed
  12.242 -
  12.243 -lemma int_of_real_number_of[simp]: "int_of_real (number_of b) = number_of b"
  12.244 -proof -
  12.245 -  have "real_is_int (number_of b)" by simp
  12.246 -  then have uu: "?! u::int. number_of b = real u" by (auto simp add: real_is_int_rep)
  12.247 -  then obtain u::int where u:"number_of b = real u" by auto
  12.248 -  have "number_of b = real ((number_of b)::int)"
  12.249 -    by (simp add: number_of_eq real_of_int_def)
  12.250 -  have ub: "number_of b = real ((number_of b)::int)"
  12.251 -    by (simp add: number_of_eq real_of_int_def)
  12.252 -  from uu u ub have unb: "u = number_of b"
  12.253 -    by blast
  12.254 -  have "int_of_real (number_of b) = u" by (simp add: u)
  12.255 -  with unb show ?thesis by simp
  12.256 -qed
  12.257 -
  12.258 -lemma float_transfer_even: "even a \<Longrightarrow> float (a, b) = float (a div 2, b+1)"
  12.259 -  apply (subst float_transfer[where a="a" and b="b" and c="-1", simplified])
  12.260 -  apply (simp_all add: pow2_def even_def real_is_int_def algebra_simps)
  12.261 -  apply (auto)
  12.262 -proof -
  12.263 -  fix q::int
  12.264 -  have a:"b - (-1\<Colon>int) = (1\<Colon>int) + b" by arith
  12.265 -  show "(float (q, (b - (-1\<Colon>int)))) = (float (q, ((1\<Colon>int) + b)))"
  12.266 -    by (simp add: a)
  12.267 -qed
  12.268 -
  12.269 -lemma int_div_zdiv: "int (a div b) = (int a) div (int b)"
  12.270 -by (rule zdiv_int)
  12.271 -
  12.272 -lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)"
  12.273 -by (rule zmod_int)
  12.274 -
  12.275 -lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
  12.276 -by arith
  12.277 -
  12.278 -function norm_float :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
  12.279 -  "norm_float a b = (if a \<noteq> 0 \<and> even a then norm_float (a div 2) (b + 1)
  12.280 -    else if a = 0 then (0, 0) else (a, b))"
  12.281 -by auto
  12.282 -
  12.283 -termination by (relation "measure (nat o abs o fst)")
  12.284 -  (auto intro: abs_div_2_less)
  12.285 -
  12.286 -lemma norm_float: "float x = float (split norm_float x)"
  12.287 -proof -
  12.288 -  {
  12.289 -    fix a b :: int
  12.290 -    have norm_float_pair: "float (a, b) = float (norm_float a b)"
  12.291 -    proof (induct a b rule: norm_float.induct)
  12.292 -      case (1 u v)
  12.293 -      show ?case
  12.294 -      proof cases
  12.295 -        assume u: "u \<noteq> 0 \<and> even u"
  12.296 -        with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto
  12.297 -        with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
  12.298 -        then show ?thesis
  12.299 -          apply (subst norm_float.simps)
  12.300 -          apply (simp add: ind)
  12.301 -          done
  12.302 -      next
  12.303 -        assume "~(u \<noteq> 0 \<and> even u)"
  12.304 -        then show ?thesis
  12.305 -          by (simp add: prems float_def)
  12.306 -      qed
  12.307 -    qed
  12.308 -  }
  12.309 -  note helper = this
  12.310 -  have "? a b. x = (a,b)" by auto
  12.311 -  then obtain a b where "x = (a, b)" by blast
  12.312 -  then show ?thesis by (simp add: helper)
  12.313 -qed
  12.314 -
  12.315 -lemma float_add_l0: "float (0, e) + x = x"
  12.316 -  by (simp add: float_def)
  12.317 -
  12.318 -lemma float_add_r0: "x + float (0, e) = x"
  12.319 -  by (simp add: float_def)
  12.320 -
  12.321 -lemma float_add:
  12.322 -  "float (a1, e1) + float (a2, e2) =
  12.323 -  (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
  12.324 -  else float (a1*2^(nat (e1-e2))+a2, e2))"
  12.325 -  apply (simp add: float_def algebra_simps)
  12.326 -  apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric])
  12.327 -  done
  12.328 -
  12.329 -lemma float_add_assoc1:
  12.330 -  "(x + float (y1, e1)) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x"
  12.331 -  by simp
  12.332 -
  12.333 -lemma float_add_assoc2:
  12.334 -  "(float (y1, e1) + x) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x"
  12.335 -  by simp
  12.336 -
  12.337 -lemma float_add_assoc3:
  12.338 -  "float (y1, e1) + (x + float (y2, e2)) = (float (y1, e1) + float (y2, e2)) + x"
  12.339 -  by simp
  12.340 -
  12.341 -lemma float_add_assoc4:
  12.342 -  "float (y1, e1) + (float (y2, e2) + x) = (float (y1, e1) + float (y2, e2)) + x"
  12.343 -  by simp
  12.344 -
  12.345 -lemma float_mult_l0: "float (0, e) * x = float (0, 0)"
  12.346 -  by (simp add: float_def)
  12.347 -
  12.348 -lemma float_mult_r0: "x * float (0, e) = float (0, 0)"
  12.349 -  by (simp add: float_def)
  12.350 -
  12.351 -definition 
  12.352 -  lbound :: "real \<Rightarrow> real"
  12.353 -where
  12.354 -  "lbound x = min 0 x"
  12.355 -
  12.356 -definition
  12.357 -  ubound :: "real \<Rightarrow> real"
  12.358 -where
  12.359 -  "ubound x = max 0 x"
  12.360 -
  12.361 -lemma lbound: "lbound x \<le> x"   
  12.362 -  by (simp add: lbound_def)
  12.363 -
  12.364 -lemma ubound: "x \<le> ubound x"
  12.365 -  by (simp add: ubound_def)
  12.366 -
  12.367 -lemma float_mult:
  12.368 -  "float (a1, e1) * float (a2, e2) =
  12.369 -  (float (a1 * a2, e1 + e2))"
  12.370 -  by (simp add: float_def pow2_add)
  12.371 -
  12.372 -lemma float_minus:
  12.373 -  "- (float (a,b)) = float (-a, b)"
  12.374 -  by (simp add: float_def)
  12.375 -
  12.376 -lemma zero_less_pow2:
  12.377 -  "0 < pow2 x"
  12.378 -proof -
  12.379 -  {
  12.380 -    fix y
  12.381 -    have "0 <= y \<Longrightarrow> 0 < pow2 y"
  12.382 -      by (induct y, induct_tac n, simp_all add: pow2_add)
  12.383 -  }
  12.384 -  note helper=this
  12.385 -  show ?thesis
  12.386 -    apply (case_tac "0 <= x")
  12.387 -    apply (simp add: helper)
  12.388 -    apply (subst pow2_neg)
  12.389 -    apply (simp add: helper)
  12.390 -    done
  12.391 -qed
  12.392 -
  12.393 -lemma zero_le_float:
  12.394 -  "(0 <= float (a,b)) = (0 <= a)"
  12.395 -  apply (auto simp add: float_def)
  12.396 -  apply (auto simp add: zero_le_mult_iff zero_less_pow2)
  12.397 -  apply (insert zero_less_pow2[of b])
  12.398 -  apply (simp_all)
  12.399 -  done
  12.400 -
  12.401 -lemma float_le_zero:
  12.402 -  "(float (a,b) <= 0) = (a <= 0)"
  12.403 -  apply (auto simp add: float_def)
  12.404 -  apply (auto simp add: mult_le_0_iff)
  12.405 -  apply (insert zero_less_pow2[of b])
  12.406 -  apply auto
  12.407 -  done
  12.408 -
  12.409 -lemma float_abs:
  12.410 -  "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
  12.411 -  apply (auto simp add: abs_if)
  12.412 -  apply (simp_all add: zero_le_float[symmetric, of a b] float_minus)
  12.413 -  done
  12.414 -
  12.415 -lemma float_zero:
  12.416 -  "float (0, b) = 0"
  12.417 -  by (simp add: float_def)
  12.418 -
  12.419 -lemma float_pprt:
  12.420 -  "pprt (float (a, b)) = (if 0 <= a then (float (a,b)) else (float (0, b)))"
  12.421 -  by (auto simp add: zero_le_float float_le_zero float_zero)
  12.422 -
  12.423 -lemma pprt_lbound: "pprt (lbound x) = float (0, 0)"
  12.424 -  apply (simp add: float_def)
  12.425 -  apply (rule pprt_eq_0)
  12.426 -  apply (simp add: lbound_def)
  12.427 -  done
  12.428 -
  12.429 -lemma nprt_ubound: "nprt (ubound x) = float (0, 0)"
  12.430 -  apply (simp add: float_def)
  12.431 -  apply (rule nprt_eq_0)
  12.432 -  apply (simp add: ubound_def)
  12.433 -  done
  12.434 -
  12.435 -lemma float_nprt:
  12.436 -  "nprt (float (a, b)) = (if 0 <= a then (float (0,b)) else (float (a, b)))"
  12.437 -  by (auto simp add: zero_le_float float_le_zero float_zero)
  12.438 -
  12.439 -lemma norm_0_1: "(0::_::number_ring) = Numeral0 & (1::_::number_ring) = Numeral1"
  12.440 -  by auto
  12.441 -
  12.442 -lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
  12.443 -  by simp
  12.444 -
  12.445 -lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)"
  12.446 -  by simp
  12.447 -
  12.448 -lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
  12.449 -  by simp
  12.450 -
  12.451 -lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
  12.452 -  by simp
  12.453 -
  12.454 -lemma int_pow_0: "(a::int)^(Numeral0) = 1"
  12.455 -  by simp
  12.456 -
  12.457 -lemma int_pow_1: "(a::int)^(Numeral1) = a"
  12.458 -  by simp
  12.459 -
  12.460 -lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0"
  12.461 -  by simp
  12.462 -
  12.463 -lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1"
  12.464 -  by simp
  12.465 -
  12.466 -lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0"
  12.467 -  by simp
  12.468 -
  12.469 -lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
  12.470 -  by simp
  12.471 -
  12.472 -lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1"
  12.473 -  by simp
  12.474 -
  12.475 -lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1"
  12.476 -proof -
  12.477 -  have 1:"((-1)::nat) = 0"
  12.478 -    by simp
  12.479 -  show ?thesis by (simp add: 1)
  12.480 -qed
  12.481 -
  12.482 -lemma fst_cong: "a=a' \<Longrightarrow> fst (a,b) = fst (a',b)"
  12.483 -  by simp
  12.484 -
  12.485 -lemma snd_cong: "b=b' \<Longrightarrow> snd (a,b) = snd (a,b')"
  12.486 -  by simp
  12.487 -
  12.488 -lemma lift_bool: "x \<Longrightarrow> x=True"
  12.489 -  by simp
  12.490 -
  12.491 -lemma nlift_bool: "~x \<Longrightarrow> x=False"
  12.492 -  by simp
  12.493 -
  12.494 -lemma not_false_eq_true: "(~ False) = True" by simp
  12.495 -
  12.496 -lemma not_true_eq_false: "(~ True) = False" by simp
  12.497 -
  12.498 -lemmas binarith =
  12.499 -  normalize_bin_simps
  12.500 -  pred_bin_simps succ_bin_simps
  12.501 -  add_bin_simps minus_bin_simps mult_bin_simps
  12.502 -
  12.503 -lemma int_eq_number_of_eq:
  12.504 -  "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)"
  12.505 -  by (rule eq_number_of_eq)
  12.506 -
  12.507 -lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
  12.508 -  by (simp only: iszero_number_of_Pls)
  12.509 -
  12.510 -lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
  12.511 -  by simp
  12.512 -
  12.513 -lemma int_iszero_number_of_Bit0: "iszero ((number_of (Int.Bit0 w))::int) = iszero ((number_of w)::int)"
  12.514 -  by simp
  12.515 -
  12.516 -lemma int_iszero_number_of_Bit1: "\<not> iszero ((number_of (Int.Bit1 w))::int)"
  12.517 -  by simp
  12.518 -
  12.519 -lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
  12.520 -  unfolding neg_def number_of_is_id by simp
  12.521 -
  12.522 -lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
  12.523 -  by simp
  12.524 -
  12.525 -lemma int_neg_number_of_Min: "neg (-1::int)"
  12.526 -  by simp
  12.527 -
  12.528 -lemma int_neg_number_of_Bit0: "neg ((number_of (Int.Bit0 w))::int) = neg ((number_of w)::int)"
  12.529 -  by simp
  12.530 -
  12.531 -lemma int_neg_number_of_Bit1: "neg ((number_of (Int.Bit1 w))::int) = neg ((number_of w)::int)"
  12.532 -  by simp
  12.533 -
  12.534 -lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
  12.535 -  unfolding neg_def number_of_is_id by (simp add: not_less)
  12.536 -
  12.537 -lemmas intarithrel =
  12.538 -  int_eq_number_of_eq
  12.539 -  lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_Bit0
  12.540 -  lift_bool[OF int_iszero_number_of_Bit1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
  12.541 -  int_neg_number_of_Bit0 int_neg_number_of_Bit1 int_le_number_of_eq
  12.542 -
  12.543 -lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
  12.544 -  by simp
  12.545 -
  12.546 -lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
  12.547 -  by simp
  12.548 -
  12.549 -lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (v * w)"
  12.550 -  by simp
  12.551 -
  12.552 -lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
  12.553 -  by simp
  12.554 -
  12.555 -lemmas intarith = int_number_of_add_sym int_number_of_minus_sym int_number_of_diff_sym int_number_of_mult_sym
  12.556 -
  12.557 -lemmas natarith = add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
  12.558 -
  12.559 -lemmas powerarith = nat_number_of zpower_number_of_even
  12.560 -  zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
  12.561 -  zpower_Pls zpower_Min
  12.562 -
  12.563 -lemmas floatarith[simplified norm_0_1] = float_add float_add_l0 float_add_r0 float_mult float_mult_l0 float_mult_r0 
  12.564 -          float_minus float_abs zero_le_float float_pprt float_nprt pprt_lbound nprt_ubound
  12.565 -
  12.566 -(* for use with the compute oracle *)
  12.567 -lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false
  12.568 -
  12.569 -use "~~/src/HOL/Tools/float_arith.ML"
  12.570 -
  12.571 -end
    13.1 --- a/src/HOL/Tools/ComputeHOL.thy	Wed Sep 02 14:11:45 2009 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,191 +0,0 @@
    13.4 -theory ComputeHOL
    13.5 -imports Complex_Main "~~/src/Tools/Compute_Oracle/Compute_Oracle"
    13.6 -begin
    13.7 -
    13.8 -lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq)
    13.9 -lemma meta_eq_trivial: "x == y \<Longrightarrow> x == y" by simp
   13.10 -lemma meta_eq_imp_eq: "x == y \<Longrightarrow> x = y" by auto
   13.11 -lemma eq_trivial: "x = y \<Longrightarrow> x = y" by auto
   13.12 -lemma bool_to_true: "x :: bool \<Longrightarrow> x == True"  by simp
   13.13 -lemma transmeta_1: "x = y \<Longrightarrow> y == z \<Longrightarrow> x = z" by simp
   13.14 -lemma transmeta_2: "x == y \<Longrightarrow> y = z \<Longrightarrow> x = z" by simp
   13.15 -lemma transmeta_3: "x == y \<Longrightarrow> y == z \<Longrightarrow> x = z" by simp
   13.16 -
   13.17 -
   13.18 -(**** compute_if ****)
   13.19 -
   13.20 -lemma If_True: "If True = (\<lambda> x y. x)" by ((rule ext)+,auto)
   13.21 -lemma If_False: "If False = (\<lambda> x y. y)" by ((rule ext)+, auto)
   13.22 -
   13.23 -lemmas compute_if = If_True If_False
   13.24 -
   13.25 -(**** compute_bool ****)
   13.26 -
   13.27 -lemma bool1: "(\<not> True) = False"  by blast
   13.28 -lemma bool2: "(\<not> False) = True"  by blast
   13.29 -lemma bool3: "(P \<and> True) = P" by blast
   13.30 -lemma bool4: "(True \<and> P) = P" by blast
   13.31 -lemma bool5: "(P \<and> False) = False" by blast
   13.32 -lemma bool6: "(False \<and> P) = False" by blast
   13.33 -lemma bool7: "(P \<or> True) = True" by blast
   13.34 -lemma bool8: "(True \<or> P) = True" by blast
   13.35 -lemma bool9: "(P \<or> False) = P" by blast
   13.36 -lemma bool10: "(False \<or> P) = P" by blast
   13.37 -lemma bool11: "(True \<longrightarrow> P) = P" by blast
   13.38 -lemma bool12: "(P \<longrightarrow> True) = True" by blast
   13.39 -lemma bool13: "(True \<longrightarrow> P) = P" by blast
   13.40 -lemma bool14: "(P \<longrightarrow> False) = (\<not> P)" by blast
   13.41 -lemma bool15: "(False \<longrightarrow> P) = True" by blast
   13.42 -lemma bool16: "(False = False) = True" by blast
   13.43 -lemma bool17: "(True = True) = True" by blast
   13.44 -lemma bool18: "(False = True) = False" by blast
   13.45 -lemma bool19: "(True = False) = False" by blast
   13.46 -
   13.47 -lemmas compute_bool = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10 bool11 bool12 bool13 bool14 bool15 bool16 bool17 bool18 bool19
   13.48 -
   13.49 -
   13.50 -(*** compute_pair ***)
   13.51 -
   13.52 -lemma compute_fst: "fst (x,y) = x" by simp
   13.53 -lemma compute_snd: "snd (x,y) = y" by simp
   13.54 -lemma compute_pair_eq: "((a, b) = (c, d)) = (a = c \<and> b = d)" by auto
   13.55 -
   13.56 -lemma prod_case_simp: "prod_case f (x,y) = f x y" by simp
   13.57 -
   13.58 -lemmas compute_pair = compute_fst compute_snd compute_pair_eq prod_case_simp
   13.59 -
   13.60 -(*** compute_option ***)
   13.61 -
   13.62 -lemma compute_the: "the (Some x) = x" by simp
   13.63 -lemma compute_None_Some_eq: "(None = Some x) = False" by auto
   13.64 -lemma compute_Some_None_eq: "(Some x = None) = False" by auto
   13.65 -lemma compute_None_None_eq: "(None = None) = True" by auto
   13.66 -lemma compute_Some_Some_eq: "(Some x = Some y) = (x = y)" by auto
   13.67 -
   13.68 -definition
   13.69 -   option_case_compute :: "'b option \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
   13.70 -where
   13.71 -   "option_case_compute opt a f = option_case a f opt"
   13.72 -
   13.73 -lemma option_case_compute: "option_case = (\<lambda> a f opt. option_case_compute opt a f)"
   13.74 -  by (simp add: option_case_compute_def)
   13.75 -
   13.76 -lemma option_case_compute_None: "option_case_compute None = (\<lambda> a f. a)"
   13.77 -  apply (rule ext)+
   13.78 -  apply (simp add: option_case_compute_def)
   13.79 -  done
   13.80 -
   13.81 -lemma option_case_compute_Some: "option_case_compute (Some x) = (\<lambda> a f. f x)"
   13.82 -  apply (rule ext)+
   13.83 -  apply (simp add: option_case_compute_def)
   13.84 -  done
   13.85 -
   13.86 -lemmas compute_option_case = option_case_compute option_case_compute_None option_case_compute_Some
   13.87 -
   13.88 -lemmas compute_option = compute_the compute_None_Some_eq compute_Some_None_eq compute_None_None_eq compute_Some_Some_eq compute_option_case
   13.89 -
   13.90 -(**** compute_list_length ****)
   13.91 -
   13.92 -lemma length_cons:"length (x#xs) = 1 + (length xs)"
   13.93 -  by simp
   13.94 -
   13.95 -lemma length_nil: "length [] = 0"
   13.96 -  by simp
   13.97 -
   13.98 -lemmas compute_list_length = length_nil length_cons
   13.99 -
  13.100 -(*** compute_list_case ***)
  13.101 -
  13.102 -definition
  13.103 -  list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
  13.104 -where
  13.105 -  "list_case_compute l a f = list_case a f l"
  13.106 -
  13.107 -lemma list_case_compute: "list_case = (\<lambda> (a::'a) f (l::'b list). list_case_compute l a f)"
  13.108 -  apply (rule ext)+
  13.109 -  apply (simp add: list_case_compute_def)
  13.110 -  done
  13.111 -
  13.112 -lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\<lambda> (a::'a) f. a)"
  13.113 -  apply (rule ext)+
  13.114 -  apply (simp add: list_case_compute_def)
  13.115 -  done
  13.116 -
  13.117 -lemma list_case_compute_cons: "list_case_compute (u#v) = (\<lambda> (a::'a) f. (f (u::'b) v))"
  13.118 -  apply (rule ext)+
  13.119 -  apply (simp add: list_case_compute_def)
  13.120 -  done
  13.121 -
  13.122 -lemmas compute_list_case = list_case_compute list_case_compute_empty list_case_compute_cons
  13.123 -
  13.124 -(*** compute_list_nth ***)
  13.125 -(* Of course, you will need computation with nats for this to work \<dots> *)
  13.126 -
  13.127 -lemma compute_list_nth: "((x#xs) ! n) = (if n = 0 then x else (xs ! (n - 1)))"
  13.128 -  by (cases n, auto)
  13.129 -  
  13.130 -(*** compute_list ***)
  13.131 -
  13.132 -lemmas compute_list = compute_list_case compute_list_length compute_list_nth
  13.133 -
  13.134 -(*** compute_let ***)
  13.135 -
  13.136 -lemmas compute_let = Let_def
  13.137 -
  13.138 -(***********************)
  13.139 -(* Everything together *)
  13.140 -(***********************)
  13.141 -
  13.142 -lemmas compute_hol = compute_if compute_bool compute_pair compute_option compute_list compute_let
  13.143 -
  13.144 -ML {*
  13.145 -signature ComputeHOL =
  13.146 -sig
  13.147 -  val prep_thms : thm list -> thm list
  13.148 -  val to_meta_eq : thm -> thm
  13.149 -  val to_hol_eq : thm -> thm
  13.150 -  val symmetric : thm -> thm 
  13.151 -  val trans : thm -> thm -> thm
  13.152 -end
  13.153 -
  13.154 -structure ComputeHOL : ComputeHOL =
  13.155 -struct
  13.156 -
  13.157 -local
  13.158 -fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq));
  13.159 -in
  13.160 -fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [])
  13.161 -  | rewrite_conv (eq :: eqs) ct =
  13.162 -      Thm.instantiate (Thm.match (lhs_of eq, ct)) eq
  13.163 -      handle Pattern.MATCH => rewrite_conv eqs ct;
  13.164 -end
  13.165 -
  13.166 -val convert_conditions = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.try_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}])))
  13.167 -
  13.168 -val eq_th = @{thm "HOL.eq_reflection"}
  13.169 -val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"}
  13.170 -val bool_to_true = @{thm "ComputeHOL.bool_to_true"}
  13.171 -
  13.172 -fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th]
  13.173 -
  13.174 -fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] 
  13.175 -
  13.176 -fun prep_thms ths = map (convert_conditions o to_meta_eq) ths
  13.177 -
  13.178 -fun symmetric th = @{thm "HOL.sym"} OF [th] handle THM _ => @{thm "Pure.symmetric"} OF [th]
  13.179 -
  13.180 -local
  13.181 -    val trans_HOL = @{thm "HOL.trans"}
  13.182 -    val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"}
  13.183 -    val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"}
  13.184 -    val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"}
  13.185 -    fun tr [] th1 th2 = trans_HOL OF [th1, th2]
  13.186 -      | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) 
  13.187 -in
  13.188 -  fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2
  13.189 -end
  13.190 -
  13.191 -end
  13.192 -*}
  13.193 -
  13.194 -end
    14.1 --- a/src/HOL/Tools/ComputeNumeral.thy	Wed Sep 02 14:11:45 2009 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,195 +0,0 @@
    14.4 -theory ComputeNumeral
    14.5 -imports ComputeHOL ComputeFloat
    14.6 -begin
    14.7 -
    14.8 -(* normalization of bit strings *)
    14.9 -lemmas bitnorm = normalize_bin_simps
   14.10 -
   14.11 -(* neg for bit strings *)
   14.12 -lemma neg1: "neg Int.Pls = False" by (simp add: Int.Pls_def)
   14.13 -lemma neg2: "neg Int.Min = True" apply (subst Int.Min_def) by auto
   14.14 -lemma neg3: "neg (Int.Bit0 x) = neg x" apply (simp add: neg_def) apply (subst Bit0_def) by auto
   14.15 -lemma neg4: "neg (Int.Bit1 x) = neg x" apply (simp add: neg_def) apply (subst Bit1_def) by auto  
   14.16 -lemmas bitneg = neg1 neg2 neg3 neg4
   14.17 -
   14.18 -(* iszero for bit strings *)
   14.19 -lemma iszero1: "iszero Int.Pls = True" by (simp add: Int.Pls_def iszero_def)
   14.20 -lemma iszero2: "iszero Int.Min = False" apply (subst Int.Min_def) apply (subst iszero_def) by simp
   14.21 -lemma iszero3: "iszero (Int.Bit0 x) = iszero x" apply (subst Int.Bit0_def) apply (subst iszero_def)+ by auto
   14.22 -lemma iszero4: "iszero (Int.Bit1 x) = False" apply (subst Int.Bit1_def) apply (subst iszero_def)+  apply simp by arith
   14.23 -lemmas bitiszero = iszero1 iszero2 iszero3 iszero4
   14.24 -
   14.25 -(* lezero for bit strings *)
   14.26 -constdefs
   14.27 -  "lezero x == (x \<le> 0)"
   14.28 -lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto
   14.29 -lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto
   14.30 -lemma lezero3: "lezero (Int.Bit0 x) = lezero x" unfolding Int.Bit0_def lezero_def by auto
   14.31 -lemma lezero4: "lezero (Int.Bit1 x) = neg x" unfolding Int.Bit1_def lezero_def neg_def by auto
   14.32 -lemmas bitlezero = lezero1 lezero2 lezero3 lezero4
   14.33 -
   14.34 -(* equality for bit strings *)
   14.35 -lemmas biteq = eq_bin_simps
   14.36 -
   14.37 -(* x < y for bit strings *)
   14.38 -lemmas bitless = less_bin_simps
   14.39 -
   14.40 -(* x \<le> y for bit strings *)
   14.41 -lemmas bitle = le_bin_simps
   14.42 -
   14.43 -(* succ for bit strings *)
   14.44 -lemmas bitsucc = succ_bin_simps
   14.45 -
   14.46 -(* pred for bit strings *)
   14.47 -lemmas bitpred = pred_bin_simps
   14.48 -
   14.49 -(* unary minus for bit strings *)
   14.50 -lemmas bituminus = minus_bin_simps
   14.51 -
   14.52 -(* addition for bit strings *)
   14.53 -lemmas bitadd = add_bin_simps
   14.54 -
   14.55 -(* multiplication for bit strings *) 
   14.56 -lemma mult_Pls_right: "x * Int.Pls = Int.Pls" by (simp add: Pls_def)
   14.57 -lemma mult_Min_right: "x * Int.Min = - x" by (subst mult_commute, simp add: mult_Min)
   14.58 -lemma multb0x: "(Int.Bit0 x) * y = Int.Bit0 (x * y)" by (rule mult_Bit0)
   14.59 -lemma multxb0: "x * (Int.Bit0 y) = Int.Bit0 (x * y)" unfolding Bit0_def by simp
   14.60 -lemma multb1: "(Int.Bit1 x) * (Int.Bit1 y) = Int.Bit1 (Int.Bit0 (x * y) + x + y)"
   14.61 -  unfolding Bit0_def Bit1_def by (simp add: algebra_simps)
   14.62 -lemmas bitmul = mult_Pls mult_Min mult_Pls_right mult_Min_right multb0x multxb0 multb1
   14.63 -
   14.64 -lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul 
   14.65 -
   14.66 -constdefs 
   14.67 -  "nat_norm_number_of (x::nat) == x"
   14.68 -
   14.69 -lemma nat_norm_number_of: "nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)"
   14.70 -  apply (simp add: nat_norm_number_of_def)
   14.71 -  unfolding lezero_def iszero_def neg_def
   14.72 -  apply (simp add: numeral_simps)
   14.73 -  done
   14.74 -
   14.75 -(* Normalization of nat literals *)
   14.76 -lemma natnorm0: "(0::nat) = number_of (Int.Pls)" by auto
   14.77 -lemma natnorm1: "(1 :: nat) = number_of (Int.Bit1 Int.Pls)"  by auto 
   14.78 -lemmas natnorm = natnorm0 natnorm1 nat_norm_number_of
   14.79 -
   14.80 -(* Suc *)
   14.81 -lemma natsuc: "Suc (number_of x) = (if neg x then 1 else number_of (Int.succ x))" by (auto simp add: number_of_is_id)
   14.82 -
   14.83 -(* Addition for nat *)
   14.84 -lemma natadd: "number_of x + ((number_of y)::nat) = (if neg x then (number_of y) else (if neg y then number_of x else (number_of (x + y))))"
   14.85 -  unfolding nat_number_of_def number_of_is_id neg_def
   14.86 -  by auto
   14.87 -
   14.88 -(* Subtraction for nat *)
   14.89 -lemma natsub: "(number_of x) - ((number_of y)::nat) = 
   14.90 -  (if neg x then 0 else (if neg y then number_of x else (nat_norm_number_of (number_of (x + (- y))))))"
   14.91 -  unfolding nat_norm_number_of
   14.92 -  by (auto simp add: number_of_is_id neg_def lezero_def iszero_def Let_def nat_number_of_def)
   14.93 -
   14.94 -(* Multiplication for nat *)
   14.95 -lemma natmul: "(number_of x) * ((number_of y)::nat) = 
   14.96 -  (if neg x then 0 else (if neg y then 0 else number_of (x * y)))"
   14.97 -  unfolding nat_number_of_def number_of_is_id neg_def
   14.98 -  by (simp add: nat_mult_distrib)
   14.99 -
  14.100 -lemma nateq: "(((number_of x)::nat) = (number_of y)) = ((lezero x \<and> lezero y) \<or> (x = y))"
  14.101 -  by (auto simp add: iszero_def lezero_def neg_def number_of_is_id)
  14.102 -
  14.103 -lemma natless: "(((number_of x)::nat) < (number_of y)) = ((x < y) \<and> (\<not> (lezero y)))"
  14.104 -  by (simp add: lezero_def numeral_simps not_le)
  14.105 -
  14.106 -lemma natle: "(((number_of x)::nat) \<le> (number_of y)) = (y < x \<longrightarrow> lezero x)"
  14.107 -  by (auto simp add: number_of_is_id lezero_def nat_number_of_def)
  14.108 -
  14.109 -fun natfac :: "nat \<Rightarrow> nat"
  14.110 -where
  14.111 -   "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))"
  14.112 -
  14.113 -lemmas compute_natarith = bitarith natnorm natsuc natadd natsub natmul nateq natless natle natfac.simps
  14.114 -
  14.115 -lemma number_eq: "(((number_of x)::'a::{number_ring, ordered_idom}) = (number_of y)) = (x = y)"
  14.116 -  unfolding number_of_eq
  14.117 -  apply simp
  14.118 -  done
  14.119 -
  14.120 -lemma number_le: "(((number_of x)::'a::{number_ring, ordered_idom}) \<le>  (number_of y)) = (x \<le> y)"
  14.121 -  unfolding number_of_eq
  14.122 -  apply simp
  14.123 -  done
  14.124 -
  14.125 -lemma number_less: "(((number_of x)::'a::{number_ring, ordered_idom}) <  (number_of y)) = (x < y)"
  14.126 -  unfolding number_of_eq 
  14.127 -  apply simp
  14.128 -  done
  14.129 -
  14.130 -lemma number_diff: "((number_of x)::'a::{number_ring, ordered_idom}) - number_of y = number_of (x + (- y))"
  14.131 -  apply (subst diff_number_of_eq)
  14.132 -  apply simp
  14.133 -  done
  14.134 -
  14.135 -lemmas number_norm = number_of_Pls[symmetric] numeral_1_eq_1[symmetric]
  14.136 -
  14.137 -lemmas compute_numberarith = number_of_minus[symmetric] number_of_add[symmetric] number_diff number_of_mult[symmetric] number_norm number_eq number_le number_less
  14.138 -
  14.139 -lemma compute_real_of_nat_number_of: "real ((number_of v)::nat) = (if neg v then 0 else number_of v)"
  14.140 -  by (simp only: real_of_nat_number_of number_of_is_id)
  14.141 -
  14.142 -lemma compute_nat_of_int_number_of: "nat ((number_of v)::int) = (number_of v)"
  14.143 -  by simp
  14.144 -
  14.145 -lemmas compute_num_conversions = compute_real_of_nat_number_of compute_nat_of_int_number_of real_number_of
  14.146 -
  14.147 -lemmas zpowerarith = zpower_number_of_even
  14.148 -  zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
  14.149 -  zpower_Pls zpower_Min
  14.150 -
  14.151 -(* div, mod *)
  14.152 -
  14.153 -lemma adjust: "adjust b (q, r) = (if 0 \<le> r - b then (2 * q + 1, r - b) else (2 * q, r))"
  14.154 -  by (auto simp only: adjust_def)
  14.155 -
  14.156 -lemma negateSnd: "negateSnd (q, r) = (q, -r)" 
  14.157 -  by (simp add: negateSnd_def)
  14.158 -
  14.159 -lemma divmod: "IntDiv.divmod a b = (if 0\<le>a then
  14.160 -                  if 0\<le>b then posDivAlg a b
  14.161 -                  else if a=0 then (0, 0)
  14.162 -                       else negateSnd (negDivAlg (-a) (-b))
  14.163 -               else 
  14.164 -                  if 0<b then negDivAlg a b
  14.165 -                  else negateSnd (posDivAlg (-a) (-b)))"
  14.166 -  by (auto simp only: IntDiv.divmod_def)
  14.167 -
  14.168 -lemmas compute_div_mod = div_def mod_def divmod adjust negateSnd posDivAlg.simps negDivAlg.simps
  14.169 -
  14.170 -
  14.171 -
  14.172 -(* collecting all the theorems *)
  14.173 -
  14.174 -lemma even_Pls: "even (Int.Pls) = True"
  14.175 -  apply (unfold Pls_def even_def)
  14.176 -  by simp
  14.177 -
  14.178 -lemma even_Min: "even (Int.Min) = False"
  14.179 -  apply (unfold Min_def even_def)
  14.180 -  by simp
  14.181 -
  14.182 -lemma even_B0: "even (Int.Bit0 x) = True"
  14.183 -  apply (unfold Bit0_def)
  14.184 -  by simp
  14.185 -
  14.186 -lemma even_B1: "even (Int.Bit1 x) = False"
  14.187 -  apply (unfold Bit1_def)
  14.188 -  by simp
  14.189 -
  14.190 -lemma even_number_of: "even ((number_of w)::int) = even w"
  14.191 -  by (simp only: number_of_is_id)
  14.192 -
  14.193 -lemmas compute_even = even_Pls even_Min even_B0 even_B1 even_number_of
  14.194 -
  14.195 -lemmas compute_numeral = compute_if compute_let compute_pair compute_bool 
  14.196 -                         compute_natarith compute_numberarith max_def min_def compute_num_conversions zpowerarith compute_div_mod compute_even
  14.197 -
  14.198 -end