--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Apr 27 18:58:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Apr 28 12:46:50 2010 +0200
@@ -33,6 +33,10 @@
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
struct
+datatype ('a, 'b, 'c, 'd, 'e) raw_step =
+ Definition of 'a * 'b * 'c |
+ Inference of 'a * 'd * 'e list
+
open Sledgehammer_Util
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
@@ -53,11 +57,11 @@
(**** PARSING OF TSTP FORMAT ****)
(* Syntax trees, either term list or formulae *)
-datatype stree = SInt of int | SBranch of string * stree list;
+datatype node = IntLeaf of int | StrNode of string * node list
-fun atom x = SBranch (x, [])
+fun atom x = StrNode (x, [])
-fun scons (x, y) = SBranch ("cons", [x, y])
+fun scons (x, y) = StrNode ("cons", [x, y])
val slist_of = List.foldl scons (atom "nil")
(*Strings enclosed in single quotes, e.g. filenames*)
@@ -75,54 +79,63 @@
(* The "x" argument is not strictly necessary, but without it Poly/ML loops
forever at compile time. *)
fun parse_term pool x =
- (parse_quoted >> atom
- || parse_integer >> SInt
+ (parse_quoted >> atom
+ || parse_integer >> IntLeaf
|| $$ "$" |-- Symbol.scan_id >> (atom o repair_bool_literal)
|| (Symbol.scan_id >> repair_name pool)
- -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> SBranch
+ -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
|| $$ "(" |-- parse_term pool --| $$ ")"
|| $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
and parse_terms pool x =
(parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
-fun negate_stree t = SBranch ("c_Not", [t])
-fun equate_strees t1 t2 = SBranch ("c_equal", [t1, t2]);
+fun negate_node u = StrNode ("c_Not", [u])
+fun equate_nodes u1 u2 = StrNode ("c_equal", [u1, u2])
(* Apply equal or not-equal to a term. *)
-fun repair_predicate_term (t, NONE) = t
- | repair_predicate_term (t1, SOME (NONE, t2)) = equate_strees t1 t2
- | repair_predicate_term (t1, SOME (SOME _, t2)) =
- negate_stree (equate_strees t1 t2)
+fun repair_predicate_term (u, NONE) = u
+ | repair_predicate_term (u1, SOME (NONE, u2)) = equate_nodes u1 u2
+ | repair_predicate_term (u1, SOME (SOME _, u2)) =
+ negate_node (equate_nodes u1 u2)
fun parse_predicate_term pool =
parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
-- parse_term pool)
>> repair_predicate_term
-(*Literals can involve negation, = and !=.*)
+(* Literals can involve "~", "=", and "!=". *)
fun parse_literal pool x =
- ($$ "~" |-- parse_literal pool >> negate_stree || parse_predicate_term pool) x
+ ($$ "~" |-- parse_literal pool >> negate_node || parse_predicate_term pool) x
fun parse_literals pool =
parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
-(* Clause: a list of literals separated by the disjunction sign. *)
+(* Clause: a list of literals separated by disjunction operators ("|"). *)
fun parse_clause pool =
$$ "(" |-- parse_literals pool --| $$ ")" || Scan.single (parse_literal pool)
-fun ints_of_stree (SInt n) = cons n
- | ints_of_stree (SBranch (_, ts)) = fold ints_of_stree ts
+fun ints_of_node (IntLeaf n) = cons n
+ | ints_of_node (StrNode (_, us)) = fold ints_of_node us
val parse_tstp_annotations =
Scan.optional ($$ "," |-- parse_term NONE
--| Scan.option ($$ "," |-- parse_terms NONE)
- >> (fn source => ints_of_stree source [])) []
+ >> (fn source => ints_of_node source [])) []
+
+fun parse_definition pool =
+ $$ "(" |-- parse_literal NONE --| Scan.this_string "<=>"
+ -- parse_clause pool --| $$ ")"
-(* cnf(<name>, <formula_role>, <cnf_formula> <annotations>).
- The <name> could be an identifier, but we assume integers. *)
-fun retuple_tstp_line ((name, ts), deps) = (name, ts, deps)
+(* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
+ The <num> could be an identifier, but we assume integers. *)
+fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
+fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
fun parse_tstp_line pool =
- (Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
- --| Symbol.scan_id --| $$ "," -- parse_clause pool -- parse_tstp_annotations
- --| $$ ")" --| $$ "."
- >> retuple_tstp_line
+ ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ ","
+ --| Scan.this_string "definition" --| $$ "," -- parse_definition pool
+ --| parse_tstp_annotations --| $$ ")" --| $$ "."
+ >> finish_tstp_definition_line)
+ || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
+ --| Symbol.scan_id --| $$ "," -- parse_clause pool
+ -- parse_tstp_annotations --| $$ ")" --| $$ "."
+ >> finish_tstp_inference_line)
(**** PARSING OF SPASS OUTPUT ****)
@@ -143,22 +156,22 @@
Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">"
-- Scan.repeat (parse_starred_predicate_term pool)
>> (fn ([], []) => [atom "c_False"]
- | (clauses1, clauses2) => map negate_stree clauses1 @ clauses2)
+ | (clauses1, clauses2) => map negate_node clauses1 @ clauses2)
-(* Syntax: <name>[0:<inference><annotations>] ||
+(* Syntax: <num>[0:<inference><annotations>] ||
<cnf_formulas> -> <cnf_formulas>. *)
-fun retuple_spass_line ((name, deps), ts) = (name, ts, deps)
+fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
fun parse_spass_line pool =
parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
-- parse_spass_annotations --| $$ "]" --| $$ "|" --| $$ "|"
-- parse_horn_clause pool --| $$ "."
- >> retuple_spass_line
+ >> finish_spass_line
fun parse_line pool = fst o (parse_tstp_line pool || parse_spass_line pool)
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
-exception STREE of stree;
+exception NODE of node
(*If string s has the prefix s1, return the result of deleting it.*)
fun strip_prefix s1 s =
@@ -181,24 +194,21 @@
(*Type variables are given the basic sort, HOL.type. Some will later be constrained
by information from type literals, or by type inference.*)
-fun type_of_stree t =
- case t of
- SInt _ => raise STREE t
- | SBranch (a,ts) =>
- let val Ts = map type_of_stree ts
- in
- case strip_prefix tconst_prefix a of
- SOME b => Type(invert_type_const b, Ts)
- | NONE =>
- if not (null ts) then raise STREE t (*only tconsts have type arguments*)
- else
- case strip_prefix tfree_prefix a of
- SOME b => TFree("'" ^ b, HOLogic.typeS)
- | NONE =>
- case strip_prefix tvar_prefix a of
- SOME b => make_tvar b
- | NONE => make_tparam a (* Variable from the ATP, say "X1" *)
- end;
+fun type_of_node (u as IntLeaf _) = raise NODE u
+ | type_of_node (u as StrNode (a, us)) =
+ let val Ts = map type_of_node us in
+ case strip_prefix tconst_prefix a of
+ SOME b => Type (invert_type_const b, Ts)
+ | NONE =>
+ if not (null us) then
+ raise NODE u (*only tconsts have type arguments*)
+ else case strip_prefix tfree_prefix a of
+ SOME b => TFree ("'" ^ b, HOLogic.typeS)
+ | NONE =>
+ case strip_prefix tvar_prefix a of
+ SOME b => make_tvar b
+ | NONE => make_tparam a (* Variable from the ATP, say "X1" *)
+ end
(*Invert the table of translations between Isabelle and ATPs*)
val const_trans_table_inv =
@@ -213,46 +223,68 @@
(*Generates a constant, given its type arguments*)
fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts));
+fun fix_atp_variable_name s =
+ let
+ fun subscript_name s n = s ^ nat_subscript n
+ val s = String.map Char.toLower s
+ in
+ case space_explode "_" s of
+ [_] => (case take_suffix Char.isDigit (String.explode s) of
+ (cs1 as _ :: _, cs2 as _ :: _) =>
+ subscript_name (String.implode cs1)
+ (the (Int.fromString (String.implode cs2)))
+ | (_, _) => s)
+ | [s1, s2] => (case Int.fromString s2 of
+ SOME n => subscript_name s1 n
+ | NONE => s)
+ | _ => s
+ end
+
(*First-order translation. No types are known for variables. HOLogic.typeT should allow
them to be inferred.*)
-fun term_of_stree args thy t =
- case t of
- SInt _ => raise STREE t
- | SBranch ("hBOOL", [t]) => term_of_stree [] thy t (*ignore hBOOL*)
- | SBranch ("hAPP", [t, u]) => term_of_stree (u::args) thy t
- | SBranch (a, ts) =>
- case strip_prefix const_prefix a of
- SOME "equal" =>
- list_comb(Const (@{const_name "op ="}, HOLogic.typeT), List.map (term_of_stree [] thy) ts)
- | SOME b =>
- let val c = invert_const b
- val nterms = length ts - num_typargs thy c
- val us = List.map (term_of_stree [] thy) (List.take(ts,nterms) @ args)
- (*Extra args from hAPP come AFTER any arguments given directly to the
- constant.*)
- val Ts = List.map type_of_stree (List.drop(ts,nterms))
- in list_comb(const_of thy (c, Ts), us) end
- | NONE => (*a variable, not a constant*)
- let val T = HOLogic.typeT
- val opr = (*a Free variable is typically a Skolem function*)
- case strip_prefix fixed_var_prefix a of
- SOME b => Free(b,T)
- | NONE =>
- case strip_prefix schematic_var_prefix a of
- SOME b => make_var (b,T)
- | NONE => make_var (a,T) (* Variable from the ATP, say "X1" *)
- in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end;
+fun term_of_node args thy u =
+ case u of
+ IntLeaf _ => raise NODE u
+ | StrNode ("hBOOL", [u]) => term_of_node [] thy u (* ignore hBOOL *)
+ | StrNode ("hAPP", [u1, u2]) => term_of_node (u2 :: args) thy u1
+ | StrNode (a, us) =>
+ case strip_prefix const_prefix a of
+ SOME "equal" =>
+ list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
+ map (term_of_node [] thy) us)
+ | SOME b =>
+ let
+ val c = invert_const b
+ val nterms = length us - num_typargs thy c
+ val ts = map (term_of_node [] thy) (take nterms us @ args)
+ (*Extra args from hAPP come AFTER any arguments given directly to the
+ constant.*)
+ val Ts = map type_of_node (drop nterms us)
+ in list_comb(const_of thy (c, Ts), ts) end
+ | NONE => (*a variable, not a constant*)
+ let
+ val opr =
+ (* a Free variable is typically a Skolem function *)
+ case strip_prefix fixed_var_prefix a of
+ SOME b => Free (b, HOLogic.typeT)
+ | NONE =>
+ case strip_prefix schematic_var_prefix a of
+ SOME b => make_var (b, HOLogic.typeT)
+ | NONE =>
+ (* Variable from the ATP, say "X1" *)
+ make_var (fix_atp_variable_name a, HOLogic.typeT)
+ in list_comb (opr, map (term_of_node [] thy) (us @ args)) end
(* Type class literal applied to a type. Returns triple of polarity, class,
type. *)
-fun constraint_of_stree pol (SBranch ("c_Not", [t])) =
- constraint_of_stree (not pol) t
- | constraint_of_stree pol t = case t of
- SInt _ => raise STREE t
- | SBranch (a, ts) =>
- (case (strip_prefix class_prefix a, map type_of_stree ts) of
- (SOME b, [T]) => (pol, b, T)
- | _ => raise STREE t);
+fun constraint_of_node pos (StrNode ("c_Not", [u])) =
+ constraint_of_node (not pos) u
+ | constraint_of_node pos u = case u of
+ IntLeaf _ => raise NODE u
+ | StrNode (a, us) =>
+ (case (strip_prefix class_prefix a, map type_of_node us) of
+ (SOME b, [T]) => (pos, b, T)
+ | _ => raise NODE u)
(** Accumulate type constraints in a clause: negative type literals **)
@@ -276,7 +308,8 @@
@{const "op |"} $ negate_term thy t1 $ negate_term thy t2
| negate_term thy (@{const "op |"} $ t1 $ t2) =
@{const "op &"} $ negate_term thy t1 $ negate_term thy t2
- | negate_term thy (@{const Not} $ t) = t
+ | negate_term _ (@{const Not} $ t) = t
+ | negate_term _ t = @{const Not} $ t
fun negate_formula thy (@{const Trueprop} $ t) =
@{const Trueprop} $ negate_term thy t
| negate_formula thy t =
@@ -301,11 +334,10 @@
|> clause_for_literals thy
(*Accumulate sort constraints in vt, with "real" literals in lits.*)
-fun lits_of_strees thy (vt, lits) [] = (vt, finish_clause thy lits)
- | lits_of_strees thy (vt, lits) (t :: ts) =
- lits_of_strees thy (add_constraint (constraint_of_stree true t, vt), lits)
- ts
- handle STREE _ => lits_of_strees thy (vt, term_of_stree [] thy t :: lits) ts
+fun lits_of_nodes thy (vt, lits) [] = (vt, finish_clause thy lits)
+ | lits_of_nodes thy (vt, lits) (u :: us) =
+ lits_of_nodes thy (add_constraint (constraint_of_node true u, vt), lits) us
+ handle NODE _ => lits_of_nodes thy (vt, term_of_node [] thy u :: lits) us
(*Update TVars/TFrees with detected sort constraints.*)
fun repair_sorts vt =
@@ -317,103 +349,133 @@
| tmsubst (Var (xi, T)) = Var (xi, tysubst T)
| tmsubst (t as Bound _) = t
| tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
- | tmsubst (t $ u) = tmsubst t $ tmsubst u;
+ | tmsubst (t1 $ t2) = tmsubst t1 $ tmsubst t2
in not (Vartab.is_empty vt) ? tmsubst end;
-(*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
- vt0 holds the initial sort constraints, from the conjecture clauses.*)
-fun clause_of_strees ctxt vt ts =
- let val (vt, dt) = lits_of_strees (ProofContext.theory_of ctxt) (vt, []) ts in
- dt |> repair_sorts vt |> TypeInfer.constrain HOLogic.boolT
- |> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic
- ctxt)
- end
-
-fun decode_line vt0 (name, ts, deps) ctxt =
- let val cl = clause_of_strees ctxt vt0 ts in
- ((name, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
+(* Interpret a list of syntax trees as a clause, given by "real" literals and
+ sort constraints. "vt" holds the initial sort constraints, from the
+ conjecture clauses. *)
+fun clause_of_nodes ctxt vt us =
+ let val (vt, dt) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in
+ dt |> repair_sorts vt
end
-
-(** Global sort constraints on TFrees (from tfree_tcs) are positive unit clauses. **)
+fun check_clause ctxt =
+ TypeInfer.constrain HOLogic.boolT
+ #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
+fun checked_clause_of_nodes ctxt = check_clause ctxt oo clause_of_nodes ctxt
-fun add_tfree_constraint ((true, cl, TFree(a,_)), vt) =
- add_var ((a, ~1) , cl) vt
- | add_tfree_constraint (_, vt) = vt;
+(** Global sort constraints on TFrees (from tfree_tcs) are positive unit
+ clauses. **)
+fun add_tfree_constraint (true, cl, TFree (a, _)) = add_var ((a, ~1), cl)
+ | add_tfree_constraint _ = I
fun tfree_constraints_of_clauses vt [] = vt
- | tfree_constraints_of_clauses vt ([lit]::tss) =
- (tfree_constraints_of_clauses (add_tfree_constraint (constraint_of_stree true lit, vt)) tss
- handle STREE _ => (*not a positive type constraint: ignore*)
- tfree_constraints_of_clauses vt tss)
- | tfree_constraints_of_clauses vt (_::tss) = tfree_constraints_of_clauses vt tss;
+ | tfree_constraints_of_clauses vt ([lit] :: uss) =
+ (tfree_constraints_of_clauses (add_tfree_constraint
+ (constraint_of_node true lit) vt) uss
+ handle NODE _ => (* Not a positive type constraint? Ignore the literal. *)
+ tfree_constraints_of_clauses vt uss)
+ | tfree_constraints_of_clauses vt (_ :: uss) =
+ tfree_constraints_of_clauses vt uss
(**** Translation of TSTP files to Isar Proofs ****)
-fun decode_lines ctxt tuples =
- let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #2 tuples) in
- #1 (fold_map (decode_line vt0) tuples ctxt)
- end
+fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
+ | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
-fun unequal t (_, t', _) = not (t aconv t');
+fun clauses_in_lines (Definition (_, u, us)) = u :: us
+ | clauses_in_lines (Inference (_, us, _)) = us
-(*No "real" literals means only type information*)
-fun eq_types t = t aconv HOLogic.true_const;
+fun decode_line vt (Definition (num, u, us)) ctxt =
+ let
+ val cl1 = clause_of_nodes ctxt vt [u]
+ val vars = snd (strip_comb cl1)
+ val frees = map unvarify_term vars
+ val unvarify_args = subst_atomic (vars ~~ frees)
+ val cl2 = clause_of_nodes ctxt vt us
+ val (cl1, cl2) =
+ HOLogic.eq_const HOLogic.typeT $ cl1 $ cl2
+ |> unvarify_args |> check_clause ctxt |> HOLogic.dest_eq
+ in
+ (Definition (num, cl1, cl2),
+ fold Variable.declare_term (maps OldTerm.term_frees [cl1, cl2]) ctxt)
+ end
+ | decode_line vt (Inference (num, us, deps)) ctxt =
+ let val cl = us |> clause_of_nodes ctxt vt |> check_clause ctxt in
+ (Inference (num, cl, deps),
+ fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
+ end
+fun decode_lines ctxt lines =
+ let
+ val vt = tfree_constraints_of_clauses Vartab.empty
+ (map clauses_in_lines lines)
+ in #1 (fold_map (decode_line vt) lines ctxt) end
-fun replace_dep (old, new) dep = if dep = old then new else [dep]
-fun replace_deps p (num, t, deps) =
- (num, t, fold (union (op =) o replace_dep p) deps [])
+fun aint_inference _ (Definition _) = true
+ | aint_inference t (Inference (_, t', _)) = not (t aconv t')
+
+(* No "real" literals means only type information (tfree_tcs, clsrel, or
+ clsarity). *)
+val is_only_type_information = curry (op aconv) HOLogic.true_const
+
+fun replace_one_dep (old, new) dep = if dep = old then new else [dep]
+fun replace_deps_in_line _ (line as Definition _) = line
+ | replace_deps_in_line p (Inference (num, t, deps)) =
+ Inference (num, t, fold (union (op =) o replace_one_dep p) deps [])
(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
only in type information.*)
-fun add_line thm_names (num, t, []) lines =
- (* No dependencies: axiom or conjecture clause? *)
- if is_axiom_clause_number thm_names num then
- (* Axioms are not proof lines *)
- if eq_types t then
- (* Must be clsrel/clsarity: type information, so delete refs to it *)
- map (replace_deps (num, [])) lines
- else
- (case take_prefix (unequal t) lines of
- (_,[]) => lines (*no repetition of proof line*)
- | (pre, (num', _, _) :: post) => (*repetition: replace later line by earlier one*)
- pre @ map (replace_deps (num', [num])) post)
- else
- (num, t, []) :: lines
- | add_line _ (num, t, deps) lines =
- if eq_types t then (num, t, deps) :: lines
- (*Type information will be deleted later; skip repetition test.*)
- else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
- case take_prefix (unequal t) lines of
- (_,[]) => (num, t, deps) :: lines (*no repetition of proof line*)
- | (pre, (num', t', _) :: post) =>
- (num, t', deps) :: (*repetition: replace later line by earlier one*)
- (pre @ map (replace_deps (num', [num])) post);
+fun add_line _ (line as Definition _) lines = line :: lines
+ | add_line thm_names (Inference (num, t, [])) lines =
+ (* No dependencies: axiom or conjecture clause *)
+ if is_axiom_clause_number thm_names num then
+ (* Axioms are not proof lines. *)
+ if is_only_type_information t then
+ map (replace_deps_in_line (num, [])) lines
+ (* Is there a repetition? If so, replace later line by earlier one. *)
+ else case take_prefix (aint_inference t) lines of
+ (_, []) => lines (*no repetition of proof line*)
+ | (pre, Inference (num', _, _) :: post) =>
+ pre @ map (replace_deps_in_line (num', [num])) post
+ else
+ Inference (num, t, []) :: lines
+ | add_line _ (Inference (num, t, deps)) lines =
+ (* Type information will be deleted later; skip repetition test. *)
+ if is_only_type_information t then
+ Inference (num, t, deps) :: lines
+ (* Is there a repetition? If so, replace later line by earlier one. *)
+ else case take_prefix (aint_inference t) lines of
+ (* FIXME: Doesn't this code risk conflating proofs involving different
+ types?? *)
+ (_, []) => Inference (num, t, deps) :: lines
+ | (pre, Inference (num', t', _) :: post) =>
+ Inference (num, t', deps) ::
+ pre @ map (replace_deps_in_line (num', [num])) post
-(*Recursively delete empty lines (type information) from the proof.*)
-fun add_nonnull_line (num, t, []) lines = (*no dependencies, so a conjecture clause*)
- if eq_types t then
- (*must be type information, tfree_tcs, clsrel, clsarity: delete refs to it*)
- delete_dep num lines
- else
- (num, t, []) :: lines
- | add_nonnull_line (num, t, deps) lines = (num, t, deps) :: lines
+(* Recursively delete empty lines (type information) from the proof. *)
+fun add_nontrivial_line (Inference (num, t, [])) lines =
+ if is_only_type_information t then delete_dep num lines
+ else Inference (num, t, []) :: lines
+ | add_nontrivial_line line lines = line :: lines
and delete_dep num lines =
- fold_rev add_nonnull_line (map (replace_deps (num, [])) lines) []
+ fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
+
+fun is_bad_free (Free (a, _)) = String.isPrefix skolem_prefix a
+ | is_bad_free _ = false
-fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a
- | bad_free _ = false;
-
-fun add_desired_line ctxt _ (num, t, []) (j, lines) =
- (j, (num, t, []) :: lines) (* conjecture clauses must be kept *)
- | add_desired_line ctxt shrink_factor (num, t, deps) (j, lines) =
+fun add_desired_line _ _ (line as Definition _) (j, lines) = (j, line :: lines)
+ | add_desired_line ctxt _ (Inference (num, t, [])) (j, lines) =
+ (j, Inference (num, t, []) :: lines) (* conjecture clauses must be kept *)
+ | add_desired_line ctxt shrink_factor (Inference (num, t, deps)) (j, lines) =
(j + 1,
- if eq_types t orelse not (null (Term.add_tvars t [])) orelse
- exists_subterm bad_free t orelse
+ if is_only_type_information t orelse
+ not (null (Term.add_tvars t [])) orelse
+ exists_subterm is_bad_free t orelse
(length deps < 2 orelse j mod shrink_factor <> 0) then
- map (replace_deps (num, deps)) lines (* delete line *)
+ map (replace_deps_in_line (num, deps)) lines (* delete line *)
else
- (num, t, deps) :: lines)
+ Inference (num, t, deps) :: lines)
(** EXTRACTING LEMMAS **)
@@ -465,20 +527,22 @@
val n = Logic.count_prems (prop_of goal)
in (metis_line i n lemmas ^ minimize_line minimize_command lemmas, lemmas) end
-val is_valid_line = String.isPrefix "cnf(" orf String.isSubstring "||"
+val is_valid_line =
+ String.isPrefix "fof(" orf String.isPrefix "cnf(" orf String.isSubstring "||"
-(** NEW PROOF RECONSTRUCTION CODE **)
+(** Isar proof construction and manipulation **)
+
+fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
+ (union (op =) ls1 ls2, union (op =) ss1 ss2)
type label = string * int
type facts = label list * string list
-fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
- (union (op =) ls1 ls2, union (op =) ss1 ss2)
-
datatype qualifier = Show | Then | Moreover | Ultimately
datatype step =
Fix of (string * typ) list |
+ Let of term * term |
Assume of label * term |
Have of qualifier list * label * term * byline
and byline =
@@ -495,11 +559,12 @@
else
apfst (insert (op =) (raw_prefix, num))
-fun generalize_all_vars t = fold_rev Logic.all (map Var (Term.add_vars t [])) t
-fun step_for_tuple _ _ (label, t, []) = Assume ((raw_prefix, label), t)
- | step_for_tuple thm_names j (label, t, deps) =
- Have (if j = 1 then [Show] else [], (raw_prefix, label),
- generalize_all_vars (HOLogic.mk_Trueprop t),
+fun quantify_over_all_vars t = fold_rev Logic.all (map Var ((*Term.add_vars t###*) [])) t
+fun step_for_line _ _ (Definition (num, t1, t2)) = Let (t1, t2)
+ | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
+ | step_for_line thm_names j (Inference (num, t, deps)) =
+ Have (if j = 1 then [Show] else [], (raw_prefix, num),
+ quantify_over_all_vars (HOLogic.mk_Trueprop t),
Facts (fold (add_fact_from_dep thm_names) deps ([], [])))
fun strip_spaces_in_list [] = ""
@@ -521,18 +586,18 @@
fun proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names frees =
let
- val tuples =
- atp_proof |> split_lines |> map strip_spaces
- |> filter is_valid_line
- |> map (parse_line pool o explode)
- |> decode_lines ctxt
- val tuples = fold_rev (add_line thm_names) tuples []
- val tuples = fold_rev add_nonnull_line tuples []
- val tuples = fold_rev (add_desired_line ctxt shrink_factor) tuples (0, [])
- |> snd
+ val lines =
+ atp_proof
+ |> split_lines |> map strip_spaces |> filter is_valid_line
+ |> map (parse_line pool o explode)
+ |> decode_lines ctxt
+ |> rpair [] |-> fold_rev (add_line thm_names)
+ |> rpair [] |-> fold_rev add_nontrivial_line
+ |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor)
+ |> snd
in
(if null frees then [] else [Fix frees]) @
- map2 (step_for_tuple thm_names) (length tuples downto 1) tuples
+ map2 (step_for_line thm_names) (length lines downto 1) lines
end
val indent_size = 2
@@ -555,6 +620,7 @@
and using_of proof = fold (union (op =) o using_of_step) proof []
fun new_labels_of_step (Fix _) = []
+ | new_labels_of_step (Let _) = []
| new_labels_of_step (Assume (l, _)) = [l]
| new_labels_of_step (Have (_, l, _, _)) = [l]
val new_labels_of = maps new_labels_of_step
@@ -594,6 +660,8 @@
fun first_pass ([], contra) = ([], contra)
| first_pass ((ps as Fix _) :: proof, contra) =
first_pass (proof, contra) |>> cons ps
+ | first_pass ((ps as Let _) :: proof, contra) =
+ first_pass (proof, contra) |>> cons ps
| first_pass ((ps as Assume (l, t)) :: proof, contra) =
if member (op =) concl_ls l then
first_pass (proof, contra ||> cons ps)
@@ -671,17 +739,15 @@
end
| _ => raise Fail "malformed proof")
| second_pass _ _ = raise Fail "malformed proof"
- val (proof_bottom, _) =
- second_pass [Show] (contra_proof, [], ([], ([], [])))
+ val proof_bottom =
+ second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
in proof_top @ proof_bottom end
val kill_duplicate_assumptions_in_proof =
let
fun relabel_facts subst =
apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
- fun do_step (ps as Fix _) (proof, subst, assums) =
- (ps :: proof, subst, assums)
- | do_step (ps as Assume (l, t)) (proof, subst, assums) =
+ fun do_step (ps as Assume (l, t)) (proof, subst, assums) =
(case AList.lookup (op aconv) assums t of
SOME l' => (proof, (l', l) :: subst, assums)
| NONE => (ps :: proof, subst, (t, l) :: assums))
@@ -692,13 +758,13 @@
| CaseSplit (proofs, facts) =>
CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
proof, subst, assums)
+ | do_step ps (proof, subst, assums) = (ps :: proof, subst, assums)
and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
in do_proof end
val then_chain_proof =
let
fun aux _ [] = []
- | aux _ ((ps as Fix _) :: proof) = ps :: aux no_label proof
| aux _ ((ps as Assume (l, _)) :: proof) = ps :: aux l proof
| aux l' (Have (qs, l, t, by) :: proof) =
(case by of
@@ -711,20 +777,21 @@
| CaseSplit (proofs, facts) =>
Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
aux l proof
+ | aux _ (ps :: proof) = ps :: aux no_label proof
in aux no_label end
fun kill_useless_labels_in_proof proof =
let
val used_ls = using_of proof
fun do_label l = if member (op =) used_ls l then l else no_label
- fun kill (Fix xs) = Fix xs
- | kill (Assume (l, t)) = Assume (do_label l, t)
+ fun kill (Assume (l, t)) = Assume (do_label l, t)
| kill (Have (qs, l, t, by)) =
Have (qs, do_label l, t,
case by of
CaseSplit (proofs, facts) =>
CaseSplit (map (map kill) proofs, facts)
| _ => by)
+ | kill ps = ps
in map kill proof end
fun prefix_for_depth n = replicate_string (n + 1)
@@ -732,8 +799,6 @@
val relabel_proof =
let
fun aux _ _ _ [] = []
- | aux subst depth nextp ((ps as Fix _) :: proof) =
- ps :: aux subst depth nextp proof
| aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
if l = no_label then
Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
@@ -751,7 +816,7 @@
let
val l' = (prefix_for_depth depth fact_prefix, next_fact)
in (l', (l, l') :: subst, next_fact + 1) end
- val relabel_facts = apfst (map (the o AList.lookup (op =) subst))
+ val relabel_facts = apfst (map_filter (AList.lookup (op =) subst))
val by =
case by of
Facts facts => Facts (relabel_facts facts)
@@ -762,6 +827,7 @@
Have (qs, l', t, by) ::
aux subst depth (next_assum, next_fact) proof
end
+ | aux subst depth nextp (ps :: proof) = ps :: aux subst depth nextp proof
in aux [] 0 (1, 1) end
fun string_for_proof ctxt sorts i n =
@@ -785,12 +851,13 @@
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
fun do_using [] = ""
| do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " "
- fun do_by_facts [] [] = "by blast"
- | do_by_facts _ [] = "by metis"
- | do_by_facts _ ss = "by (metis " ^ space_implode " " ss ^ ")"
- fun do_facts (ls, ss) = do_using ls ^ do_by_facts ls ss
+ fun do_by_facts [] = "by metis"
+ | do_by_facts ss = "by (metis " ^ space_implode " " ss ^ ")"
+ fun do_facts (ls, ss) = do_using ls ^ do_by_facts ss
and do_step ind (Fix xs) =
do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
+ | do_step ind (Let (t1, t2)) =
+ do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
| do_step ind (Assume (l, t)) =
do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
| do_step ind (Have (qs, l, t, Facts facts)) =