src/HOL/Tools/SMT/smt_real.ML
author boehmes
Wed, 23 May 2012 16:03:38 +0200
changeset 47965 8ba6438557bc
parent 46497 89ccf66aa73d
child 51717 9e7d1c139569
permissions -rw-r--r--
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT/smt_real.ML
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     3
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     4
SMT setup for reals.
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     5
*)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     6
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     7
signature SMT_REAL =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     8
sig
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     9
  val setup: theory -> theory
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    10
end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    11
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    12
structure SMT_Real: SMT_REAL =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    13
struct
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    14
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    15
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    16
(* SMT-LIB logic *)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    17
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    18
fun smtlib_logic ts =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    19
  if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    20
  then SOME "AUFLIRA"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    21
  else NONE
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    22
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    23
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40579
diff changeset
    24
(* SMT-LIB and Z3 built-ins *)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    25
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    26
local
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40579
diff changeset
    27
  fun real_num _ i = SOME (string_of_int i ^ ".0")
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    28
41439
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    29
  fun is_linear [t] = SMT_Utils.is_number t
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    30
    | is_linear [t, u] = SMT_Utils.is_number t orelse SMT_Utils.is_number u
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    31
    | is_linear _ = false
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    32
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    33
  fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    34
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41280
diff changeset
    35
  fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    36
    | times _ _ _  = NONE
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    37
in
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    38
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40579
diff changeset
    39
val setup_builtins =
41439
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    40
  SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    41
    (@{typ real}, K (SOME "Real"), real_num) #>
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    42
  fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    43
    (@{const less (real)}, "<"),
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    44
    (@{const less_eq (real)}, "<="),
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40579
diff changeset
    45
    (@{const uminus (real)}, "~"),
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40579
diff changeset
    46
    (@{const plus (real)}, "+"),
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    47
    (@{const minus (real)}, "-") ] #>
41439
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    48
  SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41072
diff changeset
    49
    (Term.dest_Const @{const times (real)}, times) #>
41439
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    50
  SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    51
    (@{const times (real)}, "*") #>
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    52
  SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
a31c451183e6 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41302
diff changeset
    53
    (@{const divide (real)}, "/")
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    54
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    55
end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    56
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    57
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    58
(* Z3 constructors *)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    59
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    60
local
41691
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    61
  fun z3_mk_builtin_typ (Z3_Interface.Sym ("Real", _)) = SOME @{typ real}
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    62
    | z3_mk_builtin_typ (Z3_Interface.Sym ("real", _)) = SOME @{typ real}
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    63
        (*FIXME: delete*)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    64
    | z3_mk_builtin_typ _ = NONE
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    65
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    66
  fun z3_mk_builtin_num _ i T =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    67
    if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    68
    else NONE
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    69
47965
8ba6438557bc extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents: 46497
diff changeset
    70
  fun mk_nary _ cu [] = cu
8ba6438557bc extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents: 46497
diff changeset
    71
    | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
8ba6438557bc extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents: 46497
diff changeset
    72
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 41691
diff changeset
    73
  val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)})
47965
8ba6438557bc extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents: 46497
diff changeset
    74
  val add = Thm.cterm_of @{theory} @{const plus (real)}
8ba6438557bc extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents: 46497
diff changeset
    75
  val real0 = Numeral.mk_cnumber @{ctyp real} 0
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40516
diff changeset
    76
  val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40516
diff changeset
    77
  val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40516
diff changeset
    78
  val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40516
diff changeset
    79
  val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40516
diff changeset
    80
  val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    81
41691
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    82
  fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
47965
8ba6438557bc extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents: 46497
diff changeset
    83
    | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts =
8ba6438557bc extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents: 46497
diff changeset
    84
        SOME (mk_nary add real0 cts)
41691
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    85
    | z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] =
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    86
        SOME (mk_sub ct cu)
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    87
    | z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] =
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    88
        SOME (mk_mul ct cu)
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    89
    | z3_mk_builtin_fun (Z3_Interface.Sym ("/", _)) [ct, cu] =
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    90
        SOME (mk_div ct cu)
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    91
    | z3_mk_builtin_fun (Z3_Interface.Sym ("<", _)) [ct, cu] =
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    92
        SOME (mk_lt ct cu)
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    93
    | z3_mk_builtin_fun (Z3_Interface.Sym ("<=", _)) [ct, cu] =
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    94
        SOME (mk_le ct cu)
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    95
    | z3_mk_builtin_fun (Z3_Interface.Sym (">", _)) [ct, cu] =
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    96
        SOME (mk_lt cu ct)
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    97
    | z3_mk_builtin_fun (Z3_Interface.Sym (">=", _)) [ct, cu] =
8f0531cf34f8 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41439
diff changeset
    98
        SOME (mk_le cu ct)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    99
    | z3_mk_builtin_fun _ _ = NONE
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   100
in
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   101
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   102
val z3_mk_builtins = {
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   103
  mk_builtin_typ = z3_mk_builtin_typ,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   104
  mk_builtin_num = z3_mk_builtin_num,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   105
  mk_builtin_fun = (fn _ => fn sym => fn cts =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   106
    (case try (#T o Thm.rep_cterm o hd) cts of
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   107
      SOME @{typ real} => z3_mk_builtin_fun sym cts
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   108
    | _ => NONE)) }
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   109
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   110
end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   111
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   112
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   113
(* Z3 proof reconstruction *)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   114
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   115
val real_rules = @{lemma
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   116
  "0 + (x::real) = x"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   117
  "x + 0 = x"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   118
  "0 * x = 0"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   119
  "1 * x = x"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   120
  "x + y = y + x"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   121
  by auto}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   122
38715
6513ea67d95d renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents: 36899
diff changeset
   123
val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   124
  "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   125
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   126
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   127
(* setup *)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   128
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   129
val setup =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   130
  Context.theory_map (
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40579
diff changeset
   131
    SMTLIB_Interface.add_logic (10, smtlib_logic) #>
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
   132
    setup_builtins #>
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   133
    Z3_Interface.add_mk_builtins z3_mk_builtins #>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   134
    fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   135
    Z3_Proof_Tools.add_simproc real_linarith_proc)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   136
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
   137
end