# HG changeset patch
# User haftmann
# Date 1253706173 -7200
# Node ID 7feb35deb6f647013174809d70f61bde741d8d70
# Parent  3175e23b79f3b5ce41c9d004e11c4277f1e496c6# Parent  af55ccf865a49f059f4709840bbf823f6cc43af7
merged

diff -r 3175e23b79f3 -r 7feb35deb6f6 src/HOL/Decision_Procs/Approximation.thy
--- 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"}, _)) $
diff -r 3175e23b79f3 -r 7feb35deb6f6 src/HOL/Decision_Procs/ex/Approximation_Ex.thy
--- 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
diff -r 3175e23b79f3 -r 7feb35deb6f6 src/HOL/Lim.thy
--- 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"
diff -r 3175e23b79f3 -r 7feb35deb6f6 src/HOL/Statespace/state_space.ML
diff -r 3175e23b79f3 -r 7feb35deb6f6 src/Pure/envir.ML
--- 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
diff -r 3175e23b79f3 -r 7feb35deb6f6 src/Pure/type.ML
--- 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