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)
|
|
55 |
| mapprox_floatarith (@{term Ln} $ a) xs = Math.ln (mapprox_floatarith a xs)
|
|
56 |
| mapprox_floatarith (@{term Power} $ a $ n) xs =
|
|
57 |
Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
|
|
58 |
| mapprox_floatarith (@{term Var} $ n) xs = nth xs (nat_of_term n)
|
|
59 |
| mapprox_floatarith (@{term Num} $ m) _ = mapprox_float m
|
|
60 |
| mapprox_floatarith t _ = raise TERM ("mapprox_floatarith", [t])
|
|
61 |
|
|
62 |
fun mapprox_atLeastAtMost eps x a b xs =
|
|
63 |
let
|
|
64 |
val x' = mapprox_floatarith x xs
|
|
65 |
in
|
|
66 |
mapprox_floatarith a xs + eps <= x' andalso x' + eps <= mapprox_floatarith b xs
|
|
67 |
end
|
|
68 |
|
|
69 |
fun mapprox_form eps (@{term Bound} $ x $ a $ b $ f) xs =
|
|
70 |
(not (mapprox_atLeastAtMost eps x a b xs)) orelse mapprox_form eps f xs
|
|
71 |
| mapprox_form eps (@{term Assign} $ x $ a $ f) xs =
|
|
72 |
(Real.!= (mapprox_floatarith x xs, mapprox_floatarith a xs)) orelse mapprox_form eps f xs
|
|
73 |
| mapprox_form eps (@{term Less} $ a $ b) xs = mapprox_floatarith a xs + eps < mapprox_floatarith b xs
|
|
74 |
| mapprox_form eps (@{term LessEqual} $ a $ b) xs = mapprox_floatarith a xs + eps <= mapprox_floatarith b xs
|
|
75 |
| mapprox_form eps (@{term AtLeastAtMost} $ x $ a $ b) xs = mapprox_atLeastAtMost eps x a b xs
|
|
76 |
| mapprox_form eps (@{term Conj} $ f $ g) xs = mapprox_form eps f xs andalso mapprox_form eps g xs
|
|
77 |
| mapprox_form eps (@{term Disj} $ f $ g) xs = mapprox_form eps f xs orelse mapprox_form eps g xs
|
|
78 |
| mapprox_form _ t _ = raise TERM ("mapprox_form", [t])
|
|
79 |
|
|
80 |
fun dest_interpret_form (@{const "interpret_form"} $ b $ xs) = (b, xs)
|
|
81 |
| dest_interpret_form t = raise TERM ("dest_interpret_form", [t])
|
|
82 |
|
|
83 |
fun optionT t = Type (@{type_name "option"}, [t])
|
|
84 |
fun mk_Some t = Const (@{const_name "Some"}, t --> optionT t)
|
|
85 |
|
|
86 |
fun random_float_list size xs seed =
|
|
87 |
fold (K (apsnd (random_float size) #-> (fn c => apfst (fn b => b::c)))) xs ([],seed)
|
|
88 |
|
|
89 |
fun real_of_Float (@{code Float} (m, e)) =
|
|
90 |
real_of_man_exp (@{code integer_of_int} m) (@{code integer_of_int} e)
|
|
91 |
|
|
92 |
fun is_True @{term True} = true
|
|
93 |
| is_True _ = false
|
|
94 |
|
|
95 |
val postproc_form_eqs =
|
|
96 |
@{lemma
|
|
97 |
"real (Float 0 a) = 0"
|
|
98 |
"real (Float (numeral m) 0) = numeral m"
|
|
99 |
"real (Float 1 0) = 1"
|
|
100 |
"real (Float (- 1) 0) = - 1"
|
|
101 |
"real (Float 1 (numeral e)) = 2 ^ numeral e"
|
|
102 |
"real (Float 1 (- numeral e)) = 1 / 2 ^ numeral e"
|
|
103 |
"real (Float a 1) = a * 2"
|
|
104 |
"real (Float a (-1)) = a / 2"
|
|
105 |
"real (Float (- a) b) = - real (Float a b)"
|
|
106 |
"real (Float (numeral m) (numeral e)) = numeral m * 2 ^ (numeral e)"
|
|
107 |
"real (Float (numeral m) (- numeral e)) = numeral m / 2 ^ (numeral e)"
|
|
108 |
"- (c * d::real) = -c * d"
|
|
109 |
"- (c / d::real) = -c / d"
|
|
110 |
"- (0::real) = 0"
|
|
111 |
"int_of_integer (numeral k) = numeral k"
|
|
112 |
"int_of_integer (- numeral k) = - numeral k"
|
|
113 |
"int_of_integer 0 = 0"
|
|
114 |
"int_of_integer 1 = 1"
|
|
115 |
"int_of_integer (- 1) = - 1"
|
|
116 |
by auto
|
|
117 |
}
|
|
118 |
|
|
119 |
fun rewrite_with ctxt thms = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps thms)
|
59629
|
120 |
fun conv_term ctxt conv r = Thm.cterm_of ctxt r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
|
58988
|
121 |
|
|
122 |
fun approx_random ctxt prec eps frees e xs genuine_only size seed =
|
|
123 |
let
|
|
124 |
val (rs, seed') = random_float_list size xs seed
|
|
125 |
fun mk_approx_form e ts =
|
|
126 |
@{const "approx_form"} $
|
|
127 |
HOLogic.mk_number @{typ nat} prec $
|
|
128 |
e $
|
|
129 |
(HOLogic.mk_list @{typ "(float * float) option"}
|
|
130 |
(map (fn t => mk_Some @{typ "float * float"} $ HOLogic.mk_prod (t, t)) ts)) $
|
|
131 |
@{term "[] :: nat list"}
|
|
132 |
in
|
|
133 |
(if mapprox_form eps e (map (real_of_Float o fst) rs)
|
|
134 |
then
|
|
135 |
let
|
|
136 |
val ts = map (fn x => snd x ()) rs
|
|
137 |
val ts' = map
|
|
138 |
(AList.lookup op = (map dest_Free xs ~~ ts)
|
|
139 |
#> the_default Term.dummy
|
|
140 |
#> curry op $ @{term "real::float\<Rightarrow>_"}
|
59629
|
141 |
#> conv_term ctxt (rewrite_with ctxt postproc_form_eqs))
|
58988
|
142 |
frees
|
|
143 |
in
|
59850
|
144 |
if Approximation.approximate ctxt (mk_approx_form e ts) |> is_True
|
58988
|
145 |
then SOME (true, ts')
|
|
146 |
else (if genuine_only then NONE else SOME (false, ts'))
|
|
147 |
end
|
|
148 |
else NONE, seed')
|
|
149 |
end
|
|
150 |
|
|
151 |
val preproc_form_eqs =
|
|
152 |
@{lemma
|
|
153 |
"(a::real) \<in> {b .. c} \<longleftrightarrow> b \<le> a \<and> a \<le> c"
|
|
154 |
"a = b \<longleftrightarrow> a \<le> b \<and> b \<le> a"
|
|
155 |
"(p \<longrightarrow> q) \<longleftrightarrow> \<not>p \<or> q"
|
|
156 |
"(p \<longleftrightarrow> q) \<longleftrightarrow> (p \<longrightarrow> q) \<and> (q \<longrightarrow> p)"
|
|
157 |
"\<not> (a < b) \<longleftrightarrow> b \<le> a"
|
|
158 |
"\<not> (a \<le> b) \<longleftrightarrow> b < a"
|
|
159 |
"\<not> (p \<and> q) \<longleftrightarrow> \<not> p \<or> \<not> q"
|
|
160 |
"\<not> (p \<or> q) \<longleftrightarrow> \<not> p \<and> \<not> q"
|
|
161 |
"\<not> \<not> q \<longleftrightarrow> q"
|
59629
|
162 |
by auto}
|
58988
|
163 |
|
59850
|
164 |
val form_equations = @{thms interpret_form_equations};
|
|
165 |
|
58988
|
166 |
fun reify_goal ctxt t =
|
|
167 |
HOLogic.mk_not t
|
59629
|
168 |
|> conv_term ctxt (rewrite_with ctxt preproc_form_eqs)
|
|
169 |
|> conv_term ctxt (Reification.conv ctxt form_equations)
|
58988
|
170 |
|> dest_interpret_form
|
|
171 |
||> HOLogic.dest_list
|
|
172 |
|
|
173 |
fun approximation_generator_raw ctxt t =
|
|
174 |
let
|
|
175 |
val iterations = Config.get ctxt Quickcheck.iterations
|
|
176 |
val prec = Config.get ctxt precision
|
|
177 |
val eps = Config.get ctxt epsilon
|
|
178 |
val cs = Config.get ctxt custom_seed
|
|
179 |
val seed = (Code_Numeral.natural_of_integer (cs + 1), Code_Numeral.natural_of_integer 1)
|
|
180 |
val run = if cs < 0
|
|
181 |
then (fn f => fn seed => (Random_Engine.run f, seed))
|
|
182 |
else (fn f => fn seed => f seed)
|
|
183 |
val frees = Term.add_frees t []
|
|
184 |
val (e, xs) = reify_goal ctxt t
|
|
185 |
fun single_tester b s =
|
|
186 |
approx_random ctxt prec eps frees e xs b s |> run
|
|
187 |
fun iterate _ _ 0 _ = NONE
|
|
188 |
| iterate genuine_only size j seed =
|
|
189 |
case single_tester genuine_only size seed of
|
|
190 |
(NONE, seed') => iterate genuine_only size (j - 1) seed'
|
|
191 |
| (SOME q, _) => SOME q
|
|
192 |
in
|
|
193 |
fn genuine_only => fn size => (iterate genuine_only size iterations seed, NONE)
|
|
194 |
end
|
|
195 |
|
|
196 |
fun approximation_generator ctxt [(t, _)] =
|
|
197 |
(fn genuine_only =>
|
|
198 |
fn [_, size] =>
|
|
199 |
approximation_generator_raw ctxt t genuine_only
|
|
200 |
(Code_Numeral.natural_of_integer size))
|
|
201 |
| approximation_generator _ _ =
|
|
202 |
error "Quickcheck-approximation does not support type variables (or finite instantiations)"
|
|
203 |
|
|
204 |
val test_goals =
|
|
205 |
Quickcheck_Common.generator_test_goal_terms
|
|
206 |
("approximation", (fn _ => fn _ => false, approximation_generator))
|
|
207 |
|
|
208 |
val active = Attrib.setup_config_bool @{binding quickcheck_approximation_active} (K false)
|
|
209 |
|
|
210 |
val setup = Context.theory_map (Quickcheck.add_tester ("approximation", (active, test_goals)))
|
|
211 |
|
|
212 |
end
|