--- a/src/HOL/Decision_Procs/Approximation.thy Fri Jun 10 16:28:48 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Jun 10 16:36:24 2016 +0200
@@ -1847,7 +1847,7 @@
thus ?thesis unfolding True power_0_left by auto
next
case False hence "real_of_float x < 0" using \<open>real_of_float x \<le> 0\<close> by auto
- show ?thesis by (rule less_imp_le, auto simp add: power_less_zero_eq \<open>real_of_float x < 0\<close>)
+ show ?thesis by (rule less_imp_le, auto simp add: \<open>real_of_float x < 0\<close>)
qed
obtain t where "\<bar>t\<bar> \<le> \<bar>real_of_float x\<bar>"
and "exp x = (\<Sum>m = 0..<get_odd n. (real_of_float x) ^ m / (fact m)) + exp t / (fact (get_odd n)) * (real_of_float x) ^ (get_odd n)"
@@ -2100,7 +2100,7 @@
have "exp x \<le> (1 :: float) / lb_exp prec (-x)"
using lb_exp lb_exp_pos[OF \<open>\<not> 0 < -x\<close>, of prec]
- by (simp del: lb_exp.simps add: exp_minus inverse_eq_divide field_simps)
+ by (simp del: lb_exp.simps add: exp_minus field_simps)
also have "\<dots> \<le> float_divr prec 1 (lb_exp prec (-x))"
using float_divr .
finally show ?thesis
@@ -2550,8 +2550,8 @@
from bitlen_div[OF \<open>0 < m\<close>] float_gt1_scale[OF \<open>1 \<le> Float m e\<close>] \<open>bl \<ge> 0\<close>
have x_bnds: "0 \<le> real_of_float (?x - 1)" "real_of_float (?x - 1) < 1"
unfolding bl_def[symmetric]
- by (auto simp: powr_realpow[symmetric] field_simps inverse_eq_divide)
- (auto simp : powr_minus field_simps inverse_eq_divide)
+ by (auto simp: powr_realpow[symmetric] field_simps)
+ (auto simp : powr_minus field_simps)
{
have "float_round_down prec (lb_ln2 prec * ?s) \<le> ln 2 * (e + (bitlen m - 1))"
@@ -2822,6 +2822,7 @@
| Powr floatarith floatarith
| Ln floatarith
| Power floatarith nat
+ | Floor floatarith
| Var nat
| Num float
@@ -2841,6 +2842,7 @@
"interpret_floatarith (Powr a b) vs = interpret_floatarith a vs powr interpret_floatarith b vs" |
"interpret_floatarith (Ln a) vs = ln (interpret_floatarith a vs)" |
"interpret_floatarith (Power a n) vs = (interpret_floatarith a vs)^n" |
+"interpret_floatarith (Floor a) vs = floor (interpret_floatarith a vs)" |
"interpret_floatarith (Num f) vs = f" |
"interpret_floatarith (Var n) vs = vs ! n"
@@ -2880,6 +2882,10 @@
and "interpret_floatarith (Num (Float (- numeral a) 0)) vs = - numeral a"
by auto
+lemma interpret_floatarith_ceiling:
+ "interpret_floatarith (Minus (Floor (Minus a))) vs = ceiling (interpret_floatarith a vs)"
+ unfolding ceiling_def interpret_floatarith.simps of_int_minus ..
+
subsection "Implement approximation function"
@@ -2960,6 +2966,7 @@
"approx prec (Powr a b) bs = lift_bin (approx' prec a bs) (approx' prec b bs) (bnds_powr prec)" |
"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 prec n)" |
+"approx prec (Floor a) bs = lift_un' (approx' prec a bs) (\<lambda> l u. (floor_fl l, floor_fl u))" |
"approx prec (Num f) bs = Some (f, f)" |
"approx prec (Var i) bs = (if i < length bs then bs ! i else None)"
@@ -3419,6 +3426,10 @@
case (Power a n)
with lift_un'_bnds[OF bnds_power] show ?case by auto
next
+ case (Floor a)
+ from lift_un'[OF Floor.prems[unfolded approx.simps] Floor.hyps]
+ show ?case by (auto simp: floor_fl.rep_eq floor_mono)
+next
case (Num f)
thus ?case by auto
next
@@ -3621,9 +3632,10 @@
"isDERIV x Pi vs = True" |
"isDERIV x (Sqrt a) vs = (isDERIV x a vs \<and> interpret_floatarith a vs > 0)" |
"isDERIV x (Exp a) vs = isDERIV x a vs" |
-"isDERIV x (Powr a b) vs =
+"isDERIV x (Powr a b) vs =
(isDERIV x a vs \<and> isDERIV x b vs \<and> interpret_floatarith a vs > 0)" |
"isDERIV x (Ln a) vs = (isDERIV x a vs \<and> interpret_floatarith a vs > 0)" |
+"isDERIV x (Floor a) vs = (isDERIV x a vs \<and> interpret_floatarith a vs \<notin> \<int>)" |
"isDERIV x (Power a 0) vs = True" |
"isDERIV x (Power a (Suc n)) vs = isDERIV x a vs" |
"isDERIV x (Num f) vs = True" |
@@ -3647,6 +3659,7 @@
"DERIV_floatarith x (Ln a) = Mult (Inverse a) (DERIV_floatarith x a)" |
"DERIV_floatarith x (Power a 0) = Num 0" |
"DERIV_floatarith x (Power a (Suc n)) = Mult (Num (Float (int (Suc n)) 0)) (Mult (Power a n) (DERIV_floatarith x a))" |
+"DERIV_floatarith x (Floor a) = Num 0" |
"DERIV_floatarith x (Num f) = Num 0" |
"DERIV_floatarith x (Var n) = (if x = n then Num 1 else Num 0)"
@@ -3692,6 +3705,10 @@
thus ?case
by (cases n) (auto intro!: derivative_eq_intros simp del: power_Suc)
next
+ case (Floor a)
+ thus ?case
+ by (auto intro!: derivative_eq_intros DERIV_isCont floor_has_real_derivative)
+next
case (Ln a)
thus ?case by (auto intro!: derivative_eq_intros simp add: divide_inverse)
next
@@ -3726,6 +3743,8 @@
"isDERIV_approx prec x (Ln a) vs =
(isDERIV_approx prec x a vs \<and> (case approx prec a vs of Some (l, u) \<Rightarrow> 0 < l | None \<Rightarrow> False))" |
"isDERIV_approx prec x (Power a 0) vs = True" |
+"isDERIV_approx prec x (Floor a) vs =
+ (isDERIV_approx prec x a vs \<and> (case approx prec a vs of Some (l, u) \<Rightarrow> l > floor u \<and> u < ceiling l | None \<Rightarrow> False))" |
"isDERIV_approx prec x (Power a (Suc n)) vs = isDERIV_approx prec x a vs" |
"isDERIV_approx prec x (Num f) vs = True" |
"isDERIV_approx prec x (Var n) vs = True"
@@ -3769,6 +3788,15 @@
with approx[OF \<open>bounded_by xs vs\<close> a]
have "0 < interpret_floatarith a xs" by auto
with Powr show ?case by auto
+next
+ case (Floor a)
+ then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
+ and "real_of_int \<lfloor>real_of_float u\<rfloor> < real_of_float l" "real_of_float u < real_of_int \<lceil>real_of_float l\<rceil>"
+ and "isDERIV x a xs"
+ by (cases "approx prec a vs") auto
+ with approx[OF \<open>bounded_by xs vs\<close> approx_Some] le_floor_iff
+ show ?case
+ by (force elim!: Ints_cases)
qed auto
lemma bounded_by_update_var:
@@ -4263,7 +4291,7 @@
lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_log
- interpret_floatarith_sin
+ interpret_floatarith_sin interpret_floatarith_ceiling
oracle approximation_oracle = \<open>fn (thy, t) =>
let
@@ -4309,6 +4337,7 @@
| floatarith_of_term (@{term Ln} $ a) = @{code Ln} (floatarith_of_term a)
| floatarith_of_term (@{term Power} $ a $ n) =
@{code Power} (floatarith_of_term a, nat_of_term n)
+ | floatarith_of_term (@{term Floor} $ a) = @{code Floor} (floatarith_of_term a)
| floatarith_of_term (@{term Var} $ n) = @{code Var} (nat_of_term n)
| floatarith_of_term (@{term Num} $ m) = @{code Num} (float_of_term m)
| floatarith_of_term t = bad t;
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Fri Jun 10 16:28:48 2016 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Fri Jun 10 16:36:24 2016 +0200
@@ -67,6 +67,9 @@
lemma "3.2 \<le> (x::real) \<and> x \<le> 6.2 \<Longrightarrow> sin x \<le> 0"
by (approximation 10)
+lemma "3.2 \<le> (x::real) \<and> x \<le> 3.9 \<Longrightarrow> real_of_int (ceiling x) \<in> {4 .. 4}"
+ by (approximation 10)
+
lemma
defines "g \<equiv> 9.80665" and "v \<equiv> 128.61" and "d \<equiv> pi / 180"
shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
--- a/src/HOL/Deriv.thy Fri Jun 10 16:28:48 2016 +0200
+++ b/src/HOL/Deriv.thy Fri Jun 10 16:36:24 2016 +0200
@@ -931,6 +931,21 @@
by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
tendsto_minus_cancel_left field_simps conj_commute)
+lemma floor_has_real_derivative:
+ fixes f::"real \<Rightarrow> 'a::{floor_ceiling,order_topology}"
+ assumes "isCont f x"
+ assumes "f x \<notin> \<int>"
+ shows "((\<lambda>x. floor (f x)) has_real_derivative 0) (at x)"
+proof (subst DERIV_cong_ev[OF refl _ refl])
+ show "((\<lambda>_. floor (f x)) has_real_derivative 0) (at x)" by simp
+ have "\<forall>\<^sub>F y in at x. \<lfloor>f y\<rfloor> = \<lfloor>f x\<rfloor>"
+ by (rule eventually_floor_eq[OF assms[unfolded continuous_at]])
+ then show "\<forall>\<^sub>F y in nhds x. real_of_int \<lfloor>f y\<rfloor> = real_of_int \<lfloor>f x\<rfloor>"
+ unfolding eventually_at_filter
+ by eventually_elim auto
+qed
+
+
text \<open>Caratheodory formulation of derivative at a point\<close>
lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*)
--- a/src/HOL/Limits.thy Fri Jun 10 16:28:48 2016 +0200
+++ b/src/HOL/Limits.thy Fri Jun 10 16:36:24 2016 +0200
@@ -1509,6 +1509,67 @@
qed simp
+subsection \<open>Floor and Ceiling\<close>
+
+lemma eventually_floor_less:
+ fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
+ assumes f: "(f \<longlongrightarrow> l) F"
+ assumes l: "l \<notin> \<int>"
+ shows "\<forall>\<^sub>F x in F. of_int (floor l) < f x"
+ by (intro order_tendstoD[OF f]) (metis Ints_of_int antisym_conv2 floor_correct l)
+
+lemma eventually_less_ceiling:
+ fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
+ assumes f: "(f \<longlongrightarrow> l) F"
+ assumes l: "l \<notin> \<int>"
+ shows "\<forall>\<^sub>F x in F. f x < of_int (ceiling l)"
+ by (intro order_tendstoD[OF f]) (metis Ints_of_int l le_of_int_ceiling less_le)
+
+lemma eventually_floor_eq:
+ fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
+ assumes f: "(f \<longlongrightarrow> l) F"
+ assumes l: "l \<notin> \<int>"
+ shows "\<forall>\<^sub>F x in F. floor (f x) = floor l"
+ using eventually_floor_less[OF assms] eventually_less_ceiling[OF assms]
+ by eventually_elim (meson floor_less_iff less_ceiling_iff not_less_iff_gr_or_eq)
+
+lemma eventually_ceiling_eq:
+ fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
+ assumes f: "(f \<longlongrightarrow> l) F"
+ assumes l: "l \<notin> \<int>"
+ shows "\<forall>\<^sub>F x in F. ceiling (f x) = ceiling l"
+ using eventually_floor_less[OF assms] eventually_less_ceiling[OF assms]
+ by eventually_elim (meson floor_less_iff less_ceiling_iff not_less_iff_gr_or_eq)
+
+lemma tendsto_of_int_floor:
+ fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
+ assumes "(f \<longlongrightarrow> l) F"
+ assumes "l \<notin> \<int>"
+ shows "((\<lambda>x. of_int (floor (f x))::'c::{ring_1, topological_space}) \<longlongrightarrow> of_int (floor l)) F"
+ using eventually_floor_eq[OF assms]
+ by (simp add: eventually_mono topological_tendstoI)
+
+lemma tendsto_of_int_ceiling:
+ fixes f::"'a \<Rightarrow> 'b::{order_topology, floor_ceiling}"
+ assumes "(f \<longlongrightarrow> l) F"
+ assumes "l \<notin> \<int>"
+ shows "((\<lambda>x. of_int (ceiling (f x))::'c::{ring_1, topological_space}) \<longlongrightarrow> of_int (ceiling l)) F"
+ using eventually_ceiling_eq[OF assms]
+ by (simp add: eventually_mono topological_tendstoI)
+
+lemma continuous_on_of_int_floor:
+ "continuous_on (UNIV - \<int>::'a::{order_topology, floor_ceiling} set)
+ (\<lambda>x. of_int (floor x)::'b::{ring_1, topological_space})"
+ unfolding continuous_on_def
+ by (auto intro!: tendsto_of_int_floor)
+
+lemma continuous_on_of_int_ceiling:
+ "continuous_on (UNIV - \<int>::'a::{order_topology, floor_ceiling} set)
+ (\<lambda>x. of_int (ceiling x)::'b::{ring_1, topological_space})"
+ unfolding continuous_on_def
+ by (auto intro!: tendsto_of_int_ceiling)
+
+
subsection \<open>Limits of Sequences\<close>
lemma [trans]: "X = Y \<Longrightarrow> Y \<longlonglongrightarrow> z \<Longrightarrow> X \<longlonglongrightarrow> z"
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Fri Jun 10 16:28:48 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Fri Jun 10 16:36:24 2016 +0200
@@ -6289,13 +6289,13 @@
obtain B where B: "\<And>x. B \<le> cmod x \<Longrightarrow> norm (f x) * 2 < cmod (f z)"
by (auto simp: dist_norm)
define R where "R = 1 + \<bar>B\<bar> + norm z"
- have "R > 0" unfolding R_def
+ have "R > 0" unfolding R_def
proof -
have "0 \<le> cmod z + \<bar>B\<bar>"
by (metis (full_types) add_nonneg_nonneg norm_ge_zero real_norm_def)
then show "0 < 1 + \<bar>B\<bar> + cmod z"
by linarith
- qed
+ qed
have *: "((\<lambda>u. f u / (u - z)) has_contour_integral 2 * complex_of_real pi * \<i> * f z) (circlepath z R)"
apply (rule Cauchy_integral_circlepath)
using \<open>R > 0\<close> apply (auto intro: holomorphic_on_subset [OF holf] holomorphic_on_imp_continuous_on)+
--- a/src/HOL/Multivariate_Analysis/Polytope.thy Fri Jun 10 16:28:48 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Polytope.thy Fri Jun 10 16:36:24 2016 +0200
@@ -2163,32 +2163,7 @@
fixes S :: "'a :: euclidean_space set"
assumes "polyhedron S" "c face_of S"
shows "polyhedron c"
-proof -
- obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
- and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
- and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
- using assms by (simp add: polyhedron_Int_affine_minimal) meson
- then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
- by metis
- show ?thesis
- proof (cases "c = {} \<or> c = S")
- case True with assms show ?thesis
- by auto
- next
- case False
- let ?ab = "\<lambda>h. {x. a h \<bullet> x = b h}"
- have "{S \<inter> ?ab h |h. h \<in> F \<and> c \<subseteq> S \<inter> ?ab h} \<subseteq> {S \<inter> ?ab h |h. h \<in> F}"
- by blast
- then have fin: "finite ({S \<inter> ?ab h |h. h \<in> F \<and> c \<subseteq> S \<inter> ?ab h})"
- by (rule finite_subset) (simp add: \<open>finite F\<close>)
- then have "polyhedron (\<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> c \<subseteq> S \<inter> ?ab h})"
- by (auto simp: \<open>polyhedron S\<close> polyhedron_hyperplane)
- with False show ?thesis
- using face_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min] assms
- by auto
- qed
-qed
-
+by (metis assms face_of_imp_eq_affine_Int polyhedron_Int polyhedron_affine_hull polyhedron_imp_closed polyhedron_imp_convex)
lemma finite_polyhedron_faces:
fixes S :: "'a :: euclidean_space set"
--- a/src/HOL/Probability/Lebesgue_Measure.thy Fri Jun 10 16:28:48 2016 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Fri Jun 10 16:36:24 2016 +0200
@@ -526,11 +526,12 @@
shows "emeasure lborel A = 0"
proof -
have "A \<subseteq> (\<Union>i. {from_nat_into A i})" using from_nat_into_surj assms by force
- moreover have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0"
+ then have "emeasure lborel A \<le> emeasure lborel (\<Union>i. {from_nat_into A i})"
+ by (intro emeasure_mono) auto
+ also have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0"
by (rule emeasure_UN_eq_0) auto
- ultimately have "emeasure lborel A \<le> 0" using emeasure_mono
- by (smt UN_E emeasure_empty equalityI from_nat_into order_refl singletonD subsetI)
- thus ?thesis by (auto simp add: )
+ finally show ?thesis
+ by (auto simp add: )
qed
lemma countable_imp_null_set_lborel: "countable A \<Longrightarrow> A \<in> null_sets lborel"
--- a/src/Provers/blast.ML Fri Jun 10 16:28:48 2016 +0200
+++ b/src/Provers/blast.ML Fri Jun 10 16:36:24 2016 +0200
@@ -29,7 +29,7 @@
the formulae get into the wrong order (see WRONG below).
With substition for equalities (hyp_subst_tac):
- When substitution affects an unsage formula or literal, it is moved
+ When substitution affects an unsafe formula or literal, it is moved
back to the list of safe formulae.
But there's no way of putting it in the right place. A "moved" or
"no DETERM" flag would prevent proofs failing here.
@@ -82,7 +82,7 @@
datatype term =
- Const of string * term list (*typargs constant--as a terms!*)
+ Const of string * term list (*typargs constant--as a term!*)
| Skolem of string * term option Unsynchronized.ref list
| Free of string
| Var of term option Unsynchronized.ref
@@ -110,15 +110,15 @@
nclosed: int Unsynchronized.ref,
ntried: int Unsynchronized.ref}
-fun reject_const thy c =
+fun reserved_const thy c =
is_some (Sign.const_type thy c) andalso
- error ("blast: theory contains illegal constant " ^ quote c);
+ error ("blast: theory contains reserved constant " ^ quote c);
fun initialize ctxt =
let
val thy = Proof_Context.theory_of ctxt;
- val _ = reject_const thy "*Goal*";
- val _ = reject_const thy "*False*";
+ val _ = reserved_const thy "*Goal*";
+ val _ = reserved_const thy "*False*";
in
State
{ctxt = ctxt,
@@ -558,6 +558,10 @@
| toTerm d (Abs(a,_)) = dummyVar
| toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u);
+(*Too flexible assertions or goals. Motivated by examples such as "(\<And>P. ~P) \<Longrightarrow> 0==1"*)
+fun isVarForm (Var _) = true
+ | isVarForm (Const (c, _) $ Var _) = (c = Data.not_name)
+ | isVarForm _ = false;
fun netMkRules state P vars (nps: Classical.netpair list) =
case P of
@@ -566,6 +570,8 @@
val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
in map (fromIntrRule state vars o #2) (order_list intrs) end
| _ =>
+ if isVarForm P then [] (*The formula is too flexible, reject*)
+ else
let val pP = mk_Trueprop (toTerm 3 P)
val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
in map_filter (fromRule state vars o #2) (order_list elims) end;