# HG changeset patch # User blanchet # Date 1272451610 -7200 # Node ID c2d7e2dff59e6f7a9fa22abf6ea09d0d7bd69891 # Parent 56ce8fc56be3864a0586e504a841736aa88b955e support Vampire definitions of constants as "let" constructs in Isar proofs diff -r 56ce8fc56be3 -r c2d7e2dff59e src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- 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(, , ). - The could be an identifier, but we assume integers. *) -fun retuple_tstp_line ((name, ts), deps) = (name, ts, deps) +(* Syntax: cnf(, , ). + The 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: [0:] || +(* Syntax: [0:] || -> . *) -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)) = diff -r 56ce8fc56be3 -r c2d7e2dff59e src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Apr 27 18:58:05 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Apr 28 12:46:50 2010 +0200 @@ -14,6 +14,7 @@ val timestamp : unit -> string val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option + val nat_subscript : int -> string val unyxml : string -> string val maybe_quote : string -> string end; @@ -74,6 +75,9 @@ SOME (Time.fromMilliseconds msecs) end +val subscript = implode o map (prefix "\<^isub>") o explode +val nat_subscript = subscript o string_of_int + fun plain_string_from_xml_tree t = Buffer.empty |> XML.add_content t |> Buffer.content val unyxml = plain_string_from_xml_tree o YXML.parse