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