--- a/src/HOL/Decision_Procs/Approximation.thy Wed Sep 23 12:03:47 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Sep 23 13:42:53 2009 +0200
@@ -3246,12 +3246,13 @@
= map (` (variable_of_bound o prop_of)) prems
fun add_deps (name, bnds)
- = Graph.add_deps_acyclic
- (name, remove (op =) name (Term.add_free_names (prop_of bnds) []))
+ = Graph.add_deps_acyclic (name,
+ remove (op =) name (Term.add_free_names (prop_of bnds) []))
+
val order = Graph.empty
|> fold Graph.new_node variable_bounds
|> fold add_deps variable_bounds
- |> Graph.topological_order |> rev
+ |> Graph.strong_conn |> map the_single |> rev
|> map_filter (AList.lookup (op =) variable_bounds)
fun prepend_prem th tac
@@ -3338,7 +3339,7 @@
etac @{thm meta_eqE},
rtac @{thm impI}] i)
THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
- THEN TRY (filter_prems_tac (K false) i)
+ THEN DETERM (TRY (filter_prems_tac (K false) i))
THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
THEN gen_eval_tac eval_oracle ctxt i))
@@ -3350,7 +3351,7 @@
fun mk_approx' prec t = (@{const "approx'"}
$ HOLogic.mk_number @{typ nat} prec
- $ t $ @{term "[] :: (float * float) list"})
+ $ t $ @{term "[] :: (float * float) option list"})
fun dest_result (Const (@{const_name "Some"}, _) $
((Const (@{const_name "Pair"}, _)) $
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Wed Sep 23 12:03:47 2009 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Wed Sep 23 13:42:53 2009 +0200
@@ -72,7 +72,9 @@
shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
using assms by (approximation 80)
-lemma "\<phi> \<in> { 0 .. 1 :: real } \<longrightarrow> \<phi> ^ 2 \<le> \<phi>"
- by (approximation 30 splitting: \<phi>=1 taylor: \<phi> = 3)
+lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x ^ 2 \<le> x"
+ by (approximation 30 splitting: x=1 taylor: x = 3)
+
+value [approximate] "10"
end
--- a/src/HOL/Lim.thy Wed Sep 23 12:03:47 2009 +0200
+++ b/src/HOL/Lim.thy Wed Sep 23 13:42:53 2009 +0200
@@ -84,6 +84,8 @@
lemma LIM_const [simp]: "(%x. k) -- x --> k"
by (simp add: LIM_def)
+lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
+
lemma LIM_add:
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
assumes f: "f -- a --> L" and g: "g -- a --> M"
--- a/src/Pure/envir.ML Wed Sep 23 12:03:47 2009 +0200
+++ b/src/Pure/envir.ML Wed Sep 23 13:42:53 2009 +0200
@@ -282,12 +282,9 @@
let
val funerr = "fastype: expected function type";
fun fast Ts (f $ u) =
- (case fast Ts f of
+ (case Type.devar tyenv (fast Ts f) of
Type ("fun", [_, T]) => T
- | TVar v =>
- (case Type.lookup tyenv v of
- SOME (Type ("fun", [_, T])) => T
- | _ => raise TERM (funerr, [f $ u]))
+ | TVar v => raise TERM (funerr, [f $ u])
| _ => raise TERM (funerr, [f $ u]))
| fast Ts (Const (_, T)) = T
| fast Ts (Free (_, T)) = T
--- a/src/Pure/type.ML Wed Sep 23 12:03:47 2009 +0200
+++ b/src/Pure/type.ML Wed Sep 23 13:42:53 2009 +0200
@@ -55,6 +55,7 @@
exception TYPE_MATCH
type tyenv = (sort * typ) Vartab.table
val lookup: tyenv -> indexname * sort -> typ option
+ val devar: tyenv -> typ -> typ
val typ_match: tsig -> typ * typ -> tyenv -> tyenv
val typ_instance: tsig -> typ * typ -> bool
val raw_match: typ * typ -> tyenv -> tyenv