author | wenzelm |
Thu, 08 Nov 2018 15:49:56 +0100 | |
changeset 69266 | 7cc2d66a92a6 |
parent 64519 | 51be997d0698 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
58988 | 1 |
(* Title: HOL/Decision_Procs/approximation_generator.ML |
2 |
Author: Fabian Immler, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
signature APPROXIMATION_GENERATOR = |
|
6 |
sig |
|
7 |
val custom_seed: int Config.T |
|
8 |
val precision: int Config.T |
|
9 |
val epsilon: real Config.T |
|
10 |
val approximation_generator: |
|
11 |
Proof.context -> |
|
12 |
(term * term list) list -> |
|
13 |
bool -> int list -> (bool * term list) option * Quickcheck.report option |
|
14 |
val setup: theory -> theory |
|
15 |
end; |
|
16 |
||
17 |
structure Approximation_Generator : APPROXIMATION_GENERATOR = |
|
18 |
struct |
|
19 |
||
20 |
val custom_seed = Attrib.setup_config_int @{binding quickcheck_approximation_custom_seed} (K ~1) |
|
21 |
||
22 |
val precision = Attrib.setup_config_int @{binding quickcheck_approximation_precision} (K 30) |
|
23 |
||
24 |
val epsilon = Attrib.setup_config_real @{binding quickcheck_approximation_epsilon} (K 0.0) |
|
25 |
||
26 |
val random_float = @{code "random_class.random::_ \<Rightarrow> _ \<Rightarrow> (float \<times> (unit \<Rightarrow> term)) \<times> _"} |
|
27 |
||
28 |
fun nat_of_term t = |
|
29 |
(HOLogic.dest_nat t handle TERM _ => snd (HOLogic.dest_number t) |
|
30 |
handle TERM _ => raise TERM ("nat_of_term", [t])); |
|
31 |
||
32 |
fun int_of_term t = snd (HOLogic.dest_number t) handle TERM _ => raise TERM ("int_of_term", [t]); |
|
33 |
||
34 |
fun real_of_man_exp m e = Real.fromManExp {man = Real.fromInt m, exp = e} |
|
35 |
||
36 |
fun mapprox_float (@{term Float} $ m $ e) = real_of_man_exp (int_of_term m) (int_of_term e) |
|
37 |
| mapprox_float t = Real.fromInt (snd (HOLogic.dest_number t)) |
|
38 |
handle TERM _ => raise TERM ("mapprox_float", [t]); |
|
39 |
||
40 |
(* TODO: define using compiled terms? *) |
|
41 |
fun mapprox_floatarith (@{term Add} $ a $ b) xs = mapprox_floatarith a xs + mapprox_floatarith b xs |
|
42 |
| mapprox_floatarith (@{term Minus} $ a) xs = ~ (mapprox_floatarith a xs) |
|
43 |
| mapprox_floatarith (@{term Mult} $ a $ b) xs = mapprox_floatarith a xs * mapprox_floatarith b xs |
|
44 |
| mapprox_floatarith (@{term Inverse} $ a) xs = 1.0 / mapprox_floatarith a xs |
|
45 |
| mapprox_floatarith (@{term Cos} $ a) xs = Math.cos (mapprox_floatarith a xs) |
|
46 |
| mapprox_floatarith (@{term Arctan} $ a) xs = Math.atan (mapprox_floatarith a xs) |
|
47 |
| mapprox_floatarith (@{term Abs} $ a) xs = abs (mapprox_floatarith a xs) |
|
48 |
| mapprox_floatarith (@{term Max} $ a $ b) xs = |
|
49 |
Real.max (mapprox_floatarith a xs, mapprox_floatarith b xs) |
|
50 |
| mapprox_floatarith (@{term Min} $ a $ b) xs = |
|
51 |
Real.min (mapprox_floatarith a xs, mapprox_floatarith b xs) |
|
52 |
| mapprox_floatarith @{term Pi} _ = Math.pi |
|
53 |
| mapprox_floatarith (@{term Sqrt} $ a) xs = Math.sqrt (mapprox_floatarith a xs) |
|
54 |
| mapprox_floatarith (@{term Exp} $ a) xs = Math.exp (mapprox_floatarith a xs) |
|
64519
51be997d0698
op powr for quickcheck[approximation] (amending 67792e4a5486)
immler
parents:
63931
diff
changeset
|
55 |
| mapprox_floatarith (@{term Powr} $ a $ b) xs = |
51be997d0698
op powr for quickcheck[approximation] (amending 67792e4a5486)
immler
parents:
63931
diff
changeset
|
56 |
Math.pow (mapprox_floatarith a xs, mapprox_floatarith b xs) |
58988 | 57 |
| mapprox_floatarith (@{term Ln} $ a) xs = Math.ln (mapprox_floatarith a xs) |
58 |
| mapprox_floatarith (@{term Power} $ a $ n) xs = |
|
59 |
Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n)) |
|
63931
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63929
diff
changeset
|
60 |
| mapprox_floatarith (@{term Floor} $ a) xs = Real.fromInt (floor (mapprox_floatarith a xs)) |
58988 | 61 |
| mapprox_floatarith (@{term Var} $ n) xs = nth xs (nat_of_term n) |
62 |
| mapprox_floatarith (@{term Num} $ m) _ = mapprox_float m |
|
63 |
| mapprox_floatarith t _ = raise TERM ("mapprox_floatarith", [t]) |
|
64 |
||
65 |
fun mapprox_atLeastAtMost eps x a b xs = |
|
66 |
let |
|
67 |
val x' = mapprox_floatarith x xs |
|
68 |
in |
|
69 |
mapprox_floatarith a xs + eps <= x' andalso x' + eps <= mapprox_floatarith b xs |
|
70 |
end |
|
71 |
||
72 |
fun mapprox_form eps (@{term Bound} $ x $ a $ b $ f) xs = |
|
73 |
(not (mapprox_atLeastAtMost eps x a b xs)) orelse mapprox_form eps f xs |
|
74 |
| mapprox_form eps (@{term Assign} $ x $ a $ f) xs = |
|
75 |
(Real.!= (mapprox_floatarith x xs, mapprox_floatarith a xs)) orelse mapprox_form eps f xs |
|
76 |
| mapprox_form eps (@{term Less} $ a $ b) xs = mapprox_floatarith a xs + eps < mapprox_floatarith b xs |
|
77 |
| mapprox_form eps (@{term LessEqual} $ a $ b) xs = mapprox_floatarith a xs + eps <= mapprox_floatarith b xs |
|
78 |
| mapprox_form eps (@{term AtLeastAtMost} $ x $ a $ b) xs = mapprox_atLeastAtMost eps x a b xs |
|
79 |
| mapprox_form eps (@{term Conj} $ f $ g) xs = mapprox_form eps f xs andalso mapprox_form eps g xs |
|
80 |
| mapprox_form eps (@{term Disj} $ f $ g) xs = mapprox_form eps f xs orelse mapprox_form eps g xs |
|
81 |
| mapprox_form _ t _ = raise TERM ("mapprox_form", [t]) |
|
82 |
||
83 |
fun dest_interpret_form (@{const "interpret_form"} $ b $ xs) = (b, xs) |
|
84 |
| dest_interpret_form t = raise TERM ("dest_interpret_form", [t]) |
|
85 |
||
86 |
fun optionT t = Type (@{type_name "option"}, [t]) |
|
87 |
fun mk_Some t = Const (@{const_name "Some"}, t --> optionT t) |
|
88 |
||
89 |
fun random_float_list size xs seed = |
|
90 |
fold (K (apsnd (random_float size) #-> (fn c => apfst (fn b => b::c)))) xs ([],seed) |
|
91 |
||
92 |
fun real_of_Float (@{code Float} (m, e)) = |
|
93 |
real_of_man_exp (@{code integer_of_int} m) (@{code integer_of_int} e) |
|
94 |
||
95 |
fun is_True @{term True} = true |
|
96 |
| is_True _ = false |
|
97 |
||
98 |
val postproc_form_eqs = |
|
99 |
@{lemma |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
59850
diff
changeset
|
100 |
"real_of_float (Float 0 a) = 0" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
59850
diff
changeset
|
101 |
"real_of_float (Float (numeral m) 0) = numeral m" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
59850
diff
changeset
|
102 |
"real_of_float (Float 1 0) = 1" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
59850
diff
changeset
|
103 |
"real_of_float (Float (- 1) 0) = - 1" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
59850
diff
changeset
|
104 |
"real_of_float (Float 1 (numeral e)) = 2 ^ numeral e" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
59850
diff
changeset
|
105 |
"real_of_float (Float 1 (- numeral e)) = 1 / 2 ^ numeral e" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
59850
diff
changeset
|
106 |
"real_of_float (Float a 1) = a * 2" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
59850
diff
changeset
|
107 |
"real_of_float (Float a (-1)) = a / 2" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
59850
diff
changeset
|
108 |
"real_of_float (Float (- a) b) = - real_of_float (Float a b)" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
59850
diff
changeset
|
109 |
"real_of_float (Float (numeral m) (numeral e)) = numeral m * 2 ^ (numeral e)" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
59850
diff
changeset
|
110 |
"real_of_float (Float (numeral m) (- numeral e)) = numeral m / 2 ^ (numeral e)" |
58988 | 111 |
"- (c * d::real) = -c * d" |
112 |
"- (c / d::real) = -c / d" |
|
113 |
"- (0::real) = 0" |
|
114 |
"int_of_integer (numeral k) = numeral k" |
|
115 |
"int_of_integer (- numeral k) = - numeral k" |
|
116 |
"int_of_integer 0 = 0" |
|
117 |
"int_of_integer 1 = 1" |
|
118 |
"int_of_integer (- 1) = - 1" |
|
119 |
by auto |
|
120 |
} |
|
121 |
||
122 |
fun rewrite_with ctxt thms = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps thms) |
|
59629 | 123 |
fun conv_term ctxt conv r = Thm.cterm_of ctxt r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd |
58988 | 124 |
|
125 |
fun approx_random ctxt prec eps frees e xs genuine_only size seed = |
|
126 |
let |
|
127 |
val (rs, seed') = random_float_list size xs seed |
|
128 |
fun mk_approx_form e ts = |
|
129 |
@{const "approx_form"} $ |
|
130 |
HOLogic.mk_number @{typ nat} prec $ |
|
131 |
e $ |
|
132 |
(HOLogic.mk_list @{typ "(float * float) option"} |
|
133 |
(map (fn t => mk_Some @{typ "float * float"} $ HOLogic.mk_prod (t, t)) ts)) $ |
|
134 |
@{term "[] :: nat list"} |
|
135 |
in |
|
63931
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63929
diff
changeset
|
136 |
(if |
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63929
diff
changeset
|
137 |
mapprox_form eps e (map (real_of_Float o fst) rs) |
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63929
diff
changeset
|
138 |
handle |
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63929
diff
changeset
|
139 |
General.Overflow => false |
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63929
diff
changeset
|
140 |
| General.Domain => false |
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63929
diff
changeset
|
141 |
| General.Div => false |
f17a1c60ac39
approximation: preprocessing for nat/int expressions
immler
parents:
63929
diff
changeset
|
142 |
| IEEEReal.Unordered => false |
58988 | 143 |
then |
144 |
let |
|
145 |
val ts = map (fn x => snd x ()) rs |
|
146 |
val ts' = map |
|
147 |
(AList.lookup op = (map dest_Free xs ~~ ts) |
|
148 |
#> the_default Term.dummy |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
59850
diff
changeset
|
149 |
#> curry op $ @{term "real_of_float::float\<Rightarrow>_"} |
59629 | 150 |
#> conv_term ctxt (rewrite_with ctxt postproc_form_eqs)) |
58988 | 151 |
frees |
152 |
in |
|
59850 | 153 |
if Approximation.approximate ctxt (mk_approx_form e ts) |> is_True |
58988 | 154 |
then SOME (true, ts') |
155 |
else (if genuine_only then NONE else SOME (false, ts')) |
|
156 |
end |
|
157 |
else NONE, seed') |
|
158 |
end |
|
159 |
||
160 |
val preproc_form_eqs = |
|
161 |
@{lemma |
|
162 |
"(a::real) \<in> {b .. c} \<longleftrightarrow> b \<le> a \<and> a \<le> c" |
|
163 |
"a = b \<longleftrightarrow> a \<le> b \<and> b \<le> a" |
|
164 |
"(p \<longrightarrow> q) \<longleftrightarrow> \<not>p \<or> q" |
|
165 |
"(p \<longleftrightarrow> q) \<longleftrightarrow> (p \<longrightarrow> q) \<and> (q \<longrightarrow> p)" |
|
59629 | 166 |
by auto} |
58988 | 167 |
|
168 |
fun reify_goal ctxt t = |
|
169 |
HOLogic.mk_not t |
|
59629 | 170 |
|> conv_term ctxt (rewrite_with ctxt preproc_form_eqs) |
63929
b673e7221b16
approximation: rewrite for reduction to base expressions
immler
parents:
61609
diff
changeset
|
171 |
|> Approximation.reify_form ctxt |
58988 | 172 |
|> dest_interpret_form |
173 |
||> HOLogic.dest_list |
|
174 |
||
175 |
fun approximation_generator_raw ctxt t = |
|
176 |
let |
|
177 |
val iterations = Config.get ctxt Quickcheck.iterations |
|
178 |
val prec = Config.get ctxt precision |
|
179 |
val eps = Config.get ctxt epsilon |
|
180 |
val cs = Config.get ctxt custom_seed |
|
181 |
val seed = (Code_Numeral.natural_of_integer (cs + 1), Code_Numeral.natural_of_integer 1) |
|
182 |
val run = if cs < 0 |
|
183 |
then (fn f => fn seed => (Random_Engine.run f, seed)) |
|
184 |
else (fn f => fn seed => f seed) |
|
185 |
val frees = Term.add_frees t [] |
|
186 |
val (e, xs) = reify_goal ctxt t |
|
187 |
fun single_tester b s = |
|
188 |
approx_random ctxt prec eps frees e xs b s |> run |
|
189 |
fun iterate _ _ 0 _ = NONE |
|
190 |
| iterate genuine_only size j seed = |
|
191 |
case single_tester genuine_only size seed of |
|
192 |
(NONE, seed') => iterate genuine_only size (j - 1) seed' |
|
193 |
| (SOME q, _) => SOME q |
|
194 |
in |
|
195 |
fn genuine_only => fn size => (iterate genuine_only size iterations seed, NONE) |
|
196 |
end |
|
197 |
||
198 |
fun approximation_generator ctxt [(t, _)] = |
|
199 |
(fn genuine_only => |
|
200 |
fn [_, size] => |
|
201 |
approximation_generator_raw ctxt t genuine_only |
|
202 |
(Code_Numeral.natural_of_integer size)) |
|
203 |
| approximation_generator _ _ = |
|
204 |
error "Quickcheck-approximation does not support type variables (or finite instantiations)" |
|
205 |
||
206 |
val test_goals = |
|
207 |
Quickcheck_Common.generator_test_goal_terms |
|
208 |
("approximation", (fn _ => fn _ => false, approximation_generator)) |
|
209 |
||
210 |
val active = Attrib.setup_config_bool @{binding quickcheck_approximation_active} (K false) |
|
211 |
||
212 |
val setup = Context.theory_map (Quickcheck.add_tester ("approximation", (active, test_goals))) |
|
213 |
||
214 |
end |