--- a/src/HOL/IsaMakefile Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/IsaMakefile Fri Mar 19 13:02:18 2010 +0100
@@ -314,6 +314,7 @@
Tools/Quotient/quotient_term.ML \
Tools/Quotient/quotient_typ.ML \
Tools/recdef.ML \
+ Tools/Sledgehammer/meson_tactic.ML \
Tools/Sledgehammer/metis_tactics.ML \
Tools/Sledgehammer/sledgehammer_fact_filter.ML \
Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \
--- a/src/HOL/Sledgehammer.thy Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/Sledgehammer.thy Fri Mar 19 13:02:18 2010 +0100
@@ -1,7 +1,8 @@
(* Title: HOL/Sledgehammer.thy
Author: Lawrence C Paulson
Author: Jia Meng, NICTA
- Author: Fabian Immler, TUM
+ Author: Fabian Immler, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
*)
header {* Sledgehammer: Isabelle--ATP Linkup *}
@@ -10,7 +11,8 @@
imports Plain Hilbert_Choice
uses
"Tools/polyhash.ML"
- "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
+ "~~/src/Tools/Metis/metis.ML"
+ ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
@@ -18,79 +20,79 @@
("Tools/ATP_Manager/atp_manager.ML")
("Tools/ATP_Manager/atp_wrapper.ML")
("Tools/ATP_Manager/atp_minimal.ML")
- "~~/src/Tools/Metis/metis.ML"
+ ("Tools/Sledgehammer/meson_tactic.ML")
("Tools/Sledgehammer/metis_tactics.ML")
begin
-definition COMBI :: "'a => 'a"
- where "COMBI P == P"
+definition COMBI :: "'a \<Rightarrow> 'a"
+ where "COMBI P \<equiv> P"
-definition COMBK :: "'a => 'b => 'a"
- where "COMBK P Q == P"
+definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
+ where "COMBK P Q \<equiv> P"
-definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
- where "COMBB P Q R == P (Q R)"
+definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
+ where "COMBB P Q R \<equiv> P (Q R)"
-definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
- where "COMBC P Q R == P R Q"
+definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
+ where "COMBC P Q R \<equiv> P R Q"
-definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
- where "COMBS P Q R == P R (Q R)"
+definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
+ where "COMBS P Q R \<equiv> P R (Q R)"
-definition fequal :: "'a => 'a => bool"
- where "fequal X Y == (X=Y)"
+definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ where "fequal X Y \<equiv> (X = Y)"
-lemma fequal_imp_equal: "fequal X Y ==> X=Y"
+lemma fequal_imp_equal: "fequal X Y \<Longrightarrow> X = Y"
by (simp add: fequal_def)
-lemma equal_imp_fequal: "X=Y ==> fequal X Y"
+lemma equal_imp_fequal: "X = Y \<Longrightarrow> fequal X Y"
by (simp add: fequal_def)
text{*These two represent the equivalence between Boolean equality and iff.
They can't be converted to clauses automatically, as the iff would be
expanded...*}
-lemma iff_positive: "P | Q | P=Q"
+lemma iff_positive: "P \<or> Q \<or> P = Q"
by blast
-lemma iff_negative: "~P | ~Q | P=Q"
+lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
by blast
text{*Theorems for translation to combinators*}
-lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
+lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBS_def)
done
-lemma abs_I: "(%x. x) == COMBI"
+lemma abs_I: "\<lambda>x. x \<equiv> COMBI"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBI_def)
done
-lemma abs_K: "(%x. y) == COMBK y"
+lemma abs_K: "\<lambda>x. y \<equiv> COMBK y"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBK_def)
done
-lemma abs_B: "(%x. a (g x)) == COMBB a g"
+lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBB_def)
done
-lemma abs_C: "(%x. (f x) b) == COMBC f b"
+lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBC_def)
done
-
subsection {* Setup of external ATPs *}
+use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
setup Sledgehammer_Fact_Preprocessor.setup
use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
@@ -119,7 +121,12 @@
setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
-
+
+
+subsection {* The MESON prover *}
+
+use "Tools/Sledgehammer/meson_tactic.ML"
+setup Meson_Tactic.setup
subsection {* The Metis prover *}
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 13:02:18 2010 +0100
@@ -20,7 +20,7 @@
val sledgehammer: string list -> Proof.state -> unit
end;
-structure ATP_Manager: ATP_MANAGER =
+structure ATP_Manager : ATP_MANAGER =
struct
(** preferences **)
@@ -263,7 +263,7 @@
val _ = register birth_time death_time (Thread.self (), desc);
val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
val message = #message (prover (! timeout) problem)
- handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => (* FIXME !? *)
+ handle Sledgehammer_HOL_Clause.TRIVIAL => (* FIXME !? *)
"Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
| ERROR msg => ("Error: " ^ msg);
val _ = unregister message (Thread.self ());
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 13:02:18 2010 +0100
@@ -14,7 +14,7 @@
(string * thm list) list -> ((string * thm list) list * int) option * string
end
-structure ATP_Minimal: ATP_MINIMAL =
+structure ATP_Minimal : ATP_MINIMAL =
struct
(* Linear minimization *)
@@ -170,7 +170,7 @@
(NONE, "Error in prover: " ^ msg)
| (Failure, _) =>
(NONE, "Failure: No proof with the theorems supplied"))
- handle Sledgehammer_HOL_Clause.TOO_TRIVIAL =>
+ handle Sledgehammer_HOL_Clause.TRIVIAL =>
(SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg => (NONE, "Error: " ^ msg)
end
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 13:02:18 2010 +0100
@@ -16,6 +16,7 @@
type prover_config =
{command: Path.T,
arguments: int -> string,
+ failure_strs: string list,
max_new_clauses: int,
insert_theory_const: bool,
emit_structured_proof: bool}
@@ -49,11 +50,12 @@
val refresh_systems: unit -> unit
end;
-structure ATP_Wrapper: ATP_WRAPPER =
+structure ATP_Wrapper : ATP_WRAPPER =
struct
-structure SFF = Sledgehammer_Fact_Filter
-structure SPR = Sledgehammer_Proof_Reconstruct
+open Sledgehammer_HOL_Clause
+open Sledgehammer_Fact_Filter
+open Sledgehammer_Proof_Reconstruct
(** generic ATP wrapper **)
@@ -76,6 +78,7 @@
type prover_config =
{command: Path.T,
arguments: int -> string,
+ failure_strs: string list,
max_new_clauses: int,
insert_theory_const: bool,
emit_structured_proof: bool};
@@ -114,13 +117,20 @@
|> Exn.release
|> tap (after path);
-fun external_prover relevance_filter prepare write cmd args produce_answer name
- ({with_full_types, subgoal, goal, axiom_clauses, filtered_clauses}: problem) =
+fun find_failure strs proof =
+ case filter (fn s => String.isSubstring s proof) strs of
+ [] => if is_proof_well_formed proof then NONE
+ else SOME "Ill-formed ATP output"
+ | (failure :: _) => SOME failure
+
+fun external_prover relevance_filter prepare write cmd args failure_strs
+ produce_answer name ({with_full_types, subgoal, goal, axiom_clauses,
+ filtered_clauses}: problem) =
let
(* get clauses and prepare them for writing *)
val (ctxt, (chain_ths, th)) = goal;
val thy = ProofContext.theory_of ctxt;
- val chain_ths = map (Thm.put_name_hint SPR.chained_hint) chain_ths;
+ val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal);
val the_filtered_clauses =
(case filtered_clauses of
@@ -184,7 +194,7 @@
with_path cleanup export run_on (prob_pathname subgoal);
(* check for success and print out some information on failure *)
- val failure = SPR.find_failure proof;
+ val failure = find_failure failure_strs proof;
val success = rc = 0 andalso is_none failure;
val (message, real_thm_names) =
if is_some failure then ("External prover failed.", [])
@@ -200,25 +210,16 @@
(* generic TPTP-based provers *)
-fun gen_tptp_prover (name, prover_config) timeout problem =
- let
- val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} =
- prover_config;
- in
- external_prover
- (SFF.get_relevant max_new_clauses insert_theory_const)
- (SFF.prepare_clauses false)
- Sledgehammer_HOL_Clause.tptp_write_file
- command
- (arguments timeout)
- (if emit_structured_proof then SPR.structured_proof
- else SPR.lemma_list false)
- name
- problem
- end;
+fun generic_tptp_prover
+ (name, {command, arguments, failure_strs, max_new_clauses,
+ insert_theory_const, emit_structured_proof}) timeout =
+ external_prover (get_relevant_facts max_new_clauses insert_theory_const)
+ (prepare_clauses false) write_tptp_file command (arguments timeout)
+ failure_strs
+ (if emit_structured_proof then structured_isar_proof
+ else metis_lemma_list false) name;
-fun tptp_prover (name, config) = (name, gen_tptp_prover (name, config));
-
+fun tptp_prover (name, p) = (name, generic_tptp_prover (name, p));
(** common provers **)
@@ -227,6 +228,8 @@
(*NB: Vampire does not work without explicit timelimit*)
+val vampire_failure_strs =
+ ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
val vampire_max_new_clauses = 60;
val vampire_insert_theory_const = false;
@@ -234,6 +237,7 @@
{command = Path.explode "$VAMPIRE_HOME/vampire",
arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
" -t " ^ string_of_int timeout),
+ failure_strs = vampire_failure_strs,
max_new_clauses = vampire_max_new_clauses,
insert_theory_const = vampire_insert_theory_const,
emit_structured_proof = full};
@@ -244,6 +248,10 @@
(* E prover *)
+val eprover_failure_strs =
+ ["SZS status: Satisfiable", "SZS status Satisfiable",
+ "SZS status: ResourceOut", "SZS status ResourceOut",
+ "# Cannot determine problem status"];
val eprover_max_new_clauses = 100;
val eprover_insert_theory_const = false;
@@ -251,6 +259,7 @@
{command = Path.explode "$E_HOME/eproof",
arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
" --silent --cpu-limit=" ^ string_of_int timeout),
+ failure_strs = eprover_failure_strs,
max_new_clauses = eprover_max_new_clauses,
insert_theory_const = eprover_insert_theory_const,
emit_structured_proof = full};
@@ -261,6 +270,9 @@
(* SPASS *)
+val spass_failure_strs =
+ ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
+ "SPASS beiseite: Maximal number of loops exceeded."];
val spass_max_new_clauses = 40;
val spass_insert_theory_const = true;
@@ -268,26 +280,25 @@
{command = Path.explode "$SPASS_HOME/SPASS",
arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
" -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout),
+ failure_strs = spass_failure_strs,
max_new_clauses = spass_max_new_clauses,
insert_theory_const = insert_theory_const,
emit_structured_proof = false};
-fun gen_dfg_prover (name, prover_config: prover_config) timeout problem =
- let
- val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config;
- in
- external_prover
- (SFF.get_relevant max_new_clauses insert_theory_const)
- (SFF.prepare_clauses true)
- Sledgehammer_HOL_Clause.dfg_write_file
- command
- (arguments timeout)
- (SPR.lemma_list true)
- name
- problem
- end;
+fun generic_dfg_prover
+ (name, ({command, arguments, failure_strs, max_new_clauses,
+ insert_theory_const, ...} : prover_config)) timeout =
+ external_prover
+ (get_relevant_facts max_new_clauses insert_theory_const)
+ (prepare_clauses true)
+ write_dfg_file
+ command
+ (arguments timeout)
+ failure_strs
+ (metis_lemma_list true)
+ name;
-fun dfg_prover (name, config) = (name, gen_dfg_prover (name, config));
+fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
val spass = dfg_prover ("spass", spass_config spass_insert_theory_const);
val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false);
@@ -316,10 +327,13 @@
NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP")
| SOME sys => sys);
+val remote_failure_strs = ["Remote-script could not extract proof"];
+
fun remote_prover_config prover_prefix args max_new insert_tc: prover_config =
{command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
- arguments =
- (fn timeout => args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
+ arguments = (fn timeout =>
+ args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
+ failure_strs = remote_failure_strs,
max_new_clauses = max_new,
insert_theory_const = insert_tc,
emit_structured_proof = false};
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Fri Mar 19 13:02:18 2010 +0100
@@ -0,0 +1,53 @@
+(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory
+
+MESON general tactic and proof method.
+*)
+
+signature MESON_TACTIC =
+sig
+ val expand_defs_tac : thm -> tactic
+ val meson_general_tac : Proof.context -> thm list -> int -> tactic
+ val setup: theory -> theory
+end;
+
+structure Meson_Tactic : MESON_TACTIC =
+struct
+
+open Sledgehammer_Fact_Preprocessor
+
+(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
+fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ u) =
+ String.isPrefix skolem_prefix a
+ | is_absko _ = false;
+
+fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ u) = (*Definition of Free, not in certain terms*)
+ is_Free t andalso not (member (op aconv) xs t)
+ | is_okdef _ _ = false
+
+(*This function tries to cope with open locales, which introduce hypotheses of the form
+ Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
+ of sko_ functions. *)
+fun expand_defs_tac st0 st =
+ let val hyps0 = #hyps (rep_thm st0)
+ val hyps = #hyps (crep_thm st)
+ val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
+ val defs = filter (is_absko o Thm.term_of) newhyps
+ val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
+ (map Thm.term_of hyps)
+ val fixed = OldTerm.term_frees (concl_of st) @
+ fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
+ in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
+
+fun meson_general_tac ctxt ths i st0 =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val ctxt0 = Classical.put_claset HOL_cs ctxt
+ in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
+
+val setup =
+ Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
+ SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
+ "MESON resolution proof procedure";
+
+end;
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Mar 19 13:02:18 2010 +0100
@@ -18,9 +18,11 @@
structure Metis_Tactics : METIS_TACTICS =
struct
-structure SFC = Sledgehammer_FOL_Clause
-structure SHC = Sledgehammer_HOL_Clause
-structure SPR = Sledgehammer_Proof_Reconstruct
+open Sledgehammer_FOL_Clause
+open Sledgehammer_Fact_Preprocessor
+open Sledgehammer_HOL_Clause
+open Sledgehammer_Proof_Reconstruct
+open Sledgehammer_Fact_Filter
val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();
@@ -67,62 +69,62 @@
fun metis_lit b c args = (b, (c, args));
-fun hol_type_to_fol (SFC.AtomV x) = Metis.Term.Var x
- | hol_type_to_fol (SFC.AtomF x) = Metis.Term.Fn(x,[])
- | hol_type_to_fol (SFC.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
+fun hol_type_to_fol (AtomV x) = Metis.Term.Var x
+ | hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, [])
+ | hol_type_to_fol (Comp (tc, tps)) =
+ Metis.Term.Fn (tc, map hol_type_to_fol tps);
(*These two functions insert type literals before the real literals. That is the
opposite order from TPTP linkup, but maybe OK.*)
fun hol_term_to_fol_FO tm =
- case SHC.strip_comb tm of
- (SHC.CombConst(c,_,tys), tms) =>
+ case strip_combterm_comb tm of
+ (CombConst(c,_,tys), tms) =>
let val tyargs = map hol_type_to_fol tys
val args = map hol_term_to_fol_FO tms
in Metis.Term.Fn (c, tyargs @ args) end
- | (SHC.CombVar(v,_), []) => Metis.Term.Var v
+ | (CombVar(v,_), []) => Metis.Term.Var v
| _ => error "hol_term_to_fol_FO";
-fun hol_term_to_fol_HO (SHC.CombVar (a, _)) = Metis.Term.Var a
- | hol_term_to_fol_HO (SHC.CombConst (a, _, tylist)) =
+fun hol_term_to_fol_HO (CombVar (a, _)) = Metis.Term.Var a
+ | hol_term_to_fol_HO (CombConst (a, _, tylist)) =
Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
- | hol_term_to_fol_HO (SHC.CombApp (tm1, tm2)) =
+ | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
(*The fully-typed translation, to avoid type errors*)
fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
-fun hol_term_to_fol_FT (SHC.CombVar(a, ty)) =
- wrap_type (Metis.Term.Var a, ty)
- | hol_term_to_fol_FT (SHC.CombConst(a, ty, _)) =
+fun hol_term_to_fol_FT (CombVar(a, ty)) = wrap_type (Metis.Term.Var a, ty)
+ | hol_term_to_fol_FT (CombConst(a, ty, _)) =
wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
- | hol_term_to_fol_FT (tm as SHC.CombApp(tm1,tm2)) =
+ | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
- SHC.type_of_combterm tm);
+ type_of_combterm tm);
-fun hol_literal_to_fol FO (SHC.Literal (pol, tm)) =
- let val (SHC.CombConst(p,_,tys), tms) = SHC.strip_comb tm
+fun hol_literal_to_fol FO (Literal (pol, tm)) =
+ let val (CombConst(p,_,tys), tms) = strip_combterm_comb tm
val tylits = if p = "equal" then [] else map hol_type_to_fol tys
val lits = map hol_term_to_fol_FO tms
in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
- | hol_literal_to_fol HO (SHC.Literal (pol, tm)) =
- (case SHC.strip_comb tm of
- (SHC.CombConst("equal",_,_), tms) =>
+ | hol_literal_to_fol HO (Literal (pol, tm)) =
+ (case strip_combterm_comb tm of
+ (CombConst("equal",_,_), tms) =>
metis_lit pol "=" (map hol_term_to_fol_HO tms)
| _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
- | hol_literal_to_fol FT (SHC.Literal (pol, tm)) =
- (case SHC.strip_comb tm of
- (SHC.CombConst("equal",_,_), tms) =>
+ | hol_literal_to_fol FT (Literal (pol, tm)) =
+ (case strip_combterm_comb tm of
+ (CombConst("equal",_,_), tms) =>
metis_lit pol "=" (map hol_term_to_fol_FT tms)
| _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
fun literals_of_hol_thm thy mode t =
- let val (lits, types_sorts) = SHC.literals_of_term thy t
+ let val (lits, types_sorts) = literals_of_term thy t
in (map (hol_literal_to_fol mode) lits, types_sorts) end;
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
-fun metis_of_typeLit pos (SFC.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
- | metis_of_typeLit pos (SFC.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
+fun metis_of_typeLit pos (LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
+ | metis_of_typeLit pos (LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
fun default_sort _ (TVar _) = false
| default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
@@ -136,10 +138,9 @@
(literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
in
if is_conjecture then
- (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), SFC.add_typs types_sorts)
+ (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), add_typs types_sorts)
else
- let val tylits = SFC.add_typs
- (filter (not o default_sort ctxt) types_sorts)
+ let val tylits = add_typs (filter (not o default_sort ctxt) types_sorts)
val mtylits = if Config.get ctxt type_lits
then map (metis_of_typeLit false) tylits else []
in
@@ -149,13 +150,13 @@
(* ARITY CLAUSE *)
-fun m_arity_cls (SFC.TConsLit (c,t,args)) =
- metis_lit true (SFC.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
- | m_arity_cls (SFC.TVarLit (c,str)) =
- metis_lit false (SFC.make_type_class c) [Metis.Term.Var str];
+fun m_arity_cls (TConsLit (c,t,args)) =
+ metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
+ | m_arity_cls (TVarLit (c,str)) =
+ metis_lit false (make_type_class c) [Metis.Term.Var str];
(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
-fun arity_cls (SFC.ArityClause{conclLit,premLits,...}) =
+fun arity_cls (ArityClause {conclLit, premLits, ...}) =
(TrueI,
Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
@@ -164,7 +165,7 @@
fun m_classrel_cls subclass superclass =
[metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
-fun classrel_cls (SFC.ClassrelClause {subclass, superclass, ...}) =
+fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
(TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
(* ------------------------------------------------------------------------- *)
@@ -213,14 +214,14 @@
| strip_happ args x = (x, args);
fun fol_type_to_isa _ (Metis.Term.Var v) =
- (case SPR.strip_prefix SFC.tvar_prefix v of
- SOME w => SPR.make_tvar w
- | NONE => SPR.make_tvar v)
+ (case strip_prefix tvar_prefix v of
+ SOME w => make_tvar w
+ | NONE => make_tvar v)
| fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
- (case SPR.strip_prefix SFC.tconst_prefix x of
- SOME tc => Term.Type (SPR.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
+ (case strip_prefix tconst_prefix x of
+ SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
| NONE =>
- case SPR.strip_prefix SFC.tfree_prefix x of
+ case strip_prefix tfree_prefix x of
SOME tf => mk_tfree ctxt tf
| NONE => error ("fol_type_to_isa: " ^ x));
@@ -229,10 +230,10 @@
let val thy = ProofContext.theory_of ctxt
val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
fun tm_to_tt (Metis.Term.Var v) =
- (case SPR.strip_prefix SFC.tvar_prefix v of
- SOME w => Type (SPR.make_tvar w)
+ (case strip_prefix tvar_prefix v of
+ SOME w => Type (make_tvar w)
| NONE =>
- case SPR.strip_prefix SFC.schematic_var_prefix v of
+ case strip_prefix schematic_var_prefix v of
SOME w => Term (mk_var (w, HOLogic.typeT))
| NONE => Term (mk_var (v, HOLogic.typeT)) )
(*Var from Metis with a name like _nnn; possibly a type variable*)
@@ -247,16 +248,16 @@
end
| tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
and applic_to_tt ("=",ts) =
- Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
+ Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
| applic_to_tt (a,ts) =
- case SPR.strip_prefix SFC.const_prefix a of
+ case strip_prefix const_prefix a of
SOME b =>
- let val c = SPR.invert_const b
- val ntypes = SPR.num_typargs thy c
+ let val c = invert_const b
+ val ntypes = num_typargs thy c
val nterms = length ts - ntypes
val tts = map tm_to_tt ts
val tys = types_of (List.take(tts,ntypes))
- val ntyargs = SPR.num_typargs thy c
+ val ntyargs = num_typargs thy c
in if length tys = ntyargs then
apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
@@ -267,14 +268,14 @@
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
end
| NONE => (*Not a constant. Is it a type constructor?*)
- case SPR.strip_prefix SFC.tconst_prefix a of
+ case strip_prefix tconst_prefix a of
SOME b =>
- Type (Term.Type (SPR.invert_type_const b, types_of (map tm_to_tt ts)))
+ Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
- case SPR.strip_prefix SFC.tfree_prefix a of
+ case strip_prefix tfree_prefix a of
SOME b => Type (mk_tfree ctxt b)
| NONE => (*a fixed variable? They are Skolem functions.*)
- case SPR.strip_prefix SFC.fixed_var_prefix a of
+ case strip_prefix fixed_var_prefix a of
SOME b =>
let val opr = Term.Free(b, HOLogic.typeT)
in apply_list opr (length ts) (map tm_to_tt ts) end
@@ -285,16 +286,16 @@
fun fol_term_to_hol_FT ctxt fol_tm =
let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
- (case SPR.strip_prefix SFC.schematic_var_prefix v of
+ (case strip_prefix schematic_var_prefix v of
SOME w => mk_var(w, dummyT)
| NONE => mk_var(v, dummyT))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
Const ("op =", HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
- (case SPR.strip_prefix SFC.const_prefix x of
- SOME c => Const (SPR.invert_const c, dummyT)
+ (case strip_prefix const_prefix x of
+ SOME c => Const (invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case SPR.strip_prefix SFC.fixed_var_prefix x of
+ case strip_prefix fixed_var_prefix x of
SOME v => Free (v, fol_type_to_isa ctxt ty)
| NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
@@ -303,12 +304,12 @@
cvt tm1 $ cvt tm2
| cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
| cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
- list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
+ list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
| cvt (t as Metis.Term.Fn (x, [])) =
- (case SPR.strip_prefix SFC.const_prefix x of
- SOME c => Const (SPR.invert_const c, dummyT)
+ (case strip_prefix const_prefix x of
+ SOME c => Const (invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case SPR.strip_prefix SFC.fixed_var_prefix x of
+ case strip_prefix fixed_var_prefix x of
SOME v => Free (v, dummyT)
| NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
fol_term_to_hol_RAW ctxt t))
@@ -331,7 +332,7 @@
ts'
in ts' end;
-fun mk_not (Const ("Not", _) $ b) = b
+fun mk_not (Const (@{const_name Not}, _) $ b) = b
| mk_not b = HOLogic.mk_not b;
val metis_eq = Metis.Term.Fn ("=", []);
@@ -387,9 +388,9 @@
" in " ^ Display.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
- case SPR.strip_prefix SFC.schematic_var_prefix a of
+ case strip_prefix schematic_var_prefix a of
SOME b => SOME (b, t)
- | NONE => case SPR.strip_prefix SFC.tvar_prefix a of
+ | NONE => case strip_prefix tvar_prefix a of
SOME _ => NONE (*type instantiations are forbidden!*)
| NONE => SOME (a,t) (*internal Metis var?*)
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
@@ -455,8 +456,8 @@
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
-fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*)
- | get_ty_arg_size thy (Const (c, _)) = (SPR.num_typargs thy c handle TYPE _ => 0)
+fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0 (*equality has no type arguments*)
+ | get_ty_arg_size thy (Const (c, _)) = (num_typargs thy c handle TYPE _ => 0)
| get_ty_arg_size _ _ = 0;
(* INFERENCE RULE: EQUALITY *)
@@ -469,7 +470,7 @@
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
fun path_finder_FO tm [] = (tm, Term.Bound 0)
| path_finder_FO tm (p::ps) =
- let val (tm1,args) = Term.strip_comb tm
+ let val (tm1,args) = strip_comb tm
val adjustment = get_ty_arg_size thy tm1
val p' = if adjustment > p then p else p-adjustment
val tm_p = List.nth(args,p')
@@ -496,13 +497,13 @@
" isa-term: " ^ Syntax.string_of_term ctxt tm ^
" fol-term: " ^ Metis.Term.toString t)
fun path_finder FO tm ps _ = path_finder_FO tm ps
- | path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ =
+ | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
(*equality: not curried, as other predicates are*)
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
else path_finder_HO tm (p::ps) (*1 selects second operand*)
| path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
- | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps)
+ | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
(Metis.Term.Fn ("=", [t1,t2])) =
(*equality: not curried, as other predicates are*)
if p=0 then path_finder_FT tm (0::1::ps)
@@ -514,7 +515,7 @@
| path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
(*if not equality, ignore head to skip the hBOOL predicate*)
| path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
- fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
+ fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
in (tm, nt $ tm_rslt) end
| path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
@@ -542,7 +543,7 @@
| step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
equality_inf ctxt mode f_lit f_p f_r;
-fun real_literal (_, (c, _)) = not (String.isPrefix SFC.class_prefix c);
+fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
fun translate _ _ thpairs [] = thpairs
| translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
@@ -568,23 +569,14 @@
(* Translation of HO Clauses *)
(* ------------------------------------------------------------------------- *)
-fun cnf_th thy th = hd (Sledgehammer_Fact_Preprocessor.cnf_axiom thy th);
-
-val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
-val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
-
-val comb_I = cnf_th @{theory} SHC.comb_I;
-val comb_K = cnf_th @{theory} SHC.comb_K;
-val comb_B = cnf_th @{theory} SHC.comb_B;
-val comb_C = cnf_th @{theory} SHC.comb_C;
-val comb_S = cnf_th @{theory} SHC.comb_S;
+fun cnf_th thy th = hd (cnf_axiom thy th);
fun type_ext thy tms =
- let val subs = Sledgehammer_Fact_Filter.tfree_classes_of_terms tms
- val supers = Sledgehammer_Fact_Filter.tvar_classes_of_terms tms
- and tycons = Sledgehammer_Fact_Filter.type_consts_of_terms thy tms
- val (supers', arity_clauses) = SFC.make_arity_clauses thy tycons supers
- val classrel_clauses = SFC.make_classrel_clauses thy subs supers'
+ let val subs = tfree_classes_of_terms tms
+ val supers = tvar_classes_of_terms tms
+ and tycons = type_consts_of_terms thy tms
+ val (supers', arity_clauses) = make_arity_clauses thy tycons supers
+ val classrel_clauses = make_classrel_clauses thy subs supers'
in map classrel_cls classrel_clauses @ map arity_cls arity_clauses
end;
@@ -593,8 +585,8 @@
(* ------------------------------------------------------------------------- *)
type logic_map =
- {axioms : (Metis.Thm.thm * thm) list,
- tfrees : SFC.type_literal list};
+ {axioms: (Metis.Thm.thm * thm) list,
+ tfrees: type_literal list};
fun const_in_metis c (pred, tm_list) =
let
@@ -606,7 +598,7 @@
(*Extract TFree constraints from context to include as conjecture clauses*)
fun init_tfrees ctxt =
let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
- in SFC.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
+ in add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
(*transform isabelle type / arity clause to metis clause *)
fun add_type_thm [] lmap = lmap
@@ -643,12 +635,12 @@
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
(*Now check for the existence of certain combinators*)
- val thI = if used "c_COMBI" then [comb_I] else []
- val thK = if used "c_COMBK" then [comb_K] else []
- val thB = if used "c_COMBB" then [comb_B] else []
- val thC = if used "c_COMBC" then [comb_C] else []
- val thS = if used "c_COMBS" then [comb_S] else []
- val thEQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
+ val thI = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else []
+ val thK = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else []
+ val thB = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else []
+ val thC = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
+ val thS = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
+ val thEQ = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
val lmap' = if mode=FO then lmap
else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
in
@@ -668,7 +660,7 @@
fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
val th_cls_pairs =
- map (fn th => (Thm.get_name_hint th, Sledgehammer_Fact_Preprocessor.cnf_axiom thy th)) ths0
+ map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
val ths = maps #2 th_cls_pairs
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
@@ -677,7 +669,7 @@
val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (trace_msg (fn () => "TFREE CLAUSES");
- app (fn tf => trace_msg (fn _ => SFC.tptp_of_typeLit true tf)) tfrees)
+ app (fn tf => trace_msg (fn _ => tptp_of_typeLit true tf)) tfrees)
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
val thms = map #1 axioms
val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
@@ -719,12 +711,12 @@
let val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
- if exists_type Sledgehammer_Fact_Preprocessor.type_has_topsort (prop_of st0)
+ if exists_type type_has_topsort (prop_of st0)
then raise METIS "Metis: Proof state contains the universal sort {}"
else
- (Meson.MESON Sledgehammer_Fact_Preprocessor.neg_clausify
+ (Meson.MESON neg_clausify
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
- THEN Sledgehammer_Fact_Preprocessor.expand_defs_tac st0) st0
+ THEN Meson_Tactic.expand_defs_tac st0) st0
end
handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
@@ -737,11 +729,11 @@
val setup =
type_lits_setup #>
- method @{binding metis} HO "METIS for FOL & HOL problems" #>
+ method @{binding metis} HO "METIS for FOL and HOL problems" #>
method @{binding metisF} FO "METIS for FOL problems" #>
method @{binding metisFT} FT "METIS with fully-typed translation" #>
Method.setup @{binding finish_clausify}
- (Scan.succeed (K (SIMPLE_METHOD (Sledgehammer_Fact_Preprocessor.expand_defs_tac refl))))
+ (Scan.succeed (K (SIMPLE_METHOD (Meson_Tactic.expand_defs_tac refl))))
"cleanup after conversion to clauses";
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Mar 19 13:02:18 2010 +0100
@@ -4,47 +4,45 @@
signature SLEDGEHAMMER_FACT_FILTER =
sig
- type classrelClause = Sledgehammer_FOL_Clause.classrelClause
- type arityClause = Sledgehammer_FOL_Clause.arityClause
+ type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
+ type arity_clause = Sledgehammer_FOL_Clause.arity_clause
type axiom_name = Sledgehammer_HOL_Clause.axiom_name
- type clause = Sledgehammer_HOL_Clause.clause
- type clause_id = Sledgehammer_HOL_Clause.clause_id
- datatype mode = Auto | Fol | Hol
+ type hol_clause = Sledgehammer_HOL_Clause.hol_clause
+ type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
val tvar_classes_of_terms : term list -> string list
val tfree_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
- val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
+ val get_relevant_facts : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
(thm * (string * int)) list
val prepare_clauses : bool -> thm list -> thm list ->
- (thm * (axiom_name * clause_id)) list ->
- (thm * (axiom_name * clause_id)) list -> theory ->
+ (thm * (axiom_name * hol_clause_id)) list ->
+ (thm * (axiom_name * hol_clause_id)) list -> theory ->
axiom_name vector *
- (clause list * clause list * clause list *
- clause list * classrelClause list * arityClause list)
+ (hol_clause list * hol_clause list * hol_clause list *
+ hol_clause list * classrel_clause list * arity_clause list)
end;
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
struct
-structure SFC = Sledgehammer_FOL_Clause
-structure SFP = Sledgehammer_Fact_Preprocessor
-structure SHC = Sledgehammer_HOL_Clause
+open Sledgehammer_FOL_Clause
+open Sledgehammer_Fact_Preprocessor
+open Sledgehammer_HOL_Clause
-type classrelClause = SFC.classrelClause
-type arityClause = SFC.arityClause
-type axiom_name = SHC.axiom_name
-type clause = SHC.clause
-type clause_id = SHC.clause_id
+type axiom_name = axiom_name
+type hol_clause = hol_clause
+type hol_clause_id = hol_clause_id
(********************************************************************)
(* some settings for both background automatic ATP calling procedure*)
(* and also explicit ATP invocation methods *)
(********************************************************************)
-(*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
+(* Translation mode can be auto-detected, or forced to be first-order or
+ higher-order *)
datatype mode = Auto | Fol | Hol;
-val linkup_logic_mode = Auto;
+val translation_mode = Auto;
(*** background linkup ***)
val run_blacklist_filter = true;
@@ -59,7 +57,7 @@
(* Relevance Filtering *)
(***************************************************************)
-fun strip_Trueprop (Const("Trueprop",_) $ t) = t
+fun strip_Trueprop (@{const Trueprop} $ t) = t
| strip_Trueprop t = t;
(*A surprising number of theorems contain only a few significant constants.
@@ -79,7 +77,10 @@
being chosen, but for some reason filtering works better with them listed. The
logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
must be within comprehensions.*)
-val standard_consts = ["Trueprop","==>","all","==","op |","Not","op ="];
+val standard_consts =
+ [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
+ @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
+ @{const_name "op ="}];
(*** constants with types ***)
@@ -233,7 +234,7 @@
end
handle ConstFree => false
in
- case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) =>
+ case tm of @{const Trueprop} $ (Const(@{const_name "op ="}, _) $ lhs $ rhs) =>
defs lhs rhs
| _ => false
end;
@@ -252,10 +253,10 @@
let val cls = sort compare_pairs newpairs
val accepted = List.take (cls, max_new)
in
- SFP.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
+ trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
", exceeds the limit of " ^ Int.toString (max_new)));
- SFP.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
- SFP.trace_msg (fn () => "Actually passed: " ^
+ trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
+ trace_msg (fn () => "Actually passed: " ^
space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
(map #1 accepted, map #1 (List.drop (cls, max_new)))
@@ -270,7 +271,7 @@
val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
val newp = p + (1.0-p) / convergence
in
- SFP.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
+ trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
(map #1 newrels) @
(relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
end
@@ -278,12 +279,12 @@
let val weight = clause_weight ctab rel_consts consts_typs
in
if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
- then (SFP.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
+ then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
" passes: " ^ Real.toString weight));
relevant ((ax,weight)::newrels, rejects) axs)
else relevant (newrels, ax::rejects) axs
end
- in SFP.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
+ in trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
relevant ([],[])
end;
@@ -292,12 +293,12 @@
then
let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
val goal_const_tab = get_goal_consts_typs thy goals
- val _ = SFP.trace_msg (fn () => ("Initial constants: " ^
+ val _ = trace_msg (fn () => ("Initial constants: " ^
space_implode ", " (Symtab.keys goal_const_tab)));
val rels = relevant_clauses max_new thy const_tab (pass_mark)
goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms)
in
- SFP.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
+ trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
rels
end
else axioms;
@@ -332,7 +333,7 @@
| hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
| hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
-fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
+fun hash_literal (@{const Not} $ P) = Word.notb(hashw_term(P,0w0))
| hash_literal P = hashw_term(P,0w0);
fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t))));
@@ -351,7 +352,7 @@
fun make_unique xs =
let val ht = mk_clause_table 7000
in
- SFP.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
+ trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
app (ignore o Polyhash.peekInsert ht) xs;
Polyhash.listItems ht
end;
@@ -383,7 +384,7 @@
val name1 = Facts.extern facts name;
val name2 = Name_Space.extern full_space name;
- val ths = filter_out SFP.bad_for_atp ths0;
+ val ths = filter_out bad_for_atp ths0;
in
if Facts.is_concealed facts name orelse null ths orelse
run_blacklist_filter andalso is_package_def name then I
@@ -403,7 +404,7 @@
(*Ignore blacklisted basenames*)
fun add_multi_names (a, ths) pairs =
- if (Long_Name.base_name a) mem_string SFP.multi_base_blacklist then pairs
+ if (Long_Name.base_name a) mem_string multi_base_blacklist then pairs
else add_single_names (a, ths) pairs;
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
@@ -412,12 +413,17 @@
fun name_thm_pairs ctxt =
let
val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
- val blacklist =
- if run_blacklist_filter then No_ATPs.get ctxt |> map Thm.prop_of else []
- fun is_blacklisted (_, th) = member (op =) blacklist (Thm.prop_of th)
+ val ps = [] |> fold add_multi_names mults
+ |> fold add_single_names singles
in
- filter_out is_blacklisted
- (fold add_single_names singles (fold add_multi_names mults []))
+ if run_blacklist_filter then
+ let
+ val blacklist = No_ATPs.get ctxt
+ |> map (`Thm.full_prop_of) |> Termtab.make
+ val is_blacklisted = Termtab.defined blacklist o Thm.full_prop_of o snd
+ in ps |> filter_out is_blacklisted end
+ else
+ ps
end;
fun check_named ("", th) =
@@ -426,7 +432,7 @@
fun get_all_lemmas ctxt =
let val included_thms =
- tap (fn ths => SFP.trace_msg
+ tap (fn ths => trace_msg
(fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
(name_thm_pairs ctxt)
in
@@ -440,7 +446,7 @@
fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts);
(*Remove this trivial type class*)
-fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
+fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
fun tvar_classes_of_terms ts =
let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
@@ -499,14 +505,10 @@
fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
| too_general_eqterms _ = false;
-fun too_general_equality (Const ("op =", _) $ x $ y) =
+fun too_general_equality (Const (@{const_name "op ="}, _) $ x $ y) =
too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
| too_general_equality _ = false;
-(* tautologous? *)
-fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
- | is_taut _ = false;
-
fun has_typed_var tycons = exists_subterm
(fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
@@ -514,28 +516,29 @@
they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
The resulting clause will have no type constraint, yielding false proofs. Even "bool"
leads to many unsound proofs, though (obviously) only for higher-order problems.*)
-val unwanted_types = ["Product_Type.unit","bool"];
+val unwanted_types = [@{type_name unit}, @{type_name bool}];
fun unwanted t =
- is_taut t orelse has_typed_var unwanted_types t orelse
+ t = @{prop True} orelse has_typed_var unwanted_types t orelse
forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
(*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
likely to lead to unsound proofs.*)
fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
-fun isFO thy goal_cls = case linkup_logic_mode of
- Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
- | Fol => true
- | Hol => false
+fun is_first_order thy goal_cls =
+ case translation_mode of
+ Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
+ | Fol => true
+ | Hol => false
-fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
+fun get_relevant_facts max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
let
val thy = ProofContext.theory_of ctxt
- val isFO = isFO thy goal_cls
+ val is_FO = is_first_order thy goal_cls
val included_cls = get_all_lemmas ctxt
- |> SFP.cnf_rules_pairs thy |> make_unique
- |> restrict_to_logic thy isFO
+ |> cnf_rules_pairs thy |> make_unique
+ |> restrict_to_logic thy is_FO
|> remove_unwanted_clauses
in
relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
@@ -547,28 +550,27 @@
let
(* add chain thms *)
val chain_cls =
- SFP.cnf_rules_pairs thy (filter check_named (map SFP.pairname chain_ths))
+ cnf_rules_pairs thy (filter check_named (map pairname chain_ths))
val axcls = chain_cls @ axcls
val extra_cls = chain_cls @ extra_cls
- val isFO = isFO thy goal_cls
+ val is_FO = is_first_order thy goal_cls
val ccls = subtract_cls goal_cls extra_cls
- val _ = app (fn th => SFP.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
+ val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
val ccltms = map prop_of ccls
and axtms = map (prop_of o #1) extra_cls
val subs = tfree_classes_of_terms ccltms
and supers = tvar_classes_of_terms axtms
- and tycons = type_consts_of_terms thy (ccltms@axtms)
+ and tycons = type_consts_of_terms thy (ccltms @ axtms)
(*TFrees in conjecture clauses; TVars in axiom clauses*)
- val conjectures = SHC.make_conjecture_clauses dfg thy ccls
- val (_, extra_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy extra_cls)
- val (clnames,axiom_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy axcls)
- val helper_clauses = SHC.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
- val (supers',arity_clauses) = SFC.make_arity_clauses_dfg dfg thy tycons supers
- val classrel_clauses = SFC.make_classrel_clauses thy subs supers'
+ val conjectures = make_conjecture_clauses dfg thy ccls
+ val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls)
+ val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls)
+ val helper_clauses = get_helper_clauses dfg thy is_FO (conjectures, extra_cls, [])
+ val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers
+ val classrel_clauses = make_classrel_clauses thy subs supers'
in
(Vector.fromList clnames,
(conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
end
end;
-
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Mar 19 13:02:18 2010 +0100
@@ -8,6 +8,7 @@
sig
val trace: bool Unsynchronized.ref
val trace_msg: (unit -> string) -> unit
+ val skolem_prefix: string
val cnf_axiom: theory -> thm -> thm list
val pairname: thm -> string * thm
val multi_base_blacklist: string list
@@ -15,7 +16,6 @@
val type_has_topsort: typ -> bool
val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
val neg_clausify: thm list -> thm list
- val expand_defs_tac: thm -> tactic
val combinators: thm -> thm
val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
val suppress_endtheory: bool Unsynchronized.ref
@@ -26,8 +26,12 @@
structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR =
struct
+open Sledgehammer_FOL_Clause
+
val trace = Unsynchronized.ref false;
-fun trace_msg msg = if ! trace then tracing (msg ()) else ();
+fun trace_msg msg = if !trace then tracing (msg ()) else ();
+
+val skolem_prefix = "sko_"
fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
@@ -75,7 +79,7 @@
fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
(*Existential: declare a Skolem function, then insert into body and continue*)
let
- val cname = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
+ val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
val args0 = OldTerm.term_frees xtp (*get the formal parameter list*)
val Ts = map type_of args0
val extraTs = rhs_extra_types (Ts ---> T) xtp
@@ -110,7 +114,7 @@
val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
val Ts = map type_of args
val cT = Ts ---> T
- val id = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
+ val id = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
val c = Free (id, cT)
val rhs = list_abs_free (map dest_Free args,
HOLogic.choice_const T $ xtp)
@@ -386,15 +390,14 @@
| cnf_rules_pairs_aux thy pairs ((name,th)::ths) =
let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs
handle THM _ => pairs |
- Sledgehammer_FOL_Clause.CLAUSE _ => pairs
+ CLAUSE _ => pairs
in cnf_rules_pairs_aux thy pairs' ths end;
(*The combination of rev and tail recursion preserves the original order*)
fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
-(**** Convert all facts of the theory into clauses
- (Sledgehammer_FOL_Clause.clause, or Sledgehammer_HOL_Clause.clause) ****)
+(**** Convert all facts of the theory into FOL or HOL clauses ****)
local
@@ -455,43 +458,6 @@
lambda_free, but then the individual theory caches become much bigger.*)
-(*** meson proof methods ***)
-
-(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
-fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a
- | is_absko _ = false;
-
-fun is_okdef xs (Const ("==", _) $ t $ u) = (*Definition of Free, not in certain terms*)
- is_Free t andalso not (member (op aconv) xs t)
- | is_okdef _ _ = false
-
-(*This function tries to cope with open locales, which introduce hypotheses of the form
- Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
- of sko_ functions. *)
-fun expand_defs_tac st0 st =
- let val hyps0 = #hyps (rep_thm st0)
- val hyps = #hyps (crep_thm st)
- val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
- val defs = filter (is_absko o Thm.term_of) newhyps
- val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
- (map Thm.term_of hyps)
- val fixed = OldTerm.term_frees (concl_of st) @
- fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
- in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
-
-
-fun meson_general_tac ctxt ths i st0 =
- let
- val thy = ProofContext.theory_of ctxt
- val ctxt0 = Classical.put_claset HOL_cs ctxt
- in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
-
-val meson_method_setup =
- Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
- SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
- "MESON resolution proof procedure";
-
-
(*** Converting a subgoal into negated conjecture clauses. ***)
fun neg_skolemize_tac ctxt =
@@ -534,11 +500,9 @@
"conversion of theorem to clauses";
-
(** setup **)
val setup =
- meson_method_setup #>
neg_clausify_setup #>
clausify_setup #>
perhaps saturate_skolem_cache #>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Mar 19 13:02:18 2010 +0100
@@ -44,19 +44,19 @@
datatype arLit =
TConsLit of class * string * string list
| TVarLit of class * string
- datatype arityClause = ArityClause of
+ datatype arity_clause = ArityClause of
{axiom_name: axiom_name, conclLit: arLit, premLits: arLit list}
- datatype classrelClause = ClassrelClause of
+ datatype classrel_clause = ClassrelClause of
{axiom_name: axiom_name, subclass: class, superclass: class}
- val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
- val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arityClause list
- val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
+ val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
+ val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list
+ val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table
- val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table
+ val add_classrel_clause_preds : classrel_clause * int Symtab.table -> int Symtab.table
val class_of_arityLit: arLit -> class
- val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table
+ val add_arity_clause_preds: arity_clause * int Symtab.table -> int Symtab.table
val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
- val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table
+ val add_arity_clause_funcs: arity_clause * int Symtab.table -> int Symtab.table
val init_functab: int Symtab.table
val dfg_sign: bool -> string -> string
val dfg_of_typeLit: bool -> type_literal -> string
@@ -67,14 +67,14 @@
val string_of_start: string -> string
val string_of_descrip : string -> string
val dfg_tfree_clause : string -> string
- val dfg_classrelClause: classrelClause -> string
- val dfg_arity_clause: arityClause -> string
+ val dfg_classrel_clause: classrel_clause -> string
+ val dfg_arity_clause: arity_clause -> string
val tptp_sign: bool -> string -> string
val tptp_of_typeLit : bool -> type_literal -> string
val gen_tptp_cls : int * string * kind * string list * string list -> string
val tptp_tfree_clause : string -> string
- val tptp_arity_clause : arityClause -> string
- val tptp_classrelClause : classrelClause -> string
+ val tptp_arity_clause : arity_clause -> string
+ val tptp_classrel_clause : classrel_clause -> string
end
structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
@@ -96,28 +96,23 @@
fun union_all xss = List.foldl (uncurry (union (op =))) [] xss;
-(*Provide readable names for the more common symbolic functions*)
+(* Provide readable names for the more common symbolic functions *)
val const_trans_table =
- Symtab.make [(@{const_name "op ="}, "equal"),
- (@{const_name Orderings.less_eq}, "lessequals"),
- (@{const_name "op &"}, "and"),
- (@{const_name "op |"}, "or"),
- (@{const_name "op -->"}, "implies"),
- (@{const_name "op :"}, "in"),
- ("Sledgehammer.fequal", "fequal"),
- ("Sledgehammer.COMBI", "COMBI"),
- ("Sledgehammer.COMBK", "COMBK"),
- ("Sledgehammer.COMBB", "COMBB"),
- ("Sledgehammer.COMBC", "COMBC"),
- ("Sledgehammer.COMBS", "COMBS"),
- ("Sledgehammer.COMBB'", "COMBB_e"),
- ("Sledgehammer.COMBC'", "COMBC_e"),
- ("Sledgehammer.COMBS'", "COMBS_e")];
+ Symtab.make [(@{const_name "op ="}, "equal"),
+ (@{const_name Orderings.less_eq}, "lessequals"),
+ (@{const_name "op &"}, "and"),
+ (@{const_name "op |"}, "or"),
+ (@{const_name "op -->"}, "implies"),
+ (@{const_name "op :"}, "in"),
+ (@{const_name fequal}, "fequal"),
+ (@{const_name COMBI}, "COMBI"),
+ (@{const_name COMBK}, "COMBK"),
+ (@{const_name COMBB}, "COMBB"),
+ (@{const_name COMBC}, "COMBC"),
+ (@{const_name COMBS}, "COMBS")];
val type_const_trans_table =
- Symtab.make [("*", "prod"),
- ("+", "sum"),
- ("~=>", "map")];
+ Symtab.make [("*", "prod"), ("+", "sum"), ("~=>", "map")];
(*Escaping of special characters.
Alphanumeric characters are left unchanged.
@@ -290,7 +285,7 @@
datatype arLit = TConsLit of class * string * string list
| TVarLit of class * string;
-datatype arityClause =
+datatype arity_clause =
ArityClause of {axiom_name: axiom_name,
conclLit: arLit,
premLits: arLit list};
@@ -316,7 +311,7 @@
(**** Isabelle class relations ****)
-datatype classrelClause =
+datatype classrel_clause =
ClassrelClause of {axiom_name: axiom_name,
subclass: class,
superclass: class};
@@ -330,13 +325,13 @@
fun add_supers (sub,pairs) = List.foldl (add_super sub) pairs supers
in List.foldl add_supers [] subs end;
-fun make_classrelClause (sub,super) =
+fun make_classrel_clause (sub,super) =
ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
subclass = make_type_class sub,
superclass = make_type_class super};
fun make_classrel_clauses thy subs supers =
- map make_classrelClause (class_pairs thy subs supers);
+ map make_classrel_clause (class_pairs thy subs supers);
(** Isabelle arities **)
@@ -391,13 +386,13 @@
fun add_type_sort_preds (T, preds) =
update_many (preds, map pred_of_sort (sorts_on_typs T));
-fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
+fun add_classrel_clause_preds (ClassrelClause {subclass,superclass,...}, preds) =
Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass
| class_of_arityLit (TVarLit (tclass, _)) = tclass;
-fun add_arityClause_preds (ArityClause {conclLit,premLits,...}, preds) =
+fun add_arity_clause_preds (ArityClause {conclLit,premLits,...}, preds) =
let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits)
fun upd (class,preds) = Symtab.update (class,1) preds
in List.foldl upd preds classes end;
@@ -414,7 +409,7 @@
| add_type_sort_funcs (TFree (a, _), funcs) =
Symtab.update (make_fixed_type_var a, 0) funcs
-fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) =
+fun add_arity_clause_funcs (ArityClause {conclLit,...}, funcs) =
let val TConsLit (_, tcons, tvars) = conclLit
in Symtab.update (tcons, length tvars) funcs end;
@@ -480,7 +475,7 @@
fun dfg_classrelLits sub sup = "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)";
-fun dfg_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
+fun dfg_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
"clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^
axiom_name ^ ").\n\n";
@@ -528,7 +523,7 @@
let val tvar = "(T)"
in tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end;
-fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
+fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
"cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n"
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Mar 19 13:02:18 2010 +0100
@@ -6,67 +6,54 @@
signature SLEDGEHAMMER_HOL_CLAUSE =
sig
- val ext: thm
- val comb_I: thm
- val comb_K: thm
- val comb_B: thm
- val comb_C: thm
- val comb_S: thm
- val minimize_applies: bool
+ type kind = Sledgehammer_FOL_Clause.kind
+ type fol_type = Sledgehammer_FOL_Clause.fol_type
+ type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
+ type arity_clause = Sledgehammer_FOL_Clause.arity_clause
type axiom_name = string
type polarity = bool
- type clause_id = int
+ type hol_clause_id = int
+
datatype combterm =
- CombConst of string * Sledgehammer_FOL_Clause.fol_type * Sledgehammer_FOL_Clause.fol_type list (*Const and Free*)
- | CombVar of string * Sledgehammer_FOL_Clause.fol_type
- | CombApp of combterm * combterm
+ CombConst of string * fol_type * fol_type list (* Const and Free *) |
+ CombVar of string * fol_type |
+ CombApp of combterm * combterm
datatype literal = Literal of polarity * combterm
- datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
- kind: Sledgehammer_FOL_Clause.kind,literals: literal list, ctypes_sorts: typ list}
- val type_of_combterm: combterm -> Sledgehammer_FOL_Clause.fol_type
- val strip_comb: combterm -> combterm * combterm list
- val literals_of_term: theory -> term -> literal list * typ list
- exception TOO_TRIVIAL
- val make_conjecture_clauses: bool -> theory -> thm list -> clause list
- val make_axiom_clauses: bool ->
- theory ->
- (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list
- val get_helper_clauses: bool ->
- theory ->
- bool ->
- clause list * (thm * (axiom_name * clause_id)) list * string list ->
- clause list
- val tptp_write_file: bool -> Path.T ->
- clause list * clause list * clause list * clause list *
- Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
+ datatype hol_clause =
+ HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
+ kind: kind, literals: literal list, ctypes_sorts: typ list}
+
+ val type_of_combterm : combterm -> fol_type
+ val strip_combterm_comb : combterm -> combterm * combterm list
+ val literals_of_term : theory -> term -> literal list * typ list
+ exception TRIVIAL
+ val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
+ val make_axiom_clauses : bool -> theory ->
+ (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
+ val get_helper_clauses : bool -> theory -> bool ->
+ hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
+ hol_clause list
+ val write_tptp_file : bool -> Path.T ->
+ hol_clause list * hol_clause list * hol_clause list * hol_clause list *
+ classrel_clause list * arity_clause list ->
int * int
- val dfg_write_file: bool -> Path.T ->
- clause list * clause list * clause list * clause list *
- Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
- int * int
+ val write_dfg_file : bool -> Path.T ->
+ hol_clause list * hol_clause list * hol_clause list * hol_clause list *
+ classrel_clause list * arity_clause list -> int * int
end
structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
struct
-structure SFC = Sledgehammer_FOL_Clause;
-
-(* theorems for combinators and function extensionality *)
-val ext = thm "HOL.ext";
-val comb_I = thm "Sledgehammer.COMBI_def";
-val comb_K = thm "Sledgehammer.COMBK_def";
-val comb_B = thm "Sledgehammer.COMBB_def";
-val comb_C = thm "Sledgehammer.COMBC_def";
-val comb_S = thm "Sledgehammer.COMBS_def";
-val fequal_imp_equal = thm "Sledgehammer.fequal_imp_equal";
-val equal_imp_fequal = thm "Sledgehammer.equal_imp_fequal";
-
+open Sledgehammer_FOL_Clause
+open Sledgehammer_Fact_Preprocessor
(* Parameter t_full below indicates that full type information is to be
exported *)
-(*If true, each function will be directly applied to as many arguments as possible, avoiding
- use of the "apply" operator. Use of hBOOL is also minimized.*)
+(* If true, each function will be directly applied to as many arguments as
+ possible, avoiding use of the "apply" operator. Use of hBOOL is also
+ minimized. *)
val minimize_applies = true;
fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
@@ -84,21 +71,18 @@
type axiom_name = string;
type polarity = bool;
-type clause_id = int;
+type hol_clause_id = int;
-datatype combterm = CombConst of string * SFC.fol_type * SFC.fol_type list (*Const and Free*)
- | CombVar of string * SFC.fol_type
- | CombApp of combterm * combterm
+datatype combterm =
+ CombConst of string * fol_type * fol_type list (* Const and Free *) |
+ CombVar of string * fol_type |
+ CombApp of combterm * combterm
datatype literal = Literal of polarity * combterm;
-datatype clause =
- Clause of {clause_id: clause_id,
- axiom_name: axiom_name,
- th: thm,
- kind: SFC.kind,
- literals: literal list,
- ctypes_sorts: typ list};
+datatype hol_clause =
+ HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
+ kind: kind, literals: literal list, ctypes_sorts: typ list};
(*********************************************************************)
@@ -106,8 +90,7 @@
(*********************************************************************)
fun isFalse (Literal(pol, CombConst(c,_,_))) =
- (pol andalso c = "c_False") orelse
- (not pol andalso c = "c_True")
+ (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
| isFalse _ = false;
fun isTrue (Literal (pol, CombConst(c,_,_))) =
@@ -115,24 +98,22 @@
(not pol andalso c = "c_False")
| isTrue _ = false;
-fun isTaut (Clause {literals,...}) = exists isTrue literals;
+fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
fun type_of dfg (Type (a, Ts)) =
let val (folTypes,ts) = types_of dfg Ts
- in (SFC.Comp(SFC.make_fixed_type_const dfg a, folTypes), ts) end
- | type_of _ (tp as TFree (a, _)) =
- (SFC.AtomF (SFC.make_fixed_type_var a), [tp])
- | type_of _ (tp as TVar (v, _)) =
- (SFC.AtomV (SFC.make_schematic_type_var v), [tp])
+ in (Comp(make_fixed_type_const dfg a, folTypes), ts) end
+ | type_of _ (tp as TFree (a, _)) = (AtomF (make_fixed_type_var a), [tp])
+ | type_of _ (tp as TVar (v, _)) = (AtomV (make_schematic_type_var v), [tp])
and types_of dfg Ts =
let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
- in (folTyps, SFC.union_all ts) end;
+ in (folTyps, union_all ts) end;
(* same as above, but no gathering of sort information *)
fun simp_type_of dfg (Type (a, Ts)) =
- SFC.Comp(SFC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
- | simp_type_of _ (TFree (a, _)) = SFC.AtomF(SFC.make_fixed_type_var a)
- | simp_type_of _ (TVar (v, _)) = SFC.AtomV(SFC.make_schematic_type_var v);
+ Comp(make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
+ | simp_type_of _ (TFree (a, _)) = AtomF (make_fixed_type_var a)
+ | simp_type_of _ (TVar (v, _)) = AtomV (make_schematic_type_var v);
fun const_type_of dfg thy (c,t) =
@@ -142,27 +123,27 @@
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
fun combterm_of dfg thy (Const(c,t)) =
let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
- val c' = CombConst(SFC.make_fixed_const dfg c, tp, tvar_list)
+ val c' = CombConst(make_fixed_const dfg c, tp, tvar_list)
in (c',ts) end
| combterm_of dfg _ (Free(v,t)) =
let val (tp,ts) = type_of dfg t
- val v' = CombConst(SFC.make_fixed_var v, tp, [])
+ val v' = CombConst(make_fixed_var v, tp, [])
in (v',ts) end
| combterm_of dfg _ (Var(v,t)) =
let val (tp,ts) = type_of dfg t
- val v' = CombVar(SFC.make_schematic_var v,tp)
+ val v' = CombVar(make_schematic_var v,tp)
in (v',ts) end
| combterm_of dfg thy (P $ Q) =
let val (P',tsP) = combterm_of dfg thy P
val (Q',tsQ) = combterm_of dfg thy Q
in (CombApp(P',Q'), union (op =) tsP tsQ) end
- | combterm_of _ _ (t as Abs _) = raise SFC.CLAUSE ("HOL CLAUSE", t);
+ | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t);
-fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
+fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
| predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
-fun literals_of_term1 dfg thy args (Const("Trueprop",_) $ P) = literals_of_term1 dfg thy args P
- | literals_of_term1 dfg thy args (Const("op |",_) $ P $ Q) =
+fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P
+ | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) =
literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
| literals_of_term1 dfg thy (lits,ts) P =
let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
@@ -173,23 +154,23 @@
fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
val literals_of_term = literals_of_term_dfg false;
-(* Problem too trivial for resolution (empty clause) *)
-exception TOO_TRIVIAL;
+(* Trivial problem, which resolution cannot handle (empty clause) *)
+exception TRIVIAL;
(* making axiom and conjecture clauses *)
-fun make_clause dfg thy (clause_id,axiom_name,kind,th) =
+fun make_clause dfg thy (clause_id, axiom_name, kind, th) =
let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
in
- if forall isFalse lits
- then raise TOO_TRIVIAL
+ if forall isFalse lits then
+ raise TRIVIAL
else
- Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
- literals = lits, ctypes_sorts = ctypes_sorts}
+ HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
+ kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}
end;
fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
- let val cls = make_clause dfg thy (id, name, SFC.Axiom, th)
+ let val cls = make_clause dfg thy (id, name, Axiom, th)
in
if isTaut cls then pairs else (name,cls)::pairs
end;
@@ -198,7 +179,7 @@
fun make_conjecture_clauses_aux _ _ _ [] = []
| make_conjecture_clauses_aux dfg thy n (th::ths) =
- make_clause dfg thy (n,"conjecture", SFC.Conjecture, th) ::
+ make_clause dfg thy (n,"conjecture", Conjecture, th) ::
make_conjecture_clauses_aux dfg thy (n+1) ths;
fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
@@ -211,7 +192,7 @@
(**********************************************************************)
(*Result of a function type; no need to check that the argument type matches.*)
-fun result_type (SFC.Comp ("tc_fun", [_, tp2])) = tp2
+fun result_type (Comp ("tc_fun", [_, tp2])) = tp2
| result_type _ = error "result_type"
fun type_of_combterm (CombConst (_, tp, _)) = tp
@@ -219,7 +200,7 @@
| type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
(*gets the head of a combinator application, along with the list of arguments*)
-fun strip_comb u =
+fun strip_combterm_comb u =
let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
| stripc x = x
in stripc(u,[]) end;
@@ -231,10 +212,10 @@
fun wrap_type t_full (s, tp) =
if t_full then
- type_wrapper ^ SFC.paren_pack [s, SFC.string_of_fol_type tp]
+ type_wrapper ^ paren_pack [s, string_of_fol_type tp]
else s;
-fun apply ss = "hAPP" ^ SFC.paren_pack ss;
+fun apply ss = "hAPP" ^ paren_pack ss;
fun rev_apply (v, []) = v
| rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
@@ -251,10 +232,9 @@
Int.toString nargs ^ " but is applied to " ^
space_implode ", " args)
val args2 = List.drop(args, nargs)
- val targs = if not t_full then map SFC.string_of_fol_type tvars
- else []
+ val targs = if not t_full then map string_of_fol_type tvars else []
in
- string_apply (c ^ SFC.paren_pack (args1@targs), args2)
+ string_apply (c ^ paren_pack (args1@targs), args2)
end
| string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
| string_of_applic _ _ _ = error "string_of_applic";
@@ -263,7 +243,7 @@
if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
fun string_of_combterm (params as (t_full, cma, cnh)) t =
- let val (head, args) = strip_comb t
+ let val (head, args) = strip_combterm_comb t
in wrap_type_if t_full cnh (head,
string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
type_of_combterm t)
@@ -271,15 +251,15 @@
(*Boolean-valued terms are here converted to literals.*)
fun boolify params t =
- "hBOOL" ^ SFC.paren_pack [string_of_combterm params t];
+ "hBOOL" ^ paren_pack [string_of_combterm params t];
fun string_of_predicate (params as (_,_,cnh)) t =
case t of
(CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
(*DFG only: new TPTP prefers infix equality*)
- ("equal" ^ SFC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
+ ("equal" ^ paren_pack [string_of_combterm params t1, string_of_combterm params t2])
| _ =>
- case #1 (strip_comb t) of
+ case #1 (strip_combterm_comb t) of
CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
| _ => boolify params t;
@@ -290,31 +270,31 @@
let val eqop = if pol then " = " else " != "
in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end;
-fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
+fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal", _, _), t1), t2))) =
tptp_of_equality params pol (t1,t2)
| tptp_literal params (Literal(pol,pred)) =
- SFC.tptp_sign pol (string_of_predicate params pred);
+ tptp_sign pol (string_of_predicate params pred);
(*Given a clause, returns its literals paired with a list of literals concerning TFrees;
the latter should only occur in conjecture clauses.*)
-fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
+fun tptp_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
(map (tptp_literal params) literals,
- map (SFC.tptp_of_typeLit pos) (SFC.add_typs ctypes_sorts));
+ map (tptp_of_typeLit pos) (add_typs ctypes_sorts));
-fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) =
- let val (lits,tylits) = tptp_type_lits params (kind = SFC.Conjecture) cls
+fun clause2tptp params (cls as HOLClause {axiom_name, clause_id, kind, ...}) =
+ let val (lits,tylits) = tptp_type_lits params (kind = Conjecture) cls
in
- (SFC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
+ (gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits)
end;
(*** dfg format ***)
-fun dfg_literal params (Literal(pol,pred)) = SFC.dfg_sign pol (string_of_predicate params pred);
+fun dfg_literal params (Literal(pol,pred)) = dfg_sign pol (string_of_predicate params pred);
-fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
+fun dfg_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
(map (dfg_literal params) literals,
- map (SFC.dfg_of_typeLit pos) (SFC.add_typs ctypes_sorts));
+ map (dfg_of_typeLit pos) (add_typs ctypes_sorts));
fun get_uvars (CombConst _) vars = vars
| get_uvars (CombVar(v,_)) vars = (v::vars)
@@ -322,20 +302,21 @@
fun get_uvars_l (Literal(_,c)) = get_uvars c [];
-fun dfg_vars (Clause {literals,...}) = SFC.union_all (map get_uvars_l literals);
+fun dfg_vars (HOLClause {literals,...}) = union_all (map get_uvars_l literals);
-fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
- let val (lits,tylits) = dfg_type_lits params (kind = SFC.Conjecture) cls
+fun clause2dfg params (cls as HOLClause {axiom_name, clause_id, kind,
+ ctypes_sorts, ...}) =
+ let val (lits,tylits) = dfg_type_lits params (kind = Conjecture) cls
val vars = dfg_vars cls
- val tvars = SFC.get_tvar_strs ctypes_sorts
+ val tvars = get_tvar_strs ctypes_sorts
in
- (SFC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
+ (gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
end;
(** For DFG format: accumulate function and predicate declarations **)
-fun addtypes tvars tab = List.foldl SFC.add_foltype_funcs tab tvars;
+fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
if c = "equal" then (addtypes tvars funcs, preds)
@@ -348,33 +329,33 @@
else (addtypes tvars funcs, addit preds)
end
| add_decls _ (CombVar(_,ctp), (funcs,preds)) =
- (SFC.add_foltype_funcs (ctp,funcs), preds)
+ (add_foltype_funcs (ctp,funcs), preds)
| add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
-fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls);
+fun add_literal_decls params (Literal (_,c), decls) = add_decls params (c,decls);
-fun add_clause_decls params (Clause {literals, ...}, decls) =
+fun add_clause_decls params (HOLClause {literals, ...}, decls) =
List.foldl (add_literal_decls params) decls literals
handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
fun decls_of_clauses params clauses arity_clauses =
- let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) SFC.init_functab)
+ let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) init_functab)
val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
in
- (Symtab.dest (List.foldl SFC.add_arityClause_funcs functab arity_clauses),
+ (Symtab.dest (List.foldl add_arity_clause_funcs functab arity_clauses),
Symtab.dest predtab)
end;
-fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
- List.foldl SFC.add_type_sort_preds preds ctypes_sorts
+fun add_clause_preds (HOLClause {ctypes_sorts, ...}, preds) =
+ List.foldl add_type_sort_preds preds ctypes_sorts
handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
(*Higher-order clauses have only the predicates hBOOL and type classes.*)
fun preds_of_clauses clauses clsrel_clauses arity_clauses =
Symtab.dest
- (List.foldl SFC.add_classrelClause_preds
- (List.foldl SFC.add_arityClause_preds
+ (List.foldl add_classrel_clause_preds
+ (List.foldl add_arity_clause_preds
(List.foldl add_clause_preds Symtab.empty clauses)
arity_clauses)
clsrel_clauses)
@@ -385,9 +366,8 @@
(**********************************************************************)
val init_counters =
- Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
- ("c_COMBB", 0), ("c_COMBC", 0),
- ("c_COMBS", 0)];
+ Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
+ ("c_COMBS", 0)];
fun count_combterm (CombConst (c, _, _), ct) =
(case Symtab.lookup ct c of NONE => ct (*no counter*)
@@ -397,18 +377,18 @@
fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
-fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals;
+fun count_clause (HOLClause {literals, ...}, ct) =
+ List.foldl count_literal ct literals;
-fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
+fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}, ct) =
if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
else ct;
-fun cnf_helper_thms thy =
- Sledgehammer_Fact_Preprocessor.cnf_rules_pairs thy
- o map Sledgehammer_Fact_Preprocessor.pairname
+fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname
fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
- if isFO then [] (*first-order*)
+ if isFO then
+ []
else
let
val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
@@ -416,15 +396,15 @@
val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
fun needed c = the (Symtab.lookup ct c) > 0
val IK = if needed "c_COMBI" orelse needed "c_COMBK"
- then cnf_helper_thms thy [comb_I,comb_K]
+ then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
else []
val BC = if needed "c_COMBB" orelse needed "c_COMBC"
- then cnf_helper_thms thy [comb_B,comb_C]
+ then cnf_helper_thms thy [@{thm COMBB_def}, @{thm COMBC_def}]
else []
- val S = if needed "c_COMBS"
- then cnf_helper_thms thy [comb_S]
+ val S = if needed "c_COMBS" then cnf_helper_thms thy [@{thm COMBS_def}]
else []
- val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
+ val other = cnf_helper_thms thy [@{thm fequal_imp_equal},
+ @{thm equal_imp_fequal}]
in
map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
end;
@@ -432,7 +412,7 @@
(*Find the minimal arity of each function mentioned in the term. Also, note which uses
are not at top level, to see if hBOOL is needed.*)
fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
- let val (head, args) = strip_comb t
+ let val (head, args) = strip_combterm_comb t
val n = length args
val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
in
@@ -451,11 +431,12 @@
fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
count_constants_term true t (const_min_arity, const_needs_hBOOL);
-fun count_constants_clause (Clause{literals,...}) (const_min_arity, const_needs_hBOOL) =
+fun count_constants_clause (HOLClause {literals, ...})
+ (const_min_arity, const_needs_hBOOL) =
fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
fun display_arity const_needs_hBOOL (c,n) =
- Sledgehammer_Fact_Preprocessor.trace_msg (fn () => "Constant: " ^ c ^
+ trace_msg (fn () => "Constant: " ^ c ^
" arity:\t" ^ Int.toString n ^
(if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
@@ -469,31 +450,31 @@
in (const_min_arity, const_needs_hBOOL) end
else (Symtab.empty, Symtab.empty);
-(* tptp format *)
+(* TPTP format *)
-fun tptp_write_file t_full file clauses =
+fun write_tptp_file t_full file clauses =
let
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
val params = (t_full, cma, cnh)
val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
- val tfree_clss = map SFC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
+ val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
val _ =
File.write_list file (
map (#1 o (clause2tptp params)) axclauses @
tfree_clss @
tptp_clss @
- map SFC.tptp_classrelClause classrel_clauses @
- map SFC.tptp_arity_clause arity_clauses @
+ map tptp_classrel_clause classrel_clauses @
+ map tptp_arity_clause arity_clauses @
map (#1 o (clause2tptp params)) helper_clauses)
in (length axclauses + 1, length tfree_clss + length tptp_clss)
end;
-(* dfg format *)
+(* DFG format *)
-fun dfg_write_file t_full file clauses =
+fun write_dfg_file t_full file clauses =
let
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
@@ -502,20 +483,20 @@
val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
and probname = Path.implode (Path.base file)
val axstrs = map (#1 o (clause2dfg params)) axclauses
- val tfree_clss = map SFC.dfg_tfree_clause (SFC.union_all tfree_litss)
+ val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
val _ =
File.write_list file (
- SFC.string_of_start probname ::
- SFC.string_of_descrip probname ::
- SFC.string_of_symbols (SFC.string_of_funcs funcs)
- (SFC.string_of_preds (cl_preds @ ty_preds)) ::
+ string_of_start probname ::
+ string_of_descrip probname ::
+ string_of_symbols (string_of_funcs funcs)
+ (string_of_preds (cl_preds @ ty_preds)) ::
"list_of_clauses(axioms,cnf).\n" ::
axstrs @
- map SFC.dfg_classrelClause classrel_clauses @
- map SFC.dfg_arity_clause arity_clauses @
+ map dfg_classrel_clause classrel_clauses @
+ map dfg_arity_clause arity_clauses @
helper_clauses_strs @
["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
tfree_clss @
@@ -530,4 +511,3 @@
end;
end;
-
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Mar 19 13:02:18 2010 +0100
@@ -7,33 +7,29 @@
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
sig
val chained_hint: string
-
- val fix_sorts: sort Vartab.table -> term -> term
val invert_const: string -> string
val invert_type_const: string -> string
val num_typargs: theory -> string -> int
val make_tvar: string -> typ
val strip_prefix: string -> string -> string option
val setup: theory -> theory
- (* extracting lemma list*)
- val find_failure: string -> string option
- val lemma_list: bool -> string ->
+ val is_proof_well_formed: string -> bool
+ val metis_lemma_list: bool -> string ->
string * string vector * (int * int) * Proof.context * thm * int -> string * string list
- (* structured proofs *)
- val structured_proof: string ->
+ val structured_isar_proof: string ->
string * string vector * (int * int) * Proof.context * thm * int -> string * string list
end;
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
struct
-structure SFC = Sledgehammer_FOL_Clause
-
-val trace_path = Path.basic "atp_trace";
+open Sledgehammer_FOL_Clause
+open Sledgehammer_Fact_Preprocessor
-fun trace s =
- if ! Sledgehammer_Fact_Preprocessor.trace then File.append (File.tmp_path trace_path) s
- else ();
+val trace_proof_path = Path.basic "atp_trace";
+
+fun trace_proof_msg f =
+ if !trace then File.append (File.tmp_path trace_proof_path) (f ()) else ();
fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
@@ -43,9 +39,6 @@
(*Indicates whether to include sort information in generated proofs*)
val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true;
-(*Indicated whether to generate full proofs or just lemma lists - now via setup of atps*)
-(* val (full_proofs, full_proofs_setup) = Attrib.config_bool "sledgehammer_full" false; *)
-
val setup = modulus_setup #> recon_sorts_setup;
(**** PARSING OF TSTP FORMAT ****)
@@ -109,12 +102,12 @@
(*If string s has the prefix s1, return the result of deleting it.*)
fun strip_prefix s1 s =
if String.isPrefix s1 s
- then SOME (SFC.undo_ascii_of (String.extract (s, size s1, NONE)))
+ then SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
else NONE;
(*Invert the table of translations between Isabelle and ATPs*)
val type_const_trans_table_inv =
- Symtab.make (map swap (Symtab.dest SFC.type_const_trans_table));
+ Symtab.make (map swap (Symtab.dest type_const_trans_table));
fun invert_type_const c =
case Symtab.lookup type_const_trans_table_inv c of
@@ -132,15 +125,15 @@
| Br (a,ts) =>
let val Ts = map type_of_stree ts
in
- case strip_prefix SFC.tconst_prefix a of
+ 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 SFC.tfree_prefix a of
+ case strip_prefix tfree_prefix a of
SOME b => TFree("'" ^ b, HOLogic.typeS)
| NONE =>
- case strip_prefix SFC.tvar_prefix a of
+ case strip_prefix tvar_prefix a of
SOME b => make_tvar b
| NONE => make_tvar a (*Variable from the ATP, say X1*)
end;
@@ -148,7 +141,7 @@
(*Invert the table of translations between Isabelle and ATPs*)
val const_trans_table_inv =
Symtab.update ("fequal", "op =")
- (Symtab.make (map swap (Symtab.dest SFC.const_trans_table)));
+ (Symtab.make (map swap (Symtab.dest const_trans_table)));
fun invert_const c =
case Symtab.lookup const_trans_table_inv c of
@@ -169,9 +162,9 @@
| Br ("hBOOL",[t]) => term_of_stree [] thy t (*ignore hBOOL*)
| Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t
| Br (a,ts) =>
- case strip_prefix SFC.const_prefix a of
+ case strip_prefix const_prefix a of
SOME "equal" =>
- list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
+ 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
@@ -183,10 +176,10 @@
| NONE => (*a variable, not a constant*)
let val T = HOLogic.typeT
val opr = (*a Free variable is typically a Skolem function*)
- case strip_prefix SFC.fixed_var_prefix a of
+ case strip_prefix fixed_var_prefix a of
SOME b => Free(b,T)
| NONE =>
- case strip_prefix SFC.schematic_var_prefix a of
+ 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;
@@ -196,7 +189,7 @@
| constraint_of_stree pol t = case t of
Int _ => raise STREE t
| Br (a,ts) =>
- (case (strip_prefix SFC.class_prefix a, map type_of_stree ts) of
+ (case (strip_prefix class_prefix a, map type_of_stree ts) of
(SOME b, [T]) => (pol, b, T)
| _ => raise STREE t);
@@ -286,7 +279,7 @@
may disagree. We have to try all combinations of literals (quadratic!) and
match up the variable names consistently. **)
-fun strip_alls_aux n (Const("all",_)$Abs(a,T,t)) =
+fun strip_alls_aux n (Const(@{const_name all}, _)$Abs(a,T,t)) =
strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t))
| strip_alls_aux _ t = t;
@@ -347,7 +340,7 @@
ATP may have their literals reordered.*)
fun isar_lines ctxt ctms =
let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term)
- val _ = trace ("\n\nisar_lines: start\n")
+ val _ = trace_proof_msg (K "\n\nisar_lines: start\n")
fun doline _ (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*)
(case permuted_clause t ctms of
SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
@@ -399,7 +392,7 @@
| add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines
and delete_dep lno lines = List.foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines);
-fun bad_free (Free (a,_)) = String.isPrefix "sko_" a
+fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a
| bad_free _ = false;
(*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies.
@@ -436,26 +429,22 @@
| isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
fun decode_tstp_file cnfs ctxt th sgno thm_names =
- let val _ = trace "\ndecode_tstp_file: start\n"
+ let val _ = trace_proof_msg (K "\ndecode_tstp_file: start\n")
val tuples = map (dest_tstp o tstp_line o explode) cnfs
- val _ = trace (Int.toString (length tuples) ^ " tuples extracted\n")
+ val _ = trace_proof_msg (fn () => Int.toString (length tuples) ^ " tuples extracted\n")
val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
- val _ = trace (Int.toString (length raw_lines) ^ " raw_lines extracted\n")
+ val _ = trace_proof_msg (fn () => Int.toString (length raw_lines) ^ " raw_lines extracted\n")
val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
- val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
- val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
- val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
- val (ccls,fixes) = Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th sgno
- val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
+ val _ = trace_proof_msg (fn () => Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
+ val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
+ val _ = trace_proof_msg (fn () => Int.toString (length lines) ^ " lines extracted\n")
+ val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno
+ val _ = trace_proof_msg (fn () => Int.toString (length ccls) ^ " conjecture clauses\n")
val ccls = map forall_intr_vars ccls
- val _ =
- if ! Sledgehammer_Fact_Preprocessor.trace then
- app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
- else
- ()
+ val _ = app (fn th => trace_proof_msg (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
- val _ = trace "\ndecode_tstp_file: finishing\n"
+ val _ = trace_proof_msg (K "\ndecode_tstp_file: finishing\n")
in
isar_header (map #1 fixes) ^ implode ilines ^ "qed\n"
end handle STREE _ => error "Could not extract proof (ATP output malformed?)";
@@ -463,11 +452,11 @@
(*=== EXTRACTING PROOF-TEXT === *)
-val begin_proof_strings = ["# SZS output start CNFRefutation.",
+val begin_proof_strs = ["# SZS output start CNFRefutation.",
"=========== Refutation ==========",
"Here is a proof"];
-val end_proof_strings = ["# SZS output end CNFRefutation",
+val end_proof_strs = ["# SZS output end CNFRefutation",
"======= End of refutation =======",
"Formulae used in the proof"];
@@ -475,8 +464,8 @@
let
(*splits to_split by the first possible of a list of splitters*)
val (begin_string, end_string) =
- (find_first (fn s => String.isSubstring s proof) begin_proof_strings,
- find_first (fn s => String.isSubstring s proof) end_proof_strings)
+ (find_first (fn s => String.isSubstring s proof) begin_proof_strs,
+ find_first (fn s => String.isSubstring s proof) end_proof_strs)
in
if is_none begin_string orelse is_none end_string
then error "Could not extract proof (no substring indicating a proof)"
@@ -484,36 +473,24 @@
|> first_field (the end_string) |> the |> fst
end;
-(* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
+(* ==== CHECK IF PROOF WAS SUCCESSFUL === *)
-val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
- "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
-val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
-val failure_strings_SPASS = ["SPASS beiseite: Completion found.",
- "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."];
-val failure_strings_remote = ["Remote-script could not extract proof"];
-fun find_failure proof =
- let val failures =
- map_filter (fn s => if String.isSubstring s proof then SOME s else NONE)
- (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
- val correct = null failures andalso
- exists (fn s => String.isSubstring s proof) begin_proof_strings andalso
- exists (fn s => String.isSubstring s proof) end_proof_strings
- in
- if correct then NONE
- else if null failures then SOME "Output of ATP not in proper format"
- else SOME (hd failures) end;
+fun is_proof_well_formed proof =
+ exists (fn s => String.isSubstring s proof) begin_proof_strs andalso
+ exists (fn s => String.isSubstring s proof) end_proof_strs
(* === EXTRACTING LEMMAS === *)
(* lines have the form "cnf(108, axiom, ...",
the number (108) has to be extracted)*)
-fun get_step_nums false proofextract =
- let val toks = String.tokens (not o Char.isAlphaNum)
- fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
- | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok
- | inputno _ = NONE
- val lines = split_lines proofextract
- in map_filter (inputno o toks) lines end
+fun get_step_nums false extract =
+ let
+ val toks = String.tokens (not o Char.isAlphaNum)
+ fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok
+ | inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) =
+ Int.fromString ntok
+ | inputno _ = NONE
+ val lines = split_lines extract
+ in map_filter (inputno o toks) lines end
(*String contains multiple lines. We want those of the form
"253[0:Inp] et cetera..."
A list consisting of the first number in each line is returned. *)
@@ -527,27 +504,25 @@
(*extracting lemmas from tstp-output between the lines from above*)
fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
let
- (* get the names of axioms from their numbers*)
- fun get_axiom_names thm_names step_nums =
- let
- val last_axiom = Vector.length thm_names
- fun is_axiom n = n <= last_axiom
- fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count
- fun getname i = Vector.sub(thm_names, i-1)
- in
- (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
- (map getname (filter is_axiom step_nums))),
- exists is_conj step_nums)
- end
- val proofextract = get_proof_extract proof
- in
- get_axiom_names thm_names (get_step_nums proofextract)
- end;
+ (* get the names of axioms from their numbers*)
+ fun get_axiom_names thm_names step_nums =
+ let
+ val last_axiom = Vector.length thm_names
+ fun is_axiom n = n <= last_axiom
+ fun is_conj n = n >= fst conj_count andalso
+ n < fst conj_count + snd conj_count
+ fun getname i = Vector.sub(thm_names, i-1)
+ in
+ (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
+ (map getname (filter is_axiom step_nums))),
+ exists is_conj step_nums)
+ end
+ in get_axiom_names thm_names (get_step_nums (get_proof_extract proof)) end;
(*Used to label theorems chained into the sledgehammer call*)
val chained_hint = "CHAINED";
-val nochained = filter_out (fn y => y = chained_hint)
-
+val kill_chained = filter_out (curry (op =) chained_hint)
+
(* metis-command *)
fun metis_line [] = "apply metis"
| metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
@@ -556,33 +531,36 @@
fun minimize_line _ [] = ""
| minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
(Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^
- space_implode " " (nochained lemmas))
+ space_implode " " (kill_chained lemmas))
-fun sendback_metis_nochained lemmas =
- (Markup.markup Markup.sendback o metis_line) (nochained lemmas)
+val sendback_metis_no_chained =
+ Markup.markup Markup.sendback o metis_line o kill_chained
-fun lemma_list dfg name result =
+fun metis_lemma_list dfg name result =
let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
- in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
- (if used_conj then ""
- else "\nWarning: Goal is provable because context is inconsistent."),
- nochained lemmas)
+ in (sendback_metis_no_chained lemmas ^ "\n" ^ minimize_line name lemmas ^
+ (if used_conj then
+ ""
+ else
+ "\nWarning: The goal is provable because the context is inconsistent."),
+ kill_chained lemmas)
end;
-(* === Extracting structured Isar-proof === *)
-fun structured_proof name (result as (proof, thm_names, conj_count, ctxt, goal, subgoalno)) =
+fun structured_isar_proof name (result as (proof, thm_names, conj_count, ctxt,
+ goal, subgoalno)) =
let
- (*Could use split_lines, but it can return blank lines...*)
- val lines = String.tokens (equal #"\n");
- val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
- val proofextract = get_proof_extract proof
- val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
- val (one_line_proof, lemma_names) = lemma_list false name result
- val structured =
- if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
- else decode_tstp_file cnfs ctxt goal subgoalno thm_names
+ (* Could use "split_lines", but it can return blank lines *)
+ val lines = String.tokens (equal #"\n");
+ val kill_spaces = String.translate (fn c => if Char.isSpace c then "" else str c)
+ val extract = get_proof_extract proof
+ val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
+ val (one_line_proof, lemma_names) = metis_lemma_list false name result
+ val structured =
+ if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
+ else decode_tstp_file cnfs ctxt goal subgoalno thm_names
in
- (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured, lemma_names)
-end
+ (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured,
+ lemma_names)
+ end
end;