src/HOL/Library/Old_SMT/old_smt_real.ML
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 59634 4b94cc030ba0
child 61144 5e94dfead1c2
permissions -rw-r--r--
isabelle update_cartouches;
blanchet@58058
     1
(*  Title:      HOL/Library/Old_SMT/old_smt_real.ML
boehmes@36899
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36899
     3
boehmes@36899
     4
SMT setup for reals.
boehmes@36899
     5
*)
boehmes@36899
     6
wenzelm@58825
     7
structure Old_SMT_Real: sig end =
boehmes@36899
     8
struct
boehmes@36899
     9
boehmes@36899
    10
boehmes@36899
    11
(* SMT-LIB logic *)
boehmes@36899
    12
boehmes@36899
    13
fun smtlib_logic ts =
boehmes@36899
    14
  if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts
boehmes@36899
    15
  then SOME "AUFLIRA"
boehmes@36899
    16
  else NONE
boehmes@36899
    17
boehmes@36899
    18
boehmes@41059
    19
(* SMT-LIB and Z3 built-ins *)
boehmes@36899
    20
boehmes@36899
    21
local
boehmes@41059
    22
  fun real_num _ i = SOME (string_of_int i ^ ".0")
boehmes@41280
    23
blanchet@58058
    24
  fun is_linear [t] = Old_SMT_Utils.is_number t
blanchet@58058
    25
    | is_linear [t, u] = Old_SMT_Utils.is_number t orelse Old_SMT_Utils.is_number u
boehmes@41280
    26
    | is_linear _ = false
boehmes@41280
    27
boehmes@41281
    28
  fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
boehmes@41281
    29
blanchet@58057
    30
  fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
boehmes@36899
    31
in
boehmes@36899
    32
boehmes@41059
    33
val setup_builtins =
blanchet@58058
    34
  Old_SMT_Builtin.add_builtin_typ Old_SMTLIB_Interface.smtlibC
boehmes@41439
    35
    (@{typ real}, K (SOME "Real"), real_num) #>
blanchet@58058
    36
  fold (Old_SMT_Builtin.add_builtin_fun' Old_SMTLIB_Interface.smtlibC) [
boehmes@41280
    37
    (@{const less (real)}, "<"),
boehmes@41280
    38
    (@{const less_eq (real)}, "<="),
boehmes@41059
    39
    (@{const uminus (real)}, "~"),
boehmes@41059
    40
    (@{const plus (real)}, "+"),
boehmes@41280
    41
    (@{const minus (real)}, "-") ] #>
blanchet@58058
    42
  Old_SMT_Builtin.add_builtin_fun Old_SMTLIB_Interface.smtlibC
boehmes@41280
    43
    (Term.dest_Const @{const times (real)}, times) #>
blanchet@58058
    44
  Old_SMT_Builtin.add_builtin_fun' Old_Z3_Interface.smtlib_z3C
boehmes@41439
    45
    (@{const times (real)}, "*") #>
blanchet@58058
    46
  Old_SMT_Builtin.add_builtin_fun' Old_Z3_Interface.smtlib_z3C
boehmes@41439
    47
    (@{const divide (real)}, "/")
boehmes@36899
    48
boehmes@36899
    49
end
boehmes@36899
    50
boehmes@36899
    51
boehmes@36899
    52
(* Z3 constructors *)
boehmes@36899
    53
boehmes@36899
    54
local
blanchet@58058
    55
  fun z3_mk_builtin_typ (Old_Z3_Interface.Sym ("Real", _)) = SOME @{typ real}
blanchet@58058
    56
    | z3_mk_builtin_typ (Old_Z3_Interface.Sym ("real", _)) = SOME @{typ real}
boehmes@41691
    57
        (*FIXME: delete*)
boehmes@36899
    58
    | z3_mk_builtin_typ _ = NONE
boehmes@36899
    59
boehmes@36899
    60
  fun z3_mk_builtin_num _ i T =
boehmes@36899
    61
    if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
boehmes@36899
    62
    else NONE
boehmes@36899
    63
boehmes@47965
    64
  fun mk_nary _ cu [] = cu
boehmes@47965
    65
    | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
boehmes@47965
    66
wenzelm@59634
    67
  val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (real)})
