--- 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"}, _)) $
--- 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
--- 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"
--- 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;