more Sledgehammer refactoring
authorblanchet
Fri Mar 19 13:02:18 2010 +0100 (2010-03-19)
changeset 358652f8fb5242799
parent 35843 23908b4dbc2f
child 35866 513074557e06
more Sledgehammer refactoring
src/HOL/IsaMakefile
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_minimal.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Sledgehammer/meson_tactic.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     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 -
   12.32 -val trace_path = Path.basic "atp_trace";
   12.33 +open Sledgehammer_FOL_Clause
   12.34 +open Sledgehammer_Fact_Preprocessor
   12.35  
   12.36 -fun trace s =
   12.37 -  if ! Sledgehammer_Fact_Preprocessor.trace then File.append (File.tmp_path trace_path) s
   12.38 -  else ();
   12.39 +val trace_proof_path = Path.basic "atp_trace";
   12.40 +
   12.41 +fun trace_proof_msg f =
   12.42 +  if !trace then File.append (File.tmp_path trace_proof_path) (f ()) else ();
   12.43  
   12.44  fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
   12.45  
   12.46 @@ -43,9 +39,6 @@
   12.47  (*Indicates whether to include sort information in generated proofs*)
   12.48  val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true;
   12.49  
   12.50 -(*Indicated whether to generate full proofs or just lemma lists - now via setup of atps*)
   12.51 -(* val (full_proofs, full_proofs_setup) = Attrib.config_bool "sledgehammer_full" false; *)
   12.52 -
   12.53  val setup = modulus_setup #> recon_sorts_setup;
   12.54  
   12.55  (**** PARSING OF TSTP FORMAT ****)
   12.56 @@ -109,12 +102,12 @@
   12.57  (*If string s has the prefix s1, return the result of deleting it.*)
   12.58  fun strip_prefix s1 s =
   12.59    if String.isPrefix s1 s
   12.60 -  then SOME (SFC.undo_ascii_of (String.extract (s, size s1, NONE)))
   12.61 +  then SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
   12.62    else NONE;
   12.63  
   12.64  (*Invert the table of translations between Isabelle and ATPs*)
   12.65  val type_const_trans_table_inv =
   12.66 -      Symtab.make (map swap (Symtab.dest SFC.type_const_trans_table));
   12.67 +      Symtab.make (map swap (Symtab.dest type_const_trans_table));
   12.68  
   12.69  fun invert_type_const c =
   12.70      case Symtab.lookup type_const_trans_table_inv c of
   12.71 @@ -132,15 +125,15 @@
   12.72      | Br (a,ts) =>
   12.73          let val Ts = map type_of_stree ts
   12.74          in
   12.75 -          case strip_prefix SFC.tconst_prefix a of
   12.76 +          case strip_prefix tconst_prefix a of
   12.77                SOME b => Type(invert_type_const b, Ts)
   12.78              | NONE =>
   12.79                  if not (null ts) then raise STREE t  (*only tconsts have type arguments*)
   12.80                  else
   12.81 -                case strip_prefix SFC.tfree_prefix a of
   12.82 +                case strip_prefix tfree_prefix a of
   12.83                      SOME b => TFree("'" ^ b, HOLogic.typeS)
   12.84                    | NONE =>
   12.85 -                case strip_prefix SFC.tvar_prefix a of
   12.86 +                case strip_prefix tvar_prefix a of
   12.87                      SOME b => make_tvar b
   12.88                    | NONE => make_tvar a   (*Variable from the ATP, say X1*)
   12.89          end;
   12.90 @@ -148,7 +141,7 @@
   12.91  (*Invert the table of translations between Isabelle and ATPs*)
   12.92  val const_trans_table_inv =
   12.93        Symtab.update ("fequal", "op =")
   12.94 -        (Symtab.make (map swap (Symtab.dest SFC.const_trans_table)));
   12.95 +        (Symtab.make (map swap (Symtab.dest const_trans_table)));
   12.96  
   12.97  fun invert_const c =
   12.98      case Symtab.lookup const_trans_table_inv c of
   12.99 @@ -169,9 +162,9 @@
  12.100      | Br ("hBOOL",[t]) => term_of_stree [] thy t  (*ignore hBOOL*)
  12.101      | Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t
  12.102      | Br (a,ts) =>
  12.103 -        case strip_prefix SFC.const_prefix a of
  12.104 +        case strip_prefix const_prefix a of
  12.105              SOME "equal" =>
  12.106 -              list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
  12.107 +              list_comb(Const (@{const_name "op ="}, HOLogic.typeT), List.map (term_of_stree [] thy) ts)
  12.108            | SOME b =>
  12.109                let val c = invert_const b
  12.110                    val nterms = length ts - num_typargs thy c
  12.111 @@ -183,10 +176,10 @@
  12.112            | NONE => (*a variable, not a constant*)
  12.113                let val T = HOLogic.typeT
  12.114                    val opr = (*a Free variable is typically a Skolem function*)
  12.115 -                    case strip_prefix SFC.fixed_var_prefix a of
  12.116 +                    case strip_prefix fixed_var_prefix a of
  12.117                          SOME b => Free(b,T)
  12.118                        | NONE =>
  12.119 -                    case strip_prefix SFC.schematic_var_prefix a of
  12.120 +                    case strip_prefix schematic_var_prefix a of
  12.121                          SOME b => make_var (b,T)
  12.122                        | NONE => make_var (a,T)    (*Variable from the ATP, say X1*)
  12.123                in  list_comb (opr, List.map (term_of_stree [] thy) (ts@args))  end;
  12.124 @@ -196,7 +189,7 @@
  12.125    | constraint_of_stree pol t = case t of
  12.126          Int _ => raise STREE t
  12.127        | Br (a,ts) =>
  12.128 -            (case (strip_prefix SFC.class_prefix a, map type_of_stree ts) of
  12.129 +            (case (strip_prefix class_prefix a, map type_of_stree ts) of
  12.130                   (SOME b, [T]) => (pol, b, T)
  12.131                 | _ => raise STREE t);
  12.132  
  12.133 @@ -286,7 +279,7 @@
  12.134      may disagree. We have to try all combinations of literals (quadratic!) and
  12.135      match up the variable names consistently. **)
  12.136  
  12.137 -fun strip_alls_aux n (Const("all",_)$Abs(a,T,t))  =
  12.138 +fun strip_alls_aux n (Const(@{const_name all}, _)$Abs(a,T,t))  =
  12.139        strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t))
  12.140    | strip_alls_aux _ t  =  t;
  12.141  
  12.142 @@ -347,7 +340,7 @@
  12.143    ATP may have their literals reordered.*)
  12.144  fun isar_lines ctxt ctms =
  12.145    let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term)
  12.146 -      val _ = trace ("\n\nisar_lines: start\n")
  12.147 +      val _ = trace_proof_msg (K "\n\nisar_lines: start\n")
  12.148        fun doline _ (lname, t, []) =  (*No deps: it's a conjecture clause, with no proof.*)
  12.149             (case permuted_clause t ctms of
  12.150                  SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
  12.151 @@ -399,7 +392,7 @@
  12.152    | add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines
  12.153  and delete_dep lno lines = List.foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines);
  12.154  
  12.155 -fun bad_free (Free (a,_)) = String.isPrefix "sko_" a
  12.156 +fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a
  12.157    | bad_free _ = false;
  12.158  
  12.159  (*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies.
  12.160 @@ -436,26 +429,22 @@
  12.161    | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
  12.162  
  12.163  fun decode_tstp_file cnfs ctxt th sgno thm_names =
  12.164 -  let val _ = trace "\ndecode_tstp_file: start\n"
  12.165 +  let val _ = trace_proof_msg (K "\ndecode_tstp_file: start\n")
  12.166        val tuples = map (dest_tstp o tstp_line o explode) cnfs
  12.167 -      val _ = trace (Int.toString (length tuples) ^ " tuples extracted\n")
  12.168 +      val _ = trace_proof_msg (fn () => Int.toString (length tuples) ^ " tuples extracted\n")
  12.169        val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
  12.170        val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
  12.171 -      val _ = trace (Int.toString (length raw_lines) ^ " raw_lines extracted\n")
  12.172 +      val _ = trace_proof_msg (fn () => Int.toString (length raw_lines) ^ " raw_lines extracted\n")
  12.173        val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
  12.174 -      val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
  12.175 -      val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
  12.176 -      val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
  12.177 -      val (ccls,fixes) = Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th sgno
  12.178 -      val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
  12.179 +      val _ = trace_proof_msg (fn () => Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
  12.180 +      val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
  12.181 +      val _ = trace_proof_msg (fn () => Int.toString (length lines) ^ " lines extracted\n")
  12.182 +      val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno
  12.183 +      val _ = trace_proof_msg (fn () => Int.toString (length ccls) ^ " conjecture clauses\n")
  12.184        val ccls = map forall_intr_vars ccls
  12.185 -      val _ =
  12.186 -        if ! Sledgehammer_Fact_Preprocessor.trace then
  12.187 -          app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
  12.188 -        else
  12.189 -          ()
  12.190 +      val _ = app (fn th => trace_proof_msg (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
  12.191        val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
  12.192 -      val _ = trace "\ndecode_tstp_file: finishing\n"
  12.193 +      val _ = trace_proof_msg (K "\ndecode_tstp_file: finishing\n")
  12.194    in
  12.195      isar_header (map #1 fixes) ^ implode ilines ^ "qed\n"
  12.196    end handle STREE _ => error "Could not extract proof (ATP output malformed?)";
  12.197 @@ -463,11 +452,11 @@
  12.198  
  12.199  (*=== EXTRACTING PROOF-TEXT === *)
  12.200  
  12.201 -val begin_proof_strings = ["# SZS output start CNFRefutation.",
  12.202 +val begin_proof_strs = ["# SZS output start CNFRefutation.",
  12.203    "=========== Refutation ==========",
  12.204    "Here is a proof"];
  12.205  
  12.206 -val end_proof_strings = ["# SZS output end CNFRefutation",
  12.207 +val end_proof_strs = ["# SZS output end CNFRefutation",
  12.208    "======= End of refutation =======",
  12.209    "Formulae used in the proof"];
  12.210  
  12.211 @@ -475,8 +464,8 @@
  12.212    let
  12.213      (*splits to_split by the first possible of a list of splitters*)
  12.214      val (begin_string, end_string) =
  12.215 -      (find_first (fn s => String.isSubstring s proof) begin_proof_strings,
  12.216 -      find_first (fn s => String.isSubstring s proof) end_proof_strings)
  12.217 +      (find_first (fn s => String.isSubstring s proof) begin_proof_strs,
  12.218 +      find_first (fn s => String.isSubstring s proof) end_proof_strs)
  12.219    in
  12.220      if is_none begin_string orelse is_none end_string
  12.221      then error "Could not extract proof (no substring indicating a proof)"
  12.222 @@ -484,36 +473,24 @@
  12.223                 |> first_field (the end_string) |> the |> fst
  12.224    end;
  12.225  
  12.226 -(* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
  12.227 +(* ==== CHECK IF PROOF WAS SUCCESSFUL === *)
  12.228  
  12.229 -val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
  12.230 -  "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
  12.231 -val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
  12.232 -val failure_strings_SPASS = ["SPASS beiseite: Completion found.",
  12.233 -  "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."];
  12.234 -val failure_strings_remote = ["Remote-script could not extract proof"];
  12.235 -fun find_failure proof =
  12.236 -  let val failures =
  12.237 -    map_filter (fn s => if String.isSubstring s proof then SOME s else NONE)
  12.238 -      (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
  12.239 -  val correct = null failures andalso
  12.240 -    exists (fn s => String.isSubstring s proof) begin_proof_strings andalso
  12.241 -    exists (fn s => String.isSubstring s proof) end_proof_strings
  12.242 -  in
  12.243 -    if correct then NONE
  12.244 -    else if null failures then SOME "Output of ATP not in proper format"
  12.245 -    else SOME (hd failures) end;
  12.246 +fun is_proof_well_formed proof =
  12.247 +  exists (fn s => String.isSubstring s proof) begin_proof_strs andalso
  12.248 +  exists (fn s => String.isSubstring s proof) end_proof_strs
  12.249  
  12.250  (* === EXTRACTING LEMMAS === *)
  12.251  (* lines have the form "cnf(108, axiom, ...",
  12.252  the number (108) has to be extracted)*)
  12.253 -fun get_step_nums false proofextract =
  12.254 -  let val toks = String.tokens (not o Char.isAlphaNum)
  12.255 -  fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
  12.256 -    | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok
  12.257 -    | inputno _ = NONE
  12.258 -  val lines = split_lines proofextract
  12.259 -  in  map_filter (inputno o toks) lines  end
  12.260 +fun get_step_nums false extract =
  12.261 +  let
  12.262 +    val toks = String.tokens (not o Char.isAlphaNum)
  12.263 +    fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok
  12.264 +      | inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) =
  12.265 +        Int.fromString ntok
  12.266 +      | inputno _ = NONE
  12.267 +    val lines = split_lines extract
  12.268 +  in map_filter (inputno o toks) lines end
  12.269  (*String contains multiple lines. We want those of the form
  12.270    "253[0:Inp] et cetera..."
  12.271    A list consisting of the first number in each line is returned. *)
  12.272 @@ -527,27 +504,25 @@
  12.273  (*extracting lemmas from tstp-output between the lines from above*)
  12.274  fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
  12.275    let
  12.276 -  (* get the names of axioms from their numbers*)
  12.277 -  fun get_axiom_names thm_names step_nums =
  12.278 -    let
  12.279 -    val last_axiom = Vector.length thm_names
  12.280 -    fun is_axiom n = n <= last_axiom
  12.281 -    fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count
  12.282 -    fun getname i = Vector.sub(thm_names, i-1)
  12.283 -    in
  12.284 -      (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
  12.285 -        (map getname (filter is_axiom step_nums))),
  12.286 -      exists is_conj step_nums)
  12.287 -    end
  12.288 -  val proofextract = get_proof_extract proof
  12.289 -  in
  12.290 -    get_axiom_names thm_names (get_step_nums proofextract)
  12.291 -  end;
  12.292 +    (* get the names of axioms from their numbers*)
  12.293 +    fun get_axiom_names thm_names step_nums =
  12.294 +      let
  12.295 +        val last_axiom = Vector.length thm_names
  12.296 +        fun is_axiom n = n <= last_axiom
  12.297 +        fun is_conj n = n >= fst conj_count andalso
  12.298 +                        n < fst conj_count + snd conj_count
  12.299 +        fun getname i = Vector.sub(thm_names, i-1)
  12.300 +      in
  12.301 +        (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
  12.302 +          (map getname (filter is_axiom step_nums))),
  12.303 +        exists is_conj step_nums)
  12.304 +      end
  12.305 +  in get_axiom_names thm_names (get_step_nums (get_proof_extract proof)) end;
  12.306  
  12.307  (*Used to label theorems chained into the sledgehammer call*)
  12.308  val chained_hint = "CHAINED";
  12.309 -val nochained = filter_out (fn y => y = chained_hint)
  12.310 -  
  12.311 +val kill_chained = filter_out (curry (op =) chained_hint)
  12.312 +
  12.313  (* metis-command *)
  12.314  fun metis_line [] = "apply metis"
  12.315    | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
  12.316 @@ -556,33 +531,36 @@
  12.317  fun minimize_line _ [] = ""
  12.318    | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
  12.319          (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^
  12.320 -                                         space_implode " " (nochained lemmas))
  12.321 +                                         space_implode " " (kill_chained lemmas))
  12.322  
  12.323 -fun sendback_metis_nochained lemmas =
  12.324 -  (Markup.markup Markup.sendback o metis_line) (nochained lemmas)
  12.325 +val sendback_metis_no_chained =
  12.326 +  Markup.markup Markup.sendback o metis_line o kill_chained
  12.327  
  12.328 -fun lemma_list dfg name result =
  12.329 +fun metis_lemma_list dfg name result =
  12.330    let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
  12.331 -  in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
  12.332 -    (if used_conj then ""
  12.333 -     else "\nWarning: Goal is provable because context is inconsistent."),
  12.334 -     nochained lemmas)
  12.335 +  in (sendback_metis_no_chained lemmas ^ "\n" ^ minimize_line name lemmas ^
  12.336 +    (if used_conj then
  12.337 +       ""
  12.338 +     else
  12.339 +       "\nWarning: The goal is provable because the context is inconsistent."),
  12.340 +     kill_chained lemmas)
  12.341    end;
  12.342  
  12.343 -(* === Extracting structured Isar-proof === *)
  12.344 -fun structured_proof name (result as (proof, thm_names, conj_count, ctxt, goal, subgoalno)) =
  12.345 +fun structured_isar_proof name (result as (proof, thm_names, conj_count, ctxt,
  12.346 +                                           goal, subgoalno)) =
  12.347    let
  12.348 -  (*Could use split_lines, but it can return blank lines...*)
  12.349 -  val lines = String.tokens (equal #"\n");
  12.350 -  val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
  12.351 -  val proofextract = get_proof_extract proof
  12.352 -  val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
  12.353 -  val (one_line_proof, lemma_names) = lemma_list false name result
  12.354 -  val structured =
  12.355 -    if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
  12.356 -    else decode_tstp_file cnfs ctxt goal subgoalno thm_names
  12.357 +    (* Could use "split_lines", but it can return blank lines *)
  12.358 +    val lines = String.tokens (equal #"\n");
  12.359 +    val kill_spaces = String.translate (fn c => if Char.isSpace c then "" else str c)
  12.360 +    val extract = get_proof_extract proof
  12.361 +    val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
  12.362 +    val (one_line_proof, lemma_names) = metis_lemma_list false name result
  12.363 +    val structured =
  12.364 +      if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
  12.365 +      else decode_tstp_file cnfs ctxt goal subgoalno thm_names
  12.366    in
  12.367 -  (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured, lemma_names)
  12.368 -end
  12.369 +    (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured,
  12.370 +     lemma_names)
  12.371 +  end
  12.372  
  12.373  end;