correct variable order in approximate-method
authorhoelzl
Wed Sep 23 13:17:17 2009 +0200 (2009-09-23)
changeset 3265034bfa2492298
parent 32649 442e03154ee6
child 32651 af55ccf865a4
correct variable order in approximate-method
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/ex/Approximation_Ex.thy
src/HOL/Lim.thy
src/HOL/Statespace/state_space.ML
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 23 11:06:32 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 23 13:17:17 2009 +0200
     1.3 @@ -3246,12 +3246,13 @@
     1.4          = map (` (variable_of_bound o prop_of)) prems
     1.5  
     1.6        fun add_deps (name, bnds)
     1.7 -        = Graph.add_deps_acyclic
     1.8 -            (name, remove (op =) name (Term.add_free_names (prop_of bnds) []))
     1.9 +        = Graph.add_deps_acyclic (name,
    1.10 +            remove (op =) name (Term.add_free_names (prop_of bnds) []))
    1.11 +
    1.12        val order = Graph.empty
    1.13                    |> fold Graph.new_node variable_bounds
    1.14                    |> fold add_deps variable_bounds
    1.15 -                  |> Graph.topological_order |> rev
    1.16 +                  |> Graph.strong_conn |> map the_single |> rev
    1.17                    |> map_filter (AList.lookup (op =) variable_bounds)
    1.18  
    1.19        fun prepend_prem th tac
    1.20 @@ -3338,7 +3339,7 @@
    1.21                        etac @{thm meta_eqE},
    1.22                        rtac @{thm impI}] i)
    1.23        THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
    1.24 -      THEN TRY (filter_prems_tac (K false) i)
    1.25 +      THEN DETERM (TRY (filter_prems_tac (K false) i))
    1.26        THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
    1.27        THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
    1.28        THEN gen_eval_tac eval_oracle ctxt i))
    1.29 @@ -3350,7 +3351,7 @@
    1.30  
    1.31    fun mk_approx' prec t = (@{const "approx'"}
    1.32                           $ HOLogic.mk_number @{typ nat} prec
    1.33 -                         $ t $ @{term "[] :: (float * float) list"})
    1.34 +                         $ t $ @{term "[] :: (float * float) option list"})
    1.35  
    1.36    fun dest_result (Const (@{const_name "Some"}, _) $
    1.37                     ((Const (@{const_name "Pair"}, _)) $
     2.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Sep 23 11:06:32 2009 +0100
     2.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Sep 23 13:17:17 2009 +0200
     2.3 @@ -72,7 +72,9 @@
     2.4    shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
     2.5    using assms by (approximation 80)
     2.6  
     2.7 -lemma "\<phi> \<in> { 0 .. 1 :: real } \<longrightarrow> \<phi> ^ 2 \<le> \<phi>"
     2.8 -  by (approximation 30 splitting: \<phi>=1 taylor: \<phi> = 3)
     2.9 +lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x ^ 2 \<le> x"
    2.10 +  by (approximation 30 splitting: x=1 taylor: x = 3)
    2.11 +
    2.12 +value [approximate] "10"
    2.13  
    2.14  end
     3.1 --- a/src/HOL/Lim.thy	Wed Sep 23 11:06:32 2009 +0100
     3.2 +++ b/src/HOL/Lim.thy	Wed Sep 23 13:17:17 2009 +0200
     3.3 @@ -84,6 +84,8 @@
     3.4  lemma LIM_const [simp]: "(%x. k) -- x --> k"
     3.5  by (simp add: LIM_def)
     3.6  
     3.7 +lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
     3.8 +
     3.9  lemma LIM_add:
    3.10    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    3.11    assumes f: "f -- a --> L" and g: "g -- a --> M"
     4.1 --- a/src/HOL/Statespace/state_space.ML	Wed Sep 23 11:06:32 2009 +0100
     4.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Sep 23 13:17:17 2009 +0200
     4.3 @@ -321,14 +321,17 @@
     4.4       |> interprete_parent name dist_thm_full_name parent_expr
     4.5    end;
     4.6  
     4.7 -fun encode_dot x = if x= #"." then #"_" else x;
     4.8 +fun encode_dot x =
     4.9 +    if x= #"." then #"_" else x;
    4.10  
    4.11  fun encode_type (TFree (s, _)) = s
    4.12    | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i
    4.13    | encode_type (Type (n,Ts)) =
    4.14        let
    4.15          val Ts' = fold1' (fn x => fn y => x ^ "_" ^ y) (map encode_type Ts) "";
    4.16 -        val n' = String.map encode_dot n;
    4.17 +        val n' = if n = "*" then "Prod" else
    4.18 +                   if n = "+" then "Sum" else
    4.19 +                     String.map encode_dot n;
    4.20        in if Ts'="" then n' else Ts' ^ "_" ^ n' end;
    4.21  
    4.22  fun project_name T = projectN ^"_"^encode_type T;
    4.23 @@ -692,4 +695,4 @@
    4.24  
    4.25  end;
    4.26  
    4.27 -end;
    4.28 \ No newline at end of file
    4.29 +end;