src/HOL/Tools/SMT/smt_translate.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 37124 fe22fc54b876
child 39298 5aefb5bc8a93
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT/smt_translate.ML
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     3
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     4
Translate theorems into an SMT intermediate format and serialize them.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     6
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     7
signature SMT_TRANSLATE =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     9
  (* intermediate term structure *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    10
  datatype squant = SForall | SExists
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
  datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    12
  datatype sterm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    13
    SVar of int |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
    SApp of string * sterm list |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
    SLet of string * sterm * sterm |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
    SQua of squant * string list * sterm spattern list * sterm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
  (* configuration options *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
  type prefixes = {sort_prefix: string, func_prefix: string}
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    20
  type header = Proof.context -> term list -> string list
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
  type strict = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
    is_builtin_conn: string * typ -> bool,
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    23
    is_builtin_pred: Proof.context -> string * typ -> bool,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
    is_builtin_distinct: bool}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
  type builtins = {
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    26
    builtin_typ: Proof.context -> typ -> string option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    27
    builtin_num: Proof.context -> typ -> int -> string option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    28
    builtin_fun: Proof.context -> string * typ -> term list ->
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    29
      (string * term list) option }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
  type sign = {
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    31
    header: string list,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
    sorts: string list,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
    funcs: (string * (string list * string)) list }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
  type config = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
    prefixes: prefixes,
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    36
    header: header,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
    strict: strict option,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    38
    builtins: builtins,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
    serialize: string list -> sign -> sterm list -> string }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
  type recon = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
    typs: typ Symtab.table,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
    terms: term Symtab.table,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
    unfolds: thm list,
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    44
    assms: thm list }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
  val translate: config -> Proof.context -> string list -> thm list ->
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
    string * recon
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    49
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
structure SMT_Translate: SMT_TRANSLATE =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
(* intermediate term structure *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    54
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
datatype squant = SForall | SExists
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
datatype sterm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
  SVar of int |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
  SApp of string * sterm list |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
  SLet of string * sterm * sterm |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
  SQua of squant * string list * sterm spattern list * sterm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
(* configuration options *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
type prefixes = {sort_prefix: string, func_prefix: string}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    71
type header = Proof.context -> term list -> string list
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    72
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
type strict = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
  is_builtin_conn: string * typ -> bool,
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    75
  is_builtin_pred: Proof.context -> string * typ -> bool,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
  is_builtin_distinct: bool}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
type builtins = {
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    79
  builtin_typ: Proof.context -> typ -> string option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    80
  builtin_num: Proof.context -> typ -> int -> string option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    81
  builtin_fun: Proof.context -> string * typ -> term list ->
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    82
    (string * term list) option }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
type sign = {
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    85
  header: string list,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
  sorts: string list,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
  funcs: (string * (string list * string)) list }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
type config = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
  prefixes: prefixes,
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    91
  header: header,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
  strict: strict option,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
  builtins: builtins,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
  serialize: string list -> sign -> sterm list -> string }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    95
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
type recon = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    97
  typs: typ Symtab.table,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
  terms: term Symtab.table,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
  unfolds: thm list,
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   100
  assms: thm list }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   101
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   102
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   103
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
(* utility functions *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
val dest_funT =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
    fun dest Ts 0 T = (rev Ts, T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
      | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   110
      | dest _ _ T = raise TYPE ("dest_funT", [T], [])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
  in dest [] end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
val quantifier = (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
    @{const_name All} => SOME SForall
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
  | @{const_name Ex} => SOME SExists
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
  | _ => NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
      if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
  | group_quant _ Ts t = (Ts, t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   122
fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   123
  | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   124
  | dest_pat t = raise TERM ("dest_pat", [t])
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   125
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   126
fun dest_pats [] = I
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   127
  | dest_pats ts =
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   128
      (case map dest_pat ts |> split_list ||> distinct (op =) of
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   129
        (ps, [true]) => cons (SPat ps)
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   130
      | (ps, [false]) => cons (SNoPat ps)
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   131
      | _ => raise TERM ("dest_pats", ts))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
fun dest_trigger (@{term trigger} $ tl $ t) =
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   134
      (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
  | dest_trigger t = ([], t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
    val (Ts, u) = group_quant qn [T] t
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
    val (ps, b) = dest_trigger u
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
  in (q, rev Ts, ps, b) end)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
  | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
fun prop_of thm = HOLogic.dest_Trueprop (Thm.prop_of thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   148
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   150
(* enforce a strict separation between formulas and terms *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   151
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   152
val term_eq_rewr = @{lemma "term_eq x y == x = y" by (simp add: term_eq_def)}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   153
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   154
val term_bool = @{lemma "~(term_eq True False)" by (simp add: term_eq_def)}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   157
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   158
val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
    Const (@{const_name Let}, _) => true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
  | @{term "op = :: bool => _"} $ _ $ @{term True} => true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
  | Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   162
  | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   163
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   164
val rewrite_rules = [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   165
  Let_def,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   166
  @{lemma "P = True == P" by (rule eq_reflection) simp},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   167
  @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   168
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   169
fun rewrite ctxt = Simplifier.full_rewrite
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
  (Simplifier.context ctxt empty_ss addsimps rewrite_rules)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   171
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
fun normalize ctxt thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   173
  if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
val unfold_rules = term_eq_rewr :: rewrite_rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
val revert_types =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
    fun revert @{typ prop} = @{typ bool}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
      | revert (Type (n, Ts)) = Type (n, map revert Ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   182
      | revert T = T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
  in Term.map_types revert end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
    fun is_builtin_conn' (@{const_name True}, _) = false
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
      | is_builtin_conn' (@{const_name False}, _) = false
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
      | is_builtin_conn' c = is_builtin_conn c
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   192
    val propT = @{typ prop} and boolT = @{typ bool}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   193
    val as_propT = (fn @{typ bool} => propT | T => T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   194
    fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
    fun conn (n, T) = (n, mapTs as_propT as_propT T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
    fun pred (n, T) = (n, mapTs I as_propT T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   197
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   198
    val term_eq = @{term "op = :: bool => _"} |> Term.dest_Const |> pred
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   199
    fun as_term t = Const term_eq $ t $ @{term True}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   200
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   201
    val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   202
    fun wrap_in_if t = if_term $ t $ @{term True} $ @{term False}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   203
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   204
    fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   205
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
    fun in_term t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   207
      (case Term.strip_comb t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   208
        (c as Const (@{const_name If}, _), [t1, t2, t3]) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   209
          c $ in_form t1 $ in_term t2 $ in_term t3
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   210
      | (h as Const c, ts) =>
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   211
          if is_builtin_conn' (conn c) orelse is_builtin_pred ctxt (pred c)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   212
          then wrap_in_if (in_form t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   213
          else Term.list_comb (h, map in_term ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   214
      | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   215
      | _ => t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   217
    and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   218
      | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   219
      | in_pat t = raise TERM ("in_pat", [t])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   220
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   221
    and in_pats ps =
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36899
diff changeset
   222
      in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   223
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   224
    and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   225
      | in_trig t = in_form t
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   226
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   227
    and in_form t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   228
      (case Term.strip_comb t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   229
        (q as Const (qn, _), [Abs (n, T, t')]) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
          if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
          else as_term (in_term t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   232
      | (Const (c as (@{const_name distinct}, T)), [t']) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
          if is_builtin_distinct then Const (pred c) $ in_list T in_term t'
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
          else as_term (in_term t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
      | (Const c, ts) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   236
          if is_builtin_conn (conn c)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
          then Term.list_comb (Const (conn c), map in_form ts)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   238
          else if is_builtin_pred ctxt (pred c)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
          then Term.list_comb (Const (pred c), map in_term ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
          else as_term (in_term t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
      | _ => as_term (in_term t))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   242
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
    map (normalize ctxt) #> (fn thms => ((unfold_rules, term_bool' :: thms),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   244
    map (in_form o prop_of) (term_bool :: thms)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   245
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
(* translation from Isabelle terms into SMT intermediate terms *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   250
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   251
val empty_context = (1, Typtab.empty, 1, Termtab.empty)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   253
fun make_sign header (_, typs, _, terms) = {
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   254
  header = header,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   255
  sorts = Typtab.fold (cons o snd) typs [],
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   256
  funcs = Termtab.fold (cons o snd) terms [] }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   258
fun make_recon (unfolds, assms) (_, typs, _, terms) = {
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
  typs = Symtab.make (map swap (Typtab.dest typs)),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   260
  terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   261
  unfolds = unfolds,
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   262
  assms = assms }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   263
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
fun string_of_index pre i = pre ^ string_of_int i
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   265
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   266
fun fresh_typ sort_prefix T (cx as (Tidx, typs, idx, terms)) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   267
  (case Typtab.lookup typs T of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
    SOME s => (s, cx)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
  | NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   270
      let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   271
        val s = string_of_index sort_prefix Tidx
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
        val typs' = Typtab.update (T, s) typs
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   273
      in (s, (Tidx+1, typs', idx, terms)) end)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   275
fun fresh_fun func_prefix t ss (cx as (Tidx, typs, idx, terms)) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
  (case Termtab.lookup terms t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
    SOME (f, _) => (f, cx)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   278
  | NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
      let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
        val f = string_of_index func_prefix idx
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   281
        val terms' = Termtab.update (revert_types t, (f, ss)) terms
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   282
      in (f, (Tidx, typs, idx+1, terms')) end)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   283
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   284
fun relaxed thms = (([], thms), map prop_of thms)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   286
fun with_context header f (ths, ts) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
  let val (us, context) = fold_map f ts empty_context
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   288
  in ((make_sign (header ts) context, us), make_recon ths context) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   289
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   290
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   291
fun translate {prefixes, strict, header, builtins, serialize} ctxt comments =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   292
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   293
    val {sort_prefix, func_prefix} = prefixes
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   294
    val {builtin_typ, builtin_num, builtin_fun} = builtins
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   295
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   296
    fun transT T =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   297
      (case builtin_typ ctxt T of
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   298
        SOME n => pair n
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   299
      | NONE => fresh_typ sort_prefix T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   300
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
    fun app n ts = SApp (n, ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
    fun trans t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   304
      (case Term.strip_comb t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   305
        (Const (qn, _), [Abs (_, T, t1)]) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
          (case dest_quant qn T t1 of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   307
            SOME (q, Ts, ps, b) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   308
              fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   309
              trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   310
          | NONE => raise TERM ("intermediate", [t]))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   311
      | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   312
          transT T ##>> trans t1 ##>> trans t2 #>>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   313
          (fn ((U, u1), u2) => SLet (U, u1, u2))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   314
      | (h as Const (c as (@{const_name distinct}, T)), [t1]) =>
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   315
          (case builtin_fun ctxt c (HOLogic.dest_list t1) of
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   316
            SOME (n, ts) => fold_map trans ts #>> app n
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   317
          | NONE => transs h T [t1])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   318
      | (h as Const (c as (_, T)), ts) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   319
          (case try HOLogic.dest_number t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   320
            SOME (T, i) =>
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   321
              (case builtin_num ctxt T i of
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   322
                SOME n => pair (SApp (n, []))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   323
              | NONE => transs t T [])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   324
          | NONE =>
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   325
              (case builtin_fun ctxt c ts of
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   326
                SOME (n, ts') => fold_map trans ts' #>> app n
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   327
              | NONE => transs h T ts))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   328
      | (h as Free (_, T), ts) => transs h T ts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   329
      | (Bound i, []) => pair (SVar i)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   330
      | _ => raise TERM ("intermediate", [t]))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   331
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   332
    and transs t T ts =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   333
      let val (Us, U) = dest_funT (length ts) T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   334
      in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   335
        fold_map transT Us ##>> transT U #-> (fn Up =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   336
        fresh_fun func_prefix t Up ##>> fold_map trans ts #>> SApp)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   337
      end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   338
  in
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   339
    (case strict of SOME strct => strictify strct ctxt | NONE => relaxed) #>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   340
    with_context (header ctxt) trans #>> uncurry (serialize comments)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   341
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   342
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   343
end