1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -1422,17 +1422,35 @@
     1.4     (("If", true), @{thms if_True if_False True_or_False})]
     1.5    |> map (apsnd (map zero_var_indexes))
     1.6  
     1.7 +fun fo_literal_from_type_literal (TyLitVar (class, name)) =
     1.8 +    (true, ATerm (class, [ATerm (name, [])]))
     1.9 +  | fo_literal_from_type_literal (TyLitFree (class, name)) =
    1.10 +    (true, ATerm (class, [ATerm (name, [])]))
    1.11 +
    1.12 +fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
    1.13 +
    1.14 +fun bound_tvars type_enc Ts =
    1.15 +  mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
    1.16 +                (type_literals_for_types type_enc add_sorts_on_tvar Ts))
    1.17 +
    1.18 +fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
    1.19 +  (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
    1.20 +   else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
    1.21 +  |> bound_tvars type_enc atomic_Ts
    1.22 +  |> close_formula_universally
    1.23 +
    1.24  val type_tag = `make_fixed_const type_tag_name
    1.25  
    1.26 -fun type_tag_idempotence_fact () =
    1.27 +fun type_tag_idempotence_fact type_enc =
    1.28    let
    1.29      fun var s = ATerm (`I s, [])
    1.30 +    (* Reconstruction in Metis is strangely dependent on these names. *)
    1.31      fun tag tm = ATerm (type_tag, [var "T", tm])
    1.32      val tagged_a = tag (var "A")
    1.33    in
    1.34      Formula (type_tag_idempotence_helper_name, Axiom,
    1.35 -             AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a]))
    1.36 -             |> close_formula_universally, isabelle_info simpN, NONE)
    1.37 +             eq_formula type_enc [] false (tag tagged_a) tagged_a,
    1.38 +             isabelle_info simpN, NONE)
    1.39    end
    1.40  
    1.41  fun should_specialize_helper type_enc t =
    1.42 @@ -1569,13 +1587,6 @@
    1.43       (conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
    1.44    end
    1.45  
    1.46 -fun fo_literal_from_type_literal (TyLitVar (class, name)) =
    1.47 -    (true, ATerm (class, [ATerm (name, [])]))
    1.48 -  | fo_literal_from_type_literal (TyLitFree (class, name)) =
    1.49 -    (true, ATerm (class, [ATerm (name, [])]))
    1.50 -
    1.51 -fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
    1.52 -
    1.53  val type_guard = `make_fixed_const type_guard_name
    1.54  
    1.55  fun type_guard_iterm ctxt format type_enc T tm =
    1.56 @@ -1591,6 +1602,11 @@
    1.57    | should_guard_var_in_formula pos phi _ name =
    1.58      formula_fold pos (is_var_positively_naked_in_term name) phi false
    1.59  
    1.60 +fun should_generate_tag_equation _ _ _ (SOME true) _ = false
    1.61 +  | should_generate_tag_equation ctxt mono (Tags (_, level, Nonuniform)) _ T =
    1.62 +    should_encode_type ctxt mono level T
    1.63 +  | should_generate_tag_equation _ _ _ _ _ = false
    1.64 +
    1.65  fun mk_aterm format type_enc name T_args args =
    1.66    ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
    1.67  
    1.68 @@ -1647,6 +1663,8 @@
    1.69          IVar (name, T)
    1.70          |> type_guard_iterm ctxt format type_enc T
    1.71          |> do_term pos |> AAtom |> SOME
    1.72 +      else if should_generate_tag_equation ctxt mono type_enc universal T then
    1.73 +        NONE (*###*)
    1.74        else
    1.75          NONE
    1.76      fun do_formula pos (AQuant (q, xs, phi)) =
    1.77 @@ -1668,10 +1686,6 @@
    1.78        | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
    1.79    in do_formula end
    1.80  
    1.81 -fun bound_tvars type_enc Ts =
    1.82 -  mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
    1.83 -                (type_literals_for_types type_enc add_sorts_on_tvar Ts))
    1.84 -
    1.85  (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    1.86     of monomorphization). The TPTP explicitly forbids name clashes, and some of
    1.87     the remote provers might care. *)
    1.88 @@ -1877,12 +1891,6 @@
    1.89             |> close_formula_universally,
    1.90             isabelle_info introN, NONE)
    1.91  
    1.92 -fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
    1.93 -  (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
    1.94 -   else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
    1.95 -  |> bound_tvars type_enc atomic_Ts
    1.96 -  |> close_formula_universally
    1.97 -
    1.98  fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
    1.99    let val x_var = ATerm (`make_bound_var "X", []) in
   1.100      Formula (tags_sym_formula_prefix ^
   1.101 @@ -2124,7 +2132,7 @@
   1.102        |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
   1.103                                      type_enc)
   1.104        |> (if needs_type_tag_idempotence type_enc then
   1.105 -            cons (type_tag_idempotence_fact ())
   1.106 +            cons (type_tag_idempotence_fact type_enc)
   1.107            else
   1.108              I)
   1.109      (* Reordering these might confuse the proof reconstruction code or the SPASS