src/HOL/Library/Old_SMT/old_smt_word.ML
author blanchet
Thu, 28 Aug 2014 00:40:38 +0200
changeset 58058 1a0b18176548
parent 58057 src/HOL/Library/Old_SMT/smt_word.ML@883f3c4c928e
child 58825 2065f49da190
permissions -rw-r--r--
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_smt_word.ML
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
     3
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
     4
SMT setup for words.
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
     5
*)
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
     6
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     7
signature OLD_SMT_WORD =
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
     8
sig
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
     9
  val setup: theory -> theory
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    10
end
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    11
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    12
structure Old_SMT_Word: OLD_SMT_WORD =
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    13
struct
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    14
47567
407cabf66f21 New tactic "word_bitwise" expands word equalities/inequalities into logic.
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 46124
diff changeset
    15
open Word_Lib
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    16
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    17
(* SMT-LIB logic *)
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    18
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    19
fun smtlib_logic ts =
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    20
  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    21
  then SOME "QF_AUFBV"
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    22
  else NONE
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    23
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    24
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    25
(* SMT-LIB builtins *)
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    26
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    27
local
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    28
  val smtlibC = Old_SMTLIB_Interface.smtlibC
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
    29
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
    30
  val wordT = @{typ "'a::len word"}
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
    31
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    32
  fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    33
  fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    34
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
    35
  fun word_typ (Type (@{type_name word}, [T])) =
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    36
        Option.map (index1 "BitVec") (try dest_binT T)
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
    37
    | word_typ _ = NONE
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    38
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
    39
  fun word_num (Type (@{type_name word}, [T])) i =
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    40
        Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
    41
    | word_num _ _ = NONE
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    42
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    43
  fun if_fixed pred m n T ts =
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41072
diff changeset
    44
    let val (Us, U) = Term.strip_type T
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41072
diff changeset
    45
    in
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    46
      if pred (U, Us) then
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    47
        SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T)))
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41072
diff changeset
    48
      else NONE
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41072
diff changeset
    49
    end
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
    50
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    51
  fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    52
  fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    53
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
    54
  fun add_word_fun f (t, n) =
46124
3ee75fe01986 misc tuning;
wenzelm
parents: 41959
diff changeset
    55
    let val (m, _) = Term.dest_Const t
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    56
    in Old_SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    57
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    58
  fun hd2 xs = hd (tl xs)
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
    59
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    60
  fun mk_nat i = @{const nat} $ HOLogic.mk_number @{typ nat} i
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    61
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    62
  fun dest_nat (@{const nat} $ n) = snd (HOLogic.dest_number n)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    63
    | dest_nat t = raise TERM ("not a natural number", [t])
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    64
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    65
  fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    66
    | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
    67
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    68
  fun shift m n T ts =
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    69
    let val U = Term.domain_type T
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    70
    in
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    71
      (case (can dest_wordT U, try (dest_nat o hd2) ts) of
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    72
        (true, SOME i) =>
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    73
          SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T))
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    74
      | _ => NONE)   (* FIXME: also support non-numerical shifts *)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    75
    end
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    76
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    77
  fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    78
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    79
  fun extract m n T ts =
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    80
    let val U = Term.range_type (Term.range_type T)
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    81
    in
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    82
      (case (try (dest_nat o hd) ts, try dest_wordT U) of
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    83
        (SOME lb, SOME i) =>
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    84
          SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    85
      | _ => NONE)
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    86
    end
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    87
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    88
  fun mk_extend c ts = Term.list_comb (Const c, ts)
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
    89
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    90
  fun extend m n T ts =
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    91
    let val (U1, U2) = Term.dest_funT T
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    92
    in
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    93
      (case (try dest_wordT U1, try dest_wordT U2) of
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    94
        (SOME i, SOME j) =>
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    95
          if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T))
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    96
          else NONE
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    97
      | _ => NONE)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
    98
    end
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
    99
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
   100
  fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
   101
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
   102
  fun rotate m n T ts =
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
   103
    let val U = Term.domain_type (Term.range_type T)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41072
diff changeset
   104
    in
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
   105
      (case (can dest_wordT U, try (dest_nat o hd) ts) of
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
   106
        (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
   107
      | _ => NONE)
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41072
diff changeset
   108
    end
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
   109
in
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
   110
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   111
val setup_builtins =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   112
  Old_SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
   113
  fold (add_word_fun if_fixed_all) [
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   114
    (@{term "uminus :: 'a::len word => _"}, "bvneg"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   115
    (@{term "plus :: 'a::len word => _"}, "bvadd"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   116
    (@{term "minus :: 'a::len word => _"}, "bvsub"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   117
    (@{term "times :: 'a::len word => _"}, "bvmul"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   118
    (@{term "bitNOT :: 'a::len word => _"}, "bvnot"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   119
    (@{term "bitAND :: 'a::len word => _"}, "bvand"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   120
    (@{term "bitOR :: 'a::len word => _"}, "bvor"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   121
    (@{term "bitXOR :: 'a::len word => _"}, "bvxor"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   122
    (@{term "word_cat :: 'a::len word => _"}, "concat") ] #>
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   123
  fold (add_word_fun shift) [
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   124
    (@{term "shiftl :: 'a::len word => _ "}, "bvshl"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   125
    (@{term "shiftr :: 'a::len word => _"}, "bvlshr"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   126
    (@{term "sshiftr :: 'a::len word => _"}, "bvashr") ] #>
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   127
  add_word_fun extract
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   128
    (@{term "slice :: _ => 'a::len word => _"}, "extract") #>
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   129
  fold (add_word_fun extend) [
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   130
    (@{term "ucast :: 'a::len word => _"}, "zero_extend"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   131
    (@{term "scast :: 'a::len word => _"}, "sign_extend") ] #>
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   132
  fold (add_word_fun rotate) [
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   133
    (@{term word_rotl}, "rotate_left"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   134
    (@{term word_rotr}, "rotate_right") ] #>
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41127
diff changeset
   135
  fold (add_word_fun if_fixed_args) [
41061
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   136
    (@{term "less :: 'a::len word => _"}, "bvult"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   137
    (@{term "less_eq :: 'a::len word => _"}, "bvule"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   138
    (@{term word_sless}, "bvslt"),
492f8fd35fc0 centralized handling of built-in types and constants for bitvectors
boehmes
parents: 41060
diff changeset
   139
    (@{term word_sle}, "bvsle") ]
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
   140
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
   141
end
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
   142
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
   143
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
   144
(* setup *)
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
   145
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
   146
val setup = 
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41061
diff changeset
   147
  Context.theory_map (
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   148
    Old_SMTLIB_Interface.add_logic (20, smtlib_logic) #>
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41061
diff changeset
   149
    setup_builtins)
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
   150
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents:
diff changeset
   151
end