1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 16:38:36 2011 +0200
1.3 @@ -114,7 +114,7 @@
1.4 val type_consts_of_terms : theory -> term list -> string list
1.5 val prepare_atp_problem :
1.6 Proof.context -> format -> formula_kind -> formula_kind -> type_system
1.7 - -> bool option -> bool -> term list -> term
1.8 + -> bool option -> bool -> bool -> term list -> term
1.9 -> (translated_formula option * ((string * 'a) * thm)) list
1.10 -> string problem * string Symtab.table * int * int
1.11 * (string * 'a) list vector * int list * int Symtab.table
1.12 @@ -796,7 +796,8 @@
1.13 #>> uncurry (mk_aconn c)
1.14 and do_formula bs t =
1.15 case t of
1.16 - @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
1.17 + @{const Trueprop} $ t1 => do_formula bs t1
1.18 + | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
1.19 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
1.20 do_quant bs AForall s T t'
1.21 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
1.22 @@ -879,22 +880,25 @@
1.23 | aux t = t
1.24 in t |> exists_subterm is_Var t ? aux end
1.25
1.26 -(* making fact and conjecture formulas *)
1.27 -fun make_formula ctxt format type_sys eq_as_iff presimp name loc kind t =
1.28 +fun preprocess_prop ctxt presimp kind t =
1.29 let
1.30 val thy = Proof_Context.theory_of ctxt
1.31 val t = t |> Envir.beta_eta_contract
1.32 |> transform_elim_prop
1.33 |> Object_Logic.atomize_term thy
1.34 val need_trueprop = (fastype_of t = @{typ bool})
1.35 - val t = t |> need_trueprop ? HOLogic.mk_Trueprop
1.36 - |> Raw_Simplifier.rewrite_term thy
1.37 - (Meson.unfold_set_const_simps ctxt) []
1.38 - |> extensionalize_term ctxt
1.39 - |> presimp ? presimplify_term ctxt
1.40 - |> perhaps (try (HOLogic.dest_Trueprop))
1.41 - |> introduce_combinators_in_term ctxt kind
1.42 - |> kind <> Axiom ? freeze_term
1.43 + in
1.44 + t |> need_trueprop ? HOLogic.mk_Trueprop
1.45 + |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
1.46 + |> extensionalize_term ctxt
1.47 + |> presimp ? presimplify_term ctxt
1.48 + |> introduce_combinators_in_term ctxt kind
1.49 + |> kind <> Axiom ? freeze_term
1.50 + end
1.51 +
1.52 +(* making fact and conjecture formulas *)
1.53 +fun make_formula thy format type_sys eq_as_iff name loc kind t =
1.54 + let
1.55 val (combformula, atomic_types) =
1.56 combformula_from_prop thy format type_sys eq_as_iff t []
1.57 in
1.58 @@ -902,16 +906,23 @@
1.59 atomic_types = atomic_types}
1.60 end
1.61
1.62 -fun make_fact ctxt format type_sys keep_trivial eq_as_iff presimp
1.63 +fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp
1.64 ((name, loc), t) =
1.65 - case (keep_trivial,
1.66 - make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of
1.67 - (false, formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
1.68 - if s = tptp_true then NONE else SOME formula
1.69 - | (_, formula) => SOME formula
1.70 + let val thy = Proof_Context.theory_of ctxt in
1.71 + case (keep_trivial,
1.72 + t |> preproc ? preprocess_prop ctxt presimp Axiom
1.73 + |> make_formula thy format type_sys eq_as_iff name loc Axiom) of
1.74 + (false,
1.75 + formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
1.76 + if s = tptp_true then NONE else SOME formula
1.77 + | (_, formula) => SOME formula
1.78 + end
1.79
1.80 -fun make_conjecture ctxt format prem_kind type_sys ts =
1.81 - let val last = length ts - 1 in
1.82 +fun make_conjecture ctxt format prem_kind type_sys preproc ts =
1.83 + let
1.84 + val thy = Proof_Context.theory_of ctxt
1.85 + val last = length ts - 1
1.86 + in
1.87 map2 (fn j => fn t =>
1.88 let
1.89 val (kind, maybe_negate) =
1.90 @@ -922,8 +933,9 @@
1.91 if prem_kind = Conjecture then update_combformula mk_anot
1.92 else I)
1.93 in
1.94 - t |> make_formula ctxt format type_sys true true
1.95 - (string_of_int j) General kind
1.96 + t |> preproc ? preprocess_prop ctxt true kind
1.97 + |> make_formula thy format type_sys true (string_of_int j)
1.98 + General kind
1.99 |> maybe_negate
1.100 end)
1.101 (0 upto last) ts
1.102 @@ -1273,7 +1285,7 @@
1.103 | _ => I)
1.104 end)
1.105 fun make_facts eq_as_iff =
1.106 - map_filter (make_fact ctxt format type_sys false eq_as_iff false)
1.107 + map_filter (make_fact ctxt format type_sys true false eq_as_iff false)
1.108 val fairly_sound = is_type_sys_fairly_sound type_sys
1.109 in
1.110 helper_table
1.111 @@ -1292,7 +1304,7 @@
1.112 []
1.113
1.114 fun translate_atp_fact ctxt format type_sys keep_trivial =
1.115 - `(make_fact ctxt format type_sys keep_trivial true true o apsnd prop_of)
1.116 + `(make_fact ctxt format type_sys keep_trivial true true true o apsnd prop_of)
1.117
1.118 (***************************************************************)
1.119 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1.120 @@ -1331,8 +1343,7 @@
1.121 fun type_consts_of_terms thy ts =
1.122 Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty)
1.123
1.124 -
1.125 -fun translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t
1.126 +fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
1.127 rich_facts =
1.128 let
1.129 val thy = Proof_Context.theory_of ctxt
1.130 @@ -1351,7 +1362,8 @@
1.131 val supers = tvar_classes_of_terms all_ts
1.132 val tycons = type_consts_of_terms thy all_ts
1.133 val conjs =
1.134 - hyp_ts @ [concl_t] |> make_conjecture ctxt format prem_kind type_sys
1.135 + hyp_ts @ [concl_t]
1.136 + |> make_conjecture ctxt format prem_kind type_sys preproc
1.137 val (supers', arity_clauses) =
1.138 if level_of_type_sys type_sys = No_Types then ([], [])
1.139 else make_arity_clauses thy tycons supers
1.140 @@ -1745,10 +1757,12 @@
1.141 val free_typesN = "Type variables"
1.142
1.143 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
1.144 - explicit_apply readable_names hyp_ts concl_t facts =
1.145 + explicit_apply readable_names preproc hyp_ts concl_t
1.146 + facts =
1.147 let
1.148 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
1.149 - translate_formulas ctxt format prem_kind type_sys hyp_ts concl_t facts
1.150 + translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
1.151 + facts
1.152 val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
1.153 val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
1.154 val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab