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