wenzelm@59634
    68
  val add = Thm.cterm_of @{context} @{const plus (real)}
boehmes@47965
    69
  val real0 = Numeral.mk_cnumber @{ctyp real} 0
wenzelm@59634
    70
  val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (real)})
wenzelm@59634
    71
  val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (real)})
wenzelm@59634
    72
  val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const divide (real)})
wenzelm@59634
    73
  val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (real)})
wenzelm@59634
    74
  val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (real)})
boehmes@36899
    75
blanchet@58058
    76
  fun z3_mk_builtin_fun (Old_Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
blanchet@58058
    77
    | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("+", _)) cts =
boehmes@47965
    78
        SOME (mk_nary add real0 cts)
blanchet@58058
    79
    | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("-", _)) [ct, cu] =
boehmes@41691
    80
        SOME (mk_sub ct cu)
blanchet@58058
    81
    | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("*", _)) [ct, cu] =
boehmes@41691
    82
        SOME (mk_mul ct cu)
blanchet@58058
    83
    | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("/", _)) [ct, cu] =
boehmes@41691
    84
        SOME (mk_div ct cu)
blanchet@58058
    85
    | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("<", _)) [ct, cu] =
boehmes@41691
    86
        SOME (mk_lt ct cu)
blanchet@58058
    87
    | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("<=", _)) [ct, cu] =
boehmes@41691
    88
        SOME (mk_le ct cu)
blanchet@58058
    89
    | z3_mk_builtin_fun (Old_Z3_Interface.Sym (">", _)) [ct, cu] =
boehmes@41691
    90
        SOME (mk_lt cu ct)
blanchet@58058
    91
    | z3_mk_builtin_fun (Old_Z3_Interface.Sym (">=", _)) [ct, cu] =
boehmes@41691
    92
        SOME (mk_le cu ct)
boehmes@36899
    93
    | z3_mk_builtin_fun _ _ = NONE
boehmes@36899
    94
in
boehmes@36899
    95
boehmes@36899
    96
val z3_mk_builtins = {
boehmes@36899
    97
  mk_builtin_typ = z3_mk_builtin_typ,
boehmes@36899
    98
  mk_builtin_num = z3_mk_builtin_num,
boehmes@36899
    99
  mk_builtin_fun = (fn _ => fn sym => fn cts =>
wenzelm@59586
   100
    (case try (Thm.typ_of_cterm o hd) cts of
boehmes@36899
   101
      SOME @{typ real} => z3_mk_builtin_fun sym cts
boehmes@36899
   102
    | _ => NONE)) }
boehmes@36899
   103
boehmes@36899
   104
end
boehmes@36899
   105
boehmes@36899
   106
boehmes@36899
   107
(* Z3 proof reconstruction *)
boehmes@36899
   108
boehmes@36899
   109
val real_rules = @{lemma
boehmes@36899
   110
  "0 + (x::real) = x"
boehmes@36899
   111
  "x + 0 = x"
boehmes@36899
   112
  "0 * x = 0"
boehmes@36899
   113
  "1 * x = x"
boehmes@36899
   114
  "x + y = y + x"
boehmes@36899
   115
  by auto}
boehmes@36899
   116
wenzelm@38715
   117
val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
wenzelm@51717
   118
  "(m::real) < n", "(m::real) <= n", "(m::real) = n"] Lin_Arith.simproc
boehmes@36899
   119
boehmes@36899
   120
boehmes@36899
   121
(* setup *)
boehmes@36899
   122
wenzelm@58825
   123
val _ =
wenzelm@58825
   124
  Theory.setup
wenzelm@58825
   125
   (Context.theory_map (
wenzelm@58825
   126
      Old_SMTLIB_Interface.add_logic (10, smtlib_logic) #>
wenzelm@58825
   127
      setup_builtins #>
wenzelm@58825
   128
      Old_Z3_Interface.add_mk_builtins z3_mk_builtins #>
wenzelm@58825
   129
      fold Old_Z3_Proof_Reconstruction.add_z3_rule real_rules #>
wenzelm@58825
   130
      Old_Z3_Proof_Tools.add_simproc real_linarith_proc))
boehmes@36899
   131
boehmes@36899
   132
end