src/HOL/Tools/SMT/smt_builtin.ML
author boehmes
Wed Nov 24 15:33:35 2010 +0100 (2010-11-24)
changeset 40686 4725ed462387
parent 40681 872b08416fb4
child 40691 a68f64f99832
permissions -rw-r--r--
swap names for built-in tester functions (to better reflect the intuition of what they do);
eta-expand all built-in functions (even those which are only partially supported)
     1 (*  Title:      HOL/Tools/SMT/smt_builtin.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Crafted collection of SMT built-in symbols.
     5 
     6 FIXME: This list is currently not automatically kept synchronized with the
     7 remaining implementation.
     8 *)
     9 
    10 signature SMT_BUILTIN =
    11 sig
    12   val is_builtin: Proof.context -> string * typ -> bool
    13   val is_partially_builtin: Proof.context -> string * typ -> bool
    14 end
    15 
    16 structure SMT_Builtin: SMT_BUILTIN =
    17 struct
    18 
    19 fun is_arithT T =
    20   (case T of
    21      @{typ int} => true
    22    | @{typ nat} => true
    23    | Type ("RealDef.real", []) => true
    24    | _ => false)
    25 
    26 fun is_arithT_dom (Type (@{type_name fun}, [T, _])) = is_arithT T
    27   | is_arithT_dom _ = false
    28 fun is_arithT_ran (Type (@{type_name fun}, [_, T])) = is_arithT T
    29   | is_arithT_ran _ = false
    30 
    31 val builtins = Symtab.make [
    32 
    33   (* Pure constants *)
    34   (@{const_name all}, K true),
    35   (@{const_name "=="}, K true),
    36   (@{const_name "==>"}, K true),
    37   (@{const_name Trueprop}, K true),
    38 
    39   (* logical constants *)
    40   (@{const_name All}, K true),
    41   (@{const_name Ex}, K true),
    42   (@{const_name Ball}, K true),
    43   (@{const_name Bex}, K true),
    44   (@{const_name Ex1}, K true),
    45   (@{const_name True}, K true),
    46   (@{const_name False}, K true),
    47   (@{const_name Not}, K true),
    48   (@{const_name HOL.conj}, K true),
    49   (@{const_name HOL.disj}, K true),
    50   (@{const_name HOL.implies}, K true),
    51 
    52   (* term abbreviations *)
    53   (@{const_name If}, K true),
    54   (@{const_name bool.bool_case}, K true),
    55   (@{const_name Let}, K true),
    56   (* (@{const_name distinct}, K true),  -- not a real builtin, only when
    57                                            applied to an explicit list *)
    58 
    59   (* technicalities *)
    60   (@{const_name SMT.pat}, K true),
    61   (@{const_name SMT.nopat}, K true),
    62   (@{const_name SMT.trigger}, K true),
    63   (@{const_name SMT.weight}, K true),
    64   (@{const_name SMT.fun_app}, K true),
    65   (@{const_name SMT.z3div}, K true),
    66   (@{const_name SMT.z3mod}, K true),
    67 
    68   (* equality *)
    69   (@{const_name HOL.eq}, K true),
    70 
    71   (* numerals *)
    72   (@{const_name zero_class.zero}, is_arithT_dom),
    73   (@{const_name one_class.one}, is_arithT_dom),
    74   (@{const_name Int.Pls}, K true),
    75   (@{const_name Int.Min}, K true),
    76   (@{const_name Int.Bit0}, K true),
    77   (@{const_name Int.Bit1}, K true),
    78   (@{const_name number_of}, is_arithT_ran),
    79 
    80   (* arithmetic *)
    81   (@{const_name nat}, K true),
    82   (@{const_name of_nat}, K true),
    83   (@{const_name Suc}, K true),
    84   (@{const_name plus}, is_arithT_dom),
    85   (@{const_name uminus}, is_arithT_dom),
    86   (@{const_name minus}, is_arithT_dom),
    87   (@{const_name abs}, is_arithT_dom),
    88   (@{const_name min}, is_arithT_dom),
    89   (@{const_name max}, is_arithT_dom),
    90   (@{const_name less}, is_arithT_dom),
    91   (@{const_name less_eq}, is_arithT_dom),
    92   
    93   (* pairs *)
    94   (@{const_name fst}, K true),
    95   (@{const_name snd}, K true),
    96   (@{const_name Pair}, K true)
    97 
    98   ]
    99 
   100 val all_builtins =
   101   builtins
   102   |> Symtab.update (@{const_name times}, is_arithT_dom)
   103   |> Symtab.update (@{const_name div_class.div}, is_arithT_dom)
   104   |> Symtab.update (@{const_name div_class.mod}, is_arithT_dom)
   105   |> Symtab.update ("Rings.inverse_class.divide", is_arithT_dom)
   106 
   107 fun lookup_builtin bs (name, T) =
   108   (case Symtab.lookup bs name of
   109     SOME proper_type => proper_type T
   110   | NONE => false)
   111 
   112 fun is_builtin _ = lookup_builtin builtins
   113 
   114 fun is_partially_builtin _ = lookup_builtin all_builtins
   115 
   116 end