author  immler 
Mon, 21 Nov 2016 15:30:35 +0100  
changeset 64519  51be997d0698 
parent 63931  f17a1c60ac39 
child 69597  ff784d5a5bfb 
permissions  rwrr 
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 "Quickcheckapproximation 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 