--- a/src/HOL/TPTP/ATP_Problem_Import.thy Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy Fri Dec 16 19:50:46 2016 +0100
@@ -22,6 +22,7 @@
(*
ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 "$TPTP/Problems/PUZ/PUZ107^5.p" *}
+ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} 20 "$TPTP/Problems/SYO/SYO304^5.p" *}
*)
end
--- a/src/HOL/TPTP/CASC/ReadMe Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/CASC/ReadMe Fri Dec 16 19:50:46 2016 +0100
@@ -1,4 +1,4 @@
-Notes from Geoff:
+Notes from Geoff Sutcliffe:
I added a few lines to the top of bin/isabelle ...
@@ -48,10 +48,11 @@
STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle_hot $TPTP/Problems/CSR/CSR150^3.p
STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle_hot $TPTP/Problems/SYO/SYO304^5.p
- The first problem is unprovable; the second one is proved by Satallax.
+ The first problem is unprovable; the second one is proved by Satallax (after
+ some delay).
- All the tools accept CNF, FOF, TFF0, or THF0 problems and output SZS
- statuses of the form
+ All the tools accept CNF, FOF, TFF0, TFF1, THF0, or THF1 problems and output
+ SZS statuses of the form
% SZS status XXX
@@ -60,43 +61,32 @@
{Unknown, TimedOut, Unsatisfiable, Theorem, Satisfiable, CounterSatisfiable}
Nitpick also output a model within "% SZS begin" and "% SZS end" tags, in
- its idiosyncratic syntax.
-
- In 2011, there were some problems with Java (needed for Nitpick), because it
- required so much memory at startup. I doubt there will be any problems this
- year, because Isabelle now includes its own version of Java, but the solution
- back then was to replace
-
- exec isabelle java
-
- in the last line of the "contrib/kodkodi-1.5.2/bin/kodkodi" script with
-
- /usr/lib64/jvm/java-1.5.0-gcj-4.5-1.5.0.0/jre/bin/java
-
- See the emails we exchanged on 18 July 2011, with the subject "No problem on
- my Linux 64-bit".
+ its idiosyncratic syntax. For TFF0 and THF0, phantom type arguments are not
+ supported, and type quantifiers are only allowed at the outermost position
+ in a formula, as "forall".
Enjoy!
Notes to myself:
- I downloaded the official Isabelle2015 Linux package from
+ I downloaded the official Isabelle2016-1 Linux package from
- http://isabelle.in.tum.de/dist/Isabelle2015_linux.tar.gz
+ http://isabelle.in.tum.de/dist/Isabelle2016-1_linux.tar.gz
- on "macbroy21" and renamed the directory "Isabelle2015-CASC". I modified
+ on "macbroy21" and renamed the directory "Isabelle2016-1-CASC". I modified
- src/HOL/TPTP/atp_problem_import.ML
+ src/HOL/TPTP
to include changes backported from the development version of Isabelle. I
- then built a "HOL-TPTP" image:
+ also modified "bin/isabelle" as suggested by Geoff above. I then built a
+ "HOL-TPTP" image:
./bin/isabelle build -b HOL-TPTP
- I copied the heaps over to "./heaps":
+ I moved the heaps over to "./heaps":
- mv ~/.isabelle/Isabelle2015/heaps .
+ mv ~/.isabelle/Isabelle2016-1/heaps .
I created some wrapper scripts in "./bin":
@@ -117,7 +107,7 @@
http://page.mi.fu-berlin.de/cbenzmueller/leo/leo2_v1.6.2.tgz
I did "make opt". I copied "bin/leo.opt" to
- "~/Isabelle2015-CASC/contrib/leo".
+ "~/Isabelle2016-1-CASC/contrib/leo".
I added this line to "etc/settings":
@@ -141,19 +131,19 @@
SATALLAX_HOME=$ISABELLE_HOME/contrib
- Vampire (2.6):
+ Vampire 4.0 (commit 2fedff6)
- I copied the file "vampire", which I probably got from the 2013 CASC
- archive and moved it to "~/Isabelle2013-CASC/contrib/vampire".
+ I copied the file "vampire", which I got from Giles Reger on 23 September
+ 2015.
I added these lines to "etc/settings":
VAMPIRE_HOME=$ISABELLE_HOME/contrib
- VAMPIRE_VERSION=3.0
+ VAMPIRE_VERSION=4.0
Z3 TPTP (4.3.2.0 postrelease):
- I cloned out the git repository:
+ For Isabelle2015, I cloned out the git repository:
git clone https://git01.codeplex.com/z3
@@ -173,9 +163,11 @@
"/tmp/T.thy" with the following content:
theory T imports Main begin
+
lemma "a = b ==> [b] = [a]"
- sledgehammer [cvc4 e leo2 satallax spass vampire z3 z3_tptp] ()
- oops
+ sledgehammer [cvc4 e leo2 satallax spass vampire z3 (*z3_tptp*)] ()
+ oops
+
end
Then I ran
@@ -196,4 +188,4 @@
Jasmin Blanchette
- 10 June 2015
+ 15 December 2016
--- a/src/HOL/TPTP/CASC/SysDesc_Isabelle.html Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/CASC/SysDesc_Isabelle.html Fri Dec 16 19:50:46 2016 +0100
@@ -1,5 +1,5 @@
<HR><!------------------------------------------------------------------------>
-<H2>Isabelle/HOL 2015</H2>
+<H2>Isabelle/HOL 2016-1</H2>
Jasmin C. Blanchette<sup>1</sup>, Lawrence C. Paulson<sup>2</sup>,
Tobias Nipkow<sup>1</sup>, Makarius Wenzel<sup>3</sup> <BR>
<sup>1</sup>Technische Universität München, Germany <BR>
@@ -8,9 +8,9 @@
<H3>Architecture</H3>
-Isabelle/HOL 2015 [<A HREF="#References">NPW13</A>] is the higher-order
-logic incarnation of the generic proof assistant
-<A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/">Isabelle2015</A>.
+Isabelle/HOL 2016-1 [<A HREF="#References">NPW13</A>] is the higher-order
+logic incarnation of the generic proof assistant
+<A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/">Isabelle2016-1</A>.
Isabelle/HOL provides several automatic proof tactics, notably an equational
reasoner [<A HREF="#References">Nip89</A>], a classical reasoner [<A
HREF="#References">Pau94</A>], and a tableau prover [<A
--- a/src/HOL/TPTP/CASC/SysDesc_Nitpick.html Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/CASC/SysDesc_Nitpick.html Fri Dec 16 19:50:46 2016 +0100
@@ -1,11 +1,11 @@
<HR><!------------------------------------------------------------------------>
-<H2>Nitpick 2015</H2>
+<H2>Nitpick 2016-1</H2>
Jasmin C. Blanchette<BR>
Technische Universität München, Germany <BR>
<H3>Architecture</H3>
-Nitpick [<A HREF="#References">BN10</A>] is an open source counterexample
+Nitpick [<A HREF="#References">BN10</A>] is an open source counterexample
generator for Isabelle/HOL [<A HREF="#References">NPW13</A>]. It builds on
Kodkod [<A HREF="#References">TJ07</A>], a highly optimized first-order
relational model finder based on SAT. The name Nitpick is appropriated from a
--- a/src/HOL/TPTP/CASC/SysDesc_Refute.html Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/CASC/SysDesc_Refute.html Fri Dec 16 19:50:46 2016 +0100
@@ -1,12 +1,12 @@
<HR><!------------------------------------------------------------------------>
-<H2>Refute 2015</H2>
+<H2>Refute 2016-1</H2>
Jasmin C. Blanchette<sup>1</sup>, Tjark Weber<sup>2</sup><BR>
<sup>1</sup>Technische Universität München, Germany <BR>
<sup>2</sup>Uppsala Universitet, Sweden <BR>
<H3>Architecture</H3>
-Refute [<A HREF="#References">Web08</A>] is an open source counterexample
+Refute [<A HREF="#References">Web08</A>] is an open source counterexample
generator for Isabelle/HOL [<A HREF="#References">NPW13</A>] based on a
SAT solver, and Nitpick's [<A HREF="#References">BN10</A>] precursor.
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Dec 16 19:50:46 2016 +0100
@@ -215,7 +215,7 @@
fun declare_constant config const_name ty thy =
if const_exists config thy const_name then
raise MISINTERPRET_TERM
- ("Const already declared", Term_Func (Uninterpreted const_name, []))
+ ("Const already declared", Term_FuncG (Uninterpreted const_name, [], []))
else
Theory.specify_const ((mk_binding config const_name, ty), NoSyn) thy
@@ -224,10 +224,10 @@
(*Types in TFF/THF are encoded as formulas. These functions translate them to type form.*)
-fun termtype_to_type (Term_Func (TypeSymbol typ, [])) =
+fun termtype_to_type (Term_FuncG (TypeSymbol typ, [], [])) =
Defined_type typ
- | termtype_to_type (Term_Func (Uninterpreted str, tms)) =
- Atom_type (str, map termtype_to_type tms)
+ | termtype_to_type (Term_FuncG (Uninterpreted str, tys, tms)) =
+ Atom_type (str, tys @ map termtype_to_type tms)
| termtype_to_type (Term_Var str) = Var_type str
(*FIXME possibly incomplete hack*)
@@ -249,6 +249,9 @@
| fmlatype_to_type (Quant (Dep_Prod, _, fmla)) = fmlatype_to_type fmla
| fmlatype_to_type (Pred (Interpreted_ExtraLogic Apply, [tm])) =
termtype_to_type tm
+ | fmlatype_to_type (Fmla (Interpreted_ExtraLogic Apply, [tm1, tm2])) =
+ (case fmlatype_to_type tm1 of
+ Atom_type (str, tys) => Atom_type (str, tys @ [fmlatype_to_type tm2]))
fun tfree_name_of_var_type str = "'" ^ Name.desymbolize (SOME false) str
fun tfree_of_var_type str = TFree (tfree_name_of_var_type str, @{sort type})
@@ -323,7 +326,7 @@
else
raise MISINTERPRET_TERM
("Could not find the interpretation of this constant in the \
- \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])))
+ \mapping to Isabelle/HOL", Term_FuncG (Uninterpreted str, [], [])))
(*Eta-expands n-ary function.
"str" is the name of an Isabelle/HOL constant*)
@@ -448,7 +451,7 @@
interpret_type config thy type_map (Defined_type Type_Bool)
else ind_type
in case tptp_atom_value of
- Atom_App (Term_Func (symb, tptp_ts)) =>
+ Atom_App (Term_FuncG (symb, tptp_tys, tptp_ts)) =>
let
val thy' = fold (fn t =>
type_atoms_to_thy config false type_map (Atom_App t)) tptp_ts thy
@@ -456,7 +459,8 @@
case symb of
Uninterpreted const_name =>
perhaps (try (snd o declare_constant config const_name
- (mk_fun_type (replicate (length tptp_ts) ind_type) value_type I))) thy'
+ (mk_fun_type (replicate (length tptp_tys + length tptp_ts) ind_type) value_type I)))
+ thy'
| _ => thy'
end
| Atom_App _ => thy
@@ -499,6 +503,25 @@
| _ => false
end
+fun strip_applies_term (Term_FuncG (Interpreted_ExtraLogic Apply, [], [tm1, tm2])) =
+ strip_applies_term tm1 ||> (fn tms => tms @ [tm2])
+ | strip_applies_term tm = (tm, [])
+
+fun termify_apply_fmla thy config (Fmla (Interpreted_ExtraLogic Apply, [fmla1, fmla2])) =
+ (case termify_apply_fmla thy config fmla1 of
+ SOME (Term_FuncG (symb, tys, tms)) =>
+ let val typ_arity = type_arity_of_symbol thy config symb in
+ (case (null tms andalso length tys < typ_arity, try fmlatype_to_type fmla2) of
+ (true, SOME ty) => SOME (Term_FuncG (symb, tys @ [ty], []))
+ | _ =>
+ (case termify_apply_fmla thy config fmla2 of
+ SOME tm2 => SOME (Term_FuncG (symb, tys, tms @ [tm2]))
+ | NONE => NONE))
+ end
+ | _ => NONE)
+ | termify_apply_fmla _ _ (Atom (THF_Atom_term tm)) = SOME tm
+ | termify_apply_fmla _ _ _ = NONE
+
(*
Information needed to be carried around:
- constant mapping: maps constant names to Isabelle terms with fully-qualified
@@ -508,29 +531,33 @@
after each call of interpret_term since variables' cannot be bound across
terms.
*)
-fun interpret_term formula_level config language const_map var_types type_map
- tptp_t thy =
+fun interpret_term formula_level config language const_map var_types type_map tptp_t thy =
case tptp_t of
- Term_Func (symb, tptp_ts) =>
+ Term_FuncG (symb, tptp_tys, tptp_ts) =>
let
val thy' =
type_atoms_to_thy config formula_level type_map (Atom_App tptp_t) thy
in
case symb of
Interpreted_ExtraLogic Apply =>
+ (case strip_applies_term tptp_t of
+ (Term_FuncG (symb, tptp_tys, tptp_ts), extra_tptp_ts) =>
+ interpret_term formula_level config language const_map var_types type_map
+ (Term_FuncG (symb, tptp_tys, tptp_ts @ extra_tptp_ts)) thy
+ | _ =>
(*apply the head of the argument list to the tail*)
(mapply'
(fold_map (interpret_term false config language const_map
var_types type_map) (tl tptp_ts) thy')
(interpret_term formula_level config language const_map
- var_types type_map (hd tptp_ts)))
- | _ =>
+ var_types type_map (hd tptp_ts))))
+ | _ =>
let
val typ_arity = type_arity_of_symbol thy' config symb
- val (tptp_type_args, tptp_term_args) = chop typ_arity tptp_ts
+ val (tptp_type_args, tptp_term_args) = chop (typ_arity - length tptp_tys) tptp_ts
val tyargs =
- map (interpret_type config thy' type_map o termtype_to_type)
- tptp_type_args
+ map (interpret_type config thy' type_map)
+ (tptp_tys @ map termtype_to_type tptp_type_args)
in
(*apply symb to tptp_ts*)
if is_prod_typed thy' config symb then
@@ -604,38 +631,40 @@
and interpret_formula config language const_map var_types type_map tptp_fmla thy =
case tptp_fmla of
- Pred app =>
+ Pred (symb, ts) =>
interpret_term true config language const_map
- var_types type_map (Term_Func app) thy
+ var_types type_map (Term_FuncG (symb, [], ts)) thy
| Fmla (symbol, tptp_formulas) =>
(case symbol of
Interpreted_ExtraLogic Apply =>
+ (case termify_apply_fmla thy config tptp_fmla of
+ SOME tptp_t =>
+ interpret_term true config language const_map var_types type_map tptp_t thy
+ | NONE =>
mapply'
(fold_map (interpret_formula config language const_map
var_types type_map) (tl tptp_formulas) thy)
(interpret_formula config language const_map
- var_types type_map (hd tptp_formulas))
+ var_types type_map (hd tptp_formulas)))
| Uninterpreted const_name =>
let
val (args, thy') = (fold_map (interpret_formula config language
- const_map var_types type_map) tptp_formulas thy)
+ const_map var_types type_map) tptp_formulas thy)
val thy' =
type_atoms_to_thy config true type_map
- (Atom_Arity (const_name, length tptp_formulas)) thy'
+ (Atom_Arity (const_name, length tptp_formulas)) thy'
in
(if is_prod_typed thy' config symbol then
mtimes thy' args (interpret_symbol config const_map symbol [] thy')
else
- mapply args (interpret_symbol config const_map symbol [] thy'),
+ mapply args (interpret_symbol config const_map symbol [] thy'),
thy')
end
| _ =>
let
val (args, thy') =
- fold_map
- (interpret_formula config language
- const_map var_types type_map)
- tptp_formulas thy
+ fold_map (interpret_formula config language const_map var_types type_map)
+ tptp_formulas thy
in
(if is_prod_typed thy' config symbol then
mtimes thy' args (interpret_symbol config const_map symbol [] thy')
@@ -737,19 +766,20 @@
| _ => ([], tptp_type)
in
fun typeof_typing (THF_typing (_, tptp_type)) = extract_type tptp_type
- fun typeof_tff_typing (Atom (TFF_Typed_Atom (_, SOME tptp_type))) =
- extract_type tptp_type
+ | typeof_typing (Atom (TFF_Typed_Atom (_, SOME tptp_type))) = extract_type tptp_type
end
-fun nameof_typing
- (THF_typing
- ((Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))), _)) = str
-fun nameof_tff_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str
+fun nameof_typing (THF_typing
+ ((Atom (THF_Atom_term (Term_FuncG (Uninterpreted str, [], [])))), _)) = str
+ | nameof_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str
fun strip_prod_type (Prod_type (ty1, ty2)) = ty1 :: strip_prod_type ty2
| strip_prod_type ty = [ty]
-fun dest_fn_type (Fn_type (ty1, ty2)) = (strip_prod_type ty1, ty2)
+fun dest_fn_type (Fn_type (ty1, ty2)) =
+ let val (tys2, ty3) = dest_fn_type ty2 in
+ (strip_prod_type ty1 @ tys2, ty3)
+ end
| dest_fn_type ty = ([], ty)
fun resolve_include_path path_prefixes path_suffix =
@@ -758,11 +788,16 @@
SOME prefix => Path.append prefix path_suffix
| NONE => error ("Cannot find include file " ^ Path.print path_suffix)
-(* Ideally, to be in sync with TFF1, we should perform full type skolemization here.
- But the problems originating from HOL systems are restricted to top-level
- universal quantification for types. *)
+fun is_type_type (Fmla_type (Atom (THF_Atom_term (Term_FuncG (TypeSymbol Type_Type, [], []))))) =
+ true
+ | is_type_type (Defined_type Type_Type) = true
+ | is_type_type _ = false;
+
+(* Ideally, to be in sync with TFF1/THF1, we should perform full type
+ skolemization here. But the problems originating from HOL systems are
+ restricted to top-level universal quantification for types. *)
fun remove_leading_type_quantifiers (Quant (Forall, varlist, tptp_fmla)) =
- (case filter_out (curry (op =) (SOME (Defined_type Type_Type)) o snd) varlist of
+ (case filter_out (fn (_, SOME ty) => is_type_type ty | _ => false) varlist of
[] => remove_leading_type_quantifiers tptp_fmla
| varlist' => Quant (Forall, varlist', tptp_fmla))
| remove_leading_type_quantifiers tptp_fmla = tptp_fmla
@@ -788,12 +823,8 @@
Role_Type =>
let
val ((tptp_type_vars, tptp_ty), name) =
- if lang = THF then
- (typeof_typing tptp_formula (*assuming tptp_formula is a typing*),
- nameof_typing tptp_formula (*and that the LHS is a (atom) name*))
- else
- (typeof_tff_typing tptp_formula,
- nameof_tff_typing tptp_formula)
+ (typeof_typing tptp_formula (*assuming tptp_formula is a typing*),
+ nameof_typing tptp_formula (*and that the LHS is a (atom) name*))
in
case dest_fn_type tptp_ty of
(tptp_binders, Defined_type Type_Type) => (*add new type*)
@@ -865,7 +896,7 @@
(*gather interpreted term, and the map of types occurring in that term*)
val (t, thy') =
interpret_formula config lang
- const_map [] type_map (remove_leading_type_quantifiers tptp_formula) thy
+ const_map [] type_map (remove_leading_type_quantifiers tptp_formula) thy
|>> HOLogic.mk_Trueprop
(*type_maps grow monotonically, so return the newest value (type_mapped);
there's no need to unify it with the type_map parameter.*)
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Fri Dec 16 19:50:46 2016 +0100
@@ -81,7 +81,7 @@
| General_List of general_term list
and tptp_term =
- Term_Func of symbol * tptp_term list
+ Term_FuncG of symbol * tptp_type list (*special hack for TPTP_Interpret*) * tptp_term list
| Term_Var of string
| Term_Conditional of tptp_formula * tptp_term * tptp_term
| Term_Num of number_kind * string
@@ -118,6 +118,8 @@
| Fmla_type of tptp_formula
| Subtype of symbol * symbol (*only THF*)
+ val Term_Func: symbol * tptp_term list -> tptp_term (*for Yacc parser*)
+
type general_list = general_term list
type parent_details = general_list
type useful_info = general_term list
@@ -230,7 +232,7 @@
| General_List of general_term list
and tptp_term =
- Term_Func of symbol * tptp_term list
+ Term_FuncG of symbol * tptp_type list (*special hack for TPTP_Interpret*) * tptp_term list
| Term_Var of string
| Term_Conditional of tptp_formula * tptp_term * tptp_term
| Term_Num of number_kind * string
@@ -267,6 +269,8 @@
| Fmla_type of tptp_formula
| Subtype of symbol * symbol
+fun Term_Func (symb, ts) = Term_FuncG (symb, [], ts)
+
type general_list = general_term list
type parent_details = general_list
type useful_info = general_term list
@@ -405,9 +409,10 @@
fun string_of_tptp_term x =
case x of
- Term_Func (symbol, tptp_term_list) =>
+ Term_FuncG (symbol, tptp_type_list, tptp_term_list) =>
"(" ^ string_of_symbol symbol ^ " " ^
- space_implode " " (map string_of_tptp_term tptp_term_list) ^ ")"
+ space_implode " " (map string_of_tptp_type tptp_type_list
+ @ map string_of_tptp_term tptp_term_list) ^ ")"
| Term_Var str => str
| Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*)
| Term_Num (_, str) => str
@@ -531,22 +536,23 @@
(*infix symbols, including \subset, \cup, \cap*)
fun latex_of_tptp_term x =
case x of
- Term_Func (Interpreted_Logic Equals, [tptp_t1, tptp_t2]) =>
+ Term_FuncG (Interpreted_Logic Equals, [], [tptp_t1, tptp_t2]) =>
"(" ^ latex_of_tptp_term tptp_t1 ^ " = " ^ latex_of_tptp_term tptp_t2 ^ ")"
- | Term_Func (Interpreted_Logic NEquals, [tptp_t1, tptp_t2]) =>
+ | Term_FuncG (Interpreted_Logic NEquals, [], [tptp_t1, tptp_t2]) =>
"(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\neq " ^ latex_of_tptp_term tptp_t2 ^ ")"
- | Term_Func (Interpreted_Logic Or, [tptp_t1, tptp_t2]) =>
+ | Term_FuncG (Interpreted_Logic Or, [], [tptp_t1, tptp_t2]) =>
"(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\vee " ^ latex_of_tptp_term tptp_t2 ^ ")"
- | Term_Func (Interpreted_Logic And, [tptp_t1, tptp_t2]) =>
+ | Term_FuncG (Interpreted_Logic And, [], [tptp_t1, tptp_t2]) =>
"(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\wedge " ^ latex_of_tptp_term tptp_t2 ^ ")"
- | Term_Func (Interpreted_Logic Iff, [tptp_t1, tptp_t2]) =>
+ | Term_FuncG (Interpreted_Logic Iff, [], [tptp_t1, tptp_t2]) =>
"(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")"
- | Term_Func (Interpreted_Logic If, [tptp_t1, tptp_t2]) =>
+ | Term_FuncG (Interpreted_Logic If, [], [tptp_t1, tptp_t2]) =>
"(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")"
- | Term_Func (symbol, tptp_term_list) =>
+ | Term_FuncG (symbol, tptp_type_list, tptp_term_list) =>
(*"(" ^*) latex_of_symbol symbol ^ "\\\\, " ^
- space_implode "\\\\, " (map latex_of_tptp_term tptp_term_list) (*^ ")"*)
+ space_implode "\\\\, " (map latex_of_tptp_type tptp_type_list
+ @ map latex_of_tptp_term tptp_term_list) (*^ ")"*)
| Term_Var str => "\\\\mathrm{" ^ str ^ "}"
| Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*)
| Term_Num (_, str) => str
@@ -647,10 +653,10 @@
latex_of_symbol symbol ^
space_implode "\\\\, " (map latex_of_tptp_term tptp_term_list)
- | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "union", []))), tptp_f1]), tptp_f2])) =
+ | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_FuncG (Uninterpreted "union", [], []))), tptp_f1]), tptp_f2])) =
"(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_f2 ^ ")"
- | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "subset", []))), tptp_f1]), tptp_f2])) =
+ | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_FuncG (Uninterpreted "subset", [], []))), tptp_f1]), tptp_f2])) =
"(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_f2 ^ ")"
| latex_of_tptp_formula (Fmla (Interpreted_Logic Equals, [tptp_f1, tptp_f2])) =
--- a/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML Fri Dec 16 19:50:46 2016 +0100
@@ -96,7 +96,7 @@
which we interpret to be the last line of the proof.*)
fun is_last_line CNF (Pred (Interpreted_Logic False, [])) = true
| is_last_line THF (Atom (THF_Atom_term
- (Term_Func (Interpreted_Logic False, [])))) = true
+ (Term_Func (Interpreted_Logic False, [], [])))) = true
| is_last_line _ _ = false
fun tptp_dot_node with_label reverse_arrows
--- a/src/HOL/TPTP/atp_problem_import.ML Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Fri Dec 16 19:50:46 2016 +0100
@@ -11,7 +11,7 @@
'a list * ('a list * 'a list) * Proof.context
val nitpick_tptp_file : theory -> int -> string -> unit
val refute_tptp_file : theory -> int -> string -> unit
- val can_tac : Proof.context -> tactic -> term -> bool
+ val can_tac : Proof.context -> (Proof.context -> tactic) -> term -> bool
val SOLVE_TIMEOUT : int -> string -> tactic -> tactic
val atp_tac : Proof.context -> int -> (string * string) list -> int -> term list -> string ->
int -> tactic
@@ -131,14 +131,15 @@
(** Sledgehammer and Isabelle (combination of provers) **)
-fun can_tac ctxt tactic conj = can (Goal.prove ctxt [] [] conj) (K tactic)
+fun can_tac ctxt tactic conj =
+ can (Goal.prove_internal ctxt [] (Thm.cterm_of ctxt conj)) (fn [] => tactic ctxt)
fun SOLVE_TIMEOUT seconds name tac st =
let
val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
val result =
Timeout.apply (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
- handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE
+ handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE
in
(case result of
NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
@@ -274,7 +275,7 @@
val conj = make_conj ([], []) conjs
val assms = op @ assms
in
- can_tac ctxt (sledgehammer_tac true ctxt timeout assms 1) conj
+ can_tac ctxt (fn ctxt => sledgehammer_tac true ctxt timeout assms 1) conj
|> print_szs_of_success conjs
end
@@ -287,9 +288,9 @@
val (last_hope_atp, last_hope_completeness) =
if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2)
in
- (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) assms 1) full_conj orelse
- can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) assms 1) conj orelse
- can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
+ (can_tac ctxt (fn ctxt => auto_etc_tac ctxt (timeout div 2) assms 1) full_conj orelse
+ can_tac ctxt (fn ctxt => sledgehammer_tac demo ctxt (timeout div 2) assms 1) conj orelse
+ can_tac ctxt (fn ctxt => SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
(atp_tac ctxt last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj)
|> print_szs_of_success conjs
end
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Fri Dec 16 19:50:46 2016 +0100
@@ -24,12 +24,12 @@
TIMEOUT=$1
shift
-isabelle build -b HOL-TPTP
+isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Fri Dec 16 19:50:46 2016 +0100
@@ -24,12 +24,12 @@
TIMEOUT=$1
shift
-isabelle build -b HOL-TPTP
+isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_nitpick Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick Fri Dec 16 19:50:46 2016 +0100
@@ -24,12 +24,12 @@
TIMEOUT=$1
shift
-isabelle build -b HOL-TPTP
+isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_refute Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute Fri Dec 16 19:50:46 2016 +0100
@@ -23,12 +23,12 @@
TIMEOUT=$1
shift
-isabelle build -b HOL-TPTP
+isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Fri Dec 16 19:50:46 2016 +0100
@@ -24,12 +24,12 @@
TIMEOUT=$1
shift
-isabelle build -b HOL-TPTP
+isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
> /tmp/$SCRATCH.thy
- isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+ isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_translate Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate Fri Dec 16 19:50:46 2016 +0100
@@ -23,9 +23,9 @@
args=("$@")
-isabelle build -b HOL-TPTP
+isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \
> /tmp/$SCRATCH.thy
-isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
+isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Fri Dec 16 19:50:46 2016 +0100
@@ -1159,24 +1159,34 @@
|> `(curry fastype_of1 bound_Ts)
|>> build_params bound_Us bound_Ts
|-> explore;
- val Us = map (fpT_to ssig_T) (snd (dest_Type (fastype_of1 (bound_Us, mapped_arg'))));
- val temporary_map = map_tm
- |> mk_map n Us Ts;
- val map_fn_Ts = fastype_of #> strip_fun_type #> fst;
- val binder_Uss = map_fn_Ts temporary_map
- |> map (map (fpT_to ssig_T) o binder_types);
- val fun_paramss = map_fn_Ts (head_of func)
- |> map (build_params bound_Us bound_Ts);
- val fs' = fs |> @{map 4} explore_fun binder_Uss (replicate n explore) fun_paramss;
- val SOME bnf = bnf_of lthy T_name;
- val Type (_, bnf_Ts) = T_of_bnf bnf;
- val typ_alist =
- lives_of_bnf bnf ~~ map (curry fastype_of1 bound_Us #> range_type) fs';
- val Us' = map2 the_default Us (map (AList.lookup (op =) typ_alist) bnf_Ts);
- val map_tm' = map_tm |> mk_map n Us Us';
in
- build_function_after_encapsulation func (list_comb (map_tm', fs')) params [mapped_arg]
- [mapped_arg']
+ (case fastype_of1 (bound_Us, mapped_arg') of
+ Type (U_name, Us0) =>
+ if U_name = T_name then
+ let
+ val Us = map (fpT_to ssig_T) Us0;
+ val temporary_map = map_tm
+ |> mk_map n Us Ts;
+ val map_fn_Ts = fastype_of #> strip_fun_type #> fst;
+ val binder_Uss = map_fn_Ts temporary_map
+ |> map (map (fpT_to ssig_T) o binder_types);
+ val fun_paramss = map_fn_Ts (head_of func)
+ |> map (build_params bound_Us bound_Ts);
+ val fs' = fs
+ |> @{map 4} explore_fun binder_Uss (replicate n explore) fun_paramss;
+ val SOME bnf = bnf_of lthy T_name;
+ val Type (_, bnf_Ts) = T_of_bnf bnf;
+ val typ_alist =
+ lives_of_bnf bnf ~~ map (curry fastype_of1 bound_Us #> range_type) fs';
+ val Us' = map2 the_default Us (map (AList.lookup (op =) typ_alist) bnf_Ts);
+ val map_tm' = map_tm |> mk_map n Us Us';
+ in
+ build_function_after_encapsulation func (list_comb (map_tm', fs')) params
+ [mapped_arg] [mapped_arg']
+ end
+ else
+ explore params t
+ | _ => explore params t)
end
| NONE => explore params t)
| massage_map explore params t = explore params t;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Fri Dec 16 19:07:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Fri Dec 16 19:50:46 2016 +0100
@@ -156,7 +156,8 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
unfold_thms_tac ctxt [rel_def] THEN
- HEADGOAL (rtac ctxt (@{thm Abs_transfer} OF [type_definition, type_definition]))))
+ HEADGOAL (rtac ctxt refl ORELSE'
+ rtac ctxt (@{thm Abs_transfer} OF [type_definition, type_definition]))))
end
end;
@@ -178,7 +179,7 @@
Variable.add_free_names ctxt goal []
|> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
unfold_thms_tac ctxt [rel_def] THEN
- HEADGOAL (rtac ctxt @{thm vimage2p_rel_fun})))
+ HEADGOAL (rtac ctxt refl ORELSE' rtac ctxt @{thm vimage2p_rel_fun})))
end
end;