(* Title: HOL/Decision_Procs/approximation.ML Author: Johannes Hoelzl, TU Muenchen
*)
signature APPROXIMATION = sig val reify_form: Proof.context -> term -> term val approx: int -> Proof.context -> term -> term val approximate: Proof.context -> term -> term val approximation_tac : int -> (string * int) list -> int option -> Proof.context -> int -> tactic end
structure Approximation = struct
fun reorder_bounds_tac ctxt prems i = let fun variable_of_bound \<^Const_>\<open>Trueprop for \<^Const_>\<open>Set.member _ for \<open>Free (name, _)\<close> _\<close>\<close> = name
| variable_of_bound \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for \<open>Free (name, _)\<close> _\<close>\<close> = name
| variable_of_bound t = raise TERM ("variable_of_bound", [t])
val variable_bounds
= map (`(variable_of_bound o Thm.prop_of)) prems
fun add_deps (name, bnds)
= Graph.add_deps_acyclic (name,
remove (op =) name (Term.add_free_names (Thm.prop_of bnds) []))
fun prepend_prem th tac =
tac THEN resolve_tac ctxt [th RSN (2, @{thm mp})] i in
fold prepend_prem order all_tac end
fun approximate ctxt t = case fastype_of t of \<^Type>\<open>bool\<close> =>
Approximation_Computation.approx_bool ctxt t
| \<^typ>\<open>float interval option\<close> =>
Approximation_Computation.approx_arith ctxt t
| \<^typ>\<open>float interval optionlist\<close> =>
Approximation_Computation.approx_form_eval ctxt t
| _ => error ("Bad term: " ^ Syntax.string_of_term ctxt t);
fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let fun lookup_splitting (Free (name, _)) =
(case AList.lookup (op =) splitting name of SOME s => HOLogic.mk_number \<^Type>\<open>nat\<close> s
| NONE => \<^term>\<open>0 :: nat\<close>)
| lookup_splitting t = raise TERM ("lookup_splitting", [t]) val vs = nth (Thm.prems_of st) (i - 1)
|> Logic.strip_imp_concl
|> HOLogic.dest_Trueprop
|> Term.strip_comb |> snd |> List.last
|> HOLogic.dest_list val p = prec
|> HOLogic.mk_number \<^Type>\<open>nat\<close>
|> Thm.cterm_of ctxt incase taylor of NONE => let val n = vs |> length
|> HOLogic.mk_number \<^Type>\<open>nat\<close>
|> Thm.cterm_of ctxt val ss = vs
|> map lookup_splitting
|> HOLogic.mk_list \<^Type>\<open>nat\<close>
|> Thm.cterm_of ctxt in
(resolve_tac ctxt [
\<^instantiate>\<open>n and prec = p and ss in
lemma (schematic)
\<open>n = length xs \<Longrightarrow> approx_form prec f (replicate n None) ss \<Longrightarrow> interpret_form f xs\<close>
by (rule approx_form)\<close>] i THEN simp_tac (put_simpset (simpset_of \<^context>) ctxt) i) st end
| SOME t => if length vs <> 1 thenraise (TERM ("More than one variable used for taylor series expansion", [Thm.prop_of st])) elselet val t = t
|> HOLogic.mk_number \<^Type>\<open>nat\<close>
|> Thm.cterm_of ctxt val s = vs |> map lookup_splitting |> hd
|> Thm.cterm_of ctxt in
resolve_tac ctxt [
\<^instantiate>\<open>s and t and prec = p in
lemma (schematic) "approx_tse_form prec t s f \ interpret_form f [x]"
by (rule approx_tse_form)\<close>] i st end end
fun calculated_subterms \<^Const_>\<open>Trueprop for t\<close> = calculated_subterms t
| calculated_subterms \<^Const_>\<open>implies for _ t\<close> = calculated_subterms t
| calculated_subterms \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close> = [t1, t2]
| calculated_subterms \<^Const_>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close> = [t1, t2]
| calculated_subterms \<^Const_>\<open>Set.member \<^Type>\<open>real\<close> for
t1 \<^Const_>\<open>atLeastAtMost \<^Type>\<open>real\<close> for t2 t3\<close>\<close> = [t1, t2, t3]
| calculated_subterms t = raise TERM ("calculated_subterms", [t])
fun dest_interpret_form \<^Const_>\<open>interpret_form for b xs\<close> = (b, xs)
| dest_interpret_form t = raise TERM ("dest_interpret_form", [t])
fun dest_interpret \<^Const_>\<open>interpret_floatarith for b xs\<close> = (b, xs)
| dest_interpret t = raise TERM ("dest_interpret", [t])
fun dest_interpret_env \<^Const_>\<open>interpret_form for _ xs\<close> = xs
| dest_interpret_env \<^Const_>\<open>interpret_floatarith for _ xs\<close> = xs
| dest_interpret_env t = raise TERM ("dest_interpret_env", [t])
fun dest_float \<^Const_>\<open>Float for m e\<close> = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
| dest_float t = raise TERM ("dest_float", [t])
fun dest_ivl \<^Const_>\<open>Some _ for \<^Const_>\<open>Interval _ for \<^Const_>\<open>Pair _ _ for u l\<close>\<close>\<close> =
SOME (dest_float u, dest_float l)
| dest_ivl \<^Const_>\<open>None _\<close> = NONE
| dest_ivl t = raise TERM ("dest_result", [t])
fun mk_approx' prec t =
\<^Const>\<open>approx' for \HOLogic.mk_number \<^Type>\nat\ prec\ t \<^Const>\Nil \<^typ>\float interval option\\\
fun mk_approx_form_eval prec t xs =
\<^Const>\<open>approx_form_eval for \<open>HOLogic.mk_number \<^Type>\<open>nat\<close> prec\<close> t xs\<close>
fun float2_float10 prec round_down (m, e) = ( let val (m, e) = (if e < 0 then (m,e) else (m * Integer.pow e 2, 0))
fun frac _ _ 0 digits cnt = (digits, cnt, 0)
| frac _ 0 r digits cnt = (digits, cnt, r)
| frac c p r digits cnt = (let val (d, r) = Integer.div_mod (r * 10) (Integer.pow (~e) 2) in frac (c orelse d <> 0) (if d <> 0 orelse c then p - 1 else p) r
(digits * 10 + d) (cnt + 1) end)
val sgn = Int.sign m val m = abs m
val round_down = (sgn = 1 andalso round_down) orelse
(sgn = ~1 andalso not round_down)
val (x, r) = Integer.div_mod m (Integer.pow (~e) 2)
val p = ((if x = 0 then prec else prec - (Integer.log2 x + 1)) * 3) div 10 + 1
val (digits, e10, r) = if p > 0 then frac (x <> 0) p r 0 0 else (0,0,0)
val digits = if round_down orelse r = 0 then digits else digits + 1
in (sgn * (digits + x * (Integer.pow e10 10)), ~e10) end)
fun mk_result prec (SOME (l, u)) =
(let fun mk_float10 rnd x = (letval (m, e) = float2_float10 prec rnd x inif e = 0 then HOLogic.mk_number \<^Type>\<open>real\<close> m elseif e = 1 then \<^Const>\<open>divide \<^Type>\<open>real\<close>\<close> $
HOLogic.mk_number \<^Type>\<open>real\<close> m $
\<^term>\<open>10\<close> else \<^Const>\<open>divide \<^Type>\<open>real\<close>\<close> $
HOLogic.mk_number \<^Type>\<open>real\<close> m $
(\<^term>\<open>power 10 :: nat \<Rightarrow> real\<close> $
HOLogic.mk_number \<^Type>\<open>nat\<close> (~e)) end) in \<^Const>\<open>atLeastAtMost \<^Type>\<open>real\<close> for \<open>mk_float10 true l\<close> \<open>mk_float10 false u\<close>\<close> end)
| mk_result _ NONE = \<^term>\<open>UNIV :: real set\<close>
fun realify t = let val t = Logic.varify_global t val m = map (fn (name, _) => (name, \<^Type>\<open>real\<close>)) (Term.add_tvars t []) val t = Term.subst_TVars m t in t end
fun apply_tactic ctxt term tactic =
Thm.cterm_of ctxt term
|> Goal.init
|> SINGLE tactic
|> the |> Thm.prems_of |> hd
fun approx prec ctxt t = if type_of t = \<^Type>\<open>prop\<close> then approx_form prec ctxt t elseif type_of t = \<^Type>\<open>bool\<close> then approx_form prec ctxt \<^Const>\<open>Trueprop for t\<close> else approx_arith prec ctxt t
fun approximate_cmd modes raw_t state = let val ctxt = Toplevel.context_of state; val t = Syntax.read_term ctxt raw_t; val t' = approx 30 ctxt t; val ty' = Term.type_of t'; val ctxt' = Proof_Context.augment t' ctxt; in
Print_Mode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) () end |> Pretty.writeln;
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
