src/HOL/Tools/ATP/atp_translate.ML
changeset 44450 d848dd7b21f4
parent 44418 800baa1b1406
child 44460 5d0754cf994a
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 22:44:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 23:18:13 2011 +0200
     1.3 @@ -165,8 +165,8 @@
     1.4  val untyped_helper_suffix = "_U"
     1.5  val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
     1.6  
     1.7 -val predicator_name = "hBOOL"
     1.8 -val app_op_name = "hAPP"
     1.9 +val predicator_name = "p"
    1.10 +val app_op_name = "a"
    1.11  val type_guard_name = "g"
    1.12  val type_tag_name = "t"
    1.13  val simple_type_prefix = "ty_"
    1.14 @@ -1151,7 +1151,7 @@
    1.15        | homo _ _ = raise Fail "expected function type"
    1.16    in homo end
    1.17  
    1.18 -(** "hBOOL" and "hAPP" **)
    1.19 +(** predicators and application operators **)
    1.20  
    1.21  type sym_info =
    1.22    {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
    1.23 @@ -1194,6 +1194,8 @@
    1.24             if String.isPrefix bound_var_prefix s orelse
    1.25                String.isPrefix all_bound_var_prefix s then
    1.26               add_universal_var T accum
    1.27 +           else if String.isPrefix exist_bound_var_prefix s then
    1.28 +             accum
    1.29             else
    1.30               let val ary = length args in
    1.31                 ((bool_vars, fun_var_Ts),
    1.32 @@ -1238,8 +1240,8 @@
    1.33        end
    1.34    in add true end
    1.35  fun add_fact_syms_to_table ctxt explicit_apply =
    1.36 -  fact_lift (formula_fold NONE
    1.37 -                          (K (add_iterm_syms_to_table ctxt explicit_apply)))
    1.38 +  formula_fold NONE (K (add_iterm_syms_to_table ctxt explicit_apply))
    1.39 +  |> fact_lift
    1.40  
    1.41  val tvar_a = TVar (("'a", 0), HOLogic.typeS)
    1.42  
    1.43 @@ -1379,6 +1381,9 @@
    1.44  
    1.45  (** Helper facts **)
    1.46  
    1.47 +val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
    1.48 +val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
    1.49 +
    1.50  (* The Boolean indicates that a fairly sound type encoding is needed. *)
    1.51  val helper_table =
    1.52    [(("COMBI", false), @{thms Meson.COMBI_def}),
    1.53 @@ -1386,9 +1391,10 @@
    1.54     (("COMBB", false), @{thms Meson.COMBB_def}),
    1.55     (("COMBC", false), @{thms Meson.COMBC_def}),
    1.56     (("COMBS", false), @{thms Meson.COMBS_def}),
    1.57 -   (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
    1.58 +   ((predicator_name, false), [not_ffalse, ftrue]),
    1.59 +   (("fFalse", false), [not_ffalse]),
    1.60     (("fFalse", true), @{thms True_or_False}),
    1.61 -   (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
    1.62 +   (("fTrue", false), [ftrue]),
    1.63     (("fTrue", true), @{thms True_or_False}),
    1.64     (("fNot", false),
    1.65      @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    1.66 @@ -1754,9 +1760,7 @@
    1.67    (case type_enc of
    1.68       Guards _ => not pred_sym
    1.69     | _ => true) andalso
    1.70 -  is_tptp_user_symbol s andalso
    1.71 -  forall (fn prefix => not (String.isPrefix prefix s))
    1.72 -         [bound_var_prefix, all_bound_var_prefix, exist_bound_var_prefix]
    1.73 +  is_tptp_user_symbol s
    1.74  
    1.75  fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
    1.76                               (conjs, facts) =