--- a/NEWS Sat Oct 29 10:00:35 2011 +0200
+++ b/NEWS Sun Oct 30 07:08:33 2011 +0100
@@ -81,7 +81,7 @@
ProofContext has been discontinued. INCOMPATIBILITY.
* Refined Local_Theory.declaration {syntax, pervasive}, with subtle
-change of semantics for syntax = false: update is applied to auxiliary
+change of semantics: update is applied to auxiliary local theory
context as well.
--- a/doc-src/Sledgehammer/sledgehammer.tex Sat Oct 29 10:00:35 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Sun Oct 30 07:08:33 2011 +0100
@@ -724,7 +724,8 @@
\item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic
higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
-with support for the TPTP many-typed higher-order syntax (THF0).
+with support for the TPTP many-typed higher-order syntax (THF0). Sledgehammer
+requires version 1.2.9 or above.
\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
the external provers, Metis itself can be used for proof search.
--- a/src/HOL/Partial_Function.thy Sat Oct 29 10:00:35 2011 +0200
+++ b/src/HOL/Partial_Function.thy Sun Oct 30 07:08:33 2011 +0100
@@ -127,7 +127,7 @@
abbreviation "le_fun \<equiv> fun_ord leq"
abbreviation "lub_fun \<equiv> fun_lub lub"
-abbreviation "fixp_fun == ccpo.fixp le_fun lub_fun"
+abbreviation "fixp_fun \<equiv> ccpo.fixp le_fun lub_fun"
abbreviation "mono_body \<equiv> monotone le_fun leq"
abbreviation "admissible \<equiv> ccpo.admissible le_fun lub_fun"
--- a/src/HOL/TPTP/ATP_Export.thy Sat Oct 29 10:00:35 2011 +0200
+++ b/src/HOL/TPTP/ATP_Export.thy Sun Oct 30 07:08:33 2011 +0100
@@ -4,6 +4,11 @@
begin
ML {*
+open ATP_Problem;
+open ATP_Export;
+*}
+
+ML {*
val do_it = false; (* switch to "true" to generate the files *)
val thy = @{theory Complex_Main};
val ctxt = @{context}
@@ -11,32 +16,40 @@
ML {*
if do_it then
- ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_preds"
- "/tmp/infs_poly_preds.tptp"
+ "/tmp/axs_mono_simple.dfg"
+ |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted)
+ "mono_simple"
else
()
*}
ML {*
if do_it then
- ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags"
- "/tmp/infs_poly_tags.tptp"
+ "/tmp/infs_poly_guards.tptp"
+ |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_guards"
else
()
*}
ML {*
if do_it then
- ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_uniform"
- "/tmp/infs_poly_tags_uniform.tptp"
+ "/tmp/infs_poly_tags.tptp"
+ |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags"
else
()
*}
ML {*
if do_it then
- ATP_Export.generate_tptp_graph_file_for_theory ctxt thy
- "/tmp/graph.out"
+ "/tmp/infs_poly_tags_uniform.tptp"
+ |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags_uniform"
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ "/tmp/graph.out" |> generate_tptp_graph_file_for_theory ctxt thy
else
()
*}
--- a/src/HOL/TPTP/atp_export.ML Sat Oct 29 10:00:35 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Sun Oct 30 07:08:33 2011 +0100
@@ -8,12 +8,14 @@
signature ATP_EXPORT =
sig
+ type atp_format = ATP_Problem.atp_format
+
val theorems_mentioned_in_proof_term :
string list option -> thm -> string list
val generate_tptp_graph_file_for_theory :
Proof.context -> theory -> string -> unit
val generate_tptp_inference_file_for_theory :
- Proof.context -> theory -> string -> string -> unit
+ Proof.context -> theory -> atp_format -> string -> string -> unit
end;
structure ATP_Export : ATP_EXPORT =
@@ -109,14 +111,13 @@
fun ident_of_problem_line (Decl (ident, _, _)) = ident
| ident_of_problem_line (Formula (ident, _, _, _, _)) = ident
-fun run_some_atp ctxt problem =
+fun run_some_atp ctxt format problem =
let
val thy = Proof_Context.theory_of ctxt
val prob_file = File.tmp_path (Path.explode "prob.tptp")
val {exec, arguments, proof_delims, known_failures, ...} =
- get_atp thy spassN
- val _ = problem |> tptp_lines_for_atp_problem FOF
- |> File.write_list prob_file
+ get_atp thy (case format of DFG _ => spassN | _ => eN)
+ val _ = problem |> lines_for_atp_problem format |> File.write_list prob_file
val command =
File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^
" " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
@@ -134,12 +135,12 @@
[@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}]
|> map (fact_name_of o Context.theory_name)
-fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) =
+fun is_problem_line_tautology ctxt format (Formula (ident, _, phi, _, _)) =
exists (fn prefix => String.isPrefix prefix ident)
likely_tautology_prefixes andalso
- is_none (run_some_atp ctxt
+ is_none (run_some_atp ctxt format
[(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])])
- | is_problem_line_tautology _ _ = false
+ | is_problem_line_tautology _ _ _ = false
structure String_Graph = Graph(type key = string val ord = string_ord);
@@ -149,21 +150,41 @@
if heading = factsN then (heading, order_facts ord lines) :: problem
else (heading, lines) :: order_problem_facts ord problem
-fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name =
+(* A fairly random selection of types used for monomorphizing. *)
+val ground_types =
+ [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool},
+ @{typ unit}]
+
+fun ground_type_for_tvar _ [] tvar =
+ raise TYPE ("ground_type_for_sorts", [TVar tvar], [])
+ | ground_type_for_tvar thy (T :: Ts) tvar =
+ if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T
+ else ground_type_for_tvar thy Ts tvar
+
+fun monomorphize_term ctxt t =
+ let val thy = Proof_Context.theory_of ctxt in
+ t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types))
+ handle TYPE _ => @{prop True}
+ end
+
+fun generate_tptp_inference_file_for_theory ctxt thy format type_enc file_name =
let
- val format = FOF
val type_enc = type_enc |> type_enc_from_string Sound
+ |> adjust_type_enc format
+ val mono = polymorphism_of_type_enc type_enc <> Polymorphic
val path = file_name |> Path.explode
val _ = File.write path ""
val facts = facts_of thy
val (atp_problem, _, _, _, _, _, _) =
facts
- |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
+ |> map (fn ((_, loc), th) =>
+ ((Thm.get_name_hint th, loc),
+ th |> prop_of |> mono ? monomorphize_term ctxt))
|> prepare_atp_problem ctxt format Axiom Axiom type_enc true combinatorsN
false true [] @{prop False}
val atp_problem =
atp_problem
- |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
+ |> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
val all_names = facts |> map (Thm.get_name_hint o snd)
val infers =
facts |> map (fn (_, th) =>
@@ -187,9 +208,10 @@
(ordered_names ~~ (1 upto length ordered_names))
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
val atp_problem =
- atp_problem |> add_inferences_to_problem infers
- |> order_problem_facts name_ord
- val ss = tptp_lines_for_atp_problem FOF atp_problem
+ atp_problem
+ |> (case format of DFG _ => I | _ => add_inferences_to_problem infers)
+ |> order_problem_facts name_ord
+ val ss = lines_for_atp_problem format atp_problem
val _ = app (File.append path) ss
in () end
--- a/src/HOL/Tools/ATP/atp_problem.ML Sat Oct 29 10:00:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sun Oct 30 07:08:33 2011 +0100
@@ -25,12 +25,15 @@
datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_flavor = THF_Without_Choice | THF_With_Choice
- datatype tptp_format =
+ datatype dfg_flavor = DFG_Unsorted | DFG_Sorted
+
+ datatype atp_format =
CNF |
CNF_UEQ |
FOF |
TFF of tptp_polymorphism * tptp_explicitness |
- THF of tptp_polymorphism * tptp_explicitness * thf_flavor
+ THF of tptp_polymorphism * tptp_explicitness * thf_flavor |
+ DFG of dfg_flavor
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -41,6 +44,11 @@
* (string, string ho_type) ho_term option
type 'a problem = (string * 'a problem_line list) list
+ val isabelle_info_prefix : string
+ val isabelle_info : atp_format -> string -> (string, 'a) ho_term option
+ val introN : string
+ val elimN : string
+ val simpN : string
val tptp_cnf : string
val tptp_fof : string
val tptp_tff : string
@@ -92,9 +100,9 @@
bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
-> 'd -> 'd
val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
- val is_format_thf : tptp_format -> bool
- val is_format_typed : tptp_format -> bool
- val tptp_lines_for_atp_problem : tptp_format -> string problem -> string list
+ val is_format_higher_order : atp_format -> bool
+ val is_format_typed : atp_format -> bool
+ val lines_for_atp_problem : atp_format -> string problem -> string list
val ensure_cnf_problem :
(string * string) problem -> (string * string) problem
val filter_cnf_ueq_problem :
@@ -133,13 +141,15 @@
datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_flavor = THF_Without_Choice | THF_With_Choice
+datatype dfg_flavor = DFG_Unsorted | DFG_Sorted
-datatype tptp_format =
+datatype atp_format =
CNF |
CNF_UEQ |
FOF |
TFF of tptp_polymorphism * tptp_explicitness |
- THF of tptp_polymorphism * tptp_explicitness * thf_flavor
+ THF of tptp_polymorphism * tptp_explicitness * thf_flavor |
+ DFG of dfg_flavor
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -148,6 +158,22 @@
* (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
type 'a problem = (string * 'a problem_line list) list
+val isabelle_info_prefix = "isabelle_"
+
+(* Currently, only newer versions of SPASS, with sorted DFG format support, can
+ process Isabelle metainformation. *)
+fun isabelle_info (DFG DFG_Sorted) s =
+ SOME (ATerm ("[]", [ATerm (isabelle_info_prefix ^ s, [])]))
+ | isabelle_info _ _ = NONE
+
+val introN = "intro"
+val elimN = "elim"
+val simpN = "simp"
+
+fun is_isabelle_info suffix (SOME (ATerm ("[]", [ATerm (s, [])]))) =
+ s = isabelle_info_prefix ^ suffix
+ | is_isabelle_info _ _ = false
+
(* official TPTP syntax *)
val tptp_cnf = "cnf"
val tptp_fof = "fof"
@@ -186,6 +212,10 @@
fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)
+val atype_of_types = AType (`I tptp_type_of_types, [])
+val bool_atype = AType (`I tptp_bool_type, [])
+val individual_atype = AType (`I tptp_individual_type, [])
+
fun raw_polarities_of_conn ANot = (SOME false, NONE)
| raw_polarities_of_conn AAnd = (SOME true, SOME true)
| raw_polarities_of_conn AOr = (SOME true, SOME true)
@@ -224,20 +254,21 @@
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)
-fun is_format_thf (THF _) = true
- | is_format_thf _ = false
+fun is_format_higher_order (THF _) = true
+ | is_format_higher_order _ = false
fun is_format_typed (TFF _) = true
| is_format_typed (THF _) = true
+ | is_format_typed (DFG DFG_Sorted) = true
| is_format_typed _ = false
-fun string_for_kind Axiom = "axiom"
- | string_for_kind Definition = "definition"
- | string_for_kind Lemma = "lemma"
- | string_for_kind Hypothesis = "hypothesis"
- | string_for_kind Conjecture = "conjecture"
+fun tptp_string_for_kind Axiom = "axiom"
+ | tptp_string_for_kind Definition = "definition"
+ | tptp_string_for_kind Lemma = "lemma"
+ | tptp_string_for_kind Hypothesis = "hypothesis"
+ | tptp_string_for_kind Conjecture = "conjecture"
-fun string_for_app format func args =
- if is_format_thf format then
+fun tptp_string_for_app format func args =
+ if is_format_higher_order format then
"(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
else
func ^ "(" ^ commas args ^ ")"
@@ -255,17 +286,21 @@
fun str_for_type format ty =
let
- fun str _ (AType (s, [])) = s
+ val dfg = (format = DFG DFG_Sorted)
+ fun str _ (AType (s, [])) =
+ if dfg andalso s = tptp_individual_type then "Top" else s
| str _ (AType (s, tys)) =
let val ss = tys |> map (str false) in
if s = tptp_product_type then
- ss |> space_implode (" " ^ tptp_product_type ^ " ")
- |> length ss > 1 ? enclose "(" ")"
+ ss |> space_implode
+ (if dfg then ", " else " " ^ tptp_product_type ^ " ")
+ |> (not dfg andalso length ss > 1) ? enclose "(" ")"
else
- string_for_app format s ss
+ tptp_string_for_app format s ss
end
| str rhs (AFun (ty1, ty2)) =
- str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
+ (str false ty1 |> dfg ? enclose "(" ")") ^ " " ^
+ (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2
|> not rhs ? enclose "(" ")"
| str _ (ATyAbs (ss, ty)) =
tptp_pi_binder ^ "[" ^
@@ -274,17 +309,16 @@
in str true ty end
fun string_for_type (format as THF _) ty = str_for_type format ty
- | string_for_type (format as TFF _) ty = str_for_type format (flatten_type ty)
- | string_for_type _ _ = raise Fail "unexpected type in untyped format"
+ | string_for_type format ty = str_for_type format (flatten_type ty)
-fun string_for_quantifier AForall = tptp_forall
- | string_for_quantifier AExists = tptp_exists
+fun tptp_string_for_quantifier AForall = tptp_forall
+ | tptp_string_for_quantifier AExists = tptp_exists
-fun string_for_connective ANot = tptp_not
- | string_for_connective AAnd = tptp_and
- | string_for_connective AOr = tptp_or
- | string_for_connective AImplies = tptp_implies
- | string_for_connective AIff = tptp_iff
+fun tptp_string_for_connective ANot = tptp_not
+ | tptp_string_for_connective AAnd = tptp_and
+ | tptp_string_for_connective AOr = tptp_or
+ | tptp_string_for_connective AImplies = tptp_implies
+ | tptp_string_for_connective AIff = tptp_iff
fun string_for_bound_var format (s, ty) =
s ^
@@ -298,84 +332,199 @@
fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true
| is_format_with_choice _ = false
-fun string_for_term _ (ATerm (s, [])) = s
- | string_for_term format (ATerm (s, ts)) =
+fun tptp_string_for_term _ (ATerm (s, [])) = s
+ | tptp_string_for_term format (ATerm (s, ts)) =
(if s = tptp_empty_list then
(* used for lists in the optional "source" field of a derivation *)
- "[" ^ commas (map (string_for_term format) ts) ^ "]"
+ "[" ^ commas (map (tptp_string_for_term format) ts) ^ "]"
else if is_tptp_equal s then
- space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
- |> is_format_thf format ? enclose "(" ")"
+ space_implode (" " ^ tptp_equal ^ " ")
+ (map (tptp_string_for_term format) ts)
+ |> is_format_higher_order format ? enclose "(" ")"
else case (s = tptp_ho_forall orelse s = tptp_ho_exists,
s = tptp_choice andalso is_format_with_choice format, ts) of
(true, _, [AAbs ((s', ty), tm)]) =>
(* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
possible, to work around LEO-II 1.2.8 parser limitation. *)
- string_for_formula format
+ tptp_string_for_formula format
(AQuant (if s = tptp_ho_forall then AForall else AExists,
[(s', SOME ty)], AAtom tm))
| (_, true, [AAbs ((s', ty), tm)]) =>
(* There is code in "ATP_Translate" to ensure that "Eps" is always
applied to an abstraction. *)
tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
- string_for_term format tm ^ ""
+ tptp_string_for_term format tm ^ ""
|> enclose "(" ")"
- | _ => string_for_app format s (map (string_for_term format) ts))
- | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
+ | _ => tptp_string_for_app format s (map (tptp_string_for_term format) ts))
+ | tptp_string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
"(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
- string_for_term format tm ^ ")"
- | string_for_term _ _ = raise Fail "unexpected term in first-order format"
-and string_for_formula format (AQuant (q, xs, phi)) =
- string_for_quantifier q ^
+ tptp_string_for_term format tm ^ ")"
+ | tptp_string_for_term _ _ =
+ raise Fail "unexpected term in first-order format"
+and tptp_string_for_formula format (AQuant (q, xs, phi)) =
+ tptp_string_for_quantifier q ^
"[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^
- string_for_formula format phi
+ tptp_string_for_formula format phi
|> enclose "(" ")"
- | string_for_formula format
+ | tptp_string_for_formula format
(AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) =
space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
- (map (string_for_term format) ts)
- |> is_format_thf format ? enclose "(" ")"
- | string_for_formula format (AConn (c, [phi])) =
- string_for_connective c ^ " " ^
- (string_for_formula format phi |> is_format_thf format ? enclose "(" ")")
+ (map (tptp_string_for_term format) ts)
+ |> is_format_higher_order format ? enclose "(" ")"
+ | tptp_string_for_formula format (AConn (c, [phi])) =
+ tptp_string_for_connective c ^ " " ^
+ (tptp_string_for_formula format phi
+ |> is_format_higher_order format ? enclose "(" ")")
|> enclose "(" ")"
- | string_for_formula format (AConn (c, phis)) =
- space_implode (" " ^ string_for_connective c ^ " ")
- (map (string_for_formula format) phis)
+ | tptp_string_for_formula format (AConn (c, phis)) =
+ space_implode (" " ^ tptp_string_for_connective c ^ " ")
+ (map (tptp_string_for_formula format) phis)
|> enclose "(" ")"
- | string_for_formula format (AAtom tm) = string_for_term format tm
+ | tptp_string_for_formula format (AAtom tm) = tptp_string_for_term format tm
fun the_source (SOME source) = source
| the_source NONE =
ATerm ("inference",
ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
-fun string_for_format CNF = tptp_cnf
- | string_for_format CNF_UEQ = tptp_cnf
- | string_for_format FOF = tptp_fof
- | string_for_format (TFF _) = tptp_tff
- | string_for_format (THF _) = tptp_thf
+fun tptp_string_for_format CNF = tptp_cnf
+ | tptp_string_for_format CNF_UEQ = tptp_cnf
+ | tptp_string_for_format FOF = tptp_fof
+ | tptp_string_for_format (TFF _) = tptp_tff
+ | tptp_string_for_format (THF _) = tptp_thf
+ | tptp_string_for_format (DFG _) = raise Fail "non-TPTP format"
-fun string_for_problem_line format (Decl (ident, sym, ty)) =
- string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
- string_for_type format ty ^ ").\n"
- | string_for_problem_line format (Formula (ident, kind, phi, source, info)) =
- string_for_format format ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^
- ",\n (" ^ string_for_formula format phi ^ ")" ^
+fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) =
+ tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^
+ " : " ^ string_for_type format ty ^ ").\n"
+ | tptp_string_for_problem_line format
+ (Formula (ident, kind, phi, source, info)) =
+ tptp_string_for_format format ^ "(" ^ ident ^ ", " ^
+ tptp_string_for_kind kind ^ ",\n (" ^
+ tptp_string_for_formula format phi ^ ")" ^
(case (source, info) of
(NONE, NONE) => ""
- | (SOME tm, NONE) => ", " ^ string_for_term format tm
+ | (SOME tm, NONE) => ", " ^ tptp_string_for_term format tm
| (_, SOME tm) =>
- ", " ^ string_for_term format (the_source source) ^
- ", " ^ string_for_term format tm) ^ ").\n"
-fun tptp_lines_for_atp_problem format problem =
- "% This file was generated by Isabelle (most likely Sledgehammer)\n\
- \% " ^ timestamp () ^ "\n" ::
+ ", " ^ tptp_string_for_term format (the_source source) ^
+ ", " ^ tptp_string_for_term format tm) ^ ").\n"
+
+fun tptp_lines format =
maps (fn (_, []) => []
| (heading, lines) =>
"\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
- map (string_for_problem_line format) lines)
- problem
+ map (tptp_string_for_problem_line format) lines)
+
+fun arity_of_type (AFun (_, ty)) = 1 + arity_of_type ty
+ | arity_of_type _ = 0
+
+fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2
+ | binder_atypes _ = []
+
+fun is_function_type (AFun (_, ty)) = is_function_type ty
+ | is_function_type (AType (s, _)) =
+ s <> tptp_type_of_types andalso s <> tptp_bool_type
+ | is_function_type _ = false
+
+fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty
+ | is_predicate_type (AType (s, _)) = (s = tptp_bool_type)
+ | is_predicate_type _ = false
+
+fun dfg_string_for_formula flavor info =
+ let
+ fun str_for_term simp (ATerm (s, tms)) =
+ (if is_tptp_equal s then "equal" |> simp ? suffix ":lr"
+ else if s = tptp_true then "true"
+ else if s = tptp_false then "false"
+ else s) ^
+ (if null tms then ""
+ else "(" ^ commas (map (str_for_term false) tms) ^ ")")
+ | str_for_term _ _ = raise Fail "unexpected term in first-order format"
+ fun str_for_quant AForall = "forall"
+ | str_for_quant AExists = "exists"
+ fun str_for_conn _ ANot = "not"
+ | str_for_conn _ AAnd = "and"
+ | str_for_conn _ AOr = "or"
+ | str_for_conn _ AImplies = "implies"
+ | str_for_conn simp AIff = "equiv" |> simp ? suffix ":lr"
+ fun str_for_formula simp (AQuant (q, xs, phi)) =
+ str_for_quant q ^ "(" ^ "[" ^
+ commas (map (string_for_bound_var (DFG flavor)) xs) ^ "], " ^
+ str_for_formula simp phi ^ ")"
+ | str_for_formula simp (AConn (c, phis)) =
+ str_for_conn simp c ^ "(" ^
+ commas (map (str_for_formula false) phis) ^ ")"
+ | str_for_formula simp (AAtom tm) = str_for_term simp tm
+ in str_for_formula (is_isabelle_info simpN info) end
+
+fun dfg_lines flavor problem =
+ let
+ val sorted = (flavor = DFG_Sorted)
+ val format = DFG flavor
+ fun ary sym ty =
+ "(" ^ sym ^ ", " ^ string_of_int (arity_of_type ty) ^ ")"
+ fun fun_typ sym ty =
+ "function(" ^ sym ^ ", " ^ string_for_type format ty ^ ")."
+ fun pred_typ sym ty =
+ "predicate(" ^
+ commas (sym :: map (string_for_type format) (binder_atypes ty)) ^ ")."
+ fun formula pred (Formula (ident, kind, phi, _, info)) =
+ if pred kind then
+ SOME ("formula(" ^ dfg_string_for_formula flavor info phi ^ ", " ^
+ ident ^ ").")
+ else
+ NONE
+ | formula _ _ = NONE
+ fun filt f = problem |> map (map_filter f o snd) |> flat
+ val func_aries =
+ filt (fn Decl (_, sym, ty) =>
+ if is_function_type ty then SOME (ary sym ty) else NONE
+ | _ => NONE)
+ |> commas |> enclose "functions [" "]."
+ val pred_aries =
+ filt (fn Decl (_, sym, ty) =>
+ if is_predicate_type ty then SOME (ary sym ty) else NONE
+ | _ => NONE)
+ |> commas |> enclose "predicates [" "]."
+ fun sorts () =
+ filt (fn Decl (_, sym, AType (s, [])) =>
+ if s = tptp_type_of_types then SOME sym else NONE
+ | _ => NONE)
+ |> commas |> enclose "sorts [" "]."
+ val syms = [func_aries, pred_aries] @ (if sorted then [sorts ()] else [])
+ fun func_sigs () =
+ filt (fn Decl (_, sym, ty) =>
+ if is_function_type ty then SOME (fun_typ sym ty) else NONE
+ | _ => NONE)
+ fun pred_sigs () =
+ filt (fn Decl (_, sym, ty) =>
+ if is_predicate_type ty then SOME (pred_typ sym ty) else NONE
+ | _ => NONE)
+ val decls = if sorted then func_sigs () @ pred_sigs () else []
+ val axioms = filt (formula (curry (op <>) Conjecture))
+ val conjs = filt (formula (curry (op =) Conjecture))
+ fun list_of _ [] = []
+ | list_of heading ss =
+ "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @
+ ["end_of_list.\n\n"]
+ in
+ "\nbegin_problem(isabelle).\n\n" ::
+ list_of "descriptions"
+ ["name({**}).", "author({**}).", "status(unknown).",
+ "description({**})."] @
+ list_of "symbols" syms @
+ list_of "declarations" decls @
+ list_of "formulae(axioms)" axioms @
+ list_of "formulae(conjectures)" conjs @
+ ["end_problem.\n"]
+ end
+
+fun lines_for_atp_problem format problem =
+ "% This file was generated by Isabelle (most likely Sledgehammer)\n\
+ \% " ^ timestamp () ^ "\n" ::
+ (case format of
+ DFG flavor => dfg_lines flavor
+ | _ => tptp_lines format) problem
(** CNF (Metis) and CNF UEQ (Waldmeister) **)
@@ -467,11 +616,6 @@
(* TFF allows implicit declarations of types, function symbols, and predicate
symbols (with "$i" as the type of individuals), but some provers (e.g.,
SNARK) require explicit declarations. The situation is similar for THF. *)
-
-val atype_of_types = AType (`I tptp_type_of_types, [])
-val bool_atype = AType (`I tptp_bool_type, [])
-val individual_atype = AType (`I tptp_individual_type, [])
-
fun default_type pred_sym =
let
fun typ 0 = if pred_sym then bool_atype else individual_atype
@@ -548,7 +692,12 @@
unreadable "op_1", "op_2", etc., in the problem files. "eq" is reserved to
ensure that "HOL.eq" is correctly mapped to equality (not clear whether this
is still necessary). *)
-val reserved_nice_names = [tptp_old_equal, "op", "eq"]
+val spass_reserved_nice_names =
+ ["forall", "exists", "le", "ls", "ge", "gs", "plus", "minus", "mult", "fract",
+ "equal", "true", "false", "or", "and", "not", "implies", "implied", "equiv",
+ "lr", "def"]
+val reserved_nice_names =
+ [tptp_old_equal, "op", "eq"] @ spass_reserved_nice_names
fun readable_name full_name s =
if s = full_name then
--- a/src/HOL/Tools/ATP/atp_proof.ML Sat Oct 29 10:00:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Sun Oct 30 07:08:33 2011 +0100
@@ -24,8 +24,6 @@
TimedOut |
Inappropriate |
OutOfResources |
- SpassTooOld |
- VampireTooOld |
NoPerl |
NoLibwwwPerl |
MalformedInput |
@@ -81,8 +79,6 @@
TimedOut |
Inappropriate |
OutOfResources |
- SpassTooOld |
- VampireTooOld |
NoPerl |
NoLibwwwPerl |
MalformedInput |
@@ -134,17 +130,6 @@
| string_for_failure Inappropriate =
"The problem lies outside the prover's scope."
| string_for_failure OutOfResources = "The prover ran out of resources."
- | string_for_failure SpassTooOld =
- "Isabelle requires a more recent version of SPASS with support for the \
- \TPTP syntax. To install it, download and extract the package \
- \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
- \\"spass-3.7\" directory's absolute path to " ^
- Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
- " on a line of its own."
- | string_for_failure VampireTooOld =
- "Isabelle requires a more recent version of Vampire. To install it, follow \
- \the instructions from the Sledgehammer manual (\"isabelle doc\
- \ sledgehammer\")."
| string_for_failure NoPerl = "Perl" ^ missing_message_tail
| string_for_failure NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail
--- a/src/HOL/Tools/ATP/atp_systems.ML Sat Oct 29 10:00:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun Oct 30 07:08:33 2011 +0100
@@ -7,7 +7,7 @@
signature ATP_SYSTEMS =
sig
- type tptp_format = ATP_Problem.tptp_format
+ type atp_format = ATP_Problem.atp_format
type formula_kind = ATP_Problem.formula_kind
type failure = ATP_Proof.failure
@@ -23,7 +23,7 @@
prem_kind : formula_kind,
best_slices :
Proof.context
- -> (real * (bool * (int * tptp_format * string * string))) list}
+ -> (real * (bool * (int * atp_format * string * string))) list}
val force_sos : bool Config.T
val e_smartN : string
@@ -46,6 +46,7 @@
val satallaxN : string
val snarkN : string
val spassN : string
+ val spass_newN : string
val vampireN : string
val waldmeisterN : string
val z3_tptpN : string
@@ -53,7 +54,7 @@
val remote_atp :
string -> string -> string list -> (string * string) list
-> (failure * string) list -> formula_kind -> formula_kind
- -> (Proof.context -> int * tptp_format * string) -> string * atp_config
+ -> (Proof.context -> int * atp_format * string) -> string * atp_config
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
val supported_atps : theory -> string list
@@ -82,7 +83,7 @@
prem_kind : formula_kind,
best_slices :
Proof.context
- -> (real * (bool * (int * tptp_format * string * string))) list}
+ -> (real * (bool * (int * atp_format * string * string))) list}
(* "best_slices" must be found empirically, taking a wholistic approach since
the ATPs are run in parallel. The "real" components give the faction of the
@@ -130,6 +131,7 @@
val satallaxN = "satallax"
val snarkN = "snark"
val spassN = "spass"
+val spass_newN = "spass_new"
val vampireN = "vampire"
val waldmeisterN = "waldmeister"
val z3_tptpN = "z3_tptp"
@@ -255,7 +257,7 @@
required_execs = [],
arguments =
fn _ => fn _ => fn sos => fn timeout => fn _ =>
- "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
+ "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout)
|> sos = sosN ? prefix "--sos ",
proof_delims = tstp_proof_delims,
known_failures =
@@ -315,20 +317,38 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(Unprovable, "No formulae and clauses found in input file"),
- (SpassTooOld, "tptp2dfg"),
(InternalError, "Please report this error")],
conj_sym_kind = Hypothesis,
prem_kind = Conjecture,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, FOF, "mono_tags??", sosN))),
- (0.333, (false, (300, FOF, "poly_tags??", sosN))),
- (0.334, (true, (50, FOF, "mono_tags??", no_sosN)))]
+ [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", sosN))),
+ (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", sosN))),
+ (0.334, (true, (50, DFG DFG_Unsorted, "mono_tags??", no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
val spass = (spassN, spass_config)
+(* Experimental *)
+val spass_new_config : atp_config =
+ {exec = ("SPASS_HOME", "SPASS"),
+ required_execs = [],
+ arguments = #arguments spass_config,
+ proof_delims = #proof_delims spass_config,
+ known_failures = #known_failures spass_config,
+ conj_sym_kind = #conj_sym_kind spass_config,
+ prem_kind = #prem_kind spass_config,
+ best_slices = fn ctxt =>
+ (* FUDGE *)
+ [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", sosN))) (*,
+ (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", sosN))),
+ (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", no_sosN)))*)]
+ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
+ else I)}
+
+val spass_new = (spass_newN, spass_new_config)
+
(* Vampire *)
@@ -359,7 +379,6 @@
(GaveUp, "CANNOT PROVE"),
(Unprovable, "Satisfiability detected"),
(Unprovable, "Termination reason: Satisfiable"),
- (VampireTooOld, "not a valid option"),
(Interrupted, "Aborted by signal SIGINT")],
conj_sym_kind = Conjecture,
prem_kind = Conjecture,
@@ -545,9 +564,9 @@
Synchronized.change systems (fn _ => get_systems ())
val atps =
- [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
- remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
- remote_e_tofof, remote_waldmeister]
+ [e, leo2, pff, phf, satallax, spass, spass_new, vampire, z3_tptp, remote_e,
+ remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine,
+ remote_snark, remote_e_tofof, remote_waldmeister]
val setup = fold add_atp atps
end;
--- a/src/HOL/Tools/ATP/atp_translate.ML Sat Oct 29 10:00:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Oct 30 07:08:33 2011 +0100
@@ -11,7 +11,7 @@
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
type connective = ATP_Problem.connective
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
- type tptp_format = ATP_Problem.tptp_format
+ type atp_format = ATP_Problem.atp_format
type formula_kind = ATP_Problem.formula_kind
type 'a problem = 'a ATP_Problem.problem
@@ -19,7 +19,7 @@
General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
- datatype soundness = Sound_Modulo_Infiniteness | Sound
+ datatype soundness = Sound_Modulo_Infinity | Sound
datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
datatype type_level =
All_Types |
@@ -86,7 +86,7 @@
val is_type_enc_quasi_sound : type_enc -> bool
val is_type_enc_fairly_sound : type_enc -> bool
val type_enc_from_string : soundness -> string -> type_enc
- val adjust_type_enc : tptp_format -> type_enc -> type_enc
+ val adjust_type_enc : atp_format -> type_enc -> type_enc
val mk_aconns :
connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
val unmangled_const : string -> string * (string, 'b) ho_term list
@@ -94,7 +94,7 @@
val helper_table : ((string * bool) * thm list) list
val factsN : string
val prepare_atp_problem :
- Proof.context -> tptp_format -> formula_kind -> formula_kind -> type_enc
+ Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
-> bool -> string -> bool -> bool -> term list -> term
-> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
@@ -123,20 +123,10 @@
val lambdasN = "lambdas"
val smartN = "smart"
-val generate_info = false (* experimental *)
-
-fun isabelle_info s =
- if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
- else NONE
-
-val introN = "intro"
-val elimN = "elim"
-val simpN = "simp"
-
(* TFF1 is still in development, and it is still unclear whether symbols will be
allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
- "dummy" type variables. *)
-val avoid_first_order_dummy_type_vars = true
+ ghost type variables. *)
+val avoid_first_order_ghost_type_vars = true
val bound_var_prefix = "B_"
val all_bound_var_prefix = "BA_"
@@ -313,7 +303,7 @@
tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
-(* "HOL.eq" and Choice are mapped to the ATP's equivalents *)
+(* "HOL.eq" and choice are mapped to the ATP's equivalents *)
local
val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
fun default c = const_prefix ^ lookup_const c
@@ -529,7 +519,7 @@
datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
-datatype soundness = Sound_Modulo_Infiniteness | Sound
+datatype soundness = Sound_Modulo_Infinity | Sound
datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
datatype type_level =
All_Types |
@@ -650,6 +640,8 @@
| adjust_type_enc (THF _) type_enc = type_enc
| adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
Simple_Types (First_Order, Mangled_Monomorphic, level)
+ | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) =
+ Simple_Types (First_Order, Mangled_Monomorphic, level)
| adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
Simple_Types (First_Order, poly, level)
| adjust_type_enc format (Simple_Types (_, poly, level)) =
@@ -755,7 +747,7 @@
AAtom (ATerm (class, arg ::
(case type_enc of
Simple_Types (First_Order, Polymorphic, _) =>
- if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])]
+ if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]
else []
| _ => [])))
fun formulas_for_types type_enc add_sorts_on_typ Ts =
@@ -1545,7 +1537,7 @@
val type_tag = `(make_fixed_const NONE) type_tag_name
-fun type_tag_idempotence_fact type_enc =
+fun type_tag_idempotence_fact format type_enc =
let
fun var s = ATerm (`I s, [])
fun tag tm = ATerm (type_tag, [var "A", tm])
@@ -1553,7 +1545,7 @@
in
Formula (type_tag_idempotence_helper_name, Axiom,
eq_formula type_enc [] false (tag tagged_var) tagged_var,
- isabelle_info simpN, NONE)
+ isabelle_info format simpN, NONE)
end
fun should_specialize_helper type_enc t =
@@ -1833,32 +1825,34 @@
|> close_formula_universally type_enc,
NONE,
case locality of
- Intro => isabelle_info introN
- | Elim => isabelle_info elimN
- | Simp => isabelle_info simpN
+ Intro => isabelle_info format introN
+ | Elim => isabelle_info format elimN
+ | Simp => isabelle_info format simpN
| _ => NONE)
|> Formula
-fun formula_line_for_class_rel_clause type_enc
+fun formula_line_for_class_rel_clause format type_enc
({name, subclass, superclass, ...} : class_rel_clause) =
let val ty_arg = ATerm (tvar_a_name, []) in
Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
AConn (AImplies,
[type_class_formula type_enc subclass ty_arg,
type_class_formula type_enc superclass ty_arg])
- |> close_formula_universally type_enc, isabelle_info introN, NONE)
+ |> close_formula_universally type_enc,
+ isabelle_info format introN, NONE)
end
fun formula_from_arity_atom type_enc (class, t, args) =
ATerm (t, map (fn arg => ATerm (arg, [])) args)
|> type_class_formula type_enc class
-fun formula_line_for_arity_clause type_enc
+fun formula_line_for_arity_clause format type_enc
({name, prem_atoms, concl_atom, ...} : arity_clause) =
Formula (arity_clause_prefix ^ name, Axiom,
mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
(formula_from_arity_atom type_enc concl_atom)
- |> close_formula_universally type_enc, isabelle_info introN, NONE)
+ |> close_formula_universally type_enc,
+ isabelle_info format introN, NONE)
fun formula_line_for_conjecture ctxt format mono type_enc
({name, kind, iformula, atomic_types, ...} : translated_formula) =
@@ -1883,7 +1877,7 @@
fun decl_line_for_class order s =
let val name as (s, _) = `make_type_class s in
Decl (sym_decl_prefix ^ s, name,
- if order = First_Order andalso avoid_first_order_dummy_type_vars then
+ if order = First_Order andalso avoid_first_order_ghost_type_vars then
ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype))
else
AFun (atype_of_types, bool_atype))
@@ -2059,7 +2053,7 @@
(K (K (K (K (K (K true)))))) (SOME true)
|> bound_tvars type_enc (atyps_of T)
|> close_formula_universally type_enc,
- isabelle_info introN, NONE)
+ isabelle_info format introN, NONE)
fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
let val x_var = ATerm (`make_bound_var "X", []) in
@@ -2069,7 +2063,7 @@
eq_formula type_enc (atyps_of T) false
(tag_with_type ctxt format mono type_enc NONE T x_var)
x_var,
- isabelle_info simpN, NONE)
+ isabelle_info format simpN, NONE)
end
fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
@@ -2143,7 +2137,7 @@
|> n > 1 ? bound_tvars type_enc (atyps_of T)
|> close_formula_universally type_enc
|> maybe_negate,
- isabelle_info introN, NONE)
+ isabelle_info format introN, NONE)
end
fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
@@ -2179,7 +2173,7 @@
in
cons (Formula (ident_base ^ "_res", kind,
eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
- isabelle_info simpN, NONE))
+ isabelle_info format simpN, NONE))
end
else
I
@@ -2191,7 +2185,7 @@
cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
(cst bounds),
- isabelle_info simpN, NONE))
+ isabelle_info format simpN, NONE))
| _ => raise Fail "expected nonempty tail"
else
I
@@ -2343,7 +2337,7 @@
|> map (formula_line_for_fact ctxt format helper_prefix I false true mono
type_enc)
|> (if needs_type_tag_idempotence ctxt type_enc then
- cons (type_tag_idempotence_fact type_enc)
+ cons (type_tag_idempotence_fact format type_enc)
else
I)
(* Reordering these might confuse the proof reconstruction code or the SPASS
@@ -2355,8 +2349,10 @@
(not exporter) (not exporter) mono type_enc)
(0 upto length facts - 1 ~~ facts)),
(class_relsN,
- map (formula_line_for_class_rel_clause type_enc) class_rel_clauses),
- (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses),
+ map (formula_line_for_class_rel_clause format type_enc)
+ class_rel_clauses),
+ (aritiesN,
+ map (formula_line_for_arity_clause format type_enc) arity_clauses),
(helpersN, helper_lines),
(conjsN,
map (formula_line_for_conjecture ctxt format mono type_enc) conjs),
--- a/src/HOL/Tools/ATP/atp_util.ML Sat Oct 29 10:00:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Sun Oct 30 07:08:33 2011 +0100
@@ -208,20 +208,23 @@
| [] =>
case Typedef.get_info ctxt s of
({abs_type, rep_type, ...}, _) :: _ =>
- (* We cheat here by assuming that typedef types are infinite if
- their underlying type is infinite. This is unsound in general
- but it's hard to think of a realistic example where this would
- not be the case. We are also slack with representation types:
- If a representation type has the form "sigma => tau", we
- consider it enough to check "sigma" for infiniteness. (Look
- for "slack" in this function.) *)
- (case varify_and_instantiate_type ctxt
- (Logic.varifyT_global abs_type) T
- (Logic.varifyT_global rep_type)
- |> aux true avoid of
- 0 => 0
- | 1 => 1
- | _ => default_card)
+ if not sound then
+ (* We cheat here by assuming that typedef types are infinite if
+ their underlying type is infinite. This is unsound in
+ general but it's hard to think of a realistic example where
+ this would not be the case. We are also slack with
+ representation types: If a representation type has the form
+ "sigma => tau", we consider it enough to check "sigma" for
+ infiniteness. *)
+ (case varify_and_instantiate_type ctxt
+ (Logic.varifyT_global abs_type) T
+ (Logic.varifyT_global rep_type)
+ |> aux true avoid of
+ 0 => 0
+ | 1 => 1
+ | _ => default_card)
+ else
+ default_card
| [] => default_card)
(* Very slightly unsound: Type variables are assumed not to be
constrained to cardinality 1. (In practice, the user would most
--- a/src/HOL/Tools/ATP/scripts/spass Sat Oct 29 10:00:35 2011 +0200
+++ b/src/HOL/Tools/ATP/scripts/spass Sun Oct 30 07:08:33 2011 +0100
@@ -8,13 +8,11 @@
options=${@:1:$(($#-1))}
name=${@:$(($#)):1}
-"$SPASS_HOME/tptp2dfg" $name $name.fof.dfg
-"$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \
+"$SPASS_HOME/SPASS" -Flotter $name \
| sed 's/description({$/description({*/' \
| sed 's/set_ClauseFormulaRelation()\.//' \
- > $name.cnf.dfg
-rm -f $name.fof.dfg
-cat $name.cnf.dfg
-"$SPASS_HOME/SPASS" $options $name.cnf.dfg \
+ > $name.cnf
+cat $name.cnf
+"$SPASS_HOME/SPASS" $options $name.cnf \
| sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
-rm -f $name.cnf.dfg
+rm -f $name.cnf
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Oct 29 10:00:35 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun Oct 30 07:08:33 2011 +0100
@@ -799,28 +799,28 @@
is_that_fact thm
end)
-fun meta_equify (@{const Trueprop}
- $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2)) =
- Const (@{const_name "=="}, T --> T --> @{typ prop}) $ t1 $ t2
- | meta_equify t = t
-
-val normalize_simp_prop =
- meta_equify
- #> map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t)
+val crude_zero_vars =
+ map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t)
#> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S)))
fun clasimpset_rule_table_of ctxt =
let
- fun add loc g f = fold (Termtab.update o rpair loc o g o prop_of o f)
- val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> Classical.rep_cs
+ val thy = Proof_Context.theory_of ctxt
+ val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
+ fun add loc g f =
+ fold (Termtab.update o rpair loc o g o crude_zero_vars o prop_of o f)
+ val {safeIs, safeEs, hazIs, hazEs, ...} =
+ ctxt |> claset_of |> Classical.rep_cs
val intros = Item_Net.content safeIs @ Item_Net.content hazIs
- val elims = map Classical.classical_rule (Item_Net.content safeEs @ Item_Net.content hazEs)
+ val elims =
+ Item_Net.content safeEs @ Item_Net.content hazEs
+ |> map Classical.classical_rule
val simps = ctxt |> simpset_of |> dest_ss |> #simps
in
Termtab.empty |> add Intro I I intros
|> add Elim I I elims
|> add Simp I snd simps
- |> add Simp normalize_simp_prop snd simps
+ |> add Simp atomize snd simps
end
fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths =
@@ -833,17 +833,20 @@
fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
val is_chained = member Thm.eq_thm_prop chained_ths
val clasimpset_table = clasimpset_rule_table_of ctxt
- fun locality_of_theorem global (name: string) th =
- if String.isSubstring ".induct" name orelse(*FIXME: use structured name*)
+ fun locality_of_theorem global name th =
+ if String.isSubstring ".induct" name orelse (*FIXME: use structured name*)
String.isSubstring ".inducts" name then
- Induction
+ Induction
else if is_chained th then
Chained
else if global then
case Termtab.lookup clasimpset_table (prop_of th) of
SOME loc => loc
| NONE => General
- else if is_assum th then Assum else Local
+ else if is_assum th then
+ Assum
+ else
+ Local
fun is_good_unnamed_local th =
not (Thm.has_name_hint th) andalso
forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Oct 29 10:00:35 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Oct 30 07:08:33 2011 +0100
@@ -160,7 +160,7 @@
end
val is_unit_equational_atp = is_atp_for_format (curry (op =) CNF_UEQ)
-val is_ho_atp = is_atp_for_format is_format_thf
+val is_ho_atp = is_atp_for_format is_format_higher_order
fun is_prover_supported ctxt name =
let val thy = Proof_Context.theory_of ctxt in
@@ -615,8 +615,7 @@
val num_facts =
length facts |> is_none max_relevant
? Integer.min best_max_relevant
- val soundness =
- if sound then Sound else Sound_Modulo_Infiniteness
+ val soundness = if sound then Sound else Sound_Modulo_Infinity
val type_enc =
type_enc |> choose_type_enc soundness best_type_enc format
val fairly_sound = is_type_enc_fairly_sound type_enc
@@ -660,11 +659,9 @@
arguments ctxt full_proof extra slice_timeout weights ^ " " ^
File.shell_path prob_file
val command = "TIMEFORMAT='%3R'; { time " ^ core ^ " ; } 2>&1"
- val _ =
- atp_problem
- |> tptp_lines_for_atp_problem format
- |> cons ("% " ^ command ^ "\n")
- |> File.write_list prob_file
+ val _ = atp_problem |> lines_for_atp_problem format
+ |> cons ("% " ^ command ^ "\n")
+ |> File.write_list prob_file
val conjecture_shape =
conjecture_offset + 1
upto conjecture_offset + length hyp_ts + 1
--- a/src/Pure/Isar/generic_target.ML Sat Oct 29 10:00:35 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML Sun Oct 30 07:08:33 2011 +0100
@@ -193,7 +193,7 @@
lthy
|> Local_Theory.background_theory (Context.theory_map global_decl)
|> Local_Theory.target (Context.proof_map global_decl)
- |> not syntax ? Context.proof_map (Morphism.form decl)
+ |> Context.proof_map (Morphism.form decl)
end;
fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
--- a/src/Pure/Isar/local_theory.ML Sat Oct 29 10:00:35 2011 +0200
+++ b/src/Pure/Isar/local_theory.ML Sun Oct 30 07:08:33 2011 +0100
@@ -231,8 +231,7 @@
fun alias global_alias local_alias b name =
declaration {syntax = true, pervasive = false} (fn phi =>
let val b' = Morphism.binding phi b
- in Context.mapping (global_alias b' name) (local_alias b' name) end)
- #> local_alias b name;
+ in Context.mapping (global_alias b' name) (local_alias b' name) end);
val class_alias = alias Sign.class_alias Proof_Context.class_alias;
val type_alias = alias Sign.type_alias Proof_Context.type_alias;
--- a/src/Pure/Isar/named_target.ML Sat Oct 29 10:00:35 2011 +0200
+++ b/src/Pure/Isar/named_target.ML Sun Oct 30 07:08:33 2011 +0100
@@ -54,7 +54,6 @@
lthy
|> pervasive ? Generic_Target.theory_declaration syntax decl
|> Local_Theory.target (add locale locale_decl)
- |> not syntax ? Context.proof_map (Morphism.form decl)
end;
fun target_declaration (Target {target, ...}) params =