--- a/src/HOL/Boogie/Tools/boogie_commands.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Mon Mar 22 13:48:15 2010 +0100
@@ -63,9 +63,8 @@
THEN' Boogie_Tactics.drop_assert_at_tac
THEN' SUBPROOF (fn _ => Tactic.rtac thm 1) context))
in
-fun boogie_vc (vc_name, vc_opts) lthy =
+fun boogie_vc (vc_name, vc_opts) thy =
let
- val thy = ProofContext.theory_of lthy
val vc = get_vc thy vc_name
fun extract vc l =
@@ -92,16 +91,16 @@
| _ => (pair ts, K I))
val discharge = fold (Boogie_VCs.discharge o pair vc_name)
- fun after_qed [thms] = Local_Theory.theory (discharge (vcs ~~ thms))
+ fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
| after_qed _ = I
in
- lthy
+ ProofContext.init thy
|> fold Variable.auto_fixes ts
- |> (fn lthy1 => lthy1
+ |> (fn ctxt1 => ctxt1
|> prepare
- |-> (fn us => fn lthy2 => lthy2
+ |-> (fn us => fn ctxt2 => ctxt2
|> Proof.theorem_i NONE (fn thmss => fn ctxt =>
- let val export = map (finish lthy1) o ProofContext.export ctxt lthy2
+ let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
end
end
@@ -300,7 +299,7 @@
"Enter into proof mode for a specific verification condition."
OuterKeyword.thy_goal
(vc_name -- vc_opts >> (fn args =>
- (Toplevel.print o Toplevel.local_theory_to_proof NONE (boogie_vc args))))
+ (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
val quick_timeout = 5
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Mon Mar 22 13:48:15 2010 +0100
@@ -238,10 +238,14 @@
|> split_list_kind thy o Termtab.dest
in
fun add_axioms verbose axs thy =
- let val (used, new) = mark_axioms thy (name_axioms axs)
+ let
+ val (used, new) = mark_axioms thy (name_axioms axs)
+ fun add (n, t) =
+ Specification.axiomatization [] [((Binding.name n, []), [t])] #>>
+ hd o hd o snd
in
thy
- |> fold_map (Drule.add_axiom o apfst Binding.name) new
+ |> fold_map add new
|-> Context.theory_map o fold Boogie_Axioms.add_thm
|> log verbose "The following axioms were added:" (map fst new)
|> (fn thy' => log verbose "The following axioms already existed:"
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Mon Mar 22 13:48:15 2010 +0100
@@ -27,6 +27,9 @@
val state_of_vc: theory -> string -> string list * string list
val close: theory -> theory
val is_closed: theory -> bool
+
+ val rewrite_vcs: (theory -> term -> term) -> (theory -> thm -> thm) ->
+ theory -> theory
end
structure Boogie_VCs: BOOGIE_VCS =
@@ -252,30 +255,35 @@
(* the VC store *)
-fun err_vcs () = error "undischarged Boogie verification conditions found"
+fun err_unfinished () = error "An unfinished Boogie environment is still open."
+
+fun err_vcs names = error (Pretty.string_of
+ (Pretty.big_list "Undischarged Boogie verification conditions found:"
+ (map Pretty.str names)))
structure VCs = Theory_Data
(
- type T = (vc * thm) Symtab.table option
+ type T = ((vc * (term * thm)) Symtab.table * (theory -> thm -> thm)) option
val empty = NONE
val extend = I
fun merge (NONE, NONE) = NONE
- | merge _ = err_vcs ()
+ | merge _ = err_unfinished ()
)
-fun prep thy t = vc_of_term t |> (fn vc => (vc, thm_of thy vc))
+fun prep thy = vc_of_term #> (fn vc => (vc, (prop_of_vc vc, thm_of thy vc)))
fun set vcs thy = VCs.map (fn
- NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs))
- | SOME _ => err_vcs ()) thy
+ NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs), K I)
+ | SOME _ => err_unfinished ()) thy
fun lookup thy name =
(case VCs.get thy of
- SOME vcs => Option.map fst (Symtab.lookup vcs name)
+ SOME (vcs, _) => Option.map fst (Symtab.lookup vcs name)
| NONE => NONE)
fun discharge (name, prf) =
- VCs.map (Option.map (Symtab.map_entry name (join prf)))
+ let fun jn (vc, (t, thm)) = join prf (vc, thm) |> apsnd (pair t)
+ in VCs.map (Option.map (apfst (Symtab.map_entry name jn))) end
datatype state = Proved | NotProved | PartiallyProved
@@ -284,21 +292,35 @@
SOME vc => names_of vc
| NONE => ([], []))
+fun state_of_vc' (vc, _) =
+ (case names_of vc of
+ ([], _) => Proved
+ | (_, []) => NotProved
+ | (_, _) => PartiallyProved)
+
fun state_of thy =
(case VCs.get thy of
- SOME vcs => Symtab.dest vcs |> map (apsnd (fst #> names_of #> (fn
- ([], _) => Proved
- | (_, []) => NotProved
- | (_, _) => PartiallyProved)))
+ SOME (vcs, _) => map (apsnd state_of_vc') (Symtab.dest vcs)
| NONE => [])
+fun finished g (_, (t, thm)) = Thm.prop_of (g thm) aconv t
+
fun close thy = thy |> VCs.map (fn
- SOME _ =>
- if forall (fn (_, Proved) => true | _ => false) (state_of thy)
- then NONE
- else err_vcs ()
+ SOME (vcs, g) =>
+ let fun check vc = state_of_vc' vc = Proved andalso finished (g thy) vc
+ in
+ Symtab.dest vcs
+ |> map_filter (fn (n, vc) => if check vc then NONE else SOME n)
+ |> (fn names => if null names then NONE else err_vcs names)
+ end
| NONE => NONE)
val is_closed = is_none o VCs.get
+fun rewrite_vcs f g thy =
+ let
+ fun rewr (_, (t, _)) = vc_of_term (f thy t)
+ |> (fn vc => (vc, (t, thm_of thy vc)))
+ in VCs.map (Option.map (fn (vcs, _) => (Symtab.map rewr vcs, g))) thy end
+
end
--- a/src/HOL/IsaMakefile Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/IsaMakefile Mon Mar 22 13:48:15 2010 +0100
@@ -313,11 +313,13 @@
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 \
Tools/Sledgehammer/sledgehammer_fol_clause.ML \
Tools/Sledgehammer/sledgehammer_hol_clause.ML \
+ Tools/Sledgehammer/sledgehammer_isar.ML \
Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
Tools/string_code.ML \
Tools/string_syntax.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Mar 22 13:48:15 2010 +0100
@@ -42,8 +42,7 @@
datatype min_data = MinData of {
succs: int,
- ab_ratios: int,
- it_ratios: int
+ ab_ratios: int
}
fun make_sh_data
@@ -51,23 +50,22 @@
ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems,
time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail}
-fun make_min_data (succs, ab_ratios, it_ratios) =
- MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios}
+fun make_min_data (succs, ab_ratios) =
+ MinData{succs=succs, ab_ratios=ab_ratios}
fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) =
MeData{calls=calls, success=success, proofs=proofs, time=time,
timeout=timeout, lemmas=lemmas, posns=posns}
val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0)
-val empty_min_data = make_min_data(0, 0, 0)
-val empty_me_data = make_me_data(0, 0, 0, 0, 0, (0,0,0), [])
+val empty_min_data = make_min_data (0, 0)
+val empty_me_data = make_me_data (0, 0, 0, 0, 0, (0,0,0), [])
fun tuple_of_sh_data (ShData {calls, success, lemmas, max_lems, time_isa,
time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa,
time_atp, time_atp_fail)
-fun tuple_of_min_data (MinData {succs, ab_ratios, it_ratios}) =
- (succs, ab_ratios, it_ratios)
+fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas,
posns}) = (calls, success, proofs, time, timeout, lemmas, posns)
@@ -147,13 +145,10 @@
=> (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail + t))
val inc_min_succs = map_min_data
- (fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios))
+ (fn (succs,ab_ratios) => (succs+1, ab_ratios))
fun inc_min_ab_ratios r = map_min_data
- (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios))
-
-fun inc_min_it_ratios r = map_min_data
- (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r))
+ (fn (succs, ab_ratios) => (succs, ab_ratios+r))
val inc_metis_calls = map_me_data
(fn (calls,success,proofs,time,timeout,lemmas,posns)
@@ -234,10 +229,9 @@
else ()
)
-fun log_min_data log (succs, ab_ratios, it_ratios) =
+fun log_min_data log (succs, ab_ratios) =
(log ("Number of successful minimizations: " ^ string_of_int succs);
- log ("After/before ratios: " ^ string_of_int ab_ratios);
- log ("Iterations ratios: " ^ string_of_int it_ratios)
+ log ("After/before ratios: " ^ string_of_int ab_ratios)
)
in
@@ -313,19 +307,19 @@
ctxt
|> change_dir dir
|> Config.put ATP_Wrapper.measure_runtime true
- val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
+ val problem = ATP_Manager.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
val time_limit =
(case hard_timeout of
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
- val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Wrapper.prover_result,
+ val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Manager.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
in
if success then (message, SH_OK (time_isa, time_atp, theorem_names))
else (message, SH_FAIL(time_isa, time_atp))
end
- handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
+ handle Sledgehammer_HOL_Clause.TRIVIAL => ("trivial", SH_OK (0, 0, []))
| ERROR msg => ("error: " ^ msg, SH_ERROR)
| TimeLimit.TimeOut => ("timeout", SH_ERROR)
@@ -380,9 +374,10 @@
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
let
+ open ATP_Minimal
val n0 = length (these (!named_thms))
val (prover_name, prover) = get_atp (Proof.theory_of st) args
- val minimize = ATP_Minimal.minimalize prover prover_name
+ val minimize = minimize_theorems linear_minimize prover prover_name
val timeout =
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o explode)
@@ -390,10 +385,9 @@
val _ = log separator
in
case minimize timeout st (these (!named_thms)) of
- (SOME (named_thms',its), msg) =>
+ (SOME named_thms', msg) =>
(change_data id inc_min_succs;
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
- change_data id (inc_min_it_ratios ((100*its) div n0));
if length named_thms' = n0
then log (minimize_tag id ^ "already minimal")
else (named_thms := SOME named_thms';
--- a/src/HOL/Sledgehammer.thy Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Sledgehammer.thy Mon Mar 22 13:48:15 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,71 +20,72 @@
("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/sledgehammer_isar.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)
@@ -91,35 +94,24 @@
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"
use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
setup Sledgehammer_Proof_Reconstruct.setup
use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
-
+use "Tools/ATP_Manager/atp_manager.ML"
use "Tools/ATP_Manager/atp_wrapper.ML"
setup ATP_Wrapper.setup
-use "Tools/ATP_Manager/atp_manager.ML"
use "Tools/ATP_Manager/atp_minimal.ML"
+use "Tools/Sledgehammer/sledgehammer_isar.ML"
-text {* basic provers *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
-text {* provers with stuctured output *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
+subsection {* The MESON prover *}
-text {* on some problems better results *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
-
-text {* remote provers via SystemOnTPTP *}
-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 *}
-
+use "Tools/Sledgehammer/meson_tactic.ML"
+setup Meson_Tactic.setup
subsection {* The Metis prover *}
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 22 13:48:15 2010 +0100
@@ -7,6 +7,23 @@
signature ATP_MANAGER =
sig
+ type problem =
+ {with_full_types: bool,
+ subgoal: int,
+ goal: Proof.context * (thm list * thm),
+ axiom_clauses: (thm * (string * int)) list option,
+ filtered_clauses: (thm * (string * int)) list option}
+ val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
+ type prover_result =
+ {success: bool,
+ message: string,
+ theorem_names: string list,
+ runtime: int,
+ proof: string,
+ internal_thm_names: string Vector.vector,
+ filtered_clauses: (thm * (string * int)) list}
+ type prover = int -> problem -> prover_result
+
val atps: string Unsynchronized.ref
val get_atps: unit -> string list
val timeout: int Unsynchronized.ref
@@ -14,15 +31,43 @@
val kill: unit -> unit
val info: unit -> unit
val messages: int option -> unit
- val add_prover: string * ATP_Wrapper.prover -> theory -> theory
- val get_prover: theory -> string -> ATP_Wrapper.prover option
+ val add_prover: string * prover -> theory -> theory
+ val get_prover: theory -> string -> prover option
val print_provers: theory -> unit
val sledgehammer: string list -> Proof.state -> unit
end;
-structure ATP_Manager: ATP_MANAGER =
+structure ATP_Manager : ATP_MANAGER =
struct
+(** problems, results, and provers **)
+
+type problem =
+ {with_full_types: bool,
+ subgoal: int,
+ goal: Proof.context * (thm list * thm),
+ axiom_clauses: (thm * (string * int)) list option,
+ filtered_clauses: (thm * (string * int)) list option};
+
+fun problem_of_goal with_full_types subgoal goal : problem =
+ {with_full_types = with_full_types,
+ subgoal = subgoal,
+ goal = goal,
+ axiom_clauses = NONE,
+ filtered_clauses = NONE};
+
+type prover_result =
+ {success: bool,
+ message: string,
+ theorem_names: string list, (*relevant theorems*)
+ runtime: int, (*user time of the ATP, in milliseconds*)
+ proof: string,
+ internal_thm_names: string Vector.vector,
+ filtered_clauses: (thm * (string * int)) list};
+
+type prover = int -> problem -> prover_result;
+
+
(** preferences **)
val message_store_limit = 20;
@@ -228,7 +273,7 @@
structure Provers = Theory_Data
(
- type T = (ATP_Wrapper.prover * stamp) Symtab.table;
+ type T = (prover * stamp) Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data : T = Symtab.merge (eq_snd op =) data
@@ -261,9 +306,9 @@
val _ = Toplevel.thread true (fn () =>
let
val _ = register birth_time death_time (Thread.self (), desc);
- val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
+ val problem = 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 ());
@@ -282,36 +327,4 @@
val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers;
in () end;
-
-
-(** Isar command syntax **)
-
-local structure K = OuterKeyword and P = OuterParse in
-
-val _ =
- OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
-
-val _ =
- OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
-
-val _ =
- OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
- (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
- (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
-
-val _ =
- OuterSyntax.improper_command "print_atps" "print external provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
- Toplevel.keep (print_provers o Toplevel.theory_of)));
-
-val _ =
- OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
- (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
-
end;
-
-end;
-
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Mar 22 13:48:15 2010 +0100
@@ -1,32 +1,40 @@
(* Title: HOL/Tools/ATP_Manager/atp_minimal.ML
Author: Philipp Meyer, TU Muenchen
-Minimization of theorem list for metis by using an external automated theorem prover
+Minimization of theorem list for Metis using automatic theorem provers.
*)
signature ATP_MINIMAL =
sig
- val minimize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
- (string * thm list) list -> ((string * thm list) list * int) option * string
- (* To be removed once TN has finished his measurements;
- the int component of the result should then be removed: *)
- val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
- (string * thm list) list -> ((string * thm list) list * int) option * string
-end
+ type prover = ATP_Manager.prover
+ type prover_result = ATP_Manager.prover_result
+ type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
-structure ATP_Minimal: ATP_MINIMAL =
+ val linear_minimize : 'a minimize_fun
+ val binary_minimize : 'a minimize_fun
+ val minimize_theorems :
+ (string * thm list) minimize_fun -> prover -> string -> int
+ -> Proof.state -> (string * thm list) list
+ -> (string * thm list) list option * string
+end;
+
+structure ATP_Minimal : ATP_MINIMAL =
struct
-(* Linear minimization *)
+open Sledgehammer_Fact_Preprocessor
+open ATP_Manager
+
+type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
+
+(* Linear minimization algorithm *)
-fun lin_gen_minimize p s =
-let
- fun min [] needed = needed
- | min (x::xs) needed =
- if p(xs @ needed) then min xs needed else min xs (x::needed)
-in (min s [], length s) end;
+fun linear_minimize p s =
+ let
+ fun aux [] needed = needed
+ | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x)
+ in aux s [] end;
-(* Clever minimalization algorithm *)
+(* Binary minimalization *)
local
fun isplit (l, r) [] = (l, r)
@@ -37,24 +45,21 @@
end
local
- fun min p sup [] = raise Empty
- | min p sup [s0] = [s0]
+ fun min _ _ [] = raise Empty
+ | min _ _ [s0] = [s0]
| min p sup s =
let
val (l0, r0) = split s
in
- if p (sup @ l0)
- then min p sup l0
+ if p (sup @ l0) then
+ min p sup l0
+ else if p (sup @ r0) then
+ min p sup r0
else
- if p (sup @ r0)
- then min p sup r0
- else
- let
- val l = min p (sup @ r0) l0
- val r = min p (sup @ l) r0
- in
- l @ r
- end
+ let
+ val l = min p (sup @ r0) l0
+ val r = min p (sup @ l) r0
+ in l @ r end
end
in
(* return a minimal subset v of s that satisfies p
@@ -62,15 +67,10 @@
@post v subset s & p(v) &
forall e in v. ~p(v \ e)
*)
- fun minimal p s =
- let
- val count = Unsynchronized.ref 0
- fun p_count xs = (Unsynchronized.inc count; p xs)
- val v =
- (case min p_count [] s of
- [x] => if p_count [] then [] else [x]
- | m => m);
- in (v, ! count) end
+ fun binary_minimize p s =
+ case min p [] s of
+ [x] => if p [] then [] else [x]
+ | m => m
end
@@ -91,32 +91,31 @@
("# Cannot determine problem status within resource limit", Timeout),
("Error", Error)]
-fun produce_answer (result: ATP_Wrapper.prover_result) =
- let
- val {success, proof = result_string, internal_thm_names = thm_name_vec,
- filtered_clauses = filtered, ...} = result
- in
- if success then
- (Success (Vector.foldr (op ::) [] thm_name_vec, filtered), result_string)
- else
- let
- val failure = failure_strings |> get_first (fn (s, t) =>
- if String.isSubstring s result_string then SOME (t, result_string) else NONE)
- in
- (case failure of
- SOME res => res
- | NONE => (Failure, result_string))
- end
- end
+fun produce_answer ({success, proof, internal_thm_names, filtered_clauses, ...}
+ : prover_result) =
+ if success then
+ (Success (Vector.foldr (op ::) [] internal_thm_names, filtered_clauses),
+ proof)
+ else
+ let
+ val failure = failure_strings |> get_first (fn (s, t) =>
+ if String.isSubstring s proof then SOME (t, proof) else NONE)
+ in
+ (case failure of
+ SOME res => res
+ | NONE => (Failure, proof))
+ end
(* wrapper for calling external prover *)
-fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs =
+fun sledgehammer_test_theorems prover time_limit subgoalno state filtered
+ name_thms_pairs =
let
- val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
+ val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
+ " theorems... ")
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
- val axclauses = Sledgehammer_Fact_Preprocessor.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
+ val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
{with_full_types = ! ATP_Manager.full_types,
@@ -126,20 +125,19 @@
filtered_clauses = filtered}
val (result, proof) = produce_answer (prover time_limit problem)
val _ = priority (string_of_result result)
- in
- (result, proof)
- end
+ in (result, proof) end
(* minimalization of thms *)
-fun gen_minimalize gen_min prover prover_name time_limit state name_thms_pairs =
+fun minimize_theorems gen_min prover prover_name time_limit state
+ name_thms_pairs =
let
val _ =
priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
" theorems, prover: " ^ prover_name ^
", time limit: " ^ string_of_int time_limit ^ " seconds")
- val test_thms_fun = sh_test_thms prover time_limit 1 state
+ val test_thms_fun = sledgehammer_test_theorems prover time_limit 1 state
fun test_thms filtered thms =
case test_thms_fun filtered thms of (Success _, _) => true | _ => false
in
@@ -152,15 +150,14 @@
if length ordered_used < length name_thms_pairs then
filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
else name_thms_pairs
- val (min_thms, n) =
- if null to_use then ([], 0)
+ val min_thms =
+ if null to_use then []
else gen_min (test_thms (SOME filtered)) to_use
val min_names = sort_distinct string_ord (map fst min_thms)
val _ = priority (cat_lines
- ["Iterations: " ^ string_of_int n (* FIXME TN remove later *),
- "Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
+ ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
in
- (SOME (min_thms, n), "Try this command: " ^
+ (SOME min_thms, "Try this command: " ^
Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
end
| (Timeout, _) =>
@@ -170,68 +167,9 @@
(NONE, "Error in prover: " ^ msg)
| (Failure, _) =>
(NONE, "Failure: No proof with the theorems supplied"))
- handle Sledgehammer_HOL_Clause.TOO_TRIVIAL =>
- (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+ handle Sledgehammer_HOL_Clause.TRIVIAL =>
+ (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg => (NONE, "Error: " ^ msg)
end
-
-(* Isar command and parsing input *)
-
-local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
-
-fun get_thms context =
- map (fn (name, interval) =>
- let
- val thmref = Facts.Named ((name, Position.none), interval)
- val ths = ProofContext.get_fact context thmref
- val name' = Facts.string_of_ref thmref
- in
- (name', ths)
- end)
-
-val default_prover = "remote_vampire"
-val default_time_limit = 5
-
-fun get_time_limit_arg time_string =
- (case Int.fromString time_string of
- SOME t => t
- | NONE => error ("Invalid time limit: " ^ quote time_string))
-
-fun get_opt (name, a) (p, t) =
- (case name of
- "time" => (p, get_time_limit_arg a)
- | "atp" => (a, t)
- | n => error ("Invalid argument: " ^ n))
-
-fun get_options args = fold get_opt args (default_prover, default_time_limit)
-
-val minimize = gen_minimalize lin_gen_minimize
-
-val minimalize = gen_minimalize minimal
-
-fun sh_min_command args thm_names state =
- let
- val (prover_name, time_limit) = get_options args
- val prover =
- (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
- SOME prover => prover
- | NONE => error ("Unknown prover: " ^ quote prover_name))
- val name_thms_pairs = get_thms (Proof.context_of state) thm_names
- in
- writeln (#2 (minimize prover prover_name time_limit state name_thms_pairs))
- end
-
-val parse_args =
- Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
-val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
-
-val _ =
- OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
- (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
- Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of)))
-
-end
-
-end
+end;
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Mar 22 13:48:15 2010 +0100
@@ -6,54 +6,24 @@
signature ATP_WRAPPER =
sig
- (*hooks for problem files*)
- val destdir: string Config.T
- val problem_prefix: string Config.T
- val measure_runtime: bool Config.T
- val setup: theory -> theory
+ type prover = ATP_Manager.prover
- (*prover configuration, problem format, and prover result*)
- type prover_config =
- {command: Path.T,
- arguments: int -> string,
- max_new_clauses: int,
- insert_theory_const: bool,
- emit_structured_proof: bool}
- type problem =
- {with_full_types: bool,
- subgoal: int,
- goal: Proof.context * (thm list * thm),
- axiom_clauses: (thm * (string * int)) list option,
- filtered_clauses: (thm * (string * int)) list option}
- val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
- type prover_result =
- {success: bool,
- message: string,
- theorem_names: string list,
- runtime: int,
- proof: string,
- internal_thm_names: string Vector.vector,
- filtered_clauses: (thm * (string * int)) list}
- type prover = int -> problem -> prover_result
+ (* hooks for problem files *)
+ val destdir : string Config.T
+ val problem_prefix : string Config.T
+ val measure_runtime : bool Config.T
- (*common provers*)
- val vampire: string * prover
- val vampire_full: string * prover
- val eprover: string * prover
- val eprover_full: string * prover
- val spass: string * prover
- val spass_no_tc: string * prover
- val remote_vampire: string * prover
- val remote_eprover: string * prover
- val remote_spass: string * prover
- val refresh_systems: unit -> unit
+ val refresh_systems_on_tptp : unit -> unit
+ val setup : theory -> theory
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
+open ATP_Manager
(** generic ATP wrapper **)
@@ -68,43 +38,17 @@
val (measure_runtime, measure_runtime_setup) =
Attrib.config_bool "atp_measure_runtime" false;
-val setup = destdir_setup #> problem_prefix_setup #> measure_runtime_setup;
-
-(* prover configuration, problem format, and prover result *)
+(* prover configuration *)
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};
-type problem =
- {with_full_types: bool,
- subgoal: int,
- goal: Proof.context * (thm list * thm),
- axiom_clauses: (thm * (string * int)) list option,
- filtered_clauses: (thm * (string * int)) list option};
-
-fun problem_of_goal with_full_types subgoal goal : problem =
- {with_full_types = with_full_types,
- subgoal = subgoal,
- goal = goal,
- axiom_clauses = NONE,
- filtered_clauses = NONE};
-
-type prover_result =
- {success: bool,
- message: string,
- theorem_names: string list, (*relevant theorems*)
- runtime: int, (*user time of the ATP, in milliseconds*)
- proof: string,
- internal_thm_names: string Vector.vector,
- filtered_clauses: (thm * (string * int)) list};
-
-type prover = int -> problem -> prover_result;
-
(* basic template *)
@@ -114,13 +58,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 +135,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 +151,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,40 +169,51 @@
(*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;
-fun vampire_prover_config full : prover_config =
+fun vampire_prover_config isar : prover_config =
{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};
+ emit_structured_proof = isar};
val vampire = tptp_prover ("vampire", vampire_prover_config false);
-val vampire_full = tptp_prover ("vampire_full", vampire_prover_config true);
+val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
(* 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;
-fun eprover_config full : prover_config =
+fun eprover_config isar : prover_config =
{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};
+ emit_structured_proof = isar};
val eprover = tptp_prover ("e", eprover_config false);
-val eprover_full = tptp_prover ("e_full", eprover_config true);
+val eprover_isar = tptp_prover ("e_isar", eprover_config true);
(* 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 +221,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);
@@ -305,7 +257,8 @@
else split_lines answer
end;
-fun refresh_systems () = Synchronized.change systems (fn _ => get_systems ());
+fun refresh_systems_on_tptp () =
+ Synchronized.change systems (fn _ => get_systems ());
fun get_system prefix = Synchronized.change_result systems (fn systems =>
(if null systems then get_systems () else systems)
@@ -316,10 +269,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};
@@ -333,4 +289,15 @@
val remote_spass = tptp_prover ("remote_spass", remote_prover_config
"SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
+val provers =
+ [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc,
+ remote_vampire, remote_spass, remote_eprover]
+val prover_setup = fold add_prover provers
+
+val setup =
+ destdir_setup
+ #> problem_prefix_setup
+ #> measure_runtime_setup
+ #> prover_setup;
+
end;
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Mar 22 13:48:15 2010 +0100
@@ -13,7 +13,7 @@
val auto: bool Unsynchronized.ref
val default_params : theory -> (string * string) list -> params
val setup : theory -> theory
-end
+end;
structure Nitpick_Isar : NITPICK_ISAR =
struct
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Mar 22 13:48:15 2010 +0100
@@ -12,7 +12,7 @@
hol_context -> (typ option * bool option) list
-> (typ option * bool option) list -> term
-> term list * term list * bool * bool * bool
-end
+end;
structure Nitpick_Preproc : NITPICK_PREPROC =
struct
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Mar 22 13:48:15 2010 +0100
@@ -8,7 +8,7 @@
signature NITPICK_TESTS =
sig
val run_all_tests : unit -> unit
-end
+end;
structure Nitpick_Tests =
struct
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Mar 22 13:48:15 2010 +0100
@@ -62,7 +62,7 @@
val pstrs : string -> Pretty.T list
val unyxml : string -> string
val maybe_quote : string -> string
-end
+end;
structure Nitpick_Util : NITPICK_UTIL =
struct
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Mon Mar 22 13:48:15 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 Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Mar 22 13:48:15 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 Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Mar 22 13:48:15 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 Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Mar 22 13:48:15 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,49 +458,13 @@
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 =
EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
-val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
+val neg_clausify =
+ Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf;
fun neg_conjecture_clauses ctxt st0 n =
let
@@ -534,11 +501,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 Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Mar 22 13:48:15 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 Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Mar 22 13:48:15 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;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 22 13:48:15 2010 +0100
@@ -0,0 +1,87 @@
+(* Title: HOL/Sledgehammer/sledgehammer_isar.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
+*)
+
+structure Sledgehammer_Isar : sig end =
+struct
+
+open ATP_Manager
+open ATP_Minimal
+
+structure K = OuterKeyword and P = OuterParse
+
+val _ =
+ OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
+
+val _ =
+ OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
+
+val _ =
+ OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
+ (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
+ (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
+
+val _ =
+ OuterSyntax.improper_command "print_atps" "print external provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+ Toplevel.keep (print_provers o Toplevel.theory_of)));
+
+val _ =
+ OuterSyntax.command "sledgehammer"
+ "search for first-order proof using automatic theorem provers" K.diag
+ (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
+ Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
+
+val default_minimize_prover = "remote_vampire"
+val default_minimize_time_limit = 5
+
+fun atp_minimize_command args thm_names state =
+ let
+ fun theorems_from_names ctxt =
+ map (fn (name, interval) =>
+ let
+ val thmref = Facts.Named ((name, Position.none), interval)
+ val ths = ProofContext.get_fact ctxt thmref
+ val name' = Facts.string_of_ref thmref
+ in (name', ths) end)
+ fun get_time_limit_arg time_string =
+ (case Int.fromString time_string of
+ SOME t => t
+ | NONE => error ("Invalid time limit: " ^ quote time_string))
+ fun get_opt (name, a) (p, t) =
+ (case name of
+ "time" => (p, get_time_limit_arg a)
+ | "atp" => (a, t)
+ | n => error ("Invalid argument: " ^ n))
+ fun get_options args =
+ fold get_opt args (default_minimize_prover, default_minimize_time_limit)
+ val (prover_name, time_limit) = get_options args
+ val prover =
+ (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
+ SOME prover => prover
+ | NONE => error ("Unknown prover: " ^ quote prover_name))
+ val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
+ in
+ writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
+ state name_thms_pairs))
+ end
+
+local structure K = OuterKeyword and P = OuterParse in
+
+val parse_args =
+ Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
+val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
+
+val _ =
+ OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
+ (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
+ Toplevel.no_timing o Toplevel.unknown_proof o
+ Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
+
+end
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Mar 22 13:48:15 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;
@@ -340,26 +333,30 @@
then SOME ctm else perm ctms
in perm end;
-fun have_or_show "show " _ = "show \""
- | have_or_show have lname = have ^ lname ^ ": \""
-
(*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
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")
- 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"
- | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n") (*no match!!*)
- | doline have (lname, t, deps) =
- have_or_show have lname ^ string_of (gen_all_vars (HOLogic.mk_Trueprop t)) ^
- "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
- fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
- | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
- in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) dolines end;
+fun isar_proof_body ctxt ctms =
+ let
+ val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
+ val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt)
+ fun have_or_show "show" _ = "show \""
+ | have_or_show have lname = have ^ " " ^ lname ^ ": \""
+ fun do_line _ (lname, t, []) =
+ (* No deps: it's a conjecture clause, with no proof. *)
+ (case permuted_clause t ctms of
+ SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
+ | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
+ [t]))
+ | do_line have (lname, t, deps) =
+ have_or_show have lname ^
+ string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^
+ "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
+ fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
+ | do_lines ((lname, t, deps) :: lines) =
+ do_line "have" (lname, t, deps) :: do_lines lines
+ in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) do_lines end;
-fun notequal t (_,t',_) = not (t aconv t');
+fun unequal t (_, t', _) = not (t aconv t');
(*No "real" literals means only type information*)
fun eq_types t = t aconv HOLogic.true_const;
@@ -375,7 +372,7 @@
if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*)
then map (replace_deps (lno, [])) lines
else
- (case take_prefix (notequal t) lines of
+ (case take_prefix (unequal t) lines of
(_,[]) => lines (*no repetition of proof line*)
| (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*)
pre @ map (replace_deps (lno', [lno])) post)
@@ -385,7 +382,7 @@
if eq_types t then (lno, t, deps) :: lines
(*Type information will be deleted later; skip repetition test.*)
else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
- case take_prefix (notequal t) lines of
+ case take_prefix (unequal t) lines of
(_,[]) => (lno, t, deps) :: lines (*no repetition of proof line*)
| (pre, (lno', t', _) :: post) =>
(lno, t', deps) :: (*repetition: replace later line by earlier one*)
@@ -399,7 +396,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.
@@ -435,39 +432,42 @@
fun isar_header [] = proofstart
| 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"
- val tuples = map (dest_tstp o tstp_line o explode) cnfs
- val _ = trace (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 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 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 ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
- val _ = trace "\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?)";
+fun isar_proof_from_tstp_file cnfs ctxt th sgno thm_names =
+ let
+ val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n")
+ val tuples = map (dest_tstp o tstp_line o explode) cnfs
+ 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_proof_msg (fn () =>
+ Int.toString (length raw_lines) ^ " raw_lines extracted\n")
+ val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
+ 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 _ = app (fn th => trace_proof_msg
+ (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
+ val body = isar_proof_body ctxt (map prop_of ccls)
+ (stringify_deps thm_names [] lines)
+ val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
+ in isar_header (map #1 fixes) ^ implode body ^ "qed\n" end
+ handle STREE _ => error "Could not extract proof (ATP output malformed?)";
(*=== 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 +475,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 +484,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 +515,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 ^ ")"
@@ -555,34 +541,37 @@
(* atp_minimize [atp=<prover>] <lemmas> *)
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))
-
-fun sendback_metis_nochained lemmas =
- (Markup.markup Markup.sendback o metis_line) (nochained lemmas)
+ Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
+ space_implode " " (kill_chained lemmas))
-fun 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)
+fun metis_lemma_list dfg name result =
+ let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
+ (Markup.markup Markup.sendback (metis_line (kill_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 tokens = String.tokens (fn c => c = #" ") one_line_proof
+ val isar_proof =
+ if member (op =) tokens chained_hint then ""
+ else isar_proof_from_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 isar_proof,
+ lemma_names)
+ end
end;
--- a/src/HOL/Tools/lin_arith.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML Mon Mar 22 13:48:15 2010 +0100
@@ -22,7 +22,6 @@
val global_setup: theory -> theory
val split_limit: int Config.T
val neq_limit: int Config.T
- val warning_count: int Unsynchronized.ref
val trace: bool Unsynchronized.ref
end;
@@ -797,7 +796,6 @@
fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
val lin_arith_tac = Fast_Arith.lin_arith_tac;
val trace = Fast_Arith.trace;
-val warning_count = Fast_Arith.warning_count;
(* reduce contradictory <= to False.
Most of the work is done by the cancel tactics. *)
--- a/src/HOL/Tools/meson.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/meson.ML Mon Mar 22 13:48:15 2010 +0100
@@ -18,6 +18,7 @@
val make_nnf: Proof.context -> thm -> thm
val skolemize: Proof.context -> thm -> thm
val is_fol_term: theory -> term -> bool
+ val make_clauses_unsorted: thm list -> thm list
val make_clauses: thm list -> thm list
val make_horns: thm list -> thm list
val best_prolog_tac: (thm -> int) -> thm list -> tactic
@@ -560,7 +561,8 @@
(*Make clauses from a list of theorems, previously Skolemized and put into nnf.
The resulting clauses are HOL disjunctions.*)
-fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []);
+fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
+val make_clauses = sort_clauses o make_clauses_unsorted;
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
fun make_horns ths =
--- a/src/Provers/Arith/fast_lin_arith.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Mon Mar 22 13:48:15 2010 +0100
@@ -96,7 +96,6 @@
number_of : serial * (theory -> typ -> int -> cterm)})
-> Context.generic -> Context.generic
val trace: bool Unsynchronized.ref
- val warning_count: int Unsynchronized.ref;
end;
functor Fast_Lin_Arith
@@ -426,9 +425,6 @@
fun trace_msg msg =
if !trace then tracing msg else ();
-val warning_count = Unsynchronized.ref 0;
-val warning_count_max = 10;
-
val union_term = union Pattern.aeconv;
val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'));
@@ -532,17 +528,11 @@
val _ =
if LA_Logic.is_False fls then ()
else
- let val count = CRITICAL (fn () => Unsynchronized.inc warning_count) in
- if count > warning_count_max then ()
- else
- (tracing (cat_lines
- (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
- ["Proved:", Display.string_of_thm ctxt fls, ""] @
- (if count <> warning_count_max then []
- else ["\n(Reached maximal message count -- disabling future warnings)"])));
- warning "Linear arithmetic should have refuted the assumptions.\n\
- \Please inform Tobias Nipkow (nipkow@in.tum.de).")
- end;
+ (tracing (cat_lines
+ (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
+ ["Proved:", Display.string_of_thm ctxt fls, ""]));
+ warning "Linear arithmetic should have refuted the assumptions.\n\
+ \Please inform Tobias Nipkow.")
in fls end
handle FalseE thm => trace_thm ctxt "False reached early:" thm
end;
--- a/src/Pure/Isar/class_target.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/Pure/Isar/class_target.ML Mon Mar 22 13:48:15 2010 +0100
@@ -16,12 +16,13 @@
val rules: theory -> class -> thm option * thm
val these_params: theory -> sort -> (string * (class * (string * typ))) list
val these_defs: theory -> sort -> thm list
- val these_operations: theory -> sort -> (string * (class * (typ * term))) list
+ val these_operations: theory -> sort
+ -> (string * (class * (typ * term))) list
val print_classes: theory -> unit
val begin: class list -> sort -> Proof.context -> Proof.context
val init: class -> theory -> Proof.context
- val declare: class -> (binding * mixfix) * term -> theory -> theory
+ val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory
val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
val class_prefix: string -> string
val refresh_syntax: class -> Proof.context -> Proof.context
@@ -253,8 +254,8 @@
(* class context syntax *)
-fun these_unchecks thy =
- map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
+fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
+ o these_operations thy;
fun redeclare_const thy c =
let val b = Long_Name.base_name c
@@ -317,15 +318,15 @@
val class_prefix = Logic.const_of_class o Long_Name.base_name;
-fun declare class ((c, mx), dict) thy =
+fun declare class ((c, mx), (type_params, dict)) thy =
let
val morph = morphism thy class;
val b = Morphism.binding morph c;
val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b);
val c' = Sign.full_name thy b;
val dict' = Morphism.term morph dict;
- val ty' = Term.fastype_of dict';
- val def_eq = Logic.mk_equals (Const (c', ty'), dict')
+ val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict';
+ val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict')
|> map_types Type.strip_sorts;
in
thy
@@ -335,7 +336,7 @@
|>> Thm.varifyT_global
|-> (fn def_thm => PureThy.store_thm (b_def, def_thm)
#> snd
- #> register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
+ #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
|> Sign.add_const_constraint (c', SOME ty')
end;
--- a/src/Pure/Isar/overloading.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/Pure/Isar/overloading.ML Mon Mar 22 13:48:15 2010 +0100
@@ -13,7 +13,7 @@
val define: bool -> binding -> string * term -> theory -> thm * theory
val operation: Proof.context -> binding -> (string * bool) option
val pretty: Proof.context -> Pretty.T
-
+
type improvable_syntax
val add_improvable_syntax: Proof.context -> Proof.context
val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
--- a/src/Pure/Isar/theory_target.ML Mon Mar 22 08:30:13 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML Mon Mar 22 13:48:15 2010 +0100
@@ -277,7 +277,7 @@
in
lthy'
|> is_locale ? syntax_declaration ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
- |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
+ |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), (type_params, t)))
|> Local_Defs.add_def ((b, NoSyn), t)
end;