author | wenzelm |
Mon, 22 Dec 2014 15:50:16 +0100 | |
changeset 59174 | 15a73dd9df51 |
parent 58893 | 9e0ecb66d6a7 |
child 59498 | 50b60f501b05 |
permissions | -rw-r--r-- |
56813 | 1 |
(* Title: HOL/Decision_Procs/approximation.ML |
2 |
Author: Johannes Hoelzl, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
signature APPROXIMATION = |
|
6 |
sig |
|
7 |
val approx: int -> Proof.context -> term -> term |
|
8 |
end |
|
9 |
||
10 |
structure Approximation: APPROXIMATION = |
|
11 |
struct |
|
12 |
||
13 |
fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t |
|
14 |
| calculated_subterms (@{const HOL.implies} $ _ $ t) = calculated_subterms t |
|
15 |
| calculated_subterms (@{term "op <= :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2] |
|
16 |
| calculated_subterms (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2] |
|
17 |
| calculated_subterms (@{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ t1 $ |
|
18 |
(@{term "atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set"} $ t2 $ t3)) = [t1, t2, t3] |
|
19 |
| calculated_subterms t = raise TERM ("calculated_subterms", [t]) |
|
20 |
||
21 |
fun dest_interpret_form (@{const "interpret_form"} $ b $ xs) = (b, xs) |
|
22 |
| dest_interpret_form t = raise TERM ("dest_interpret_form", [t]) |
|
23 |
||
24 |
fun dest_interpret (@{const "interpret_floatarith"} $ b $ xs) = (b, xs) |
|
25 |
| dest_interpret t = raise TERM ("dest_interpret", [t]) |
|
26 |
||
27 |
||
28 |
fun dest_float (@{const "Float"} $ m $ e) = |
|
29 |
(snd (HOLogic.dest_number m), snd (HOLogic.dest_number e)) |
|
30 |
||
31 |
fun dest_ivl (Const (@{const_name "Some"}, _) $ |
|
32 |
(Const (@{const_name Pair}, _) $ u $ l)) = SOME (dest_float u, dest_float l) |
|
33 |
| dest_ivl (Const (@{const_name "None"}, _)) = NONE |
|
34 |
| dest_ivl t = raise TERM ("dest_result", [t]) |
|
35 |
||
36 |
fun mk_approx' prec t = (@{const "approx'"} |
|
37 |
$ HOLogic.mk_number @{typ nat} prec |
|
38 |
$ t $ @{term "[] :: (float * float) option list"}) |
|
39 |
||
40 |
fun mk_approx_form_eval prec t xs = (@{const "approx_form_eval"} |
|
41 |
$ HOLogic.mk_number @{typ nat} prec |
|
42 |
$ t $ xs) |
|
43 |
||
44 |
fun float2_float10 prec round_down (m, e) = ( |
|
45 |
let |
|
46 |
val (m, e) = (if e < 0 then (m,e) else (m * Integer.pow e 2, 0)) |
|
47 |
||
48 |
fun frac c p 0 digits cnt = (digits, cnt, 0) |
|
49 |
| frac c 0 r digits cnt = (digits, cnt, r) |
|
50 |
| frac c p r digits cnt = (let |
|
51 |
val (d, r) = Integer.div_mod (r * 10) (Integer.pow (~e) 2) |
|
52 |
in frac (c orelse d <> 0) (if d <> 0 orelse c then p - 1 else p) r |
|
53 |
(digits * 10 + d) (cnt + 1) |
|
54 |
end) |
|
55 |
||
56 |
val sgn = Int.sign m |
|
57 |
val m = abs m |
|
58 |
||
59 |
val round_down = (sgn = 1 andalso round_down) orelse |
|
60 |
(sgn = ~1 andalso not round_down) |
|
61 |
||
62 |
val (x, r) = Integer.div_mod m (Integer.pow (~e) 2) |
|
63 |
||
64 |
val p = ((if x = 0 then prec else prec - (IntInf.log2 x + 1)) * 3) div 10 + 1 |
|
65 |
||
66 |
val (digits, e10, r) = if p > 0 then frac (x <> 0) p r 0 0 else (0,0,0) |
|
67 |
||
68 |
val digits = if round_down orelse r = 0 then digits else digits + 1 |
|
69 |
||
70 |
in (sgn * (digits + x * (Integer.pow e10 10)), ~e10) |
|
71 |
end) |
|
72 |
||
73 |
fun mk_result prec (SOME (l, u)) = |
|
74 |
(let |
|
75 |
fun mk_float10 rnd x = (let val (m, e) = float2_float10 prec rnd x |
|
76 |
in if e = 0 then HOLogic.mk_number @{typ real} m |
|
77 |
else if e = 1 then @{term "divide :: real \<Rightarrow> real \<Rightarrow> real"} $ |
|
78 |
HOLogic.mk_number @{typ real} m $ |
|
79 |
@{term "10"} |
|
80 |
else @{term "divide :: real \<Rightarrow> real \<Rightarrow> real"} $ |
|
81 |
HOLogic.mk_number @{typ real} m $ |
|
82 |
(@{term "power 10 :: nat \<Rightarrow> real"} $ |
|
83 |
HOLogic.mk_number @{typ nat} (~e)) end) |
|
84 |
in @{term "atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set"} $ mk_float10 true l $ mk_float10 false u end) |
|
85 |
| mk_result _ NONE = @{term "UNIV :: real set"} |
|
86 |
||
87 |
fun realify t = |
|
88 |
let |
|
89 |
val t = Logic.varify_global t |
|
90 |
val m = map (fn (name, _) => (name, @{typ real})) (Term.add_tvars t []) |
|
91 |
val t = Term.subst_TVars m t |
|
92 |
in t end |
|
93 |
||
94 |
fun apply_tactic ctxt term tactic = |
|
95 |
cterm_of (Proof_Context.theory_of ctxt) term |
|
96 |
|> Goal.init |
|
97 |
|> SINGLE tactic |
|
98 |
|> the |> prems_of |> hd |
|
99 |
||
100 |
fun prepare_form ctxt term = apply_tactic ctxt term ( |
|
101 |
REPEAT (FIRST' [etac @{thm intervalE}, etac @{thm meta_eqE}, rtac @{thm impI}] 1) |
|
102 |
THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems 1) ctxt 1 |
|
103 |
THEN DETERM (TRY (filter_prems_tac (K false) 1))) |
|
104 |
||
105 |
fun reify_form ctxt term = apply_tactic ctxt term |
|
106 |
(Reification.tac ctxt form_equations NONE 1) |
|
107 |
||
108 |
fun approx_form prec ctxt t = |
|
109 |
realify t |
|
110 |
|> prepare_form ctxt |
|
111 |
|> (fn arith_term => reify_form ctxt arith_term |
|
112 |
|> HOLogic.dest_Trueprop |> dest_interpret_form |
|
113 |
|> (fn (data, xs) => |
|
114 |
mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"} |
|
115 |
(map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs))) |
|
116 |
|> approximate ctxt |
|
117 |
|> HOLogic.dest_list |
|
118 |
|> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term) |
|
119 |
|> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s)) |
|
120 |
|> foldr1 HOLogic.mk_conj)) |
|
121 |
||
122 |
fun approx_arith prec ctxt t = realify t |
|
123 |
|> Thm.cterm_of (Proof_Context.theory_of ctxt) |
|
124 |
|> Reification.conv ctxt form_equations |
|
125 |
|> prop_of |
|
126 |
|> Logic.dest_equals |> snd |
|
127 |
|> dest_interpret |> fst |
|
128 |
|> mk_approx' prec |
|
129 |
|> approximate ctxt |
|
130 |
|> dest_ivl |
|
131 |
|> mk_result prec |
|
132 |
||
133 |
fun approx prec ctxt t = |
|
134 |
if type_of t = @{typ prop} then approx_form prec ctxt t |
|
135 |
else if type_of t = @{typ bool} then approx_form prec ctxt (@{const Trueprop} $ t) |
|
136 |
else approx_arith prec ctxt t |
|
137 |
||
56923 | 138 |
fun approximate_cmd modes raw_t state = |
139 |
let |
|
140 |
val ctxt = Toplevel.context_of state; |
|
141 |
val t = Syntax.read_term ctxt raw_t; |
|
142 |
val t' = approx 30 ctxt t; |
|
143 |
val ty' = Term.type_of t'; |
|
144 |
val ctxt' = Variable.auto_fixes t' ctxt; |
|
59174 | 145 |
in |
146 |
Print_Mode.with_modes modes (fn () => |
|
56923 | 147 |
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, |
59174 | 148 |
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) () |
149 |
end |> Pretty.writeln; |
|
56923 | 150 |
|
151 |
val opt_modes = |
|
152 |
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []; |
|
153 |
||
154 |
val _ = |
|
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
56923
diff
changeset
|
155 |
Outer_Syntax.command @{command_spec "approximate"} "print approximation of term" |
56923 | 156 |
(opt_modes -- Parse.term |
157 |
>> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t))); |
|
158 |
||
56813 | 159 |
end; |