src/HOL/Tools/SMT/z3_real.ML
author haftmann
Mon Jun 01 18:59:21 2015 +0200 (2015-06-01)
changeset 60352 d46de31a50c4
parent 58061 3d060f43accb
child 61609 77b453bd616f
permissions -rw-r--r--
separate class for division operator, with particular syntax added in more specific classes
blanchet@58061
     1
(*  Title:      HOL/Tools/SMT/z3_real.ML
blanchet@56078
     2
    Author:     Sascha Boehme, TU Muenchen
blanchet@56078
     3
blanchet@56078
     4
Z3 setup for reals.
blanchet@56078
     5
*)
blanchet@56078
     6
blanchet@58061
     7
structure Z3_Real: sig end =
blanchet@56078
     8
struct
blanchet@56078
     9
blanchet@58061
    10
fun real_type_parser (SMTLIB.Sym "Real", []) = SOME @{typ Real.real}
blanchet@56078
    11
  | real_type_parser _ = NONE
blanchet@56078
    12
blanchet@58061
    13
fun real_term_parser (SMTLIB.Dec (i, 0), []) = SOME (HOLogic.mk_number @{typ Real.real} i)
blanchet@58061
    14
  | real_term_parser (SMTLIB.Sym "/", [t1, t2]) =
haftmann@60352
    15
      SOME (@{term "Rings.divide :: real => _"} $ t1 $ t2)
blanchet@58061
    16
  | real_term_parser (SMTLIB.Sym "to_real", [t]) = SOME (@{term "Real.real :: int => _"} $ t)
blanchet@56078
    17
  | real_term_parser _ = NONE
blanchet@56078
    18
blanchet@56078
    19
fun abstract abs t =
blanchet@56078
    20
  (case t of
haftmann@60352
    21
    (c as @{term "Rings.divide :: real => _"}) $ t1 $ t2 =>
blanchet@56078
    22
      abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
blanchet@56078
    23
  | (c as @{term "Real.real :: int => _"}) $ t =>
blanchet@56078
    24
      abs t #>> (fn u => SOME (c $ u))
blanchet@56078
    25
  | _ => pair NONE)
blanchet@56078
    26
blanchet@56078
    27
val _ = Theory.setup (Context.theory_map (
blanchet@58061
    28
  SMTLIB_Proof.add_type_parser real_type_parser #>
blanchet@58061
    29
  SMTLIB_Proof.add_term_parser real_term_parser #>
blanchet@58061
    30
  Z3_Replay_Methods.add_arith_abstracter abstract))
blanchet@56078
    31
blanchet@57229
    32
end;