--- a/src/HOL/IsaMakefile Mon Nov 14 19:35:05 2011 +0100
+++ b/src/HOL/IsaMakefile Mon Nov 14 19:35:41 2011 +0100
@@ -435,6 +435,7 @@
Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
Library/Code_Char_ord.thy Library/Code_Integer.thy \
Library/Code_Natural.thy Library/Code_Prolog.thy \
+ Library/Code_Real_Approx_By_Float.thy \
Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \
Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy \
Library/Convex.thy Library/Countable.thy Library/Diagonalize.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Mon Nov 14 19:35:41 2011 +0100
@@ -0,0 +1,146 @@
+(* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
+
+theory Code_Real_Approx_By_Float
+imports Complex_Main "~~/src/HOL/Library/Code_Integer"
+begin
+
+text{* \textbf{WARNING} This theory implements mathematical reals by machine
+reals (floats). This is inconsistent. See the proof of False at the end of
+the theory, where an equality on mathematical reals is (incorrectly)
+disproved by mapping it to machine reals.
+
+The value command cannot display real results yet.
+
+The only legitimate use of this theory is as a tool for code generation
+purposes. *}
+
+code_type real
+ (SML "real")
+ (OCaml "float")
+
+code_const Ratreal
+ (SML "error/ \"Bad constant: Ratreal\"")
+
+code_const "0 :: real"
+ (SML "0.0")
+ (OCaml "0.0")
+declare zero_real_code[code_unfold del]
+
+code_const "1 :: real"
+ (SML "1.0")
+ (OCaml "1.0")
+declare one_real_code[code_unfold del]
+
+code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
+ (SML "Real.== ((_), (_))")
+ (OCaml "Pervasives.(=)")
+
+code_const "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool"
+ (SML "Real.<= ((_), (_))")
+ (OCaml "Pervasives.(<=)")
+
+code_const "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool"
+ (SML "Real.< ((_), (_))")
+ (OCaml "Pervasives.(<)")
+
+code_const "op + :: real \<Rightarrow> real \<Rightarrow> real"
+ (SML "Real.+ ((_), (_))")
+ (OCaml "Pervasives.( +. )")
+
+code_const "op * :: real \<Rightarrow> real \<Rightarrow> real"
+ (SML "Real.* ((_), (_))")
+ (OCaml "Pervasives.( *. )")
+
+code_const "op - :: real \<Rightarrow> real \<Rightarrow> real"
+ (SML "Real.- ((_), (_))")
+ (OCaml "Pervasives.( -. )")
+
+code_const "uminus :: real \<Rightarrow> real"
+ (SML "Real.~")
+ (OCaml "Pervasives.( ~-. )")
+
+code_const "op / :: real \<Rightarrow> real \<Rightarrow> real"
+ (SML "Real.'/ ((_), (_))")
+ (OCaml "Pervasives.( '/. )")
+
+code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
+ (SML "Real.== ((_:real), (_))")
+
+code_const "sqrt :: real \<Rightarrow> real"
+ (SML "Math.sqrt")
+ (OCaml "Pervasives.sqrt")
+declare sqrt_def[code del]
+
+definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
+
+lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
+ unfolding real_exp_def ..
+
+code_const real_exp
+ (SML "Math.exp")
+ (OCaml "Pervasives.exp")
+declare real_exp_def[code del]
+declare exp_def[code del]
+
+hide_const (open) real_exp
+
+code_const ln
+ (SML "Math.ln")
+ (OCaml "Pervasives.ln")
+declare ln_def[code del]
+
+code_const cos
+ (SML "Math.cos")
+ (OCaml "Pervasives.cos")
+declare cos_def[code del]
+
+code_const sin
+ (SML "Math.sin")
+ (OCaml "Pervasives.sin")
+declare sin_def[code del]
+
+code_const pi
+ (SML "Math.pi")
+ (OCaml "Pervasives.pi")
+declare pi_def[code del]
+
+code_const arctan
+ (SML "Math.atan")
+ (OCaml "Pervasives.atan")
+declare arctan_def[code del]
+
+code_const arccos
+ (SML "Math.scos")
+ (OCaml "Pervasives.acos")
+declare arccos_def[code del]
+
+code_const arcsin
+ (SML "Math.asin")
+ (OCaml "Pervasives.asin")
+declare arcsin_def[code del]
+
+definition real_of_int :: "int \<Rightarrow> real" where
+ "real_of_int \<equiv> of_int"
+
+code_const real_of_int
+ (SML "Real.fromInt")
+ (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
+
+lemma of_int_eq_real_of_int[code_unfold]: "of_int = real_of_int"
+ unfolding real_of_int_def ..
+
+hide_const (open) real_of_int
+
+declare number_of_real_code [code_unfold del]
+
+lemma "False"
+proof-
+ have "cos(pi/2) = 0" by(rule cos_pi_half)
+ moreover have "cos(pi/2) \<noteq> 0" by eval
+ ultimately show "False" by blast
+qed
+
+lemma False
+ sorry -- "Use quick_and_dirty to load this theory."
+
+end
--- a/src/HOL/Library/Float.thy Mon Nov 14 19:35:05 2011 +0100
+++ b/src/HOL/Library/Float.thy Mon Nov 14 19:35:41 2011 +0100
@@ -72,78 +72,19 @@
lemma pow2_1[simp]: "pow2 1 = 2" by simp
lemma pow2_neg: "pow2 x = inverse (pow2 (-x))" by simp
-declare pow2_def[simp del]
+lemma pow2_powr: "pow2 a = 2 powr a"
+ by (simp add: powr_realpow[symmetric] powr_minus)
-lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
-proof -
- have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith
- have g: "! a b. a - -1 = a + (1::int)" by arith
- have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)"
- apply (auto, induct_tac n)
- apply (simp_all add: pow2_def)
- apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
- by (auto simp add: h)
- show ?thesis
- proof (induct a)
- case (nonneg n)
- from pos show ?case by (simp add: algebra_simps)
- next
- case (neg n)
- show ?case
- apply (auto)
- apply (subst pow2_neg[of "- int n"])
- apply (subst pow2_neg[of "-1 - int n"])
- apply (auto simp add: g pos)
- done
- qed
-qed
+declare pow2_def[simp del]
lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
-proof (induct b)
- case (nonneg n)
- show ?case
- proof (induct n)
- case 0
- show ?case by simp
- next
- case (Suc m)
- then show ?case by (auto simp add: algebra_simps pow2_add1)
- qed
-next
- case (neg n)
- show ?case
- proof (induct n)
- case 0
- show ?case
- apply (auto)
- apply (subst pow2_neg[of "a + -1"])
- apply (subst pow2_neg[of "-1"])
- apply (simp)
- apply (insert pow2_add1[of "-a"])
- apply (simp add: algebra_simps)
- apply (subst pow2_neg[of "-a"])
- apply (simp)
- done
- next
- case (Suc m)
- have a: "int m - (a + -2) = 1 + (int m - a + 1)" by arith
- have b: "int m - -2 = 1 + (int m + 1)" by arith
- show ?case
- apply (auto)
- apply (subst pow2_neg[of "a + (-2 - int m)"])
- apply (subst pow2_neg[of "-2 - int m"])
- apply (auto simp add: algebra_simps)
- apply (subst a)
- apply (subst b)
- apply (simp only: pow2_add1)
- apply (subst pow2_neg[of "int m - a + 1"])
- apply (subst pow2_neg[of "int m + 1"])
- apply auto
- apply (insert Suc)
- apply (auto simp add: algebra_simps)
- done
- qed
-qed
+ by (simp add: pow2_powr powr_add)
+
+lemma pow2_diff: "pow2 (a - b) = pow2 a / pow2 b"
+ by (simp add: pow2_powr powr_divide2)
+
+lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
+ by (simp add: pow2_add)
lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f) auto
@@ -185,23 +126,7 @@
lemma zero_less_pow2[simp]:
"0 < pow2 x"
-proof -
- {
- fix y
- have "0 <= y \<Longrightarrow> 0 < pow2 y"
- apply (induct y)
- apply (induct_tac n)
- apply (simp_all add: pow2_add)
- done
- }
- note helper=this
- show ?thesis
- apply (case_tac "0 <= x")
- apply (simp add: helper)
- apply (subst pow2_neg)
- apply (simp add: helper)
- done
-qed
+ by (simp add: pow2_powr)
lemma normfloat_imp_odd_or_zero: "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)"
proof (induct f rule: normfloat.induct)
@@ -245,46 +170,19 @@
and floateq: "real (Float a b) = real (Float a' b')"
shows "b \<le> b'"
proof -
+ from odd have "a' \<noteq> 0" by auto
+ with floateq have a': "real a' = real a * pow2 (b - b')"
+ by (simp add: pow2_diff field_simps)
+
{
assume bcmp: "b > b'"
- from floateq have eq: "real a * pow2 b = real a' * pow2 b'" by simp
- {
- fix x y z :: real
- assume "y \<noteq> 0"
- then have "(x * inverse y = z) = (x = z * y)"
- by auto
- }
- note inverse = this
- have eq': "real a * (pow2 (b - b')) = real a'"
- apply (subst diff_int_def)
- apply (subst pow2_add)
- apply (subst pow2_neg[where x = "-b'"])
- apply simp
- apply (subst mult_assoc[symmetric])
- apply (subst inverse)
- apply (simp_all add: eq)
- done
- have "\<exists> z > 0. pow2 (b-b') = 2^z"
- apply (rule exI[where x="nat (b - b')"])
- apply (auto)
- apply (insert bcmp)
- apply simp
- apply (subst pow2_int[symmetric])
- apply auto
- done
- then obtain z where z: "z > 0 \<and> pow2 (b-b') = 2^z" by auto
- with eq' have "real a * 2^z = real a'"
- by auto
- then have "real a * real ((2::int)^z) = real a'"
- by auto
- then have "real (a * 2^z) = real a'"
- apply (subst real_of_int_mult)
- apply simp
- done
- then have a'_rep: "a * 2^z = a'" by arith
- then have "a' = a*2^z" by simp
- with z have "even a'" by simp
- with odd have False by auto
+ then have "\<exists>c::nat. b - b' = int c + 1"
+ by arith
+ then guess c ..
+ with a' have "real a' = real (a * 2^c * 2)"
+ by (simp add: pow2_def nat_add_distrib)
+ with odd have False
+ unfolding real_of_int_inject by simp
}
then show ?thesis by arith
qed
--- a/src/HOL/Library/ROOT.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/HOL/Library/ROOT.ML Mon Nov 14 19:35:41 2011 +0100
@@ -3,4 +3,5 @@
use_thys ["Library", "List_Cset", "List_Prefix", "List_lexord", "Sublist_Order",
"Product_Lattice",
- "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];
+ "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*),
+ "Code_Real_Approx_By_Float" ];
--- a/src/HOL/Matrix/ComputeFloat.thy Mon Nov 14 19:35:05 2011 +0100
+++ b/src/HOL/Matrix/ComputeFloat.thy Mon Nov 14 19:35:41 2011 +0100
@@ -9,94 +9,6 @@
uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
begin
-definition pow2 :: "int \<Rightarrow> real"
- where "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
-
-definition float :: "int * int \<Rightarrow> real"
- where "float x = real (fst x) * pow2 (snd x)"
-
-lemma pow2_0[simp]: "pow2 0 = 1"
-by (simp add: pow2_def)
-
-lemma pow2_1[simp]: "pow2 1 = 2"
-by (simp add: pow2_def)
-
-lemma pow2_neg: "pow2 x = inverse (pow2 (-x))"
-by (simp add: pow2_def)
-
-lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
-proof -
- have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith
- have g: "! a b. a - -1 = a + (1::int)" by arith
- have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)"
- apply (auto, induct_tac n)
- apply (simp_all add: pow2_def)
- apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
- by (auto simp add: h)
- show ?thesis
- proof (induct a)
- case (nonneg n)
- from pos show ?case by (simp add: algebra_simps)
- next
- case (neg n)
- show ?case
- apply (auto)
- apply (subst pow2_neg[of "- int n"])
- apply (subst pow2_neg[of "-1 - int n"])
- apply (auto simp add: g pos)
- done
- qed
-qed
-
-lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
-proof (induct b)
- case (nonneg n)
- show ?case
- proof (induct n)
- case 0
- show ?case by simp
- next
- case (Suc m)
- show ?case by (auto simp add: algebra_simps pow2_add1 nonneg Suc)
- qed
-next
- case (neg n)
- show ?case
- proof (induct n)
- case 0
- show ?case
- apply (auto)
- apply (subst pow2_neg[of "a + -1"])
- apply (subst pow2_neg[of "-1"])
- apply (simp)
- apply (insert pow2_add1[of "-a"])
- apply (simp add: algebra_simps)
- apply (subst pow2_neg[of "-a"])
- apply (simp)
- done
- case (Suc m)
- have a: "int m - (a + -2) = 1 + (int m - a + 1)" by arith
- have b: "int m - -2 = 1 + (int m + 1)" by arith
- show ?case
- apply (auto)
- apply (subst pow2_neg[of "a + (-2 - int m)"])
- apply (subst pow2_neg[of "-2 - int m"])
- apply (auto simp add: algebra_simps)
- apply (subst a)
- apply (subst b)
- apply (simp only: pow2_add1)
- apply (subst pow2_neg[of "int m - a + 1"])
- apply (subst pow2_neg[of "int m + 1"])
- apply auto
- apply (insert Suc)
- apply (auto simp add: algebra_simps)
- done
- qed
-qed
-
-lemma "float (a, e) + float (b, e) = float (a + b, e)"
-by (simp add: float_def algebra_simps)
-
definition int_of_real :: "real \<Rightarrow> int"
where "int_of_real x = (SOME y. real y = x)"
@@ -104,16 +16,7 @@
where "real_is_int x = (EX (u::int). x = real u)"
lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"
-by (auto simp add: real_is_int_def int_of_real_def)
-
-lemma float_transfer: "real_is_int ((real a)*(pow2 c)) \<Longrightarrow> float (a, b) = float (int_of_real ((real a)*(pow2 c)), b - c)"
-by (simp add: float_def real_is_int_def2 pow2_add[symmetric])
-
-lemma pow2_int: "pow2 (int c) = 2^c"
-by (simp add: pow2_def)
-
-lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)"
-by (simp add: float_def pow2_int[symmetric] pow2_add[symmetric])
+ by (auto simp add: real_is_int_def int_of_real_def)
lemma real_is_int_real[simp]: "real_is_int (real (x::int))"
by (auto simp add: real_is_int_def int_of_real_def)
@@ -146,18 +49,9 @@
lemma int_of_real_mult:
assumes "real_is_int a" "real_is_int b"
shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)"
-proof -
- from assms have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto)
- from assms have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto)
- from a obtain a'::int where a':"a = real a'" by auto
- from b obtain b'::int where b':"b = real b'" by auto
- have r: "real a' * real b' = real (a' * b')" by auto
- show ?thesis
- apply (simp add: a' b')
- apply (subst r)
- apply (simp only: int_of_real_real)
- done
-qed
+ using assms
+ by (auto simp add: real_is_int_def real_of_int_mult[symmetric]
+ simp del: real_of_int_mult)
lemma real_is_int_mult[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a*b)"
apply (subst real_is_int_def2)
@@ -182,47 +76,7 @@
qed
lemma real_is_int_number_of[simp]: "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
-proof -
- have neg1: "real_is_int (-1::real)"
- proof -
- have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto
- also have "\<dots> = True" by (simp only: real_is_int_real)
- ultimately show ?thesis by auto
- qed
-
- {
- fix x :: int
- have "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
- unfolding number_of_eq
- apply (induct x)
- apply (induct_tac n)
- apply (simp)
- apply (simp)
- apply (induct_tac n)
- apply (simp add: neg1)
- proof -
- fix n :: nat
- assume rn: "(real_is_int (of_int (- (int (Suc n)))))"
- have s: "-(int (Suc (Suc n))) = -1 + - (int (Suc n))" by simp
- show "real_is_int (of_int (- (int (Suc (Suc n)))))"
- apply (simp only: s of_int_add)
- apply (rule real_is_int_add)
- apply (simp add: neg1)
- apply (simp only: rn)
- done
- qed
- }
- note Abs_Bin = this
- {
- fix x :: int
- have "? u. x = u"
- apply (rule exI[where x = "x"])
- apply (simp)
- done
- }
- then obtain u::int where "x = u" by auto
- with Abs_Bin show ?thesis by auto
-qed
+ by (auto simp: real_is_int_def intro!: exI[of _ "number_of x"])
lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)"
by (simp add: int_of_real_def)
@@ -234,30 +88,9 @@
qed
lemma int_of_real_number_of[simp]: "int_of_real (number_of b) = number_of b"
-proof -
- have "real_is_int (number_of b)" by simp
- then have uu: "?! u::int. number_of b = real u" by (auto simp add: real_is_int_rep)
- then obtain u::int where u:"number_of b = real u" by auto
- have "number_of b = real ((number_of b)::int)"
- by (simp add: number_of_eq real_of_int_def)
- have ub: "number_of b = real ((number_of b)::int)"
- by (simp add: number_of_eq real_of_int_def)
- from uu u ub have unb: "u = number_of b"
- by blast
- have "int_of_real (number_of b) = u" by (simp add: u)
- with unb show ?thesis by simp
-qed
-
-lemma float_transfer_even: "even a \<Longrightarrow> float (a, b) = float (a div 2, b+1)"
- apply (subst float_transfer[where a="a" and b="b" and c="-1", simplified])
- apply (simp_all add: pow2_def even_def real_is_int_def algebra_simps)
- apply (auto)
-proof -
- fix q::int
- have a:"b - (-1\<Colon>int) = (1\<Colon>int) + b" by arith
- show "(float (q, (b - (-1\<Colon>int)))) = (float (q, ((1\<Colon>int) + b)))"
- by (simp add: a)
-qed
+ unfolding int_of_real_def
+ by (intro some_equality)
+ (auto simp add: real_of_int_inject[symmetric] simp del: real_of_int_inject)
lemma int_div_zdiv: "int (a div b) = (int a) div (int b)"
by (rule zdiv_int)
@@ -268,163 +101,6 @@
lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
by arith
-function norm_float :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
- "norm_float a b = (if a \<noteq> 0 \<and> even a then norm_float (a div 2) (b + 1)
- else if a = 0 then (0, 0) else (a, b))"
-by auto
-
-termination by (relation "measure (nat o abs o fst)")
- (auto intro: abs_div_2_less)
-
-lemma norm_float: "float x = float (split norm_float x)"
-proof -
- {
- fix a b :: int
- have norm_float_pair: "float (a, b) = float (norm_float a b)"
- proof (induct a b rule: norm_float.induct)
- case (1 u v)
- show ?case
- proof cases
- assume u: "u \<noteq> 0 \<and> even u"
- with 1 have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto
- with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
- then show ?thesis
- apply (subst norm_float.simps)
- apply (simp add: ind)
- done
- next
- assume nu: "~(u \<noteq> 0 \<and> even u)"
- show ?thesis
- by (simp add: nu float_def)
- qed
- qed
- }
- note helper = this
- have "? a b. x = (a,b)" by auto
- then obtain a b where "x = (a, b)" by blast
- then show ?thesis by (simp add: helper)
-qed
-
-lemma float_add_l0: "float (0, e) + x = x"
- by (simp add: float_def)
-
-lemma float_add_r0: "x + float (0, e) = x"
- by (simp add: float_def)
-
-lemma float_add:
- "float (a1, e1) + float (a2, e2) =
- (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
- else float (a1*2^(nat (e1-e2))+a2, e2))"
- apply (simp add: float_def algebra_simps)
- apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric])
- done
-
-lemma float_add_assoc1:
- "(x + float (y1, e1)) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x"
- by simp
-
-lemma float_add_assoc2:
- "(float (y1, e1) + x) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x"
- by simp
-
-lemma float_add_assoc3:
- "float (y1, e1) + (x + float (y2, e2)) = (float (y1, e1) + float (y2, e2)) + x"
- by simp
-
-lemma float_add_assoc4:
- "float (y1, e1) + (float (y2, e2) + x) = (float (y1, e1) + float (y2, e2)) + x"
- by simp
-
-lemma float_mult_l0: "float (0, e) * x = float (0, 0)"
- by (simp add: float_def)
-
-lemma float_mult_r0: "x * float (0, e) = float (0, 0)"
- by (simp add: float_def)
-
-definition lbound :: "real \<Rightarrow> real"
- where "lbound x = min 0 x"
-
-definition ubound :: "real \<Rightarrow> real"
- where "ubound x = max 0 x"
-
-lemma lbound: "lbound x \<le> x"
- by (simp add: lbound_def)
-
-lemma ubound: "x \<le> ubound x"
- by (simp add: ubound_def)
-
-lemma float_mult:
- "float (a1, e1) * float (a2, e2) =
- (float (a1 * a2, e1 + e2))"
- by (simp add: float_def pow2_add)
-
-lemma float_minus:
- "- (float (a,b)) = float (-a, b)"
- by (simp add: float_def)
-
-lemma zero_less_pow2:
- "0 < pow2 x"
-proof -
- {
- fix y
- have "0 <= y \<Longrightarrow> 0 < pow2 y"
- by (induct y, induct_tac n, simp_all add: pow2_add)
- }
- note helper=this
- show ?thesis
- apply (case_tac "0 <= x")
- apply (simp add: helper)
- apply (subst pow2_neg)
- apply (simp add: helper)
- done
-qed
-
-lemma zero_le_float:
- "(0 <= float (a,b)) = (0 <= a)"
- apply (auto simp add: float_def)
- apply (auto simp add: zero_le_mult_iff zero_less_pow2)
- apply (insert zero_less_pow2[of b])
- apply (simp_all)
- done
-
-lemma float_le_zero:
- "(float (a,b) <= 0) = (a <= 0)"
- apply (auto simp add: float_def)
- apply (auto simp add: mult_le_0_iff)
- apply (insert zero_less_pow2[of b])
- apply auto
- done
-
-lemma float_abs:
- "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
- apply (auto simp add: abs_if)
- apply (simp_all add: zero_le_float[symmetric, of a b] float_minus)
- done
-
-lemma float_zero:
- "float (0, b) = 0"
- by (simp add: float_def)
-
-lemma float_pprt:
- "pprt (float (a, b)) = (if 0 <= a then (float (a,b)) else (float (0, b)))"
- by (auto simp add: zero_le_float float_le_zero float_zero)
-
-lemma pprt_lbound: "pprt (lbound x) = float (0, 0)"
- apply (simp add: float_def)
- apply (rule pprt_eq_0)
- apply (simp add: lbound_def)
- done
-
-lemma nprt_ubound: "nprt (ubound x) = float (0, 0)"
- apply (simp add: float_def)
- apply (rule nprt_eq_0)
- apply (simp add: ubound_def)
- done
-
-lemma float_nprt:
- "nprt (float (a, b)) = (if 0 <= a then (float (0,b)) else (float (a, b)))"
- by (auto simp add: zero_le_float float_le_zero float_zero)
-
lemma norm_0_1: "(0::_::number_ring) = Numeral0 & (1::_::number_ring) = Numeral1"
by auto
@@ -549,6 +225,79 @@
zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
zpower_Pls zpower_Min
+definition float :: "(int \<times> int) \<Rightarrow> real" where
+ "float = (\<lambda>(a, b). real a * 2 powr real b)"
+
+lemma float_add_l0: "float (0, e) + x = x"
+ by (simp add: float_def)
+
+lemma float_add_r0: "x + float (0, e) = x"
+ by (simp add: float_def)
+
+lemma float_add:
+ "float (a1, e1) + float (a2, e2) =
+ (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1) else float (a1*2^(nat (e1-e2))+a2, e2))"
+ by (simp add: float_def algebra_simps powr_realpow[symmetric] powr_divide2[symmetric])
+
+lemma float_mult_l0: "float (0, e) * x = float (0, 0)"
+ by (simp add: float_def)
+
+lemma float_mult_r0: "x * float (0, e) = float (0, 0)"
+ by (simp add: float_def)
+
+lemma float_mult:
+ "float (a1, e1) * float (a2, e2) = (float (a1 * a2, e1 + e2))"
+ by (simp add: float_def powr_add)
+
+lemma float_minus:
+ "- (float (a,b)) = float (-a, b)"
+ by (simp add: float_def)
+
+lemma zero_le_float:
+ "(0 <= float (a,b)) = (0 <= a)"
+ using powr_gt_zero[of 2 "real b", arith]
+ by (simp add: float_def zero_le_mult_iff)
+
+lemma float_le_zero:
+ "(float (a,b) <= 0) = (a <= 0)"
+ using powr_gt_zero[of 2 "real b", arith]
+ by (simp add: float_def mult_le_0_iff)
+
+lemma float_abs:
+ "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
+ using powr_gt_zero[of 2 "real b", arith]
+ by (simp add: float_def abs_if mult_less_0_iff)
+
+lemma float_zero:
+ "float (0, b) = 0"
+ by (simp add: float_def)
+
+lemma float_pprt:
+ "pprt (float (a, b)) = (if 0 <= a then (float (a,b)) else (float (0, b)))"
+ by (auto simp add: zero_le_float float_le_zero float_zero)
+
+lemma float_nprt:
+ "nprt (float (a, b)) = (if 0 <= a then (float (0,b)) else (float (a, b)))"
+ by (auto simp add: zero_le_float float_le_zero float_zero)
+
+definition lbound :: "real \<Rightarrow> real"
+ where "lbound x = min 0 x"
+
+definition ubound :: "real \<Rightarrow> real"
+ where "ubound x = max 0 x"
+
+lemma lbound: "lbound x \<le> x"
+ by (simp add: lbound_def)
+
+lemma ubound: "x \<le> ubound x"
+ by (simp add: ubound_def)
+
+lemma pprt_lbound: "pprt (lbound x) = float (0, 0)"
+ by (auto simp: float_def lbound_def)
+
+lemma nprt_ubound: "nprt (ubound x) = float (0, 0)"
+ by (auto simp: float_def ubound_def)
+
lemmas floatarith[simplified norm_0_1] = float_add float_add_l0 float_add_r0 float_mult float_mult_l0 float_mult_r0
float_minus float_abs zero_le_float float_pprt float_nprt pprt_lbound nprt_ubound
--- a/src/HOL/String.thy Mon Nov 14 19:35:05 2011 +0100
+++ b/src/HOL/String.thy Mon Nov 14 19:35:41 2011 +0100
@@ -69,7 +69,7 @@
by (simp add: fun_eq_iff split: char.split)
syntax
- "_Char" :: "xstr => char" ("CHR _")
+ "_Char" :: "xstr_position => char" ("CHR _")
subsection {* Strings *}
@@ -77,7 +77,7 @@
type_synonym string = "char list"
syntax
- "_String" :: "xstr => string" ("_")
+ "_String" :: "xstr_position => string" ("_")
use "Tools/string_syntax.ML"
setup String_Syntax.setup
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Nov 14 19:35:41 2011 +0100
@@ -414,8 +414,9 @@
val smart_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_smart_exhaustive_active} (K true);
val smart_slow_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_slow_smart_exhaustive_active} (K false);
-val setup =
- Context.theory_map (Quickcheck.add_tester ("smart_exhaustive",
+val setup =
+ Exhaustive_Generators.setup_exhaustive_datatype_interpretation
+ #> Context.theory_map (Quickcheck.add_tester ("smart_exhaustive",
(smart_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_CPS, false))))
#> Context.theory_map (Quickcheck.add_tester ("smart_slow_exhaustive",
(smart_slow_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_DSeq, false))))
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Nov 14 19:35:41 2011 +0100
@@ -18,6 +18,7 @@
exception Counterexample of term list
val smart_quantifier : bool Config.T
val quickcheck_pretty : bool Config.T
+ val setup_exhaustive_datatype_interpretation : theory -> theory
val setup: theory -> theory
end;
@@ -492,6 +493,10 @@
(* setup *)
+val setup_exhaustive_datatype_interpretation =
+ Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+ (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
+
val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
val setup =
--- a/src/HOL/Tools/string_syntax.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/HOL/Tools/string_syntax.ML Mon Nov 14 19:35:41 2011 +0100
@@ -52,6 +52,8 @@
(case Lexicon.explode_xstr xstr of
[c] => mk_char c
| _ => error ("Single character expected: " ^ xstr))
+ | char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
+ Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2]
| char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
fun char_ast_tr' [c1, c2] =
@@ -72,6 +74,8 @@
[Ast.Constant @{syntax_const "_constrain"},
Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
| cs => mk_string cs)
+ | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
+ Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2]
| string_ast_tr asts = raise Ast.AST ("string_tr", asts);
fun list_ast_tr' [args] =
--- a/src/Pure/Isar/isar_cmd.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Mon Nov 14 19:35:41 2011 +0100
@@ -77,7 +77,7 @@
val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
- val local_theory_markup: xstring option * (Symbol_Pos.text * Position.T) ->
+ val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.text * Position.T) ->
Toplevel.transition -> Toplevel.transition
val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
end;
--- a/src/Pure/Isar/isar_syn.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Nov 14 19:35:41 2011 +0100
@@ -394,7 +394,7 @@
val _ =
Outer_Syntax.command "context" "enter local theory context" Keyword.thy_decl
- (Parse.name --| Parse.begin >> (fn name =>
+ (Parse.position Parse.name --| Parse.begin >> (fn name =>
Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
--- a/src/Pure/Isar/locale.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/Pure/Isar/locale.ML Mon Nov 14 19:35:41 2011 +0100
@@ -37,6 +37,7 @@
(string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
(string * morphism) list -> theory -> theory
val intern: theory -> xstring -> string
+ val check: theory -> xstring * Position.T -> string
val extern: theory -> string -> xstring
val defined: theory -> string -> bool
val params_of: theory -> string -> ((string * typ) * mixfix) list
@@ -162,6 +163,7 @@
);
val intern = Name_Space.intern o #1 o Locales.get;
+fun check thy = #1 o Name_Space.check (Proof_Context.init_global thy) (Locales.get thy);
fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
val get_locale = Symtab.lookup o #2 o Locales.get;
--- a/src/Pure/Isar/named_target.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/Pure/Isar/named_target.ML Mon Nov 14 19:35:41 2011 +0100
@@ -10,7 +10,7 @@
val init: (local_theory -> local_theory) -> string -> theory -> local_theory
val theory_init: theory -> local_theory
val reinit: local_theory -> local_theory -> local_theory
- val context_cmd: xstring -> theory -> local_theory
+ val context_cmd: xstring * Position.T -> theory -> local_theory
val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
end;
@@ -209,7 +209,7 @@
init before_exit target o Local_Theory.exit_global
| NONE => error "Not in a named target");
-fun context_cmd "-" thy = init I "" thy
- | context_cmd target thy = init I (Locale.intern thy target) thy;
+fun context_cmd ("-", _) thy = init I "" thy
+ | context_cmd target thy = init I (Locale.check thy target) thy;
end;
--- a/src/Pure/Isar/parse.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/Pure/Isar/parse.ML Mon Nov 14 19:35:41 2011 +0100
@@ -99,8 +99,8 @@
val literal_fact: string parser
val propp: (string * string list) parser
val termp: (string * string list) parser
- val target: xstring parser
- val opt_target: xstring option parser
+ val target: (xstring * Position.T) parser
+ val opt_target: (xstring * Position.T) option parser
end;
structure Parse: PARSE =
@@ -362,7 +362,7 @@
(* targets *)
-val target = ($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")");
+val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
val opt_target = Scan.option target;
end;
--- a/src/Pure/Isar/runtime.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/Pure/Isar/runtime.ML Mon Nov 14 19:35:41 2011 +0100
@@ -55,8 +55,6 @@
| _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
end;
- val detailed = ! debug;
-
fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
| flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
| flatten context exn =
@@ -79,22 +77,18 @@
| ERROR msg => msg
| Fail msg => raised exn "Fail" [msg]
| THEORY (msg, thys) =>
- raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
+ raised exn "THEORY" (msg :: map Context.str_of_thy thys)
| Ast.AST (msg, asts) =>
- raised exn "AST" (msg ::
- (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))
+ raised exn "AST" (msg :: map (Pretty.string_of o Ast.pretty_ast) asts)
| TYPE (msg, Ts, ts) =>
raised exn "TYPE" (msg ::
- (if detailed then
- if_context context Syntax.string_of_typ Ts @
- if_context context Syntax.string_of_term ts
- else []))
+ (if_context context Syntax.string_of_typ Ts @
+ if_context context Syntax.string_of_term ts))
| TERM (msg, ts) =>
- raised exn "TERM" (msg ::
- (if detailed then if_context context Syntax.string_of_term ts else []))
+ raised exn "TERM" (msg :: if_context context Syntax.string_of_term ts)
| THM (msg, i, thms) =>
- raised exn ("THM " ^ string_of_int i) (msg ::
- (if detailed then if_context context Display.string_of_thm thms else []))
+ raised exn ("THM " ^ string_of_int i)
+ (msg :: if_context context Display.string_of_thm thms)
| _ => raised exn (General.exnMessage exn) []);
in [(i, msg)] end)
and sorted_msgs context exn =
@@ -111,11 +105,8 @@
(** controlled execution **)
fun debugging f x =
- if ! debug then
- Exn.release (exception_trace (fn () =>
- Exn.Res (f x) handle
- exn as UNDEF => Exn.Exn exn
- | exn as EXCURSION_FAIL _ => Exn.Exn exn))
+ if ! debug
+ then exception_trace (fn () => f x)
else f x;
fun controlled_execution f x =
--- a/src/Pure/Isar/toplevel.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Nov 14 19:35:41 2011 +0100
@@ -58,14 +58,16 @@
val theory': (bool -> theory -> theory) -> transition -> transition
val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
val end_local_theory: transition -> transition
- val local_theory': xstring option -> (bool -> local_theory -> local_theory) ->
+ val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) ->
+ transition -> transition
+ val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) ->
transition -> transition
- val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
- val present_local_theory: xstring option -> (state -> unit) -> transition -> transition
- val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
+ val present_local_theory: (xstring * Position.T) option -> (state -> unit) ->
transition -> transition
- val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) ->
- transition -> transition
+ val local_theory_to_proof': (xstring * Position.T) option ->
+ (bool -> local_theory -> Proof.state) -> transition -> transition
+ val local_theory_to_proof: (xstring * Position.T) option ->
+ (local_theory -> Proof.state) -> transition -> transition
val theory_to_proof: (theory -> Proof.state) -> transition -> transition
val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
val forget_proof: transition -> transition
@@ -105,7 +107,7 @@
val loc_init = Named_Target.context_cmd;
val loc_exit = Local_Theory.exit_global;
-fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
+fun loc_begin loc (Context.Theory thy) = loc_init (the_default ("-", Position.none) loc) thy
| loc_begin NONE (Context.Proof lthy) = lthy
| loc_begin (SOME loc) (Context.Proof lthy) = (loc_init loc o loc_exit) lthy;
--- a/src/Pure/Syntax/syntax.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML Mon Nov 14 19:35:41 2011 +0100
@@ -543,7 +543,7 @@
(Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
"args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
"any", "prop'", "num_const", "float_const", "index", "struct",
- "id_position", "longid_position", "type_name", "class_name"]);
+ "id_position", "longid_position", "xstr_position", "type_name", "class_name"]);
--- a/src/Pure/pure_thy.ML Mon Nov 14 19:35:05 2011 +0100
+++ b/src/Pure/pure_thy.ML Mon Nov 14 19:35:41 2011 +0100
@@ -135,6 +135,7 @@
("_constrainAbs", typ "'a", NoSyn),
("_position", typ "id => id_position", Delimfix "_"),
("_position", typ "longid => longid_position", Delimfix "_"),
+ ("_position", typ "xstr => xstr_position", Delimfix "_"),
("_type_constraint_", typ "'a", NoSyn),
("_context_const", typ "id_position => logic", Delimfix "CONST _"),
("_context_const", typ "id_position => aprop", Delimfix "CONST _"),
--- a/src/Tools/jEdit/src/isabelle_markup.scala Mon Nov 14 19:35:05 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Mon Nov 14 19:35:41 2011 +0100
@@ -215,7 +215,7 @@
private val subexp_include =
Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
- Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
+ Markup.ENTITY, Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE)
val subexp =