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