1.1 --- a/src/HOL/IsaMakefile Fri Mar 19 06:14:37 2010 +0100
1.2 +++ b/src/HOL/IsaMakefile Fri Mar 19 13:02:18 2010 +0100
1.3 @@ -314,6 +314,7 @@
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 \
2.1 --- a/src/HOL/Sledgehammer.thy Fri Mar 19 06:14:37 2010 +0100
2.2 +++ b/src/HOL/Sledgehammer.thy Fri Mar 19 13:02:18 2010 +0100
2.3 @@ -1,7 +1,8 @@
2.4 (* Title: HOL/Sledgehammer.thy
2.5 Author: Lawrence C Paulson
2.6 Author: Jia Meng, NICTA
2.7 - Author: Fabian Immler, TUM
2.8 + Author: Fabian Immler, TU Muenchen
2.9 + Author: Jasmin Blanchette, TU Muenchen
2.10 *)
2.11
2.12 header {* Sledgehammer: Isabelle--ATP Linkup *}
2.13 @@ -10,7 +11,8 @@
2.14 imports Plain Hilbert_Choice
2.15 uses
2.16 "Tools/polyhash.ML"
2.17 - "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
2.18 + "~~/src/Tools/Metis/metis.ML"
2.19 + ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
2.20 ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
2.21 ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
2.22 ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
2.23 @@ -18,79 +20,79 @@
2.24 ("Tools/ATP_Manager/atp_manager.ML")
2.25 ("Tools/ATP_Manager/atp_wrapper.ML")
2.26 ("Tools/ATP_Manager/atp_minimal.ML")
2.27 - "~~/src/Tools/Metis/metis.ML"
2.28 + ("Tools/Sledgehammer/meson_tactic.ML")
2.29 ("Tools/Sledgehammer/metis_tactics.ML")
2.30 begin
2.31
2.32 -definition COMBI :: "'a => 'a"
2.33 - where "COMBI P == P"
2.34 +definition COMBI :: "'a \<Rightarrow> 'a"
2.35 + where "COMBI P \<equiv> P"
2.36
2.37 -definition COMBK :: "'a => 'b => 'a"
2.38 - where "COMBK P Q == P"
2.39 +definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
2.40 + where "COMBK P Q \<equiv> P"
2.41
2.42 -definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
2.43 - where "COMBB P Q R == P (Q R)"
2.44 +definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
2.45 + where "COMBB P Q R \<equiv> P (Q R)"
2.46
2.47 -definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
2.48 - where "COMBC P Q R == P R Q"
2.49 +definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
2.50 + where "COMBC P Q R \<equiv> P R Q"
2.51
2.52 -definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
2.53 - where "COMBS P Q R == P R (Q R)"
2.54 +definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
2.55 + where "COMBS P Q R \<equiv> P R (Q R)"
2.56
2.57 -definition fequal :: "'a => 'a => bool"
2.58 - where "fequal X Y == (X=Y)"
2.59 +definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
2.60 + where "fequal X Y \<equiv> (X = Y)"
2.61
2.62 -lemma fequal_imp_equal: "fequal X Y ==> X=Y"
2.63 +lemma fequal_imp_equal: "fequal X Y \<Longrightarrow> X = Y"
2.64 by (simp add: fequal_def)
2.65
2.66 -lemma equal_imp_fequal: "X=Y ==> fequal X Y"
2.67 +lemma equal_imp_fequal: "X = Y \<Longrightarrow> fequal X Y"
2.68 by (simp add: fequal_def)
2.69
2.70 text{*These two represent the equivalence between Boolean equality and iff.
2.71 They can't be converted to clauses automatically, as the iff would be
2.72 expanded...*}
2.73
2.74 -lemma iff_positive: "P | Q | P=Q"
2.75 +lemma iff_positive: "P \<or> Q \<or> P = Q"
2.76 by blast
2.77
2.78 -lemma iff_negative: "~P | ~Q | P=Q"
2.79 +lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
2.80 by blast
2.81
2.82 text{*Theorems for translation to combinators*}
2.83
2.84 -lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
2.85 +lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
2.86 apply (rule eq_reflection)
2.87 apply (rule ext)
2.88 apply (simp add: COMBS_def)
2.89 done
2.90
2.91 -lemma abs_I: "(%x. x) == COMBI"
2.92 +lemma abs_I: "\<lambda>x. x \<equiv> COMBI"
2.93 apply (rule eq_reflection)
2.94 apply (rule ext)
2.95 apply (simp add: COMBI_def)
2.96 done
2.97
2.98 -lemma abs_K: "(%x. y) == COMBK y"
2.99 +lemma abs_K: "\<lambda>x. y \<equiv> COMBK y"
2.100 apply (rule eq_reflection)
2.101 apply (rule ext)
2.102 apply (simp add: COMBK_def)
2.103 done
2.104
2.105 -lemma abs_B: "(%x. a (g x)) == COMBB a g"
2.106 +lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g"
2.107 apply (rule eq_reflection)
2.108 apply (rule ext)
2.109 apply (simp add: COMBB_def)
2.110 done
2.111
2.112 -lemma abs_C: "(%x. (f x) b) == COMBC f b"
2.113 +lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b"
2.114 apply (rule eq_reflection)
2.115 apply (rule ext)
2.116 apply (simp add: COMBC_def)
2.117 done
2.118
2.119 -
2.120 subsection {* Setup of external ATPs *}
2.121
2.122 +use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
2.123 use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
2.124 setup Sledgehammer_Fact_Preprocessor.setup
2.125 use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
2.126 @@ -119,7 +121,12 @@
2.127 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
2.128 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
2.129 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
2.130 -
2.131 +
2.132 +
2.133 +subsection {* The MESON prover *}
2.134 +
2.135 +use "Tools/Sledgehammer/meson_tactic.ML"
2.136 +setup Meson_Tactic.setup
2.137
2.138
2.139 subsection {* The Metis prover *}
3.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 06:14:37 2010 +0100
3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 13:02:18 2010 +0100
3.3 @@ -20,7 +20,7 @@
3.4 val sledgehammer: string list -> Proof.state -> unit
3.5 end;
3.6
3.7 -structure ATP_Manager: ATP_MANAGER =
3.8 +structure ATP_Manager : ATP_MANAGER =
3.9 struct
3.10
3.11 (** preferences **)
3.12 @@ -263,7 +263,7 @@
3.13 val _ = register birth_time death_time (Thread.self (), desc);
3.14 val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
3.15 val message = #message (prover (! timeout) problem)
3.16 - handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => (* FIXME !? *)
3.17 + handle Sledgehammer_HOL_Clause.TRIVIAL => (* FIXME !? *)
3.18 "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
3.19 | ERROR msg => ("Error: " ^ msg);
3.20 val _ = unregister message (Thread.self ());
4.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 06:14:37 2010 +0100
4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 13:02:18 2010 +0100
4.3 @@ -14,7 +14,7 @@
4.4 (string * thm list) list -> ((string * thm list) list * int) option * string
4.5 end
4.6
4.7 -structure ATP_Minimal: ATP_MINIMAL =
4.8 +structure ATP_Minimal : ATP_MINIMAL =
4.9 struct
4.10
4.11 (* Linear minimization *)
4.12 @@ -170,7 +170,7 @@
4.13 (NONE, "Error in prover: " ^ msg)
4.14 | (Failure, _) =>
4.15 (NONE, "Failure: No proof with the theorems supplied"))
4.16 - handle Sledgehammer_HOL_Clause.TOO_TRIVIAL =>
4.17 + handle Sledgehammer_HOL_Clause.TRIVIAL =>
4.18 (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
4.19 | ERROR msg => (NONE, "Error: " ^ msg)
4.20 end
5.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 06:14:37 2010 +0100
5.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 13:02:18 2010 +0100
5.3 @@ -16,6 +16,7 @@
5.4 type prover_config =
5.5 {command: Path.T,
5.6 arguments: int -> string,
5.7 + failure_strs: string list,
5.8 max_new_clauses: int,
5.9 insert_theory_const: bool,
5.10 emit_structured_proof: bool}
5.11 @@ -49,11 +50,12 @@
5.12 val refresh_systems: unit -> unit
5.13 end;
5.14
5.15 -structure ATP_Wrapper: ATP_WRAPPER =
5.16 +structure ATP_Wrapper : ATP_WRAPPER =
5.17 struct
5.18
5.19 -structure SFF = Sledgehammer_Fact_Filter
5.20 -structure SPR = Sledgehammer_Proof_Reconstruct
5.21 +open Sledgehammer_HOL_Clause
5.22 +open Sledgehammer_Fact_Filter
5.23 +open Sledgehammer_Proof_Reconstruct
5.24
5.25 (** generic ATP wrapper **)
5.26
5.27 @@ -76,6 +78,7 @@
5.28 type prover_config =
5.29 {command: Path.T,
5.30 arguments: int -> string,
5.31 + failure_strs: string list,
5.32 max_new_clauses: int,
5.33 insert_theory_const: bool,
5.34 emit_structured_proof: bool};
5.35 @@ -114,13 +117,20 @@
5.36 |> Exn.release
5.37 |> tap (after path);
5.38
5.39 -fun external_prover relevance_filter prepare write cmd args produce_answer name
5.40 - ({with_full_types, subgoal, goal, axiom_clauses, filtered_clauses}: problem) =
5.41 +fun find_failure strs proof =
5.42 + case filter (fn s => String.isSubstring s proof) strs of
5.43 + [] => if is_proof_well_formed proof then NONE
5.44 + else SOME "Ill-formed ATP output"
5.45 + | (failure :: _) => SOME failure
5.46 +
5.47 +fun external_prover relevance_filter prepare write cmd args failure_strs
5.48 + produce_answer name ({with_full_types, subgoal, goal, axiom_clauses,
5.49 + filtered_clauses}: problem) =
5.50 let
5.51 (* get clauses and prepare them for writing *)
5.52 val (ctxt, (chain_ths, th)) = goal;
5.53 val thy = ProofContext.theory_of ctxt;
5.54 - val chain_ths = map (Thm.put_name_hint SPR.chained_hint) chain_ths;
5.55 + val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
5.56 val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal);
5.57 val the_filtered_clauses =
5.58 (case filtered_clauses of
5.59 @@ -184,7 +194,7 @@
5.60 with_path cleanup export run_on (prob_pathname subgoal);
5.61
5.62 (* check for success and print out some information on failure *)
5.63 - val failure = SPR.find_failure proof;
5.64 + val failure = find_failure failure_strs proof;
5.65 val success = rc = 0 andalso is_none failure;
5.66 val (message, real_thm_names) =
5.67 if is_some failure then ("External prover failed.", [])
5.68 @@ -200,25 +210,16 @@
5.69
5.70 (* generic TPTP-based provers *)
5.71
5.72 -fun gen_tptp_prover (name, prover_config) timeout problem =
5.73 - let
5.74 - val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} =
5.75 - prover_config;
5.76 - in
5.77 - external_prover
5.78 - (SFF.get_relevant max_new_clauses insert_theory_const)
5.79 - (SFF.prepare_clauses false)
5.80 - Sledgehammer_HOL_Clause.tptp_write_file
5.81 - command
5.82 - (arguments timeout)
5.83 - (if emit_structured_proof then SPR.structured_proof
5.84 - else SPR.lemma_list false)
5.85 - name
5.86 - problem
5.87 - end;
5.88 +fun generic_tptp_prover
5.89 + (name, {command, arguments, failure_strs, max_new_clauses,
5.90 + insert_theory_const, emit_structured_proof}) timeout =
5.91 + external_prover (get_relevant_facts max_new_clauses insert_theory_const)
5.92 + (prepare_clauses false) write_tptp_file command (arguments timeout)
5.93 + failure_strs
5.94 + (if emit_structured_proof then structured_isar_proof
5.95 + else metis_lemma_list false) name;
5.96
5.97 -fun tptp_prover (name, config) = (name, gen_tptp_prover (name, config));
5.98 -
5.99 +fun tptp_prover (name, p) = (name, generic_tptp_prover (name, p));
5.100
5.101
5.102 (** common provers **)
5.103 @@ -227,6 +228,8 @@
5.104
5.105 (*NB: Vampire does not work without explicit timelimit*)
5.106
5.107 +val vampire_failure_strs =
5.108 + ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
5.109 val vampire_max_new_clauses = 60;
5.110 val vampire_insert_theory_const = false;
5.111
5.112 @@ -234,6 +237,7 @@
5.113 {command = Path.explode "$VAMPIRE_HOME/vampire",
5.114 arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
5.115 " -t " ^ string_of_int timeout),
5.116 + failure_strs = vampire_failure_strs,
5.117 max_new_clauses = vampire_max_new_clauses,
5.118 insert_theory_const = vampire_insert_theory_const,
5.119 emit_structured_proof = full};
5.120 @@ -244,6 +248,10 @@
5.121
5.122 (* E prover *)
5.123
5.124 +val eprover_failure_strs =
5.125 + ["SZS status: Satisfiable", "SZS status Satisfiable",
5.126 + "SZS status: ResourceOut", "SZS status ResourceOut",
5.127 + "# Cannot determine problem status"];
5.128 val eprover_max_new_clauses = 100;
5.129 val eprover_insert_theory_const = false;
5.130
5.131 @@ -251,6 +259,7 @@
5.132 {command = Path.explode "$E_HOME/eproof",
5.133 arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
5.134 " --silent --cpu-limit=" ^ string_of_int timeout),
5.135 + failure_strs = eprover_failure_strs,
5.136 max_new_clauses = eprover_max_new_clauses,
5.137 insert_theory_const = eprover_insert_theory_const,
5.138 emit_structured_proof = full};
5.139 @@ -261,6 +270,9 @@
5.140
5.141 (* SPASS *)
5.142
5.143 +val spass_failure_strs =
5.144 + ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
5.145 + "SPASS beiseite: Maximal number of loops exceeded."];
5.146 val spass_max_new_clauses = 40;
5.147 val spass_insert_theory_const = true;
5.148
5.149 @@ -268,26 +280,25 @@
5.150 {command = Path.explode "$SPASS_HOME/SPASS",
5.151 arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
5.152 " -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout),
5.153 + failure_strs = spass_failure_strs,
5.154 max_new_clauses = spass_max_new_clauses,
5.155 insert_theory_const = insert_theory_const,
5.156 emit_structured_proof = false};
5.157
5.158 -fun gen_dfg_prover (name, prover_config: prover_config) timeout problem =
5.159 - let
5.160 - val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config;
5.161 - in
5.162 - external_prover
5.163 - (SFF.get_relevant max_new_clauses insert_theory_const)
5.164 - (SFF.prepare_clauses true)
5.165 - Sledgehammer_HOL_Clause.dfg_write_file
5.166 - command
5.167 - (arguments timeout)
5.168 - (SPR.lemma_list true)
5.169 - name
5.170 - problem
5.171 - end;
5.172 +fun generic_dfg_prover
5.173 + (name, ({command, arguments, failure_strs, max_new_clauses,
5.174 + insert_theory_const, ...} : prover_config)) timeout =
5.175 + external_prover
5.176 + (get_relevant_facts max_new_clauses insert_theory_const)
5.177 + (prepare_clauses true)
5.178 + write_dfg_file
5.179 + command
5.180 + (arguments timeout)
5.181 + failure_strs
5.182 + (metis_lemma_list true)
5.183 + name;
5.184
5.185 -fun dfg_prover (name, config) = (name, gen_dfg_prover (name, config));
5.186 +fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
5.187
5.188 val spass = dfg_prover ("spass", spass_config spass_insert_theory_const);
5.189 val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false);
5.190 @@ -316,10 +327,13 @@
5.191 NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP")
5.192 | SOME sys => sys);
5.193
5.194 +val remote_failure_strs = ["Remote-script could not extract proof"];
5.195 +
5.196 fun remote_prover_config prover_prefix args max_new insert_tc: prover_config =
5.197 {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
5.198 - arguments =
5.199 - (fn timeout => args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
5.200 + arguments = (fn timeout =>
5.201 + args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
5.202 + failure_strs = remote_failure_strs,
5.203 max_new_clauses = max_new,
5.204 insert_theory_const = insert_tc,
5.205 emit_structured_proof = false};
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Fri Mar 19 13:02:18 2010 +0100
6.3 @@ -0,0 +1,53 @@
6.4 +(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML
6.5 + Author: Jia Meng, Cambridge University Computer Laboratory
6.6 +
6.7 +MESON general tactic and proof method.
6.8 +*)
6.9 +
6.10 +signature MESON_TACTIC =
6.11 +sig
6.12 + val expand_defs_tac : thm -> tactic
6.13 + val meson_general_tac : Proof.context -> thm list -> int -> tactic
6.14 + val setup: theory -> theory
6.15 +end;
6.16 +
6.17 +structure Meson_Tactic : MESON_TACTIC =
6.18 +struct
6.19 +
6.20 +open Sledgehammer_Fact_Preprocessor
6.21 +
6.22 +(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
6.23 +fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ u) =
6.24 + String.isPrefix skolem_prefix a
6.25 + | is_absko _ = false;
6.26 +
6.27 +fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ u) = (*Definition of Free, not in certain terms*)
6.28 + is_Free t andalso not (member (op aconv) xs t)
6.29 + | is_okdef _ _ = false
6.30 +
6.31 +(*This function tries to cope with open locales, which introduce hypotheses of the form
6.32 + Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
6.33 + of sko_ functions. *)
6.34 +fun expand_defs_tac st0 st =
6.35 + let val hyps0 = #hyps (rep_thm st0)
6.36 + val hyps = #hyps (crep_thm st)
6.37 + val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
6.38 + val defs = filter (is_absko o Thm.term_of) newhyps
6.39 + val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
6.40 + (map Thm.term_of hyps)
6.41 + val fixed = OldTerm.term_frees (concl_of st) @
6.42 + fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
6.43 + in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
6.44 +
6.45 +fun meson_general_tac ctxt ths i st0 =
6.46 + let
6.47 + val thy = ProofContext.theory_of ctxt
6.48 + val ctxt0 = Classical.put_claset HOL_cs ctxt
6.49 + in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
6.50 +
6.51 +val setup =
6.52 + Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
6.53 + SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
6.54 + "MESON resolution proof procedure";
6.55 +
6.56 +end;
7.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Mar 19 06:14:37 2010 +0100
7.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Mar 19 13:02:18 2010 +0100
7.3 @@ -18,9 +18,11 @@
7.4 structure Metis_Tactics : METIS_TACTICS =
7.5 struct
7.6
7.7 -structure SFC = Sledgehammer_FOL_Clause
7.8 -structure SHC = Sledgehammer_HOL_Clause
7.9 -structure SPR = Sledgehammer_Proof_Reconstruct
7.10 +open Sledgehammer_FOL_Clause
7.11 +open Sledgehammer_Fact_Preprocessor
7.12 +open Sledgehammer_HOL_Clause
7.13 +open Sledgehammer_Proof_Reconstruct
7.14 +open Sledgehammer_Fact_Filter
7.15
7.16 val trace = Unsynchronized.ref false;
7.17 fun trace_msg msg = if !trace then tracing (msg ()) else ();
7.18 @@ -67,62 +69,62 @@
7.19
7.20 fun metis_lit b c args = (b, (c, args));
7.21
7.22 -fun hol_type_to_fol (SFC.AtomV x) = Metis.Term.Var x
7.23 - | hol_type_to_fol (SFC.AtomF x) = Metis.Term.Fn(x,[])
7.24 - | hol_type_to_fol (SFC.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
7.25 +fun hol_type_to_fol (AtomV x) = Metis.Term.Var x
7.26 + | hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, [])
7.27 + | hol_type_to_fol (Comp (tc, tps)) =
7.28 + Metis.Term.Fn (tc, map hol_type_to_fol tps);
7.29
7.30 (*These two functions insert type literals before the real literals. That is the
7.31 opposite order from TPTP linkup, but maybe OK.*)
7.32
7.33 fun hol_term_to_fol_FO tm =
7.34 - case SHC.strip_comb tm of
7.35 - (SHC.CombConst(c,_,tys), tms) =>
7.36 + case strip_combterm_comb tm of
7.37 + (CombConst(c,_,tys), tms) =>
7.38 let val tyargs = map hol_type_to_fol tys
7.39 val args = map hol_term_to_fol_FO tms
7.40 in Metis.Term.Fn (c, tyargs @ args) end
7.41 - | (SHC.CombVar(v,_), []) => Metis.Term.Var v
7.42 + | (CombVar(v,_), []) => Metis.Term.Var v
7.43 | _ => error "hol_term_to_fol_FO";
7.44
7.45 -fun hol_term_to_fol_HO (SHC.CombVar (a, _)) = Metis.Term.Var a
7.46 - | hol_term_to_fol_HO (SHC.CombConst (a, _, tylist)) =
7.47 +fun hol_term_to_fol_HO (CombVar (a, _)) = Metis.Term.Var a
7.48 + | hol_term_to_fol_HO (CombConst (a, _, tylist)) =
7.49 Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
7.50 - | hol_term_to_fol_HO (SHC.CombApp (tm1, tm2)) =
7.51 + | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
7.52 Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
7.53
7.54 (*The fully-typed translation, to avoid type errors*)
7.55 fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
7.56
7.57 -fun hol_term_to_fol_FT (SHC.CombVar(a, ty)) =
7.58 - wrap_type (Metis.Term.Var a, ty)
7.59 - | hol_term_to_fol_FT (SHC.CombConst(a, ty, _)) =
7.60 +fun hol_term_to_fol_FT (CombVar(a, ty)) = wrap_type (Metis.Term.Var a, ty)
7.61 + | hol_term_to_fol_FT (CombConst(a, ty, _)) =
7.62 wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
7.63 - | hol_term_to_fol_FT (tm as SHC.CombApp(tm1,tm2)) =
7.64 + | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
7.65 wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
7.66 - SHC.type_of_combterm tm);
7.67 + type_of_combterm tm);
7.68
7.69 -fun hol_literal_to_fol FO (SHC.Literal (pol, tm)) =
7.70 - let val (SHC.CombConst(p,_,tys), tms) = SHC.strip_comb tm
7.71 +fun hol_literal_to_fol FO (Literal (pol, tm)) =
7.72 + let val (CombConst(p,_,tys), tms) = strip_combterm_comb tm
7.73 val tylits = if p = "equal" then [] else map hol_type_to_fol tys
7.74 val lits = map hol_term_to_fol_FO tms
7.75 in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
7.76 - | hol_literal_to_fol HO (SHC.Literal (pol, tm)) =
7.77 - (case SHC.strip_comb tm of
7.78 - (SHC.CombConst("equal",_,_), tms) =>
7.79 + | hol_literal_to_fol HO (Literal (pol, tm)) =
7.80 + (case strip_combterm_comb tm of
7.81 + (CombConst("equal",_,_), tms) =>
7.82 metis_lit pol "=" (map hol_term_to_fol_HO tms)
7.83 | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
7.84 - | hol_literal_to_fol FT (SHC.Literal (pol, tm)) =
7.85 - (case SHC.strip_comb tm of
7.86 - (SHC.CombConst("equal",_,_), tms) =>
7.87 + | hol_literal_to_fol FT (Literal (pol, tm)) =
7.88 + (case strip_combterm_comb tm of
7.89 + (CombConst("equal",_,_), tms) =>
7.90 metis_lit pol "=" (map hol_term_to_fol_FT tms)
7.91 | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
7.92
7.93 fun literals_of_hol_thm thy mode t =
7.94 - let val (lits, types_sorts) = SHC.literals_of_term thy t
7.95 + let val (lits, types_sorts) = literals_of_term thy t
7.96 in (map (hol_literal_to_fol mode) lits, types_sorts) end;
7.97
7.98 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
7.99 -fun metis_of_typeLit pos (SFC.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
7.100 - | metis_of_typeLit pos (SFC.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
7.101 +fun metis_of_typeLit pos (LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
7.102 + | metis_of_typeLit pos (LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
7.103
7.104 fun default_sort _ (TVar _) = false
7.105 | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
7.106 @@ -136,10 +138,9 @@
7.107 (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
7.108 in
7.109 if is_conjecture then
7.110 - (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), SFC.add_typs types_sorts)
7.111 + (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), add_typs types_sorts)
7.112 else
7.113 - let val tylits = SFC.add_typs
7.114 - (filter (not o default_sort ctxt) types_sorts)
7.115 + let val tylits = add_typs (filter (not o default_sort ctxt) types_sorts)
7.116 val mtylits = if Config.get ctxt type_lits
7.117 then map (metis_of_typeLit false) tylits else []
7.118 in
7.119 @@ -149,13 +150,13 @@
7.120
7.121 (* ARITY CLAUSE *)
7.122
7.123 -fun m_arity_cls (SFC.TConsLit (c,t,args)) =
7.124 - metis_lit true (SFC.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
7.125 - | m_arity_cls (SFC.TVarLit (c,str)) =
7.126 - metis_lit false (SFC.make_type_class c) [Metis.Term.Var str];
7.127 +fun m_arity_cls (TConsLit (c,t,args)) =
7.128 + metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
7.129 + | m_arity_cls (TVarLit (c,str)) =
7.130 + metis_lit false (make_type_class c) [Metis.Term.Var str];
7.131
7.132 (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
7.133 -fun arity_cls (SFC.ArityClause{conclLit,premLits,...}) =
7.134 +fun arity_cls (ArityClause {conclLit, premLits, ...}) =
7.135 (TrueI,
7.136 Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
7.137
7.138 @@ -164,7 +165,7 @@
7.139 fun m_classrel_cls subclass superclass =
7.140 [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
7.141
7.142 -fun classrel_cls (SFC.ClassrelClause {subclass, superclass, ...}) =
7.143 +fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
7.144 (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
7.145
7.146 (* ------------------------------------------------------------------------- *)
7.147 @@ -213,14 +214,14 @@
7.148 | strip_happ args x = (x, args);
7.149
7.150 fun fol_type_to_isa _ (Metis.Term.Var v) =
7.151 - (case SPR.strip_prefix SFC.tvar_prefix v of
7.152 - SOME w => SPR.make_tvar w
7.153 - | NONE => SPR.make_tvar v)
7.154 + (case strip_prefix tvar_prefix v of
7.155 + SOME w => make_tvar w
7.156 + | NONE => make_tvar v)
7.157 | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
7.158 - (case SPR.strip_prefix SFC.tconst_prefix x of
7.159 - SOME tc => Term.Type (SPR.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
7.160 + (case strip_prefix tconst_prefix x of
7.161 + SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
7.162 | NONE =>
7.163 - case SPR.strip_prefix SFC.tfree_prefix x of
7.164 + case strip_prefix tfree_prefix x of
7.165 SOME tf => mk_tfree ctxt tf
7.166 | NONE => error ("fol_type_to_isa: " ^ x));
7.167
7.168 @@ -229,10 +230,10 @@
7.169 let val thy = ProofContext.theory_of ctxt
7.170 val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
7.171 fun tm_to_tt (Metis.Term.Var v) =
7.172 - (case SPR.strip_prefix SFC.tvar_prefix v of
7.173 - SOME w => Type (SPR.make_tvar w)
7.174 + (case strip_prefix tvar_prefix v of
7.175 + SOME w => Type (make_tvar w)
7.176 | NONE =>
7.177 - case SPR.strip_prefix SFC.schematic_var_prefix v of
7.178 + case strip_prefix schematic_var_prefix v of
7.179 SOME w => Term (mk_var (w, HOLogic.typeT))
7.180 | NONE => Term (mk_var (v, HOLogic.typeT)) )
7.181 (*Var from Metis with a name like _nnn; possibly a type variable*)
7.182 @@ -247,16 +248,16 @@
7.183 end
7.184 | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
7.185 and applic_to_tt ("=",ts) =
7.186 - Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
7.187 + Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
7.188 | applic_to_tt (a,ts) =
7.189 - case SPR.strip_prefix SFC.const_prefix a of
7.190 + case strip_prefix const_prefix a of
7.191 SOME b =>
7.192 - let val c = SPR.invert_const b
7.193 - val ntypes = SPR.num_typargs thy c
7.194 + let val c = invert_const b
7.195 + val ntypes = num_typargs thy c
7.196 val nterms = length ts - ntypes
7.197 val tts = map tm_to_tt ts
7.198 val tys = types_of (List.take(tts,ntypes))
7.199 - val ntyargs = SPR.num_typargs thy c
7.200 + val ntyargs = num_typargs thy c
7.201 in if length tys = ntyargs then
7.202 apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
7.203 else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
7.204 @@ -267,14 +268,14 @@
7.205 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
7.206 end
7.207 | NONE => (*Not a constant. Is it a type constructor?*)
7.208 - case SPR.strip_prefix SFC.tconst_prefix a of
7.209 + case strip_prefix tconst_prefix a of
7.210 SOME b =>
7.211 - Type (Term.Type (SPR.invert_type_const b, types_of (map tm_to_tt ts)))
7.212 + Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
7.213 | NONE => (*Maybe a TFree. Should then check that ts=[].*)
7.214 - case SPR.strip_prefix SFC.tfree_prefix a of
7.215 + case strip_prefix tfree_prefix a of
7.216 SOME b => Type (mk_tfree ctxt b)
7.217 | NONE => (*a fixed variable? They are Skolem functions.*)
7.218 - case SPR.strip_prefix SFC.fixed_var_prefix a of
7.219 + case strip_prefix fixed_var_prefix a of
7.220 SOME b =>
7.221 let val opr = Term.Free(b, HOLogic.typeT)
7.222 in apply_list opr (length ts) (map tm_to_tt ts) end
7.223 @@ -285,16 +286,16 @@
7.224 fun fol_term_to_hol_FT ctxt fol_tm =
7.225 let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
7.226 fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
7.227 - (case SPR.strip_prefix SFC.schematic_var_prefix v of
7.228 + (case strip_prefix schematic_var_prefix v of
7.229 SOME w => mk_var(w, dummyT)
7.230 | NONE => mk_var(v, dummyT))
7.231 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
7.232 Const ("op =", HOLogic.typeT)
7.233 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
7.234 - (case SPR.strip_prefix SFC.const_prefix x of
7.235 - SOME c => Const (SPR.invert_const c, dummyT)
7.236 + (case strip_prefix const_prefix x of
7.237 + SOME c => Const (invert_const c, dummyT)
7.238 | NONE => (*Not a constant. Is it a fixed variable??*)
7.239 - case SPR.strip_prefix SFC.fixed_var_prefix x of
7.240 + case strip_prefix fixed_var_prefix x of
7.241 SOME v => Free (v, fol_type_to_isa ctxt ty)
7.242 | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
7.243 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
7.244 @@ -303,12 +304,12 @@
7.245 cvt tm1 $ cvt tm2
7.246 | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
7.247 | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
7.248 - list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
7.249 + list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
7.250 | cvt (t as Metis.Term.Fn (x, [])) =
7.251 - (case SPR.strip_prefix SFC.const_prefix x of
7.252 - SOME c => Const (SPR.invert_const c, dummyT)
7.253 + (case strip_prefix const_prefix x of
7.254 + SOME c => Const (invert_const c, dummyT)
7.255 | NONE => (*Not a constant. Is it a fixed variable??*)
7.256 - case SPR.strip_prefix SFC.fixed_var_prefix x of
7.257 + case strip_prefix fixed_var_prefix x of
7.258 SOME v => Free (v, dummyT)
7.259 | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
7.260 fol_term_to_hol_RAW ctxt t))
7.261 @@ -331,7 +332,7 @@
7.262 ts'
7.263 in ts' end;
7.264
7.265 -fun mk_not (Const ("Not", _) $ b) = b
7.266 +fun mk_not (Const (@{const_name Not}, _) $ b) = b
7.267 | mk_not b = HOLogic.mk_not b;
7.268
7.269 val metis_eq = Metis.Term.Fn ("=", []);
7.270 @@ -387,9 +388,9 @@
7.271 " in " ^ Display.string_of_thm ctxt i_th);
7.272 NONE)
7.273 fun remove_typeinst (a, t) =
7.274 - case SPR.strip_prefix SFC.schematic_var_prefix a of
7.275 + case strip_prefix schematic_var_prefix a of
7.276 SOME b => SOME (b, t)
7.277 - | NONE => case SPR.strip_prefix SFC.tvar_prefix a of
7.278 + | NONE => case strip_prefix tvar_prefix a of
7.279 SOME _ => NONE (*type instantiations are forbidden!*)
7.280 | NONE => SOME (a,t) (*internal Metis var?*)
7.281 val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
7.282 @@ -455,8 +456,8 @@
7.283 val c_t = cterm_incr_types thy refl_idx i_t
7.284 in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
7.285
7.286 -fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*)
7.287 - | get_ty_arg_size thy (Const (c, _)) = (SPR.num_typargs thy c handle TYPE _ => 0)
7.288 +fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0 (*equality has no type arguments*)
7.289 + | get_ty_arg_size thy (Const (c, _)) = (num_typargs thy c handle TYPE _ => 0)
7.290 | get_ty_arg_size _ _ = 0;
7.291
7.292 (* INFERENCE RULE: EQUALITY *)
7.293 @@ -469,7 +470,7 @@
7.294 | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
7.295 fun path_finder_FO tm [] = (tm, Term.Bound 0)
7.296 | path_finder_FO tm (p::ps) =
7.297 - let val (tm1,args) = Term.strip_comb tm
7.298 + let val (tm1,args) = strip_comb tm
7.299 val adjustment = get_ty_arg_size thy tm1
7.300 val p' = if adjustment > p then p else p-adjustment
7.301 val tm_p = List.nth(args,p')
7.302 @@ -496,13 +497,13 @@
7.303 " isa-term: " ^ Syntax.string_of_term ctxt tm ^
7.304 " fol-term: " ^ Metis.Term.toString t)
7.305 fun path_finder FO tm ps _ = path_finder_FO tm ps
7.306 - | path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ =
7.307 + | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
7.308 (*equality: not curried, as other predicates are*)
7.309 if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
7.310 else path_finder_HO tm (p::ps) (*1 selects second operand*)
7.311 | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
7.312 path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
7.313 - | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps)
7.314 + | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
7.315 (Metis.Term.Fn ("=", [t1,t2])) =
7.316 (*equality: not curried, as other predicates are*)
7.317 if p=0 then path_finder_FT tm (0::1::ps)
7.318 @@ -514,7 +515,7 @@
7.319 | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
7.320 (*if not equality, ignore head to skip the hBOOL predicate*)
7.321 | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
7.322 - fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
7.323 + fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
7.324 let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
7.325 in (tm, nt $ tm_rslt) end
7.326 | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
7.327 @@ -542,7 +543,7 @@
7.328 | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
7.329 equality_inf ctxt mode f_lit f_p f_r;
7.330
7.331 -fun real_literal (_, (c, _)) = not (String.isPrefix SFC.class_prefix c);
7.332 +fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
7.333
7.334 fun translate _ _ thpairs [] = thpairs
7.335 | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
7.336 @@ -568,23 +569,14 @@
7.337 (* Translation of HO Clauses *)
7.338 (* ------------------------------------------------------------------------- *)
7.339
7.340 -fun cnf_th thy th = hd (Sledgehammer_Fact_Preprocessor.cnf_axiom thy th);
7.341 -
7.342 -val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
7.343 -val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
7.344 -
7.345 -val comb_I = cnf_th @{theory} SHC.comb_I;
7.346 -val comb_K = cnf_th @{theory} SHC.comb_K;
7.347 -val comb_B = cnf_th @{theory} SHC.comb_B;
7.348 -val comb_C = cnf_th @{theory} SHC.comb_C;
7.349 -val comb_S = cnf_th @{theory} SHC.comb_S;
7.350 +fun cnf_th thy th = hd (cnf_axiom thy th);
7.351
7.352 fun type_ext thy tms =
7.353 - let val subs = Sledgehammer_Fact_Filter.tfree_classes_of_terms tms
7.354 - val supers = Sledgehammer_Fact_Filter.tvar_classes_of_terms tms
7.355 - and tycons = Sledgehammer_Fact_Filter.type_consts_of_terms thy tms
7.356 - val (supers', arity_clauses) = SFC.make_arity_clauses thy tycons supers
7.357 - val classrel_clauses = SFC.make_classrel_clauses thy subs supers'
7.358 + let val subs = tfree_classes_of_terms tms
7.359 + val supers = tvar_classes_of_terms tms
7.360 + and tycons = type_consts_of_terms thy tms
7.361 + val (supers', arity_clauses) = make_arity_clauses thy tycons supers
7.362 + val classrel_clauses = make_classrel_clauses thy subs supers'
7.363 in map classrel_cls classrel_clauses @ map arity_cls arity_clauses
7.364 end;
7.365
7.366 @@ -593,8 +585,8 @@
7.367 (* ------------------------------------------------------------------------- *)
7.368
7.369 type logic_map =
7.370 - {axioms : (Metis.Thm.thm * thm) list,
7.371 - tfrees : SFC.type_literal list};
7.372 + {axioms: (Metis.Thm.thm * thm) list,
7.373 + tfrees: type_literal list};
7.374
7.375 fun const_in_metis c (pred, tm_list) =
7.376 let
7.377 @@ -606,7 +598,7 @@
7.378 (*Extract TFree constraints from context to include as conjecture clauses*)
7.379 fun init_tfrees ctxt =
7.380 let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
7.381 - in SFC.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
7.382 + in add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
7.383
7.384 (*transform isabelle type / arity clause to metis clause *)
7.385 fun add_type_thm [] lmap = lmap
7.386 @@ -643,12 +635,12 @@
7.387 val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
7.388 fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
7.389 (*Now check for the existence of certain combinators*)
7.390 - val thI = if used "c_COMBI" then [comb_I] else []
7.391 - val thK = if used "c_COMBK" then [comb_K] else []
7.392 - val thB = if used "c_COMBB" then [comb_B] else []
7.393 - val thC = if used "c_COMBC" then [comb_C] else []
7.394 - val thS = if used "c_COMBS" then [comb_S] else []
7.395 - val thEQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
7.396 + val thI = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else []
7.397 + val thK = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else []
7.398 + val thB = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else []
7.399 + val thC = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
7.400 + val thS = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
7.401 + val thEQ = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
7.402 val lmap' = if mode=FO then lmap
7.403 else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
7.404 in
7.405 @@ -668,7 +660,7 @@
7.406 fun FOL_SOLVE mode ctxt cls ths0 =
7.407 let val thy = ProofContext.theory_of ctxt
7.408 val th_cls_pairs =
7.409 - map (fn th => (Thm.get_name_hint th, Sledgehammer_Fact_Preprocessor.cnf_axiom thy th)) ths0
7.410 + map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
7.411 val ths = maps #2 th_cls_pairs
7.412 val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
7.413 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
7.414 @@ -677,7 +669,7 @@
7.415 val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
7.416 val _ = if null tfrees then ()
7.417 else (trace_msg (fn () => "TFREE CLAUSES");
7.418 - app (fn tf => trace_msg (fn _ => SFC.tptp_of_typeLit true tf)) tfrees)
7.419 + app (fn tf => trace_msg (fn _ => tptp_of_typeLit true tf)) tfrees)
7.420 val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
7.421 val thms = map #1 axioms
7.422 val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
7.423 @@ -719,12 +711,12 @@
7.424 let val _ = trace_msg (fn () =>
7.425 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
7.426 in
7.427 - if exists_type Sledgehammer_Fact_Preprocessor.type_has_topsort (prop_of st0)
7.428 + if exists_type type_has_topsort (prop_of st0)
7.429 then raise METIS "Metis: Proof state contains the universal sort {}"
7.430 else
7.431 - (Meson.MESON Sledgehammer_Fact_Preprocessor.neg_clausify
7.432 + (Meson.MESON neg_clausify
7.433 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
7.434 - THEN Sledgehammer_Fact_Preprocessor.expand_defs_tac st0) st0
7.435 + THEN Meson_Tactic.expand_defs_tac st0) st0
7.436 end
7.437 handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
7.438
7.439 @@ -737,11 +729,11 @@
7.440
7.441 val setup =
7.442 type_lits_setup #>
7.443 - method @{binding metis} HO "METIS for FOL & HOL problems" #>
7.444 + method @{binding metis} HO "METIS for FOL and HOL problems" #>
7.445 method @{binding metisF} FO "METIS for FOL problems" #>
7.446 method @{binding metisFT} FT "METIS with fully-typed translation" #>
7.447 Method.setup @{binding finish_clausify}
7.448 - (Scan.succeed (K (SIMPLE_METHOD (Sledgehammer_Fact_Preprocessor.expand_defs_tac refl))))
7.449 + (Scan.succeed (K (SIMPLE_METHOD (Meson_Tactic.expand_defs_tac refl))))
7.450 "cleanup after conversion to clauses";
7.451
7.452 end;
8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Mar 19 06:14:37 2010 +0100
8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Mar 19 13:02:18 2010 +0100
8.3 @@ -4,47 +4,45 @@
8.4
8.5 signature SLEDGEHAMMER_FACT_FILTER =
8.6 sig
8.7 - type classrelClause = Sledgehammer_FOL_Clause.classrelClause
8.8 - type arityClause = Sledgehammer_FOL_Clause.arityClause
8.9 + type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
8.10 + type arity_clause = Sledgehammer_FOL_Clause.arity_clause
8.11 type axiom_name = Sledgehammer_HOL_Clause.axiom_name
8.12 - type clause = Sledgehammer_HOL_Clause.clause
8.13 - type clause_id = Sledgehammer_HOL_Clause.clause_id
8.14 - datatype mode = Auto | Fol | Hol
8.15 + type hol_clause = Sledgehammer_HOL_Clause.hol_clause
8.16 + type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
8.17 val tvar_classes_of_terms : term list -> string list
8.18 val tfree_classes_of_terms : term list -> string list
8.19 val type_consts_of_terms : theory -> term list -> string list
8.20 - val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
8.21 + val get_relevant_facts : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
8.22 (thm * (string * int)) list
8.23 val prepare_clauses : bool -> thm list -> thm list ->
8.24 - (thm * (axiom_name * clause_id)) list ->
8.25 - (thm * (axiom_name * clause_id)) list -> theory ->
8.26 + (thm * (axiom_name * hol_clause_id)) list ->
8.27 + (thm * (axiom_name * hol_clause_id)) list -> theory ->
8.28 axiom_name vector *
8.29 - (clause list * clause list * clause list *
8.30 - clause list * classrelClause list * arityClause list)
8.31 + (hol_clause list * hol_clause list * hol_clause list *
8.32 + hol_clause list * classrel_clause list * arity_clause list)
8.33 end;
8.34
8.35 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
8.36 struct
8.37
8.38 -structure SFC = Sledgehammer_FOL_Clause
8.39 -structure SFP = Sledgehammer_Fact_Preprocessor
8.40 -structure SHC = Sledgehammer_HOL_Clause
8.41 +open Sledgehammer_FOL_Clause
8.42 +open Sledgehammer_Fact_Preprocessor
8.43 +open Sledgehammer_HOL_Clause
8.44
8.45 -type classrelClause = SFC.classrelClause
8.46 -type arityClause = SFC.arityClause
8.47 -type axiom_name = SHC.axiom_name
8.48 -type clause = SHC.clause
8.49 -type clause_id = SHC.clause_id
8.50 +type axiom_name = axiom_name
8.51 +type hol_clause = hol_clause
8.52 +type hol_clause_id = hol_clause_id
8.53
8.54 (********************************************************************)
8.55 (* some settings for both background automatic ATP calling procedure*)
8.56 (* and also explicit ATP invocation methods *)
8.57 (********************************************************************)
8.58
8.59 -(*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
8.60 +(* Translation mode can be auto-detected, or forced to be first-order or
8.61 + higher-order *)
8.62 datatype mode = Auto | Fol | Hol;
8.63
8.64 -val linkup_logic_mode = Auto;
8.65 +val translation_mode = Auto;
8.66
8.67 (*** background linkup ***)
8.68 val run_blacklist_filter = true;
8.69 @@ -59,7 +57,7 @@
8.70 (* Relevance Filtering *)
8.71 (***************************************************************)
8.72
8.73 -fun strip_Trueprop (Const("Trueprop",_) $ t) = t
8.74 +fun strip_Trueprop (@{const Trueprop} $ t) = t
8.75 | strip_Trueprop t = t;
8.76
8.77 (*A surprising number of theorems contain only a few significant constants.
8.78 @@ -79,7 +77,10 @@
8.79 being chosen, but for some reason filtering works better with them listed. The
8.80 logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
8.81 must be within comprehensions.*)
8.82 -val standard_consts = ["Trueprop","==>","all","==","op |","Not","op ="];
8.83 +val standard_consts =
8.84 + [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
8.85 + @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
8.86 + @{const_name "op ="}];
8.87
8.88
8.89 (*** constants with types ***)
8.90 @@ -233,7 +234,7 @@
8.91 end
8.92 handle ConstFree => false
8.93 in
8.94 - case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) =>
8.95 + case tm of @{const Trueprop} $ (Const(@{const_name "op ="}, _) $ lhs $ rhs) =>
8.96 defs lhs rhs
8.97 | _ => false
8.98 end;
8.99 @@ -252,10 +253,10 @@
8.100 let val cls = sort compare_pairs newpairs
8.101 val accepted = List.take (cls, max_new)
8.102 in
8.103 - SFP.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
8.104 + trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
8.105 ", exceeds the limit of " ^ Int.toString (max_new)));
8.106 - SFP.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
8.107 - SFP.trace_msg (fn () => "Actually passed: " ^
8.108 + trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
8.109 + trace_msg (fn () => "Actually passed: " ^
8.110 space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
8.111
8.112 (map #1 accepted, map #1 (List.drop (cls, max_new)))
8.113 @@ -270,7 +271,7 @@
8.114 val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
8.115 val newp = p + (1.0-p) / convergence
8.116 in
8.117 - SFP.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
8.118 + trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
8.119 (map #1 newrels) @
8.120 (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
8.121 end
8.122 @@ -278,12 +279,12 @@
8.123 let val weight = clause_weight ctab rel_consts consts_typs
8.124 in
8.125 if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
8.126 - then (SFP.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
8.127 + then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
8.128 " passes: " ^ Real.toString weight));
8.129 relevant ((ax,weight)::newrels, rejects) axs)
8.130 else relevant (newrels, ax::rejects) axs
8.131 end
8.132 - in SFP.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
8.133 + in trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
8.134 relevant ([],[])
8.135 end;
8.136
8.137 @@ -292,12 +293,12 @@
8.138 then
8.139 let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
8.140 val goal_const_tab = get_goal_consts_typs thy goals
8.141 - val _ = SFP.trace_msg (fn () => ("Initial constants: " ^
8.142 + val _ = trace_msg (fn () => ("Initial constants: " ^
8.143 space_implode ", " (Symtab.keys goal_const_tab)));
8.144 val rels = relevant_clauses max_new thy const_tab (pass_mark)
8.145 goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms)
8.146 in
8.147 - SFP.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
8.148 + trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
8.149 rels
8.150 end
8.151 else axioms;
8.152 @@ -332,7 +333,7 @@
8.153 | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
8.154 | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
8.155
8.156 -fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
8.157 +fun hash_literal (@{const Not} $ P) = Word.notb(hashw_term(P,0w0))
8.158 | hash_literal P = hashw_term(P,0w0);
8.159
8.160 fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t))));
8.161 @@ -351,7 +352,7 @@
8.162 fun make_unique xs =
8.163 let val ht = mk_clause_table 7000
8.164 in
8.165 - SFP.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
8.166 + trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
8.167 app (ignore o Polyhash.peekInsert ht) xs;
8.168 Polyhash.listItems ht
8.169 end;
8.170 @@ -383,7 +384,7 @@
8.171
8.172 val name1 = Facts.extern facts name;
8.173 val name2 = Name_Space.extern full_space name;
8.174 - val ths = filter_out SFP.bad_for_atp ths0;
8.175 + val ths = filter_out bad_for_atp ths0;
8.176 in
8.177 if Facts.is_concealed facts name orelse null ths orelse
8.178 run_blacklist_filter andalso is_package_def name then I
8.179 @@ -403,7 +404,7 @@
8.180
8.181 (*Ignore blacklisted basenames*)
8.182 fun add_multi_names (a, ths) pairs =
8.183 - if (Long_Name.base_name a) mem_string SFP.multi_base_blacklist then pairs
8.184 + if (Long_Name.base_name a) mem_string multi_base_blacklist then pairs
8.185 else add_single_names (a, ths) pairs;
8.186
8.187 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
8.188 @@ -412,12 +413,17 @@
8.189 fun name_thm_pairs ctxt =
8.190 let
8.191 val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
8.192 - val blacklist =
8.193 - if run_blacklist_filter then No_ATPs.get ctxt |> map Thm.prop_of else []
8.194 - fun is_blacklisted (_, th) = member (op =) blacklist (Thm.prop_of th)
8.195 + val ps = [] |> fold add_multi_names mults
8.196 + |> fold add_single_names singles
8.197 in
8.198 - filter_out is_blacklisted
8.199 - (fold add_single_names singles (fold add_multi_names mults []))
8.200 + if run_blacklist_filter then
8.201 + let
8.202 + val blacklist = No_ATPs.get ctxt
8.203 + |> map (`Thm.full_prop_of) |> Termtab.make
8.204 + val is_blacklisted = Termtab.defined blacklist o Thm.full_prop_of o snd
8.205 + in ps |> filter_out is_blacklisted end
8.206 + else
8.207 + ps
8.208 end;
8.209
8.210 fun check_named ("", th) =
8.211 @@ -426,7 +432,7 @@
8.212
8.213 fun get_all_lemmas ctxt =
8.214 let val included_thms =
8.215 - tap (fn ths => SFP.trace_msg
8.216 + tap (fn ths => trace_msg
8.217 (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
8.218 (name_thm_pairs ctxt)
8.219 in
8.220 @@ -440,7 +446,7 @@
8.221 fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts);
8.222
8.223 (*Remove this trivial type class*)
8.224 -fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
8.225 +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
8.226
8.227 fun tvar_classes_of_terms ts =
8.228 let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
8.229 @@ -499,14 +505,10 @@
8.230 fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
8.231 | too_general_eqterms _ = false;
8.232
8.233 -fun too_general_equality (Const ("op =", _) $ x $ y) =
8.234 +fun too_general_equality (Const (@{const_name "op ="}, _) $ x $ y) =
8.235 too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
8.236 | too_general_equality _ = false;
8.237
8.238 -(* tautologous? *)
8.239 -fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
8.240 - | is_taut _ = false;
8.241 -
8.242 fun has_typed_var tycons = exists_subterm
8.243 (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
8.244
8.245 @@ -514,28 +516,29 @@
8.246 they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
8.247 The resulting clause will have no type constraint, yielding false proofs. Even "bool"
8.248 leads to many unsound proofs, though (obviously) only for higher-order problems.*)
8.249 -val unwanted_types = ["Product_Type.unit","bool"];
8.250 +val unwanted_types = [@{type_name unit}, @{type_name bool}];
8.251
8.252 fun unwanted t =
8.253 - is_taut t orelse has_typed_var unwanted_types t orelse
8.254 + t = @{prop True} orelse has_typed_var unwanted_types t orelse
8.255 forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
8.256
8.257 (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
8.258 likely to lead to unsound proofs.*)
8.259 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
8.260
8.261 -fun isFO thy goal_cls = case linkup_logic_mode of
8.262 - Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
8.263 - | Fol => true
8.264 - | Hol => false
8.265 +fun is_first_order thy goal_cls =
8.266 + case translation_mode of
8.267 + Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
8.268 + | Fol => true
8.269 + | Hol => false
8.270
8.271 -fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
8.272 +fun get_relevant_facts max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
8.273 let
8.274 val thy = ProofContext.theory_of ctxt
8.275 - val isFO = isFO thy goal_cls
8.276 + val is_FO = is_first_order thy goal_cls
8.277 val included_cls = get_all_lemmas ctxt
8.278 - |> SFP.cnf_rules_pairs thy |> make_unique
8.279 - |> restrict_to_logic thy isFO
8.280 + |> cnf_rules_pairs thy |> make_unique
8.281 + |> restrict_to_logic thy is_FO
8.282 |> remove_unwanted_clauses
8.283 in
8.284 relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
8.285 @@ -547,28 +550,27 @@
8.286 let
8.287 (* add chain thms *)
8.288 val chain_cls =
8.289 - SFP.cnf_rules_pairs thy (filter check_named (map SFP.pairname chain_ths))
8.290 + cnf_rules_pairs thy (filter check_named (map pairname chain_ths))
8.291 val axcls = chain_cls @ axcls
8.292 val extra_cls = chain_cls @ extra_cls
8.293 - val isFO = isFO thy goal_cls
8.294 + val is_FO = is_first_order thy goal_cls
8.295 val ccls = subtract_cls goal_cls extra_cls
8.296 - val _ = app (fn th => SFP.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
8.297 + val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
8.298 val ccltms = map prop_of ccls
8.299 and axtms = map (prop_of o #1) extra_cls
8.300 val subs = tfree_classes_of_terms ccltms
8.301 and supers = tvar_classes_of_terms axtms
8.302 - and tycons = type_consts_of_terms thy (ccltms@axtms)
8.303 + and tycons = type_consts_of_terms thy (ccltms @ axtms)
8.304 (*TFrees in conjecture clauses; TVars in axiom clauses*)
8.305 - val conjectures = SHC.make_conjecture_clauses dfg thy ccls
8.306 - val (_, extra_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy extra_cls)
8.307 - val (clnames,axiom_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy axcls)
8.308 - val helper_clauses = SHC.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
8.309 - val (supers',arity_clauses) = SFC.make_arity_clauses_dfg dfg thy tycons supers
8.310 - val classrel_clauses = SFC.make_classrel_clauses thy subs supers'
8.311 + val conjectures = make_conjecture_clauses dfg thy ccls
8.312 + val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls)
8.313 + val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls)
8.314 + val helper_clauses = get_helper_clauses dfg thy is_FO (conjectures, extra_cls, [])
8.315 + val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers
8.316 + val classrel_clauses = make_classrel_clauses thy subs supers'
8.317 in
8.318 (Vector.fromList clnames,
8.319 (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
8.320 end
8.321
8.322 end;
8.323 -
9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Mar 19 06:14:37 2010 +0100
9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Mar 19 13:02:18 2010 +0100
9.3 @@ -8,6 +8,7 @@
9.4 sig
9.5 val trace: bool Unsynchronized.ref
9.6 val trace_msg: (unit -> string) -> unit
9.7 + val skolem_prefix: string
9.8 val cnf_axiom: theory -> thm -> thm list
9.9 val pairname: thm -> string * thm
9.10 val multi_base_blacklist: string list
9.11 @@ -15,7 +16,6 @@
9.12 val type_has_topsort: typ -> bool
9.13 val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
9.14 val neg_clausify: thm list -> thm list
9.15 - val expand_defs_tac: thm -> tactic
9.16 val combinators: thm -> thm
9.17 val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
9.18 val suppress_endtheory: bool Unsynchronized.ref
9.19 @@ -26,8 +26,12 @@
9.20 structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR =
9.21 struct
9.22
9.23 +open Sledgehammer_FOL_Clause
9.24 +
9.25 val trace = Unsynchronized.ref false;
9.26 -fun trace_msg msg = if ! trace then tracing (msg ()) else ();
9.27 +fun trace_msg msg = if !trace then tracing (msg ()) else ();
9.28 +
9.29 +val skolem_prefix = "sko_"
9.30
9.31 fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
9.32
9.33 @@ -75,7 +79,7 @@
9.34 fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
9.35 (*Existential: declare a Skolem function, then insert into body and continue*)
9.36 let
9.37 - val cname = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
9.38 + val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
9.39 val args0 = OldTerm.term_frees xtp (*get the formal parameter list*)
9.40 val Ts = map type_of args0
9.41 val extraTs = rhs_extra_types (Ts ---> T) xtp
9.42 @@ -110,7 +114,7 @@
9.43 val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
9.44 val Ts = map type_of args
9.45 val cT = Ts ---> T
9.46 - val id = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
9.47 + val id = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
9.48 val c = Free (id, cT)
9.49 val rhs = list_abs_free (map dest_Free args,
9.50 HOLogic.choice_const T $ xtp)
9.51 @@ -386,15 +390,14 @@
9.52 | cnf_rules_pairs_aux thy pairs ((name,th)::ths) =
9.53 let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs
9.54 handle THM _ => pairs |
9.55 - Sledgehammer_FOL_Clause.CLAUSE _ => pairs
9.56 + CLAUSE _ => pairs
9.57 in cnf_rules_pairs_aux thy pairs' ths end;
9.58
9.59 (*The combination of rev and tail recursion preserves the original order*)
9.60 fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
9.61
9.62
9.63 -(**** Convert all facts of the theory into clauses
9.64 - (Sledgehammer_FOL_Clause.clause, or Sledgehammer_HOL_Clause.clause) ****)
9.65 +(**** Convert all facts of the theory into FOL or HOL clauses ****)
9.66
9.67 local
9.68
9.69 @@ -455,43 +458,6 @@
9.70 lambda_free, but then the individual theory caches become much bigger.*)
9.71
9.72
9.73 -(*** meson proof methods ***)
9.74 -
9.75 -(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
9.76 -fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a
9.77 - | is_absko _ = false;
9.78 -
9.79 -fun is_okdef xs (Const ("==", _) $ t $ u) = (*Definition of Free, not in certain terms*)
9.80 - is_Free t andalso not (member (op aconv) xs t)
9.81 - | is_okdef _ _ = false
9.82 -
9.83 -(*This function tries to cope with open locales, which introduce hypotheses of the form
9.84 - Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
9.85 - of sko_ functions. *)
9.86 -fun expand_defs_tac st0 st =
9.87 - let val hyps0 = #hyps (rep_thm st0)
9.88 - val hyps = #hyps (crep_thm st)
9.89 - val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
9.90 - val defs = filter (is_absko o Thm.term_of) newhyps
9.91 - val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
9.92 - (map Thm.term_of hyps)
9.93 - val fixed = OldTerm.term_frees (concl_of st) @
9.94 - fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
9.95 - in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
9.96 -
9.97 -
9.98 -fun meson_general_tac ctxt ths i st0 =
9.99 - let
9.100 - val thy = ProofContext.theory_of ctxt
9.101 - val ctxt0 = Classical.put_claset HOL_cs ctxt
9.102 - in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
9.103 -
9.104 -val meson_method_setup =
9.105 - Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
9.106 - SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
9.107 - "MESON resolution proof procedure";
9.108 -
9.109 -
9.110 (*** Converting a subgoal into negated conjecture clauses. ***)
9.111
9.112 fun neg_skolemize_tac ctxt =
9.113 @@ -534,11 +500,9 @@
9.114 "conversion of theorem to clauses";
9.115
9.116
9.117 -
9.118 (** setup **)
9.119
9.120 val setup =
9.121 - meson_method_setup #>
9.122 neg_clausify_setup #>
9.123 clausify_setup #>
9.124 perhaps saturate_skolem_cache #>
10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Mar 19 06:14:37 2010 +0100
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Mar 19 13:02:18 2010 +0100
10.3 @@ -44,19 +44,19 @@
10.4 datatype arLit =
10.5 TConsLit of class * string * string list
10.6 | TVarLit of class * string
10.7 - datatype arityClause = ArityClause of
10.8 + datatype arity_clause = ArityClause of
10.9 {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list}
10.10 - datatype classrelClause = ClassrelClause of
10.11 + datatype classrel_clause = ClassrelClause of
10.12 {axiom_name: axiom_name, subclass: class, superclass: class}
10.13 - val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
10.14 - val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arityClause list
10.15 - val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
10.16 + val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
10.17 + val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list
10.18 + val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
10.19 val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table
10.20 - val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table
10.21 + val add_classrel_clause_preds : classrel_clause * int Symtab.table -> int Symtab.table
10.22 val class_of_arityLit: arLit -> class
10.23 - val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table
10.24 + val add_arity_clause_preds: arity_clause * int Symtab.table -> int Symtab.table
10.25 val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
10.26 - val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table
10.27 + val add_arity_clause_funcs: arity_clause * int Symtab.table -> int Symtab.table
10.28 val init_functab: int Symtab.table
10.29 val dfg_sign: bool -> string -> string
10.30 val dfg_of_typeLit: bool -> type_literal -> string
10.31 @@ -67,14 +67,14 @@
10.32 val string_of_start: string -> string
10.33 val string_of_descrip : string -> string
10.34 val dfg_tfree_clause : string -> string
10.35 - val dfg_classrelClause: classrelClause -> string
10.36 - val dfg_arity_clause: arityClause -> string
10.37 + val dfg_classrel_clause: classrel_clause -> string
10.38 + val dfg_arity_clause: arity_clause -> string
10.39 val tptp_sign: bool -> string -> string
10.40 val tptp_of_typeLit : bool -> type_literal -> string
10.41 val gen_tptp_cls : int * string * kind * string list * string list -> string
10.42 val tptp_tfree_clause : string -> string
10.43 - val tptp_arity_clause : arityClause -> string
10.44 - val tptp_classrelClause : classrelClause -> string
10.45 + val tptp_arity_clause : arity_clause -> string
10.46 + val tptp_classrel_clause : classrel_clause -> string
10.47 end
10.48
10.49 structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
10.50 @@ -96,28 +96,23 @@
10.51
10.52 fun union_all xss = List.foldl (uncurry (union (op =))) [] xss;
10.53
10.54 -(*Provide readable names for the more common symbolic functions*)
10.55 +(* Provide readable names for the more common symbolic functions *)
10.56 val const_trans_table =
10.57 - Symtab.make [(@{const_name "op ="}, "equal"),
10.58 - (@{const_name Orderings.less_eq}, "lessequals"),
10.59 - (@{const_name "op &"}, "and"),
10.60 - (@{const_name "op |"}, "or"),
10.61 - (@{const_name "op -->"}, "implies"),
10.62 - (@{const_name "op :"}, "in"),
10.63 - ("Sledgehammer.fequal", "fequal"),
10.64 - ("Sledgehammer.COMBI", "COMBI"),
10.65 - ("Sledgehammer.COMBK", "COMBK"),
10.66 - ("Sledgehammer.COMBB", "COMBB"),
10.67 - ("Sledgehammer.COMBC", "COMBC"),
10.68 - ("Sledgehammer.COMBS", "COMBS"),
10.69 - ("Sledgehammer.COMBB'", "COMBB_e"),
10.70 - ("Sledgehammer.COMBC'", "COMBC_e"),
10.71 - ("Sledgehammer.COMBS'", "COMBS_e")];
10.72 + Symtab.make [(@{const_name "op ="}, "equal"),
10.73 + (@{const_name Orderings.less_eq}, "lessequals"),
10.74 + (@{const_name "op &"}, "and"),
10.75 + (@{const_name "op |"}, "or"),
10.76 + (@{const_name "op -->"}, "implies"),
10.77 + (@{const_name "op :"}, "in"),
10.78 + (@{const_name fequal}, "fequal"),
10.79 + (@{const_name COMBI}, "COMBI"),
10.80 + (@{const_name COMBK}, "COMBK"),
10.81 + (@{const_name COMBB}, "COMBB"),
10.82 + (@{const_name COMBC}, "COMBC"),
10.83 + (@{const_name COMBS}, "COMBS")];
10.84
10.85 val type_const_trans_table =
10.86 - Symtab.make [("*", "prod"),
10.87 - ("+", "sum"),
10.88 - ("~=>", "map")];
10.89 + Symtab.make [("*", "prod"), ("+", "sum"), ("~=>", "map")];
10.90
10.91 (*Escaping of special characters.
10.92 Alphanumeric characters are left unchanged.
10.93 @@ -290,7 +285,7 @@
10.94 datatype arLit = TConsLit of class * string * string list
10.95 | TVarLit of class * string;
10.96
10.97 -datatype arityClause =
10.98 +datatype arity_clause =
10.99 ArityClause of {axiom_name: axiom_name,
10.100 conclLit: arLit,
10.101 premLits: arLit list};
10.102 @@ -316,7 +311,7 @@
10.103
10.104 (**** Isabelle class relations ****)
10.105
10.106 -datatype classrelClause =
10.107 +datatype classrel_clause =
10.108 ClassrelClause of {axiom_name: axiom_name,
10.109 subclass: class,
10.110 superclass: class};
10.111 @@ -330,13 +325,13 @@
10.112 fun add_supers (sub,pairs) = List.foldl (add_super sub) pairs supers
10.113 in List.foldl add_supers [] subs end;
10.114
10.115 -fun make_classrelClause (sub,super) =
10.116 +fun make_classrel_clause (sub,super) =
10.117 ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
10.118 subclass = make_type_class sub,
10.119 superclass = make_type_class super};
10.120
10.121 fun make_classrel_clauses thy subs supers =
10.122 - map make_classrelClause (class_pairs thy subs supers);
10.123 + map make_classrel_clause (class_pairs thy subs supers);
10.124
10.125
10.126 (** Isabelle arities **)
10.127 @@ -391,13 +386,13 @@
10.128 fun add_type_sort_preds (T, preds) =
10.129 update_many (preds, map pred_of_sort (sorts_on_typs T));
10.130
10.131 -fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
10.132 +fun add_classrel_clause_preds (ClassrelClause {subclass,superclass,...}, preds) =
10.133 Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
10.134
10.135 fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass
10.136 | class_of_arityLit (TVarLit (tclass, _)) = tclass;
10.137
10.138 -fun add_arityClause_preds (ArityClause {conclLit,premLits,...}, preds) =
10.139 +fun add_arity_clause_preds (ArityClause {conclLit,premLits,...}, preds) =
10.140 let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits)
10.141 fun upd (class,preds) = Symtab.update (class,1) preds
10.142 in List.foldl upd preds classes end;
10.143 @@ -414,7 +409,7 @@
10.144 | add_type_sort_funcs (TFree (a, _), funcs) =
10.145 Symtab.update (make_fixed_type_var a, 0) funcs
10.146
10.147 -fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) =
10.148 +fun add_arity_clause_funcs (ArityClause {conclLit,...}, funcs) =
10.149 let val TConsLit (_, tcons, tvars) = conclLit
10.150 in Symtab.update (tcons, length tvars) funcs end;
10.151
10.152 @@ -480,7 +475,7 @@
10.153
10.154 fun dfg_classrelLits sub sup = "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)";
10.155
10.156 -fun dfg_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
10.157 +fun dfg_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
10.158 "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^
10.159 axiom_name ^ ").\n\n";
10.160
10.161 @@ -528,7 +523,7 @@
10.162 let val tvar = "(T)"
10.163 in tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end;
10.164
10.165 -fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
10.166 +fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
10.167 "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n"
10.168
10.169 end;
11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Mar 19 06:14:37 2010 +0100
11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Mar 19 13:02:18 2010 +0100
11.3 @@ -6,67 +6,54 @@
11.4
11.5 signature SLEDGEHAMMER_HOL_CLAUSE =
11.6 sig
11.7 - val ext: thm
11.8 - val comb_I: thm
11.9 - val comb_K: thm
11.10 - val comb_B: thm
11.11 - val comb_C: thm
11.12 - val comb_S: thm
11.13 - val minimize_applies: bool
11.14 + type kind = Sledgehammer_FOL_Clause.kind
11.15 + type fol_type = Sledgehammer_FOL_Clause.fol_type
11.16 + type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
11.17 + type arity_clause = Sledgehammer_FOL_Clause.arity_clause
11.18 type axiom_name = string
11.19 type polarity = bool
11.20 - type clause_id = int
11.21 + type hol_clause_id = int
11.22 +
11.23 datatype combterm =
11.24 - CombConst of string * Sledgehammer_FOL_Clause.fol_type * Sledgehammer_FOL_Clause.fol_type list (*Const and Free*)
11.25 - | CombVar of string * Sledgehammer_FOL_Clause.fol_type
11.26 - | CombApp of combterm * combterm
11.27 + CombConst of string * fol_type * fol_type list (* Const and Free *) |
11.28 + CombVar of string * fol_type |
11.29 + CombApp of combterm * combterm
11.30 datatype literal = Literal of polarity * combterm
11.31 - datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
11.32 - kind: Sledgehammer_FOL_Clause.kind,literals: literal list, ctypes_sorts: typ list}
11.33 - val type_of_combterm: combterm -> Sledgehammer_FOL_Clause.fol_type
11.34 - val strip_comb: combterm -> combterm * combterm list
11.35 - val literals_of_term: theory -> term -> literal list * typ list
11.36 - exception TOO_TRIVIAL
11.37 - val make_conjecture_clauses: bool -> theory -> thm list -> clause list
11.38 - val make_axiom_clauses: bool ->
11.39 - theory ->
11.40 - (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list
11.41 - val get_helper_clauses: bool ->
11.42 - theory ->
11.43 - bool ->
11.44 - clause list * (thm * (axiom_name * clause_id)) list * string list ->
11.45 - clause list
11.46 - val tptp_write_file: bool -> Path.T ->
11.47 - clause list * clause list * clause list * clause list *
11.48 - Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
11.49 + datatype hol_clause =
11.50 + HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
11.51 + kind: kind, literals: literal list, ctypes_sorts: typ list}
11.52 +
11.53 + val type_of_combterm : combterm -> fol_type
11.54 + val strip_combterm_comb : combterm -> combterm * combterm list
11.55 + val literals_of_term : theory -> term -> literal list * typ list
11.56 + exception TRIVIAL
11.57 + val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
11.58 + val make_axiom_clauses : bool -> theory ->
11.59 + (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
11.60 + val get_helper_clauses : bool -> theory -> bool ->
11.61 + hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
11.62 + hol_clause list
11.63 + val write_tptp_file : bool -> Path.T ->
11.64 + hol_clause list * hol_clause list * hol_clause list * hol_clause list *
11.65 + classrel_clause list * arity_clause list ->
11.66 int * int
11.67 - val dfg_write_file: bool -> Path.T ->
11.68 - clause list * clause list * clause list * clause list *
11.69 - Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
11.70 - int * int
11.71 + val write_dfg_file : bool -> Path.T ->
11.72 + hol_clause list * hol_clause list * hol_clause list * hol_clause list *
11.73 + classrel_clause list * arity_clause list -> int * int
11.74 end
11.75
11.76 structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
11.77 struct
11.78
11.79 -structure SFC = Sledgehammer_FOL_Clause;
11.80 -
11.81 -(* theorems for combinators and function extensionality *)
11.82 -val ext = thm "HOL.ext";
11.83 -val comb_I = thm "Sledgehammer.COMBI_def";
11.84 -val comb_K = thm "Sledgehammer.COMBK_def";
11.85 -val comb_B = thm "Sledgehammer.COMBB_def";
11.86 -val comb_C = thm "Sledgehammer.COMBC_def";
11.87 -val comb_S = thm "Sledgehammer.COMBS_def";
11.88 -val fequal_imp_equal = thm "Sledgehammer.fequal_imp_equal";
11.89 -val equal_imp_fequal = thm "Sledgehammer.equal_imp_fequal";
11.90 -
11.91 +open Sledgehammer_FOL_Clause
11.92 +open Sledgehammer_Fact_Preprocessor
11.93
11.94 (* Parameter t_full below indicates that full type information is to be
11.95 exported *)
11.96
11.97 -(*If true, each function will be directly applied to as many arguments as possible, avoiding
11.98 - use of the "apply" operator. Use of hBOOL is also minimized.*)
11.99 +(* If true, each function will be directly applied to as many arguments as
11.100 + possible, avoiding use of the "apply" operator. Use of hBOOL is also
11.101 + minimized. *)
11.102 val minimize_applies = true;
11.103
11.104 fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
11.105 @@ -84,21 +71,18 @@
11.106
11.107 type axiom_name = string;
11.108 type polarity = bool;
11.109 -type clause_id = int;
11.110 +type hol_clause_id = int;
11.111
11.112 -datatype combterm = CombConst of string * SFC.fol_type * SFC.fol_type list (*Const and Free*)
11.113 - | CombVar of string * SFC.fol_type
11.114 - | CombApp of combterm * combterm
11.115 +datatype combterm =
11.116 + CombConst of string * fol_type * fol_type list (* Const and Free *) |
11.117 + CombVar of string * fol_type |
11.118 + CombApp of combterm * combterm
11.119
11.120 datatype literal = Literal of polarity * combterm;
11.121
11.122 -datatype clause =
11.123 - Clause of {clause_id: clause_id,
11.124 - axiom_name: axiom_name,
11.125 - th: thm,
11.126 - kind: SFC.kind,
11.127 - literals: literal list,
11.128 - ctypes_sorts: typ list};
11.129 +datatype hol_clause =
11.130 + HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
11.131 + kind: kind, literals: literal list, ctypes_sorts: typ list};
11.132
11.133
11.134 (*********************************************************************)
11.135 @@ -106,8 +90,7 @@
11.136 (*********************************************************************)
11.137
11.138 fun isFalse (Literal(pol, CombConst(c,_,_))) =
11.139 - (pol andalso c = "c_False") orelse
11.140 - (not pol andalso c = "c_True")
11.141 + (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
11.142 | isFalse _ = false;
11.143
11.144 fun isTrue (Literal (pol, CombConst(c,_,_))) =
11.145 @@ -115,24 +98,22 @@
11.146 (not pol andalso c = "c_False")
11.147 | isTrue _ = false;
11.148
11.149 -fun isTaut (Clause {literals,...}) = exists isTrue literals;
11.150 +fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
11.151
11.152 fun type_of dfg (Type (a, Ts)) =
11.153 let val (folTypes,ts) = types_of dfg Ts
11.154 - in (SFC.Comp(SFC.make_fixed_type_const dfg a, folTypes), ts) end
11.155 - | type_of _ (tp as TFree (a, _)) =
11.156 - (SFC.AtomF (SFC.make_fixed_type_var a), [tp])
11.157 - | type_of _ (tp as TVar (v, _)) =
11.158 - (SFC.AtomV (SFC.make_schematic_type_var v), [tp])
11.159 + in (Comp(make_fixed_type_const dfg a, folTypes), ts) end
11.160 + | type_of _ (tp as TFree (a, _)) = (AtomF (make_fixed_type_var a), [tp])
11.161 + | type_of _ (tp as TVar (v, _)) = (AtomV (make_schematic_type_var v), [tp])
11.162 and types_of dfg Ts =
11.163 let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
11.164 - in (folTyps, SFC.union_all ts) end;
11.165 + in (folTyps, union_all ts) end;
11.166
11.167 (* same as above, but no gathering of sort information *)
11.168 fun simp_type_of dfg (Type (a, Ts)) =
11.169 - SFC.Comp(SFC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
11.170 - | simp_type_of _ (TFree (a, _)) = SFC.AtomF(SFC.make_fixed_type_var a)
11.171 - | simp_type_of _ (TVar (v, _)) = SFC.AtomV(SFC.make_schematic_type_var v);
11.172 + Comp(make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
11.173 + | simp_type_of _ (TFree (a, _)) = AtomF (make_fixed_type_var a)
11.174 + | simp_type_of _ (TVar (v, _)) = AtomV (make_schematic_type_var v);
11.175
11.176
11.177 fun const_type_of dfg thy (c,t) =
11.178 @@ -142,27 +123,27 @@
11.179 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
11.180 fun combterm_of dfg thy (Const(c,t)) =
11.181 let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
11.182 - val c' = CombConst(SFC.make_fixed_const dfg c, tp, tvar_list)
11.183 + val c' = CombConst(make_fixed_const dfg c, tp, tvar_list)
11.184 in (c',ts) end
11.185 | combterm_of dfg _ (Free(v,t)) =
11.186 let val (tp,ts) = type_of dfg t
11.187 - val v' = CombConst(SFC.make_fixed_var v, tp, [])
11.188 + val v' = CombConst(make_fixed_var v, tp, [])
11.189 in (v',ts) end
11.190 | combterm_of dfg _ (Var(v,t)) =
11.191 let val (tp,ts) = type_of dfg t
11.192 - val v' = CombVar(SFC.make_schematic_var v,tp)
11.193 + val v' = CombVar(make_schematic_var v,tp)
11.194 in (v',ts) end
11.195 | combterm_of dfg thy (P $ Q) =
11.196 let val (P',tsP) = combterm_of dfg thy P
11.197 val (Q',tsQ) = combterm_of dfg thy Q
11.198 in (CombApp(P',Q'), union (op =) tsP tsQ) end
11.199 - | combterm_of _ _ (t as Abs _) = raise SFC.CLAUSE ("HOL CLAUSE", t);
11.200 + | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t);
11.201
11.202 -fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
11.203 +fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
11.204 | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
11.205
11.206 -fun literals_of_term1 dfg thy args (Const("Trueprop",_) $ P) = literals_of_term1 dfg thy args P
11.207 - | literals_of_term1 dfg thy args (Const("op |",_) $ P $ Q) =
11.208 +fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P
11.209 + | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) =
11.210 literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
11.211 | literals_of_term1 dfg thy (lits,ts) P =
11.212 let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
11.213 @@ -173,23 +154,23 @@
11.214 fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
11.215 val literals_of_term = literals_of_term_dfg false;
11.216
11.217 -(* Problem too trivial for resolution (empty clause) *)
11.218 -exception TOO_TRIVIAL;
11.219 +(* Trivial problem, which resolution cannot handle (empty clause) *)
11.220 +exception TRIVIAL;
11.221
11.222 (* making axiom and conjecture clauses *)
11.223 -fun make_clause dfg thy (clause_id,axiom_name,kind,th) =
11.224 +fun make_clause dfg thy (clause_id, axiom_name, kind, th) =
11.225 let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
11.226 in
11.227 - if forall isFalse lits
11.228 - then raise TOO_TRIVIAL
11.229 + if forall isFalse lits then
11.230 + raise TRIVIAL
11.231 else
11.232 - Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
11.233 - literals = lits, ctypes_sorts = ctypes_sorts}
11.234 + HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
11.235 + kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}
11.236 end;
11.237
11.238
11.239 fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
11.240 - let val cls = make_clause dfg thy (id, name, SFC.Axiom, th)
11.241 + let val cls = make_clause dfg thy (id, name, Axiom, th)
11.242 in
11.243 if isTaut cls then pairs else (name,cls)::pairs
11.244 end;
11.245 @@ -198,7 +179,7 @@
11.246
11.247 fun make_conjecture_clauses_aux _ _ _ [] = []
11.248 | make_conjecture_clauses_aux dfg thy n (th::ths) =
11.249 - make_clause dfg thy (n,"conjecture", SFC.Conjecture, th) ::
11.250 + make_clause dfg thy (n,"conjecture", Conjecture, th) ::
11.251 make_conjecture_clauses_aux dfg thy (n+1) ths;
11.252
11.253 fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
11.254 @@ -211,7 +192,7 @@
11.255 (**********************************************************************)
11.256
11.257 (*Result of a function type; no need to check that the argument type matches.*)
11.258 -fun result_type (SFC.Comp ("tc_fun", [_, tp2])) = tp2
11.259 +fun result_type (Comp ("tc_fun", [_, tp2])) = tp2
11.260 | result_type _ = error "result_type"
11.261
11.262 fun type_of_combterm (CombConst (_, tp, _)) = tp
11.263 @@ -219,7 +200,7 @@
11.264 | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
11.265
11.266 (*gets the head of a combinator application, along with the list of arguments*)
11.267 -fun strip_comb u =
11.268 +fun strip_combterm_comb u =
11.269 let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
11.270 | stripc x = x
11.271 in stripc(u,[]) end;
11.272 @@ -231,10 +212,10 @@
11.273
11.274 fun wrap_type t_full (s, tp) =
11.275 if t_full then
11.276 - type_wrapper ^ SFC.paren_pack [s, SFC.string_of_fol_type tp]
11.277 + type_wrapper ^ paren_pack [s, string_of_fol_type tp]
11.278 else s;
11.279
11.280 -fun apply ss = "hAPP" ^ SFC.paren_pack ss;
11.281 +fun apply ss = "hAPP" ^ paren_pack ss;
11.282
11.283 fun rev_apply (v, []) = v
11.284 | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
11.285 @@ -251,10 +232,9 @@
11.286 Int.toString nargs ^ " but is applied to " ^
11.287 space_implode ", " args)
11.288 val args2 = List.drop(args, nargs)
11.289 - val targs = if not t_full then map SFC.string_of_fol_type tvars
11.290 - else []
11.291 + val targs = if not t_full then map string_of_fol_type tvars else []
11.292 in
11.293 - string_apply (c ^ SFC.paren_pack (args1@targs), args2)
11.294 + string_apply (c ^ paren_pack (args1@targs), args2)
11.295 end
11.296 | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
11.297 | string_of_applic _ _ _ = error "string_of_applic";
11.298 @@ -263,7 +243,7 @@
11.299 if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
11.300
11.301 fun string_of_combterm (params as (t_full, cma, cnh)) t =
11.302 - let val (head, args) = strip_comb t
11.303 + let val (head, args) = strip_combterm_comb t
11.304 in wrap_type_if t_full cnh (head,
11.305 string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
11.306 type_of_combterm t)
11.307 @@ -271,15 +251,15 @@
11.308
11.309 (*Boolean-valued terms are here converted to literals.*)
11.310 fun boolify params t =
11.311 - "hBOOL" ^ SFC.paren_pack [string_of_combterm params t];
11.312 + "hBOOL" ^ paren_pack [string_of_combterm params t];
11.313
11.314 fun string_of_predicate (params as (_,_,cnh)) t =
11.315 case t of
11.316 (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
11.317 (*DFG only: new TPTP prefers infix equality*)
11.318 - ("equal" ^ SFC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
11.319 + ("equal" ^ paren_pack [string_of_combterm params t1, string_of_combterm params t2])
11.320 | _ =>
11.321 - case #1 (strip_comb t) of
11.322 + case #1 (strip_combterm_comb t) of
11.323 CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
11.324 | _ => boolify params t;
11.325
11.326 @@ -290,31 +270,31 @@
11.327 let val eqop = if pol then " = " else " != "
11.328 in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end;
11.329
11.330 -fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
11.331 +fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal", _, _), t1), t2))) =
11.332 tptp_of_equality params pol (t1,t2)
11.333 | tptp_literal params (Literal(pol,pred)) =
11.334 - SFC.tptp_sign pol (string_of_predicate params pred);
11.335 + tptp_sign pol (string_of_predicate params pred);
11.336
11.337 (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
11.338 the latter should only occur in conjecture clauses.*)
11.339 -fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
11.340 +fun tptp_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
11.341 (map (tptp_literal params) literals,
11.342 - map (SFC.tptp_of_typeLit pos) (SFC.add_typs ctypes_sorts));
11.343 + map (tptp_of_typeLit pos) (add_typs ctypes_sorts));
11.344
11.345 -fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) =
11.346 - let val (lits,tylits) = tptp_type_lits params (kind = SFC.Conjecture) cls
11.347 +fun clause2tptp params (cls as HOLClause {axiom_name, clause_id, kind, ...}) =
11.348 + let val (lits,tylits) = tptp_type_lits params (kind = Conjecture) cls
11.349 in
11.350 - (SFC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
11.351 + (gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits)
11.352 end;
11.353
11.354
11.355 (*** dfg format ***)
11.356
11.357 -fun dfg_literal params (Literal(pol,pred)) = SFC.dfg_sign pol (string_of_predicate params pred);
11.358 +fun dfg_literal params (Literal(pol,pred)) = dfg_sign pol (string_of_predicate params pred);
11.359
11.360 -fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
11.361 +fun dfg_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
11.362 (map (dfg_literal params) literals,
11.363 - map (SFC.dfg_of_typeLit pos) (SFC.add_typs ctypes_sorts));
11.364 + map (dfg_of_typeLit pos) (add_typs ctypes_sorts));
11.365
11.366 fun get_uvars (CombConst _) vars = vars
11.367 | get_uvars (CombVar(v,_)) vars = (v::vars)
11.368 @@ -322,20 +302,21 @@
11.369
11.370 fun get_uvars_l (Literal(_,c)) = get_uvars c [];
11.371
11.372 -fun dfg_vars (Clause {literals,...}) = SFC.union_all (map get_uvars_l literals);
11.373 +fun dfg_vars (HOLClause {literals,...}) = union_all (map get_uvars_l literals);
11.374
11.375 -fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
11.376 - let val (lits,tylits) = dfg_type_lits params (kind = SFC.Conjecture) cls
11.377 +fun clause2dfg params (cls as HOLClause {axiom_name, clause_id, kind,
11.378 + ctypes_sorts, ...}) =
11.379 + let val (lits,tylits) = dfg_type_lits params (kind = Conjecture) cls
11.380 val vars = dfg_vars cls
11.381 - val tvars = SFC.get_tvar_strs ctypes_sorts
11.382 + val tvars = get_tvar_strs ctypes_sorts
11.383 in
11.384 - (SFC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
11.385 + (gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
11.386 end;
11.387
11.388
11.389 (** For DFG format: accumulate function and predicate declarations **)
11.390
11.391 -fun addtypes tvars tab = List.foldl SFC.add_foltype_funcs tab tvars;
11.392 +fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
11.393
11.394 fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
11.395 if c = "equal" then (addtypes tvars funcs, preds)
11.396 @@ -348,33 +329,33 @@
11.397 else (addtypes tvars funcs, addit preds)
11.398 end
11.399 | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
11.400 - (SFC.add_foltype_funcs (ctp,funcs), preds)
11.401 + (add_foltype_funcs (ctp,funcs), preds)
11.402 | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
11.403
11.404 -fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls);
11.405 +fun add_literal_decls params (Literal (_,c), decls) = add_decls params (c,decls);
11.406
11.407 -fun add_clause_decls params (Clause {literals, ...}, decls) =
11.408 +fun add_clause_decls params (HOLClause {literals, ...}, decls) =
11.409 List.foldl (add_literal_decls params) decls literals
11.410 handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
11.411
11.412 fun decls_of_clauses params clauses arity_clauses =
11.413 - let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) SFC.init_functab)
11.414 + let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) init_functab)
11.415 val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
11.416 val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
11.417 in
11.418 - (Symtab.dest (List.foldl SFC.add_arityClause_funcs functab arity_clauses),
11.419 + (Symtab.dest (List.foldl add_arity_clause_funcs functab arity_clauses),
11.420 Symtab.dest predtab)
11.421 end;
11.422
11.423 -fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
11.424 - List.foldl SFC.add_type_sort_preds preds ctypes_sorts
11.425 +fun add_clause_preds (HOLClause {ctypes_sorts, ...}, preds) =
11.426 + List.foldl add_type_sort_preds preds ctypes_sorts
11.427 handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
11.428
11.429 (*Higher-order clauses have only the predicates hBOOL and type classes.*)
11.430 fun preds_of_clauses clauses clsrel_clauses arity_clauses =
11.431 Symtab.dest
11.432 - (List.foldl SFC.add_classrelClause_preds
11.433 - (List.foldl SFC.add_arityClause_preds
11.434 + (List.foldl add_classrel_clause_preds
11.435 + (List.foldl add_arity_clause_preds
11.436 (List.foldl add_clause_preds Symtab.empty clauses)
11.437 arity_clauses)
11.438 clsrel_clauses)
11.439 @@ -385,9 +366,8 @@
11.440 (**********************************************************************)
11.441
11.442 val init_counters =
11.443 - Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
11.444 - ("c_COMBB", 0), ("c_COMBC", 0),
11.445 - ("c_COMBS", 0)];
11.446 + Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
11.447 + ("c_COMBS", 0)];
11.448
11.449 fun count_combterm (CombConst (c, _, _), ct) =
11.450 (case Symtab.lookup ct c of NONE => ct (*no counter*)
11.451 @@ -397,18 +377,18 @@
11.452
11.453 fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
11.454
11.455 -fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals;
11.456 +fun count_clause (HOLClause {literals, ...}, ct) =
11.457 + List.foldl count_literal ct literals;
11.458
11.459 -fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
11.460 +fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}, ct) =
11.461 if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
11.462 else ct;
11.463
11.464 -fun cnf_helper_thms thy =
11.465 - Sledgehammer_Fact_Preprocessor.cnf_rules_pairs thy
11.466 - o map Sledgehammer_Fact_Preprocessor.pairname
11.467 +fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname
11.468
11.469 fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
11.470 - if isFO then [] (*first-order*)
11.471 + if isFO then
11.472 + []
11.473 else
11.474 let
11.475 val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
11.476 @@ -416,15 +396,15 @@
11.477 val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
11.478 fun needed c = the (Symtab.lookup ct c) > 0
11.479 val IK = if needed "c_COMBI" orelse needed "c_COMBK"
11.480 - then cnf_helper_thms thy [comb_I,comb_K]
11.481 + then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
11.482 else []
11.483 val BC = if needed "c_COMBB" orelse needed "c_COMBC"
11.484 - then cnf_helper_thms thy [comb_B,comb_C]
11.485 + then cnf_helper_thms thy [@{thm COMBB_def}, @{thm COMBC_def}]
11.486 else []
11.487 - val S = if needed "c_COMBS"
11.488 - then cnf_helper_thms thy [comb_S]
11.489 + val S = if needed "c_COMBS" then cnf_helper_thms thy [@{thm COMBS_def}]
11.490 else []
11.491 - val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
11.492 + val other = cnf_helper_thms thy [@{thm fequal_imp_equal},
11.493 + @{thm equal_imp_fequal}]
11.494 in
11.495 map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
11.496 end;
11.497 @@ -432,7 +412,7 @@
11.498 (*Find the minimal arity of each function mentioned in the term. Also, note which uses
11.499 are not at top level, to see if hBOOL is needed.*)
11.500 fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
11.501 - let val (head, args) = strip_comb t
11.502 + let val (head, args) = strip_combterm_comb t
11.503 val n = length args
11.504 val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
11.505 in
11.506 @@ -451,11 +431,12 @@
11.507 fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
11.508 count_constants_term true t (const_min_arity, const_needs_hBOOL);
11.509
11.510 -fun count_constants_clause (Clause{literals,...}) (const_min_arity, const_needs_hBOOL) =
11.511 +fun count_constants_clause (HOLClause {literals, ...})
11.512 + (const_min_arity, const_needs_hBOOL) =
11.513 fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
11.514
11.515 fun display_arity const_needs_hBOOL (c,n) =
11.516 - Sledgehammer_Fact_Preprocessor.trace_msg (fn () => "Constant: " ^ c ^
11.517 + trace_msg (fn () => "Constant: " ^ c ^
11.518 " arity:\t" ^ Int.toString n ^
11.519 (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
11.520
11.521 @@ -469,31 +450,31 @@
11.522 in (const_min_arity, const_needs_hBOOL) end
11.523 else (Symtab.empty, Symtab.empty);
11.524
11.525 -(* tptp format *)
11.526 +(* TPTP format *)
11.527
11.528 -fun tptp_write_file t_full file clauses =
11.529 +fun write_tptp_file t_full file clauses =
11.530 let
11.531 val (conjectures, axclauses, _, helper_clauses,
11.532 classrel_clauses, arity_clauses) = clauses
11.533 val (cma, cnh) = count_constants clauses
11.534 val params = (t_full, cma, cnh)
11.535 val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
11.536 - val tfree_clss = map SFC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
11.537 + val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
11.538 val _ =
11.539 File.write_list file (
11.540 map (#1 o (clause2tptp params)) axclauses @
11.541 tfree_clss @
11.542 tptp_clss @
11.543 - map SFC.tptp_classrelClause classrel_clauses @
11.544 - map SFC.tptp_arity_clause arity_clauses @
11.545 + map tptp_classrel_clause classrel_clauses @
11.546 + map tptp_arity_clause arity_clauses @
11.547 map (#1 o (clause2tptp params)) helper_clauses)
11.548 in (length axclauses + 1, length tfree_clss + length tptp_clss)
11.549 end;
11.550
11.551
11.552 -(* dfg format *)
11.553 +(* DFG format *)
11.554
11.555 -fun dfg_write_file t_full file clauses =
11.556 +fun write_dfg_file t_full file clauses =
11.557 let
11.558 val (conjectures, axclauses, _, helper_clauses,
11.559 classrel_clauses, arity_clauses) = clauses
11.560 @@ -502,20 +483,20 @@
11.561 val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
11.562 and probname = Path.implode (Path.base file)
11.563 val axstrs = map (#1 o (clause2dfg params)) axclauses
11.564 - val tfree_clss = map SFC.dfg_tfree_clause (SFC.union_all tfree_litss)
11.565 + val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
11.566 val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
11.567 val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
11.568 and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
11.569 val _ =
11.570 File.write_list file (
11.571 - SFC.string_of_start probname ::
11.572 - SFC.string_of_descrip probname ::
11.573 - SFC.string_of_symbols (SFC.string_of_funcs funcs)
11.574 - (SFC.string_of_preds (cl_preds @ ty_preds)) ::
11.575 + string_of_start probname ::
11.576 + string_of_descrip probname ::
11.577 + string_of_symbols (string_of_funcs funcs)
11.578 + (string_of_preds (cl_preds @ ty_preds)) ::
11.579 "list_of_clauses(axioms,cnf).\n" ::
11.580 axstrs @
11.581 - map SFC.dfg_classrelClause classrel_clauses @
11.582 - map SFC.dfg_arity_clause arity_clauses @
11.583 + map dfg_classrel_clause classrel_clauses @
11.584 + map dfg_arity_clause arity_clauses @
11.585 helper_clauses_strs @
11.586 ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
11.587 tfree_clss @
11.588 @@ -530,4 +511,3 @@
11.589 end;
11.590
11.591 end;
11.592 -
12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Mar 19 06:14:37 2010 +0100
12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Mar 19 13:02:18 2010 +0100
12.3 @@ -7,33 +7,29 @@
12.4 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
12.5 sig
12.6 val chained_hint: string
12.7 -
12.8 - val fix_sorts: sort Vartab.table -> term -> term
12.9 val invert_const: string -> string
12.10 val invert_type_const: string -> string
12.11 val num_typargs: theory -> string -> int
12.12 val make_tvar: string -> typ
12.13 val strip_prefix: string -> string -> string option
12.14 val setup: theory -> theory
12.15 - (* extracting lemma list*)
12.16 - val find_failure: string -> string option
12.17 - val lemma_list: bool -> string ->
12.18 + val is_proof_well_formed: string -> bool
12.19 + val metis_lemma_list: bool -> string ->
12.20 string * string vector * (int * int) * Proof.context * thm * int -> string * string list
12.21 - (* structured proofs *)
12.22 - val structured_proof: string ->
12.23 + val structured_isar_proof: string ->
12.24 string * string vector * (int * int) * Proof.context * thm * int -> string * string list
12.25 end;
12.26
12.27 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
12.28 struct
12.29
12.30 -structure SFC = Sledgehammer_FOL_Clause
12.31 +open Sledgehammer_FOL_Clause
12.32 +open Sledgehammer_Fact_Preprocessor
12.33
12.34 -val trace_path = Path.basic "atp_trace";
12.35 +val trace_proof_path = Path.basic "atp_trace";
12.36
12.37 -fun trace s =
12.38 - if ! Sledgehammer_Fact_Preprocessor.trace then File.append (File.tmp_path trace_path) s
12.39 - else ();
12.40 +fun trace_proof_msg f =
12.41 + if !trace then File.append (File.tmp_path trace_proof_path) (f ()) else ();
12.42
12.43 fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
12.44
12.45 @@ -43,9 +39,6 @@
12.46 (*Indicates whether to include sort information in generated proofs*)
12.47 val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true;
12.48
12.49 -(*Indicated whether to generate full proofs or just lemma lists - now via setup of atps*)
12.50 -(* val (full_proofs, full_proofs_setup) = Attrib.config_bool "sledgehammer_full" false; *)
12.51 -
12.52 val setup = modulus_setup #> recon_sorts_setup;
12.53
12.54 (**** PARSING OF TSTP FORMAT ****)
12.55 @@ -109,12 +102,12 @@
12.56 (*If string s has the prefix s1, return the result of deleting it.*)
12.57 fun strip_prefix s1 s =
12.58 if String.isPrefix s1 s
12.59 - then SOME (SFC.undo_ascii_of (String.extract (s, size s1, NONE)))
12.60 + then SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
12.61 else NONE;
12.62
12.63 (*Invert the table of translations between Isabelle and ATPs*)
12.64 val type_const_trans_table_inv =
12.65 - Symtab.make (map swap (Symtab.dest SFC.type_const_trans_table));
12.66 + Symtab.make (map swap (Symtab.dest type_const_trans_table));
12.67
12.68 fun invert_type_const c =
12.69 case Symtab.lookup type_const_trans_table_inv c of
12.70 @@ -132,15 +125,15 @@
12.71 | Br (a,ts) =>
12.72 let val Ts = map type_of_stree ts
12.73 in
12.74 - case strip_prefix SFC.tconst_prefix a of
12.75 + case strip_prefix tconst_prefix a of
12.76 SOME b => Type(invert_type_const b, Ts)
12.77 | NONE =>
12.78 if not (null ts) then raise STREE t (*only tconsts have type arguments*)
12.79 else
12.80 - case strip_prefix SFC.tfree_prefix a of
12.81 + case strip_prefix tfree_prefix a of
12.82 SOME b => TFree("'" ^ b, HOLogic.typeS)
12.83 | NONE =>
12.84 - case strip_prefix SFC.tvar_prefix a of
12.85 + case strip_prefix tvar_prefix a of
12.86 SOME b => make_tvar b
12.87 | NONE => make_tvar a (*Variable from the ATP, say X1*)
12.88 end;
12.89 @@ -148,7 +141,7 @@
12.90 (*Invert the table of translations between Isabelle and ATPs*)
12.91 val const_trans_table_inv =
12.92 Symtab.update ("fequal", "op =")
12.93 - (Symtab.make (map swap (Symtab.dest SFC.const_trans_table)));
12.94 + (Symtab.make (map swap (Symtab.dest const_trans_table)));
12.95
12.96 fun invert_const c =
12.97 case Symtab.lookup const_trans_table_inv c of
12.98 @@ -169,9 +162,9 @@
12.99 | Br ("hBOOL",[t]) => term_of_stree [] thy t (*ignore hBOOL*)
12.100 | Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t
12.101 | Br (a,ts) =>
12.102 - case strip_prefix SFC.const_prefix a of
12.103 + case strip_prefix const_prefix a of
12.104 SOME "equal" =>
12.105 - list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
12.106 + list_comb(Const (@{const_name "op ="}, HOLogic.typeT), List.map (term_of_stree [] thy) ts)
12.107 | SOME b =>
12.108 let val c = invert_const b
12.109 val nterms = length ts - num_typargs thy c
12.110 @@ -183,10 +176,10 @@
12.111 | NONE => (*a variable, not a constant*)
12.112 let val T = HOLogic.typeT
12.113 val opr = (*a Free variable is typically a Skolem function*)
12.114 - case strip_prefix SFC.fixed_var_prefix a of
12.115 + case strip_prefix fixed_var_prefix a of
12.116 SOME b => Free(b,T)
12.117 | NONE =>
12.118 - case strip_prefix SFC.schematic_var_prefix a of
12.119 + case strip_prefix schematic_var_prefix a of
12.120 SOME b => make_var (b,T)
12.121 | NONE => make_var (a,T) (*Variable from the ATP, say X1*)
12.122 in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end;
12.123 @@ -196,7 +189,7 @@
12.124 | constraint_of_stree pol t = case t of
12.125 Int _ => raise STREE t
12.126 | Br (a,ts) =>
12.127 - (case (strip_prefix SFC.class_prefix a, map type_of_stree ts) of
12.128 + (case (strip_prefix class_prefix a, map type_of_stree ts) of
12.129 (SOME b, [T]) => (pol, b, T)
12.130 | _ => raise STREE t);
12.131
12.132 @@ -286,7 +279,7 @@
12.133 may disagree. We have to try all combinations of literals (quadratic!) and
12.134 match up the variable names consistently. **)
12.135
12.136 -fun strip_alls_aux n (Const("all",_)$Abs(a,T,t)) =
12.137 +fun strip_alls_aux n (Const(@{const_name all}, _)$Abs(a,T,t)) =
12.138 strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t))
12.139 | strip_alls_aux _ t = t;
12.140
12.141 @@ -347,7 +340,7 @@
12.142 ATP may have their literals reordered.*)
12.143 fun isar_lines ctxt ctms =
12.144 let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term)
12.145 - val _ = trace ("\n\nisar_lines: start\n")
12.146 + val _ = trace_proof_msg (K "\n\nisar_lines: start\n")
12.147 fun doline _ (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*)
12.148 (case permuted_clause t ctms of
12.149 SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
12.150 @@ -399,7 +392,7 @@
12.151 | add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines
12.152 and delete_dep lno lines = List.foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines);
12.153
12.154 -fun bad_free (Free (a,_)) = String.isPrefix "sko_" a
12.155 +fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a
12.156 | bad_free _ = false;
12.157
12.158 (*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies.
12.159 @@ -436,26 +429,22 @@
12.160 | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
12.161
12.162 fun decode_tstp_file cnfs ctxt th sgno thm_names =
12.163 - let val _ = trace "\ndecode_tstp_file: start\n"
12.164 + let val _ = trace_proof_msg (K "\ndecode_tstp_file: start\n")
12.165 val tuples = map (dest_tstp o tstp_line o explode) cnfs
12.166 - val _ = trace (Int.toString (length tuples) ^ " tuples extracted\n")
12.167 + val _ = trace_proof_msg (fn () => Int.toString (length tuples) ^ " tuples extracted\n")
12.168 val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
12.169 val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
12.170 - val _ = trace (Int.toString (length raw_lines) ^ " raw_lines extracted\n")
12.171 + val _ = trace_proof_msg (fn () => Int.toString (length raw_lines) ^ " raw_lines extracted\n")
12.172 val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
12.173 - val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
12.174 - val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
12.175 - val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
12.176 - val (ccls,fixes) = Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th sgno
12.177 - val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
12.178 + val _ = trace_proof_msg (fn () => Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
12.179 + val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
12.180 + val _ = trace_proof_msg (fn () => Int.toString (length lines) ^ " lines extracted\n")
12.181 + val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno
12.182 + val _ = trace_proof_msg (fn () => Int.toString (length ccls) ^ " conjecture clauses\n")
12.183 val ccls = map forall_intr_vars ccls
12.184 - val _ =
12.185 - if ! Sledgehammer_Fact_Preprocessor.trace then
12.186 - app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
12.187 - else
12.188 - ()
12.189 + val _ = app (fn th => trace_proof_msg (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
12.190 val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
12.191 - val _ = trace "\ndecode_tstp_file: finishing\n"
12.192 + val _ = trace_proof_msg (K "\ndecode_tstp_file: finishing\n")
12.193 in
12.194 isar_header (map #1 fixes) ^ implode ilines ^ "qed\n"
12.195 end handle STREE _ => error "Could not extract proof (ATP output malformed?)";
12.196 @@ -463,11 +452,11 @@
12.197
12.198 (*=== EXTRACTING PROOF-TEXT === *)
12.199
12.200 -val begin_proof_strings = ["# SZS output start CNFRefutation.",
12.201 +val begin_proof_strs = ["# SZS output start CNFRefutation.",
12.202 "=========== Refutation ==========",
12.203 "Here is a proof"];
12.204
12.205 -val end_proof_strings = ["# SZS output end CNFRefutation",
12.206 +val end_proof_strs = ["# SZS output end CNFRefutation",
12.207 "======= End of refutation =======",
12.208 "Formulae used in the proof"];
12.209
12.210 @@ -475,8 +464,8 @@
12.211 let
12.212 (*splits to_split by the first possible of a list of splitters*)
12.213 val (begin_string, end_string) =
12.214 - (find_first (fn s => String.isSubstring s proof) begin_proof_strings,
12.215 - find_first (fn s => String.isSubstring s proof) end_proof_strings)
12.216 + (find_first (fn s => String.isSubstring s proof) begin_proof_strs,
12.217 + find_first (fn s => String.isSubstring s proof) end_proof_strs)
12.218 in
12.219 if is_none begin_string orelse is_none end_string
12.220 then error "Could not extract proof (no substring indicating a proof)"
12.221 @@ -484,36 +473,24 @@
12.222 |> first_field (the end_string) |> the |> fst
12.223 end;
12.224
12.225 -(* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
12.226 +(* ==== CHECK IF PROOF WAS SUCCESSFUL === *)
12.227
12.228 -val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
12.229 - "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
12.230 -val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
12.231 -val failure_strings_SPASS = ["SPASS beiseite: Completion found.",
12.232 - "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."];
12.233 -val failure_strings_remote = ["Remote-script could not extract proof"];
12.234 -fun find_failure proof =
12.235 - let val failures =
12.236 - map_filter (fn s => if String.isSubstring s proof then SOME s else NONE)
12.237 - (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
12.238 - val correct = null failures andalso
12.239 - exists (fn s => String.isSubstring s proof) begin_proof_strings andalso
12.240 - exists (fn s => String.isSubstring s proof) end_proof_strings
12.241 - in
12.242 - if correct then NONE
12.243 - else if null failures then SOME "Output of ATP not in proper format"
12.244 - else SOME (hd failures) end;
12.245 +fun is_proof_well_formed proof =
12.246 + exists (fn s => String.isSubstring s proof) begin_proof_strs andalso
12.247 + exists (fn s => String.isSubstring s proof) end_proof_strs
12.248
12.249 (* === EXTRACTING LEMMAS === *)
12.250 (* lines have the form "cnf(108, axiom, ...",
12.251 the number (108) has to be extracted)*)
12.252 -fun get_step_nums false proofextract =
12.253 - let val toks = String.tokens (not o Char.isAlphaNum)
12.254 - fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
12.255 - | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok
12.256 - | inputno _ = NONE
12.257 - val lines = split_lines proofextract
12.258 - in map_filter (inputno o toks) lines end
12.259 +fun get_step_nums false extract =
12.260 + let
12.261 + val toks = String.tokens (not o Char.isAlphaNum)
12.262 + fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok
12.263 + | inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) =
12.264 + Int.fromString ntok
12.265 + | inputno _ = NONE
12.266 + val lines = split_lines extract
12.267 + in map_filter (inputno o toks) lines end
12.268 (*String contains multiple lines. We want those of the form
12.269 "253[0:Inp] et cetera..."
12.270 A list consisting of the first number in each line is returned. *)
12.271 @@ -527,27 +504,25 @@
12.272 (*extracting lemmas from tstp-output between the lines from above*)
12.273 fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
12.274 let
12.275 - (* get the names of axioms from their numbers*)
12.276 - fun get_axiom_names thm_names step_nums =
12.277 - let
12.278 - val last_axiom = Vector.length thm_names
12.279 - fun is_axiom n = n <= last_axiom
12.280 - fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count
12.281 - fun getname i = Vector.sub(thm_names, i-1)
12.282 - in
12.283 - (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
12.284 - (map getname (filter is_axiom step_nums))),
12.285 - exists is_conj step_nums)
12.286 - end
12.287 - val proofextract = get_proof_extract proof
12.288 - in
12.289 - get_axiom_names thm_names (get_step_nums proofextract)
12.290 - end;
12.291 + (* get the names of axioms from their numbers*)
12.292 + fun get_axiom_names thm_names step_nums =
12.293 + let
12.294 + val last_axiom = Vector.length thm_names
12.295 + fun is_axiom n = n <= last_axiom
12.296 + fun is_conj n = n >= fst conj_count andalso
12.297 + n < fst conj_count + snd conj_count
12.298 + fun getname i = Vector.sub(thm_names, i-1)
12.299 + in
12.300 + (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
12.301 + (map getname (filter is_axiom step_nums))),
12.302 + exists is_conj step_nums)
12.303 + end
12.304 + in get_axiom_names thm_names (get_step_nums (get_proof_extract proof)) end;
12.305
12.306 (*Used to label theorems chained into the sledgehammer call*)
12.307 val chained_hint = "CHAINED";
12.308 -val nochained = filter_out (fn y => y = chained_hint)
12.309 -
12.310 +val kill_chained = filter_out (curry (op =) chained_hint)
12.311 +
12.312 (* metis-command *)
12.313 fun metis_line [] = "apply metis"
12.314 | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
12.315 @@ -556,33 +531,36 @@
12.316 fun minimize_line _ [] = ""
12.317 | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
12.318 (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^
12.319 - space_implode " " (nochained lemmas))
12.320 + space_implode " " (kill_chained lemmas))
12.321
12.322 -fun sendback_metis_nochained lemmas =
12.323 - (Markup.markup Markup.sendback o metis_line) (nochained lemmas)
12.324 +val sendback_metis_no_chained =
12.325 + Markup.markup Markup.sendback o metis_line o kill_chained
12.326
12.327 -fun lemma_list dfg name result =
12.328 +fun metis_lemma_list dfg name result =
12.329 let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
12.330 - in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
12.331 - (if used_conj then ""
12.332 - else "\nWarning: Goal is provable because context is inconsistent."),
12.333 - nochained lemmas)
12.334 + in (sendback_metis_no_chained lemmas ^ "\n" ^ minimize_line name lemmas ^
12.335 + (if used_conj then
12.336 + ""
12.337 + else
12.338 + "\nWarning: The goal is provable because the context is inconsistent."),
12.339 + kill_chained lemmas)
12.340 end;
12.341
12.342 -(* === Extracting structured Isar-proof === *)
12.343 -fun structured_proof name (result as (proof, thm_names, conj_count, ctxt, goal, subgoalno)) =
12.344 +fun structured_isar_proof name (result as (proof, thm_names, conj_count, ctxt,
12.345 + goal, subgoalno)) =
12.346 let
12.347 - (*Could use split_lines, but it can return blank lines...*)
12.348 - val lines = String.tokens (equal #"\n");
12.349 - val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
12.350 - val proofextract = get_proof_extract proof
12.351 - val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
12.352 - val (one_line_proof, lemma_names) = lemma_list false name result
12.353 - val structured =
12.354 - if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
12.355 - else decode_tstp_file cnfs ctxt goal subgoalno thm_names
12.356 + (* Could use "split_lines", but it can return blank lines *)
12.357 + val lines = String.tokens (equal #"\n");
12.358 + val kill_spaces = String.translate (fn c => if Char.isSpace c then "" else str c)
12.359 + val extract = get_proof_extract proof
12.360 + val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
12.361 + val (one_line_proof, lemma_names) = metis_lemma_list false name result
12.362 + val structured =
12.363 + if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
12.364 + else decode_tstp_file cnfs ctxt goal subgoalno thm_names
12.365 in
12.366 - (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured, lemma_names)
12.367 -end
12.368 + (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured,
12.369 + lemma_names)
12.370 + end
12.371
12.372 end;