merged
authorhaftmann
Wed Sep 23 13:42:53 2009 +0200 (2009-09-23)
changeset 326537feb35deb6f6
parent 32652 3175e23b79f3
parent 32651 af55ccf865a4
child 32654 5f9127407430
child 32657 5f13912245ff
merged
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 23 12:03:47 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 23 13:42:53 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 12:03:47 2009 +0200
     2.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Wed Sep 23 13:42:53 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 12:03:47 2009 +0200
     3.2 +++ b/src/HOL/Lim.thy	Wed Sep 23 13:42:53 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"
     5.1 --- a/src/Pure/envir.ML	Wed Sep 23 12:03:47 2009 +0200
     5.2 +++ b/src/Pure/envir.ML	Wed Sep 23 13:42:53 2009 +0200
     5.3 @@ -282,12 +282,9 @@
     5.4    let
     5.5      val funerr = "fastype: expected function type";
     5.6      fun fast Ts (f $ u) =
     5.7 -          (case fast Ts f of
     5.8 +          (case Type.devar tyenv (fast Ts f) of
     5.9              Type ("fun", [_, T]) => T
    5.10 -          | TVar v =>
    5.11 -              (case Type.lookup tyenv v of
    5.12 -                SOME (Type ("fun", [_, T])) => T
    5.13 -              | _ => raise TERM (funerr, [f $ u]))
    5.14 +          | TVar v => raise TERM (funerr, [f $ u])
    5.15            | _ => raise TERM (funerr, [f $ u]))
    5.16        | fast Ts (Const (_, T)) = T
    5.17        | fast Ts (Free (_, T)) = T
     6.1 --- a/src/Pure/type.ML	Wed Sep 23 12:03:47 2009 +0200
     6.2 +++ b/src/Pure/type.ML	Wed Sep 23 13:42:53 2009 +0200
     6.3 @@ -55,6 +55,7 @@
     6.4    exception TYPE_MATCH
     6.5    type tyenv = (sort * typ) Vartab.table
     6.6    val lookup: tyenv -> indexname * sort -> typ option
     6.7 +  val devar: tyenv -> typ -> typ
     6.8    val typ_match: tsig -> typ * typ -> tyenv -> tyenv
     6.9    val typ_instance: tsig -> typ * typ -> bool
    6.10    val raw_match: typ * typ -> tyenv -> tyenv