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