src/HOL/Tools/SMT/smt_monomorph.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 36898 8e55aa1306c5
child 38864 4abe644fcea5
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_monomorph.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
Monomorphization of theorems, i.e., computation of all (necessary) instances.
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_MONOMORPH =
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
  val monomorph: thm list -> Proof.context -> thm list * Proof.context
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    10
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    12
structure SMT_Monomorph: SMT_MONOMORPH =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    13
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
val ignored = member (op =) [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
  @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
  @{const_name "op ="}, @{const_name zero_class.zero},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
  @{const_name one_class.one}, @{const_name number_of}]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
fun is_const f (n, T) = not (ignored n) andalso f T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
fun add_const_if f g (Const c) = if is_const f c then g c else I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
  | add_const_if _ _ _ = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
fun collect_consts_if f g thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    27
  Term.fold_aterms (add_const_if f g) (Thm.prop_of thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    28
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    29
fun add_consts f =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
  collect_consts_if f (fn (n, T) => Symtab.map_entry n (insert (op =) T))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
val insert_const = OrdList.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
fun incr_indexes thms =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
  let fun inc thm idx = (Thm.incr_indexes idx thm, Thm.maxidx_of thm + idx + 1)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    38
  in fst (fold_map inc thms 0) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
(* Compute all substitutions from the types "Ts" to all relevant
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
   types in "grounds", with respect to the given substitution. *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
fun new_substitutions thy grounds (n, T) subst =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
  if not (typ_has_tvars T) then [subst]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
  else
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
    Symtab.lookup_list grounds n
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
    |> map_filter (try (fn U => Sign.typ_match thy (T, U) subst))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
    |> cons subst
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    49
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
(* Instantiate a set of constants with a substitution.  Also collect
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
   all new ground instances for the next round of specialization. *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
fun apply_subst grounds consts subst =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    54
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
    fun is_new_ground (n, T) = not (typ_has_tvars T) andalso
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
      not (member (op =) (Symtab.lookup_list grounds n) T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
    fun apply_const (n, T) new_grounds =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
      let val c = (n, Envir.subst_type subst T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
      in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
        new_grounds
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
        |> is_new_ground c ? Symtab.insert_list (op =) c
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
        |> pair c
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
      end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
  in fold_map apply_const consts #>> pair subst end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
(* Compute new substitutions for the theorem "thm", based on
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
   previously found substitutions.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
     Also collect new grounds, i.e., instantiated constants
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    71
   (without schematic types) which do not occur in any of the
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
   previous rounds. Note that thus no schematic type variables are
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
   shared among theorems. *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
fun specialize thy all_grounds new_grounds (thm, scs) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    75
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
    fun spec (subst, consts) next_grounds =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
      [subst]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
      |> fold (maps o new_substitutions thy new_grounds) consts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
      |> rpair next_grounds
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
      |-> fold_map (apply_subst all_grounds consts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    81
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
    fold_map spec scs #>> (fn scss =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
    (thm, fold (fold (insert (eq_snd (op =)))) scss []))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
(* Compute all necessary substitutions.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
     Instead of operating on the propositions of the theorems, the
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
   computation uses only the constants occurring with schematic type
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
   variables in the propositions. To ease comparisons, such sets of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
   costants are always kept in their initial order. *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
fun incremental_monomorph thy limit all_grounds new_grounds ths =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
    val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    95
    val spec = specialize thy all_grounds' new_grounds
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
    val (ths', new_grounds') = fold_map spec ths Symtab.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    97
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
    if Symtab.is_empty new_grounds' then ths'
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
    else if limit > 0
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   100
    then incremental_monomorph thy (limit-1) all_grounds' new_grounds' ths'
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   101
    else (warning "SMT: monomorphization limit reached"; ths')
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   102
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   103
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
fun filter_most_specific thy =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
    fun typ_match (_, T) (_, U) = Sign.typ_match thy (T, U)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
    fun is_trivial subst = Vartab.is_empty subst orelse
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   110
      forall (fn (v, (S, T)) => TVar (v, S) = T) (Vartab.dest subst)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
    fun match general specific =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
      (case try (fold2 typ_match general specific) Vartab.empty of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
        NONE => false
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
      | SOME subst => not (is_trivial subst))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
    fun most_specific _ [] = []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
      | most_specific css ((ss, cs) :: scs) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
          let val substs = most_specific (cs :: css) scs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
          in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
            if exists (match cs) css orelse exists (match cs o snd) scs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
            then substs else ss :: substs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
          end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
  in most_specific [] end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
fun instantiate thy Tenv =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
    fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
      | replace _ T = T
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 complete (vT as (v, _)) subst =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
      subst
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
      |> not (Vartab.defined subst v) ? Vartab.update vT
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
      |> Vartab.map (apsnd (Term.map_atyps (replace vT)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
    fun inst thm subst =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
      let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
      in Thm.instantiate (cTs, []) thm end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
  in uncurry (map o inst) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
fun mono_all ctxt _ [] monos = (monos, ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   148
  | mono_all ctxt limit polys monos =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
      let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   150
        fun invent_types thm ctxt =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   151
          let val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) [])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   152
          in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   153
            ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
            |> Variable.invent_types Ss
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
            |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
          end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   157
        val (Tenvs, ctxt') = fold_map invent_types polys ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   158
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
        val thy = ProofContext.theory_of ctxt'
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
        val ths = polys
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   162
          |> map (fn thm => (thm, [(Vartab.empty, tvar_consts_of thm)]))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   163
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   164
        (* all constant names occurring with schematic types *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   165
        val ns = fold (fold (fold (insert (op =) o fst) o snd) o snd) ths []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   166
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   167
        (* all known instances with non-schematic types *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   168
        val grounds =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   169
          Symtab.make (map (rpair []) ns)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
          |> fold (add_consts (K true)) monos
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   171
          |> fold (add_consts (not o typ_has_tvars)) polys
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
      in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   173
        polys
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
        |> map (fn thm => (thm, [(Vartab.empty, tvar_consts_of thm)]))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
        |> incremental_monomorph thy limit Symtab.empty grounds
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
        |> map (apsnd (filter_most_specific thy))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
        |> flat o map2 (instantiate thy) Tenvs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
        |> append monos
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
        |> rpair ctxt'
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
      end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   182
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
val monomorph_limit = 10
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
(* Instantiate all polymorphic constants (i.e., constants occurring
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
   both with ground types and type variables) with all (necessary)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
   ground types; thereby create copies of theorems containing those
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
   constants.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
     To prevent non-termination, there is an upper limit for the
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
   number of recursions involved in the fixpoint construction.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   192
     The initial set of theorems must not contain any schematic term
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   193
   variables, and the final list of theorems does not contain any
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   194
   schematic type variables anymore. *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
fun monomorph thms ctxt =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
  thms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   197
  |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   198
  |>> incr_indexes
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   199
  |-> mono_all ctxt monomorph_limit
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   200
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   201
end