author blanchet Thu May 24 15:01:29 2012 +0200 (2012-05-24) changeset 47981 df35a8dd6368 parent 47977 455a9f89c47d child 47984 a1a5bf806d8b
gracefully handle definition-looking premises
```     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 24 13:56:21 2012 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 24 15:01:29 2012 +0200
1.3 @@ -819,19 +819,18 @@
1.4      in HOLogic.eq_const head_T \$ head \$ fold lam arg_Ts u end
1.5    | intentionalize_def t = t
1.6
1.7 -type translated_formula =
1.8 +type ifact =
1.9    {name : string,
1.10     stature : stature,
1.11     role : formula_role,
1.12     iformula : (name, typ, iterm) formula,
1.13     atomic_types : typ list}
1.14
1.15 -fun update_iformula f ({name, stature, role, iformula, atomic_types}
1.16 -                       : translated_formula) =
1.17 +fun update_iformula f ({name, stature, role, iformula, atomic_types} : ifact) =
1.18    {name = name, stature = stature, role = role, iformula = f iformula,
1.19 -   atomic_types = atomic_types} : translated_formula
1.20 +   atomic_types = atomic_types} : ifact
1.21
1.22 -fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
1.23 +fun ifact_lift f ({iformula, ...} : ifact) = f iformula
1.24
1.25  fun insert_type thy get_T x xs =
1.26    let val T = get_T x in
1.27 @@ -1327,8 +1326,17 @@
1.28
1.29  fun make_conjecture ctxt format type_enc =
1.30    map (fn ((name, stature), (role, t)) =>
1.31 -          t |> role = Conjecture ? s_not
1.32 -            |> make_formula ctxt format type_enc true name stature role)
1.33 +          let
1.34 +            val role =
1.35 +              if is_type_enc_higher_order type_enc andalso
1.36 +                 role <> Conjecture andalso is_legitimate_thf_def t then
1.37 +                Definition
1.38 +              else
1.39 +                role
1.40 +          in
1.41 +            t |> role = Conjecture ? s_not
1.42 +              |> make_formula ctxt format type_enc true name stature role
1.43 +          end)
1.44
1.45  (** Finite and infinite type inference **)
1.46
1.47 @@ -1575,7 +1583,7 @@
1.49        add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true
1.51 -      K (add_iterm_syms conj_fact) |> formula_fold NONE |> fact_lift
1.52 +      K (add_iterm_syms conj_fact) |> formula_fold NONE |> ifact_lift
1.53    in
1.54      ((false, []), Symtab.empty)
1.55      |> fold (add_fact_syms true) conjs
1.56 @@ -1893,29 +1901,30 @@
1.57    else
1.58      error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
1.59
1.60 -fun order_definitions facts =
1.61 +val pull_and_reorder_definitions =
1.62    let
1.65        | add_consts (IConst (name, _, _)) = insert (op =) name
1.66        | add_consts (IVar _) = I
1.67 -    fun consts_of_hs l_or_r (_, {iformula, ...} : translated_formula) =
1.68 +    fun consts_of_hs l_or_r ({iformula, ...} : ifact) =
1.69        case iformula of
1.70          AAtom (IApp (IApp (IConst _, t), u)) => add_consts (l_or_r (t, u)) []
1.71        | _ => []
1.72      (* Quadratic, but usually OK. *)
1.73 -    fun order [] [] = []
1.74 -      | order (fact :: skipped) [] = fact :: order [] skipped (* break cycle *)
1.75 -      | order skipped (fact :: facts) =
1.76 +    fun reorder [] [] = []
1.77 +      | reorder (fact :: skipped) [] =
1.78 +        fact :: reorder [] skipped (* break cycle *)
1.79 +      | reorder skipped (fact :: facts) =
1.80          let val rhs_consts = consts_of_hs snd fact in
1.81            if exists (exists (member (op =) rhs_consts o the_single
1.82                       o consts_of_hs fst))
1.83                      [skipped, facts] then
1.84 -            order (fact :: skipped) facts
1.85 +            reorder (fact :: skipped) facts
1.86            else
1.87 -            fact :: order [] (facts @ skipped)
1.88 +            fact :: reorder [] (facts @ skipped)
1.89          end
1.90 -  in order [] facts end
1.91 +  in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end
1.92
1.93  fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts
1.94                         concl_t facts =
1.95 @@ -1943,15 +1952,15 @@
1.96              op @
1.97              #> preprocess_abstractions_in_terms trans_lams
1.98              #>> chop (length conjs))
1.99 -    val conjs = conjs |> make_conjecture ctxt format type_enc
1.100 -    val (fact_names, facts) =
1.101 -      facts
1.102 -      |> map_filter (fn (name, (_, t)) =>
1.103 -                        make_fact ctxt format type_enc true (name, t)
1.104 -                        |> Option.map (pair name))
1.105 -      |> List.partition (fn (_, {role, ...}) => role = Definition)
1.106 -      |>> order_definitions
1.107 -      |> op @ |> ListPair.unzip
1.108 +    val conjs =
1.109 +      conjs |> make_conjecture ctxt format type_enc
1.110 +            |> pull_and_reorder_definitions
1.111 +    val facts =
1.112 +      facts |> map_filter (fn (name, (_, t)) =>
1.113 +                              make_fact ctxt format type_enc true (name, t))
1.114 +            |> pull_and_reorder_definitions
1.115 +    val fact_names =
1.116 +      facts |> map (fn {name, stature, ...} : ifact => (name, stature))
1.117      val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
1.118      val lam_facts =
1.119        lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
1.120 @@ -2157,7 +2166,7 @@
1.121             NONE, isabelle_info inductiveN helper_rank)
1.122
1.123  fun formula_line_for_conjecture ctxt polym_constrs mono type_enc
1.124 -        ({name, role, iformula, atomic_types, ...} : translated_formula) =
1.125 +        ({name, role, iformula, atomic_types, ...} : ifact) =
1.126    Formula (conjecture_prefix ^ name, role,
1.127             iformula
1.128             |> formula_from_iformula ctxt polym_constrs mono type_enc
1.129 @@ -2171,7 +2180,7 @@
1.130
1.131  fun formula_line_for_free_type j phi =
1.132    Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
1.133 -fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
1.134 +fun formula_lines_for_free_types type_enc (facts : ifact list) =
1.135    if type_enc_needs_free_types type_enc then
1.136      let
1.137        val phis =
1.138 @@ -2230,7 +2239,7 @@
1.139           | _ => I)
1.141        end
1.142 -    val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
1.143 +    val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> ifact_lift
1.144      fun add_formula_var_types (AQuant (_, xs, phi)) =
1.145          fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
1.147 @@ -2239,7 +2248,7 @@
1.148        | add_formula_var_types _ = I
1.149      fun var_types () =
1.150        if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
1.151 -      else fold (fact_lift add_formula_var_types) (conjs @ facts) []
1.152 +      else fold (ifact_lift add_formula_var_types) (conjs @ facts) []
1.154        let
1.155          val (s, s') =
1.156 @@ -2329,8 +2338,7 @@
1.157          mono
1.158      end
1.159    | add_iterm_mononotonicity_info _ _ _ _ mono = mono
1.161 -        ({role, iformula, ...} : translated_formula) =
1.162 +fun add_fact_mononotonicity_info ctxt level ({role, iformula, ...} : ifact) =
1.163    formula_fold (SOME (role <> Conjecture))
1.165  fun mononotonicity_info_for_facts ctxt type_enc facts =
1.166 @@ -2351,7 +2359,7 @@
1.168    in formula_fold NONE (K add_term) end
1.169  fun add_fact_monotonic_types ctxt mono type_enc =
1.170 -  add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
1.171 +  add_iformula_monotonic_types ctxt mono type_enc |> ifact_lift
1.172  fun monotonic_types_for_facts ctxt mono type_enc facts =
1.173    let val level = level_of_type_enc type_enc in
1.174      [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
```
```     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu May 24 13:56:21 2012 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 24 15:01:29 2012 +0200
2.3 @@ -363,7 +363,7 @@
2.4     proof_delims =
2.5       [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
2.6     known_failures = known_szs_status_failures,
2.7 -   prem_role = Definition (* motivated by "isabelle tptp_sledgehammer" tool *),
2.8 +   prem_role = Hypothesis,
2.9     best_slices =
2.10       (* FUDGE *)
2.11       K [(1.0, (true, ((120, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))],
```