# HG changeset patch
# User hoelzl
# Date 1253704637 -7200
# Node ID 34bfa2492298b709a4aa52b49e765ee2e3ded997
# Parent  442e03154ee6f4d857cf5a57a140094086feab18
correct variable order in approximate-method

diff -r 442e03154ee6 -r 34bfa2492298 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 23 11:06:32 2009 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 23 13:17:17 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 442e03154ee6 -r 34bfa2492298 src/HOL/Decision_Procs/ex/Approximation_Ex.thy
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Sep 23 11:06:32 2009 +0100
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Sep 23 13:17:17 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 442e03154ee6 -r 34bfa2492298 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Wed Sep 23 11:06:32 2009 +0100
+++ b/src/HOL/Lim.thy	Wed Sep 23 13:17:17 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 442e03154ee6 -r 34bfa2492298 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Sep 23 11:06:32 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Wed Sep 23 13:17:17 2009 +0200
@@ -321,14 +321,17 @@
      |> interprete_parent name dist_thm_full_name parent_expr
   end;
 
-fun encode_dot x = if x= #"." then #"_" else x;
+fun encode_dot x =
+    if x= #"." then #"_" else x;
 
 fun encode_type (TFree (s, _)) = s
   | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i
   | encode_type (Type (n,Ts)) =
       let
         val Ts' = fold1' (fn x => fn y => x ^ "_" ^ y) (map encode_type Ts) "";
-        val n' = String.map encode_dot n;
+        val n' = if n = "*" then "Prod" else
+                   if n = "+" then "Sum" else
+                     String.map encode_dot n;
       in if Ts'="" then n' else Ts' ^ "_" ^ n' end;
 
 fun project_name T = projectN ^"_"^encode_type T;
@@ -692,4 +695,4 @@
 
 end;
 
-end;
\ No newline at end of file
+end;