1.1 --- a/src/HOL/IsaMakefile Mon Mar 22 09:54:22 2010 +0100
1.2 +++ b/src/HOL/IsaMakefile Mon Mar 22 10:25:44 2010 +0100
1.3 @@ -314,11 +314,13 @@
1.4 Tools/Quotient/quotient_term.ML \
1.5 Tools/Quotient/quotient_typ.ML \
1.6 Tools/recdef.ML \
1.7 + Tools/Sledgehammer/meson_tactic.ML \
1.8 Tools/Sledgehammer/metis_tactics.ML \
1.9 Tools/Sledgehammer/sledgehammer_fact_filter.ML \
1.10 Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \
1.11 Tools/Sledgehammer/sledgehammer_fol_clause.ML \
1.12 Tools/Sledgehammer/sledgehammer_hol_clause.ML \
1.13 + Tools/Sledgehammer/sledgehammer_isar.ML \
1.14 Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
1.15 Tools/string_code.ML \
1.16 Tools/string_syntax.ML \
2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Mar 22 09:54:22 2010 +0100
2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Mar 22 10:25:44 2010 +0100
2.3 @@ -42,8 +42,7 @@
2.4
2.5 datatype min_data = MinData of {
2.6 succs: int,
2.7 - ab_ratios: int,
2.8 - it_ratios: int
2.9 + ab_ratios: int
2.10 }
2.11
2.12 fun make_sh_data
2.13 @@ -51,8 +50,8 @@
2.14 ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems,
2.15 time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail}
2.16
2.17 -fun make_min_data (succs, ab_ratios, it_ratios) =
2.18 - MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios}
2.19 +fun make_min_data (succs, ab_ratios) =
2.20 + MinData{succs=succs, ab_ratios=ab_ratios}
2.21
2.22 fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) =
2.23 MeData{calls=calls, success=success, proofs=proofs, time=time,
2.24 @@ -66,8 +65,7 @@
2.25 time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa,
2.26 time_atp, time_atp_fail)
2.27
2.28 -fun tuple_of_min_data (MinData {succs, ab_ratios, it_ratios}) =
2.29 - (succs, ab_ratios, it_ratios)
2.30 +fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
2.31
2.32 fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas,
2.33 posns}) = (calls, success, proofs, time, timeout, lemmas, posns)
2.34 @@ -147,13 +145,10 @@
2.35 => (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail + t))
2.36
2.37 val inc_min_succs = map_min_data
2.38 - (fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios))
2.39 + (fn (succs,ab_ratios) => (succs+1, ab_ratios))
2.40
2.41 fun inc_min_ab_ratios r = map_min_data
2.42 - (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios))
2.43 -
2.44 -fun inc_min_it_ratios r = map_min_data
2.45 - (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r))
2.46 + (fn (succs, ab_ratios) => (succs, ab_ratios+r))
2.47
2.48 val inc_metis_calls = map_me_data
2.49 (fn (calls,success,proofs,time,timeout,lemmas,posns)
2.50 @@ -234,10 +229,9 @@
2.51 else ()
2.52 )
2.53
2.54 -fun log_min_data log (succs, ab_ratios, it_ratios) =
2.55 +fun log_min_data log (succs, ab_ratios) =
2.56 (log ("Number of successful minimizations: " ^ string_of_int succs);
2.57 - log ("After/before ratios: " ^ string_of_int ab_ratios);
2.58 - log ("Iterations ratios: " ^ string_of_int it_ratios)
2.59 + log ("After/before ratios: " ^ string_of_int ab_ratios)
2.60 )
2.61
2.62 in
2.63 @@ -313,13 +307,13 @@
2.64 ctxt
2.65 |> change_dir dir
2.66 |> Config.put ATP_Wrapper.measure_runtime true
2.67 - val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
2.68 + val problem = ATP_Manager.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
2.69
2.70 val time_limit =
2.71 (case hard_timeout of
2.72 NONE => I
2.73 | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
2.74 - val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Wrapper.prover_result,
2.75 + val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Manager.prover_result,
2.76 time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
2.77 in
2.78 if success then (message, SH_OK (time_isa, time_atp, theorem_names))
2.79 @@ -380,9 +374,10 @@
2.80
2.81 fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
2.82 let
2.83 + open ATP_Minimal
2.84 val n0 = length (these (!named_thms))
2.85 val (prover_name, prover) = get_atp (Proof.theory_of st) args
2.86 - val minimize = ATP_Minimal.minimalize prover prover_name
2.87 + val minimize = minimize_theorems linear_minimize prover prover_name
2.88 val timeout =
2.89 AList.lookup (op =) args minimize_timeoutK
2.90 |> Option.map (fst o read_int o explode)
2.91 @@ -393,7 +388,6 @@
2.92 (SOME (named_thms',its), msg) =>
2.93 (change_data id inc_min_succs;
2.94 change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
2.95 - change_data id (inc_min_it_ratios ((100*its) div n0));
2.96 if length named_thms' = n0
2.97 then log (minimize_tag id ^ "already minimal")
2.98 else (named_thms := SOME named_thms';
3.1 --- a/src/HOL/Sledgehammer.thy Mon Mar 22 09:54:22 2010 +0100
3.2 +++ b/src/HOL/Sledgehammer.thy Mon Mar 22 10:25:44 2010 +0100
3.3 @@ -1,7 +1,8 @@
3.4 (* Title: HOL/Sledgehammer.thy
3.5 Author: Lawrence C Paulson
3.6 Author: Jia Meng, NICTA
3.7 - Author: Fabian Immler, TUM
3.8 + Author: Fabian Immler, TU Muenchen
3.9 + Author: Jasmin Blanchette, TU Muenchen
3.10 *)
3.11
3.12 header {* Sledgehammer: Isabelle--ATP Linkup *}
3.13 @@ -10,7 +11,8 @@
3.14 imports Plain Hilbert_Choice
3.15 uses
3.16 "Tools/polyhash.ML"
3.17 - "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
3.18 + "~~/src/Tools/Metis/metis.ML"
3.19 + ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
3.20 ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
3.21 ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
3.22 ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
3.23 @@ -18,71 +20,72 @@
3.24 ("Tools/ATP_Manager/atp_manager.ML")
3.25 ("Tools/ATP_Manager/atp_wrapper.ML")
3.26 ("Tools/ATP_Manager/atp_minimal.ML")
3.27 - "~~/src/Tools/Metis/metis.ML"
3.28 + ("Tools/Sledgehammer/sledgehammer_isar.ML")
3.29 + ("Tools/Sledgehammer/meson_tactic.ML")
3.30 ("Tools/Sledgehammer/metis_tactics.ML")
3.31 begin
3.32
3.33 -definition COMBI :: "'a => 'a"
3.34 - where "COMBI P == P"
3.35 +definition COMBI :: "'a \<Rightarrow> 'a"
3.36 + where "COMBI P \<equiv> P"
3.37
3.38 -definition COMBK :: "'a => 'b => 'a"
3.39 - where "COMBK P Q == P"
3.40 +definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
3.41 + where "COMBK P Q \<equiv> P"
3.42
3.43 -definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
3.44 - where "COMBB P Q R == P (Q R)"
3.45 +definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
3.46 + where "COMBB P Q R \<equiv> P (Q R)"
3.47
3.48 -definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
3.49 - where "COMBC P Q R == P R Q"
3.50 +definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
3.51 + where "COMBC P Q R \<equiv> P R Q"
3.52
3.53 -definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
3.54 - where "COMBS P Q R == P R (Q R)"
3.55 +definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
3.56 + where "COMBS P Q R \<equiv> P R (Q R)"
3.57
3.58 -definition fequal :: "'a => 'a => bool"
3.59 - where "fequal X Y == (X=Y)"
3.60 +definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
3.61 + where "fequal X Y \<equiv> (X = Y)"
3.62
3.63 -lemma fequal_imp_equal: "fequal X Y ==> X=Y"
3.64 +lemma fequal_imp_equal: "fequal X Y \<Longrightarrow> X = Y"
3.65 by (simp add: fequal_def)
3.66
3.67 -lemma equal_imp_fequal: "X=Y ==> fequal X Y"
3.68 +lemma equal_imp_fequal: "X = Y \<Longrightarrow> fequal X Y"
3.69 by (simp add: fequal_def)
3.70
3.71 text{*These two represent the equivalence between Boolean equality and iff.
3.72 They can't be converted to clauses automatically, as the iff would be
3.73 expanded...*}
3.74
3.75 -lemma iff_positive: "P | Q | P=Q"
3.76 +lemma iff_positive: "P \<or> Q \<or> P = Q"
3.77 by blast
3.78
3.79 -lemma iff_negative: "~P | ~Q | P=Q"
3.80 +lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
3.81 by blast
3.82
3.83 text{*Theorems for translation to combinators*}
3.84
3.85 -lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
3.86 +lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
3.87 apply (rule eq_reflection)
3.88 apply (rule ext)
3.89 apply (simp add: COMBS_def)
3.90 done
3.91
3.92 -lemma abs_I: "(%x. x) == COMBI"
3.93 +lemma abs_I: "\<lambda>x. x \<equiv> COMBI"
3.94 apply (rule eq_reflection)
3.95 apply (rule ext)
3.96 apply (simp add: COMBI_def)
3.97 done
3.98
3.99 -lemma abs_K: "(%x. y) == COMBK y"
3.100 +lemma abs_K: "\<lambda>x. y \<equiv> COMBK y"
3.101 apply (rule eq_reflection)
3.102 apply (rule ext)
3.103 apply (simp add: COMBK_def)
3.104 done
3.105
3.106 -lemma abs_B: "(%x. a (g x)) == COMBB a g"
3.107 +lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g"
3.108 apply (rule eq_reflection)
3.109 apply (rule ext)
3.110 apply (simp add: COMBB_def)
3.111 done
3.112
3.113 -lemma abs_C: "(%x. (f x) b) == COMBC f b"
3.114 +lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b"
3.115 apply (rule eq_reflection)
3.116 apply (rule ext)
3.117 apply (simp add: COMBC_def)
3.118 @@ -91,35 +94,24 @@
3.119
3.120 subsection {* Setup of external ATPs *}
3.121
3.122 +use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
3.123 use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
3.124 setup Sledgehammer_Fact_Preprocessor.setup
3.125 use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
3.126 use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
3.127 setup Sledgehammer_Proof_Reconstruct.setup
3.128 use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
3.129 -
3.130 +use "Tools/ATP_Manager/atp_manager.ML"
3.131 use "Tools/ATP_Manager/atp_wrapper.ML"
3.132 setup ATP_Wrapper.setup
3.133 -use "Tools/ATP_Manager/atp_manager.ML"
3.134 use "Tools/ATP_Manager/atp_minimal.ML"
3.135 +use "Tools/Sledgehammer/sledgehammer_isar.ML"
3.136
3.137 -text {* basic provers *}
3.138 -setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
3.139 -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
3.140 -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
3.141
3.142 -text {* provers with stuctured output *}
3.143 -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
3.144 -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
3.145 +subsection {* The MESON prover *}
3.146
3.147 -text {* on some problems better results *}
3.148 -setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
3.149 -
3.150 -text {* remote provers via SystemOnTPTP *}
3.151 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
3.152 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
3.153 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
3.154 -
3.155 +use "Tools/Sledgehammer/meson_tactic.ML"
3.156 +setup Meson_Tactic.setup
3.157
3.158
3.159 subsection {* The Metis prover *}
4.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 22 09:54:22 2010 +0100
4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 22 10:25:44 2010 +0100
4.3 @@ -7,6 +7,23 @@
4.4
4.5 signature ATP_MANAGER =
4.6 sig
4.7 + type problem =
4.8 + {with_full_types: bool,
4.9 + subgoal: int,
4.10 + goal: Proof.context * (thm list * thm),
4.11 + axiom_clauses: (thm * (string * int)) list option,
4.12 + filtered_clauses: (thm * (string * int)) list option}
4.13 + val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
4.14 + type prover_result =
4.15 + {success: bool,
4.16 + message: string,
4.17 + theorem_names: string list,
4.18 + runtime: int,
4.19 + proof: string,
4.20 + internal_thm_names: string Vector.vector,
4.21 + filtered_clauses: (thm * (string * int)) list}
4.22 + type prover = int -> problem -> prover_result
4.23 +
4.24 val atps: string Unsynchronized.ref
4.25 val get_atps: unit -> string list
4.26 val timeout: int Unsynchronized.ref
4.27 @@ -14,15 +31,43 @@
4.28 val kill: unit -> unit
4.29 val info: unit -> unit
4.30 val messages: int option -> unit
4.31 - val add_prover: string * ATP_Wrapper.prover -> theory -> theory
4.32 - val get_prover: theory -> string -> ATP_Wrapper.prover option
4.33 + val add_prover: string * prover -> theory -> theory
4.34 + val get_prover: theory -> string -> prover option
4.35 val print_provers: theory -> unit
4.36 val sledgehammer: string list -> Proof.state -> unit
4.37 end;
4.38
4.39 -structure ATP_Manager: ATP_MANAGER =
4.40 +structure ATP_Manager : ATP_MANAGER =
4.41 struct
4.42
4.43 +(** problems, results, and provers **)
4.44 +
4.45 +type problem =
4.46 + {with_full_types: bool,
4.47 + subgoal: int,
4.48 + goal: Proof.context * (thm list * thm),
4.49 + axiom_clauses: (thm * (string * int)) list option,
4.50 + filtered_clauses: (thm * (string * int)) list option};
4.51 +
4.52 +fun problem_of_goal with_full_types subgoal goal : problem =
4.53 + {with_full_types = with_full_types,
4.54 + subgoal = subgoal,
4.55 + goal = goal,
4.56 + axiom_clauses = NONE,
4.57 + filtered_clauses = NONE};
4.58 +
4.59 +type prover_result =
4.60 + {success: bool,
4.61 + message: string,
4.62 + theorem_names: string list, (*relevant theorems*)
4.63 + runtime: int, (*user time of the ATP, in milliseconds*)
4.64 + proof: string,
4.65 + internal_thm_names: string Vector.vector,
4.66 + filtered_clauses: (thm * (string * int)) list};
4.67 +
4.68 +type prover = int -> problem -> prover_result;
4.69 +
4.70 +
4.71 (** preferences **)
4.72
4.73 val message_store_limit = 20;
4.74 @@ -228,7 +273,7 @@
4.75
4.76 structure Provers = Theory_Data
4.77 (
4.78 - type T = (ATP_Wrapper.prover * stamp) Symtab.table;
4.79 + type T = (prover * stamp) Symtab.table;
4.80 val empty = Symtab.empty;
4.81 val extend = I;
4.82 fun merge data : T = Symtab.merge (eq_snd op =) data
4.83 @@ -261,9 +306,9 @@
4.84 val _ = Toplevel.thread true (fn () =>
4.85 let
4.86 val _ = register birth_time death_time (Thread.self (), desc);
4.87 - val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
4.88 + val problem = problem_of_goal (! full_types) i (ctxt, (facts, goal));
4.89 val message = #message (prover (! timeout) problem)
4.90 - handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => (* FIXME !? *)
4.91 + handle Sledgehammer_HOL_Clause.TRIVIAL => (* FIXME !? *)
4.92 "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
4.93 | ERROR msg => ("Error: " ^ msg);
4.94 val _ = unregister message (Thread.self ());
4.95 @@ -282,36 +327,4 @@
4.96 val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers;
4.97 in () end;
4.98
4.99 -
4.100 -
4.101 -(** Isar command syntax **)
4.102 -
4.103 -local structure K = OuterKeyword and P = OuterParse in
4.104 -
4.105 -val _ =
4.106 - OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
4.107 - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
4.108 -
4.109 -val _ =
4.110 - OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
4.111 - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
4.112 -
4.113 -val _ =
4.114 - OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
4.115 - (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
4.116 - (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
4.117 -
4.118 -val _ =
4.119 - OuterSyntax.improper_command "print_atps" "print external provers" K.diag
4.120 - (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
4.121 - Toplevel.keep (print_provers o Toplevel.theory_of)));
4.122 -
4.123 -val _ =
4.124 - OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
4.125 - (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
4.126 - Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
4.127 -
4.128 end;
4.129 -
4.130 -end;
4.131 -
5.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Mar 22 09:54:22 2010 +0100
5.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Mar 22 10:25:44 2010 +0100
5.3 @@ -1,32 +1,40 @@
5.4 (* Title: HOL/Tools/ATP_Manager/atp_minimal.ML
5.5 Author: Philipp Meyer, TU Muenchen
5.6
5.7 -Minimization of theorem list for metis by using an external automated theorem prover
5.8 +Minimization of theorem list for Metis using automatic theorem provers.
5.9 *)
5.10
5.11 signature ATP_MINIMAL =
5.12 sig
5.13 - val minimize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
5.14 - (string * thm list) list -> ((string * thm list) list * int) option * string
5.15 - (* To be removed once TN has finished his measurements;
5.16 - the int component of the result should then be removed: *)
5.17 - val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
5.18 - (string * thm list) list -> ((string * thm list) list * int) option * string
5.19 -end
5.20 + type prover = ATP_Manager.prover
5.21 + type prover_result = ATP_Manager.prover_result
5.22 + type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
5.23
5.24 -structure ATP_Minimal: ATP_MINIMAL =
5.25 + val linear_minimize : 'a minimize_fun
5.26 + val binary_minimize : 'a minimize_fun
5.27 + val minimize_theorems :
5.28 + (string * thm list) minimize_fun -> prover -> string -> int
5.29 + -> Proof.state -> (string * thm list) list
5.30 + -> (string * thm list) list option * string
5.31 +end;
5.32 +
5.33 +structure ATP_Minimal : ATP_MINIMAL =
5.34 struct
5.35
5.36 -(* Linear minimization *)
5.37 +open Sledgehammer_Fact_Preprocessor
5.38 +open ATP_Manager
5.39
5.40 -fun lin_gen_minimize p s =
5.41 -let
5.42 - fun min [] needed = needed
5.43 - | min (x::xs) needed =
5.44 - if p(xs @ needed) then min xs needed else min xs (x::needed)
5.45 -in (min s [], length s) end;
5.46 +type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
5.47
5.48 -(* Clever minimalization algorithm *)
5.49 +(* Linear minimization algorithm *)
5.50 +
5.51 +fun linear_minimize p s =
5.52 + let
5.53 + fun aux [] needed = needed
5.54 + | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x)
5.55 + in aux s [] end;
5.56 +
5.57 +(* Binary minimalization *)
5.58
5.59 local
5.60 fun isplit (l, r) [] = (l, r)
5.61 @@ -37,24 +45,21 @@
5.62 end
5.63
5.64 local
5.65 - fun min p sup [] = raise Empty
5.66 - | min p sup [s0] = [s0]
5.67 + fun min _ _ [] = raise Empty
5.68 + | min _ _ [s0] = [s0]
5.69 | min p sup s =
5.70 let
5.71 val (l0, r0) = split s
5.72 in
5.73 - if p (sup @ l0)
5.74 - then min p sup l0
5.75 + if p (sup @ l0) then
5.76 + min p sup l0
5.77 + else if p (sup @ r0) then
5.78 + min p sup r0
5.79 else
5.80 - if p (sup @ r0)
5.81 - then min p sup r0
5.82 - else
5.83 - let
5.84 - val l = min p (sup @ r0) l0
5.85 - val r = min p (sup @ l) r0
5.86 - in
5.87 - l @ r
5.88 - end
5.89 + let
5.90 + val l = min p (sup @ r0) l0
5.91 + val r = min p (sup @ l) r0
5.92 + in l @ r end
5.93 end
5.94 in
5.95 (* return a minimal subset v of s that satisfies p
5.96 @@ -62,15 +67,10 @@
5.97 @post v subset s & p(v) &
5.98 forall e in v. ~p(v \ e)
5.99 *)
5.100 - fun minimal p s =
5.101 - let
5.102 - val count = Unsynchronized.ref 0
5.103 - fun p_count xs = (Unsynchronized.inc count; p xs)
5.104 - val v =
5.105 - (case min p_count [] s of
5.106 - [x] => if p_count [] then [] else [x]
5.107 - | m => m);
5.108 - in (v, ! count) end
5.109 + fun binary_minimize p s =
5.110 + case min p [] s of
5.111 + [x] => if p [] then [] else [x]
5.112 + | m => m
5.113 end
5.114
5.115
5.116 @@ -91,32 +91,31 @@
5.117 ("# Cannot determine problem status within resource limit", Timeout),
5.118 ("Error", Error)]
5.119
5.120 -fun produce_answer (result: ATP_Wrapper.prover_result) =
5.121 - let
5.122 - val {success, proof = result_string, internal_thm_names = thm_name_vec,
5.123 - filtered_clauses = filtered, ...} = result
5.124 - in
5.125 - if success then
5.126 - (Success (Vector.foldr (op ::) [] thm_name_vec, filtered), result_string)
5.127 - else
5.128 - let
5.129 - val failure = failure_strings |> get_first (fn (s, t) =>
5.130 - if String.isSubstring s result_string then SOME (t, result_string) else NONE)
5.131 - in
5.132 - (case failure of
5.133 - SOME res => res
5.134 - | NONE => (Failure, result_string))
5.135 - end
5.136 - end
5.137 +fun produce_answer ({success, proof, internal_thm_names, filtered_clauses, ...}
5.138 + : prover_result) =
5.139 + if success then
5.140 + (Success (Vector.foldr (op ::) [] internal_thm_names, filtered_clauses),
5.141 + proof)
5.142 + else
5.143 + let
5.144 + val failure = failure_strings |> get_first (fn (s, t) =>
5.145 + if String.isSubstring s proof then SOME (t, proof) else NONE)
5.146 + in
5.147 + (case failure of
5.148 + SOME res => res
5.149 + | NONE => (Failure, proof))
5.150 + end
5.151
5.152
5.153 (* wrapper for calling external prover *)
5.154
5.155 -fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs =
5.156 +fun sledgehammer_test_theorems prover time_limit subgoalno state filtered
5.157 + name_thms_pairs =
5.158 let
5.159 - val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
5.160 + val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
5.161 + " theorems... ")
5.162 val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
5.163 - val axclauses = Sledgehammer_Fact_Preprocessor.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
5.164 + val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
5.165 val {context = ctxt, facts, goal} = Proof.goal state
5.166 val problem =
5.167 {with_full_types = ! ATP_Manager.full_types,
5.168 @@ -126,20 +125,19 @@
5.169 filtered_clauses = filtered}
5.170 val (result, proof) = produce_answer (prover time_limit problem)
5.171 val _ = priority (string_of_result result)
5.172 - in
5.173 - (result, proof)
5.174 - end
5.175 + in (result, proof) end
5.176
5.177
5.178 (* minimalization of thms *)
5.179
5.180 -fun gen_minimalize gen_min prover prover_name time_limit state name_thms_pairs =
5.181 +fun minimize_theorems gen_min prover prover_name time_limit state
5.182 + name_thms_pairs =
5.183 let
5.184 val _ =
5.185 priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
5.186 " theorems, prover: " ^ prover_name ^
5.187 ", time limit: " ^ string_of_int time_limit ^ " seconds")
5.188 - val test_thms_fun = sh_test_thms prover time_limit 1 state
5.189 + val test_thms_fun = sledgehammer_test_theorems prover time_limit 1 state
5.190 fun test_thms filtered thms =
5.191 case test_thms_fun filtered thms of (Success _, _) => true | _ => false
5.192 in
5.193 @@ -152,15 +150,14 @@
5.194 if length ordered_used < length name_thms_pairs then
5.195 filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
5.196 else name_thms_pairs
5.197 - val (min_thms, n) =
5.198 - if null to_use then ([], 0)
5.199 + val min_thms =
5.200 + if null to_use then []
5.201 else gen_min (test_thms (SOME filtered)) to_use
5.202 val min_names = sort_distinct string_ord (map fst min_thms)
5.203 val _ = priority (cat_lines
5.204 - ["Iterations: " ^ string_of_int n (* FIXME TN remove later *),
5.205 - "Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
5.206 + ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
5.207 in
5.208 - (SOME (min_thms, n), "Try this command: " ^
5.209 + (SOME min_thms, "Try this command: " ^
5.210 Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
5.211 end
5.212 | (Timeout, _) =>
5.213 @@ -170,68 +167,9 @@
5.214 (NONE, "Error in prover: " ^ msg)
5.215 | (Failure, _) =>
5.216 (NONE, "Failure: No proof with the theorems supplied"))
5.217 - handle Sledgehammer_HOL_Clause.TOO_TRIVIAL =>
5.218 - (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
5.219 + handle Sledgehammer_HOL_Clause.TRIVIAL =>
5.220 + (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
5.221 | ERROR msg => (NONE, "Error: " ^ msg)
5.222 end
5.223
5.224 -
5.225 -(* Isar command and parsing input *)
5.226 -
5.227 -local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
5.228 -
5.229 -fun get_thms context =
5.230 - map (fn (name, interval) =>
5.231 - let
5.232 - val thmref = Facts.Named ((name, Position.none), interval)
5.233 - val ths = ProofContext.get_fact context thmref
5.234 - val name' = Facts.string_of_ref thmref
5.235 - in
5.236 - (name', ths)
5.237 - end)
5.238 -
5.239 -val default_prover = "remote_vampire"
5.240 -val default_time_limit = 5
5.241 -
5.242 -fun get_time_limit_arg time_string =
5.243 - (case Int.fromString time_string of
5.244 - SOME t => t
5.245 - | NONE => error ("Invalid time limit: " ^ quote time_string))
5.246 -
5.247 -fun get_opt (name, a) (p, t) =
5.248 - (case name of
5.249 - "time" => (p, get_time_limit_arg a)
5.250 - | "atp" => (a, t)
5.251 - | n => error ("Invalid argument: " ^ n))
5.252 -
5.253 -fun get_options args = fold get_opt args (default_prover, default_time_limit)
5.254 -
5.255 -val minimize = gen_minimalize lin_gen_minimize
5.256 -
5.257 -val minimalize = gen_minimalize minimal
5.258 -
5.259 -fun sh_min_command args thm_names state =
5.260 - let
5.261 - val (prover_name, time_limit) = get_options args
5.262 - val prover =
5.263 - (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
5.264 - SOME prover => prover
5.265 - | NONE => error ("Unknown prover: " ^ quote prover_name))
5.266 - val name_thms_pairs = get_thms (Proof.context_of state) thm_names
5.267 - in
5.268 - writeln (#2 (minimize prover prover_name time_limit state name_thms_pairs))
5.269 - end
5.270 -
5.271 -val parse_args =
5.272 - Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
5.273 -val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
5.274 -
5.275 -val _ =
5.276 - OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
5.277 - (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
5.278 - Toplevel.no_timing o Toplevel.unknown_proof o
5.279 - Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of)))
5.280 -
5.281 -end
5.282 -
5.283 -end
5.284 +end;
6.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Mar 22 09:54:22 2010 +0100
6.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Mar 22 10:25:44 2010 +0100
6.3 @@ -6,54 +6,24 @@
6.4
6.5 signature ATP_WRAPPER =
6.6 sig
6.7 - (*hooks for problem files*)
6.8 - val destdir: string Config.T
6.9 - val problem_prefix: string Config.T
6.10 - val measure_runtime: bool Config.T
6.11 - val setup: theory -> theory
6.12 + type prover = ATP_Manager.prover
6.13
6.14 - (*prover configuration, problem format, and prover result*)
6.15 - type prover_config =
6.16 - {command: Path.T,
6.17 - arguments: int -> string,
6.18 - max_new_clauses: int,
6.19 - insert_theory_const: bool,
6.20 - emit_structured_proof: bool}
6.21 - type problem =
6.22 - {with_full_types: bool,
6.23 - subgoal: int,
6.24 - goal: Proof.context * (thm list * thm),
6.25 - axiom_clauses: (thm * (string * int)) list option,
6.26 - filtered_clauses: (thm * (string * int)) list option}
6.27 - val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
6.28 - type prover_result =
6.29 - {success: bool,
6.30 - message: string,
6.31 - theorem_names: string list,
6.32 - runtime: int,
6.33 - proof: string,
6.34 - internal_thm_names: string Vector.vector,
6.35 - filtered_clauses: (thm * (string * int)) list}
6.36 - type prover = int -> problem -> prover_result
6.37 + (* hooks for problem files *)
6.38 + val destdir : string Config.T
6.39 + val problem_prefix : string Config.T
6.40 + val measure_runtime : bool Config.T
6.41
6.42 - (*common provers*)
6.43 - val vampire: string * prover
6.44 - val vampire_full: string * prover
6.45 - val eprover: string * prover
6.46 - val eprover_full: string * prover
6.47 - val spass: string * prover
6.48 - val spass_no_tc: string * prover
6.49 - val remote_vampire: string * prover
6.50 - val remote_eprover: string * prover
6.51 - val remote_spass: string * prover
6.52 - val refresh_systems: unit -> unit
6.53 + val refresh_systems_on_tptp : unit -> unit
6.54 + val setup : theory -> theory
6.55 end;
6.56
6.57 -structure ATP_Wrapper: ATP_WRAPPER =
6.58 +structure ATP_Wrapper : ATP_WRAPPER =
6.59 struct
6.60
6.61 -structure SFF = Sledgehammer_Fact_Filter
6.62 -structure SPR = Sledgehammer_Proof_Reconstruct
6.63 +open Sledgehammer_HOL_Clause
6.64 +open Sledgehammer_Fact_Filter
6.65 +open Sledgehammer_Proof_Reconstruct
6.66 +open ATP_Manager
6.67
6.68 (** generic ATP wrapper **)
6.69
6.70 @@ -68,43 +38,17 @@
6.71 val (measure_runtime, measure_runtime_setup) =
6.72 Attrib.config_bool "atp_measure_runtime" false;
6.73
6.74 -val setup = destdir_setup #> problem_prefix_setup #> measure_runtime_setup;
6.75
6.76 -
6.77 -(* prover configuration, problem format, and prover result *)
6.78 +(* prover configuration *)
6.79
6.80 type prover_config =
6.81 {command: Path.T,
6.82 arguments: int -> string,
6.83 + failure_strs: string list,
6.84 max_new_clauses: int,
6.85 insert_theory_const: bool,
6.86 emit_structured_proof: bool};
6.87
6.88 -type problem =
6.89 - {with_full_types: bool,
6.90 - subgoal: int,
6.91 - goal: Proof.context * (thm list * thm),
6.92 - axiom_clauses: (thm * (string * int)) list option,
6.93 - filtered_clauses: (thm * (string * int)) list option};
6.94 -
6.95 -fun problem_of_goal with_full_types subgoal goal : problem =
6.96 - {with_full_types = with_full_types,
6.97 - subgoal = subgoal,
6.98 - goal = goal,
6.99 - axiom_clauses = NONE,
6.100 - filtered_clauses = NONE};
6.101 -
6.102 -type prover_result =
6.103 - {success: bool,
6.104 - message: string,
6.105 - theorem_names: string list, (*relevant theorems*)
6.106 - runtime: int, (*user time of the ATP, in milliseconds*)
6.107 - proof: string,
6.108 - internal_thm_names: string Vector.vector,
6.109 - filtered_clauses: (thm * (string * int)) list};
6.110 -
6.111 -type prover = int -> problem -> prover_result;
6.112 -
6.113
6.114 (* basic template *)
6.115
6.116 @@ -114,13 +58,20 @@
6.117 |> Exn.release
6.118 |> tap (after path);
6.119
6.120 -fun external_prover relevance_filter prepare write cmd args produce_answer name
6.121 - ({with_full_types, subgoal, goal, axiom_clauses, filtered_clauses}: problem) =
6.122 +fun find_failure strs proof =
6.123 + case filter (fn s => String.isSubstring s proof) strs of
6.124 + [] => if is_proof_well_formed proof then NONE
6.125 + else SOME "Ill-formed ATP output"
6.126 + | (failure :: _) => SOME failure
6.127 +
6.128 +fun external_prover relevance_filter prepare write cmd args failure_strs
6.129 + produce_answer name ({with_full_types, subgoal, goal, axiom_clauses,
6.130 + filtered_clauses}: problem) =
6.131 let
6.132 (* get clauses and prepare them for writing *)
6.133 val (ctxt, (chain_ths, th)) = goal;
6.134 val thy = ProofContext.theory_of ctxt;
6.135 - val chain_ths = map (Thm.put_name_hint SPR.chained_hint) chain_ths;
6.136 + val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
6.137 val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal);
6.138 val the_filtered_clauses =
6.139 (case filtered_clauses of
6.140 @@ -184,7 +135,7 @@
6.141 with_path cleanup export run_on (prob_pathname subgoal);
6.142
6.143 (* check for success and print out some information on failure *)
6.144 - val failure = SPR.find_failure proof;
6.145 + val failure = find_failure failure_strs proof;
6.146 val success = rc = 0 andalso is_none failure;
6.147 val (message, real_thm_names) =
6.148 if is_some failure then ("External prover failed.", [])
6.149 @@ -200,25 +151,16 @@
6.150
6.151 (* generic TPTP-based provers *)
6.152
6.153 -fun gen_tptp_prover (name, prover_config) timeout problem =
6.154 - let
6.155 - val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} =
6.156 - prover_config;
6.157 - in
6.158 - external_prover
6.159 - (SFF.get_relevant max_new_clauses insert_theory_const)
6.160 - (SFF.prepare_clauses false)
6.161 - Sledgehammer_HOL_Clause.tptp_write_file
6.162 - command
6.163 - (arguments timeout)
6.164 - (if emit_structured_proof then SPR.structured_proof
6.165 - else SPR.lemma_list false)
6.166 - name
6.167 - problem
6.168 - end;
6.169 +fun generic_tptp_prover
6.170 + (name, {command, arguments, failure_strs, max_new_clauses,
6.171 + insert_theory_const, emit_structured_proof}) timeout =
6.172 + external_prover (get_relevant_facts max_new_clauses insert_theory_const)
6.173 + (prepare_clauses false) write_tptp_file command (arguments timeout)
6.174 + failure_strs
6.175 + (if emit_structured_proof then structured_isar_proof
6.176 + else metis_lemma_list false) name;
6.177
6.178 -fun tptp_prover (name, config) = (name, gen_tptp_prover (name, config));
6.179 -
6.180 +fun tptp_prover (name, p) = (name, generic_tptp_prover (name, p));
6.181
6.182
6.183 (** common provers **)
6.184 @@ -227,40 +169,51 @@
6.185
6.186 (*NB: Vampire does not work without explicit timelimit*)
6.187
6.188 +val vampire_failure_strs =
6.189 + ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
6.190 val vampire_max_new_clauses = 60;
6.191 val vampire_insert_theory_const = false;
6.192
6.193 -fun vampire_prover_config full : prover_config =
6.194 +fun vampire_prover_config isar : prover_config =
6.195 {command = Path.explode "$VAMPIRE_HOME/vampire",
6.196 arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
6.197 " -t " ^ string_of_int timeout),
6.198 + failure_strs = vampire_failure_strs,
6.199 max_new_clauses = vampire_max_new_clauses,
6.200 insert_theory_const = vampire_insert_theory_const,
6.201 - emit_structured_proof = full};
6.202 + emit_structured_proof = isar};
6.203
6.204 val vampire = tptp_prover ("vampire", vampire_prover_config false);
6.205 -val vampire_full = tptp_prover ("vampire_full", vampire_prover_config true);
6.206 +val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
6.207
6.208
6.209 (* E prover *)
6.210
6.211 +val eprover_failure_strs =
6.212 + ["SZS status: Satisfiable", "SZS status Satisfiable",
6.213 + "SZS status: ResourceOut", "SZS status ResourceOut",
6.214 + "# Cannot determine problem status"];
6.215 val eprover_max_new_clauses = 100;
6.216 val eprover_insert_theory_const = false;
6.217
6.218 -fun eprover_config full : prover_config =
6.219 +fun eprover_config isar : prover_config =
6.220 {command = Path.explode "$E_HOME/eproof",
6.221 arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
6.222 " --silent --cpu-limit=" ^ string_of_int timeout),
6.223 + failure_strs = eprover_failure_strs,
6.224 max_new_clauses = eprover_max_new_clauses,
6.225 insert_theory_const = eprover_insert_theory_const,
6.226 - emit_structured_proof = full};
6.227 + emit_structured_proof = isar};
6.228
6.229 val eprover = tptp_prover ("e", eprover_config false);
6.230 -val eprover_full = tptp_prover ("e_full", eprover_config true);
6.231 +val eprover_isar = tptp_prover ("e_isar", eprover_config true);
6.232
6.233
6.234 (* SPASS *)
6.235
6.236 +val spass_failure_strs =
6.237 + ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
6.238 + "SPASS beiseite: Maximal number of loops exceeded."];
6.239 val spass_max_new_clauses = 40;
6.240 val spass_insert_theory_const = true;
6.241
6.242 @@ -268,26 +221,25 @@
6.243 {command = Path.explode "$SPASS_HOME/SPASS",
6.244 arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
6.245 " -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout),
6.246 + failure_strs = spass_failure_strs,
6.247 max_new_clauses = spass_max_new_clauses,
6.248 insert_theory_const = insert_theory_const,
6.249 emit_structured_proof = false};
6.250
6.251 -fun gen_dfg_prover (name, prover_config: prover_config) timeout problem =
6.252 - let
6.253 - val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config;
6.254 - in
6.255 - external_prover
6.256 - (SFF.get_relevant max_new_clauses insert_theory_const)
6.257 - (SFF.prepare_clauses true)
6.258 - Sledgehammer_HOL_Clause.dfg_write_file
6.259 - command
6.260 - (arguments timeout)
6.261 - (SPR.lemma_list true)
6.262 - name
6.263 - problem
6.264 - end;
6.265 +fun generic_dfg_prover
6.266 + (name, ({command, arguments, failure_strs, max_new_clauses,
6.267 + insert_theory_const, ...} : prover_config)) timeout =
6.268 + external_prover
6.269 + (get_relevant_facts max_new_clauses insert_theory_const)
6.270 + (prepare_clauses true)
6.271 + write_dfg_file
6.272 + command
6.273 + (arguments timeout)
6.274 + failure_strs
6.275 + (metis_lemma_list true)
6.276 + name;
6.277
6.278 -fun dfg_prover (name, config) = (name, gen_dfg_prover (name, config));
6.279 +fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
6.280
6.281 val spass = dfg_prover ("spass", spass_config spass_insert_theory_const);
6.282 val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false);
6.283 @@ -305,7 +257,8 @@
6.284 else split_lines answer
6.285 end;
6.286
6.287 -fun refresh_systems () = Synchronized.change systems (fn _ => get_systems ());
6.288 +fun refresh_systems_on_tptp () =
6.289 + Synchronized.change systems (fn _ => get_systems ());
6.290
6.291 fun get_system prefix = Synchronized.change_result systems (fn systems =>
6.292 (if null systems then get_systems () else systems)
6.293 @@ -316,10 +269,13 @@
6.294 NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP")
6.295 | SOME sys => sys);
6.296
6.297 +val remote_failure_strs = ["Remote-script could not extract proof"];
6.298 +
6.299 fun remote_prover_config prover_prefix args max_new insert_tc: prover_config =
6.300 {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
6.301 - arguments =
6.302 - (fn timeout => args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
6.303 + arguments = (fn timeout =>
6.304 + args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
6.305 + failure_strs = remote_failure_strs,
6.306 max_new_clauses = max_new,
6.307 insert_theory_const = insert_tc,
6.308 emit_structured_proof = false};
6.309 @@ -333,4 +289,15 @@
6.310 val remote_spass = tptp_prover ("remote_spass", remote_prover_config
6.311 "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
6.312
6.313 +val provers =
6.314 + [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc,
6.315 + remote_vampire, remote_spass, remote_eprover]
6.316 +val prover_setup = fold add_prover provers
6.317 +
6.318 +val setup =
6.319 + destdir_setup
6.320 + #> problem_prefix_setup
6.321 + #> measure_runtime_setup
6.322 + #> prover_setup;
6.323 +
6.324 end;
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Mar 22 09:54:22 2010 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Mar 22 10:25:44 2010 +0100
7.3 @@ -13,7 +13,7 @@
7.4 val auto: bool Unsynchronized.ref
7.5 val default_params : theory -> (string * string) list -> params
7.6 val setup : theory -> theory
7.7 -end
7.8 +end;
7.9
7.10 structure Nitpick_Isar : NITPICK_ISAR =
7.11 struct
8.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Mar 22 09:54:22 2010 +0100
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Mar 22 10:25:44 2010 +0100
8.3 @@ -12,7 +12,7 @@
8.4 hol_context -> (typ option * bool option) list
8.5 -> (typ option * bool option) list -> term
8.6 -> term list * term list * bool * bool * bool
8.7 -end
8.8 +end;
8.9
8.10 structure Nitpick_Preproc : NITPICK_PREPROC =
8.11 struct
9.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Mar 22 09:54:22 2010 +0100
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Mar 22 10:25:44 2010 +0100
9.3 @@ -8,7 +8,7 @@
9.4 signature NITPICK_TESTS =
9.5 sig
9.6 val run_all_tests : unit -> unit
9.7 -end
9.8 +end;
9.9
9.10 structure Nitpick_Tests =
9.11 struct
10.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Mar 22 09:54:22 2010 +0100
10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Mar 22 10:25:44 2010 +0100
10.3 @@ -62,7 +62,7 @@
10.4 val pstrs : string -> Pretty.T list
10.5 val unyxml : string -> string
10.6 val maybe_quote : string -> string
10.7 -end
10.8 +end;
10.9
10.10 structure Nitpick_Util : NITPICK_UTIL =
10.11 struct
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Mon Mar 22 10:25:44 2010 +0100
11.3 @@ -0,0 +1,53 @@
11.4 +(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML
11.5 + Author: Jia Meng, Cambridge University Computer Laboratory
11.6 +
11.7 +MESON general tactic and proof method.
11.8 +*)
11.9 +
11.10 +signature MESON_TACTIC =
11.11 +sig
11.12 + val expand_defs_tac : thm -> tactic
11.13 + val meson_general_tac : Proof.context -> thm list -> int -> tactic
11.14 + val setup: theory -> theory
11.15 +end;
11.16 +
11.17 +structure Meson_Tactic : MESON_TACTIC =
11.18 +struct
11.19 +
11.20 +open Sledgehammer_Fact_Preprocessor
11.21 +
11.22 +(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
11.23 +fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ u) =
11.24 + String.isPrefix skolem_prefix a
11.25 + | is_absko _ = false;
11.26 +
11.27 +fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ u) = (*Definition of Free, not in certain terms*)
11.28 + is_Free t andalso not (member (op aconv) xs t)
11.29 + | is_okdef _ _ = false
11.30 +
11.31 +(*This function tries to cope with open locales, which introduce hypotheses of the form
11.32 + Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
11.33 + of sko_ functions. *)
11.34 +fun expand_defs_tac st0 st =
11.35 + let val hyps0 = #hyps (rep_thm st0)
11.36 + val hyps = #hyps (crep_thm st)
11.37 + val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
11.38 + val defs = filter (is_absko o Thm.term_of) newhyps
11.39 + val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
11.40 + (map Thm.term_of hyps)
11.41 + val fixed = OldTerm.term_frees (concl_of st) @
11.42 + fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
11.43 + in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
11.44 +
11.45 +fun meson_general_tac ctxt ths i st0 =
11.46 + let
11.47 + val thy = ProofContext.theory_of ctxt
11.48 + val ctxt0 = Classical.put_claset HOL_cs ctxt
11.49 + in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
11.50 +
11.51 +val setup =
11.52 + Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
11.53 + SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
11.54 + "MESON resolution proof procedure";
11.55 +
11.56 +end;
12.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Mar 22 09:54:22 2010 +0100
12.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Mar 22 10:25:44 2010 +0100
12.3 @@ -18,9 +18,11 @@
12.4 structure Metis_Tactics : METIS_TACTICS =
12.5 struct
12.6
12.7 -structure SFC = Sledgehammer_FOL_Clause
12.8 -structure SHC = Sledgehammer_HOL_Clause
12.9 -structure SPR = Sledgehammer_Proof_Reconstruct
12.10 +open Sledgehammer_FOL_Clause
12.11 +open Sledgehammer_Fact_Preprocessor
12.12 +open Sledgehammer_HOL_Clause
12.13 +open Sledgehammer_Proof_Reconstruct
12.14 +open Sledgehammer_Fact_Filter
12.15
12.16 val trace = Unsynchronized.ref false;
12.17 fun trace_msg msg = if !trace then tracing (msg ()) else ();
12.18 @@ -67,62 +69,62 @@
12.19
12.20 fun metis_lit b c args = (b, (c, args));
12.21
12.22 -fun hol_type_to_fol (SFC.AtomV x) = Metis.Term.Var x
12.23 - | hol_type_to_fol (SFC.AtomF x) = Metis.Term.Fn(x,[])
12.24 - | hol_type_to_fol (SFC.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
12.25 +fun hol_type_to_fol (AtomV x) = Metis.Term.Var x
12.26 + | hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, [])
12.27 + | hol_type_to_fol (Comp (tc, tps)) =
12.28 + Metis.Term.Fn (tc, map hol_type_to_fol tps);
12.29
12.30 (*These two functions insert type literals before the real literals. That is the
12.31 opposite order from TPTP linkup, but maybe OK.*)
12.32
12.33 fun hol_term_to_fol_FO tm =
12.34 - case SHC.strip_comb tm of
12.35 - (SHC.CombConst(c,_,tys), tms) =>
12.36 + case strip_combterm_comb tm of
12.37 + (CombConst(c,_,tys), tms) =>
12.38 let val tyargs = map hol_type_to_fol tys
12.39 val args = map hol_term_to_fol_FO tms
12.40 in Metis.Term.Fn (c, tyargs @ args) end
12.41 - | (SHC.CombVar(v,_), []) => Metis.Term.Var v
12.42 + | (CombVar(v,_), []) => Metis.Term.Var v
12.43 | _ => error "hol_term_to_fol_FO";
12.44
12.45 -fun hol_term_to_fol_HO (SHC.CombVar (a, _)) = Metis.Term.Var a
12.46 - | hol_term_to_fol_HO (SHC.CombConst (a, _, tylist)) =
12.47 +fun hol_term_to_fol_HO (CombVar (a, _)) = Metis.Term.Var a
12.48 + | hol_term_to_fol_HO (CombConst (a, _, tylist)) =
12.49 Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
12.50 - | hol_term_to_fol_HO (SHC.CombApp (tm1, tm2)) =
12.51 + | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
12.52 Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
12.53
12.54 (*The fully-typed translation, to avoid type errors*)
12.55 fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
12.56
12.57 -fun hol_term_to_fol_FT (SHC.CombVar(a, ty)) =
12.58 - wrap_type (Metis.Term.Var a, ty)
12.59 - | hol_term_to_fol_FT (SHC.CombConst(a, ty, _)) =
12.60 +fun hol_term_to_fol_FT (CombVar(a, ty)) = wrap_type (Metis.Term.Var a, ty)
12.61 + | hol_term_to_fol_FT (CombConst(a, ty, _)) =
12.62 wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
12.63 - | hol_term_to_fol_FT (tm as SHC.CombApp(tm1,tm2)) =
12.64 + | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
12.65 wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
12.66 - SHC.type_of_combterm tm);
12.67 + type_of_combterm tm);
12.68
12.69 -fun hol_literal_to_fol FO (SHC.Literal (pol, tm)) =
12.70 - let val (SHC.CombConst(p,_,tys), tms) = SHC.strip_comb tm
12.71 +fun hol_literal_to_fol FO (Literal (pol, tm)) =
12.72 + let val (CombConst(p,_,tys), tms) = strip_combterm_comb tm
12.73 val tylits = if p = "equal" then [] else map hol_type_to_fol tys
12.74 val lits = map hol_term_to_fol_FO tms
12.75 in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
12.76 - | hol_literal_to_fol HO (SHC.Literal (pol, tm)) =
12.77 - (case SHC.strip_comb tm of
12.78 - (SHC.CombConst("equal",_,_), tms) =>
12.79 + | hol_literal_to_fol HO (Literal (pol, tm)) =
12.80 + (case strip_combterm_comb tm of
12.81 + (CombConst("equal",_,_), tms) =>
12.82 metis_lit pol "=" (map hol_term_to_fol_HO tms)
12.83 | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
12.84 - | hol_literal_to_fol FT (SHC.Literal (pol, tm)) =
12.85 - (case SHC.strip_comb tm of
12.86 - (SHC.CombConst("equal",_,_), tms) =>
12.87 + | hol_literal_to_fol FT (Literal (pol, tm)) =
12.88 + (case strip_combterm_comb tm of
12.89 + (CombConst("equal",_,_), tms) =>
12.90 metis_lit pol "=" (map hol_term_to_fol_FT tms)
12.91 | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
12.92
12.93 fun literals_of_hol_thm thy mode t =
12.94 - let val (lits, types_sorts) = SHC.literals_of_term thy t
12.95 + let val (lits, types_sorts) = literals_of_term thy t
12.96 in (map (hol_literal_to_fol mode) lits, types_sorts) end;
12.97
12.98 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
12.99 -fun metis_of_typeLit pos (SFC.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
12.100 - | metis_of_typeLit pos (SFC.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
12.101 +fun metis_of_typeLit pos (LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
12.102 + | metis_of_typeLit pos (LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
12.103
12.104 fun default_sort _ (TVar _) = false
12.105 | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
12.106 @@ -136,10 +138,9 @@
12.107 (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
12.108 in
12.109 if is_conjecture then
12.110 - (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), SFC.add_typs types_sorts)
12.111 + (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), add_typs types_sorts)
12.112 else
12.113 - let val tylits = SFC.add_typs
12.114 - (filter (not o default_sort ctxt) types_sorts)
12.115 + let val tylits = add_typs (filter (not o default_sort ctxt) types_sorts)
12.116 val mtylits = if Config.get ctxt type_lits
12.117 then map (metis_of_typeLit false) tylits else []
12.118 in
12.119 @@ -149,13 +150,13 @@
12.120
12.121 (* ARITY CLAUSE *)
12.122
12.123 -fun m_arity_cls (SFC.TConsLit (c,t,args)) =
12.124 - metis_lit true (SFC.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
12.125 - | m_arity_cls (SFC.TVarLit (c,str)) =
12.126 - metis_lit false (SFC.make_type_class c) [Metis.Term.Var str];
12.127 +fun m_arity_cls (TConsLit (c,t,args)) =
12.128 + metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
12.129 + | m_arity_cls (TVarLit (c,str)) =
12.130 + metis_lit false (make_type_class c) [Metis.Term.Var str];
12.131
12.132 (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
12.133 -fun arity_cls (SFC.ArityClause{conclLit,premLits,...}) =
12.134 +fun arity_cls (ArityClause {conclLit, premLits, ...}) =
12.135 (TrueI,
12.136 Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
12.137
12.138 @@ -164,7 +165,7 @@
12.139 fun m_classrel_cls subclass superclass =
12.140 [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
12.141
12.142 -fun classrel_cls (SFC.ClassrelClause {subclass, superclass, ...}) =
12.143 +fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
12.144 (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
12.145
12.146 (* ------------------------------------------------------------------------- *)
12.147 @@ -213,14 +214,14 @@
12.148 | strip_happ args x = (x, args);
12.149
12.150 fun fol_type_to_isa _ (Metis.Term.Var v) =
12.151 - (case SPR.strip_prefix SFC.tvar_prefix v of
12.152 - SOME w => SPR.make_tvar w
12.153 - | NONE => SPR.make_tvar v)
12.154 + (case strip_prefix tvar_prefix v of
12.155 + SOME w => make_tvar w
12.156 + | NONE => make_tvar v)
12.157 | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
12.158 - (case SPR.strip_prefix SFC.tconst_prefix x of
12.159 - SOME tc => Term.Type (SPR.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
12.160 + (case strip_prefix tconst_prefix x of
12.161 + SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
12.162 | NONE =>
12.163 - case SPR.strip_prefix SFC.tfree_prefix x of
12.164 + case strip_prefix tfree_prefix x of
12.165 SOME tf => mk_tfree ctxt tf
12.166 | NONE => error ("fol_type_to_isa: " ^ x));
12.167
12.168 @@ -229,10 +230,10 @@
12.169 let val thy = ProofContext.theory_of ctxt
12.170 val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
12.171 fun tm_to_tt (Metis.Term.Var v) =
12.172 - (case SPR.strip_prefix SFC.tvar_prefix v of
12.173 - SOME w => Type (SPR.make_tvar w)
12.174 + (case strip_prefix tvar_prefix v of
12.175 + SOME w => Type (make_tvar w)
12.176 | NONE =>
12.177 - case SPR.strip_prefix SFC.schematic_var_prefix v of
12.178 + case strip_prefix schematic_var_prefix v of
12.179 SOME w => Term (mk_var (w, HOLogic.typeT))
12.180 | NONE => Term (mk_var (v, HOLogic.typeT)) )
12.181 (*Var from Metis with a name like _nnn; possibly a type variable*)
12.182 @@ -247,16 +248,16 @@
12.183 end
12.184 | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
12.185 and applic_to_tt ("=",ts) =
12.186 - Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
12.187 + Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
12.188 | applic_to_tt (a,ts) =
12.189 - case SPR.strip_prefix SFC.const_prefix a of
12.190 + case strip_prefix const_prefix a of
12.191 SOME b =>
12.192 - let val c = SPR.invert_const b
12.193 - val ntypes = SPR.num_typargs thy c
12.194 + let val c = invert_const b
12.195 + val ntypes = num_typargs thy c
12.196 val nterms = length ts - ntypes
12.197 val tts = map tm_to_tt ts
12.198 val tys = types_of (List.take(tts,ntypes))
12.199 - val ntyargs = SPR.num_typargs thy c
12.200 + val ntyargs = num_typargs thy c
12.201 in if length tys = ntyargs then
12.202 apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
12.203 else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
12.204 @@ -267,14 +268,14 @@
12.205 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
12.206 end
12.207 | NONE => (*Not a constant. Is it a type constructor?*)
12.208 - case SPR.strip_prefix SFC.tconst_prefix a of
12.209 + case strip_prefix tconst_prefix a of
12.210 SOME b =>
12.211 - Type (Term.Type (SPR.invert_type_const b, types_of (map tm_to_tt ts)))
12.212 + Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
12.213 | NONE => (*Maybe a TFree. Should then check that ts=[].*)
12.214 - case SPR.strip_prefix SFC.tfree_prefix a of
12.215 + case strip_prefix tfree_prefix a of
12.216 SOME b => Type (mk_tfree ctxt b)
12.217 | NONE => (*a fixed variable? They are Skolem functions.*)
12.218 - case SPR.strip_prefix SFC.fixed_var_prefix a of
12.219 + case strip_prefix fixed_var_prefix a of
12.220 SOME b =>
12.221 let val opr = Term.Free(b, HOLogic.typeT)
12.222 in apply_list opr (length ts) (map tm_to_tt ts) end
12.223 @@ -285,16 +286,16 @@
12.224 fun fol_term_to_hol_FT ctxt fol_tm =
12.225 let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
12.226 fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
12.227 - (case SPR.strip_prefix SFC.schematic_var_prefix v of
12.228 + (case strip_prefix schematic_var_prefix v of
12.229 SOME w => mk_var(w, dummyT)
12.230 | NONE => mk_var(v, dummyT))
12.231 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
12.232 Const ("op =", HOLogic.typeT)
12.233 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
12.234 - (case SPR.strip_prefix SFC.const_prefix x of
12.235 - SOME c => Const (SPR.invert_const c, dummyT)
12.236 + (case strip_prefix const_prefix x of
12.237 + SOME c => Const (invert_const c, dummyT)
12.238 | NONE => (*Not a constant. Is it a fixed variable??*)
12.239 - case SPR.strip_prefix SFC.fixed_var_prefix x of
12.240 + case strip_prefix fixed_var_prefix x of
12.241 SOME v => Free (v, fol_type_to_isa ctxt ty)
12.242 | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
12.243 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
12.244 @@ -303,12 +304,12 @@
12.245 cvt tm1 $ cvt tm2
12.246 | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
12.247 | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
12.248 - list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
12.249 + list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
12.250 | cvt (t as Metis.Term.Fn (x, [])) =
12.251 - (case SPR.strip_prefix SFC.const_prefix x of
12.252 - SOME c => Const (SPR.invert_const c, dummyT)
12.253 + (case strip_prefix const_prefix x of
12.254 + SOME c => Const (invert_const c, dummyT)
12.255 | NONE => (*Not a constant. Is it a fixed variable??*)
12.256 - case SPR.strip_prefix SFC.fixed_var_prefix x of
12.257 + case strip_prefix fixed_var_prefix x of
12.258 SOME v => Free (v, dummyT)
12.259 | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
12.260 fol_term_to_hol_RAW ctxt t))
12.261 @@ -331,7 +332,7 @@
12.262 ts'
12.263 in ts' end;
12.264
12.265 -fun mk_not (Const ("Not", _) $ b) = b
12.266 +fun mk_not (Const (@{const_name Not}, _) $ b) = b
12.267 | mk_not b = HOLogic.mk_not b;
12.268
12.269 val metis_eq = Metis.Term.Fn ("=", []);
12.270 @@ -387,9 +388,9 @@
12.271 " in " ^ Display.string_of_thm ctxt i_th);
12.272 NONE)
12.273 fun remove_typeinst (a, t) =
12.274 - case SPR.strip_prefix SFC.schematic_var_prefix a of
12.275 + case strip_prefix schematic_var_prefix a of
12.276 SOME b => SOME (b, t)
12.277 - | NONE => case SPR.strip_prefix SFC.tvar_prefix a of
12.278 + | NONE => case strip_prefix tvar_prefix a of
12.279 SOME _ => NONE (*type instantiations are forbidden!*)
12.280 | NONE => SOME (a,t) (*internal Metis var?*)
12.281 val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
12.282 @@ -455,8 +456,8 @@
12.283 val c_t = cterm_incr_types thy refl_idx i_t
12.284 in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
12.285
12.286 -fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*)
12.287 - | get_ty_arg_size thy (Const (c, _)) = (SPR.num_typargs thy c handle TYPE _ => 0)
12.288 +fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0 (*equality has no type arguments*)
12.289 + | get_ty_arg_size thy (Const (c, _)) = (num_typargs thy c handle TYPE _ => 0)
12.290 | get_ty_arg_size _ _ = 0;
12.291
12.292 (* INFERENCE RULE: EQUALITY *)
12.293 @@ -469,7 +470,7 @@
12.294 | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
12.295 fun path_finder_FO tm [] = (tm, Term.Bound 0)
12.296 | path_finder_FO tm (p::ps) =
12.297 - let val (tm1,args) = Term.strip_comb tm
12.298 + let val (tm1,args) = strip_comb tm
12.299 val adjustment = get_ty_arg_size thy tm1
12.300 val p' = if adjustment > p then p else p-adjustment
12.301 val tm_p = List.nth(args,p')
12.302 @@ -496,13 +497,13 @@
12.303 " isa-term: " ^ Syntax.string_of_term ctxt tm ^
12.304 " fol-term: " ^ Metis.Term.toString t)
12.305 fun path_finder FO tm ps _ = path_finder_FO tm ps
12.306 - | path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ =
12.307 + | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
12.308 (*equality: not curried, as other predicates are*)
12.309 if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
12.310 else path_finder_HO tm (p::ps) (*1 selects second operand*)
12.311 | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
12.312 path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
12.313 - | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps)
12.314 + | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
12.315 (Metis.Term.Fn ("=", [t1,t2])) =
12.316 (*equality: not curried, as other predicates are*)
12.317 if p=0 then path_finder_FT tm (0::1::ps)
12.318 @@ -514,7 +515,7 @@
12.319 | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
12.320 (*if not equality, ignore head to skip the hBOOL predicate*)
12.321 | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
12.322 - fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
12.323 + fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
12.324 let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
12.325 in (tm, nt $ tm_rslt) end
12.326 | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
12.327 @@ -542,7 +543,7 @@
12.328 | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
12.329 equality_inf ctxt mode f_lit f_p f_r;
12.330
12.331 -fun real_literal (_, (c, _)) = not (String.isPrefix SFC.class_prefix c);
12.332 +fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
12.333
12.334 fun translate _ _ thpairs [] = thpairs
12.335 | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
12.336 @@ -568,23 +569,14 @@
12.337 (* Translation of HO Clauses *)
12.338 (* ------------------------------------------------------------------------- *)
12.339
12.340 -fun cnf_th thy th = hd (Sledgehammer_Fact_Preprocessor.cnf_axiom thy th);
12.341 -
12.342 -val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
12.343 -val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
12.344 -
12.345 -val comb_I = cnf_th @{theory} SHC.comb_I;
12.346 -val comb_K = cnf_th @{theory} SHC.comb_K;
12.347 -val comb_B = cnf_th @{theory} SHC.comb_B;
12.348 -val comb_C = cnf_th @{theory} SHC.comb_C;
12.349 -val comb_S = cnf_th @{theory} SHC.comb_S;
12.350 +fun cnf_th thy th = hd (cnf_axiom thy th);
12.351
12.352 fun type_ext thy tms =
12.353 - let val subs = Sledgehammer_Fact_Filter.tfree_classes_of_terms tms
12.354 - val supers = Sledgehammer_Fact_Filter.tvar_classes_of_terms tms
12.355 - and tycons = Sledgehammer_Fact_Filter.type_consts_of_terms thy tms
12.356 - val (supers', arity_clauses) = SFC.make_arity_clauses thy tycons supers
12.357 - val classrel_clauses = SFC.make_classrel_clauses thy subs supers'
12.358 + let val subs = tfree_classes_of_terms tms
12.359 + val supers = tvar_classes_of_terms tms
12.360 + and tycons = type_consts_of_terms thy tms
12.361 + val (supers', arity_clauses) = make_arity_clauses thy tycons supers
12.362 + val classrel_clauses = make_classrel_clauses thy subs supers'
12.363 in map classrel_cls classrel_clauses @ map arity_cls arity_clauses
12.364 end;
12.365
12.366 @@ -593,8 +585,8 @@
12.367 (* ------------------------------------------------------------------------- *)
12.368
12.369 type logic_map =
12.370 - {axioms : (Metis.Thm.thm * thm) list,
12.371 - tfrees : SFC.type_literal list};
12.372 + {axioms: (Metis.Thm.thm * thm) list,
12.373 + tfrees: type_literal list};
12.374
12.375 fun const_in_metis c (pred, tm_list) =
12.376 let
12.377 @@ -606,7 +598,7 @@
12.378 (*Extract TFree constraints from context to include as conjecture clauses*)
12.379 fun init_tfrees ctxt =
12.380 let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
12.381 - in SFC.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
12.382 + in add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
12.383
12.384 (*transform isabelle type / arity clause to metis clause *)
12.385 fun add_type_thm [] lmap = lmap
12.386 @@ -643,12 +635,12 @@
12.387 val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
12.388 fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
12.389 (*Now check for the existence of certain combinators*)
12.390 - val thI = if used "c_COMBI" then [comb_I] else []
12.391 - val thK = if used "c_COMBK" then [comb_K] else []
12.392 - val thB = if used "c_COMBB" then [comb_B] else []
12.393 - val thC = if used "c_COMBC" then [comb_C] else []
12.394 - val thS = if used "c_COMBS" then [comb_S] else []
12.395 - val thEQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
12.396 + val thI = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else []
12.397 + val thK = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else []
12.398 + val thB = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else []
12.399 + val thC = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
12.400 + val thS = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
12.401 + val thEQ = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
12.402 val lmap' = if mode=FO then lmap
12.403 else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
12.404 in
12.405 @@ -668,7 +660,7 @@
12.406 fun FOL_SOLVE mode ctxt cls ths0 =
12.407 let val thy = ProofContext.theory_of ctxt
12.408 val th_cls_pairs =
12.409 - map (fn th => (Thm.get_name_hint th, Sledgehammer_Fact_Preprocessor.cnf_axiom thy th)) ths0
12.410 + map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
12.411 val ths = maps #2 th_cls_pairs
12.412 val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
12.413 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
12.414 @@ -677,7 +669,7 @@
12.415 val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
12.416 val _ = if null tfrees then ()
12.417 else (trace_msg (fn () => "TFREE CLAUSES");
12.418 - app (fn tf => trace_msg (fn _ => SFC.tptp_of_typeLit true tf)) tfrees)
12.419 + app (fn tf => trace_msg (fn _ => tptp_of_typeLit true tf)) tfrees)
12.420 val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
12.421 val thms = map #1 axioms
12.422 val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
12.423 @@ -719,12 +711,12 @@
12.424 let val _ = trace_msg (fn () =>
12.425 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
12.426 in
12.427 - if exists_type Sledgehammer_Fact_Preprocessor.type_has_topsort (prop_of st0)
12.428 + if exists_type type_has_topsort (prop_of st0)
12.429 then raise METIS "Metis: Proof state contains the universal sort {}"
12.430 else
12.431 - (Meson.MESON Sledgehammer_Fact_Preprocessor.neg_clausify
12.432 + (Meson.MESON neg_clausify
12.433 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
12.434 - THEN Sledgehammer_Fact_Preprocessor.expand_defs_tac st0) st0
12.435 + THEN Meson_Tactic.expand_defs_tac st0) st0
12.436 end
12.437 handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
12.438
12.439 @@ -737,11 +729,11 @@
12.440
12.441 val setup =
12.442 type_lits_setup #>
12.443 - method @{binding metis} HO "METIS for FOL & HOL problems" #>
12.444 + method @{binding metis} HO "METIS for FOL and HOL problems" #>
12.445 method @{binding metisF} FO "METIS for FOL problems" #>
12.446 method @{binding metisFT} FT "METIS with fully-typed translation" #>
12.447 Method.setup @{binding finish_clausify}
12.448 - (Scan.succeed (K (SIMPLE_METHOD (Sledgehammer_Fact_Preprocessor.expand_defs_tac refl))))
12.449 + (Scan.succeed (K (SIMPLE_METHOD (Meson_Tactic.expand_defs_tac refl))))
12.450 "cleanup after conversion to clauses";
12.451
12.452 end;
13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Mar 22 09:54:22 2010 +0100
13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Mar 22 10:25:44 2010 +0100
13.3 @@ -4,47 +4,45 @@
13.4
13.5 signature SLEDGEHAMMER_FACT_FILTER =
13.6 sig
13.7 - type classrelClause = Sledgehammer_FOL_Clause.classrelClause
13.8 - type arityClause = Sledgehammer_FOL_Clause.arityClause
13.9 + type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
13.10 + type arity_clause = Sledgehammer_FOL_Clause.arity_clause
13.11 type axiom_name = Sledgehammer_HOL_Clause.axiom_name
13.12 - type clause = Sledgehammer_HOL_Clause.clause
13.13 - type clause_id = Sledgehammer_HOL_Clause.clause_id
13.14 - datatype mode = Auto | Fol | Hol
13.15 + type hol_clause = Sledgehammer_HOL_Clause.hol_clause
13.16 + type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
13.17 val tvar_classes_of_terms : term list -> string list
13.18 val tfree_classes_of_terms : term list -> string list
13.19 val type_consts_of_terms : theory -> term list -> string list
13.20 - val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
13.21 + val get_relevant_facts : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
13.22 (thm * (string * int)) list
13.23 val prepare_clauses : bool -> thm list -> thm list ->
13.24 - (thm * (axiom_name * clause_id)) list ->
13.25 - (thm * (axiom_name * clause_id)) list -> theory ->
13.26 + (thm * (axiom_name * hol_clause_id)) list ->
13.27 + (thm * (axiom_name * hol_clause_id)) list -> theory ->
13.28 axiom_name vector *
13.29 - (clause list * clause list * clause list *
13.30 - clause list * classrelClause list * arityClause list)
13.31 + (hol_clause list * hol_clause list * hol_clause list *
13.32 + hol_clause list * classrel_clause list * arity_clause list)
13.33 end;
13.34
13.35 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
13.36 struct
13.37
13.38 -structure SFC = Sledgehammer_FOL_Clause
13.39 -structure SFP = Sledgehammer_Fact_Preprocessor
13.40 -structure SHC = Sledgehammer_HOL_Clause
13.41 +open Sledgehammer_FOL_Clause
13.42 +open Sledgehammer_Fact_Preprocessor
13.43 +open Sledgehammer_HOL_Clause
13.44
13.45 -type classrelClause = SFC.classrelClause
13.46 -type arityClause = SFC.arityClause
13.47 -type axiom_name = SHC.axiom_name
13.48 -type clause = SHC.clause
13.49 -type clause_id = SHC.clause_id
13.50 +type axiom_name = axiom_name
13.51 +type hol_clause = hol_clause
13.52 +type hol_clause_id = hol_clause_id
13.53
13.54 (********************************************************************)
13.55 (* some settings for both background automatic ATP calling procedure*)
13.56 (* and also explicit ATP invocation methods *)
13.57 (********************************************************************)
13.58
13.59 -(*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
13.60 +(* Translation mode can be auto-detected, or forced to be first-order or
13.61 + higher-order *)
13.62 datatype mode = Auto | Fol | Hol;
13.63
13.64 -val linkup_logic_mode = Auto;
13.65 +val translation_mode = Auto;
13.66
13.67 (*** background linkup ***)
13.68 val run_blacklist_filter = true;
13.69 @@ -59,7 +57,7 @@
13.70 (* Relevance Filtering *)
13.71 (***************************************************************)
13.72
13.73 -fun strip_Trueprop (Const("Trueprop",_) $ t) = t
13.74 +fun strip_Trueprop (@{const Trueprop} $ t) = t
13.75 | strip_Trueprop t = t;
13.76
13.77 (*A surprising number of theorems contain only a few significant constants.
13.78 @@ -79,7 +77,10 @@
13.79 being chosen, but for some reason filtering works better with them listed. The
13.80 logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
13.81 must be within comprehensions.*)
13.82 -val standard_consts = ["Trueprop","==>","all","==","op |","Not","op ="];
13.83 +val standard_consts =
13.84 + [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
13.85 + @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
13.86 + @{const_name "op ="}];
13.87
13.88
13.89 (*** constants with types ***)
13.90 @@ -233,7 +234,7 @@
13.91 end
13.92 handle ConstFree => false
13.93 in
13.94 - case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) =>
13.95 + case tm of @{const Trueprop} $ (Const(@{const_name "op ="}, _) $ lhs $ rhs) =>
13.96 defs lhs rhs
13.97 | _ => false
13.98 end;
13.99 @@ -252,10 +253,10 @@
13.100 let val cls = sort compare_pairs newpairs
13.101 val accepted = List.take (cls, max_new)
13.102 in
13.103 - SFP.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
13.104 + trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
13.105 ", exceeds the limit of " ^ Int.toString (max_new)));
13.106 - SFP.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
13.107 - SFP.trace_msg (fn () => "Actually passed: " ^
13.108 + trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
13.109 + trace_msg (fn () => "Actually passed: " ^
13.110 space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
13.111
13.112 (map #1 accepted, map #1 (List.drop (cls, max_new)))
13.113 @@ -270,7 +271,7 @@
13.114 val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
13.115 val newp = p + (1.0-p) / convergence
13.116 in
13.117 - SFP.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
13.118 + trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
13.119 (map #1 newrels) @
13.120 (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
13.121 end
13.122 @@ -278,12 +279,12 @@
13.123 let val weight = clause_weight ctab rel_consts consts_typs
13.124 in
13.125 if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
13.126 - then (SFP.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
13.127 + then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
13.128 " passes: " ^ Real.toString weight));
13.129 relevant ((ax,weight)::newrels, rejects) axs)
13.130 else relevant (newrels, ax::rejects) axs
13.131 end
13.132 - in SFP.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
13.133 + in trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
13.134 relevant ([],[])
13.135 end;
13.136
13.137 @@ -292,12 +293,12 @@
13.138 then
13.139 let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
13.140 val goal_const_tab = get_goal_consts_typs thy goals
13.141 - val _ = SFP.trace_msg (fn () => ("Initial constants: " ^
13.142 + val _ = trace_msg (fn () => ("Initial constants: " ^
13.143 space_implode ", " (Symtab.keys goal_const_tab)));
13.144 val rels = relevant_clauses max_new thy const_tab (pass_mark)
13.145 goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms)
13.146 in
13.147 - SFP.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
13.148 + trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
13.149 rels
13.150 end
13.151 else axioms;
13.152 @@ -332,7 +333,7 @@
13.153 | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
13.154 | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
13.155
13.156 -fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
13.157 +fun hash_literal (@{const Not} $ P) = Word.notb(hashw_term(P,0w0))
13.158 | hash_literal P = hashw_term(P,0w0);
13.159
13.160 fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t))));
13.161 @@ -351,7 +352,7 @@
13.162 fun make_unique xs =
13.163 let val ht = mk_clause_table 7000
13.164 in
13.165 - SFP.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
13.166 + trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
13.167 app (ignore o Polyhash.peekInsert ht) xs;
13.168 Polyhash.listItems ht
13.169 end;
13.170 @@ -383,7 +384,7 @@
13.171
13.172 val name1 = Facts.extern facts name;
13.173 val name2 = Name_Space.extern full_space name;
13.174 - val ths = filter_out SFP.bad_for_atp ths0;
13.175 + val ths = filter_out bad_for_atp ths0;
13.176 in
13.177 if Facts.is_concealed facts name orelse null ths orelse
13.178 run_blacklist_filter andalso is_package_def name then I
13.179 @@ -403,7 +404,7 @@
13.180
13.181 (*Ignore blacklisted basenames*)
13.182 fun add_multi_names (a, ths) pairs =
13.183 - if (Long_Name.base_name a) mem_string SFP.multi_base_blacklist then pairs
13.184 + if (Long_Name.base_name a) mem_string multi_base_blacklist then pairs
13.185 else add_single_names (a, ths) pairs;
13.186
13.187 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
13.188 @@ -412,12 +413,17 @@
13.189 fun name_thm_pairs ctxt =
13.190 let
13.191 val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
13.192 - val blacklist =
13.193 - if run_blacklist_filter then No_ATPs.get ctxt |> map Thm.prop_of else []
13.194 - fun is_blacklisted (_, th) = member (op =) blacklist (Thm.prop_of th)
13.195 + val ps = [] |> fold add_multi_names mults
13.196 + |> fold add_single_names singles
13.197 in
13.198 - filter_out is_blacklisted
13.199 - (fold add_single_names singles (fold add_multi_names mults []))
13.200 + if run_blacklist_filter then
13.201 + let
13.202 + val blacklist = No_ATPs.get ctxt
13.203 + |> map (`Thm.full_prop_of) |> Termtab.make
13.204 + val is_blacklisted = Termtab.defined blacklist o Thm.full_prop_of o snd
13.205 + in ps |> filter_out is_blacklisted end
13.206 + else
13.207 + ps
13.208 end;
13.209
13.210 fun check_named ("", th) =
13.211 @@ -426,7 +432,7 @@
13.212
13.213 fun get_all_lemmas ctxt =
13.214 let val included_thms =
13.215 - tap (fn ths => SFP.trace_msg
13.216 + tap (fn ths => trace_msg
13.217 (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
13.218 (name_thm_pairs ctxt)
13.219 in
13.220 @@ -440,7 +446,7 @@
13.221 fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts);
13.222
13.223 (*Remove this trivial type class*)
13.224 -fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
13.225 +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
13.226
13.227 fun tvar_classes_of_terms ts =
13.228 let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
13.229 @@ -499,14 +505,10 @@
13.230 fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
13.231 | too_general_eqterms _ = false;
13.232
13.233 -fun too_general_equality (Const ("op =", _) $ x $ y) =
13.234 +fun too_general_equality (Const (@{const_name "op ="}, _) $ x $ y) =
13.235 too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
13.236 | too_general_equality _ = false;
13.237
13.238 -(* tautologous? *)
13.239 -fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
13.240 - | is_taut _ = false;
13.241 -
13.242 fun has_typed_var tycons = exists_subterm
13.243 (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
13.244
13.245 @@ -514,28 +516,29 @@
13.246 they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
13.247 The resulting clause will have no type constraint, yielding false proofs. Even "bool"
13.248 leads to many unsound proofs, though (obviously) only for higher-order problems.*)
13.249 -val unwanted_types = ["Product_Type.unit","bool"];
13.250 +val unwanted_types = [@{type_name unit}, @{type_name bool}];
13.251
13.252 fun unwanted t =
13.253 - is_taut t orelse has_typed_var unwanted_types t orelse
13.254 + t = @{prop True} orelse has_typed_var unwanted_types t orelse
13.255 forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
13.256
13.257 (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
13.258 likely to lead to unsound proofs.*)
13.259 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
13.260
13.261 -fun isFO thy goal_cls = case linkup_logic_mode of
13.262 - Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
13.263 - | Fol => true
13.264 - | Hol => false
13.265 +fun is_first_order thy goal_cls =
13.266 + case translation_mode of
13.267 + Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
13.268 + | Fol => true
13.269 + | Hol => false
13.270
13.271 -fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
13.272 +fun get_relevant_facts max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
13.273 let
13.274 val thy = ProofContext.theory_of ctxt
13.275 - val isFO = isFO thy goal_cls
13.276 + val is_FO = is_first_order thy goal_cls
13.277 val included_cls = get_all_lemmas ctxt
13.278 - |> SFP.cnf_rules_pairs thy |> make_unique
13.279 - |> restrict_to_logic thy isFO
13.280 + |> cnf_rules_pairs thy |> make_unique
13.281 + |> restrict_to_logic thy is_FO
13.282 |> remove_unwanted_clauses
13.283 in
13.284 relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
13.285 @@ -547,28 +550,27 @@
13.286 let
13.287 (* add chain thms *)
13.288 val chain_cls =
13.289 - SFP.cnf_rules_pairs thy (filter check_named (map SFP.pairname chain_ths))
13.290 + cnf_rules_pairs thy (filter check_named (map pairname chain_ths))
13.291 val axcls = chain_cls @ axcls
13.292 val extra_cls = chain_cls @ extra_cls
13.293 - val isFO = isFO thy goal_cls
13.294 + val is_FO = is_first_order thy goal_cls
13.295 val ccls = subtract_cls goal_cls extra_cls
13.296 - val _ = app (fn th => SFP.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
13.297 + val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
13.298 val ccltms = map prop_of ccls
13.299 and axtms = map (prop_of o #1) extra_cls
13.300 val subs = tfree_classes_of_terms ccltms
13.301 and supers = tvar_classes_of_terms axtms
13.302 - and tycons = type_consts_of_terms thy (ccltms@axtms)
13.303 + and tycons = type_consts_of_terms thy (ccltms @ axtms)
13.304 (*TFrees in conjecture clauses; TVars in axiom clauses*)
13.305 - val conjectures = SHC.make_conjecture_clauses dfg thy ccls
13.306 - val (_, extra_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy extra_cls)
13.307 - val (clnames,axiom_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy axcls)
13.308 - val helper_clauses = SHC.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
13.309 - val (supers',arity_clauses) = SFC.make_arity_clauses_dfg dfg thy tycons supers
13.310 - val classrel_clauses = SFC.make_classrel_clauses thy subs supers'
13.311 + val conjectures = make_conjecture_clauses dfg thy ccls
13.312 + val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls)
13.313 + val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls)
13.314 + val helper_clauses = get_helper_clauses dfg thy is_FO (conjectures, extra_cls, [])
13.315 + val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers
13.316 + val classrel_clauses = make_classrel_clauses thy subs supers'
13.317 in
13.318 (Vector.fromList clnames,
13.319 (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
13.320 end
13.321
13.322 end;
13.323 -
14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Mar 22 09:54:22 2010 +0100
14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Mar 22 10:25:44 2010 +0100
14.3 @@ -8,6 +8,7 @@
14.4 sig
14.5 val trace: bool Unsynchronized.ref
14.6 val trace_msg: (unit -> string) -> unit
14.7 + val skolem_prefix: string
14.8 val cnf_axiom: theory -> thm -> thm list
14.9 val pairname: thm -> string * thm
14.10 val multi_base_blacklist: string list
14.11 @@ -15,7 +16,6 @@
14.12 val type_has_topsort: typ -> bool
14.13 val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
14.14 val neg_clausify: thm list -> thm list
14.15 - val expand_defs_tac: thm -> tactic
14.16 val combinators: thm -> thm
14.17 val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
14.18 val suppress_endtheory: bool Unsynchronized.ref
14.19 @@ -26,8 +26,12 @@
14.20 structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR =
14.21 struct
14.22
14.23 +open Sledgehammer_FOL_Clause
14.24 +
14.25 val trace = Unsynchronized.ref false;
14.26 -fun trace_msg msg = if ! trace then tracing (msg ()) else ();
14.27 +fun trace_msg msg = if !trace then tracing (msg ()) else ();
14.28 +
14.29 +val skolem_prefix = "sko_"
14.30
14.31 fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
14.32
14.33 @@ -75,7 +79,7 @@
14.34 fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
14.35 (*Existential: declare a Skolem function, then insert into body and continue*)
14.36 let
14.37 - val cname = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
14.38 + val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
14.39 val args0 = OldTerm.term_frees xtp (*get the formal parameter list*)
14.40 val Ts = map type_of args0
14.41 val extraTs = rhs_extra_types (Ts ---> T) xtp
14.42 @@ -110,7 +114,7 @@
14.43 val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
14.44 val Ts = map type_of args
14.45 val cT = Ts ---> T
14.46 - val id = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
14.47 + val id = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
14.48 val c = Free (id, cT)
14.49 val rhs = list_abs_free (map dest_Free args,
14.50 HOLogic.choice_const T $ xtp)
14.51 @@ -386,15 +390,14 @@
14.52 | cnf_rules_pairs_aux thy pairs ((name,th)::ths) =
14.53 let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs
14.54 handle THM _ => pairs |
14.55 - Sledgehammer_FOL_Clause.CLAUSE _ => pairs
14.56 + CLAUSE _ => pairs
14.57 in cnf_rules_pairs_aux thy pairs' ths end;
14.58
14.59 (*The combination of rev and tail recursion preserves the original order*)
14.60 fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
14.61
14.62
14.63 -(**** Convert all facts of the theory into clauses
14.64 - (Sledgehammer_FOL_Clause.clause, or Sledgehammer_HOL_Clause.clause) ****)
14.65 +(**** Convert all facts of the theory into FOL or HOL clauses ****)
14.66
14.67 local
14.68
14.69 @@ -455,49 +458,13 @@
14.70 lambda_free, but then the individual theory caches become much bigger.*)
14.71
14.72
14.73 -(*** meson proof methods ***)
14.74 -
14.75 -(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
14.76 -fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a
14.77 - | is_absko _ = false;
14.78 -
14.79 -fun is_okdef xs (Const ("==", _) $ t $ u) = (*Definition of Free, not in certain terms*)
14.80 - is_Free t andalso not (member (op aconv) xs t)
14.81 - | is_okdef _ _ = false
14.82 -
14.83 -(*This function tries to cope with open locales, which introduce hypotheses of the form
14.84 - Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
14.85 - of sko_ functions. *)
14.86 -fun expand_defs_tac st0 st =
14.87 - let val hyps0 = #hyps (rep_thm st0)
14.88 - val hyps = #hyps (crep_thm st)
14.89 - val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
14.90 - val defs = filter (is_absko o Thm.term_of) newhyps
14.91 - val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
14.92 - (map Thm.term_of hyps)
14.93 - val fixed = OldTerm.term_frees (concl_of st) @
14.94 - fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
14.95 - in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
14.96 -
14.97 -
14.98 -fun meson_general_tac ctxt ths i st0 =
14.99 - let
14.100 - val thy = ProofContext.theory_of ctxt
14.101 - val ctxt0 = Classical.put_claset HOL_cs ctxt
14.102 - in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
14.103 -
14.104 -val meson_method_setup =
14.105 - Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
14.106 - SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
14.107 - "MESON resolution proof procedure";
14.108 -
14.109 -
14.110 (*** Converting a subgoal into negated conjecture clauses. ***)
14.111
14.112 fun neg_skolemize_tac ctxt =
14.113 EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
14.114
14.115 -val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
14.116 +val neg_clausify =
14.117 + Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf;
14.118
14.119 fun neg_conjecture_clauses ctxt st0 n =
14.120 let
14.121 @@ -534,11 +501,9 @@
14.122 "conversion of theorem to clauses";
14.123
14.124
14.125 -
14.126 (** setup **)
14.127
14.128 val setup =
14.129 - meson_method_setup #>
14.130 neg_clausify_setup #>
14.131 clausify_setup #>
14.132 perhaps saturate_skolem_cache #>
15.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Mar 22 09:54:22 2010 +0100
15.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon Mar 22 10:25:44 2010 +0100
15.3 @@ -44,19 +44,19 @@
15.4 datatype arLit =
15.5 TConsLit of class * string * string list
15.6 | TVarLit of class * string
15.7 - datatype arityClause = ArityClause of
15.8 + datatype arity_clause = ArityClause of
15.9 {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list}
15.10 - datatype classrelClause = ClassrelClause of
15.11 + datatype classrel_clause = ClassrelClause of
15.12 {axiom_name: axiom_name, subclass: class, superclass: class}
15.13 - val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
15.14 - val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arityClause list
15.15 - val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
15.16 + val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
15.17 + val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list
15.18 + val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
15.19 val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table
15.20 - val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table
15.21 + val add_classrel_clause_preds : classrel_clause * int Symtab.table -> int Symtab.table
15.22 val class_of_arityLit: arLit -> class
15.23 - val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table
15.24 + val add_arity_clause_preds: arity_clause * int Symtab.table -> int Symtab.table
15.25 val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
15.26 - val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table
15.27 + val add_arity_clause_funcs: arity_clause * int Symtab.table -> int Symtab.table
15.28 val init_functab: int Symtab.table
15.29 val dfg_sign: bool -> string -> string
15.30 val dfg_of_typeLit: bool -> type_literal -> string
15.31 @@ -67,14 +67,14 @@
15.32 val string_of_start: string -> string
15.33 val string_of_descrip : string -> string
15.34 val dfg_tfree_clause : string -> string
15.35 - val dfg_classrelClause: classrelClause -> string
15.36 - val dfg_arity_clause: arityClause -> string
15.37 + val dfg_classrel_clause: classrel_clause -> string
15.38 + val dfg_arity_clause: arity_clause -> string
15.39 val tptp_sign: bool -> string -> string
15.40 val tptp_of_typeLit : bool -> type_literal -> string
15.41 val gen_tptp_cls : int * string * kind * string list * string list -> string
15.42 val tptp_tfree_clause : string -> string
15.43 - val tptp_arity_clause : arityClause -> string
15.44 - val tptp_classrelClause : classrelClause -> string
15.45 + val tptp_arity_clause : arity_clause -> string
15.46 + val tptp_classrel_clause : classrel_clause -> string
15.47 end
15.48
15.49 structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
15.50 @@ -96,28 +96,23 @@
15.51
15.52 fun union_all xss = List.foldl (uncurry (union (op =))) [] xss;
15.53
15.54 -(*Provide readable names for the more common symbolic functions*)
15.55 +(* Provide readable names for the more common symbolic functions *)
15.56 val const_trans_table =
15.57 - Symtab.make [(@{const_name "op ="}, "equal"),
15.58 - (@{const_name Orderings.less_eq}, "lessequals"),
15.59 - (@{const_name "op &"}, "and"),
15.60 - (@{const_name "op |"}, "or"),
15.61 - (@{const_name "op -->"}, "implies"),
15.62 - (@{const_name "op :"}, "in"),
15.63 - ("Sledgehammer.fequal", "fequal"),
15.64 - ("Sledgehammer.COMBI", "COMBI"),
15.65 - ("Sledgehammer.COMBK", "COMBK"),
15.66 - ("Sledgehammer.COMBB", "COMBB"),
15.67 - ("Sledgehammer.COMBC", "COMBC"),
15.68 - ("Sledgehammer.COMBS", "COMBS"),
15.69 - ("Sledgehammer.COMBB'", "COMBB_e"),
15.70 - ("Sledgehammer.COMBC'", "COMBC_e"),
15.71 - ("Sledgehammer.COMBS'", "COMBS_e")];
15.72 + Symtab.make [(@{const_name "op ="}, "equal"),
15.73 + (@{const_name Orderings.less_eq}, "lessequals"),
15.74 + (@{const_name "op &"}, "and"),
15.75 + (@{const_name "op |"}, "or"),
15.76 + (@{const_name "op -->"}, "implies"),
15.77 + (@{const_name "op :"}, "in"),
15.78 + (@{const_name fequal}, "fequal"),
15.79 + (@{const_name COMBI}, "COMBI"),
15.80 + (@{const_name COMBK}, "COMBK"),
15.81 + (@{const_name COMBB}, "COMBB"),
15.82 + (@{const_name COMBC}, "COMBC"),
15.83 + (@{const_name COMBS}, "COMBS")];
15.84
15.85 val type_const_trans_table =
15.86 - Symtab.make [("*", "prod"),
15.87 - ("+", "sum"),
15.88 - ("~=>", "map")];
15.89 + Symtab.make [("*", "prod"), ("+", "sum"), ("~=>", "map")];
15.90
15.91 (*Escaping of special characters.
15.92 Alphanumeric characters are left unchanged.
15.93 @@ -290,7 +285,7 @@
15.94 datatype arLit = TConsLit of class * string * string list
15.95 | TVarLit of class * string;
15.96
15.97 -datatype arityClause =
15.98 +datatype arity_clause =
15.99 ArityClause of {axiom_name: axiom_name,
15.100 conclLit: arLit,
15.101 premLits: arLit list};
15.102 @@ -316,7 +311,7 @@
15.103
15.104 (**** Isabelle class relations ****)
15.105
15.106 -datatype classrelClause =
15.107 +datatype classrel_clause =
15.108 ClassrelClause of {axiom_name: axiom_name,
15.109 subclass: class,
15.110 superclass: class};
15.111 @@ -330,13 +325,13 @@
15.112 fun add_supers (sub,pairs) = List.foldl (add_super sub) pairs supers
15.113 in List.foldl add_supers [] subs end;
15.114
15.115 -fun make_classrelClause (sub,super) =
15.116 +fun make_classrel_clause (sub,super) =
15.117 ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
15.118 subclass = make_type_class sub,
15.119 superclass = make_type_class super};
15.120
15.121 fun make_classrel_clauses thy subs supers =
15.122 - map make_classrelClause (class_pairs thy subs supers);
15.123 + map make_classrel_clause (class_pairs thy subs supers);
15.124
15.125
15.126 (** Isabelle arities **)
15.127 @@ -391,13 +386,13 @@
15.128 fun add_type_sort_preds (T, preds) =
15.129 update_many (preds, map pred_of_sort (sorts_on_typs T));
15.130
15.131 -fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
15.132 +fun add_classrel_clause_preds (ClassrelClause {subclass,superclass,...}, preds) =
15.133 Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
15.134
15.135 fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass
15.136 | class_of_arityLit (TVarLit (tclass, _)) = tclass;
15.137
15.138 -fun add_arityClause_preds (ArityClause {conclLit,premLits,...}, preds) =
15.139 +fun add_arity_clause_preds (ArityClause {conclLit,premLits,...}, preds) =
15.140 let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits)
15.141 fun upd (class,preds) = Symtab.update (class,1) preds
15.142 in List.foldl upd preds classes end;
15.143 @@ -414,7 +409,7 @@
15.144 | add_type_sort_funcs (TFree (a, _), funcs) =
15.145 Symtab.update (make_fixed_type_var a, 0) funcs
15.146
15.147 -fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) =
15.148 +fun add_arity_clause_funcs (ArityClause {conclLit,...}, funcs) =
15.149 let val TConsLit (_, tcons, tvars) = conclLit
15.150 in Symtab.update (tcons, length tvars) funcs end;
15.151
15.152 @@ -480,7 +475,7 @@
15.153
15.154 fun dfg_classrelLits sub sup = "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)";
15.155
15.156 -fun dfg_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
15.157 +fun dfg_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
15.158 "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^
15.159 axiom_name ^ ").\n\n";
15.160
15.161 @@ -528,7 +523,7 @@
15.162 let val tvar = "(T)"
15.163 in tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end;
15.164
15.165 -fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
15.166 +fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
15.167 "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n"
15.168
15.169 end;
16.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Mar 22 09:54:22 2010 +0100
16.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Mar 22 10:25:44 2010 +0100
16.3 @@ -6,67 +6,54 @@
16.4
16.5 signature SLEDGEHAMMER_HOL_CLAUSE =
16.6 sig
16.7 - val ext: thm
16.8 - val comb_I: thm
16.9 - val comb_K: thm
16.10 - val comb_B: thm
16.11 - val comb_C: thm
16.12 - val comb_S: thm
16.13 - val minimize_applies: bool
16.14 + type kind = Sledgehammer_FOL_Clause.kind
16.15 + type fol_type = Sledgehammer_FOL_Clause.fol_type
16.16 + type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
16.17 + type arity_clause = Sledgehammer_FOL_Clause.arity_clause
16.18 type axiom_name = string
16.19 type polarity = bool
16.20 - type clause_id = int
16.21 + type hol_clause_id = int
16.22 +
16.23 datatype combterm =
16.24 - CombConst of string * Sledgehammer_FOL_Clause.fol_type * Sledgehammer_FOL_Clause.fol_type list (*Const and Free*)
16.25 - | CombVar of string * Sledgehammer_FOL_Clause.fol_type
16.26 - | CombApp of combterm * combterm
16.27 + CombConst of string * fol_type * fol_type list (* Const and Free *) |
16.28 + CombVar of string * fol_type |
16.29 + CombApp of combterm * combterm
16.30 datatype literal = Literal of polarity * combterm
16.31 - datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
16.32 - kind: Sledgehammer_FOL_Clause.kind,literals: literal list, ctypes_sorts: typ list}
16.33 - val type_of_combterm: combterm -> Sledgehammer_FOL_Clause.fol_type
16.34 - val strip_comb: combterm -> combterm * combterm list
16.35 - val literals_of_term: theory -> term -> literal list * typ list
16.36 - exception TOO_TRIVIAL
16.37 - val make_conjecture_clauses: bool -> theory -> thm list -> clause list
16.38 - val make_axiom_clauses: bool ->
16.39 - theory ->
16.40 - (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list
16.41 - val get_helper_clauses: bool ->
16.42 - theory ->
16.43 - bool ->
16.44 - clause list * (thm * (axiom_name * clause_id)) list * string list ->
16.45 - clause list
16.46 - val tptp_write_file: bool -> Path.T ->
16.47 - clause list * clause list * clause list * clause list *
16.48 - Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
16.49 + datatype hol_clause =
16.50 + HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
16.51 + kind: kind, literals: literal list, ctypes_sorts: typ list}
16.52 +
16.53 + val type_of_combterm : combterm -> fol_type
16.54 + val strip_combterm_comb : combterm -> combterm * combterm list
16.55 + val literals_of_term : theory -> term -> literal list * typ list
16.56 + exception TRIVIAL
16.57 + val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
16.58 + val make_axiom_clauses : bool -> theory ->
16.59 + (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
16.60 + val get_helper_clauses : bool -> theory -> bool ->
16.61 + hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
16.62 + hol_clause list
16.63 + val write_tptp_file : bool -> Path.T ->
16.64 + hol_clause list * hol_clause list * hol_clause list * hol_clause list *
16.65 + classrel_clause list * arity_clause list ->
16.66 int * int
16.67 - val dfg_write_file: bool -> Path.T ->
16.68 - clause list * clause list * clause list * clause list *
16.69 - Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
16.70 - int * int
16.71 + val write_dfg_file : bool -> Path.T ->
16.72 + hol_clause list * hol_clause list * hol_clause list * hol_clause list *
16.73 + classrel_clause list * arity_clause list -> int * int
16.74 end
16.75
16.76 structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
16.77 struct
16.78
16.79 -structure SFC = Sledgehammer_FOL_Clause;
16.80 -
16.81 -(* theorems for combinators and function extensionality *)
16.82 -val ext = thm "HOL.ext";
16.83 -val comb_I = thm "Sledgehammer.COMBI_def";
16.84 -val comb_K = thm "Sledgehammer.COMBK_def";
16.85 -val comb_B = thm "Sledgehammer.COMBB_def";
16.86 -val comb_C = thm "Sledgehammer.COMBC_def";
16.87 -val comb_S = thm "Sledgehammer.COMBS_def";
16.88 -val fequal_imp_equal = thm "Sledgehammer.fequal_imp_equal";
16.89 -val equal_imp_fequal = thm "Sledgehammer.equal_imp_fequal";
16.90 -
16.91 +open Sledgehammer_FOL_Clause
16.92 +open Sledgehammer_Fact_Preprocessor
16.93
16.94 (* Parameter t_full below indicates that full type information is to be
16.95 exported *)
16.96
16.97 -(*If true, each function will be directly applied to as many arguments as possible, avoiding
16.98 - use of the "apply" operator. Use of hBOOL is also minimized.*)
16.99 +(* If true, each function will be directly applied to as many arguments as
16.100 + possible, avoiding use of the "apply" operator. Use of hBOOL is also
16.101 + minimized. *)
16.102 val minimize_applies = true;
16.103
16.104 fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
16.105 @@ -84,21 +71,18 @@
16.106
16.107 type axiom_name = string;
16.108 type polarity = bool;
16.109 -type clause_id = int;
16.110 +type hol_clause_id = int;
16.111
16.112 -datatype combterm = CombConst of string * SFC.fol_type * SFC.fol_type list (*Const and Free*)
16.113 - | CombVar of string * SFC.fol_type
16.114 - | CombApp of combterm * combterm
16.115 +datatype combterm =
16.116 + CombConst of string * fol_type * fol_type list (* Const and Free *) |
16.117 + CombVar of string * fol_type |
16.118 + CombApp of combterm * combterm
16.119
16.120 datatype literal = Literal of polarity * combterm;
16.121
16.122 -datatype clause =
16.123 - Clause of {clause_id: clause_id,
16.124 - axiom_name: axiom_name,
16.125 - th: thm,
16.126 - kind: SFC.kind,
16.127 - literals: literal list,
16.128 - ctypes_sorts: typ list};
16.129 +datatype hol_clause =
16.130 + HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
16.131 + kind: kind, literals: literal list, ctypes_sorts: typ list};
16.132
16.133
16.134 (*********************************************************************)
16.135 @@ -106,8 +90,7 @@
16.136 (*********************************************************************)
16.137
16.138 fun isFalse (Literal(pol, CombConst(c,_,_))) =
16.139 - (pol andalso c = "c_False") orelse
16.140 - (not pol andalso c = "c_True")
16.141 + (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
16.142 | isFalse _ = false;
16.143
16.144 fun isTrue (Literal (pol, CombConst(c,_,_))) =
16.145 @@ -115,24 +98,22 @@
16.146 (not pol andalso c = "c_False")
16.147 | isTrue _ = false;
16.148
16.149 -fun isTaut (Clause {literals,...}) = exists isTrue literals;
16.150 +fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
16.151
16.152 fun type_of dfg (Type (a, Ts)) =
16.153 let val (folTypes,ts) = types_of dfg Ts
16.154 - in (SFC.Comp(SFC.make_fixed_type_const dfg a, folTypes), ts) end
16.155 - | type_of _ (tp as TFree (a, _)) =
16.156 - (SFC.AtomF (SFC.make_fixed_type_var a), [tp])
16.157 - | type_of _ (tp as TVar (v, _)) =
16.158 - (SFC.AtomV (SFC.make_schematic_type_var v), [tp])
16.159 + in (Comp(make_fixed_type_const dfg a, folTypes), ts) end
16.160 + | type_of _ (tp as TFree (a, _)) = (AtomF (make_fixed_type_var a), [tp])
16.161 + | type_of _ (tp as TVar (v, _)) = (AtomV (make_schematic_type_var v), [tp])
16.162 and types_of dfg Ts =
16.163 let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
16.164 - in (folTyps, SFC.union_all ts) end;
16.165 + in (folTyps, union_all ts) end;
16.166
16.167 (* same as above, but no gathering of sort information *)
16.168 fun simp_type_of dfg (Type (a, Ts)) =
16.169 - SFC.Comp(SFC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
16.170 - | simp_type_of _ (TFree (a, _)) = SFC.AtomF(SFC.make_fixed_type_var a)
16.171 - | simp_type_of _ (TVar (v, _)) = SFC.AtomV(SFC.make_schematic_type_var v);
16.172 + Comp(make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
16.173 + | simp_type_of _ (TFree (a, _)) = AtomF (make_fixed_type_var a)
16.174 + | simp_type_of _ (TVar (v, _)) = AtomV (make_schematic_type_var v);
16.175
16.176
16.177 fun const_type_of dfg thy (c,t) =
16.178 @@ -142,27 +123,27 @@
16.179 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
16.180 fun combterm_of dfg thy (Const(c,t)) =
16.181 let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
16.182 - val c' = CombConst(SFC.make_fixed_const dfg c, tp, tvar_list)
16.183 + val c' = CombConst(make_fixed_const dfg c, tp, tvar_list)
16.184 in (c',ts) end
16.185 | combterm_of dfg _ (Free(v,t)) =
16.186 let val (tp,ts) = type_of dfg t
16.187 - val v' = CombConst(SFC.make_fixed_var v, tp, [])
16.188 + val v' = CombConst(make_fixed_var v, tp, [])
16.189 in (v',ts) end
16.190 | combterm_of dfg _ (Var(v,t)) =
16.191 let val (tp,ts) = type_of dfg t
16.192 - val v' = CombVar(SFC.make_schematic_var v,tp)
16.193 + val v' = CombVar(make_schematic_var v,tp)
16.194 in (v',ts) end
16.195 | combterm_of dfg thy (P $ Q) =
16.196 let val (P',tsP) = combterm_of dfg thy P
16.197 val (Q',tsQ) = combterm_of dfg thy Q
16.198 in (CombApp(P',Q'), union (op =) tsP tsQ) end
16.199 - | combterm_of _ _ (t as Abs _) = raise SFC.CLAUSE ("HOL CLAUSE", t);
16.200 + | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t);
16.201
16.202 -fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
16.203 +fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
16.204 | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
16.205
16.206 -fun literals_of_term1 dfg thy args (Const("Trueprop",_) $ P) = literals_of_term1 dfg thy args P
16.207 - | literals_of_term1 dfg thy args (Const("op |",_) $ P $ Q) =
16.208 +fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P
16.209 + | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) =
16.210 literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
16.211 | literals_of_term1 dfg thy (lits,ts) P =
16.212 let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
16.213 @@ -173,23 +154,23 @@
16.214 fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
16.215 val literals_of_term = literals_of_term_dfg false;
16.216
16.217 -(* Problem too trivial for resolution (empty clause) *)
16.218 -exception TOO_TRIVIAL;
16.219 +(* Trivial problem, which resolution cannot handle (empty clause) *)
16.220 +exception TRIVIAL;
16.221
16.222 (* making axiom and conjecture clauses *)
16.223 -fun make_clause dfg thy (clause_id,axiom_name,kind,th) =
16.224 +fun make_clause dfg thy (clause_id, axiom_name, kind, th) =
16.225 let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
16.226 in
16.227 - if forall isFalse lits
16.228 - then raise TOO_TRIVIAL
16.229 + if forall isFalse lits then
16.230 + raise TRIVIAL
16.231 else
16.232 - Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
16.233 - literals = lits, ctypes_sorts = ctypes_sorts}
16.234 + HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
16.235 + kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}
16.236 end;
16.237
16.238
16.239 fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
16.240 - let val cls = make_clause dfg thy (id, name, SFC.Axiom, th)
16.241 + let val cls = make_clause dfg thy (id, name, Axiom, th)
16.242 in
16.243 if isTaut cls then pairs else (name,cls)::pairs
16.244 end;
16.245 @@ -198,7 +179,7 @@
16.246
16.247 fun make_conjecture_clauses_aux _ _ _ [] = []
16.248 | make_conjecture_clauses_aux dfg thy n (th::ths) =
16.249 - make_clause dfg thy (n,"conjecture", SFC.Conjecture, th) ::
16.250 + make_clause dfg thy (n,"conjecture", Conjecture, th) ::
16.251 make_conjecture_clauses_aux dfg thy (n+1) ths;
16.252
16.253 fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
16.254 @@ -211,7 +192,7 @@
16.255 (**********************************************************************)
16.256
16.257 (*Result of a function type; no need to check that the argument type matches.*)
16.258 -fun result_type (SFC.Comp ("tc_fun", [_, tp2])) = tp2
16.259 +fun result_type (Comp ("tc_fun", [_, tp2])) = tp2
16.260 | result_type _ = error "result_type"
16.261
16.262 fun type_of_combterm (CombConst (_, tp, _)) = tp
16.263 @@ -219,7 +200,7 @@
16.264 | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
16.265
16.266 (*gets the head of a combinator application, along with the list of arguments*)
16.267 -fun strip_comb u =
16.268 +fun strip_combterm_comb u =
16.269 let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
16.270 | stripc x = x
16.271 in stripc(u,[]) end;
16.272 @@ -231,10 +212,10 @@
16.273
16.274 fun wrap_type t_full (s, tp) =
16.275 if t_full then
16.276 - type_wrapper ^ SFC.paren_pack [s, SFC.string_of_fol_type tp]
16.277 + type_wrapper ^ paren_pack [s, string_of_fol_type tp]
16.278 else s;
16.279
16.280 -fun apply ss = "hAPP" ^ SFC.paren_pack ss;
16.281 +fun apply ss = "hAPP" ^ paren_pack ss;
16.282
16.283 fun rev_apply (v, []) = v
16.284 | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
16.285 @@ -251,10 +232,9 @@
16.286 Int.toString nargs ^ " but is applied to " ^
16.287 space_implode ", " args)
16.288 val args2 = List.drop(args, nargs)
16.289 - val targs = if not t_full then map SFC.string_of_fol_type tvars
16.290 - else []
16.291 + val targs = if not t_full then map string_of_fol_type tvars else []
16.292 in
16.293 - string_apply (c ^ SFC.paren_pack (args1@targs), args2)
16.294 + string_apply (c ^ paren_pack (args1@targs), args2)
16.295 end
16.296 | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
16.297 | string_of_applic _ _ _ = error "string_of_applic";
16.298 @@ -263,7 +243,7 @@
16.299 if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
16.300
16.301 fun string_of_combterm (params as (t_full, cma, cnh)) t =
16.302 - let val (head, args) = strip_comb t
16.303 + let val (head, args) = strip_combterm_comb t
16.304 in wrap_type_if t_full cnh (head,
16.305 string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
16.306 type_of_combterm t)
16.307 @@ -271,15 +251,15 @@
16.308
16.309 (*Boolean-valued terms are here converted to literals.*)
16.310 fun boolify params t =
16.311 - "hBOOL" ^ SFC.paren_pack [string_of_combterm params t];
16.312 + "hBOOL" ^ paren_pack [string_of_combterm params t];
16.313
16.314 fun string_of_predicate (params as (_,_,cnh)) t =
16.315 case t of
16.316 (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
16.317 (*DFG only: new TPTP prefers infix equality*)
16.318 - ("equal" ^ SFC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
16.319 + ("equal" ^ paren_pack [string_of_combterm params t1, string_of_combterm params t2])
16.320 | _ =>
16.321 - case #1 (strip_comb t) of
16.322 + case #1 (strip_combterm_comb t) of
16.323 CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
16.324 | _ => boolify params t;
16.325
16.326 @@ -290,31 +270,31 @@
16.327 let val eqop = if pol then " = " else " != "
16.328 in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end;
16.329
16.330 -fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
16.331 +fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal", _, _), t1), t2))) =
16.332 tptp_of_equality params pol (t1,t2)
16.333 | tptp_literal params (Literal(pol,pred)) =
16.334 - SFC.tptp_sign pol (string_of_predicate params pred);
16.335 + tptp_sign pol (string_of_predicate params pred);
16.336
16.337 (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
16.338 the latter should only occur in conjecture clauses.*)
16.339 -fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
16.340 +fun tptp_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
16.341 (map (tptp_literal params) literals,
16.342 - map (SFC.tptp_of_typeLit pos) (SFC.add_typs ctypes_sorts));
16.343 + map (tptp_of_typeLit pos) (add_typs ctypes_sorts));
16.344
16.345 -fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) =
16.346 - let val (lits,tylits) = tptp_type_lits params (kind = SFC.Conjecture) cls
16.347 +fun clause2tptp params (cls as HOLClause {axiom_name, clause_id, kind, ...}) =
16.348 + let val (lits,tylits) = tptp_type_lits params (kind = Conjecture) cls
16.349 in
16.350 - (SFC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
16.351 + (gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits)
16.352 end;
16.353
16.354
16.355 (*** dfg format ***)
16.356
16.357 -fun dfg_literal params (Literal(pol,pred)) = SFC.dfg_sign pol (string_of_predicate params pred);
16.358 +fun dfg_literal params (Literal(pol,pred)) = dfg_sign pol (string_of_predicate params pred);
16.359
16.360 -fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
16.361 +fun dfg_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
16.362 (map (dfg_literal params) literals,
16.363 - map (SFC.dfg_of_typeLit pos) (SFC.add_typs ctypes_sorts));
16.364 + map (dfg_of_typeLit pos) (add_typs ctypes_sorts));
16.365
16.366 fun get_uvars (CombConst _) vars = vars
16.367 | get_uvars (CombVar(v,_)) vars = (v::vars)
16.368 @@ -322,20 +302,21 @@
16.369
16.370 fun get_uvars_l (Literal(_,c)) = get_uvars c [];
16.371
16.372 -fun dfg_vars (Clause {literals,...}) = SFC.union_all (map get_uvars_l literals);
16.373 +fun dfg_vars (HOLClause {literals,...}) = union_all (map get_uvars_l literals);
16.374
16.375 -fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
16.376 - let val (lits,tylits) = dfg_type_lits params (kind = SFC.Conjecture) cls
16.377 +fun clause2dfg params (cls as HOLClause {axiom_name, clause_id, kind,
16.378 + ctypes_sorts, ...}) =
16.379 + let val (lits,tylits) = dfg_type_lits params (kind = Conjecture) cls
16.380 val vars = dfg_vars cls
16.381 - val tvars = SFC.get_tvar_strs ctypes_sorts
16.382 + val tvars = get_tvar_strs ctypes_sorts
16.383 in
16.384 - (SFC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
16.385 + (gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
16.386 end;
16.387
16.388
16.389 (** For DFG format: accumulate function and predicate declarations **)
16.390
16.391 -fun addtypes tvars tab = List.foldl SFC.add_foltype_funcs tab tvars;
16.392 +fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
16.393
16.394 fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
16.395 if c = "equal" then (addtypes tvars funcs, preds)
16.396 @@ -348,33 +329,33 @@
16.397 else (addtypes tvars funcs, addit preds)
16.398 end
16.399 | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
16.400 - (SFC.add_foltype_funcs (ctp,funcs), preds)
16.401 + (add_foltype_funcs (ctp,funcs), preds)
16.402 | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
16.403
16.404 -fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls);
16.405 +fun add_literal_decls params (Literal (_,c), decls) = add_decls params (c,decls);
16.406
16.407 -fun add_clause_decls params (Clause {literals, ...}, decls) =
16.408 +fun add_clause_decls params (HOLClause {literals, ...}, decls) =
16.409 List.foldl (add_literal_decls params) decls literals
16.410 handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
16.411
16.412 fun decls_of_clauses params clauses arity_clauses =
16.413 - let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) SFC.init_functab)
16.414 + let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) init_functab)
16.415 val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
16.416 val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
16.417 in
16.418 - (Symtab.dest (List.foldl SFC.add_arityClause_funcs functab arity_clauses),
16.419 + (Symtab.dest (List.foldl add_arity_clause_funcs functab arity_clauses),
16.420 Symtab.dest predtab)
16.421 end;
16.422
16.423 -fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
16.424 - List.foldl SFC.add_type_sort_preds preds ctypes_sorts
16.425 +fun add_clause_preds (HOLClause {ctypes_sorts, ...}, preds) =
16.426 + List.foldl add_type_sort_preds preds ctypes_sorts
16.427 handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
16.428
16.429 (*Higher-order clauses have only the predicates hBOOL and type classes.*)
16.430 fun preds_of_clauses clauses clsrel_clauses arity_clauses =
16.431 Symtab.dest
16.432 - (List.foldl SFC.add_classrelClause_preds
16.433 - (List.foldl SFC.add_arityClause_preds
16.434 + (List.foldl add_classrel_clause_preds
16.435 + (List.foldl add_arity_clause_preds
16.436 (List.foldl add_clause_preds Symtab.empty clauses)
16.437 arity_clauses)
16.438 clsrel_clauses)
16.439 @@ -385,9 +366,8 @@
16.440 (**********************************************************************)
16.441
16.442 val init_counters =
16.443 - Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
16.444 - ("c_COMBB", 0), ("c_COMBC", 0),
16.445 - ("c_COMBS", 0)];
16.446 + Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
16.447 + ("c_COMBS", 0)];
16.448
16.449 fun count_combterm (CombConst (c, _, _), ct) =
16.450 (case Symtab.lookup ct c of NONE => ct (*no counter*)
16.451 @@ -397,18 +377,18 @@
16.452
16.453 fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
16.454
16.455 -fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals;
16.456 +fun count_clause (HOLClause {literals, ...}, ct) =
16.457 + List.foldl count_literal ct literals;
16.458
16.459 -fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
16.460 +fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}, ct) =
16.461 if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
16.462 else ct;
16.463
16.464 -fun cnf_helper_thms thy =
16.465 - Sledgehammer_Fact_Preprocessor.cnf_rules_pairs thy
16.466 - o map Sledgehammer_Fact_Preprocessor.pairname
16.467 +fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname
16.468
16.469 fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
16.470 - if isFO then [] (*first-order*)
16.471 + if isFO then
16.472 + []
16.473 else
16.474 let
16.475 val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
16.476 @@ -416,15 +396,15 @@
16.477 val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
16.478 fun needed c = the (Symtab.lookup ct c) > 0
16.479 val IK = if needed "c_COMBI" orelse needed "c_COMBK"
16.480 - then cnf_helper_thms thy [comb_I,comb_K]
16.481 + then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
16.482 else []
16.483 val BC = if needed "c_COMBB" orelse needed "c_COMBC"
16.484 - then cnf_helper_thms thy [comb_B,comb_C]
16.485 + then cnf_helper_thms thy [@{thm COMBB_def}, @{thm COMBC_def}]
16.486 else []
16.487 - val S = if needed "c_COMBS"
16.488 - then cnf_helper_thms thy [comb_S]
16.489 + val S = if needed "c_COMBS" then cnf_helper_thms thy [@{thm COMBS_def}]
16.490 else []
16.491 - val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
16.492 + val other = cnf_helper_thms thy [@{thm fequal_imp_equal},
16.493 + @{thm equal_imp_fequal}]
16.494 in
16.495 map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
16.496 end;
16.497 @@ -432,7 +412,7 @@
16.498 (*Find the minimal arity of each function mentioned in the term. Also, note which uses
16.499 are not at top level, to see if hBOOL is needed.*)
16.500 fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
16.501 - let val (head, args) = strip_comb t
16.502 + let val (head, args) = strip_combterm_comb t
16.503 val n = length args
16.504 val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
16.505 in
16.506 @@ -451,11 +431,12 @@
16.507 fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
16.508 count_constants_term true t (const_min_arity, const_needs_hBOOL);
16.509
16.510 -fun count_constants_clause (Clause{literals,...}) (const_min_arity, const_needs_hBOOL) =
16.511 +fun count_constants_clause (HOLClause {literals, ...})
16.512 + (const_min_arity, const_needs_hBOOL) =
16.513 fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
16.514
16.515 fun display_arity const_needs_hBOOL (c,n) =
16.516 - Sledgehammer_Fact_Preprocessor.trace_msg (fn () => "Constant: " ^ c ^
16.517 + trace_msg (fn () => "Constant: " ^ c ^
16.518 " arity:\t" ^ Int.toString n ^
16.519 (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
16.520
16.521 @@ -469,31 +450,31 @@
16.522 in (const_min_arity, const_needs_hBOOL) end
16.523 else (Symtab.empty, Symtab.empty);
16.524
16.525 -(* tptp format *)
16.526 +(* TPTP format *)
16.527
16.528 -fun tptp_write_file t_full file clauses =
16.529 +fun write_tptp_file t_full file clauses =
16.530 let
16.531 val (conjectures, axclauses, _, helper_clauses,
16.532 classrel_clauses, arity_clauses) = clauses
16.533 val (cma, cnh) = count_constants clauses
16.534 val params = (t_full, cma, cnh)
16.535 val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
16.536 - val tfree_clss = map SFC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
16.537 + val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
16.538 val _ =
16.539 File.write_list file (
16.540 map (#1 o (clause2tptp params)) axclauses @
16.541 tfree_clss @
16.542 tptp_clss @
16.543 - map SFC.tptp_classrelClause classrel_clauses @
16.544 - map SFC.tptp_arity_clause arity_clauses @
16.545 + map tptp_classrel_clause classrel_clauses @
16.546 + map tptp_arity_clause arity_clauses @
16.547 map (#1 o (clause2tptp params)) helper_clauses)
16.548 in (length axclauses + 1, length tfree_clss + length tptp_clss)
16.549 end;
16.550
16.551
16.552 -(* dfg format *)
16.553 +(* DFG format *)
16.554
16.555 -fun dfg_write_file t_full file clauses =
16.556 +fun write_dfg_file t_full file clauses =
16.557 let
16.558 val (conjectures, axclauses, _, helper_clauses,
16.559 classrel_clauses, arity_clauses) = clauses
16.560 @@ -502,20 +483,20 @@
16.561 val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
16.562 and probname = Path.implode (Path.base file)
16.563 val axstrs = map (#1 o (clause2dfg params)) axclauses
16.564 - val tfree_clss = map SFC.dfg_tfree_clause (SFC.union_all tfree_litss)
16.565 + val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
16.566 val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
16.567 val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
16.568 and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
16.569 val _ =
16.570 File.write_list file (
16.571 - SFC.string_of_start probname ::
16.572 - SFC.string_of_descrip probname ::
16.573 - SFC.string_of_symbols (SFC.string_of_funcs funcs)
16.574 - (SFC.string_of_preds (cl_preds @ ty_preds)) ::
16.575 + string_of_start probname ::
16.576 + string_of_descrip probname ::
16.577 + string_of_symbols (string_of_funcs funcs)
16.578 + (string_of_preds (cl_preds @ ty_preds)) ::
16.579 "list_of_clauses(axioms,cnf).\n" ::
16.580 axstrs @
16.581 - map SFC.dfg_classrelClause classrel_clauses @
16.582 - map SFC.dfg_arity_clause arity_clauses @
16.583 + map dfg_classrel_clause classrel_clauses @
16.584 + map dfg_arity_clause arity_clauses @
16.585 helper_clauses_strs @
16.586 ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
16.587 tfree_clss @
16.588 @@ -530,4 +511,3 @@
16.589 end;
16.590
16.591 end;
16.592 -
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 22 10:25:44 2010 +0100
17.3 @@ -0,0 +1,87 @@
17.4 +(* Title: HOL/Sledgehammer/sledgehammer_isar.ML
17.5 + Author: Jasmin Blanchette, TU Muenchen
17.6 +
17.7 +Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
17.8 +*)
17.9 +
17.10 +structure Sledgehammer_Isar : sig end =
17.11 +struct
17.12 +
17.13 +open ATP_Manager
17.14 +open ATP_Minimal
17.15 +
17.16 +structure K = OuterKeyword and P = OuterParse
17.17 +
17.18 +val _ =
17.19 + OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
17.20 + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
17.21 +
17.22 +val _ =
17.23 + OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
17.24 + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
17.25 +
17.26 +val _ =
17.27 + OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
17.28 + (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
17.29 + (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
17.30 +
17.31 +val _ =
17.32 + OuterSyntax.improper_command "print_atps" "print external provers" K.diag
17.33 + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
17.34 + Toplevel.keep (print_provers o Toplevel.theory_of)));
17.35 +
17.36 +val _ =
17.37 + OuterSyntax.command "sledgehammer"
17.38 + "search for first-order proof using automatic theorem provers" K.diag
17.39 + (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
17.40 + Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
17.41 +
17.42 +val default_minimize_prover = "remote_vampire"
17.43 +val default_minimize_time_limit = 5
17.44 +
17.45 +fun atp_minimize_command args thm_names state =
17.46 + let
17.47 + fun theorems_from_names ctxt =
17.48 + map (fn (name, interval) =>
17.49 + let
17.50 + val thmref = Facts.Named ((name, Position.none), interval)
17.51 + val ths = ProofContext.get_fact ctxt thmref
17.52 + val name' = Facts.string_of_ref thmref
17.53 + in (name', ths) end)
17.54 + fun get_time_limit_arg time_string =
17.55 + (case Int.fromString time_string of
17.56 + SOME t => t
17.57 + | NONE => error ("Invalid time limit: " ^ quote time_string))
17.58 + fun get_opt (name, a) (p, t) =
17.59 + (case name of
17.60 + "time" => (p, get_time_limit_arg a)
17.61 + | "atp" => (a, t)
17.62 + | n => error ("Invalid argument: " ^ n))
17.63 + fun get_options args =
17.64 + fold get_opt args (default_minimize_prover, default_minimize_time_limit)
17.65 + val (prover_name, time_limit) = get_options args
17.66 + val prover =
17.67 + (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
17.68 + SOME prover => prover
17.69 + | NONE => error ("Unknown prover: " ^ quote prover_name))
17.70 + val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
17.71 + in
17.72 + writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
17.73 + state name_thms_pairs))
17.74 + end
17.75 +
17.76 +local structure K = OuterKeyword and P = OuterParse in
17.77 +
17.78 +val parse_args =
17.79 + Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
17.80 +val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
17.81 +
17.82 +val _ =
17.83 + OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
17.84 + (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
17.85 + Toplevel.no_timing o Toplevel.unknown_proof o
17.86 + Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
17.87 +
17.88 +end
17.89 +
17.90 +end;
18.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Mar 22 09:54:22 2010 +0100
18.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Mar 22 10:25:44 2010 +0100
18.3 @@ -7,33 +7,29 @@
18.4 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
18.5 sig
18.6 val chained_hint: string
18.7 -
18.8 - val fix_sorts: sort Vartab.table -> term -> term
18.9 val invert_const: string -> string
18.10 val invert_type_const: string -> string
18.11 val num_typargs: theory -> string -> int
18.12 val make_tvar: string -> typ
18.13 val strip_prefix: string -> string -> string option
18.14 val setup: theory -> theory
18.15 - (* extracting lemma list*)
18.16 - val find_failure: string -> string option
18.17 - val lemma_list: bool -> string ->
18.18 + val is_proof_well_formed: string -> bool
18.19 + val metis_lemma_list: bool -> string ->
18.20 string * string vector * (int * int) * Proof.context * thm * int -> string * string list
18.21 - (* structured proofs *)
18.22 - val structured_proof: string ->
18.23 + val structured_isar_proof: string ->
18.24 string * string vector * (int * int) * Proof.context * thm * int -> string * string list
18.25 end;
18.26
18.27 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
18.28 struct
18.29
18.30 -structure SFC = Sledgehammer_FOL_Clause
18.31 +open Sledgehammer_FOL_Clause
18.32 +open Sledgehammer_Fact_Preprocessor
18.33
18.34 -val trace_path = Path.basic "atp_trace";
18.35 +val trace_proof_path = Path.basic "atp_trace";
18.36
18.37 -fun trace s =
18.38 - if ! Sledgehammer_Fact_Preprocessor.trace then File.append (File.tmp_path trace_path) s
18.39 - else ();
18.40 +fun trace_proof_msg f =
18.41 + if !trace then File.append (File.tmp_path trace_proof_path) (f ()) else ();
18.42
18.43 fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
18.44
18.45 @@ -43,9 +39,6 @@
18.46 (*Indicates whether to include sort information in generated proofs*)
18.47 val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true;
18.48
18.49 -(*Indicated whether to generate full proofs or just lemma lists - now via setup of atps*)
18.50 -(* val (full_proofs, full_proofs_setup) = Attrib.config_bool "sledgehammer_full" false; *)
18.51 -
18.52 val setup = modulus_setup #> recon_sorts_setup;
18.53
18.54 (**** PARSING OF TSTP FORMAT ****)
18.55 @@ -109,12 +102,12 @@
18.56 (*If string s has the prefix s1, return the result of deleting it.*)
18.57 fun strip_prefix s1 s =
18.58 if String.isPrefix s1 s
18.59 - then SOME (SFC.undo_ascii_of (String.extract (s, size s1, NONE)))
18.60 + then SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
18.61 else NONE;
18.62
18.63 (*Invert the table of translations between Isabelle and ATPs*)
18.64 val type_const_trans_table_inv =
18.65 - Symtab.make (map swap (Symtab.dest SFC.type_const_trans_table));
18.66 + Symtab.make (map swap (Symtab.dest type_const_trans_table));
18.67
18.68 fun invert_type_const c =
18.69 case Symtab.lookup type_const_trans_table_inv c of
18.70 @@ -132,15 +125,15 @@
18.71 | Br (a,ts) =>
18.72 let val Ts = map type_of_stree ts
18.73 in
18.74 - case strip_prefix SFC.tconst_prefix a of
18.75 + case strip_prefix tconst_prefix a of
18.76 SOME b => Type(invert_type_const b, Ts)
18.77 | NONE =>
18.78 if not (null ts) then raise STREE t (*only tconsts have type arguments*)
18.79 else
18.80 - case strip_prefix SFC.tfree_prefix a of
18.81 + case strip_prefix tfree_prefix a of
18.82 SOME b => TFree("'" ^ b, HOLogic.typeS)
18.83 | NONE =>
18.84 - case strip_prefix SFC.tvar_prefix a of
18.85 + case strip_prefix tvar_prefix a of
18.86 SOME b => make_tvar b
18.87 | NONE => make_tvar a (*Variable from the ATP, say X1*)
18.88 end;
18.89 @@ -148,7 +141,7 @@
18.90 (*Invert the table of translations between Isabelle and ATPs*)
18.91 val const_trans_table_inv =
18.92 Symtab.update ("fequal", "op =")
18.93 - (Symtab.make (map swap (Symtab.dest SFC.const_trans_table)));
18.94 + (Symtab.make (map swap (Symtab.dest const_trans_table)));
18.95
18.96 fun invert_const c =
18.97 case Symtab.lookup const_trans_table_inv c of
18.98 @@ -169,9 +162,9 @@
18.99 | Br ("hBOOL",[t]) => term_of_stree [] thy t (*ignore hBOOL*)
18.100 | Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t
18.101 | Br (a,ts) =>
18.102 - case strip_prefix SFC.const_prefix a of
18.103 + case strip_prefix const_prefix a of
18.104 SOME "equal" =>
18.105 - list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
18.106 + list_comb(Const (@{const_name "op ="}, HOLogic.typeT), List.map (term_of_stree [] thy) ts)
18.107 | SOME b =>
18.108 let val c = invert_const b
18.109 val nterms = length ts - num_typargs thy c
18.110 @@ -183,10 +176,10 @@
18.111 | NONE => (*a variable, not a constant*)
18.112 let val T = HOLogic.typeT
18.113 val opr = (*a Free variable is typically a Skolem function*)
18.114 - case strip_prefix SFC.fixed_var_prefix a of
18.115 + case strip_prefix fixed_var_prefix a of
18.116 SOME b => Free(b,T)
18.117 | NONE =>
18.118 - case strip_prefix SFC.schematic_var_prefix a of
18.119 + case strip_prefix schematic_var_prefix a of
18.120 SOME b => make_var (b,T)
18.121 | NONE => make_var (a,T) (*Variable from the ATP, say X1*)
18.122 in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end;
18.123 @@ -196,7 +189,7 @@
18.124 | constraint_of_stree pol t = case t of
18.125 Int _ => raise STREE t
18.126 | Br (a,ts) =>
18.127 - (case (strip_prefix SFC.class_prefix a, map type_of_stree ts) of
18.128 + (case (strip_prefix class_prefix a, map type_of_stree ts) of
18.129 (SOME b, [T]) => (pol, b, T)
18.130 | _ => raise STREE t);
18.131
18.132 @@ -286,7 +279,7 @@
18.133 may disagree. We have to try all combinations of literals (quadratic!) and
18.134 match up the variable names consistently. **)
18.135
18.136 -fun strip_alls_aux n (Const("all",_)$Abs(a,T,t)) =
18.137 +fun strip_alls_aux n (Const(@{const_name all}, _)$Abs(a,T,t)) =
18.138 strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t))
18.139 | strip_alls_aux _ t = t;
18.140
18.141 @@ -340,26 +333,30 @@
18.142 then SOME ctm else perm ctms
18.143 in perm end;
18.144
18.145 -fun have_or_show "show " _ = "show \""
18.146 - | have_or_show have lname = have ^ lname ^ ": \""
18.147 -
18.148 (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
18.149 ATP may have their literals reordered.*)
18.150 -fun isar_lines ctxt ctms =
18.151 - let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term)
18.152 - val _ = trace ("\n\nisar_lines: start\n")
18.153 - fun doline _ (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*)
18.154 - (case permuted_clause t ctms of
18.155 - SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
18.156 - | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n") (*no match!!*)
18.157 - | doline have (lname, t, deps) =
18.158 - have_or_show have lname ^ string_of (gen_all_vars (HOLogic.mk_Trueprop t)) ^
18.159 - "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
18.160 - fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
18.161 - | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
18.162 - in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) dolines end;
18.163 +fun isar_proof_body ctxt ctms =
18.164 + let
18.165 + val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
18.166 + val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt)
18.167 + fun have_or_show "show" _ = "show \""
18.168 + | have_or_show have lname = have ^ " " ^ lname ^ ": \""
18.169 + fun do_line _ (lname, t, []) =
18.170 + (* No deps: it's a conjecture clause, with no proof. *)
18.171 + (case permuted_clause t ctms of
18.172 + SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
18.173 + | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
18.174 + [t]))
18.175 + | do_line have (lname, t, deps) =
18.176 + have_or_show have lname ^
18.177 + string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^
18.178 + "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
18.179 + fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
18.180 + | do_lines ((lname, t, deps) :: lines) =
18.181 + do_line "have" (lname, t, deps) :: do_lines lines
18.182 + in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) do_lines end;
18.183
18.184 -fun notequal t (_,t',_) = not (t aconv t');
18.185 +fun unequal t (_, t', _) = not (t aconv t');
18.186
18.187 (*No "real" literals means only type information*)
18.188 fun eq_types t = t aconv HOLogic.true_const;
18.189 @@ -375,7 +372,7 @@
18.190 if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*)
18.191 then map (replace_deps (lno, [])) lines
18.192 else
18.193 - (case take_prefix (notequal t) lines of
18.194 + (case take_prefix (unequal t) lines of
18.195 (_,[]) => lines (*no repetition of proof line*)
18.196 | (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*)
18.197 pre @ map (replace_deps (lno', [lno])) post)
18.198 @@ -385,7 +382,7 @@
18.199 if eq_types t then (lno, t, deps) :: lines
18.200 (*Type information will be deleted later; skip repetition test.*)
18.201 else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
18.202 - case take_prefix (notequal t) lines of
18.203 + case take_prefix (unequal t) lines of
18.204 (_,[]) => (lno, t, deps) :: lines (*no repetition of proof line*)
18.205 | (pre, (lno', t', _) :: post) =>
18.206 (lno, t', deps) :: (*repetition: replace later line by earlier one*)
18.207 @@ -399,7 +396,7 @@
18.208 | add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines
18.209 and delete_dep lno lines = List.foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines);
18.210
18.211 -fun bad_free (Free (a,_)) = String.isPrefix "sko_" a
18.212 +fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a
18.213 | bad_free _ = false;
18.214
18.215 (*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies.
18.216 @@ -435,39 +432,42 @@
18.217 fun isar_header [] = proofstart
18.218 | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
18.219
18.220 -fun decode_tstp_file cnfs ctxt th sgno thm_names =
18.221 - let val _ = trace "\ndecode_tstp_file: start\n"
18.222 - val tuples = map (dest_tstp o tstp_line o explode) cnfs
18.223 - val _ = trace (Int.toString (length tuples) ^ " tuples extracted\n")
18.224 - val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
18.225 - val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
18.226 - val _ = trace (Int.toString (length raw_lines) ^ " raw_lines extracted\n")
18.227 - val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
18.228 - val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
18.229 - val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
18.230 - val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
18.231 - val (ccls,fixes) = Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th sgno
18.232 - val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
18.233 - val ccls = map forall_intr_vars ccls
18.234 - val _ =
18.235 - if ! Sledgehammer_Fact_Preprocessor.trace then
18.236 - app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
18.237 - else
18.238 - ()
18.239 - val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
18.240 - val _ = trace "\ndecode_tstp_file: finishing\n"
18.241 - in
18.242 - isar_header (map #1 fixes) ^ implode ilines ^ "qed\n"
18.243 - end handle STREE _ => error "Could not extract proof (ATP output malformed?)";
18.244 +fun isar_proof_from_tstp_file cnfs ctxt th sgno thm_names =
18.245 + let
18.246 + val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n")
18.247 + val tuples = map (dest_tstp o tstp_line o explode) cnfs
18.248 + val _ = trace_proof_msg (fn () =>
18.249 + Int.toString (length tuples) ^ " tuples extracted\n")
18.250 + val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
18.251 + val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
18.252 + val _ = trace_proof_msg (fn () =>
18.253 + Int.toString (length raw_lines) ^ " raw_lines extracted\n")
18.254 + val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
18.255 + val _ = trace_proof_msg (fn () =>
18.256 + Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
18.257 + val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
18.258 + val _ = trace_proof_msg (fn () =>
18.259 + Int.toString (length lines) ^ " lines extracted\n")
18.260 + val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno
18.261 + val _ = trace_proof_msg (fn () =>
18.262 + Int.toString (length ccls) ^ " conjecture clauses\n")
18.263 + val ccls = map forall_intr_vars ccls
18.264 + val _ = app (fn th => trace_proof_msg
18.265 + (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
18.266 + val body = isar_proof_body ctxt (map prop_of ccls)
18.267 + (stringify_deps thm_names [] lines)
18.268 + val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
18.269 + in isar_header (map #1 fixes) ^ implode body ^ "qed\n" end
18.270 + handle STREE _ => error "Could not extract proof (ATP output malformed?)";
18.271
18.272
18.273 (*=== EXTRACTING PROOF-TEXT === *)
18.274
18.275 -val begin_proof_strings = ["# SZS output start CNFRefutation.",
18.276 +val begin_proof_strs = ["# SZS output start CNFRefutation.",
18.277 "=========== Refutation ==========",
18.278 "Here is a proof"];
18.279
18.280 -val end_proof_strings = ["# SZS output end CNFRefutation",
18.281 +val end_proof_strs = ["# SZS output end CNFRefutation",
18.282 "======= End of refutation =======",
18.283 "Formulae used in the proof"];
18.284
18.285 @@ -475,8 +475,8 @@
18.286 let
18.287 (*splits to_split by the first possible of a list of splitters*)
18.288 val (begin_string, end_string) =
18.289 - (find_first (fn s => String.isSubstring s proof) begin_proof_strings,
18.290 - find_first (fn s => String.isSubstring s proof) end_proof_strings)
18.291 + (find_first (fn s => String.isSubstring s proof) begin_proof_strs,
18.292 + find_first (fn s => String.isSubstring s proof) end_proof_strs)
18.293 in
18.294 if is_none begin_string orelse is_none end_string
18.295 then error "Could not extract proof (no substring indicating a proof)"
18.296 @@ -484,36 +484,24 @@
18.297 |> first_field (the end_string) |> the |> fst
18.298 end;
18.299
18.300 -(* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
18.301 +(* ==== CHECK IF PROOF WAS SUCCESSFUL === *)
18.302
18.303 -val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
18.304 - "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
18.305 -val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
18.306 -val failure_strings_SPASS = ["SPASS beiseite: Completion found.",
18.307 - "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."];
18.308 -val failure_strings_remote = ["Remote-script could not extract proof"];
18.309 -fun find_failure proof =
18.310 - let val failures =
18.311 - map_filter (fn s => if String.isSubstring s proof then SOME s else NONE)
18.312 - (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
18.313 - val correct = null failures andalso
18.314 - exists (fn s => String.isSubstring s proof) begin_proof_strings andalso
18.315 - exists (fn s => String.isSubstring s proof) end_proof_strings
18.316 - in
18.317 - if correct then NONE
18.318 - else if null failures then SOME "Output of ATP not in proper format"
18.319 - else SOME (hd failures) end;
18.320 +fun is_proof_well_formed proof =
18.321 + exists (fn s => String.isSubstring s proof) begin_proof_strs andalso
18.322 + exists (fn s => String.isSubstring s proof) end_proof_strs
18.323
18.324 (* === EXTRACTING LEMMAS === *)
18.325 (* lines have the form "cnf(108, axiom, ...",
18.326 the number (108) has to be extracted)*)
18.327 -fun get_step_nums false proofextract =
18.328 - let val toks = String.tokens (not o Char.isAlphaNum)
18.329 - fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
18.330 - | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok
18.331 - | inputno _ = NONE
18.332 - val lines = split_lines proofextract
18.333 - in map_filter (inputno o toks) lines end
18.334 +fun get_step_nums false extract =
18.335 + let
18.336 + val toks = String.tokens (not o Char.isAlphaNum)
18.337 + fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok
18.338 + | inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) =
18.339 + Int.fromString ntok
18.340 + | inputno _ = NONE
18.341 + val lines = split_lines extract
18.342 + in map_filter (inputno o toks) lines end
18.343 (*String contains multiple lines. We want those of the form
18.344 "253[0:Inp] et cetera..."
18.345 A list consisting of the first number in each line is returned. *)
18.346 @@ -527,27 +515,25 @@
18.347 (*extracting lemmas from tstp-output between the lines from above*)
18.348 fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
18.349 let
18.350 - (* get the names of axioms from their numbers*)
18.351 - fun get_axiom_names thm_names step_nums =
18.352 - let
18.353 - val last_axiom = Vector.length thm_names
18.354 - fun is_axiom n = n <= last_axiom
18.355 - fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count
18.356 - fun getname i = Vector.sub(thm_names, i-1)
18.357 - in
18.358 - (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
18.359 - (map getname (filter is_axiom step_nums))),
18.360 - exists is_conj step_nums)
18.361 - end
18.362 - val proofextract = get_proof_extract proof
18.363 - in
18.364 - get_axiom_names thm_names (get_step_nums proofextract)
18.365 - end;
18.366 + (* get the names of axioms from their numbers*)
18.367 + fun get_axiom_names thm_names step_nums =
18.368 + let
18.369 + val last_axiom = Vector.length thm_names
18.370 + fun is_axiom n = n <= last_axiom
18.371 + fun is_conj n = n >= fst conj_count andalso
18.372 + n < fst conj_count + snd conj_count
18.373 + fun getname i = Vector.sub(thm_names, i-1)
18.374 + in
18.375 + (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
18.376 + (map getname (filter is_axiom step_nums))),
18.377 + exists is_conj step_nums)
18.378 + end
18.379 + in get_axiom_names thm_names (get_step_nums (get_proof_extract proof)) end;
18.380
18.381 (*Used to label theorems chained into the sledgehammer call*)
18.382 val chained_hint = "CHAINED";
18.383 -val nochained = filter_out (fn y => y = chained_hint)
18.384 -
18.385 +val kill_chained = filter_out (curry (op =) chained_hint)
18.386 +
18.387 (* metis-command *)
18.388 fun metis_line [] = "apply metis"
18.389 | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
18.390 @@ -555,34 +541,37 @@
18.391 (* atp_minimize [atp=<prover>] <lemmas> *)
18.392 fun minimize_line _ [] = ""
18.393 | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
18.394 - (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^
18.395 - space_implode " " (nochained lemmas))
18.396 + Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
18.397 + space_implode " " (kill_chained lemmas))
18.398
18.399 -fun sendback_metis_nochained lemmas =
18.400 - (Markup.markup Markup.sendback o metis_line) (nochained lemmas)
18.401 -
18.402 -fun lemma_list dfg name result =
18.403 - let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
18.404 - in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
18.405 - (if used_conj then ""
18.406 - else "\nWarning: Goal is provable because context is inconsistent."),
18.407 - nochained lemmas)
18.408 +fun metis_lemma_list dfg name result =
18.409 + let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
18.410 + (Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^
18.411 + minimize_line name lemmas ^
18.412 + (if used_conj then
18.413 + ""
18.414 + else
18.415 + "\nWarning: The goal is provable because the context is inconsistent."),
18.416 + kill_chained lemmas)
18.417 end;
18.418
18.419 -(* === Extracting structured Isar-proof === *)
18.420 -fun structured_proof name (result as (proof, thm_names, conj_count, ctxt, goal, subgoalno)) =
18.421 +fun structured_isar_proof name (result as (proof, thm_names, conj_count, ctxt,
18.422 + goal, subgoalno)) =
18.423 let
18.424 - (*Could use split_lines, but it can return blank lines...*)
18.425 - val lines = String.tokens (equal #"\n");
18.426 - val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
18.427 - val proofextract = get_proof_extract proof
18.428 - val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
18.429 - val (one_line_proof, lemma_names) = lemma_list false name result
18.430 - val structured =
18.431 - if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
18.432 - else decode_tstp_file cnfs ctxt goal subgoalno thm_names
18.433 + (* Could use "split_lines", but it can return blank lines *)
18.434 + val lines = String.tokens (equal #"\n");
18.435 + val kill_spaces =
18.436 + String.translate (fn c => if Char.isSpace c then "" else str c)
18.437 + val extract = get_proof_extract proof
18.438 + val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
18.439 + val (one_line_proof, lemma_names) = metis_lemma_list false name result
18.440 + val tokens = String.tokens (fn c => c = #" ") one_line_proof
18.441 + val isar_proof =
18.442 + if member (op =) tokens chained_hint then ""
18.443 + else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
18.444 in
18.445 - (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured, lemma_names)
18.446 -end
18.447 + (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback isar_proof,
18.448 + lemma_names)
18.449 + end
18.450
18.451 end;
19.1 --- a/src/HOL/Tools/meson.ML Mon Mar 22 09:54:22 2010 +0100
19.2 +++ b/src/HOL/Tools/meson.ML Mon Mar 22 10:25:44 2010 +0100
19.3 @@ -18,6 +18,7 @@
19.4 val make_nnf: Proof.context -> thm -> thm
19.5 val skolemize: Proof.context -> thm -> thm
19.6 val is_fol_term: theory -> term -> bool
19.7 + val make_clauses_unsorted: thm list -> thm list
19.8 val make_clauses: thm list -> thm list
19.9 val make_horns: thm list -> thm list
19.10 val best_prolog_tac: (thm -> int) -> thm list -> tactic
19.11 @@ -560,7 +561,8 @@
19.12
19.13 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
19.14 The resulting clauses are HOL disjunctions.*)
19.15 -fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []);
19.16 +fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
19.17 +val make_clauses = sort_clauses o make_clauses_unsorted;
19.18
19.19 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
19.20 fun make_horns ths =