gracefully handle definition-looking premises
authorblanchet
Thu May 24 15:01:29 2012 +0200 (2012-05-24)
changeset 47981df35a8dd6368
parent 47977 455a9f89c47d
child 47984 a1a5bf806d8b
gracefully handle definition-looking premises
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_systems.ML
     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.48      fun add_iterm_syms conj_fact =
    1.49        add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true
    1.50      fun add_fact_syms conj_fact =
    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.63      fun add_consts (IApp (t, u)) = fold add_consts [t, u]
    1.64        | add_consts (IAbs (_, t)) = add_consts t
    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.140          #> fold add_iterm_syms args
   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.146          #> add_formula_var_types phi
   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.153      fun add_undefined_const T =
   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.160 -fun add_fact_mononotonicity_info ctxt level
   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.164                 (add_iterm_mononotonicity_info ctxt level) iformula
   1.165  fun mononotonicity_info_for_facts ctxt type_enc facts =
   1.166 @@ -2351,7 +2359,7 @@
   1.167      and add_term tm = add_type (ityp_of tm) #> add_args tm
   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), "")))],