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)


120 
fun conv_term thy conv r = cterm_of thy r > conv > Thm.prop_of > Logic.dest_equals > snd


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>_"}


141 
#> conv_term (Proof_Context.theory_of ctxt) (rewrite_with ctxt postproc_form_eqs))


142 
frees


143 
in


144 
if approximate ctxt (mk_approx_form e ts) > is_True


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"


162 
by auto


163 
}


164 


165 
fun reify_goal ctxt t =


166 
HOLogic.mk_not t


167 
> conv_term (Proof_Context.theory_of ctxt) (rewrite_with ctxt preproc_form_eqs)


168 
> conv_term (Proof_Context.theory_of ctxt) (Reification.conv ctxt form_equations)


169 
> dest_interpret_form


170 
> HOLogic.dest_list


171 


172 
fun approximation_generator_raw ctxt t =


173 
let


174 
val iterations = Config.get ctxt Quickcheck.iterations


175 
val prec = Config.get ctxt precision


176 
val eps = Config.get ctxt epsilon


177 
val cs = Config.get ctxt custom_seed


178 
val seed = (Code_Numeral.natural_of_integer (cs + 1), Code_Numeral.natural_of_integer 1)


179 
val run = if cs < 0


180 
then (fn f => fn seed => (Random_Engine.run f, seed))


181 
else (fn f => fn seed => f seed)


182 
val frees = Term.add_frees t []


183 
val (e, xs) = reify_goal ctxt t


184 
fun single_tester b s =


185 
approx_random ctxt prec eps frees e xs b s > run


186 
fun iterate _ _ 0 _ = NONE


187 
 iterate genuine_only size j seed =


188 
case single_tester genuine_only size seed of


189 
(NONE, seed') => iterate genuine_only size (j  1) seed'


190 
 (SOME q, _) => SOME q


191 
in


192 
fn genuine_only => fn size => (iterate genuine_only size iterations seed, NONE)


193 
end


194 


195 
fun approximation_generator ctxt [(t, _)] =


196 
(fn genuine_only =>


197 
fn [_, size] =>


198 
approximation_generator_raw ctxt t genuine_only


199 
(Code_Numeral.natural_of_integer size))


200 
 approximation_generator _ _ =


201 
error "Quickcheckapproximation does not support type variables (or finite instantiations)"


202 


203 
val test_goals =


204 
Quickcheck_Common.generator_test_goal_terms


205 
("approximation", (fn _ => fn _ => false, approximation_generator))


206 


207 
val active = Attrib.setup_config_bool @{binding quickcheck_approximation_active} (K false)


208 


209 
val setup = Context.theory_map (Quickcheck.add_tester ("approximation", (active, test_goals)))


210 


211 
end
