--- a/src/HOL/Tools/ATP/atp_translate.ML Mon Oct 31 17:51:01 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Oct 31 17:51:01 2011 +0100
@@ -466,7 +466,7 @@
| stripc x = x
in stripc (u, []) end
-fun atyps_of T = fold_atyps (insert (op =)) T []
+fun atomic_types_of T = fold_atyps (insert (op =)) T []
fun new_skolem_const_name s num_T_args =
[new_skolem_const_prefix, s, string_of_int num_T_args]
@@ -491,11 +491,11 @@
| iterm_from_term thy format _ (Const (c, T)) =
(IConst (`(make_fixed_const (SOME format)) c, T,
robust_const_typargs thy (c, T)),
- atyps_of T)
+ atomic_types_of T)
| iterm_from_term _ _ _ (Free (s, T)) =
(IConst (`make_fixed_var s, T,
if String.isPrefix polymorphic_free_prefix s then [T] else []),
- atyps_of T)
+ atomic_types_of T)
| iterm_from_term _ format _ (Var (v as (s, _), T)) =
(if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
let
@@ -503,16 +503,16 @@
val s' = new_skolem_const_name s (length Ts)
in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
else
- IVar ((make_schematic_var v, s), T), atyps_of T)
+ IVar ((make_schematic_var v, s), T), atomic_types_of T)
| iterm_from_term _ _ bs (Bound j) =
- nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atyps_of T))
+ nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
| iterm_from_term thy format bs (Abs (s, T, t)) =
let
fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
val s = vary s
val name = `make_bound_var s
val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
- in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
+ in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
datatype locality =
General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
@@ -780,13 +780,10 @@
fun add_term_vars type_enc =
let
fun vars bounds (ATerm (name as (s, _), tms)) =
- (if is_tptp_variable s andalso not (member (op =) bounds name) then
- (case type_enc of
- Simple_Types (_, Polymorphic, _) =>
- if String.isPrefix tvar_prefix s then SOME atype_of_types
- else NONE
- | _ => NONE)
- |> pair name |> insert (op =)
+ (if is_tptp_variable s andalso
+ not (String.isPrefix tvar_prefix s) andalso
+ not (member (op =) bounds name) then
+ insert (op =) (name, NONE)
else
I)
#> fold (vars bounds) tms
@@ -1015,12 +1012,12 @@
fun iformula_from_prop ctxt format type_enc eq_as_iff =
let
val thy = Proof_Context.theory_of ctxt
- fun do_term bs t atomic_types =
+ fun do_term bs t atomic_Ts =
iterm_from_term thy format bs (Envir.eta_contract t)
|>> (introduce_proxies_in_iterm type_enc
#> mangle_type_args_in_iterm format type_enc
#> AAtom)
- ||> union (op =) atomic_types
+ ||> union (op =) atomic_Ts
fun do_quant bs q pos s T t' =
let
val s = singleton (Name.variant_list (map fst bs)) s
@@ -1033,6 +1030,7 @@
in
do_formula ((s, (name, T)) :: bs) pos t'
#>> mk_aquant q [(name, SOME T)]
+ ##> union (op =) (atomic_types_of T)
end
and do_conn bs c pos1 t1 pos2 t2 =
do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
@@ -1177,15 +1175,15 @@
handle TERM _ => if role = Conjecture then @{term False} else @{term True})
|> pair role
-(* making fact and conjecture formulas *)
fun make_formula ctxt format type_enc eq_as_iff name loc kind t =
let
- val (iformula, atomic_types) =
+ val (iformula, atomic_Ts) =
iformula_from_prop ctxt format type_enc eq_as_iff
(SOME (kind <> Conjecture)) t []
+ |>> close_iformula_universally
in
{name = name, locality = loc, kind = kind, iformula = iformula,
- atomic_types = atomic_types}
+ atomic_types = atomic_Ts}
end
fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
@@ -1529,8 +1527,13 @@
(("If", true), @{thms if_True if_False True_or_False})]
|> map (apsnd (map zero_var_indexes))
-fun bound_tvars type_enc =
- mk_ahorn o formulas_for_types type_enc add_sorts_on_tvar
+fun bound_tvars type_enc Ts =
+ mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts)
+ #> mk_aquant AForall
+ (map_filter (fn TVar (x as (s, _), _) =>
+ SOME ((make_schematic_type_var x, s),
+ SOME atype_of_types)
+ | _ => NONE) Ts)
fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
(if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
@@ -1820,7 +1823,6 @@
(j, {name, locality, kind, iformula, atomic_types}) =
(prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
iformula
- |> close_iformula_universally
|> formula_from_iformula ctxt format mono type_enc
should_guard_var_in_formula
(if pos then SOME true else NONE)
@@ -1860,9 +1862,9 @@
fun formula_line_for_conjecture ctxt format mono type_enc
({name, kind, iformula, atomic_types, ...} : translated_formula) =
Formula (conjecture_prefix ^ name, kind,
- formula_from_iformula ctxt format mono type_enc
- should_guard_var_in_formula (SOME false)
- (close_iformula_universally iformula)
+ iformula
+ |> formula_from_iformula ctxt format mono type_enc
+ should_guard_var_in_formula (SOME false)
|> close_formula_universally type_enc
|> bound_tvars type_enc atomic_types, NONE, NONE)
@@ -2055,7 +2057,7 @@
|> formula_from_iformula ctxt format mono type_enc
(K (K (K (K (K (K true)))))) (SOME true)
|> close_formula_universally type_enc
- |> bound_tvars type_enc (atyps_of T),
+ |> bound_tvars type_enc (atomic_types_of T),
isabelle_info format introN, NONE)
fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
@@ -2063,7 +2065,7 @@
Formula (tags_sym_formula_prefix ^
ascii_of (mangled_type format type_enc T),
Axiom,
- eq_formula type_enc (atyps_of T) false
+ eq_formula type_enc (atomic_types_of T) false
(tag_with_type ctxt format mono type_enc NONE T x_var)
x_var,
isabelle_info format simpN, NONE)
@@ -2138,7 +2140,7 @@
|> formula_from_iformula ctxt format mono type_enc
(K (K (K (K (K (K true)))))) (SOME true)
|> close_formula_universally type_enc
- |> n > 1 ? bound_tvars type_enc (atyps_of T)
+ |> n > 1 ? bound_tvars type_enc (atomic_types_of T)
|> maybe_negate,
isabelle_info format introN, NONE)
end
@@ -2159,7 +2161,7 @@
val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
val bounds = bound_names |> map (fn name => ATerm (name, []))
val cst = mk_aterm format type_enc (s, s') T_args
- val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
+ val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) pred_sym
val should_encode = should_encode_type ctxt mono level
val tag_with = tag_with_type ctxt format mono type_enc NONE
val add_formula_for_res =