generate THF definitions
authorblanchet
Wed May 23 21:19:48 2012 +0200 (2012-05-23)
changeset 479712aea51a14200
parent 47970 257fc09aa8a1
child 47972 96c9b8381909
generate THF definitions
src/HOL/Tools/ATP/atp_problem_generate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 23 17:57:28 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 23 21:19:48 2012 +0200
     1.3 @@ -1297,11 +1297,26 @@
     1.4       atomic_types = atomic_Ts}
     1.5    end
     1.6  
     1.7 -fun make_fact ctxt format type_enc iff_for_eq ((name, stature), t) =
     1.8 -  case t |> make_formula ctxt format type_enc iff_for_eq name stature Axiom of
     1.9 -    formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
    1.10 -    if s = tptp_true then NONE else SOME formula
    1.11 -  | formula => SOME formula
    1.12 +fun is_legitimate_thf_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
    1.13 +    (is_Const t orelse is_Free t) andalso
    1.14 +    not (exists_subterm (curry (op =) t) u)
    1.15 +  | is_legitimate_thf_def _ = false
    1.16 +
    1.17 +fun make_fact ctxt format type_enc iff_for_eq
    1.18 +              ((name, stature as (_, status)), t) =
    1.19 +  let
    1.20 +    val role =
    1.21 +      if is_type_enc_higher_order type_enc andalso status = Def andalso
    1.22 +         is_legitimate_thf_def t then
    1.23 +        Definition
    1.24 +      else
    1.25 +        Axiom
    1.26 +  in
    1.27 +    case t |> make_formula ctxt format type_enc iff_for_eq name stature role of
    1.28 +      formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
    1.29 +      if s = tptp_true then NONE else SOME formula
    1.30 +    | formula => SOME formula
    1.31 +  end
    1.32  
    1.33  fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
    1.34    | s_not_prop _ = @{prop True} (* "t" is too meta for "metis" *)
    1.35 @@ -2878,8 +2893,7 @@
    1.36          else
    1.37            I
    1.38        | add_eq_deps _ _ = I
    1.39 -    fun has_status status (_, info) =
    1.40 -      extract_isabelle_status info = SOME status
    1.41 +    fun has_status status (_, info) = extract_isabelle_status info = SOME status
    1.42      fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
    1.43      val graph =
    1.44        Graph.empty