--- a/Admin/isatest/isatest-makeall Mon Jun 08 09:22:47 2009 +0200
+++ b/Admin/isatest/isatest-makeall Mon Jun 08 09:23:04 2009 +0200
@@ -76,6 +76,11 @@
NICE=""
;;
+ macbroy23)
+ MFLAGS=""
+ NICE=""
+ ;;
+
macbroy2[0-9])
MFLAGS="-j 2"
NICE=""
--- a/doc-src/System/Thy/Misc.thy Mon Jun 08 09:22:47 2009 +0200
+++ b/doc-src/System/Thy/Misc.thy Mon Jun 08 09:23:04 2009 +0200
@@ -85,6 +85,8 @@
Options are:
-a display complete environment
-b print values only (doesn't work for -a)
+ -d FILE dump complete environment to FILE
+ (null terminated entries)
Get value of VARNAMES from the Isabelle settings.
\end{ttbox}
@@ -95,6 +97,10 @@
Normally, output is a list of lines of the form @{text
name}@{verbatim "="}@{text value}. The @{verbatim "-b"} option
causes only the values to be printed.
+
+ Option @{verbatim "-d"} produces a dump of the complete environment
+ to the specified file. Entries are terminated by the ASCII null
+ character, i.e.\ the C string terminator.
*}
--- a/doc-src/System/Thy/document/Misc.tex Mon Jun 08 09:22:47 2009 +0200
+++ b/doc-src/System/Thy/document/Misc.tex Mon Jun 08 09:23:04 2009 +0200
@@ -110,6 +110,8 @@
Options are:
-a display complete environment
-b print values only (doesn't work for -a)
+ -d FILE dump complete environment to FILE
+ (null terminated entries)
Get value of VARNAMES from the Isabelle settings.
\end{ttbox}
@@ -118,7 +120,11 @@
environment that Isabelle related programs are run in. This usually
contains much more variables than are actually Isabelle settings.
Normally, output is a list of lines of the form \isa{name}\verb|=|\isa{value}. The \verb|-b| option
- causes only the values to be printed.%
+ causes only the values to be printed.
+
+ Option \verb|-d| produces a dump of the complete environment
+ to the specified file. Entries are terminated by the ASCII null
+ character, i.e.\ the C string terminator.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/lib/Tools/getenv Mon Jun 08 09:22:47 2009 +0200
+++ b/lib/Tools/getenv Mon Jun 08 09:23:04 2009 +0200
@@ -17,6 +17,8 @@
echo " Options are:"
echo " -a display complete environment"
echo " -b print values only (doesn't work for -a)"
+ echo " -d FILE dump complete environment to FILE"
+ echo " (null terminated entries)"
echo
echo " Get value of VARNAMES from the Isabelle settings."
echo
@@ -30,8 +32,9 @@
ALL=""
BASE=""
+DUMP=""
-while getopts "ab" OPT
+while getopts "abd:" OPT
do
case "$OPT" in
a)
@@ -40,6 +43,9 @@
b)
BASE=true
;;
+ d)
+ DUMP="$OPTARG"
+ ;;
\?)
usage
;;
@@ -68,3 +74,8 @@
fi
done
fi
+
+if [ -n "$DUMP" ]; then
+ exec perl -w -e 'for $key (keys %ENV) { print $key, "=", $ENV{$key}, "\x00"; }' > "$DUMP"
+fi
+
--- a/src/HOL/Decision_Procs/Approximation.thy Mon Jun 08 09:22:47 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Jun 08 09:23:04 2009 +0200
@@ -142,7 +142,7 @@
lemma get_odd_ex: "\<exists> k. Suc k = get_odd n \<and> odd (Suc k)"
proof (cases "odd n")
case True hence "0 < n" by (rule odd_pos)
- from gr0_implies_Suc[OF this] obtain k where "Suc k = n" by auto
+ from gr0_implies_Suc[OF this] obtain k where "Suc k = n" by auto
thus ?thesis unfolding get_odd_def if_P[OF True] using True[unfolded `Suc k = n`[symmetric]] by blast
next
case False hence "odd (Suc n)" by auto
@@ -162,7 +162,7 @@
lemma float_power_bnds: assumes "(l1, u1) = float_power_bnds n l u" and "x \<in> {real l .. real u}"
shows "x ^ n \<in> {real l1..real u1}"
proof (cases "even n")
- case True
+ case True
show ?thesis
proof (cases "0 < l")
case True hence "odd n \<or> 0 < l" and "0 \<le> real l" unfolding less_float_def by auto
@@ -179,7 +179,7 @@
moreover have u1: "u1 = l ^ n" and l1: "l1 = u ^ n" using assms unfolding float_power_bnds_def if_not_P[OF P] if_P[OF True] by auto
ultimately show ?thesis using float_power by auto
next
- case False
+ case False
have "\<bar>x\<bar> \<le> real (max (-l) u)"
proof (cases "-l \<le> u")
case True thus ?thesis unfolding max_def if_P[OF True] using assms unfolding le_float_def by auto
@@ -212,14 +212,21 @@
fun sqrt_iteration :: "nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" where
"sqrt_iteration prec 0 (Float m e) = Float 1 ((e + bitlen m) div 2 + 1)" |
-"sqrt_iteration prec (Suc m) x = (let y = sqrt_iteration prec m x
+"sqrt_iteration prec (Suc m) x = (let y = sqrt_iteration prec m x
in Float 1 -1 * (y + float_divr prec x y))"
-definition ub_sqrt :: "nat \<Rightarrow> float \<Rightarrow> float option" where
-"ub_sqrt prec x = (if 0 < x then Some (sqrt_iteration prec prec x) else if x < 0 then None else Some 0)"
+function ub_sqrt lb_sqrt :: "nat \<Rightarrow> float \<Rightarrow> float" where
+"ub_sqrt prec x = (if 0 < x then (sqrt_iteration prec prec x)
+ else if x < 0 then - lb_sqrt prec (- x)
+ else 0)" |
+"lb_sqrt prec x = (if 0 < x then (float_divl prec x (sqrt_iteration prec prec x))
+ else if x < 0 then - ub_sqrt prec (- x)
+ else 0)"
+by pat_completeness auto
+termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto simp add: less_float_def)
-definition lb_sqrt :: "nat \<Rightarrow> float \<Rightarrow> float option" where
-"lb_sqrt prec x = (if 0 < x then Some (float_divl prec x (sqrt_iteration prec prec x)) else if x < 0 then None else Some 0)"
+declare lb_sqrt.simps[simp del]
+declare ub_sqrt.simps[simp del]
lemma sqrt_ub_pos_pos_1:
assumes "sqrt x < b" and "0 < b" and "0 < x"
@@ -250,7 +257,7 @@
unfolding pow2_add pow2_int Float real_of_float_simp by auto
also have "\<dots> < 1 * pow2 (e + int (nat (bitlen m)))"
proof (rule mult_strict_right_mono, auto)
- show "real m < 2^nat (bitlen m)" using bitlen_bounds[OF `0 < m`, THEN conjunct2]
+ show "real m < 2^nat (bitlen m)" using bitlen_bounds[OF `0 < m`, THEN conjunct2]
unfolding real_of_int_less_iff[of m, symmetric] by auto
qed
finally have "sqrt (real x) < sqrt (pow2 (e + bitlen m))" unfolding int_nat_bl by auto
@@ -261,8 +268,8 @@
proof (cases "?E mod 2 = 1")
case True thus ?thesis by auto
next
- case False
- have "0 \<le> ?E mod 2" by auto
+ case False
+ have "0 \<le> ?E mod 2" by auto
have "?E mod 2 < 2" by auto
from this[THEN zless_imp_add1_zle]
have "?E mod 2 \<le> 0" using False by auto
@@ -277,12 +284,12 @@
unfolding E_eq unfolding pow2_add ..
also have "\<dots> = pow2 (?E div 2) * sqrt (pow2 (?E mod 2))"
unfolding real_sqrt_mult[of _ "pow2 (?E mod 2)"] real_sqrt_abs2 by auto
- also have "\<dots> < pow2 (?E div 2) * 2"
+ also have "\<dots> < pow2 (?E div 2) * 2"
by (rule mult_strict_left_mono, auto intro: E_mod_pow)
also have "\<dots> = pow2 (?E div 2 + 1)" unfolding zadd_commute[of _ 1] pow2_add1 by auto
finally show ?thesis by auto
qed
- finally show ?thesis
+ finally show ?thesis
unfolding Float sqrt_iteration.simps real_of_float_simp by auto
qed
next
@@ -305,88 +312,77 @@
qed
lemma lb_sqrt_lower_bound: assumes "0 \<le> real x"
- shows "0 \<le> real (the (lb_sqrt prec x))"
+ shows "0 \<le> real (lb_sqrt prec x)"
proof (cases "0 < x")
case True hence "0 < real x" and "0 \<le> x" using `0 \<le> real x` unfolding less_float_def le_float_def by auto
hence "0 < sqrt_iteration prec prec x" unfolding less_float_def using sqrt_iteration_lower_bound by auto
hence "0 \<le> real (float_divl prec x (sqrt_iteration prec prec x))" using float_divl_lower_bound[OF `0 \<le> x`] unfolding le_float_def by auto
- thus ?thesis unfolding lb_sqrt_def using True by auto
+ thus ?thesis unfolding lb_sqrt.simps using True by auto
next
case False with `0 \<le> real x` have "real x = 0" unfolding less_float_def by auto
- thus ?thesis unfolding lb_sqrt_def less_float_def by auto
-qed
-
-lemma lb_sqrt_upper_bound: assumes "0 \<le> real x"
- shows "real (the (lb_sqrt prec x)) \<le> sqrt (real x)"
-proof (cases "0 < x")
- case True hence "0 < real x" and "0 \<le> real x" unfolding less_float_def by auto
- hence sqrt_gt0: "0 < sqrt (real x)" by auto
- hence sqrt_ub: "sqrt (real x) < real (sqrt_iteration prec prec x)" using sqrt_iteration_bound by auto
-
- have "real (float_divl prec x (sqrt_iteration prec prec x)) \<le> real x / real (sqrt_iteration prec prec x)" by (rule float_divl)
- also have "\<dots> < real x / sqrt (real x)"
- by (rule divide_strict_left_mono[OF sqrt_ub `0 < real x` mult_pos_pos[OF order_less_trans[OF sqrt_gt0 sqrt_ub] sqrt_gt0]])
- also have "\<dots> = sqrt (real x)" unfolding inverse_eq_iff_eq[of _ "sqrt (real x)", symmetric] sqrt_divide_self_eq[OF `0 \<le> real x`, symmetric] by auto
- finally show ?thesis unfolding lb_sqrt_def if_P[OF `0 < x`] by auto
-next
- case False with `0 \<le> real x`
- have "\<not> x < 0" unfolding less_float_def le_float_def by auto
- show ?thesis unfolding lb_sqrt_def if_not_P[OF False] if_not_P[OF `\<not> x < 0`] using assms by auto
-qed
-
-lemma lb_sqrt: assumes "Some y = lb_sqrt prec x"
- shows "real y \<le> sqrt (real x)" and "0 \<le> real x"
-proof -
- show "0 \<le> real x"
- proof (rule ccontr)
- assume "\<not> 0 \<le> real x"
- hence "lb_sqrt prec x = None" unfolding lb_sqrt_def less_float_def by auto
- thus False using assms by auto
- qed
- from lb_sqrt_upper_bound[OF this, of prec]
- show "real y \<le> sqrt (real x)" unfolding assms[symmetric] by auto
+ thus ?thesis unfolding lb_sqrt.simps less_float_def by auto
qed
-lemma ub_sqrt_lower_bound: assumes "0 \<le> real x"
- shows "sqrt (real x) \<le> real (the (ub_sqrt prec x))"
-proof (cases "0 < x")
- case True hence "0 < real x" unfolding less_float_def by auto
- hence "0 < sqrt (real x)" by auto
- hence "sqrt (real x) < real (sqrt_iteration prec prec x)" using sqrt_iteration_bound by auto
- thus ?thesis unfolding ub_sqrt_def if_P[OF `0 < x`] by auto
-next
- case False with `0 \<le> real x`
- have "real x = 0" unfolding less_float_def le_float_def by auto
- thus ?thesis unfolding ub_sqrt_def less_float_def le_float_def by auto
+lemma bnds_sqrt':
+ shows "sqrt (real x) \<in> { real (lb_sqrt prec x) .. real (ub_sqrt prec x) }"
+proof -
+ { fix x :: float assume "0 < x"
+ hence "0 < real x" and "0 \<le> real x" unfolding less_float_def by auto
+ hence sqrt_gt0: "0 < sqrt (real x)" by auto
+ hence sqrt_ub: "sqrt (real x) < real (sqrt_iteration prec prec x)" using sqrt_iteration_bound by auto
+
+ have "real (float_divl prec x (sqrt_iteration prec prec x)) \<le>
+ real x / real (sqrt_iteration prec prec x)" by (rule float_divl)
+ also have "\<dots> < real x / sqrt (real x)"
+ by (rule divide_strict_left_mono[OF sqrt_ub `0 < real x`
+ mult_pos_pos[OF order_less_trans[OF sqrt_gt0 sqrt_ub] sqrt_gt0]])
+ also have "\<dots> = sqrt (real x)"
+ unfolding inverse_eq_iff_eq[of _ "sqrt (real x)", symmetric]
+ sqrt_divide_self_eq[OF `0 \<le> real x`, symmetric] by auto
+ finally have "real (lb_sqrt prec x) \<le> sqrt (real x)"
+ unfolding lb_sqrt.simps if_P[OF `0 < x`] by auto }
+ note lb = this
+
+ { fix x :: float assume "0 < x"
+ hence "0 < real x" unfolding less_float_def by auto
+ hence "0 < sqrt (real x)" by auto
+ hence "sqrt (real x) < real (sqrt_iteration prec prec x)"
+ using sqrt_iteration_bound by auto
+ hence "sqrt (real x) \<le> real (ub_sqrt prec x)"
+ unfolding ub_sqrt.simps if_P[OF `0 < x`] by auto }
+ note ub = this
+
+ show ?thesis
+ proof (cases "0 < x")
+ case True with lb ub show ?thesis by auto
+ next case False show ?thesis
+ proof (cases "real x = 0")
+ case True thus ?thesis
+ by (auto simp add: less_float_def lb_sqrt.simps ub_sqrt.simps)
+ next
+ case False with `\<not> 0 < x` have "x < 0" and "0 < -x"
+ by (auto simp add: less_float_def)
+
+ with `\<not> 0 < x`
+ show ?thesis using lb[OF `0 < -x`] ub[OF `0 < -x`]
+ by (auto simp add: real_sqrt_minus lb_sqrt.simps ub_sqrt.simps)
+ qed qed
qed
-lemma ub_sqrt: assumes "Some y = ub_sqrt prec x"
- shows "sqrt (real x) \<le> real y" and "0 \<le> real x"
-proof -
- show "0 \<le> real x"
- proof (rule ccontr)
- assume "\<not> 0 \<le> real x"
- hence "ub_sqrt prec x = None" unfolding ub_sqrt_def less_float_def by auto
- thus False using assms by auto
- qed
- from ub_sqrt_lower_bound[OF this, of prec]
- show "sqrt (real x) \<le> real y" unfolding assms[symmetric] by auto
-qed
+lemma bnds_sqrt: "\<forall> x lx ux. (l, u) = (lb_sqrt prec lx, ub_sqrt prec ux) \<and> x \<in> {real lx .. real ux} \<longrightarrow> real l \<le> sqrt x \<and> sqrt x \<le> real u"
+proof ((rule allI) +, rule impI, erule conjE, rule conjI)
+ fix x lx ux
+ assume "(l, u) = (lb_sqrt prec lx, ub_sqrt prec ux)"
+ and x: "x \<in> {real lx .. real ux}"
+ hence l: "l = lb_sqrt prec lx " and u: "u = ub_sqrt prec ux" by auto
-lemma bnds_sqrt: "\<forall> x lx ux. (Some l, Some u) = (lb_sqrt prec lx, ub_sqrt prec ux) \<and> x \<in> {real lx .. real ux} \<longrightarrow> real l \<le> sqrt x \<and> sqrt x \<le> real u"
-proof (rule allI, rule allI, rule allI, rule impI)
- fix x lx ux
- assume "(Some l, Some u) = (lb_sqrt prec lx, ub_sqrt prec ux) \<and> x \<in> {real lx .. real ux}"
- hence l: "Some l = lb_sqrt prec lx " and u: "Some u = ub_sqrt prec ux" and x: "x \<in> {real lx .. real ux}" by auto
-
- have "real lx \<le> x" and "x \<le> real ux" using x by auto
+ have "sqrt (real lx) \<le> sqrt x" using x by auto
+ from order_trans[OF _ this]
+ show "real l \<le> sqrt x" unfolding l using bnds_sqrt'[of lx prec] by auto
- from lb_sqrt(1)[OF l] real_sqrt_le_mono[OF `real lx \<le> x`]
- have "real l \<le> sqrt x" by (rule order_trans)
- moreover
- from real_sqrt_le_mono[OF `x \<le> real ux`] ub_sqrt(1)[OF u]
- have "sqrt x \<le> real u" by (rule order_trans)
- ultimately show "real l \<le> sqrt x \<and> sqrt x \<le> real u" ..
+ have "sqrt x \<le> sqrt (real ux)" using x by auto
+ from order_trans[OF this]
+ show "sqrt x \<le> real u" unfolding u using bnds_sqrt'[of ux prec] by auto
qed
section "Arcus tangens and \<pi>"
@@ -545,23 +541,23 @@
subsection "Compute arcus tangens in the entire domain"
-function lb_arctan :: "nat \<Rightarrow> float \<Rightarrow> float" and ub_arctan :: "nat \<Rightarrow> float \<Rightarrow> float" where
+function lb_arctan :: "nat \<Rightarrow> float \<Rightarrow> float" and ub_arctan :: "nat \<Rightarrow> float \<Rightarrow> float" where
"lb_arctan prec x = (let ub_horner = \<lambda> x. x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x) ;
lb_horner = \<lambda> x. x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)
in (if x < 0 then - ub_arctan prec (-x) else
if x \<le> Float 1 -1 then lb_horner x else
- if x \<le> Float 1 1 then Float 1 1 * lb_horner (float_divl prec x (1 + the (ub_sqrt prec (1 + x * x))))
- else (let inv = float_divr prec 1 x
- in if inv > 1 then 0
+ if x \<le> Float 1 1 then Float 1 1 * lb_horner (float_divl prec x (1 + ub_sqrt prec (1 + x * x)))
+ else (let inv = float_divr prec 1 x
+ in if inv > 1 then 0
else lb_pi prec * Float 1 -1 - ub_horner inv)))"
| "ub_arctan prec x = (let lb_horner = \<lambda> x. x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x) ;
ub_horner = \<lambda> x. x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x)
in (if x < 0 then - lb_arctan prec (-x) else
if x \<le> Float 1 -1 then ub_horner x else
- if x \<le> Float 1 1 then let y = float_divr prec x (1 + the (lb_sqrt prec (1 + x * x)))
- in if y > 1 then ub_pi prec * Float 1 -1
- else Float 1 1 * ub_horner y
+ if x \<le> Float 1 1 then let y = float_divr prec x (1 + lb_sqrt prec (1 + x * x))
+ in if y > 1 then ub_pi prec * Float 1 -1
+ else Float 1 1 * ub_horner y
else ub_pi prec * Float 1 -1 - lb_horner (float_divl prec 1 x)))"
by pat_completeness auto
termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto simp add: less_float_def)
@@ -584,13 +580,15 @@
next
case False hence "0 < real x" unfolding le_float_def Float_num by auto
let ?R = "1 + sqrt (1 + real x * real x)"
- let ?fR = "1 + the (ub_sqrt prec (1 + x * x))"
+ let ?fR = "1 + ub_sqrt prec (1 + x * x)"
let ?DIV = "float_divl prec x ?fR"
-
+
have sqr_ge0: "0 \<le> 1 + real x * real x" using sum_power2_ge_zero[of 1 "real x", unfolded numeral_2_eq_2] by auto
hence divisor_gt0: "0 < ?R" by (auto intro: add_pos_nonneg)
- have "sqrt (real (1 + x * x)) \<le> real (the (ub_sqrt prec (1 + x * x)))" by (rule ub_sqrt_lower_bound, auto simp add: sqr_ge0)
+ have "sqrt (real (1 + x * x)) \<le> real (ub_sqrt prec (1 + x * x))"
+ using bnds_sqrt'[of "1 + x * x"] by auto
+
hence "?R \<le> real ?fR" by auto
hence "0 < ?fR" and "0 < real ?fR" unfolding less_float_def using `0 < ?R` by auto
@@ -604,9 +602,10 @@
show ?thesis
proof (cases "x \<le> Float 1 1")
case True
-
+
have "real x \<le> sqrt (real (1 + x * x))" using real_sqrt_sum_squares_ge2[where x=1, unfolded numeral_2_eq_2] by auto
- also have "\<dots> \<le> real (the (ub_sqrt prec (1 + x * x)))" by (rule ub_sqrt_lower_bound, auto simp add: sqr_ge0)
+ also have "\<dots> \<le> real (ub_sqrt prec (1 + x * x))"
+ using bnds_sqrt'[of "1 + x * x"] by auto
finally have "real x \<le> real ?fR" by auto
moreover have "real ?DIV \<le> real x / real ?fR" by (rule float_divl)
ultimately have "real ?DIV \<le> 1" unfolding divide_le_eq_1_pos[OF `0 < real ?fR`, symmetric] by auto
@@ -638,11 +637,11 @@
have "0 \<le> real ?invx" by (rule order_trans[OF _ float_divr], auto simp add: `0 \<le> real x`)
have "1 / real x \<noteq> 0" and "0 < 1 / real x" using `0 < real x` by auto
-
+
have "arctan (1 / real x) \<le> arctan (real ?invx)" unfolding real_of_float_1[symmetric] by (rule arctan_monotone', rule float_divr)
also have "\<dots> \<le> real (?ub_horner ?invx)" using arctan_0_1_bounds[OF `0 \<le> real ?invx` `real ?invx \<le> 1`] by auto
- finally have "pi / 2 - real (?ub_horner ?invx) \<le> arctan (real x)"
- using `0 \<le> arctan (real x)` arctan_inverse[OF `1 / real x \<noteq> 0`]
+ finally have "pi / 2 - real (?ub_horner ?invx) \<le> arctan (real x)"
+ using `0 \<le> arctan (real x)` arctan_inverse[OF `1 / real x \<noteq> 0`]
unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
moreover
have "real (lb_pi prec * Float 1 -1) \<le> pi / 2" unfolding real_of_float_mult Float_num times_divide_eq_right real_mult_1 using pi_boundaries by auto
@@ -670,15 +669,16 @@
next
case False hence "0 < real x" unfolding le_float_def Float_num by auto
let ?R = "1 + sqrt (1 + real x * real x)"
- let ?fR = "1 + the (lb_sqrt prec (1 + x * x))"
+ let ?fR = "1 + lb_sqrt prec (1 + x * x)"
let ?DIV = "float_divr prec x ?fR"
-
+
have sqr_ge0: "0 \<le> 1 + real x * real x" using sum_power2_ge_zero[of 1 "real x", unfolded numeral_2_eq_2] by auto
hence "0 \<le> real (1 + x*x)" by auto
-
+
hence divisor_gt0: "0 < ?R" by (auto intro: add_pos_nonneg)
- have "real (the (lb_sqrt prec (1 + x * x))) \<le> sqrt (real (1 + x * x))" by (rule lb_sqrt_upper_bound, auto simp add: sqr_ge0)
+ have "real (lb_sqrt prec (1 + x * x)) \<le> sqrt (real (1 + x * x))"
+ using bnds_sqrt'[of "1 + x * x"] by auto
hence "real ?fR \<le> ?R" by auto
have "0 < real ?fR" unfolding real_of_float_add real_of_float_1 by (rule order_less_le_trans[OF zero_less_one], auto simp add: lb_sqrt_lower_bound[OF `0 \<le> real (1 + x*x)`])
@@ -702,7 +702,7 @@
next
case False
hence "real ?DIV \<le> 1" unfolding less_float_def by auto
-
+
have "0 \<le> real x / ?R" using `0 \<le> real x` `0 < ?R` unfolding real_0_le_divide_iff by auto
hence "0 \<le> real ?DIV" using monotone by (rule order_trans)
@@ -725,9 +725,9 @@
have "real ?invx \<le> 1" unfolding less_float_def by (rule order_trans[OF float_divl], auto simp add: `1 \<le> real x` divide_le_eq_1_pos[OF `0 < real x`])
have "0 \<le> real ?invx" unfolding real_of_float_0[symmetric] by (rule float_divl_lower_bound[unfolded le_float_def], auto simp add: `0 < x`)
-
+
have "1 / real x \<noteq> 0" and "0 < 1 / real x" using `0 < real x` by auto
-
+
have "real (?lb_horner ?invx) \<le> arctan (real ?invx)" using arctan_0_1_bounds[OF `0 \<le> real ?invx` `real ?invx \<le> 1`] by auto
also have "\<dots> \<le> arctan (1 / real x)" unfolding real_of_float_1[symmetric] by (rule arctan_monotone', rule float_divl)
finally have "arctan (real x) \<le> pi / 2 - real (?lb_horner ?invx)"
@@ -1027,14 +1027,7 @@
else if x < 1 then half (horner (x * Float 1 -1))
else half (half (horner (x * Float 1 -2))))"
-definition bnds_cos :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float * float" where
-"bnds_cos prec lx ux = (let lpi = lb_pi prec
- in if lx < -lpi \<or> ux > lpi then (Float -1 0, Float 1 0)
- else if ux \<le> 0 then (lb_cos prec (-lx), ub_cos prec (-ux))
- else if 0 \<le> lx then (lb_cos prec ux, ub_cos prec lx)
- else (min (lb_cos prec (-lx)) (lb_cos prec ux), Float 1 0))"
-
-lemma lb_cos: assumes "0 \<le> real x" and "real x \<le> pi"
+lemma lb_cos: assumes "0 \<le> real x" and "real x \<le> pi"
shows "cos (real x) \<in> {real (lb_cos prec x) .. real (ub_cos prec x)}" (is "?cos x \<in> { real (?lb x) .. real (?ub x) }")
proof -
{ fix x :: real
@@ -1058,12 +1051,11 @@
using cos_boundaries[OF `0 \<le> real x` `real x \<le> pi / 2`] .
next
case False
-
{ fix y x :: float let ?x2 = "real (x * Float 1 -1)"
assume "real y \<le> cos ?x2" and "-pi \<le> real x" and "real x \<le> pi"
hence "- (pi / 2) \<le> ?x2" and "?x2 \<le> pi / 2" using pi_ge_two unfolding real_of_float_mult Float_num by auto
hence "0 \<le> cos ?x2" by (rule cos_ge_zero)
-
+
have "real (?lb_half y) \<le> cos (real x)"
proof (cases "y < 0")
case True show ?thesis using cos_ge_minus_one unfolding if_P[OF True] by auto
@@ -1077,12 +1069,12 @@
thus ?thesis unfolding if_not_P[OF False] x_half Float_num real_of_float_mult real_of_float_sub by auto
qed
} note lb_half = this
-
+
{ fix y x :: float let ?x2 = "real (x * Float 1 -1)"
assume ub: "cos ?x2 \<le> real y" and "- pi \<le> real x" and "real x \<le> pi"
hence "- (pi / 2) \<le> ?x2" and "?x2 \<le> pi / 2" using pi_ge_two unfolding real_of_float_mult Float_num by auto
hence "0 \<le> cos ?x2" by (rule cos_ge_zero)
-
+
have "cos (real x) \<le> real (?ub_half y)"
proof -
have "0 \<le> real y" using `0 \<le> cos ?x2` ub by (rule order_trans)
@@ -1093,19 +1085,19 @@
thus ?thesis unfolding x_half real_of_float_mult Float_num real_of_float_sub by auto
qed
} note ub_half = this
-
+
let ?x2 = "x * Float 1 -1"
let ?x4 = "x * Float 1 -1 * Float 1 -1"
-
+
have "-pi \<le> real x" using pi_ge_zero[THEN le_imp_neg_le, unfolded minus_zero] `0 \<le> real x` by (rule order_trans)
-
+
show ?thesis
proof (cases "x < 1")
case True hence "real x \<le> 1" unfolding less_float_def by auto
have "0 \<le> real ?x2" and "real ?x2 \<le> pi / 2" using pi_ge_two `0 \<le> real x` unfolding real_of_float_mult Float_num using assms by auto
from cos_boundaries[OF this]
have lb: "real (?lb_horner ?x2) \<le> ?cos ?x2" and ub: "?cos ?x2 \<le> real (?ub_horner ?x2)" by auto
-
+
have "real (?lb x) \<le> ?cos x"
proof -
from lb_half[OF lb `-pi \<le> real x` `real x \<le> pi`]
@@ -1122,9 +1114,9 @@
have "0 \<le> real ?x4" and "real ?x4 \<le> pi / 2" using pi_ge_two `0 \<le> real x` `real x \<le> pi` unfolding real_of_float_mult Float_num by auto
from cos_boundaries[OF this]
have lb: "real (?lb_horner ?x4) \<le> ?cos ?x4" and ub: "?cos ?x4 \<le> real (?ub_horner ?x4)" by auto
-
+
have eq_4: "?x2 * Float 1 -1 = x * Float 1 -2" by (cases x, auto simp add: times_float.simps)
-
+
have "real (?lb x) \<le> ?cos x"
proof -
have "-pi \<le> real ?x2" and "real ?x2 \<le> pi" unfolding real_of_float_mult Float_num using pi_ge_two `0 \<le> real x` `real x \<le> pi` by auto
@@ -1142,230 +1134,229 @@
qed
qed
-lemma lb_cos_minus: assumes "-pi \<le> real x" and "real x \<le> 0"
+lemma lb_cos_minus: assumes "-pi \<le> real x" and "real x \<le> 0"
shows "cos (real (-x)) \<in> {real (lb_cos prec (-x)) .. real (ub_cos prec (-x))}"
proof -
have "0 \<le> real (-x)" and "real (-x) \<le> pi" using `-pi \<le> real x` `real x \<le> 0` by auto
from lb_cos[OF this] show ?thesis .
qed
-lemma bnds_cos: "\<forall> x lx ux. (l, u) = bnds_cos prec lx ux \<and> x \<in> {real lx .. real ux} \<longrightarrow> real l \<le> cos x \<and> cos x \<le> real u"
-proof (rule allI, rule allI, rule allI, rule impI)
- fix x lx ux
- assume "(l, u) = bnds_cos prec lx ux \<and> x \<in> {real lx .. real ux}"
- hence bnds: "(l, u) = bnds_cos prec lx ux" and x: "x \<in> {real lx .. real ux}" by auto
-
- let ?lpi = "lb_pi prec"
- have [intro!]: "real lx \<le> real ux" using x by auto
- hence "lx \<le> ux" unfolding le_float_def .
+definition bnds_cos :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float * float" where
+"bnds_cos prec lx ux = (let
+ lpi = round_down prec (lb_pi prec) ;
+ upi = round_up prec (ub_pi prec) ;
+ k = floor_fl (float_divr prec (lx + lpi) (2 * lpi)) ;
+ lx = lx - k * 2 * (if k < 0 then lpi else upi) ;
+ ux = ux - k * 2 * (if k < 0 then upi else lpi)
+ in if - lpi \<le> lx \<and> ux \<le> 0 then (lb_cos prec (-lx), ub_cos prec (-ux))
+ else if 0 \<le> lx \<and> ux \<le> lpi then (lb_cos prec ux, ub_cos prec lx)
+ else if - lpi \<le> lx \<and> ux \<le> lpi then (min (lb_cos prec (-lx)) (lb_cos prec ux), Float 1 0)
+ else if 0 \<le> lx \<and> ux \<le> 2 * lpi then (Float -1 0, max (ub_cos prec lx) (ub_cos prec (- (ux - 2 * lpi))))
+ else (Float -1 0, Float 1 0))"
- show "real l \<le> cos x \<and> cos x \<le> real u"
- proof (cases "lx < -?lpi \<or> ux > ?lpi")
- case True
- show ?thesis using bnds unfolding bnds_cos_def if_P[OF True] Let_def using cos_le_one cos_ge_minus_one by auto
- next
- case False note not_out = this
- hence lpi_lx: "- real ?lpi \<le> real lx" and lpi_ux: "real ux \<le> real ?lpi" unfolding le_float_def less_float_def by auto
-
- from pi_boundaries[unfolded atLeastAtMost_iff, THEN conjunct1, THEN le_imp_neg_le] lpi_lx
- have "- pi \<le> real lx" by (rule order_trans)
- hence "- pi \<le> x" and "- pi \<le> real ux" and "x \<le> real ux" using x by auto
-
- from lpi_ux pi_boundaries[unfolded atLeastAtMost_iff, THEN conjunct1]
- have "real ux \<le> pi" by (rule order_trans)
- hence "x \<le> pi" and "real lx \<le> pi" and "real lx \<le> x" using x by auto
-
- note lb_cos_minus_bottom = lb_cos_minus[unfolded atLeastAtMost_iff, THEN conjunct1]
- note lb_cos_minus_top = lb_cos_minus[unfolded atLeastAtMost_iff, THEN conjunct2]
- note lb_cos_bottom = lb_cos[unfolded atLeastAtMost_iff, THEN conjunct1]
- note lb_cos_top = lb_cos[unfolded atLeastAtMost_iff, THEN conjunct2]
+lemma floor_int:
+ obtains k :: int where "real k = real (floor_fl f)"
+proof -
+ assume *: "\<And> k :: int. real k = real (floor_fl f) \<Longrightarrow> thesis"
+ obtain m e where fl: "Float m e = floor_fl f" by (cases "floor_fl f", auto)
+ from floor_pos_exp[OF this]
+ have "real (m* 2^(nat e)) = real (floor_fl f)"
+ by (auto simp add: fl[symmetric] real_of_float_def pow2_def)
+ from *[OF this] show thesis by blast
+qed
- show ?thesis
- proof (cases "ux \<le> 0")
- case True hence "real ux \<le> 0" unfolding le_float_def by auto
- hence "x \<le> 0" and "real lx \<le> 0" using x by auto
-
- { have "real (lb_cos prec (-lx)) \<le> cos (real (-lx))" using lb_cos_minus_bottom[OF `-pi \<le> real lx` `real lx \<le> 0`] .
- also have "\<dots> \<le> cos x" unfolding real_of_float_minus cos_minus using cos_monotone_minus_pi_0'[OF `- pi \<le> real lx` `real lx \<le> x` `x \<le> 0`] .
- finally have "real (lb_cos prec (-lx)) \<le> cos x" . }
- moreover
- { have "cos x \<le> cos (real (-ux))" unfolding real_of_float_minus cos_minus using cos_monotone_minus_pi_0'[OF `- pi \<le> x` `x \<le> real ux` `real ux \<le> 0`] .
- also have "\<dots> \<le> real (ub_cos prec (-ux))" using lb_cos_minus_top[OF `-pi \<le> real ux` `real ux \<le> 0`] .
- finally have "cos x \<le> real (ub_cos prec (-ux))" . }
- ultimately show ?thesis using bnds unfolding bnds_cos_def Let_def if_not_P[OF not_out] if_P[OF True] by auto
- next
- case False note not_ux = this
-
- show ?thesis
- proof (cases "0 \<le> lx")
- case True hence "0 \<le> real lx" unfolding le_float_def by auto
- hence "0 \<le> x" and "0 \<le> real ux" using x by auto
-
- { have "real (lb_cos prec ux) \<le> cos (real ux)" using lb_cos_bottom[OF `0 \<le> real ux` `real ux \<le> pi`] .
- also have "\<dots> \<le> cos x" using cos_monotone_0_pi'[OF `0 \<le> x` `x \<le> real ux` `real ux \<le> pi`] .
- finally have "real (lb_cos prec ux) \<le> cos x" . }
- moreover
- { have "cos x \<le> cos (real lx)" using cos_monotone_0_pi'[OF `0 \<le> real lx` `real lx \<le> x` `x \<le> pi`] .
- also have "\<dots> \<le> real (ub_cos prec lx)" using lb_cos_top[OF `0 \<le> real lx` `real lx \<le> pi`] .
- finally have "cos x \<le> real (ub_cos prec lx)" . }
- ultimately show ?thesis using bnds unfolding bnds_cos_def Let_def if_not_P[OF not_out] if_not_P[OF not_ux] if_P[OF True] by auto
- next
- case False with not_ux
- have "real lx \<le> 0" and "0 \<le> real ux" unfolding le_float_def by auto
+lemma float_remove_real_numeral[simp]: "real (number_of k :: float) = number_of k"
+proof -
+ have "real (number_of k :: float) = real k"
+ unfolding number_of_float_def real_of_float_def pow2_def by auto
+ also have "\<dots> = real (number_of k :: int)"
+ by (simp add: number_of_is_id)
+ finally show ?thesis by auto
+qed
- have "real (min (lb_cos prec (-lx)) (lb_cos prec ux)) \<le> cos x"
- proof (cases "x \<le> 0")
- case True
- have "real (lb_cos prec (-lx)) \<le> cos (real (-lx))" using lb_cos_minus_bottom[OF `-pi \<le> real lx` `real lx \<le> 0`] .
- also have "\<dots> \<le> cos x" unfolding real_of_float_minus cos_minus using cos_monotone_minus_pi_0'[OF `- pi \<le> real lx` `real lx \<le> x` `x \<le> 0`] .
- finally show ?thesis unfolding real_of_float_min by auto
- next
- case False hence "0 \<le> x" by auto
- have "real (lb_cos prec ux) \<le> cos (real ux)" using lb_cos_bottom[OF `0 \<le> real ux` `real ux \<le> pi`] .
- also have "\<dots> \<le> cos x" using cos_monotone_0_pi'[OF `0 \<le> x` `x \<le> real ux` `real ux \<le> pi`] .
- finally show ?thesis unfolding real_of_float_min by auto
- qed
- moreover have "cos x \<le> real (Float 1 0)" by auto
- ultimately show ?thesis using bnds unfolding bnds_cos_def Let_def if_not_P[OF not_out] if_not_P[OF not_ux] if_not_P[OF False] by auto
- qed
- qed
- qed
+lemma cos_periodic_nat[simp]: fixes n :: nat shows "cos (x + real n * 2 * pi) = cos x"
+proof (induct n arbitrary: x)
+ case (Suc n)
+ have split_pi_off: "x + real (Suc n) * 2 * pi = (x + real n * 2 * pi) + 2 * pi"
+ unfolding Suc_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
+ show ?case unfolding split_pi_off using Suc by auto
+qed auto
+
+lemma cos_periodic_int[simp]: fixes i :: int shows "cos (x + real i * 2 * pi) = cos x"
+proof (cases "0 \<le> i")
+ case True hence i_nat: "real i = real (nat i)" by auto
+ show ?thesis unfolding i_nat by auto
+next
+ case False hence i_nat: "real i = - real (nat (-i))" by auto
+ have "cos x = cos (x + real i * 2 * pi - real i * 2 * pi)" by auto
+ also have "\<dots> = cos (x + real i * 2 * pi)"
+ unfolding i_nat mult_minus_left diff_minus_eq_add by (rule cos_periodic_nat)
+ finally show ?thesis by auto
qed
-subsection "Compute the sinus in the entire domain"
+lemma bnds_cos: "\<forall> x lx ux. (l, u) = bnds_cos prec lx ux \<and> x \<in> {real lx .. real ux} \<longrightarrow> real l \<le> cos x \<and> cos x \<le> real u"
+proof ((rule allI | rule impI | erule conjE) +)
+ fix x lx ux
+ assume bnds: "(l, u) = bnds_cos prec lx ux" and x: "x \<in> {real lx .. real ux}"
+
+ let ?lpi = "round_down prec (lb_pi prec)"
+ let ?upi = "round_up prec (ub_pi prec)"
+ let ?k = "floor_fl (float_divr prec (lx + ?lpi) (2 * ?lpi))"
+ let ?lx = "lx - ?k * 2 * (if ?k < 0 then ?lpi else ?upi)"
+ let ?ux = "ux - ?k * 2 * (if ?k < 0 then ?upi else ?lpi)"
+
+ obtain k :: int where k: "real k = real ?k" using floor_int .
+
+ have upi: "pi \<le> real ?upi" and lpi: "real ?lpi \<le> pi"
+ using round_up[of "ub_pi prec" prec] pi_boundaries[of prec]
+ round_down[of prec "lb_pi prec"] by auto
+ hence "real ?lx \<le> x - real k * 2 * pi \<and> x - real k * 2 * pi \<le> real ?ux"
+ using x by (cases "k = 0") (auto intro!: add_mono
+ simp add: real_diff_def k[symmetric] less_float_def)
+ note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
+ hence lx_less_ux: "real ?lx \<le> real ?ux" by (rule order_trans)
+
+ { assume "- ?lpi \<le> ?lx" and x_le_0: "x - real k * 2 * pi \<le> 0"
+ with lpi[THEN le_imp_neg_le] lx
+ have pi_lx: "- pi \<le> real ?lx" and lx_0: "real ?lx \<le> 0"
+ by (simp_all add: le_float_def)
-function lb_sin :: "nat \<Rightarrow> float \<Rightarrow> float" and ub_sin :: "nat \<Rightarrow> float \<Rightarrow> float" where
-"lb_sin prec x = (let sqr_diff = \<lambda> x. if x > 1 then 0 else 1 - x * x
- in if x < 0 then - ub_sin prec (- x)
-else if x \<le> Float 1 -1 then x * lb_sin_cos_aux prec (get_even (prec div 4 + 1)) 2 1 (x * x)
- else the (lb_sqrt prec (sqr_diff (ub_cos prec x))))" |
+ have "real (lb_cos prec (- ?lx)) \<le> cos (real (- ?lx))"
+ using lb_cos_minus[OF pi_lx lx_0] by simp
+ also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
+ using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
+ by (simp only: real_of_float_minus real_of_int_minus
+ cos_minus real_diff_def mult_minus_left)
+ finally have "real (lb_cos prec (- ?lx)) \<le> cos x"
+ unfolding cos_periodic_int . }
+ note negative_lx = this
+
+ { assume "0 \<le> ?lx" and pi_x: "x - real k * 2 * pi \<le> pi"
+ with lx
+ have pi_lx: "real ?lx \<le> pi" and lx_0: "0 \<le> real ?lx"
+ by (auto simp add: le_float_def)
-"ub_sin prec x = (let sqr_diff = \<lambda> x. if x < 0 then 1 else 1 - x * x
- in if x < 0 then - lb_sin prec (- x)
-else if x \<le> Float 1 -1 then x * ub_sin_cos_aux prec (get_odd (prec div 4 + 1)) 2 1 (x * x)
- else the (ub_sqrt prec (sqr_diff (lb_cos prec x))))"
-by pat_completeness auto
-termination by (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 0 then 1 else 0))", auto simp add: less_float_def)
+ have "cos (x + real (-k) * 2 * pi) \<le> cos (real ?lx)"
+ using cos_monotone_0_pi'[OF lx_0 lx pi_x]
+ by (simp only: real_of_float_minus real_of_int_minus
+ cos_minus real_diff_def mult_minus_left)
+ also have "\<dots> \<le> real (ub_cos prec ?lx)"
+ using lb_cos[OF lx_0 pi_lx] by simp
+ finally have "cos x \<le> real (ub_cos prec ?lx)"
+ unfolding cos_periodic_int . }
+ note positive_lx = this
+
+ { assume pi_x: "- pi \<le> x - real k * 2 * pi" and "?ux \<le> 0"
+ with ux
+ have pi_ux: "- pi \<le> real ?ux" and ux_0: "real ?ux \<le> 0"
+ by (simp_all add: le_float_def)
-definition bnds_sin :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float * float" where
-"bnds_sin prec lx ux = (let
- lpi = lb_pi prec ;
- half_pi = lpi * Float 1 -1
- in if lx \<le> - half_pi \<or> half_pi \<le> ux then (Float -1 0, Float 1 0)
- else (lb_sin prec lx, ub_sin prec ux))"
+ have "cos (x + real (-k) * 2 * pi) \<le> cos (real (- ?ux))"
+ using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
+ by (simp only: real_of_float_minus real_of_int_minus
+ cos_minus real_diff_def mult_minus_left)
+ also have "\<dots> \<le> real (ub_cos prec (- ?ux))"
+ using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
+ finally have "cos x \<le> real (ub_cos prec (- ?ux))"
+ unfolding cos_periodic_int . }
+ note negative_ux = this
+
+ { assume "?ux \<le> ?lpi" and x_ge_0: "0 \<le> x - real k * 2 * pi"
+ with lpi ux
+ have pi_ux: "real ?ux \<le> pi" and ux_0: "0 \<le> real ?ux"
+ by (simp_all add: le_float_def)
+
+ have "real (lb_cos prec ?ux) \<le> cos (real ?ux)"
+ using lb_cos[OF ux_0 pi_ux] by simp
+ also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
+ using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
+ by (simp only: real_of_float_minus real_of_int_minus
+ cos_minus real_diff_def mult_minus_left)
+ finally have "real (lb_cos prec ?ux) \<le> cos x"
+ unfolding cos_periodic_int . }
+ note positive_ux = this
+
+ show "real l \<le> cos x \<and> cos x \<le> real u"
+ proof (cases "- ?lpi \<le> ?lx \<and> ?ux \<le> 0")
+ case True with bnds
+ have l: "l = lb_cos prec (-?lx)"
+ and u: "u = ub_cos prec (-?ux)"
+ by (auto simp add: bnds_cos_def Let_def)
-lemma lb_sin: assumes "- (pi / 2) \<le> real x" and "real x \<le> pi / 2"
- shows "sin (real x) \<in> { real (lb_sin prec x) .. real (ub_sin prec x) }" (is "?sin x \<in> { ?lb x .. ?ub x}")
-proof -
- { fix x :: float assume "0 \<le> real x" and "real x \<le> pi / 2"
- hence "\<not> (x < 0)" and "- (pi / 2) \<le> real x" unfolding less_float_def using pi_ge_two by auto
+ from True lpi[THEN le_imp_neg_le] lx ux
+ have "- pi \<le> x - real k * 2 * pi"
+ and "x - real k * 2 * pi \<le> 0"
+ by (auto simp add: le_float_def)
+ with True negative_ux negative_lx
+ show ?thesis unfolding l u by simp
+ next case False note 1 = this show ?thesis
+ proof (cases "0 \<le> ?lx \<and> ?ux \<le> ?lpi")
+ case True with bnds 1
+ have l: "l = lb_cos prec ?ux"
+ and u: "u = ub_cos prec ?lx"
+ by (auto simp add: bnds_cos_def Let_def)
- have "real x \<le> pi" using `real x \<le> pi / 2` using pi_ge_two by auto
+ from True lpi lx ux
+ have "0 \<le> x - real k * 2 * pi"
+ and "x - real k * 2 * pi \<le> pi"
+ by (auto simp add: le_float_def)
+ with True positive_ux positive_lx
+ show ?thesis unfolding l u by simp
+ next case False note 2 = this show ?thesis
+ proof (cases "- ?lpi \<le> ?lx \<and> ?ux \<le> ?lpi")
+ case True note Cond = this with bnds 1 2
+ have l: "l = min (lb_cos prec (-?lx)) (lb_cos prec ?ux)"
+ and u: "u = Float 1 0"
+ by (auto simp add: bnds_cos_def Let_def)
- have "?sin x \<in> { ?lb x .. ?ub x}"
- proof (cases "x \<le> Float 1 -1")
- case True from sin_boundaries[OF `0 \<le> real x` `real x \<le> pi / 2`]
- show ?thesis unfolding lb_sin.simps[of prec x] ub_sin.simps[of prec x] if_not_P[OF `\<not> (x < 0)`] if_P[OF True] Let_def .
+ show ?thesis unfolding u l using negative_lx positive_ux Cond
+ by (cases "x - real k * 2 * pi < 0", simp_all add: real_of_float_min)
+ next case False note 3 = this show ?thesis
+ proof (cases "0 \<le> ?lx \<and> ?ux \<le> 2 * ?lpi")
+ case True note Cond = this with bnds 1 2 3
+ have l: "l = Float -1 0"
+ and u: "u = max (ub_cos prec ?lx) (ub_cos prec (- (?ux - 2 * ?lpi)))"
+ by (auto simp add: bnds_cos_def Let_def)
+
+ have "cos x \<le> real u"
+ proof (cases "x - real k * 2 * pi < pi")
+ case True hence "x - real k * 2 * pi \<le> pi" by simp
+ from positive_lx[OF Cond[THEN conjunct1] this]
+ show ?thesis unfolding u by (simp add: real_of_float_max)
next
- case False
- have "0 \<le> cos (real x)" using cos_ge_zero[OF _ `real x \<le> pi /2`] `0 \<le> real x` pi_ge_two by auto
- have "0 \<le> sin (real x)" using `0 \<le> real x` and `real x \<le> pi / 2` using sin_ge_zero by auto
-
- have "?sin x \<le> ?ub x"
- proof (cases "lb_cos prec x < 0")
- case True
- have "?sin x \<le> 1" using sin_le_one .
- also have "\<dots> \<le> real (the (ub_sqrt prec 1))" using ub_sqrt_lower_bound[where prec=prec and x=1] unfolding real_of_float_1 by auto
- finally show ?thesis unfolding ub_sin.simps if_not_P[OF `\<not> (x < 0)`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF True] Let_def .
- next
- case False hence "0 \<le> real (lb_cos prec x)" unfolding less_float_def by auto
-
- have "sin (real x) = sqrt (1 - cos (real x) ^ 2)" unfolding sin_squared_eq[symmetric] real_sqrt_abs using `0 \<le> sin (real x)` by auto
- also have "\<dots> \<le> sqrt (real (1 - lb_cos prec x * lb_cos prec x))"
- proof (rule real_sqrt_le_mono)
- have "real (lb_cos prec x * lb_cos prec x) \<le> cos (real x) ^ 2" unfolding numeral_2_eq_2 power_Suc2 power_0 real_of_float_mult
- using `0 \<le> real (lb_cos prec x)` lb_cos[OF `0 \<le> real x` `real x \<le> pi`] `0 \<le> cos (real x)` by(auto intro!: mult_mono)
- thus "1 - cos (real x) ^ 2 \<le> real (1 - lb_cos prec x * lb_cos prec x)" unfolding real_of_float_sub real_of_float_1 by auto
- qed
- also have "\<dots> \<le> real (the (ub_sqrt prec (1 - lb_cos prec x * lb_cos prec x)))"
- proof (rule ub_sqrt_lower_bound)
- have "real (lb_cos prec x) \<le> cos (real x)" using lb_cos[OF `0 \<le> real x` `real x \<le> pi`] by auto
- from mult_mono[OF order_trans[OF this cos_le_one] order_trans[OF this cos_le_one]]
- have "real (lb_cos prec x) * real (lb_cos prec x) \<le> 1" using `0 \<le> real (lb_cos prec x)` by auto
- thus "0 \<le> real (1 - lb_cos prec x * lb_cos prec x)" by auto
- qed
- finally show ?thesis unfolding ub_sin.simps if_not_P[OF `\<not> (x < 0)`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF False] Let_def .
- qed
- moreover
- have "?lb x \<le> ?sin x"
- proof (cases "1 < ub_cos prec x")
- case True
- show ?thesis unfolding lb_sin.simps if_not_P[OF `\<not> (x < 0)`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF True] Let_def
- by (rule order_trans[OF _ sin_ge_zero[OF `0 \<le> real x` `real x \<le> pi`]])
- (auto simp add: lb_sqrt_upper_bound[where prec=prec and x=0, unfolded real_of_float_0 real_sqrt_zero])
- next
- case False hence "real (ub_cos prec x) \<le> 1" unfolding less_float_def by auto
- have "0 \<le> real (ub_cos prec x)" using order_trans[OF `0 \<le> cos (real x)`] lb_cos `0 \<le> real x` `real x \<le> pi` by auto
-
- have "real (the (lb_sqrt prec (1 - ub_cos prec x * ub_cos prec x))) \<le> sqrt (real (1 - ub_cos prec x * ub_cos prec x))"
- proof (rule lb_sqrt_upper_bound)
- from mult_mono[OF `real (ub_cos prec x) \<le> 1` `real (ub_cos prec x) \<le> 1`] `0 \<le> real (ub_cos prec x)`
- have "real (ub_cos prec x) * real (ub_cos prec x) \<le> 1" by auto
- thus "0 \<le> real (1 - ub_cos prec x * ub_cos prec x)" by auto
- qed
- also have "\<dots> \<le> sqrt (1 - cos (real x) ^ 2)"
- proof (rule real_sqrt_le_mono)
- have "cos (real x) ^ 2 \<le> real (ub_cos prec x * ub_cos prec x)" unfolding numeral_2_eq_2 power_Suc2 power_0 real_of_float_mult
- using `0 \<le> real (ub_cos prec x)` lb_cos[OF `0 \<le> real x` `real x \<le> pi`] `0 \<le> cos (real x)` by(auto intro!: mult_mono)
- thus "real (1 - ub_cos prec x * ub_cos prec x) \<le> 1 - cos (real x) ^ 2" unfolding real_of_float_sub real_of_float_1 by auto
- qed
- also have "\<dots> = sin (real x)" unfolding sin_squared_eq[symmetric] real_sqrt_abs using `0 \<le> sin (real x)` by auto
- finally show ?thesis unfolding lb_sin.simps if_not_P[OF `\<not> (x < 0)`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF False] Let_def .
- qed
- ultimately show ?thesis by auto
+ case False hence "pi \<le> x - real k * 2 * pi" by simp
+ hence pi_x: "- pi \<le> x - real k * 2 * pi - 2 * pi" by simp
+
+ have "real ?ux \<le> 2 * pi" using Cond lpi by (auto simp add: le_float_def)
+ hence "x - real k * 2 * pi - 2 * pi \<le> 0" using ux by simp
+
+ have ux_0: "real (?ux - 2 * ?lpi) \<le> 0"
+ using Cond by (auto simp add: le_float_def)
+
+ from 2 and Cond have "\<not> ?ux \<le> ?lpi" by auto
+ hence "- ?lpi \<le> ?ux - 2 * ?lpi" by (auto simp add: le_float_def)
+ hence pi_ux: "- pi \<le> real (?ux - 2 * ?lpi)"
+ using lpi[THEN le_imp_neg_le] by (auto simp add: le_float_def)
+
+ have x_le_ux: "x - real k * 2 * pi - 2 * pi \<le> real (?ux - 2 * ?lpi)"
+ using ux lpi by auto
+
+ have "cos x = cos (x + real (-k) * 2 * pi + real (-1 :: int) * 2 * pi)"
+ unfolding cos_periodic_int ..
+ also have "\<dots> \<le> cos (real (?ux - 2 * ?lpi))"
+ using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
+ by (simp only: real_of_float_minus real_of_int_minus real_of_one
+ number_of_Min real_diff_def mult_minus_left real_mult_1)
+ also have "\<dots> = cos (real (- (?ux - 2 * ?lpi)))"
+ unfolding real_of_float_minus cos_minus ..
+ also have "\<dots> \<le> real (ub_cos prec (- (?ux - 2 * ?lpi)))"
+ using lb_cos_minus[OF pi_ux ux_0] by simp
+ finally show ?thesis unfolding u by (simp add: real_of_float_max)
qed
- } note for_pos = this
-
- show ?thesis
- proof (cases "x < 0")
- case True
- hence "0 \<le> real (-x)" and "real (- x) \<le> pi / 2" using `-(pi/2) \<le> real x` unfolding less_float_def by auto
- from for_pos[OF this]
- show ?thesis unfolding real_of_float_minus sin_minus lb_sin.simps[of prec x] ub_sin.simps[of prec x] if_P[OF True] Let_def atLeastAtMost_iff by auto
+ thus ?thesis unfolding l by auto
next
- case False hence "0 \<le> real x" unfolding less_float_def by auto
- from for_pos[OF this `real x \<le> pi /2`]
- show ?thesis .
- qed
-qed
-
-lemma bnds_sin: "\<forall> x lx ux. (l, u) = bnds_sin prec lx ux \<and> x \<in> {real lx .. real ux} \<longrightarrow> real l \<le> sin x \<and> sin x \<le> real u"
-proof (rule allI, rule allI, rule allI, rule impI)
- fix x lx ux
- assume "(l, u) = bnds_sin prec lx ux \<and> x \<in> {real lx .. real ux}"
- hence bnds: "(l, u) = bnds_sin prec lx ux" and x: "x \<in> {real lx .. real ux}" by auto
- show "real l \<le> sin x \<and> sin x \<le> real u"
- proof (cases "lx \<le> - (lb_pi prec * Float 1 -1) \<or> lb_pi prec * Float 1 -1 \<le> ux")
- case True show ?thesis using bnds unfolding bnds_sin_def if_P[OF True] Let_def by auto
- next
- case False
- hence "- lb_pi prec * Float 1 -1 \<le> lx" and "ux \<le> lb_pi prec * Float 1 -1" unfolding le_float_def by auto
- moreover have "real (lb_pi prec * Float 1 -1) \<le> pi / 2" unfolding real_of_float_mult using pi_boundaries by auto
- ultimately have "- (pi / 2) \<le> real lx" and "real ux \<le> pi / 2" and "real lx \<le> real ux" unfolding le_float_def using x by auto
- hence "- (pi / 2) \<le> real ux" and "real lx \<le> pi / 2" by auto
-
- have "- (pi / 2) \<le> x""x \<le> pi / 2" using `real ux \<le> pi / 2` `- (pi /2) \<le> real lx` x by auto
-
- { have "real (lb_sin prec lx) \<le> sin (real lx)" using lb_sin[OF `- (pi / 2) \<le> real lx` `real lx \<le> pi / 2`] unfolding atLeastAtMost_iff by auto
- also have "\<dots> \<le> sin x" using sin_monotone_2pi' `- (pi / 2) \<le> real lx` x `x \<le> pi / 2` by auto
- finally have "real (lb_sin prec lx) \<le> sin x" . }
- moreover
- { have "sin x \<le> sin (real ux)" using sin_monotone_2pi' `- (pi / 2) \<le> x` x `real ux \<le> pi / 2` by auto
- also have "\<dots> \<le> real (ub_sin prec ux)" using lb_sin[OF `- (pi / 2) \<le> real ux` `real ux \<le> pi / 2`] unfolding atLeastAtMost_iff by auto
- finally have "sin x \<le> real (ub_sin prec ux)" . }
- ultimately
- show ?thesis using bnds unfolding bnds_sin_def if_not_P[OF False] Let_def by auto
- qed
+ case False with bnds 1 2 3 show ?thesis by (auto simp add: bnds_cos_def Let_def)
+ qed qed qed qed
qed
section "Exponential function"
@@ -1384,7 +1375,7 @@
{ fix n
have F: "\<And> m. ((\<lambda>i. i + 1) ^^ n) m = n + m" by (induct n, auto)
have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) ^^ n) 1" unfolding F by auto } note f_eq = this
-
+
note bounds = horner_bounds_nonpos[where f="fact" and lb="lb_exp_horner prec" and ub="ub_exp_horner prec" and j'=0 and s=1,
OF assms f_eq lb_exp_horner.simps ub_exp_horner.simps]
@@ -1743,18 +1734,21 @@
subsection "Compute the logarithm in the entire domain"
function ub_ln :: "nat \<Rightarrow> float \<Rightarrow> float option" and lb_ln :: "nat \<Rightarrow> float \<Rightarrow> float option" where
-"ub_ln prec x = (if x \<le> 0 then None
- else if x < 1 then Some (- the (lb_ln prec (float_divl (max prec 1) 1 x)))
- else let horner = \<lambda>x. (x - 1) * ub_ln_horner prec (get_odd prec) 1 (x - 1) in
- if x < Float 1 1 then Some (horner x)
- else let l = bitlen (mantissa x) - 1 in
- Some (ub_ln2 prec * (Float (scale x + l) 0) + horner (Float (mantissa x) (- l))))" |
-"lb_ln prec x = (if x \<le> 0 then None
- else if x < 1 then Some (- the (ub_ln prec (float_divr prec 1 x)))
- else let horner = \<lambda>x. (x - 1) * lb_ln_horner prec (get_even prec) 1 (x - 1) in
- if x < Float 1 1 then Some (horner x)
- else let l = bitlen (mantissa x) - 1 in
- Some (lb_ln2 prec * (Float (scale x + l) 0) + horner (Float (mantissa x) (- l))))"
+"ub_ln prec x = (if x \<le> 0 then None
+ else if x < 1 then Some (- the (lb_ln prec (float_divl (max prec 1) 1 x)))
+ else let horner = \<lambda>x. x * ub_ln_horner prec (get_odd prec) 1 x in
+ if x \<le> Float 3 -1 then Some (horner (x - 1))
+ else if x < Float 1 1 then Some (horner (Float 1 -1) + horner (x * rapprox_rat prec 2 3 - 1))
+ else let l = bitlen (mantissa x) - 1 in
+ Some (ub_ln2 prec * (Float (scale x + l) 0) + horner (Float (mantissa x) (- l) - 1)))" |
+"lb_ln prec x = (if x \<le> 0 then None
+ else if x < 1 then Some (- the (ub_ln prec (float_divr prec 1 x)))
+ else let horner = \<lambda>x. x * lb_ln_horner prec (get_even prec) 1 x in
+ if x \<le> Float 3 -1 then Some (horner (x - 1))
+ else if x < Float 1 1 then Some (horner (Float 1 -1) +
+ horner (max (x * lapprox_rat prec 2 3 - 1) 0))
+ else let l = bitlen (mantissa x) - 1 in
+ Some (lb_ln2 prec * (Float (scale x + l) 0) + horner (Float (mantissa x) (- l) - 1)))"
by pat_completeness auto
termination proof (relation "measure (\<lambda> v. let (prec, x) = sum_case id id v in (if x < 1 then 1 else 0))", auto)
@@ -1774,19 +1768,19 @@
let ?B = "2^nat (bitlen m - 1)"
have "0 < real m" and "\<And>X. (0 :: real) < 2^X" and "0 < (2 :: real)" and "m \<noteq> 0" using assms by auto
hence "0 \<le> bitlen m - 1" using bitlen_ge1[OF `m \<noteq> 0`] by auto
- show ?thesis
+ show ?thesis
proof (cases "0 \<le> e")
case True
show ?thesis unfolding normalized_float[OF `m \<noteq> 0`]
- unfolding ln_div[OF `0 < real m` `0 < ?B`] real_of_int_add ln_realpow[OF `0 < 2`]
- unfolding real_of_float_ge0_exp[OF True] ln_mult[OF `0 < real m` `0 < 2^nat e`]
+ unfolding ln_div[OF `0 < real m` `0 < ?B`] real_of_int_add ln_realpow[OF `0 < 2`]
+ unfolding real_of_float_ge0_exp[OF True] ln_mult[OF `0 < real m` `0 < 2^nat e`]
ln_realpow[OF `0 < 2`] algebra_simps using `0 \<le> bitlen m - 1` True by auto
next
case False hence "0 < -e" by auto
hence pow_gt0: "(0::real) < 2^nat (-e)" by auto
hence inv_gt0: "(0::real) < inverse (2^nat (-e))" by auto
show ?thesis unfolding normalized_float[OF `m \<noteq> 0`]
- unfolding ln_div[OF `0 < real m` `0 < ?B`] real_of_int_add ln_realpow[OF `0 < 2`]
+ unfolding ln_div[OF `0 < real m` `0 < ?B`] real_of_int_add ln_realpow[OF `0 < 2`]
unfolding real_of_float_nge0_exp[OF False] ln_mult[OF `0 < real m` inv_gt0] ln_inverse[OF pow_gt0]
ln_realpow[OF `0 < 2`] algebra_simps using `0 \<le> bitlen m - 1` False by auto
qed
@@ -1796,14 +1790,91 @@
shows "real (the (lb_ln prec x)) \<le> ln (real x) \<and> ln (real x) \<le> real (the (ub_ln prec x))"
(is "?lb \<le> ?ln \<and> ?ln \<le> ?ub")
proof (cases "x < Float 1 1")
- case True hence "real (x - 1) < 1" unfolding less_float_def Float_num by auto
+ case True
+ hence "real (x - 1) < 1" and "real x < 2" unfolding less_float_def Float_num by auto
have "\<not> x \<le> 0" and "\<not> x < 1" using `1 \<le> x` unfolding less_float_def le_float_def by auto
hence "0 \<le> real (x - 1)" using `1 \<le> x` unfolding less_float_def Float_num by auto
- show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps Let_def
- using ln_float_bounds[OF `0 \<le> real (x - 1)` `real (x - 1) < 1`] `\<not> x \<le> 0` `\<not> x < 1` True by auto
+
+ have [simp]: "real (Float 3 -1) = 3 / 2" by (simp add: real_of_float_def pow2_def)
+
+ show ?thesis
+ proof (cases "x \<le> Float 3 -1")
+ case True
+ show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps Let_def
+ using ln_float_bounds[OF `0 \<le> real (x - 1)` `real (x - 1) < 1`, of prec] `\<not> x \<le> 0` `\<not> x < 1` True
+ by auto
+ next
+ case False hence *: "3 / 2 < real x" by (auto simp add: le_float_def)
+
+ with ln_add[of "3 / 2" "real x - 3 / 2"]
+ have add: "ln (real x) = ln (3 / 2) + ln (real x * 2 / 3)"
+ by (auto simp add: algebra_simps diff_divide_distrib)
+
+ let "?ub_horner x" = "x * ub_ln_horner prec (get_odd prec) 1 x"
+ let "?lb_horner x" = "x * lb_ln_horner prec (get_even prec) 1 x"
+
+ { have up: "real (rapprox_rat prec 2 3) \<le> 1"
+ by (rule rapprox_rat_le1) simp_all
+ have low: "2 / 3 \<le> real (rapprox_rat prec 2 3)"
+ by (rule order_trans[OF _ rapprox_rat]) simp
+ from mult_less_le_imp_less[OF * low] *
+ have pos: "0 < real (x * rapprox_rat prec 2 3 - 1)" by auto
+
+ have "ln (real x * 2/3)
+ \<le> ln (real (x * rapprox_rat prec 2 3 - 1) + 1)"
+ proof (rule ln_le_cancel_iff[symmetric, THEN iffD1])
+ show "real x * 2 / 3 \<le> real (x * rapprox_rat prec 2 3 - 1) + 1"
+ using * low by auto
+ show "0 < real x * 2 / 3" using * by simp
+ show "0 < real (x * rapprox_rat prec 2 3 - 1) + 1" using pos by auto
+ qed
+ also have "\<dots> \<le> real (?ub_horner (x * rapprox_rat prec 2 3 - 1))"
+ proof (rule ln_float_bounds(2))
+ from mult_less_le_imp_less[OF `real x < 2` up] low *
+ show "real (x * rapprox_rat prec 2 3 - 1) < 1" by auto
+ show "0 \<le> real (x * rapprox_rat prec 2 3 - 1)" using pos by auto
+ qed
+ finally have "ln (real x)
+ \<le> real (?ub_horner (Float 1 -1))
+ + real (?ub_horner (x * rapprox_rat prec 2 3 - 1))"
+ using ln_float_bounds(2)[of "Float 1 -1" prec prec] add by auto }
+ moreover
+ { let ?max = "max (x * lapprox_rat prec 2 3 - 1) 0"
+
+ have up: "real (lapprox_rat prec 2 3) \<le> 2/3"
+ by (rule order_trans[OF lapprox_rat], simp)
+
+ have low: "0 \<le> real (lapprox_rat prec 2 3)"
+ using lapprox_rat_bottom[of 2 3 prec] by simp
+
+ have "real (?lb_horner ?max)
+ \<le> ln (real ?max + 1)"
+ proof (rule ln_float_bounds(1))
+ from mult_less_le_imp_less[OF `real x < 2` up] * low
+ show "real ?max < 1" by (cases "real (lapprox_rat prec 2 3) = 0",
+ auto simp add: real_of_float_max)
+ show "0 \<le> real ?max" by (auto simp add: real_of_float_max)
+ qed
+ also have "\<dots> \<le> ln (real x * 2/3)"
+ proof (rule ln_le_cancel_iff[symmetric, THEN iffD1])
+ show "0 < real ?max + 1" by (auto simp add: real_of_float_max)
+ show "0 < real x * 2/3" using * by auto
+ show "real ?max + 1 \<le> real x * 2/3" using * up
+ by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
+ auto simp add: real_of_float_max max_def)
+ qed
+ finally have "real (?lb_horner (Float 1 -1)) + real (?lb_horner ?max)
+ \<le> ln (real x)"
+ using ln_float_bounds(1)[of "Float 1 -1" prec prec] add by auto }
+ ultimately
+ show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps Let_def
+ using `\<not> x \<le> 0` `\<not> x < 1` True False by auto
+ qed
next
case False
- have "\<not> x \<le> 0" and "\<not> x < 1" "0 < x" using `1 \<le> x` unfolding less_float_def le_float_def by auto
+ hence "\<not> x \<le> 0" and "\<not> x < 1" "0 < x" "\<not> x \<le> Float 3 -1"
+ using `1 \<le> x` unfolding less_float_def le_float_def real_of_float_simp pow2_def
+ by auto
show ?thesis
proof (cases x)
case (Float m e)
@@ -1828,7 +1899,7 @@
have "real ((?x - 1) * lb_ln_horner prec (get_even prec) 1 (?x - 1)) \<le> ln (real ?x)" (is "?lb_horner \<le> _") by auto
ultimately have "?lb2 + ?lb_horner \<le> ln (real x)"
unfolding Float ln_shifted_float[OF `0 < m`, of e] by auto
- }
+ }
moreover
{
from bitlen_div[OF `0 < m`, unfolded normalized_float[OF `m \<noteq> 0`, symmetric]]
@@ -1838,7 +1909,7 @@
moreover
have "ln 2 * real (e + (bitlen m - 1)) \<le> real (ub_ln2 prec * ?s)" (is "_ \<le> ?ub2")
unfolding real_of_float_mult real_of_float_ge0_exp[OF order_refl] nat_0 power_0 mult_1_right
- using ub_ln2[of prec]
+ using ub_ln2[of prec]
proof (rule mult_right_mono)
have "1 \<le> Float m e" using `1 \<le> x` Float unfolding le_float_def by auto
from float_gt1_scale[OF this]
@@ -1848,8 +1919,9 @@
unfolding Float ln_shifted_float[OF `0 < m`, of e] by auto
}
ultimately show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps
- unfolding if_not_P[OF `\<not> x \<le> 0`] if_not_P[OF `\<not> x < 1`] if_not_P[OF False] Let_def
- unfolding scale.simps[of m e, unfolded Float[symmetric]] mantissa.simps[of m e, unfolded Float[symmetric]] real_of_float_add by auto
+ unfolding if_not_P[OF `\<not> x \<le> 0`] if_not_P[OF `\<not> x < 1`] if_not_P[OF False] if_not_P[OF `\<not> x \<le> Float 3 -1`] Let_def
+ unfolding scale.simps[of m e, unfolded Float[symmetric]] mantissa.simps[of m e, unfolded Float[symmetric]] real_of_float_add
+ by auto
qed
qed
@@ -1869,17 +1941,17 @@
let ?divl = "float_divl (max prec 1) 1 x"
have A': "1 \<le> ?divl" using float_divl_pos_less1_bound[OF `0 < x` `x < 1`] unfolding le_float_def less_float_def by auto
hence B: "0 < real ?divl" unfolding le_float_def by auto
-
+
have "ln (real ?divl) \<le> ln (1 / real x)" unfolding ln_le_cancel_iff[OF B A] using float_divl[of _ 1 x] by auto
hence "ln (real x) \<le> - ln (real ?divl)" unfolding nonzero_inverse_eq_divide[OF `real x \<noteq> 0`, symmetric] ln_inverse[OF `0 < real x`] by auto
- from this ub_ln_lb_ln_bounds'[OF A', THEN conjunct1, THEN le_imp_neg_le]
+ from this ub_ln_lb_ln_bounds'[OF A', THEN conjunct1, THEN le_imp_neg_le]
have "?ln \<le> real (- the (lb_ln prec ?divl))" unfolding real_of_float_minus by (rule order_trans)
} moreover
{
let ?divr = "float_divr prec 1 x"
have A': "1 \<le> ?divr" using float_divr_pos_less1_lower_bound[OF `0 < x` `x < 1`] unfolding le_float_def less_float_def by auto
hence B: "0 < real ?divr" unfolding le_float_def by auto
-
+
have "ln (1 / real x) \<le> ln (real ?divr)" unfolding ln_le_cancel_iff[OF A B] using float_divr[of 1 x] by auto
hence "- ln (real ?divr) \<le> ln (real x)" unfolding nonzero_inverse_eq_divide[OF `real x \<noteq> 0`, symmetric] ln_inverse[OF `0 < real x`] by auto
from ub_ln_lb_ln_bounds'[OF A', THEN conjunct2, THEN le_imp_neg_le] this
@@ -1924,15 +1996,14 @@
have "ln (real ux) \<le> real u" and "0 < real ux" using ub_ln u by auto
have "real l \<le> ln (real lx)" and "0 < real lx" and "0 < x" using lb_ln[OF l] x by auto
- from ln_le_cancel_iff[OF `0 < real lx` `0 < x`] `real l \<le> ln (real lx)`
+ from ln_le_cancel_iff[OF `0 < real lx` `0 < x`] `real l \<le> ln (real lx)`
have "real l \<le> ln x" using x unfolding atLeastAtMost_iff by auto
moreover
- from ln_le_cancel_iff[OF `0 < x` `0 < real ux`] `ln (real ux) \<le> real u`
+ from ln_le_cancel_iff[OF `0 < x` `0 < real ux`] `ln (real ux) \<le> real u`
have "ln x \<le> real u" using x unfolding atLeastAtMost_iff by auto
ultimately show "real l \<le> ln x \<and> ln x \<le> real u" ..
qed
-
section "Implement floatarith"
subsection "Define syntax and semantics"
@@ -1942,7 +2013,6 @@
| Minus floatarith
| Mult floatarith floatarith
| Inverse floatarith
- | Sin floatarith
| Cos floatarith
| Arctan floatarith
| Abs floatarith
@@ -1962,7 +2032,6 @@
"interpret_floatarith (Minus a) vs = - (interpret_floatarith a vs)" |
"interpret_floatarith (Mult a b) vs = (interpret_floatarith a vs) * (interpret_floatarith b vs)" |
"interpret_floatarith (Inverse a) vs = inverse (interpret_floatarith a vs)" |
-"interpret_floatarith (Sin a) vs = sin (interpret_floatarith a vs)" |
"interpret_floatarith (Cos a) vs = cos (interpret_floatarith a vs)" |
"interpret_floatarith (Arctan a) vs = arctan (interpret_floatarith a vs)" |
"interpret_floatarith (Min a b) vs = min (interpret_floatarith a vs) (interpret_floatarith b vs)" |
@@ -1978,11 +2047,6 @@
subsection "Implement approximation function"
-fun lift_bin :: "(float * float) option \<Rightarrow> (float * float) option \<Rightarrow> (float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> (float option * float option)) \<Rightarrow> (float * float) option" where
-"lift_bin (Some (l1, u1)) (Some (l2, u2)) f = (case (f l1 u1 l2 u2) of (Some l, Some u) \<Rightarrow> Some (l, u)
- | t \<Rightarrow> None)" |
-"lift_bin a b f = None"
-
fun lift_bin' :: "(float * float) option \<Rightarrow> (float * float) option \<Rightarrow> (float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> (float * float)) \<Rightarrow> (float * float) option" where
"lift_bin' (Some (l1, u1)) (Some (l2, u2)) f = Some (f l1 u1 l2 u2)" |
"lift_bin' a b f = None"
@@ -2027,14 +2091,13 @@
(\<lambda> a1 a2 b1 b2. (float_nprt a1 * float_pprt b2 + float_nprt a2 * float_nprt b2 + float_pprt a1 * float_pprt b1 + float_pprt a2 * float_nprt b1,
float_pprt a2 * float_pprt b2 + float_pprt a1 * float_nprt b2 + float_nprt a2 * float_pprt b1 + float_nprt a1 * float_nprt b1))" |
"approx prec (Inverse a) bs = lift_un (approx' prec a bs) (\<lambda> l u. if (0 < l \<or> u < 0) then (Some (float_divl prec 1 u), Some (float_divr prec 1 l)) else (None, None))" |
-"approx prec (Sin a) bs = lift_un' (approx' prec a bs) (bnds_sin prec)" |
"approx prec (Cos a) bs = lift_un' (approx' prec a bs) (bnds_cos prec)" |
"approx prec Pi bs = Some (lb_pi prec, ub_pi prec)" |
"approx prec (Min a b) bs = lift_bin' (approx' prec a bs) (approx' prec b bs) (\<lambda> l1 u1 l2 u2. (min l1 l2, min u1 u2))" |
"approx prec (Max a b) bs = lift_bin' (approx' prec a bs) (approx' prec b bs) (\<lambda> l1 u1 l2 u2. (max l1 l2, max u1 u2))" |
"approx prec (Abs a) bs = lift_un' (approx' prec a bs) (\<lambda>l u. (if l < 0 \<and> 0 < u then 0 else min \<bar>l\<bar> \<bar>u\<bar>, max \<bar>l\<bar> \<bar>u\<bar>))" |
"approx prec (Arctan a) bs = lift_un' (approx' prec a bs) (\<lambda> l u. (lb_arctan prec l, ub_arctan prec u))" |
-"approx prec (Sqrt a) bs = lift_un (approx' prec a bs) (\<lambda> l u. (lb_sqrt prec l, ub_sqrt prec u))" |
+"approx prec (Sqrt a) bs = lift_un' (approx' prec a bs) (\<lambda> l u. (lb_sqrt prec l, ub_sqrt prec u))" |
"approx prec (Exp a) bs = lift_un' (approx' prec a bs) (\<lambda> l u. (lb_exp prec l, ub_exp prec u))" |
"approx prec (Ln a) bs = lift_un (approx' prec a bs) (\<lambda> l u. (lb_ln prec l, ub_ln prec u))" |
"approx prec (Power a n) bs = lift_un' (approx' prec a bs) (float_power_bnds n)" |
@@ -2275,7 +2338,7 @@
inverse_le_iff_le_neg[OF `interpret_floatarith a xs < 0` `real l1 < 0`]
using l1 u1 by auto
qed
-
+
from l' have "l = float_divl prec 1 u1" by (cases "0 < l1 \<or> u1 < 0", auto)
hence "real l \<le> inverse (real u1)" unfolding nonzero_inverse_eq_divide[OF `real u1 \<noteq> 0`] using float_divl[of prec 1 u1] by auto
also have "\<dots> \<le> inverse (interpret_floatarith a xs)" using inv by auto
@@ -2305,11 +2368,10 @@
and l1: "real l1 \<le> interpret_floatarith a xs" and u1: "interpret_floatarith a xs \<le> real u1"
and l1: "real l2 \<le> interpret_floatarith b xs" and u1: "interpret_floatarith b xs \<le> real u2" by blast
thus ?case unfolding l' u' by (auto simp add: real_of_float_max)
-next case (Sin a) with lift_un'_bnds[OF bnds_sin] show ?case by auto
next case (Cos a) with lift_un'_bnds[OF bnds_cos] show ?case by auto
next case (Arctan a) with lift_un'_bnds[OF bnds_arctan] show ?case by auto
next case Pi with pi_boundaries show ?case by auto
-next case (Sqrt a) with lift_un_bnds[OF bnds_sqrt] show ?case by auto
+next case (Sqrt a) with lift_un'_bnds[OF bnds_sqrt] show ?case by auto
next case (Exp a) with lift_un'_bnds[OF bnds_exp] show ?case by auto
next case (Ln a) with lift_un_bnds[OF bnds_ln] show ?case by auto
next case (Power a n) with lift_un'_bnds[OF bnds_power] show ?case by auto
@@ -2391,8 +2453,17 @@
lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
unfolding real_diff_def interpret_floatarith.simps ..
-lemma interpret_floatarith_tan: "interpret_floatarith (Mult (Sin a) (Inverse (Cos a))) vs = tan (interpret_floatarith a vs)"
- unfolding tan_def interpret_floatarith.simps real_divide_def ..
+lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
+ sin (interpret_floatarith a vs)"
+ unfolding sin_cos_eq interpret_floatarith.simps
+ interpret_floatarith_divide interpret_floatarith_diff real_diff_def
+ by auto
+
+lemma interpret_floatarith_tan:
+ "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (Inverse (Cos a))) vs =
+ tan (interpret_floatarith a vs)"
+ unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def real_divide_def
+ by auto
lemma interpret_floatarith_powr: "interpret_floatarith (Exp (Mult b (Ln a))) vs = (interpret_floatarith a vs) powr (interpret_floatarith b vs)"
unfolding powr_def interpret_floatarith.simps ..
@@ -2420,13 +2491,14 @@
lemmas bounded_by_equations = bounded_by_Cons bounded_by_Nil float_power bounded_divl bounded_divr bounded_num HOL.simp_thms
lemmas interpret_inequality_equations = interpret_inequality.simps interpret_floatarith.simps interpret_floatarith_num
interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log
+ interpret_floatarith_sin
ML {*
structure Float_Arith =
struct
@{code_datatype float = Float}
-@{code_datatype floatarith = Add | Minus | Mult | Inverse | Sin | Cos | Arctan
+@{code_datatype floatarith = Add | Minus | Mult | Inverse | Cos | Arctan
| Abs | Max | Min | Pi | Sqrt | Exp | Ln | Power | Atom | Num }
@{code_datatype inequality = Less | LessEqual }
@@ -2441,10 +2513,10 @@
code_const Float (Eval "Float'_Arith.Float/ (_,/ _)")
code_type floatarith (Eval "Float'_Arith.floatarith")
-code_const Add and Minus and Mult and Inverse and Sin and Cos and Arctan and Abs and Max and Min and
+code_const Add and Minus and Mult and Inverse and Cos and Arctan and Abs and Max and Min and
Pi and Sqrt and Exp and Ln and Power and Atom and Num
(Eval "Float'_Arith.Add/ (_,/ _)" and "Float'_Arith.Minus" and "Float'_Arith.Mult/ (_,/ _)" and
- "Float'_Arith.Inverse" and "Float'_Arith.Sin" and "Float'_Arith.Cos" and
+ "Float'_Arith.Inverse" and "Float'_Arith.Cos" and
"Float'_Arith.Arctan" and "Float'_Arith.Abs" and "Float'_Arith.Max/ (_,/ _)" and
"Float'_Arith.Min/ (_,/ _)" and "Float'_Arith.Pi" and "Float'_Arith.Sqrt" and
"Float'_Arith.Exp" and "Float'_Arith.Ln" and "Float'_Arith.Power/ (_,/ _)" and
@@ -2505,9 +2577,9 @@
val goal' : term = List.nth (prems_of thm, i - 1)
- fun lift_bnd (t as (Const (@{const_name "op &"}, _) $
- (Const (@{const_name "less_eq"}, _) $
- bottom $ (Free (name, _))) $
+ fun lift_bnd (t as (Const (@{const_name "op &"}, _) $
+ (Const (@{const_name "less_eq"}, _) $
+ bottom $ (Free (name, _))) $
(Const (@{const_name "less_eq"}, _) $ _ $ top)))
= ((name, HOLogic.mk_prod (bot_float bottom, top_float top))
handle TERM (txt, ts) => raise TERM ("Invalid bound number format: " ^
@@ -2542,11 +2614,9 @@
SIMPLE_METHOD' (fn i =>
(DETERM (reify_ineq ctxt i)
THEN rule_ineq ctxt prec i
- THEN Simplifier.asm_full_simp_tac bounded_by_simpset i
+ THEN Simplifier.asm_full_simp_tac bounded_by_simpset i
THEN (TRY (filter_prems_tac (fn t => false) i))
THEN (gen_eval_tac eval_oracle ctxt) i)))
*} "real number approximation"
-lemma "sin 1 > 0" by (approximation 10)
-
end
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Mon Jun 08 09:22:47 2009 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Mon Jun 08 09:23:04 2009 +0200
@@ -32,6 +32,9 @@
lemma "\<bar> pi - 3.1415926535897932385 \<bar> < inverse 10 ^ 18"
by (approximation 80)
+lemma "\<bar> sin 100 + 0.50636564110975879 \<bar> < inverse 10 ^ 17"
+ by (approximation 80)
+
section "Use variable ranges"
lemma "0.5 \<le> x \<and> x \<le> 4.5 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
@@ -43,8 +46,8 @@
lemma "1 / 2^1 \<le> x \<and> x \<le> 9 / 2^1 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
by (approximation 10)
-lemma "0 \<le> x \<and> x \<le> 1 \<Longrightarrow> 0 \<le> sin x"
- by (approximation 10)
+lemma "3.2 \<le> x \<and> x \<le> 6.2 \<Longrightarrow> sin x \<le> 0"
+ by (approximation 9)
end
--- a/src/HOL/Library/Float.thy Mon Jun 08 09:22:47 2009 +0200
+++ b/src/HOL/Library/Float.thy Mon Jun 08 09:23:04 2009 +0200
@@ -28,7 +28,7 @@
"scale (Float a b) = b"
instantiation float :: zero begin
-definition zero_float where "0 = Float 0 0"
+definition zero_float where "0 = Float 0 0"
instance ..
end
@@ -42,6 +42,10 @@
instance ..
end
+lemma number_of_float_Float [code inline, symmetric, code post]:
+ "number_of k = Float (number_of k) 0"
+ by (simp add: number_of_float_def number_of_is_id)
+
lemma real_of_float_simp[simp]: "real (Float a b) = real a * pow2 b"
unfolding real_of_float_def using of_float.simps .
@@ -50,7 +54,7 @@
lemma real_of_float_ge0_exp: "0 \<le> e \<Longrightarrow> real (Float m e) = real m * (2^nat e)" by auto
lemma Float_num[simp]: shows
- "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
+ "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
"real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and
"real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n"
by auto
--- a/src/HOL/SetInterval.thy Mon Jun 08 09:22:47 2009 +0200
+++ b/src/HOL/SetInterval.thy Mon Jun 08 09:23:04 2009 +0200
@@ -833,6 +833,13 @@
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps)
done
+lemma setsum_ub_add_nat: assumes "(m::nat) \<le> n + 1"
+ shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"
+proof-
+ have "{m .. n+p} = {m..n} \<union> {n+1..n+p}" using `m \<le> n+1` by auto
+ thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint
+ atLeastSucAtMost_greaterThanAtMost)
+qed
lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
--- a/src/HOL/Tools/res_reconstruct.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Mon Jun 08 09:23:04 2009 +0200
@@ -452,7 +452,7 @@
isar_header (map #1 fixes) ^ String.concat ilines ^ "qed\n"
end
handle e => (*FIXME: exn handler is too general!*)
- let val msg = "Translation of TSTP raised an exception: " ^ Toplevel.exn_message e
+ let val msg = "Translation of TSTP raised an exception: " ^ ML_Compiler.exn_message e
in trace msg; msg end;
--- a/src/Pure/General/basics.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/General/basics.ML Mon Jun 08 09:23:04 2009 +0200
@@ -94,7 +94,7 @@
(* partiality *)
fun try f x = SOME (f x)
- handle Exn.Interrupt => raise Exn.Interrupt | _ => NONE;
+ handle (exn as Exn.Interrupt) => reraise exn | _ => NONE;
fun can f x = is_some (try f x);
--- a/src/Pure/General/markup.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/General/markup.ML Mon Jun 08 09:23:04 2009 +0200
@@ -71,6 +71,8 @@
val ML_commentN: string val ML_comment: T
val ML_malformedN: string val ML_malformed: T
val ML_defN: string val ML_def: T
+ val ML_openN: string val ML_open: T
+ val ML_structN: string val ML_struct: T
val ML_refN: string val ML_ref: T
val ML_typingN: string val ML_typing: T
val ML_sourceN: string val ML_source: T
@@ -237,6 +239,8 @@
val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
val (ML_defN, ML_def) = markup_elem "ML_def";
+val (ML_openN, ML_open) = markup_elem "ML_open";
+val (ML_structN, ML_struct) = markup_elem "ML_struct";
val (ML_refN, ML_ref) = markup_elem "ML_ref";
val (ML_typingN, ML_typing) = markup_elem "ML_typing";
--- a/src/Pure/General/markup.scala Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/General/markup.scala Mon Jun 08 09:23:04 2009 +0200
@@ -92,6 +92,8 @@
val ML_MALFORMED = "ML_malformed"
val ML_DEF = "ML_def"
+ val ML_OPEN = "ML_open"
+ val ML_STRUCT = "ML_struct"
val ML_REF = "ML_ref"
val ML_TYPING = "ML_typing"
--- a/src/Pure/General/secure.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/General/secure.ML Mon Jun 08 09:23:04 2009 +0200
@@ -70,7 +70,7 @@
val use_text = Secure.use_text;
val use_file = Secure.use_file;
fun use s = Secure.use_file ML_Parse.global_context true s
- handle ERROR msg => (writeln msg; raise Fail "ML error");
+ handle ERROR msg => (writeln msg; error "ML error");
val toplevel_pp = Secure.toplevel_pp;
val system_out = Secure.system_out;
val system = Secure.system;
--- a/src/Pure/General/xml.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/General/xml.ML Mon Jun 08 09:23:04 2009 +0200
@@ -11,7 +11,6 @@
Elem of string * attributes * tree list
| Text of string
val add_content: tree -> Buffer.T -> Buffer.T
- val detect: string -> bool
val header: string
val text: string -> string
val element: string -> attributes -> string list -> string
@@ -43,7 +42,6 @@
(** string representation **)
-val detect = String.isPrefix "<?xml";
val header = "<?xml version=\"1.0\"?>\n";
--- a/src/Pure/General/yxml.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/General/yxml.ML Mon Jun 08 09:23:04 2009 +0200
@@ -15,7 +15,6 @@
signature YXML =
sig
- val detect: string -> bool
val output_markup: Markup.T -> string * string
val element: string -> XML.attributes -> string list -> string
val string_of: XML.tree -> string
@@ -35,8 +34,6 @@
val XY = X ^ Y;
val XYX = XY ^ X;
-val detect = String.isPrefix XY;
-
(* output *)
--- a/src/Pure/General/yxml.scala Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/General/yxml.scala Mon Jun 08 09:23:04 2009 +0200
@@ -18,12 +18,6 @@
private val X_string = X.toString
private val Y_string = Y.toString
- def detect(source: CharSequence) = {
- source.length >= 2 &&
- source.charAt(0) == X &&
- source.charAt(1) == Y
- }
-
/* iterate over chunks (resembles space_explode in ML) */
--- a/src/Pure/IsaMakefile Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/IsaMakefile Mon Jun 08 09:23:04 2009 +0200
@@ -62,12 +62,12 @@
Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \
Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
- Isar/rule_cases.ML Isar/rule_insts.ML Isar/skip_proof.ML \
- Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \
- Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \
- ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML \
- ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
- ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
+ Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML \
+ Isar/skip_proof.ML Isar/spec_parse.ML Isar/specification.ML \
+ Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML \
+ ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML \
+ ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML \
+ ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \
Proof/extraction.ML Proof/proof_rewrite_rules.ML \
Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
@@ -118,8 +118,9 @@
General/position.scala General/swing.scala General/symbol.scala \
General/xml.scala General/yxml.scala Isar/isar.scala \
Isar/isar_document.scala Isar/outer_keyword.scala \
- System/isabelle_process.scala System/isabelle_system.scala \
- Thy/thy_header.scala Tools/isabelle_syntax.scala
+ System/cygwin.scala System/isabelle_process.scala \
+ System/isabelle_system.scala Thy/thy_header.scala \
+ Tools/isabelle_syntax.scala
SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/runtime.ML Mon Jun 08 09:23:04 2009 +0200
@@ -0,0 +1,107 @@
+(* Title: Pure/Isar/runtime.ML
+ Author: Makarius
+
+Isar toplevel runtime support.
+*)
+
+signature RUNTIME =
+sig
+ exception UNDEF
+ exception TERMINATE
+ exception EXCURSION_FAIL of exn * string
+ exception TOPLEVEL_ERROR
+ val exn_context: Proof.context option -> exn -> exn
+ val exn_message: (exn -> Position.T) -> exn -> string
+ val debugging: ('a -> 'b) -> 'a -> 'b
+ val controlled_execution: ('a -> 'b) -> 'a -> 'b
+ val toplevel_error: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
+end;
+
+structure Runtime: RUNTIME =
+struct
+
+(** exceptions **)
+
+exception UNDEF;
+exception TERMINATE;
+exception EXCURSION_FAIL of exn * string;
+exception TOPLEVEL_ERROR;
+
+
+(* exn_context *)
+
+exception CONTEXT of Proof.context * exn;
+
+fun exn_context NONE exn = exn
+ | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
+
+
+(* exn_message *)
+
+fun if_context NONE _ _ = []
+ | if_context (SOME ctxt) f xs = map (f ctxt) xs;
+
+fun exn_message exn_position e =
+ let
+ fun raised exn name msgs =
+ let val pos = Position.str_of (exn_position exn) in
+ (case msgs of
+ [] => "exception " ^ name ^ " raised" ^ pos
+ | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
+ | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
+ end;
+
+ val detailed = ! Output.debugging;
+
+ fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
+ | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
+ | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
+ exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
+ | exn_msg _ TERMINATE = "Exit."
+ | exn_msg _ Exn.Interrupt = "Interrupt."
+ | exn_msg _ TimeLimit.TimeOut = "Timeout."
+ | exn_msg _ TOPLEVEL_ERROR = "Error."
+ | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
+ | exn_msg _ (ERROR msg) = msg
+ | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
+ | exn_msg _ (exn as THEORY (msg, thys)) =
+ raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
+ | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
+ (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
+ | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
+ (if detailed then
+ if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
+ else []))
+ | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
+ (if detailed then if_context ctxt Syntax.string_of_term ts else []))
+ | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
+ (if detailed then if_context ctxt ProofContext.string_of_thm thms else []))
+ | exn_msg _ exn = raised exn (General.exnMessage exn) [];
+ in exn_msg NONE e end;
+
+
+
+(** controlled execution **)
+
+fun debugging f x =
+ if ! Output.debugging then
+ Exn.release (exception_trace (fn () =>
+ Exn.Result (f x) handle
+ exn as UNDEF => Exn.Exn exn
+ | exn as EXCURSION_FAIL _ => Exn.Exn exn))
+ else f x;
+
+fun controlled_execution f =
+ f
+ |> debugging
+ |> Future.interruptible_task;
+
+fun toplevel_error exn_message f x =
+ let val ctxt = Option.map Context.proof_of (Context.thread_data ()) in
+ f x handle exn =>
+ (Output.error_msg (exn_message (exn_context ctxt exn));
+ raise TOPLEVEL_ERROR)
+ end;
+
+end;
+
--- a/src/Pure/Isar/toplevel.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/Isar/toplevel.ML Mon Jun 08 09:23:04 2009 +0200
@@ -32,8 +32,6 @@
val skip_proofs: bool ref
exception TERMINATE
exception TOPLEVEL_ERROR
- exception CONTEXT of Proof.context * exn
- val exn_message: exn -> string
val program: (unit -> 'a) -> 'a
type transition
val empty: transition
@@ -98,7 +96,7 @@
(** toplevel state **)
-exception UNDEF;
+exception UNDEF = Runtime.UNDEF;
(* local theory wrappers *)
@@ -225,102 +223,20 @@
val profiling = ref 0;
val skip_proofs = ref false;
-exception TERMINATE;
-exception EXCURSION_FAIL of exn * string;
-exception FAILURE of state * exn;
-exception TOPLEVEL_ERROR;
-
-
-(* print exceptions *)
-
-exception CONTEXT of Proof.context * exn;
-
-fun exn_context NONE exn = exn
- | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
-
-local
-
-fun if_context NONE _ _ = []
- | if_context (SOME ctxt) f xs = map (f ctxt) xs;
-
-fun raised exn name msgs =
- let val pos = Position.str_of (ML_Compiler.exception_position exn) in
- (case msgs of
- [] => "exception " ^ name ^ " raised" ^ pos
- | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
- | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
- end;
-
-in
-
-fun exn_message e =
- let
- val detailed = ! debug;
-
- fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
- | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
- | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
- exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
- | exn_msg _ TERMINATE = "Exit."
- | exn_msg _ Exn.Interrupt = "Interrupt."
- | exn_msg _ TimeLimit.TimeOut = "Timeout."
- | exn_msg _ TOPLEVEL_ERROR = "Error."
- | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
- | exn_msg _ (ERROR msg) = msg
- | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
- | exn_msg _ (exn as THEORY (msg, thys)) =
- raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
- | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
- (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
- | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
- (if detailed then
- if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
- else []))
- | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
- (if detailed then if_context ctxt Syntax.string_of_term ts else []))
- | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
- (if detailed then if_context ctxt ProofContext.string_of_thm thms else []))
- | exn_msg _ exn = raised exn (General.exnMessage exn) []
- in exn_msg NONE e end;
-
-end;
-
-
-(* controlled execution *)
-
-local
-
-fun debugging f x =
- if ! debug then
- Exn.release (exception_trace (fn () =>
- Exn.Result (f x) handle
- exn as UNDEF => Exn.Exn exn
- | exn as EXCURSION_FAIL _ => Exn.Exn exn))
- else f x;
-
-fun toplevel_error f x =
- let val ctxt = try ML_Context.the_local_context () in
- f x handle exn =>
- (Output.error_msg (exn_message (exn_context ctxt exn)); raise TOPLEVEL_ERROR)
- end;
-
-in
-
-fun controlled_execution f =
- f
- |> debugging
- |> Future.interruptible_task;
+exception TERMINATE = Runtime.TERMINATE;
+exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
+exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
fun program f =
(f
- |> controlled_execution
- |> toplevel_error) ();
-
-end;
+ |> Runtime.controlled_execution
+ |> Runtime.toplevel_error ML_Compiler.exn_message) ();
(* node transactions -- maintaining stable checkpoints *)
+exception FAILURE of state * exn;
+
local
fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
@@ -329,7 +245,7 @@
fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy)
| is_draft_theory _ = false;
-fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
+fun is_stale state = Context.is_stale (theory_of state) handle Runtime.UNDEF => false;
fun stale_error NONE = SOME (ERROR "Stale theory encountered after successful execution!")
| stale_error some = some;
@@ -349,7 +265,7 @@
val (result, err) =
cont_node
- |> controlled_execution f
+ |> Runtime.controlled_execution f
|> map_theory Theory.checkpoint
|> state_error NONE
handle exn => state_error (SOME exn) cont_node;
@@ -382,9 +298,9 @@
| apply_tr _ _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
State (NONE, prev)
| apply_tr _ _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
- (controlled_execution exit thy; toplevel)
+ (Runtime.controlled_execution exit thy; toplevel)
| apply_tr int _ (Keep f) state =
- controlled_execution (fn x => tap (f int) x) state
+ Runtime.controlled_execution (fn x => tap (f int) x) state
| apply_tr int pos (Transaction (f, g)) (State (SOME state, _)) =
apply_transaction pos (fn x => f int x) g state
| apply_tr _ _ _ _ = raise UNDEF;
@@ -392,7 +308,7 @@
fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
| apply_union int pos (tr :: trs) state =
apply_union int pos trs state
- handle UNDEF => apply_tr int pos tr state
+ handle Runtime.UNDEF => apply_tr int pos tr state
| FAILURE (alt_state, UNDEF) => apply_tr int pos tr alt_state
| exn as FAILURE _ => raise exn
| exn => raise FAILURE (state, exn);
@@ -628,7 +544,8 @@
setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
fun error_msg tr exn_info =
- setmp_thread_position tr (fn () => Output.error_msg (exn_message (EXCURSION_FAIL exn_info))) ();
+ setmp_thread_position tr (fn () =>
+ Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
(* post-transition hooks *)
@@ -671,7 +588,7 @@
(case app int tr st of
(_, SOME TERMINATE) => NONE
| (st', SOME (EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
- | (st', SOME exn) => SOME (st', SOME (exn_context ctxt exn, at_command tr))
+ | (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr))
| (st', NONE) => SOME (st', NONE));
val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
in res end;
--- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML Mon Jun 08 09:23:04 2009 +0200
@@ -21,7 +21,7 @@
[] => ()
| _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
in
- exec () handle exn => (error (output ()); raise exn);
+ exec () handle exn => (error (output ()); reraise exn);
if verbose then print (output ()) else ()
end;
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML Mon Jun 08 09:23:04 2009 +0200
@@ -38,7 +38,7 @@
PolyML.compiler (get, parameters) ())
handle exn =>
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); raise exn);
+ error (output ()); reraise exn);
in if verbose then print (output ()) else () end;
fun use_file context verbose name =
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Mon Jun 08 09:23:04 2009 +0200
@@ -14,7 +14,7 @@
fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
(start_line, name) verbose txt =
let
- val current_line = ref start_line;
+ val line = ref start_line;
val in_buffer = ref (String.explode (tune_source txt));
val out_buffer = ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
@@ -22,8 +22,7 @@
fun get () =
(case ! in_buffer of
[] => NONE
- | c :: cs =>
- (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
+ | c :: cs => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c));
fun put s = out_buffer := s :: ! out_buffer;
fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
(put (if hard then "Error: " else "Warning: ");
@@ -33,16 +32,17 @@
val parameters =
[PolyML.Compiler.CPOutStream put,
- PolyML.Compiler.CPLineNo (fn () => ! current_line),
+ PolyML.Compiler.CPNameSpace name_space,
PolyML.Compiler.CPErrorMessageProc put_message,
- PolyML.Compiler.CPNameSpace name_space,
+ PolyML.Compiler.CPLineNo (fn () => ! line),
+ PolyML.Compiler.CPFileName name,
PolyML.Compiler.CPPrintInAlphabeticalOrder false];
val _ =
(while not (List.null (! in_buffer)) do
PolyML.compiler (get, parameters) ())
handle exn =>
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); raise exn);
+ error (output ()); reraise exn);
in if verbose then print (output ()) else () end;
fun use_file context verbose name =
--- a/src/Pure/ML/ml_compiler.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/ML/ml_compiler.ML Mon Jun 08 09:23:04 2009 +0200
@@ -6,14 +6,16 @@
signature ML_COMPILER =
sig
- val exception_position: exn -> Position.T
+ val exn_position: exn -> Position.T
+ val exn_message: exn -> string
val eval: bool -> Position.T -> ML_Lex.token list -> unit
end
structure ML_Compiler: ML_COMPILER =
struct
-fun exception_position _ = Position.none;
+fun exn_position _ = Position.none;
+val exn_message = Runtime.exn_message exn_position;
fun eval verbose pos toks =
let
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Jun 08 09:23:04 2009 +0200
@@ -1,12 +1,13 @@
(* Title: Pure/ML/ml_compiler_polyml-5.3.ML
Author: Makarius
-Advanced runtime compilation for Poly/ML 5.3 (SVN 762).
+Advanced runtime compilation for Poly/ML 5.3 (SVN 773).
*)
signature ML_COMPILER =
sig
- val exception_position: exn -> Position.T
+ val exn_position: exn -> Position.T
+ val exn_message: exn -> string
val eval: bool -> Position.T -> ML_Lex.token list -> unit
end
@@ -31,24 +32,28 @@
loc_props
end |> Position.of_properties;
-fun exception_position exn =
+fun exn_position exn =
(case PolyML.exceptionLocation exn of
NONE => Position.none
| SOME loc => position_of loc);
+val exn_message = Runtime.exn_message exn_position;
+
(* parse trees *)
fun report_parse_tree depth space =
let
+ fun report_decl markup loc decl =
+ Position.report_text Markup.ML_ref (position_of loc)
+ (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
fun report loc (PolyML.PTtype types) =
PolyML.NameSpace.displayTypeExpression (types, depth, space)
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of
|> Position.report_text Markup.ML_typing (position_of loc)
- | report loc (PolyML.PTdeclaredAt decl) =
- Markup.markup
- (Markup.properties (Position.properties_of (position_of decl)) Markup.ML_def) ""
- |> Position.report_text Markup.ML_ref (position_of loc)
+ | report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
+ | report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
+ | report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
| report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
| report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
| report _ _ = ()
@@ -77,7 +82,11 @@
(Position.reset_range (ML_Lex.pos_of tok));
in ps ~~ map (String.explode o Symbol.esc) syms end);
- val input_buffer = ref input;
+ val end_pos =
+ if null toks then Position.none
+ else ML_Lex.end_pos_of (List.last toks);
+
+ val input_buffer = ref (input @ [(end_pos, [#"\n"])]);
val line = ref (the_default 1 (Position.line_of pos));
fun get_offset () =
@@ -139,10 +148,13 @@
end;
fun result_fun (phase1, phase2) () =
- (case phase1 of NONE => ()
- | SOME parse_tree => report_parse_tree depth space parse_tree;
- case phase2 of NONE => err "Static Errors"
- | SOME code => apply_result (code ())); (* FIXME cf. Toplevel.program *)
+ ((case phase1 of
+ NONE => ()
+ | SOME parse_tree => report_parse_tree depth space parse_tree);
+ (case phase2 of
+ NONE => err "Static Errors"
+ | SOME code =>
+ apply_result ((code |> Runtime.debugging |> Runtime.toplevel_error exn_message) ())));
(* compiler invocation *)
@@ -152,15 +164,16 @@
PolyML.Compiler.CPNameSpace space,
PolyML.Compiler.CPErrorMessageProc put_message,
PolyML.Compiler.CPLineNo (fn () => ! line),
+ PolyML.Compiler.CPLineOffset get_offset,
PolyML.Compiler.CPFileName location_props,
- PolyML.Compiler.CPLineOffset get_offset,
- PolyML.Compiler.CPCompilerResultFun result_fun];
+ PolyML.Compiler.CPCompilerResultFun result_fun,
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false];
val _ =
(while not (List.null (! input_buffer)) do
PolyML.compiler (get, parameters) ())
handle exn =>
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
- err (output ()); raise exn);
+ err (output ()); reraise exn);
in if verbose then print (output ()) else () end;
end;
--- a/src/Pure/ML/ml_env.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/ML/ml_env.ML Mon Jun 08 09:23:04 2009 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/ML/ml_env.ML
Author: Makarius
-Local environment of ML sources and results.
+Local environment of ML results.
*)
signature ML_ENV =
--- a/src/Pure/ML/ml_lex.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/ML/ml_lex.ML Mon Jun 08 09:23:04 2009 +0200
@@ -15,6 +15,7 @@
val is_improper: token -> bool
val set_range: Position.range -> token -> token
val pos_of: token -> Position.T
+ val end_pos_of: token -> Position.T
val kind_of: token -> token_kind
val content_of: token -> string
val check_content_of: token -> string
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Jun 08 09:23:04 2009 +0200
@@ -1000,7 +1000,7 @@
| (Toplevel.UNDEF,SOME src) =>
(Output.error_msg "No working context defined"; loop true src)
| (e,SOME src) =>
- (Output.error_msg (Toplevel.exn_message e); loop true src)
+ (Output.error_msg (ML_Compiler.exn_message e); loop true src)
| (PGIP_QUIT,_) => ()
| (_,NONE) => ()
in
--- a/src/Pure/ROOT.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/ROOT.ML Mon Jun 08 09:23:04 2009 +0200
@@ -155,6 +155,7 @@
(*ML support*)
use "ML/ml_syntax.ML";
use "ML/ml_env.ML";
+use "Isar/runtime.ML";
if ml_system = "polyml-experimental"
then use "ML/ml_compiler_polyml-5.3.ML"
else use "ML/ml_compiler.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/cygwin.scala Mon Jun 08 09:23:04 2009 +0200
@@ -0,0 +1,84 @@
+/* Title: Pure/System/cygwin.scala
+ Author: Makarius
+
+Accessing the Cygwin installation.
+*/
+
+package isabelle
+
+import java.lang.reflect.Method
+
+
+object Cygwin
+{
+ /* registry access */
+
+ // Some black magic involving private WindowsPreferences from Sun, cf.
+ // http://www.docjar.com/html/api/java/util/prefs/WindowsPreferences.java.html
+
+ private val WindowsPreferences = Class.forName("java.util.prefs.WindowsPreferences")
+
+ private val HKEY_CURRENT_USER = 0x80000001
+ private val HKEY_LOCAL_MACHINE = 0x80000002
+ private val KEY_READ = 0x20019
+ private val NATIVE_HANDLE = 0
+ private val ERROR_CODE = 1
+
+ private def C_string(s: String): Array[Byte] =
+ (s + "\0").getBytes("US-ASCII")
+
+ private def J_string(bs: Array[Byte]): String =
+ new String(bs, 0, bs.length - 1, "US-ASCII")
+
+ private val INT = Integer.TYPE
+ private val BYTES = (new Array[Byte](0)).getClass
+
+ private def open_key(handle: Int, subkey: Array[Byte], mask: Int): Array[Int] =
+ {
+ val m = WindowsPreferences.getDeclaredMethod("WindowsRegOpenKey", INT, BYTES, INT)
+ m.setAccessible(true)
+ m.invoke(null, handle.asInstanceOf[Object], subkey.asInstanceOf[Object],
+ mask.asInstanceOf[Object]).asInstanceOf[Array[Int]]
+ }
+
+ private def close_key(handle: Int): Int =
+ {
+ val m = WindowsPreferences.getDeclaredMethod("WindowsRegCloseKey", INT)
+ m.setAccessible(true)
+ m.invoke(null, handle.asInstanceOf[Object]).asInstanceOf[Int]
+ }
+
+ private def query(handle: Int, name: Array[Byte]) =
+ {
+ val m = WindowsPreferences.getDeclaredMethod("WindowsRegQueryValueEx", INT, BYTES)
+ m.setAccessible(true)
+ m.invoke(null, handle.asInstanceOf[Object], name.asInstanceOf[Object]).
+ asInstanceOf[Array[Byte]]
+ }
+
+ def query_registry(sys: Boolean, path: String, name: String): Option[String] =
+ {
+ val handle = if (sys) HKEY_LOCAL_MACHINE else HKEY_CURRENT_USER
+ val result = open_key(handle, C_string(path), KEY_READ)
+ if (result(ERROR_CODE) != 0) None
+ else {
+ val res = query(result(NATIVE_HANDLE), C_string(name))
+ if (res == null) None
+ else Some(J_string(res))
+ }
+ }
+
+ def query_registry(path: String, name: String): Option[String] =
+ query_registry(false, path, name) orElse
+ query_registry(true, path, name)
+
+
+ /* Cygwin installation */
+
+ private val CYGWIN_MOUNTS = "Software\\Cygnus Solutions\\Cygwin\\mounts v2"
+
+ def cygdrive(): Option[String] = query_registry(CYGWIN_MOUNTS, "cygdrive prefix")
+ def root(): Option[String] = query_registry(CYGWIN_MOUNTS + "\\/", "native")
+
+}
+
--- a/src/Pure/System/isabelle_process.scala Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/System/isabelle_process.scala Mon Jun 08 09:23:04 2009 +0200
@@ -230,7 +230,7 @@
private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
override def run() = {
- val writer = new BufferedWriter(new OutputStreamWriter(out_stream, isabelle_system.charset))
+ val writer = new BufferedWriter(new OutputStreamWriter(out_stream, IsabelleSystem.charset))
var finished = false
while (!finished) {
try {
@@ -260,7 +260,7 @@
private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
override def run() = {
- val reader = new BufferedReader(new InputStreamReader(in_stream, isabelle_system.charset))
+ val reader = new BufferedReader(new InputStreamReader(in_stream, IsabelleSystem.charset))
var result = new StringBuilder(100)
var finished = false
--- a/src/Pure/System/isabelle_system.scala Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala Mon Jun 08 09:23:04 2009 +0200
@@ -12,10 +12,43 @@
import scala.io.Source
-class IsabelleSystem {
+object IsabelleSystem
+{
val charset = "UTF-8"
+ val is_cygwin = System.getProperty("os.name").startsWith("Windows")
+
+
+ /* shell processes */
+
+ private def raw_execute(env: Map[String, String], redirect: Boolean, args: String*): Process =
+ {
+ val cmdline = new java.util.LinkedList[String]
+ for (s <- args) cmdline.add(s)
+
+ val proc = new ProcessBuilder(cmdline)
+ proc.environment.clear
+ for ((x, y) <- env) proc.environment.put(x, y)
+ proc.redirectErrorStream(redirect)
+
+ try { proc.start }
+ catch { case e: IOException => error(e.getMessage) }
+ }
+
+ private def process_output(proc: Process): (String, Int) =
+ {
+ proc.getOutputStream.close
+ val output = Source.fromInputStream(proc.getInputStream, charset).mkString
+ val rc = proc.waitFor
+ (output, rc)
+ }
+
+}
+
+
+class IsabelleSystem
+{
/* unique ids */
@@ -23,47 +56,99 @@
def id(): String = synchronized { id_count += 1; "j" + id_count }
- /* Isabelle environment settings */
-
- private val environment = System.getenv
+ /* Isabelle settings environment */
- def getenv(name: String) = {
- val value = environment.get(if (name == "HOME") "HOME_JVM" else name)
- if (value != null) value else ""
+ private val (cygdrive_pattern, cygwin_root, shell_prefix) =
+ {
+ if (IsabelleSystem.is_cygwin) {
+ val cygdrive = Cygwin.cygdrive getOrElse "/cygdrive"
+ val pattern = Pattern.compile(cygdrive + "/([a-zA-Z])($|/.*)")
+ val root = Cygwin.root getOrElse "C:\\cygwin"
+ val bash = List(root + "\\bin\\bash", "-l")
+ (Some(pattern), Some(root), bash)
+ }
+ else (None, None, Nil)
}
- def getenv_strict(name: String) = {
+ private val environment: Map[String, String] =
+ {
+ import scala.collection.jcl.Conversions._
+
+ val env0 = Map(java.lang.System.getenv.toList: _*)
+
+ val isabelle =
+ env0.get("ISABELLE_TOOL") match {
+ case None | Some("") =>
+ val isabelle = java.lang.System.getProperty("isabelle.tool")
+ if (isabelle == null || isabelle == "") "isabelle"
+ else isabelle
+ case Some(isabelle) => isabelle
+ }
+
+ val dump = File.createTempFile("isabelle", null)
+ try {
+ val cmdline = shell_prefix ::: List(isabelle, "getenv", "-d", dump.toString)
+ val proc = IsabelleSystem.raw_execute(env0, true, cmdline: _*)
+ val (output, rc) = IsabelleSystem.process_output(proc)
+ if (rc != 0) error(output)
+
+ val entries =
+ for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
+ val i = entry.indexOf('=')
+ if (i <= 0) (entry -> "")
+ else (entry.substring(0, i) -> entry.substring(i + 1))
+ }
+ Map(entries: _*)
+ }
+ finally { dump.delete }
+ }
+
+ def getenv(name: String): String =
+ {
+ environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
+ }
+
+ def getenv_strict(name: String): String =
+ {
val value = getenv(name)
if (value != "") value else error("Undefined environment variable: " + name)
}
- val is_cygwin = Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM"))
-
/* file path specifications */
- private val cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)")
-
- def platform_path(source_path: String) = {
+ def platform_path(source_path: String): String =
+ {
val result_path = new StringBuilder
- def init(path: String) = {
- val cygdrive = cygdrive_pattern.matcher(path)
- if (cygdrive.matches) {
- result_path.length = 0
- result_path.append(cygdrive.group(1))
- result_path.append(":")
- result_path.append(File.separator)
- cygdrive.group(2)
- }
- else if (path.startsWith("/")) {
+ def init_plain(path: String): String =
+ {
+ if (path.startsWith("/")) {
result_path.length = 0
result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))
path.substring(1)
}
else path
}
- def append(path: String) = {
+ def init(path: String): String =
+ {
+ cygdrive_pattern match {
+ case Some(pattern) =>
+ val cygdrive = pattern.matcher(path)
+ if (cygdrive.matches) {
+ result_path.length = 0
+ result_path.append(cygdrive.group(1))
+ result_path.append(":")
+ result_path.append(File.separator)
+ cygdrive.group(2)
+ }
+ else init_plain(path)
+ case None => init_plain(path)
+ }
+ }
+
+ def append(path: String)
+ {
for (p <- init(path).split("/")) {
if (p != "") {
val len = result_path.length
@@ -82,17 +167,16 @@
result_path.toString
}
- def platform_file(path: String) =
- new File(platform_path(path))
+ def platform_file(path: String) = new File(platform_path(path))
/* source files */
private def try_file(file: File) = if (file.isFile) Some(file) else None
- def source_file(path: String): Option[File] = {
- if (path == "ML") None
- else if (path.startsWith("/") || path == "")
+ def source_file(path: String): Option[File] =
+ {
+ if (path.startsWith("/") || path == "")
try_file(platform_file(path))
else {
val pure_file = platform_file("~~/src/Pure/" + path)
@@ -104,59 +188,52 @@
}
- /* shell processes */
+ /* external processes */
- def execute(redirect: Boolean, args: String*): Process = {
- val cmdline = new java.util.LinkedList[String]
- if (is_cygwin) cmdline.add(platform_path("/bin/env"))
- for (s <- args) cmdline.add(s)
-
- val proc = new ProcessBuilder(cmdline)
- proc.environment.clear
- proc.environment.putAll(environment)
- proc.redirectErrorStream(redirect)
- proc.start
+ def execute(redirect: Boolean, args: String*): Process =
+ {
+ val cmdline =
+ if (IsabelleSystem.is_cygwin) List(platform_path("/bin/env")) ++ args
+ else args
+ IsabelleSystem.raw_execute(environment, redirect, cmdline: _*)
}
-
- /* Isabelle tools (non-interactive) */
-
- def isabelle_tool(args: String*) = {
- val proc =
- try { execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*) }
- catch { case e: IOException => error(e.getMessage) }
- proc.getOutputStream.close
- val output = Source.fromInputStream(proc.getInputStream, charset).mkString
- val rc = proc.waitFor
- (output, rc)
+ def isabelle_tool(args: String*): (String, Int) =
+ {
+ val proc = execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*)
+ IsabelleSystem.process_output(proc)
}
/* named pipes */
- def mk_fifo() = {
+ def mk_fifo(): String =
+ {
val (result, rc) = isabelle_tool("mkfifo")
if (rc == 0) result.trim
else error(result)
}
- def rm_fifo(fifo: String) = {
+ def rm_fifo(fifo: String)
+ {
val (result, rc) = isabelle_tool("rmfifo", fifo)
if (rc != 0) error(result)
}
- def fifo_reader(fifo: String) = {
+ def fifo_reader(fifo: String): BufferedReader =
+ {
// blocks until writer is ready
val stream =
- if (is_cygwin) execute(false, "cat", fifo).getInputStream
+ if (IsabelleSystem.is_cygwin) execute(false, "cat", fifo).getInputStream
else new FileInputStream(fifo)
- new BufferedReader(new InputStreamReader(stream, charset))
+ new BufferedReader(new InputStreamReader(stream, IsabelleSystem.charset))
}
/* find logics */
- def find_logics() = {
+ def find_logics(): List[String] =
+ {
val ml_ident = getenv_strict("ML_IDENTIFIER")
var logics: Set[String] = Set()
for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
@@ -171,7 +248,8 @@
/* symbols */
- private def read_symbols(path: String) = {
+ private def read_symbols(path: String): Iterator[String] =
+ {
val file = new File(platform_path(path))
if (file.isFile) Source.fromFile(file).getLines
else Iterator.empty
--- a/src/Pure/System/isar.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/System/isar.ML Mon Jun 08 09:23:04 2009 +0200
@@ -134,7 +134,7 @@
NONE => if secure then quit () else ()
| SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
handle exn =>
- (Output.error_msg (Toplevel.exn_message exn)
+ (Output.error_msg (ML_Compiler.exn_message exn)
handle crash =>
(CRITICAL (fn () => change crashes (cons crash));
warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
--- a/src/Pure/System/session.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Pure/System/session.ML Mon Jun 08 09:23:04 2009 +0200
@@ -107,6 +107,6 @@
|> setmp_noncritical Multithreading.max_threads
(if Multithreading.available then max_threads
else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
- handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
+ handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
end;
--- a/src/Tools/code/code_ml.ML Mon Jun 08 09:22:47 2009 +0200
+++ b/src/Tools/code/code_ml.ML Mon Jun 08 09:23:04 2009 +0200
@@ -47,9 +47,6 @@
fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
let
- val pr_label_classrel = translate_string (fn "." => "__" | c => c)
- o Long_Name.qualifier;
- val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier;
fun pr_dicts fxy ds =
let
fun pr_dictvar (v, (_, 1)) = Code_Printer.first_upper v ^ "_"
@@ -272,11 +269,11 @@
val w = Code_Printer.first_upper v ^ "_";
fun pr_superclass_field (class, classrel) =
(concat o map str) [
- pr_label_classrel classrel, ":", "'" ^ v, deresolve class
+ deresolve classrel, ":", "'" ^ v, deresolve class
];
fun pr_classparam_field (classparam, ty) =
concat [
- (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty
+ (str o deresolve) classparam, str ":", pr_typ NOBR ty
];
fun pr_classparam_proj (classparam, _) =
semicolon [
@@ -284,7 +281,7 @@
(str o deresolve) classparam,
Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
str "=",
- str ("#" ^ pr_label_classparam classparam),
+ str ("#" ^ deresolve classparam),
str w
];
fun pr_superclass_proj (_, classrel) =
@@ -293,7 +290,7 @@
(str o deresolve) classrel,
Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
str "=",
- str ("#" ^ pr_label_classrel classrel),
+ str ("#" ^ deresolve classrel),
str w
];
in
@@ -314,13 +311,13 @@
let
fun pr_superclass (_, (classrel, dss)) =
concat [
- (str o pr_label_classrel) classrel,
+ (str o deresolve) classrel,
str "=",
pr_dicts NOBR [DictConst dss]
];
fun pr_classparam ((classparam, c_inst), (thm, _)) =
concat [
- (str o pr_label_classparam) classparam,
+ (str o deresolve) classparam,
str "=",
pr_app (K false) thm reserved_names NOBR (c_inst, [])
];