merged
authorbulwahn
Mon Mar 22 13:48:15 2010 +0100 (2010-03-22)
changeset 358925ed2e9a545ac
parent 35891 3122bdd95275
parent 35872 9b579860d59b
child 35893 02595d4a3a7c
merged
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Mar 22 08:30:13 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon Mar 22 13:48:15 2010 +0100
     1.3 @@ -63,9 +63,8 @@
     1.4        THEN' Boogie_Tactics.drop_assert_at_tac
     1.5        THEN' SUBPROOF (fn _ => Tactic.rtac thm 1) context))
     1.6  in
     1.7 -fun boogie_vc (vc_name, vc_opts) lthy =
     1.8 +fun boogie_vc (vc_name, vc_opts) thy =
     1.9    let
    1.10 -    val thy = ProofContext.theory_of lthy
    1.11      val vc = get_vc thy vc_name
    1.12  
    1.13      fun extract vc l =
    1.14 @@ -92,16 +91,16 @@
    1.15        | _ => (pair ts, K I))
    1.16  
    1.17      val discharge = fold (Boogie_VCs.discharge o pair vc_name)
    1.18 -    fun after_qed [thms] = Local_Theory.theory (discharge (vcs ~~ thms))
    1.19 +    fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
    1.20        | after_qed _ = I
    1.21    in
    1.22 -    lthy
    1.23 +    ProofContext.init thy
    1.24      |> fold Variable.auto_fixes ts
    1.25 -    |> (fn lthy1 => lthy1
    1.26 +    |> (fn ctxt1 => ctxt1
    1.27      |> prepare
    1.28 -    |-> (fn us => fn lthy2 => lthy2
    1.29 +    |-> (fn us => fn ctxt2 => ctxt2
    1.30      |> Proof.theorem_i NONE (fn thmss => fn ctxt =>
    1.31 -         let val export = map (finish lthy1) o ProofContext.export ctxt lthy2
    1.32 +         let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
    1.33           in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
    1.34    end
    1.35  end
    1.36 @@ -300,7 +299,7 @@
    1.37      "Enter into proof mode for a specific verification condition."
    1.38      OuterKeyword.thy_goal
    1.39      (vc_name -- vc_opts >> (fn args =>
    1.40 -      (Toplevel.print o Toplevel.local_theory_to_proof NONE (boogie_vc args))))
    1.41 +      (Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
    1.42  
    1.43  
    1.44  val quick_timeout = 5
     2.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Mon Mar 22 08:30:13 2010 +0100
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Mon Mar 22 13:48:15 2010 +0100
     2.3 @@ -238,10 +238,14 @@
     2.4      |> split_list_kind thy o Termtab.dest
     2.5  in
     2.6  fun add_axioms verbose axs thy =
     2.7 -  let val (used, new) = mark_axioms thy (name_axioms axs)
     2.8 +  let
     2.9 +    val (used, new) = mark_axioms thy (name_axioms axs)
    2.10 +    fun add (n, t) =
    2.11 +      Specification.axiomatization [] [((Binding.name n, []), [t])] #>>
    2.12 +      hd o hd o snd
    2.13    in
    2.14      thy
    2.15 -    |> fold_map (Drule.add_axiom o apfst Binding.name) new
    2.16 +    |> fold_map add new
    2.17      |-> Context.theory_map o fold Boogie_Axioms.add_thm
    2.18      |> log verbose "The following axioms were added:" (map fst new)
    2.19      |> (fn thy' => log verbose "The following axioms already existed:"
     3.1 --- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Mon Mar 22 08:30:13 2010 +0100
     3.2 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Mon Mar 22 13:48:15 2010 +0100
     3.3 @@ -27,6 +27,9 @@
     3.4    val state_of_vc: theory -> string -> string list * string list
     3.5    val close: theory -> theory
     3.6    val is_closed: theory -> bool
     3.7 +
     3.8 +  val rewrite_vcs: (theory -> term -> term) -> (theory -> thm -> thm) ->
     3.9 +    theory -> theory
    3.10  end
    3.11  
    3.12  structure Boogie_VCs: BOOGIE_VCS =
    3.13 @@ -252,30 +255,35 @@
    3.14  
    3.15  (* the VC store *)
    3.16  
    3.17 -fun err_vcs () = error "undischarged Boogie verification conditions found"
    3.18 +fun err_unfinished () = error "An unfinished Boogie environment is still open."
    3.19 +
    3.20 +fun err_vcs names = error (Pretty.string_of
    3.21 +  (Pretty.big_list "Undischarged Boogie verification conditions found:"
    3.22 +    (map Pretty.str names)))
    3.23  
    3.24  structure VCs = Theory_Data
    3.25  (
    3.26 -  type T = (vc * thm) Symtab.table option
    3.27 +  type T = ((vc * (term * thm)) Symtab.table * (theory -> thm -> thm)) option
    3.28    val empty = NONE
    3.29    val extend = I
    3.30    fun merge (NONE, NONE) = NONE
    3.31 -    | merge _ = err_vcs ()
    3.32 +    | merge _ = err_unfinished ()
    3.33  )
    3.34  
    3.35 -fun prep thy t = vc_of_term t |> (fn vc => (vc, thm_of thy vc))
    3.36 +fun prep thy = vc_of_term #> (fn vc => (vc, (prop_of_vc vc, thm_of thy vc)))
    3.37  
    3.38  fun set vcs thy = VCs.map (fn
    3.39 -    NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs))
    3.40 -  | SOME _ => err_vcs ()) thy
    3.41 +    NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs), K I)
    3.42 +  | SOME _ => err_unfinished ()) thy
    3.43  
    3.44  fun lookup thy name =
    3.45    (case VCs.get thy of
    3.46 -    SOME vcs => Option.map fst (Symtab.lookup vcs name)
    3.47 +    SOME (vcs, _) => Option.map fst (Symtab.lookup vcs name)
    3.48    | NONE => NONE)
    3.49  
    3.50  fun discharge (name, prf) =
    3.51 -  VCs.map (Option.map (Symtab.map_entry name (join prf)))
    3.52 +  let fun jn (vc, (t, thm)) = join prf (vc, thm) |> apsnd (pair t)
    3.53 +  in VCs.map (Option.map (apfst (Symtab.map_entry name jn))) end
    3.54  
    3.55  datatype state = Proved | NotProved | PartiallyProved
    3.56  
    3.57 @@ -284,21 +292,35 @@
    3.58      SOME vc => names_of vc
    3.59    | NONE => ([], []))
    3.60  
    3.61 +fun state_of_vc' (vc, _) =
    3.62 +  (case names_of vc of
    3.63 +    ([], _) => Proved
    3.64 +  | (_, []) => NotProved
    3.65 +  | (_, _) => PartiallyProved)
    3.66 +
    3.67  fun state_of thy =
    3.68    (case VCs.get thy of
    3.69 -    SOME vcs => Symtab.dest vcs |> map (apsnd (fst #> names_of #> (fn
    3.70 -        ([], _) => Proved
    3.71 -      | (_, []) => NotProved
    3.72 -      | (_, _) => PartiallyProved)))
    3.73 +    SOME (vcs, _) => map (apsnd state_of_vc') (Symtab.dest vcs)
    3.74    | NONE => [])
    3.75  
    3.76 +fun finished g (_, (t, thm)) = Thm.prop_of (g thm) aconv t
    3.77 +
    3.78  fun close thy = thy |> VCs.map (fn
    3.79 -    SOME _ =>
    3.80 -      if forall (fn (_, Proved) => true | _ => false) (state_of thy)
    3.81 -      then NONE
    3.82 -      else err_vcs ()
    3.83 +    SOME (vcs, g) =>
    3.84 +      let fun check vc = state_of_vc' vc = Proved andalso finished (g thy) vc
    3.85 +      in
    3.86 +        Symtab.dest vcs
    3.87 +        |> map_filter (fn (n, vc) => if check vc then NONE else SOME n)
    3.88 +        |> (fn names => if null names then NONE else err_vcs names)
    3.89 +      end
    3.90    | NONE => NONE)
    3.91  
    3.92  val is_closed = is_none o VCs.get
    3.93  
    3.94 +fun rewrite_vcs f g thy =
    3.95 +  let
    3.96 +    fun rewr (_, (t, _)) = vc_of_term (f thy t)
    3.97 +      |> (fn vc => (vc, (t, thm_of thy vc)))
    3.98 +  in VCs.map (Option.map (fn (vcs, _) => (Symtab.map rewr vcs, g))) thy end
    3.99 +
   3.100  end
     4.1 --- a/src/HOL/IsaMakefile	Mon Mar 22 08:30:13 2010 +0100
     4.2 +++ b/src/HOL/IsaMakefile	Mon Mar 22 13:48:15 2010 +0100
     4.3 @@ -313,11 +313,13 @@
     4.4    Tools/Quotient/quotient_term.ML \
     4.5    Tools/Quotient/quotient_typ.ML \
     4.6    Tools/recdef.ML \
     4.7 +  Tools/Sledgehammer/meson_tactic.ML \
     4.8    Tools/Sledgehammer/metis_tactics.ML \
     4.9    Tools/Sledgehammer/sledgehammer_fact_filter.ML \
    4.10    Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \
    4.11    Tools/Sledgehammer/sledgehammer_fol_clause.ML \
    4.12    Tools/Sledgehammer/sledgehammer_hol_clause.ML \
    4.13 +  Tools/Sledgehammer/sledgehammer_isar.ML \
    4.14    Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
    4.15    Tools/string_code.ML \
    4.16    Tools/string_syntax.ML \
     5.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Mar 22 08:30:13 2010 +0100
     5.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Mar 22 13:48:15 2010 +0100
     5.3 @@ -42,8 +42,7 @@
     5.4  
     5.5  datatype min_data = MinData of {
     5.6    succs: int,
     5.7 -  ab_ratios: int,
     5.8 -  it_ratios: int
     5.9 +  ab_ratios: int
    5.10    }
    5.11  
    5.12  fun make_sh_data
    5.13 @@ -51,23 +50,22 @@
    5.14    ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems,
    5.15           time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail}
    5.16  
    5.17 -fun make_min_data (succs, ab_ratios, it_ratios) =
    5.18 -  MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios}
    5.19 +fun make_min_data (succs, ab_ratios) =
    5.20 +  MinData{succs=succs, ab_ratios=ab_ratios}
    5.21  
    5.22  fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) =
    5.23    MeData{calls=calls, success=success, proofs=proofs, time=time,
    5.24           timeout=timeout, lemmas=lemmas, posns=posns}
    5.25  
    5.26  val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0)
    5.27 -val empty_min_data = make_min_data(0, 0, 0)
    5.28 -val empty_me_data = make_me_data(0, 0, 0, 0, 0, (0,0,0), [])
    5.29 +val empty_min_data = make_min_data (0, 0)
    5.30 +val empty_me_data = make_me_data (0, 0, 0, 0, 0, (0,0,0), [])
    5.31  
    5.32  fun tuple_of_sh_data (ShData {calls, success, lemmas, max_lems, time_isa,
    5.33    time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa,
    5.34    time_atp, time_atp_fail)
    5.35  
    5.36 -fun tuple_of_min_data (MinData {succs, ab_ratios, it_ratios}) =
    5.37 -  (succs, ab_ratios, it_ratios)
    5.38 +fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
    5.39  
    5.40  fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas,
    5.41    posns}) = (calls, success, proofs, time, timeout, lemmas, posns)
    5.42 @@ -147,13 +145,10 @@
    5.43      => (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail + t))
    5.44  
    5.45  val inc_min_succs = map_min_data
    5.46 -  (fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios))
    5.47 +  (fn (succs,ab_ratios) => (succs+1, ab_ratios))
    5.48  
    5.49  fun inc_min_ab_ratios r = map_min_data
    5.50 -  (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios))
    5.51 -
    5.52 -fun inc_min_it_ratios r = map_min_data
    5.53 -  (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r))
    5.54 +  (fn (succs, ab_ratios) => (succs, ab_ratios+r))
    5.55  
    5.56  val inc_metis_calls = map_me_data
    5.57    (fn (calls,success,proofs,time,timeout,lemmas,posns)
    5.58 @@ -234,10 +229,9 @@
    5.59    else ()
    5.60   )
    5.61  
    5.62 -fun log_min_data log (succs, ab_ratios, it_ratios) =
    5.63 +fun log_min_data log (succs, ab_ratios) =
    5.64    (log ("Number of successful minimizations: " ^ string_of_int succs);
    5.65 -   log ("After/before ratios: " ^ string_of_int ab_ratios);
    5.66 -   log ("Iterations ratios: " ^ string_of_int it_ratios)
    5.67 +   log ("After/before ratios: " ^ string_of_int ab_ratios)
    5.68    )
    5.69  
    5.70  in
    5.71 @@ -313,19 +307,19 @@
    5.72        ctxt
    5.73        |> change_dir dir
    5.74        |> Config.put ATP_Wrapper.measure_runtime true
    5.75 -    val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
    5.76 +    val problem = ATP_Manager.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
    5.77  
    5.78      val time_limit =
    5.79        (case hard_timeout of
    5.80          NONE => I
    5.81        | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
    5.82 -    val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Wrapper.prover_result,
    5.83 +    val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Manager.prover_result,
    5.84          time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
    5.85    in
    5.86      if success then (message, SH_OK (time_isa, time_atp, theorem_names))
    5.87      else (message, SH_FAIL(time_isa, time_atp))
    5.88    end
    5.89 -  handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
    5.90 +  handle Sledgehammer_HOL_Clause.TRIVIAL => ("trivial", SH_OK (0, 0, []))
    5.91         | ERROR msg => ("error: " ^ msg, SH_ERROR)
    5.92         | TimeLimit.TimeOut => ("timeout", SH_ERROR)
    5.93  
    5.94 @@ -380,9 +374,10 @@
    5.95  
    5.96  fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
    5.97    let
    5.98 +    open ATP_Minimal
    5.99      val n0 = length (these (!named_thms))
   5.100      val (prover_name, prover) = get_atp (Proof.theory_of st) args
   5.101 -    val minimize = ATP_Minimal.minimalize prover prover_name
   5.102 +    val minimize = minimize_theorems linear_minimize prover prover_name
   5.103      val timeout =
   5.104        AList.lookup (op =) args minimize_timeoutK
   5.105        |> Option.map (fst o read_int o explode)
   5.106 @@ -390,10 +385,9 @@
   5.107      val _ = log separator
   5.108    in
   5.109      case minimize timeout st (these (!named_thms)) of
   5.110 -      (SOME (named_thms',its), msg) =>
   5.111 +      (SOME named_thms', msg) =>
   5.112          (change_data id inc_min_succs;
   5.113           change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
   5.114 -         change_data id (inc_min_it_ratios ((100*its) div n0));
   5.115           if length named_thms' = n0
   5.116           then log (minimize_tag id ^ "already minimal")
   5.117           else (named_thms := SOME named_thms';
     6.1 --- a/src/HOL/Sledgehammer.thy	Mon Mar 22 08:30:13 2010 +0100
     6.2 +++ b/src/HOL/Sledgehammer.thy	Mon Mar 22 13:48:15 2010 +0100
     6.3 @@ -1,7 +1,8 @@
     6.4  (*  Title:      HOL/Sledgehammer.thy
     6.5      Author:     Lawrence C Paulson
     6.6      Author:     Jia Meng, NICTA
     6.7 -    Author:     Fabian Immler, TUM
     6.8 +    Author:     Fabian Immler, TU Muenchen
     6.9 +    Author:     Jasmin Blanchette, TU Muenchen
    6.10  *)
    6.11  
    6.12  header {* Sledgehammer: Isabelle--ATP Linkup *}
    6.13 @@ -10,7 +11,8 @@
    6.14  imports Plain Hilbert_Choice
    6.15  uses
    6.16    "Tools/polyhash.ML"
    6.17 -  "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
    6.18 +  "~~/src/Tools/Metis/metis.ML"
    6.19 +  ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
    6.20    ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
    6.21    ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
    6.22    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    6.23 @@ -18,71 +20,72 @@
    6.24    ("Tools/ATP_Manager/atp_manager.ML")
    6.25    ("Tools/ATP_Manager/atp_wrapper.ML")
    6.26    ("Tools/ATP_Manager/atp_minimal.ML")
    6.27 -  "~~/src/Tools/Metis/metis.ML"
    6.28 +  ("Tools/Sledgehammer/sledgehammer_isar.ML")
    6.29 +  ("Tools/Sledgehammer/meson_tactic.ML")
    6.30    ("Tools/Sledgehammer/metis_tactics.ML")
    6.31  begin
    6.32  
    6.33 -definition COMBI :: "'a => 'a"
    6.34 -  where "COMBI P == P"
    6.35 +definition COMBI :: "'a \<Rightarrow> 'a"
    6.36 +  where "COMBI P \<equiv> P"
    6.37  
    6.38 -definition COMBK :: "'a => 'b => 'a"
    6.39 -  where "COMBK P Q == P"
    6.40 +definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
    6.41 +  where "COMBK P Q \<equiv> P"
    6.42  
    6.43 -definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
    6.44 -  where "COMBB P Q R == P (Q R)"
    6.45 +definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
    6.46 +  where "COMBB P Q R \<equiv> P (Q R)"
    6.47  
    6.48 -definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
    6.49 -  where "COMBC P Q R == P R Q"
    6.50 +definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
    6.51 +  where "COMBC P Q R \<equiv> P R Q"
    6.52  
    6.53 -definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
    6.54 -  where "COMBS P Q R == P R (Q R)"
    6.55 +definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
    6.56 +  where "COMBS P Q R \<equiv> P R (Q R)"
    6.57  
    6.58 -definition fequal :: "'a => 'a => bool"
    6.59 -  where "fequal X Y == (X=Y)"
    6.60 +definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    6.61 +  where "fequal X Y \<equiv> (X = Y)"
    6.62  
    6.63 -lemma fequal_imp_equal: "fequal X Y ==> X=Y"
    6.64 +lemma fequal_imp_equal: "fequal X Y \<Longrightarrow> X = Y"
    6.65    by (simp add: fequal_def)
    6.66  
    6.67 -lemma equal_imp_fequal: "X=Y ==> fequal X Y"
    6.68 +lemma equal_imp_fequal: "X = Y \<Longrightarrow> fequal X Y"
    6.69    by (simp add: fequal_def)
    6.70  
    6.71  text{*These two represent the equivalence between Boolean equality and iff.
    6.72  They can't be converted to clauses automatically, as the iff would be
    6.73  expanded...*}
    6.74  
    6.75 -lemma iff_positive: "P | Q | P=Q"
    6.76 +lemma iff_positive: "P \<or> Q \<or> P = Q"
    6.77  by blast
    6.78  
    6.79 -lemma iff_negative: "~P | ~Q | P=Q"
    6.80 +lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
    6.81  by blast
    6.82  
    6.83  text{*Theorems for translation to combinators*}
    6.84  
    6.85 -lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
    6.86 +lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
    6.87  apply (rule eq_reflection)
    6.88  apply (rule ext) 
    6.89  apply (simp add: COMBS_def) 
    6.90  done
    6.91  
    6.92 -lemma abs_I: "(%x. x) == COMBI"
    6.93 +lemma abs_I: "\<lambda>x. x \<equiv> COMBI"
    6.94  apply (rule eq_reflection)
    6.95  apply (rule ext) 
    6.96  apply (simp add: COMBI_def) 
    6.97  done
    6.98  
    6.99 -lemma abs_K: "(%x. y) == COMBK y"
   6.100 +lemma abs_K: "\<lambda>x. y \<equiv> COMBK y"
   6.101  apply (rule eq_reflection)
   6.102  apply (rule ext) 
   6.103  apply (simp add: COMBK_def) 
   6.104  done
   6.105  
   6.106 -lemma abs_B: "(%x. a (g x)) == COMBB a g"
   6.107 +lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g"
   6.108  apply (rule eq_reflection)
   6.109  apply (rule ext) 
   6.110  apply (simp add: COMBB_def) 
   6.111  done
   6.112  
   6.113 -lemma abs_C: "(%x. (f x) b) == COMBC f b"
   6.114 +lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b"
   6.115  apply (rule eq_reflection)
   6.116  apply (rule ext) 
   6.117  apply (simp add: COMBC_def) 
   6.118 @@ -91,35 +94,24 @@
   6.119  
   6.120  subsection {* Setup of external ATPs *}
   6.121  
   6.122 +use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
   6.123  use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
   6.124  setup Sledgehammer_Fact_Preprocessor.setup
   6.125  use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
   6.126  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
   6.127  setup Sledgehammer_Proof_Reconstruct.setup
   6.128  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
   6.129 -
   6.130 +use "Tools/ATP_Manager/atp_manager.ML"
   6.131  use "Tools/ATP_Manager/atp_wrapper.ML"
   6.132  setup ATP_Wrapper.setup
   6.133 -use "Tools/ATP_Manager/atp_manager.ML"
   6.134  use "Tools/ATP_Manager/atp_minimal.ML"
   6.135 +use "Tools/Sledgehammer/sledgehammer_isar.ML"
   6.136  
   6.137 -text {* basic provers *}
   6.138 -setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
   6.139 -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
   6.140 -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
   6.141  
   6.142 -text {* provers with stuctured output *}
   6.143 -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
   6.144 -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
   6.145 +subsection {* The MESON prover *}
   6.146  
   6.147 -text {* on some problems better results *}
   6.148 -setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
   6.149 -
   6.150 -text {* remote provers via SystemOnTPTP *}
   6.151 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
   6.152 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
   6.153 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
   6.154 -  
   6.155 +use "Tools/Sledgehammer/meson_tactic.ML"
   6.156 +setup Meson_Tactic.setup
   6.157  
   6.158  
   6.159  subsection {* The Metis prover *}
     7.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 22 08:30:13 2010 +0100
     7.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 22 13:48:15 2010 +0100
     7.3 @@ -7,6 +7,23 @@
     7.4  
     7.5  signature ATP_MANAGER =
     7.6  sig
     7.7 +  type problem =
     7.8 +   {with_full_types: bool,
     7.9 +    subgoal: int,
    7.10 +    goal: Proof.context * (thm list * thm),
    7.11 +    axiom_clauses: (thm * (string * int)) list option,
    7.12 +    filtered_clauses: (thm * (string * int)) list option}
    7.13 +  val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
    7.14 +  type prover_result =
    7.15 +   {success: bool,
    7.16 +    message: string,
    7.17 +    theorem_names: string list,
    7.18 +    runtime: int,
    7.19 +    proof: string,
    7.20 +    internal_thm_names: string Vector.vector,
    7.21 +    filtered_clauses: (thm * (string * int)) list}
    7.22 +  type prover = int -> problem -> prover_result
    7.23 +
    7.24    val atps: string Unsynchronized.ref
    7.25    val get_atps: unit -> string list
    7.26    val timeout: int Unsynchronized.ref
    7.27 @@ -14,15 +31,43 @@
    7.28    val kill: unit -> unit
    7.29    val info: unit -> unit
    7.30    val messages: int option -> unit
    7.31 -  val add_prover: string * ATP_Wrapper.prover -> theory -> theory
    7.32 -  val get_prover: theory -> string -> ATP_Wrapper.prover option
    7.33 +  val add_prover: string * prover -> theory -> theory
    7.34 +  val get_prover: theory -> string -> prover option
    7.35    val print_provers: theory -> unit
    7.36    val sledgehammer: string list -> Proof.state -> unit
    7.37  end;
    7.38  
    7.39 -structure ATP_Manager: ATP_MANAGER =
    7.40 +structure ATP_Manager : ATP_MANAGER =
    7.41  struct
    7.42  
    7.43 +(** problems, results, and provers **)
    7.44 +
    7.45 +type problem =
    7.46 + {with_full_types: bool,
    7.47 +  subgoal: int,
    7.48 +  goal: Proof.context * (thm list * thm),
    7.49 +  axiom_clauses: (thm * (string * int)) list option,
    7.50 +  filtered_clauses: (thm * (string * int)) list option};
    7.51 +
    7.52 +fun problem_of_goal with_full_types subgoal goal : problem =
    7.53 + {with_full_types = with_full_types,
    7.54 +  subgoal = subgoal,
    7.55 +  goal = goal,
    7.56 +  axiom_clauses = NONE,
    7.57 +  filtered_clauses = NONE};
    7.58 +
    7.59 +type prover_result =
    7.60 + {success: bool,
    7.61 +  message: string,
    7.62 +  theorem_names: string list,  (*relevant theorems*)
    7.63 +  runtime: int,  (*user time of the ATP, in milliseconds*)
    7.64 +  proof: string,
    7.65 +  internal_thm_names: string Vector.vector,
    7.66 +  filtered_clauses: (thm * (string * int)) list};
    7.67 +
    7.68 +type prover = int -> problem -> prover_result;
    7.69 +
    7.70 +
    7.71  (** preferences **)
    7.72  
    7.73  val message_store_limit = 20;
    7.74 @@ -228,7 +273,7 @@
    7.75  
    7.76  structure Provers = Theory_Data
    7.77  (
    7.78 -  type T = (ATP_Wrapper.prover * stamp) Symtab.table;
    7.79 +  type T = (prover * stamp) Symtab.table;
    7.80    val empty = Symtab.empty;
    7.81    val extend = I;
    7.82    fun merge data : T = Symtab.merge (eq_snd op =) data
    7.83 @@ -261,9 +306,9 @@
    7.84          val _ = Toplevel.thread true (fn () =>
    7.85            let
    7.86              val _ = register birth_time death_time (Thread.self (), desc);
    7.87 -            val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
    7.88 +            val problem = problem_of_goal (! full_types) i (ctxt, (facts, goal));
    7.89              val message = #message (prover (! timeout) problem)
    7.90 -              handle Sledgehammer_HOL_Clause.TOO_TRIVIAL =>   (* FIXME !? *)
    7.91 +              handle Sledgehammer_HOL_Clause.TRIVIAL =>   (* FIXME !? *)
    7.92                    "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
    7.93                  | ERROR msg => ("Error: " ^ msg);
    7.94              val _ = unregister message (Thread.self ());
    7.95 @@ -282,36 +327,4 @@
    7.96      val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers;
    7.97    in () end;
    7.98  
    7.99 -
   7.100 -
   7.101 -(** Isar command syntax **)
   7.102 -
   7.103 -local structure K = OuterKeyword and P = OuterParse in
   7.104 -
   7.105 -val _ =
   7.106 -  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
   7.107 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
   7.108 -
   7.109 -val _ =
   7.110 -  OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
   7.111 -    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
   7.112 -
   7.113 -val _ =
   7.114 -  OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
   7.115 -    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
   7.116 -      (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
   7.117 -
   7.118 -val _ =
   7.119 -  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
   7.120 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
   7.121 -      Toplevel.keep (print_provers o Toplevel.theory_of)));
   7.122 -
   7.123 -val _ =
   7.124 -  OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
   7.125 -    (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
   7.126 -      Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
   7.127 -
   7.128  end;
   7.129 -
   7.130 -end;
   7.131 -
     8.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Mar 22 08:30:13 2010 +0100
     8.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Mar 22 13:48:15 2010 +0100
     8.3 @@ -1,32 +1,40 @@
     8.4  (*  Title:      HOL/Tools/ATP_Manager/atp_minimal.ML
     8.5      Author:     Philipp Meyer, TU Muenchen
     8.6  
     8.7 -Minimization of theorem list for metis by using an external automated theorem prover
     8.8 +Minimization of theorem list for Metis using automatic theorem provers.
     8.9  *)
    8.10  
    8.11  signature ATP_MINIMAL =
    8.12  sig
    8.13 -  val minimize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
    8.14 -    (string * thm list) list -> ((string * thm list) list * int) option * string
    8.15 -  (* To be removed once TN has finished his measurements;
    8.16 -     the int component of the result should then be removed: *)
    8.17 -  val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
    8.18 -    (string * thm list) list -> ((string * thm list) list * int) option * string
    8.19 -end
    8.20 +  type prover = ATP_Manager.prover
    8.21 +  type prover_result = ATP_Manager.prover_result
    8.22 +  type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
    8.23  
    8.24 -structure ATP_Minimal: ATP_MINIMAL =
    8.25 +  val linear_minimize : 'a minimize_fun
    8.26 +  val binary_minimize : 'a minimize_fun
    8.27 +  val minimize_theorems :
    8.28 +    (string * thm list) minimize_fun -> prover -> string -> int
    8.29 +    -> Proof.state -> (string * thm list) list
    8.30 +    -> (string * thm list) list option * string
    8.31 +end;
    8.32 +
    8.33 +structure ATP_Minimal : ATP_MINIMAL =
    8.34  struct
    8.35  
    8.36 -(* Linear minimization *)
    8.37 +open Sledgehammer_Fact_Preprocessor
    8.38 +open ATP_Manager
    8.39 +
    8.40 +type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
    8.41 +
    8.42 +(* Linear minimization algorithm *)
    8.43  
    8.44 -fun lin_gen_minimize p s =
    8.45 -let
    8.46 -  fun min [] needed = needed
    8.47 -    | min (x::xs) needed =
    8.48 -        if p(xs @ needed) then min xs needed else min xs (x::needed)
    8.49 -in (min s [], length s) end;
    8.50 +fun linear_minimize p s =
    8.51 +  let
    8.52 +    fun aux [] needed = needed
    8.53 +      | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x)
    8.54 +  in aux s [] end;
    8.55  
    8.56 -(* Clever minimalization algorithm *)
    8.57 +(* Binary minimalization *)
    8.58  
    8.59  local
    8.60    fun isplit (l, r) [] = (l, r)
    8.61 @@ -37,24 +45,21 @@
    8.62  end
    8.63  
    8.64  local
    8.65 -  fun min p sup [] = raise Empty
    8.66 -    | min p sup [s0] = [s0]
    8.67 +  fun min _ _ [] = raise Empty
    8.68 +    | min _ _ [s0] = [s0]
    8.69      | min p sup s =
    8.70        let
    8.71          val (l0, r0) = split s
    8.72        in
    8.73 -        if p (sup @ l0)
    8.74 -        then min p sup l0
    8.75 +        if p (sup @ l0) then
    8.76 +          min p sup l0
    8.77 +        else if p (sup @ r0) then
    8.78 +          min p sup r0
    8.79          else
    8.80 -          if p (sup @ r0)
    8.81 -          then min p sup r0
    8.82 -          else
    8.83 -            let
    8.84 -              val l = min p (sup @ r0) l0
    8.85 -              val r = min p (sup @ l) r0
    8.86 -            in
    8.87 -              l @ r
    8.88 -            end
    8.89 +          let
    8.90 +            val l = min p (sup @ r0) l0
    8.91 +            val r = min p (sup @ l) r0
    8.92 +          in l @ r end
    8.93        end
    8.94  in
    8.95    (* return a minimal subset v of s that satisfies p
    8.96 @@ -62,15 +67,10 @@
    8.97     @post v subset s & p(v) &
    8.98           forall e in v. ~p(v \ e)
    8.99     *)
   8.100 -  fun minimal p s =
   8.101 -    let
   8.102 -      val count = Unsynchronized.ref 0
   8.103 -      fun p_count xs = (Unsynchronized.inc count; p xs)
   8.104 -      val v =
   8.105 -        (case min p_count [] s of
   8.106 -          [x] => if p_count [] then [] else [x]
   8.107 -        | m => m);
   8.108 -    in (v, ! count) end
   8.109 +  fun binary_minimize p s =
   8.110 +    case min p [] s of
   8.111 +      [x] => if p [] then [] else [x]
   8.112 +    | m => m
   8.113  end
   8.114  
   8.115  
   8.116 @@ -91,32 +91,31 @@
   8.117     ("# Cannot determine problem status within resource limit", Timeout),
   8.118     ("Error", Error)]
   8.119  
   8.120 -fun produce_answer (result: ATP_Wrapper.prover_result) =
   8.121 -  let
   8.122 -    val {success, proof = result_string, internal_thm_names = thm_name_vec,
   8.123 -      filtered_clauses = filtered, ...} = result
   8.124 -  in
   8.125 -    if success then
   8.126 -      (Success (Vector.foldr (op ::) [] thm_name_vec, filtered), result_string)
   8.127 -    else
   8.128 -      let
   8.129 -        val failure = failure_strings |> get_first (fn (s, t) =>
   8.130 -            if String.isSubstring s result_string then SOME (t, result_string) else NONE)
   8.131 -      in
   8.132 -        (case failure of
   8.133 -          SOME res => res
   8.134 -        | NONE => (Failure, result_string))
   8.135 -      end
   8.136 -  end
   8.137 +fun produce_answer ({success, proof, internal_thm_names, filtered_clauses, ...}
   8.138 +                    : prover_result) =
   8.139 +  if success then
   8.140 +    (Success (Vector.foldr (op ::) [] internal_thm_names, filtered_clauses),
   8.141 +     proof)
   8.142 +  else
   8.143 +    let
   8.144 +      val failure = failure_strings |> get_first (fn (s, t) =>
   8.145 +          if String.isSubstring s proof then SOME (t, proof) else NONE)
   8.146 +    in
   8.147 +      (case failure of
   8.148 +        SOME res => res
   8.149 +      | NONE => (Failure, proof))
   8.150 +    end
   8.151  
   8.152  
   8.153  (* wrapper for calling external prover *)
   8.154  
   8.155 -fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs =
   8.156 +fun sledgehammer_test_theorems prover time_limit subgoalno state filtered
   8.157 +                               name_thms_pairs =
   8.158    let
   8.159 -    val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
   8.160 +    val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
   8.161 +                      " theorems... ")
   8.162      val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
   8.163 -    val axclauses = Sledgehammer_Fact_Preprocessor.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
   8.164 +    val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
   8.165      val {context = ctxt, facts, goal} = Proof.goal state
   8.166      val problem =
   8.167       {with_full_types = ! ATP_Manager.full_types,
   8.168 @@ -126,20 +125,19 @@
   8.169        filtered_clauses = filtered}
   8.170      val (result, proof) = produce_answer (prover time_limit problem)
   8.171      val _ = priority (string_of_result result)
   8.172 -  in
   8.173 -    (result, proof)
   8.174 -  end
   8.175 +  in (result, proof) end
   8.176  
   8.177  
   8.178  (* minimalization of thms *)
   8.179  
   8.180 -fun gen_minimalize gen_min prover prover_name time_limit state name_thms_pairs =
   8.181 +fun minimize_theorems gen_min prover prover_name time_limit state
   8.182 +                      name_thms_pairs =
   8.183    let
   8.184      val _ =
   8.185        priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
   8.186          " theorems, prover: " ^ prover_name ^
   8.187          ", time limit: " ^ string_of_int time_limit ^ " seconds")
   8.188 -    val test_thms_fun = sh_test_thms prover time_limit 1 state
   8.189 +    val test_thms_fun = sledgehammer_test_theorems prover time_limit 1 state
   8.190      fun test_thms filtered thms =
   8.191        case test_thms_fun filtered thms of (Success _, _) => true | _ => false
   8.192    in
   8.193 @@ -152,15 +150,14 @@
   8.194              if length ordered_used < length name_thms_pairs then
   8.195                filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
   8.196              else name_thms_pairs
   8.197 -          val (min_thms, n) =
   8.198 -            if null to_use then ([], 0)
   8.199 +          val min_thms =
   8.200 +            if null to_use then []
   8.201              else gen_min (test_thms (SOME filtered)) to_use
   8.202            val min_names = sort_distinct string_ord (map fst min_thms)
   8.203            val _ = priority (cat_lines
   8.204 -            ["Iterations: " ^ string_of_int n (* FIXME TN remove later *),
   8.205 -             "Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
   8.206 +            ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
   8.207          in
   8.208 -          (SOME (min_thms, n), "Try this command: " ^
   8.209 +          (SOME min_thms, "Try this command: " ^
   8.210              Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
   8.211          end
   8.212      | (Timeout, _) =>
   8.213 @@ -170,68 +167,9 @@
   8.214          (NONE, "Error in prover: " ^ msg)
   8.215      | (Failure, _) =>
   8.216          (NONE, "Failure: No proof with the theorems supplied"))
   8.217 -    handle Sledgehammer_HOL_Clause.TOO_TRIVIAL =>
   8.218 -        (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
   8.219 +    handle Sledgehammer_HOL_Clause.TRIVIAL =>
   8.220 +        (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
   8.221        | ERROR msg => (NONE, "Error: " ^ msg)
   8.222    end
   8.223  
   8.224 -
   8.225 -(* Isar command and parsing input *)
   8.226 -
   8.227 -local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
   8.228 -
   8.229 -fun get_thms context =
   8.230 -  map (fn (name, interval) =>
   8.231 -    let
   8.232 -      val thmref = Facts.Named ((name, Position.none), interval)
   8.233 -      val ths = ProofContext.get_fact context thmref
   8.234 -      val name' = Facts.string_of_ref thmref
   8.235 -    in
   8.236 -      (name', ths)
   8.237 -    end)
   8.238 -
   8.239 -val default_prover = "remote_vampire"
   8.240 -val default_time_limit = 5
   8.241 -
   8.242 -fun get_time_limit_arg time_string =
   8.243 -  (case Int.fromString time_string of
   8.244 -    SOME t => t
   8.245 -  | NONE => error ("Invalid time limit: " ^ quote time_string))
   8.246 -
   8.247 -fun get_opt (name, a) (p, t) =
   8.248 -  (case name of
   8.249 -    "time" => (p, get_time_limit_arg a)
   8.250 -  | "atp" => (a, t)
   8.251 -  | n => error ("Invalid argument: " ^ n))
   8.252 -
   8.253 -fun get_options args = fold get_opt args (default_prover, default_time_limit)
   8.254 -
   8.255 -val minimize = gen_minimalize lin_gen_minimize
   8.256 -
   8.257 -val minimalize = gen_minimalize minimal
   8.258 -
   8.259 -fun sh_min_command args thm_names state =
   8.260 -  let
   8.261 -    val (prover_name, time_limit) = get_options args
   8.262 -    val prover =
   8.263 -      (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
   8.264 -        SOME prover => prover
   8.265 -      | NONE => error ("Unknown prover: " ^ quote prover_name))
   8.266 -    val name_thms_pairs = get_thms (Proof.context_of state) thm_names
   8.267 -  in
   8.268 -    writeln (#2 (minimize prover prover_name time_limit state name_thms_pairs))
   8.269 -  end
   8.270 -
   8.271 -val parse_args =
   8.272 -  Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
   8.273 -val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
   8.274 -
   8.275 -val _ =
   8.276 -  OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
   8.277 -    (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
   8.278 -      Toplevel.no_timing o Toplevel.unknown_proof o
   8.279 -        Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of)))
   8.280 -
   8.281 -end
   8.282 -
   8.283 -end
   8.284 +end;
     9.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Mar 22 08:30:13 2010 +0100
     9.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Mar 22 13:48:15 2010 +0100
     9.3 @@ -6,54 +6,24 @@
     9.4  
     9.5  signature ATP_WRAPPER =
     9.6  sig
     9.7 -  (*hooks for problem files*)
     9.8 -  val destdir: string Config.T
     9.9 -  val problem_prefix: string Config.T
    9.10 -  val measure_runtime: bool Config.T
    9.11 -  val setup: theory -> theory
    9.12 +  type prover = ATP_Manager.prover
    9.13  
    9.14 -  (*prover configuration, problem format, and prover result*)
    9.15 -  type prover_config =
    9.16 -   {command: Path.T,
    9.17 -    arguments: int -> string,
    9.18 -    max_new_clauses: int,
    9.19 -    insert_theory_const: bool,
    9.20 -    emit_structured_proof: bool}
    9.21 -  type problem =
    9.22 -   {with_full_types: bool,
    9.23 -    subgoal: int,
    9.24 -    goal: Proof.context * (thm list * thm),
    9.25 -    axiom_clauses: (thm * (string * int)) list option,
    9.26 -    filtered_clauses: (thm * (string * int)) list option}
    9.27 -  val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
    9.28 -  type prover_result =
    9.29 -   {success: bool,
    9.30 -    message: string,
    9.31 -    theorem_names: string list,
    9.32 -    runtime: int,
    9.33 -    proof: string,
    9.34 -    internal_thm_names: string Vector.vector,
    9.35 -    filtered_clauses: (thm * (string * int)) list}
    9.36 -  type prover = int -> problem -> prover_result
    9.37 +  (* hooks for problem files *)
    9.38 +  val destdir : string Config.T
    9.39 +  val problem_prefix : string Config.T
    9.40 +  val measure_runtime : bool Config.T
    9.41  
    9.42 -  (*common provers*)
    9.43 -  val vampire: string * prover
    9.44 -  val vampire_full: string * prover
    9.45 -  val eprover: string * prover
    9.46 -  val eprover_full: string * prover
    9.47 -  val spass: string * prover
    9.48 -  val spass_no_tc: string * prover
    9.49 -  val remote_vampire: string * prover
    9.50 -  val remote_eprover: string * prover
    9.51 -  val remote_spass: string * prover
    9.52 -  val refresh_systems: unit -> unit
    9.53 +  val refresh_systems_on_tptp : unit -> unit
    9.54 +  val setup : theory -> theory
    9.55  end;
    9.56  
    9.57 -structure ATP_Wrapper: ATP_WRAPPER =
    9.58 +structure ATP_Wrapper : ATP_WRAPPER =
    9.59  struct
    9.60  
    9.61 -structure SFF = Sledgehammer_Fact_Filter
    9.62 -structure SPR = Sledgehammer_Proof_Reconstruct
    9.63 +open Sledgehammer_HOL_Clause
    9.64 +open Sledgehammer_Fact_Filter
    9.65 +open Sledgehammer_Proof_Reconstruct
    9.66 +open ATP_Manager
    9.67  
    9.68  (** generic ATP wrapper **)
    9.69  
    9.70 @@ -68,43 +38,17 @@
    9.71  val (measure_runtime, measure_runtime_setup) =
    9.72    Attrib.config_bool "atp_measure_runtime" false;
    9.73  
    9.74 -val setup = destdir_setup #> problem_prefix_setup #> measure_runtime_setup;
    9.75  
    9.76 -
    9.77 -(* prover configuration, problem format, and prover result *)
    9.78 +(* prover configuration *)
    9.79  
    9.80  type prover_config =
    9.81   {command: Path.T,
    9.82    arguments: int -> string,
    9.83 +  failure_strs: string list,
    9.84    max_new_clauses: int,
    9.85    insert_theory_const: bool,
    9.86    emit_structured_proof: bool};
    9.87  
    9.88 -type problem =
    9.89 - {with_full_types: bool,
    9.90 -  subgoal: int,
    9.91 -  goal: Proof.context * (thm list * thm),
    9.92 -  axiom_clauses: (thm * (string * int)) list option,
    9.93 -  filtered_clauses: (thm * (string * int)) list option};
    9.94 -
    9.95 -fun problem_of_goal with_full_types subgoal goal : problem =
    9.96 - {with_full_types = with_full_types,
    9.97 -  subgoal = subgoal,
    9.98 -  goal = goal,
    9.99 -  axiom_clauses = NONE,
   9.100 -  filtered_clauses = NONE};
   9.101 -
   9.102 -type prover_result =
   9.103 - {success: bool,
   9.104 -  message: string,
   9.105 -  theorem_names: string list,  (*relevant theorems*)
   9.106 -  runtime: int,  (*user time of the ATP, in milliseconds*)
   9.107 -  proof: string,
   9.108 -  internal_thm_names: string Vector.vector,
   9.109 -  filtered_clauses: (thm * (string * int)) list};
   9.110 -
   9.111 -type prover = int -> problem -> prover_result;
   9.112 -
   9.113  
   9.114  (* basic template *)
   9.115  
   9.116 @@ -114,13 +58,20 @@
   9.117    |> Exn.release
   9.118    |> tap (after path);
   9.119  
   9.120 -fun external_prover relevance_filter prepare write cmd args produce_answer name
   9.121 -    ({with_full_types, subgoal, goal, axiom_clauses, filtered_clauses}: problem) =
   9.122 +fun find_failure strs proof =
   9.123 +  case filter (fn s => String.isSubstring s proof) strs of
   9.124 +    [] => if is_proof_well_formed proof then NONE
   9.125 +          else SOME "Ill-formed ATP output"
   9.126 +  | (failure :: _) => SOME failure
   9.127 +
   9.128 +fun external_prover relevance_filter prepare write cmd args failure_strs
   9.129 +        produce_answer name ({with_full_types, subgoal, goal, axiom_clauses,
   9.130 +                              filtered_clauses}: problem) =
   9.131    let
   9.132      (* get clauses and prepare them for writing *)
   9.133      val (ctxt, (chain_ths, th)) = goal;
   9.134      val thy = ProofContext.theory_of ctxt;
   9.135 -    val chain_ths = map (Thm.put_name_hint SPR.chained_hint) chain_ths;
   9.136 +    val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
   9.137      val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal);
   9.138      val the_filtered_clauses =
   9.139        (case filtered_clauses of
   9.140 @@ -184,7 +135,7 @@
   9.141        with_path cleanup export run_on (prob_pathname subgoal);
   9.142  
   9.143      (* check for success and print out some information on failure *)
   9.144 -    val failure = SPR.find_failure proof;
   9.145 +    val failure = find_failure failure_strs proof;
   9.146      val success = rc = 0 andalso is_none failure;
   9.147      val (message, real_thm_names) =
   9.148        if is_some failure then ("External prover failed.", [])
   9.149 @@ -200,25 +151,16 @@
   9.150  
   9.151  (* generic TPTP-based provers *)
   9.152  
   9.153 -fun gen_tptp_prover (name, prover_config) timeout problem =
   9.154 -  let
   9.155 -    val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} =
   9.156 -      prover_config;
   9.157 -  in
   9.158 -    external_prover
   9.159 -      (SFF.get_relevant max_new_clauses insert_theory_const)
   9.160 -      (SFF.prepare_clauses false)
   9.161 -      Sledgehammer_HOL_Clause.tptp_write_file
   9.162 -      command
   9.163 -      (arguments timeout)
   9.164 -      (if emit_structured_proof then SPR.structured_proof
   9.165 -       else SPR.lemma_list false)
   9.166 -      name
   9.167 -      problem
   9.168 -  end;
   9.169 +fun generic_tptp_prover
   9.170 +        (name, {command, arguments, failure_strs, max_new_clauses,
   9.171 +                insert_theory_const, emit_structured_proof}) timeout =
   9.172 +  external_prover (get_relevant_facts max_new_clauses insert_theory_const)
   9.173 +      (prepare_clauses false) write_tptp_file command (arguments timeout)
   9.174 +      failure_strs
   9.175 +      (if emit_structured_proof then structured_isar_proof
   9.176 +       else metis_lemma_list false) name;
   9.177  
   9.178 -fun tptp_prover (name, config) = (name, gen_tptp_prover (name, config));
   9.179 -
   9.180 +fun tptp_prover (name, p) = (name, generic_tptp_prover (name, p));
   9.181  
   9.182  
   9.183  (** common provers **)
   9.184 @@ -227,40 +169,51 @@
   9.185  
   9.186  (*NB: Vampire does not work without explicit timelimit*)
   9.187  
   9.188 +val vampire_failure_strs =
   9.189 +  ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
   9.190  val vampire_max_new_clauses = 60;
   9.191  val vampire_insert_theory_const = false;
   9.192  
   9.193 -fun vampire_prover_config full : prover_config =
   9.194 +fun vampire_prover_config isar : prover_config =
   9.195   {command = Path.explode "$VAMPIRE_HOME/vampire",
   9.196    arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
   9.197      " -t " ^ string_of_int timeout),
   9.198 +  failure_strs = vampire_failure_strs,
   9.199    max_new_clauses = vampire_max_new_clauses,
   9.200    insert_theory_const = vampire_insert_theory_const,
   9.201 -  emit_structured_proof = full};
   9.202 +  emit_structured_proof = isar};
   9.203  
   9.204  val vampire = tptp_prover ("vampire", vampire_prover_config false);
   9.205 -val vampire_full = tptp_prover ("vampire_full", vampire_prover_config true);
   9.206 +val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
   9.207  
   9.208  
   9.209  (* E prover *)
   9.210  
   9.211 +val eprover_failure_strs =
   9.212 +  ["SZS status: Satisfiable", "SZS status Satisfiable",
   9.213 +   "SZS status: ResourceOut", "SZS status ResourceOut",
   9.214 +   "# Cannot determine problem status"];
   9.215  val eprover_max_new_clauses = 100;
   9.216  val eprover_insert_theory_const = false;
   9.217  
   9.218 -fun eprover_config full : prover_config =
   9.219 +fun eprover_config isar : prover_config =
   9.220   {command = Path.explode "$E_HOME/eproof",
   9.221    arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
   9.222      " --silent --cpu-limit=" ^ string_of_int timeout),
   9.223 +  failure_strs = eprover_failure_strs,
   9.224    max_new_clauses = eprover_max_new_clauses,
   9.225    insert_theory_const = eprover_insert_theory_const,
   9.226 -  emit_structured_proof = full};
   9.227 +  emit_structured_proof = isar};
   9.228  
   9.229  val eprover = tptp_prover ("e", eprover_config false);
   9.230 -val eprover_full = tptp_prover ("e_full", eprover_config true);
   9.231 +val eprover_isar = tptp_prover ("e_isar", eprover_config true);
   9.232  
   9.233  
   9.234  (* SPASS *)
   9.235  
   9.236 +val spass_failure_strs =
   9.237 +  ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
   9.238 +   "SPASS beiseite: Maximal number of loops exceeded."];
   9.239  val spass_max_new_clauses = 40;
   9.240  val spass_insert_theory_const = true;
   9.241  
   9.242 @@ -268,26 +221,25 @@
   9.243   {command = Path.explode "$SPASS_HOME/SPASS",
   9.244    arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
   9.245      " -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout),
   9.246 +  failure_strs = spass_failure_strs,
   9.247    max_new_clauses = spass_max_new_clauses,
   9.248    insert_theory_const = insert_theory_const,
   9.249    emit_structured_proof = false};
   9.250  
   9.251 -fun gen_dfg_prover (name, prover_config: prover_config) timeout problem =
   9.252 -  let
   9.253 -    val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config;
   9.254 -  in
   9.255 -    external_prover
   9.256 -      (SFF.get_relevant max_new_clauses insert_theory_const)
   9.257 -      (SFF.prepare_clauses true)
   9.258 -      Sledgehammer_HOL_Clause.dfg_write_file
   9.259 -      command
   9.260 -      (arguments timeout)
   9.261 -      (SPR.lemma_list true)
   9.262 -      name
   9.263 -      problem
   9.264 -  end;
   9.265 +fun generic_dfg_prover
   9.266 +        (name, ({command, arguments, failure_strs, max_new_clauses,
   9.267 +                 insert_theory_const, ...} : prover_config)) timeout =
   9.268 +  external_prover
   9.269 +    (get_relevant_facts max_new_clauses insert_theory_const)
   9.270 +    (prepare_clauses true)
   9.271 +    write_dfg_file
   9.272 +    command
   9.273 +    (arguments timeout)
   9.274 +    failure_strs
   9.275 +    (metis_lemma_list true)
   9.276 +    name;
   9.277  
   9.278 -fun dfg_prover (name, config) = (name, gen_dfg_prover (name, config));
   9.279 +fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
   9.280  
   9.281  val spass = dfg_prover ("spass", spass_config spass_insert_theory_const);
   9.282  val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false);
   9.283 @@ -305,7 +257,8 @@
   9.284      else split_lines answer
   9.285    end;
   9.286  
   9.287 -fun refresh_systems () = Synchronized.change systems (fn _ => get_systems ());
   9.288 +fun refresh_systems_on_tptp () =
   9.289 +  Synchronized.change systems (fn _ => get_systems ());
   9.290  
   9.291  fun get_system prefix = Synchronized.change_result systems (fn systems =>
   9.292    (if null systems then get_systems () else systems)
   9.293 @@ -316,10 +269,13 @@
   9.294      NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP")
   9.295    | SOME sys => sys);
   9.296  
   9.297 +val remote_failure_strs = ["Remote-script could not extract proof"];
   9.298 +
   9.299  fun remote_prover_config prover_prefix args max_new insert_tc: prover_config =
   9.300   {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
   9.301 -  arguments =
   9.302 -    (fn timeout => args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
   9.303 +  arguments = (fn timeout =>
   9.304 +    args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
   9.305 +  failure_strs = remote_failure_strs,
   9.306    max_new_clauses = max_new,
   9.307    insert_theory_const = insert_tc,
   9.308    emit_structured_proof = false};
   9.309 @@ -333,4 +289,15 @@
   9.310  val remote_spass = tptp_prover ("remote_spass", remote_prover_config
   9.311    "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
   9.312  
   9.313 +val provers =
   9.314 +  [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc,
   9.315 +   remote_vampire, remote_spass, remote_eprover]
   9.316 +val prover_setup = fold add_prover provers
   9.317 +
   9.318 +val setup =
   9.319 +  destdir_setup
   9.320 +  #> problem_prefix_setup
   9.321 +  #> measure_runtime_setup
   9.322 +  #> prover_setup;
   9.323 +
   9.324  end;
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Mar 22 08:30:13 2010 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Mar 22 13:48:15 2010 +0100
    10.3 @@ -13,7 +13,7 @@
    10.4    val auto: bool Unsynchronized.ref
    10.5    val default_params : theory -> (string * string) list -> params
    10.6    val setup : theory -> theory
    10.7 -end
    10.8 +end;
    10.9  
   10.10  structure Nitpick_Isar : NITPICK_ISAR =
   10.11  struct
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Mar 22 08:30:13 2010 +0100
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Mar 22 13:48:15 2010 +0100
    11.3 @@ -12,7 +12,7 @@
    11.4      hol_context -> (typ option * bool option) list
    11.5      -> (typ option * bool option) list -> term
    11.6      -> term list * term list * bool * bool * bool
    11.7 -end
    11.8 +end;
    11.9  
   11.10  structure Nitpick_Preproc : NITPICK_PREPROC =
   11.11  struct
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Mar 22 08:30:13 2010 +0100
    12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Mar 22 13:48:15 2010 +0100
    12.3 @@ -8,7 +8,7 @@
    12.4  signature NITPICK_TESTS =
    12.5  sig
    12.6    val run_all_tests : unit -> unit
    12.7 -end
    12.8 +end;
    12.9  
   12.10  structure Nitpick_Tests =
   12.11  struct
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Mar 22 08:30:13 2010 +0100
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Mar 22 13:48:15 2010 +0100
    13.3 @@ -62,7 +62,7 @@
    13.4    val pstrs : string -> Pretty.T list
    13.5    val unyxml : string -> string
    13.6    val maybe_quote : string -> string
    13.7 -end
    13.8 +end;
    13.9  
   13.10  structure Nitpick_Util : NITPICK_UTIL =
   13.11  struct
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Mon Mar 22 13:48:15 2010 +0100
    14.3 @@ -0,0 +1,53 @@
    14.4 +(*  Title:      HOL/Tools/Sledgehammer/meson_tactic.ML
    14.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory
    14.6 +
    14.7 +MESON general tactic and proof method.
    14.8 +*)
    14.9 +
   14.10 +signature MESON_TACTIC =
   14.11 +sig
   14.12 +  val expand_defs_tac : thm -> tactic
   14.13 +  val meson_general_tac : Proof.context -> thm list -> int -> tactic
   14.14 +  val setup: theory -> theory
   14.15 +end;
   14.16 +
   14.17 +structure Meson_Tactic : MESON_TACTIC =
   14.18 +struct
   14.19 +
   14.20 +open Sledgehammer_Fact_Preprocessor
   14.21 +
   14.22 +(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
   14.23 +fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ u) =
   14.24 +    String.isPrefix skolem_prefix a
   14.25 +  | is_absko _ = false;
   14.26 +
   14.27 +fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ u) =   (*Definition of Free, not in certain terms*)
   14.28 +      is_Free t andalso not (member (op aconv) xs t)
   14.29 +  | is_okdef _ _ = false
   14.30 +
   14.31 +(*This function tries to cope with open locales, which introduce hypotheses of the form
   14.32 +  Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
   14.33 +  of sko_ functions. *)
   14.34 +fun expand_defs_tac st0 st =
   14.35 +  let val hyps0 = #hyps (rep_thm st0)
   14.36 +      val hyps = #hyps (crep_thm st)
   14.37 +      val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
   14.38 +      val defs = filter (is_absko o Thm.term_of) newhyps
   14.39 +      val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
   14.40 +                                      (map Thm.term_of hyps)
   14.41 +      val fixed = OldTerm.term_frees (concl_of st) @
   14.42 +                  fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
   14.43 +  in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
   14.44 +
   14.45 +fun meson_general_tac ctxt ths i st0 =
   14.46 +  let
   14.47 +    val thy = ProofContext.theory_of ctxt
   14.48 +    val ctxt0 = Classical.put_claset HOL_cs ctxt
   14.49 +  in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
   14.50 +
   14.51 +val setup =
   14.52 +  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
   14.53 +    SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
   14.54 +    "MESON resolution proof procedure";
   14.55 +
   14.56 +end;
    15.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Mar 22 08:30:13 2010 +0100
    15.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Mar 22 13:48:15 2010 +0100
    15.3 @@ -18,9 +18,11 @@
    15.4  structure Metis_Tactics : METIS_TACTICS =
    15.5  struct
    15.6  
    15.7 -structure SFC = Sledgehammer_FOL_Clause
    15.8 -structure SHC = Sledgehammer_HOL_Clause
    15.9 -structure SPR = Sledgehammer_Proof_Reconstruct
   15.10 +open Sledgehammer_FOL_Clause
   15.11 +open Sledgehammer_Fact_Preprocessor
   15.12 +open Sledgehammer_HOL_Clause
   15.13 +open Sledgehammer_Proof_Reconstruct
   15.14 +open Sledgehammer_Fact_Filter
   15.15  
   15.16  val trace = Unsynchronized.ref false;
   15.17  fun trace_msg msg = if !trace then tracing (msg ()) else ();
   15.18 @@ -67,62 +69,62 @@
   15.19  
   15.20  fun metis_lit b c args = (b, (c, args));
   15.21  
   15.22 -fun hol_type_to_fol (SFC.AtomV x) = Metis.Term.Var x
   15.23 -  | hol_type_to_fol (SFC.AtomF x) = Metis.Term.Fn(x,[])
   15.24 -  | hol_type_to_fol (SFC.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
   15.25 +fun hol_type_to_fol (AtomV x) = Metis.Term.Var x
   15.26 +  | hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, [])
   15.27 +  | hol_type_to_fol (Comp (tc, tps)) =
   15.28 +    Metis.Term.Fn (tc, map hol_type_to_fol tps);
   15.29  
   15.30  (*These two functions insert type literals before the real literals. That is the
   15.31    opposite order from TPTP linkup, but maybe OK.*)
   15.32  
   15.33  fun hol_term_to_fol_FO tm =
   15.34 -  case SHC.strip_comb tm of
   15.35 -      (SHC.CombConst(c,_,tys), tms) =>
   15.36 +  case strip_combterm_comb tm of
   15.37 +      (CombConst(c,_,tys), tms) =>
   15.38          let val tyargs = map hol_type_to_fol tys
   15.39              val args   = map hol_term_to_fol_FO tms
   15.40          in Metis.Term.Fn (c, tyargs @ args) end
   15.41 -    | (SHC.CombVar(v,_), []) => Metis.Term.Var v
   15.42 +    | (CombVar(v,_), []) => Metis.Term.Var v
   15.43      | _ => error "hol_term_to_fol_FO";
   15.44  
   15.45 -fun hol_term_to_fol_HO (SHC.CombVar (a, _)) = Metis.Term.Var a
   15.46 -  | hol_term_to_fol_HO (SHC.CombConst (a, _, tylist)) =
   15.47 +fun hol_term_to_fol_HO (CombVar (a, _)) = Metis.Term.Var a
   15.48 +  | hol_term_to_fol_HO (CombConst (a, _, tylist)) =
   15.49        Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
   15.50 -  | hol_term_to_fol_HO (SHC.CombApp (tm1, tm2)) =
   15.51 +  | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
   15.52         Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
   15.53  
   15.54  (*The fully-typed translation, to avoid type errors*)
   15.55  fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
   15.56  
   15.57 -fun hol_term_to_fol_FT (SHC.CombVar(a, ty)) =
   15.58 -      wrap_type (Metis.Term.Var a, ty)
   15.59 -  | hol_term_to_fol_FT (SHC.CombConst(a, ty, _)) =
   15.60 +fun hol_term_to_fol_FT (CombVar(a, ty)) = wrap_type (Metis.Term.Var a, ty)
   15.61 +  | hol_term_to_fol_FT (CombConst(a, ty, _)) =
   15.62        wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
   15.63 -  | hol_term_to_fol_FT (tm as SHC.CombApp(tm1,tm2)) =
   15.64 +  | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
   15.65         wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
   15.66 -                  SHC.type_of_combterm tm);
   15.67 +                  type_of_combterm tm);
   15.68  
   15.69 -fun hol_literal_to_fol FO (SHC.Literal (pol, tm)) =
   15.70 -      let val (SHC.CombConst(p,_,tys), tms) = SHC.strip_comb tm
   15.71 +fun hol_literal_to_fol FO (Literal (pol, tm)) =
   15.72 +      let val (CombConst(p,_,tys), tms) = strip_combterm_comb tm
   15.73            val tylits = if p = "equal" then [] else map hol_type_to_fol tys
   15.74            val lits = map hol_term_to_fol_FO tms
   15.75        in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
   15.76 -  | hol_literal_to_fol HO (SHC.Literal (pol, tm)) =
   15.77 -     (case SHC.strip_comb tm of
   15.78 -          (SHC.CombConst("equal",_,_), tms) =>
   15.79 +  | hol_literal_to_fol HO (Literal (pol, tm)) =
   15.80 +     (case strip_combterm_comb tm of
   15.81 +          (CombConst("equal",_,_), tms) =>
   15.82              metis_lit pol "=" (map hol_term_to_fol_HO tms)
   15.83          | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
   15.84 -  | hol_literal_to_fol FT (SHC.Literal (pol, tm)) =
   15.85 -     (case SHC.strip_comb tm of
   15.86 -          (SHC.CombConst("equal",_,_), tms) =>
   15.87 +  | hol_literal_to_fol FT (Literal (pol, tm)) =
   15.88 +     (case strip_combterm_comb tm of
   15.89 +          (CombConst("equal",_,_), tms) =>
   15.90              metis_lit pol "=" (map hol_term_to_fol_FT tms)
   15.91          | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
   15.92  
   15.93  fun literals_of_hol_thm thy mode t =
   15.94 -      let val (lits, types_sorts) = SHC.literals_of_term thy t
   15.95 +      let val (lits, types_sorts) = literals_of_term thy t
   15.96        in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
   15.97  
   15.98  (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
   15.99 -fun metis_of_typeLit pos (SFC.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
  15.100 -  | metis_of_typeLit pos (SFC.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
  15.101 +fun metis_of_typeLit pos (LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
  15.102 +  | metis_of_typeLit pos (LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
  15.103  
  15.104  fun default_sort _ (TVar _) = false
  15.105    | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
  15.106 @@ -136,10 +138,9 @@
  15.107               (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
  15.108    in
  15.109        if is_conjecture then
  15.110 -          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), SFC.add_typs types_sorts)
  15.111 +          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), add_typs types_sorts)
  15.112        else
  15.113 -        let val tylits = SFC.add_typs
  15.114 -                           (filter (not o default_sort ctxt) types_sorts)
  15.115 +        let val tylits = add_typs (filter (not o default_sort ctxt) types_sorts)
  15.116              val mtylits = if Config.get ctxt type_lits
  15.117                            then map (metis_of_typeLit false) tylits else []
  15.118          in
  15.119 @@ -149,13 +150,13 @@
  15.120  
  15.121  (* ARITY CLAUSE *)
  15.122  
  15.123 -fun m_arity_cls (SFC.TConsLit (c,t,args)) =
  15.124 -      metis_lit true (SFC.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
  15.125 -  | m_arity_cls (SFC.TVarLit (c,str))     =
  15.126 -      metis_lit false (SFC.make_type_class c) [Metis.Term.Var str];
  15.127 +fun m_arity_cls (TConsLit (c,t,args)) =
  15.128 +      metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
  15.129 +  | m_arity_cls (TVarLit (c,str))     =
  15.130 +      metis_lit false (make_type_class c) [Metis.Term.Var str];
  15.131  
  15.132  (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
  15.133 -fun arity_cls (SFC.ArityClause{conclLit,premLits,...}) =
  15.134 +fun arity_cls (ArityClause {conclLit, premLits, ...}) =
  15.135    (TrueI,
  15.136     Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
  15.137  
  15.138 @@ -164,7 +165,7 @@
  15.139  fun m_classrel_cls subclass superclass =
  15.140    [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
  15.141  
  15.142 -fun classrel_cls (SFC.ClassrelClause {subclass, superclass, ...}) =
  15.143 +fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
  15.144    (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
  15.145  
  15.146  (* ------------------------------------------------------------------------- *)
  15.147 @@ -213,14 +214,14 @@
  15.148    | strip_happ args x = (x, args);
  15.149  
  15.150  fun fol_type_to_isa _ (Metis.Term.Var v) =
  15.151 -     (case SPR.strip_prefix SFC.tvar_prefix v of
  15.152 -          SOME w => SPR.make_tvar w
  15.153 -        | NONE   => SPR.make_tvar v)
  15.154 +     (case strip_prefix tvar_prefix v of
  15.155 +          SOME w => make_tvar w
  15.156 +        | NONE   => make_tvar v)
  15.157    | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
  15.158 -     (case SPR.strip_prefix SFC.tconst_prefix x of
  15.159 -          SOME tc => Term.Type (SPR.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
  15.160 +     (case strip_prefix tconst_prefix x of
  15.161 +          SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
  15.162          | NONE    =>
  15.163 -      case SPR.strip_prefix SFC.tfree_prefix x of
  15.164 +      case strip_prefix tfree_prefix x of
  15.165            SOME tf => mk_tfree ctxt tf
  15.166          | NONE    => error ("fol_type_to_isa: " ^ x));
  15.167  
  15.168 @@ -229,10 +230,10 @@
  15.169    let val thy = ProofContext.theory_of ctxt
  15.170        val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
  15.171        fun tm_to_tt (Metis.Term.Var v) =
  15.172 -             (case SPR.strip_prefix SFC.tvar_prefix v of
  15.173 -                  SOME w => Type (SPR.make_tvar w)
  15.174 +             (case strip_prefix tvar_prefix v of
  15.175 +                  SOME w => Type (make_tvar w)
  15.176                  | NONE =>
  15.177 -              case SPR.strip_prefix SFC.schematic_var_prefix v of
  15.178 +              case strip_prefix schematic_var_prefix v of
  15.179                    SOME w => Term (mk_var (w, HOLogic.typeT))
  15.180                  | NONE   => Term (mk_var (v, HOLogic.typeT)) )
  15.181                      (*Var from Metis with a name like _nnn; possibly a type variable*)
  15.182 @@ -247,16 +248,16 @@
  15.183              end
  15.184          | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
  15.185        and applic_to_tt ("=",ts) =
  15.186 -            Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
  15.187 +            Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
  15.188          | applic_to_tt (a,ts) =
  15.189 -            case SPR.strip_prefix SFC.const_prefix a of
  15.190 +            case strip_prefix const_prefix a of
  15.191                  SOME b =>
  15.192 -                  let val c = SPR.invert_const b
  15.193 -                      val ntypes = SPR.num_typargs thy c
  15.194 +                  let val c = invert_const b
  15.195 +                      val ntypes = num_typargs thy c
  15.196                        val nterms = length ts - ntypes
  15.197                        val tts = map tm_to_tt ts
  15.198                        val tys = types_of (List.take(tts,ntypes))
  15.199 -                      val ntyargs = SPR.num_typargs thy c
  15.200 +                      val ntyargs = num_typargs thy c
  15.201                    in if length tys = ntyargs then
  15.202                           apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
  15.203                       else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
  15.204 @@ -267,14 +268,14 @@
  15.205                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
  15.206                       end
  15.207                | NONE => (*Not a constant. Is it a type constructor?*)
  15.208 -            case SPR.strip_prefix SFC.tconst_prefix a of
  15.209 +            case strip_prefix tconst_prefix a of
  15.210                  SOME b =>
  15.211 -                  Type (Term.Type (SPR.invert_type_const b, types_of (map tm_to_tt ts)))
  15.212 +                  Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
  15.213                | NONE => (*Maybe a TFree. Should then check that ts=[].*)
  15.214 -            case SPR.strip_prefix SFC.tfree_prefix a of
  15.215 +            case strip_prefix tfree_prefix a of
  15.216                  SOME b => Type (mk_tfree ctxt b)
  15.217                | NONE => (*a fixed variable? They are Skolem functions.*)
  15.218 -            case SPR.strip_prefix SFC.fixed_var_prefix a of
  15.219 +            case strip_prefix fixed_var_prefix a of
  15.220                  SOME b =>
  15.221                    let val opr = Term.Free(b, HOLogic.typeT)
  15.222                    in  apply_list opr (length ts) (map tm_to_tt ts)  end
  15.223 @@ -285,16 +286,16 @@
  15.224  fun fol_term_to_hol_FT ctxt fol_tm =
  15.225    let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
  15.226        fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
  15.227 -             (case SPR.strip_prefix SFC.schematic_var_prefix v of
  15.228 +             (case strip_prefix schematic_var_prefix v of
  15.229                    SOME w =>  mk_var(w, dummyT)
  15.230                  | NONE   => mk_var(v, dummyT))
  15.231          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
  15.232              Const ("op =", HOLogic.typeT)
  15.233          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
  15.234 -           (case SPR.strip_prefix SFC.const_prefix x of
  15.235 -                SOME c => Const (SPR.invert_const c, dummyT)
  15.236 +           (case strip_prefix const_prefix x of
  15.237 +                SOME c => Const (invert_const c, dummyT)
  15.238                | NONE => (*Not a constant. Is it a fixed variable??*)
  15.239 -            case SPR.strip_prefix SFC.fixed_var_prefix x of
  15.240 +            case strip_prefix fixed_var_prefix x of
  15.241                  SOME v => Free (v, fol_type_to_isa ctxt ty)
  15.242                | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
  15.243          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
  15.244 @@ -303,12 +304,12 @@
  15.245              cvt tm1 $ cvt tm2
  15.246          | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
  15.247          | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
  15.248 -            list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
  15.249 +            list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
  15.250          | cvt (t as Metis.Term.Fn (x, [])) =
  15.251 -           (case SPR.strip_prefix SFC.const_prefix x of
  15.252 -                SOME c => Const (SPR.invert_const c, dummyT)
  15.253 +           (case strip_prefix const_prefix x of
  15.254 +                SOME c => Const (invert_const c, dummyT)
  15.255                | NONE => (*Not a constant. Is it a fixed variable??*)
  15.256 -            case SPR.strip_prefix SFC.fixed_var_prefix x of
  15.257 +            case strip_prefix fixed_var_prefix x of
  15.258                  SOME v => Free (v, dummyT)
  15.259                | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
  15.260                    fol_term_to_hol_RAW ctxt t))
  15.261 @@ -331,7 +332,7 @@
  15.262                    ts'
  15.263    in  ts'  end;
  15.264  
  15.265 -fun mk_not (Const ("Not", _) $ b) = b
  15.266 +fun mk_not (Const (@{const_name Not}, _) $ b) = b
  15.267    | mk_not b = HOLogic.mk_not b;
  15.268  
  15.269  val metis_eq = Metis.Term.Fn ("=", []);
  15.270 @@ -387,9 +388,9 @@
  15.271                                         " in " ^ Display.string_of_thm ctxt i_th);
  15.272                   NONE)
  15.273        fun remove_typeinst (a, t) =
  15.274 -            case SPR.strip_prefix SFC.schematic_var_prefix a of
  15.275 +            case strip_prefix schematic_var_prefix a of
  15.276                  SOME b => SOME (b, t)
  15.277 -              | NONE   => case SPR.strip_prefix SFC.tvar_prefix a of
  15.278 +              | NONE   => case strip_prefix tvar_prefix a of
  15.279                  SOME _ => NONE          (*type instantiations are forbidden!*)
  15.280                | NONE   => SOME (a,t)    (*internal Metis var?*)
  15.281        val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
  15.282 @@ -455,8 +456,8 @@
  15.283        val c_t = cterm_incr_types thy refl_idx i_t
  15.284    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
  15.285  
  15.286 -fun get_ty_arg_size _ (Const ("op =", _)) = 0  (*equality has no type arguments*)
  15.287 -  | get_ty_arg_size thy (Const (c, _)) = (SPR.num_typargs thy c handle TYPE _ => 0)
  15.288 +fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0  (*equality has no type arguments*)
  15.289 +  | get_ty_arg_size thy (Const (c, _)) = (num_typargs thy c handle TYPE _ => 0)
  15.290    | get_ty_arg_size _ _ = 0;
  15.291  
  15.292  (* INFERENCE RULE: EQUALITY *)
  15.293 @@ -469,7 +470,7 @@
  15.294          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
  15.295        fun path_finder_FO tm [] = (tm, Term.Bound 0)
  15.296          | path_finder_FO tm (p::ps) =
  15.297 -            let val (tm1,args) = Term.strip_comb tm
  15.298 +            let val (tm1,args) = strip_comb tm
  15.299                  val adjustment = get_ty_arg_size thy tm1
  15.300                  val p' = if adjustment > p then p else p-adjustment
  15.301                  val tm_p = List.nth(args,p')
  15.302 @@ -496,13 +497,13 @@
  15.303                                          " isa-term: " ^  Syntax.string_of_term ctxt tm ^
  15.304                                          " fol-term: " ^ Metis.Term.toString t)
  15.305        fun path_finder FO tm ps _ = path_finder_FO tm ps
  15.306 -        | path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ =
  15.307 +        | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
  15.308               (*equality: not curried, as other predicates are*)
  15.309               if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
  15.310               else path_finder_HO tm (p::ps)        (*1 selects second operand*)
  15.311          | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
  15.312               path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
  15.313 -        | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps)
  15.314 +        | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
  15.315                              (Metis.Term.Fn ("=", [t1,t2])) =
  15.316               (*equality: not curried, as other predicates are*)
  15.317               if p=0 then path_finder_FT tm (0::1::ps)
  15.318 @@ -514,7 +515,7 @@
  15.319          | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
  15.320               (*if not equality, ignore head to skip the hBOOL predicate*)
  15.321          | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
  15.322 -      fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
  15.323 +      fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
  15.324              let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
  15.325              in (tm, nt $ tm_rslt) end
  15.326          | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
  15.327 @@ -542,7 +543,7 @@
  15.328    | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
  15.329        equality_inf ctxt mode f_lit f_p f_r;
  15.330  
  15.331 -fun real_literal (_, (c, _)) = not (String.isPrefix SFC.class_prefix c);
  15.332 +fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
  15.333  
  15.334  fun translate _ _ thpairs [] = thpairs
  15.335    | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
  15.336 @@ -568,23 +569,14 @@
  15.337  (* Translation of HO Clauses                                                 *)
  15.338  (* ------------------------------------------------------------------------- *)
  15.339  
  15.340 -fun cnf_th thy th = hd (Sledgehammer_Fact_Preprocessor.cnf_axiom thy th);
  15.341 -
  15.342 -val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
  15.343 -val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
  15.344 -
  15.345 -val comb_I = cnf_th @{theory} SHC.comb_I;
  15.346 -val comb_K = cnf_th @{theory} SHC.comb_K;
  15.347 -val comb_B = cnf_th @{theory} SHC.comb_B;
  15.348 -val comb_C = cnf_th @{theory} SHC.comb_C;
  15.349 -val comb_S = cnf_th @{theory} SHC.comb_S;
  15.350 +fun cnf_th thy th = hd (cnf_axiom thy th);
  15.351  
  15.352  fun type_ext thy tms =
  15.353 -  let val subs = Sledgehammer_Fact_Filter.tfree_classes_of_terms tms
  15.354 -      val supers = Sledgehammer_Fact_Filter.tvar_classes_of_terms tms
  15.355 -      and tycons = Sledgehammer_Fact_Filter.type_consts_of_terms thy tms
  15.356 -      val (supers', arity_clauses) = SFC.make_arity_clauses thy tycons supers
  15.357 -      val classrel_clauses = SFC.make_classrel_clauses thy subs supers'
  15.358 +  let val subs = tfree_classes_of_terms tms
  15.359 +      val supers = tvar_classes_of_terms tms
  15.360 +      and tycons = type_consts_of_terms thy tms
  15.361 +      val (supers', arity_clauses) = make_arity_clauses thy tycons supers
  15.362 +      val classrel_clauses = make_classrel_clauses thy subs supers'
  15.363    in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
  15.364    end;
  15.365  
  15.366 @@ -593,8 +585,8 @@
  15.367  (* ------------------------------------------------------------------------- *)
  15.368  
  15.369  type logic_map =
  15.370 -  {axioms : (Metis.Thm.thm * thm) list,
  15.371 -   tfrees : SFC.type_literal list};
  15.372 +  {axioms: (Metis.Thm.thm * thm) list,
  15.373 +   tfrees: type_literal list};
  15.374  
  15.375  fun const_in_metis c (pred, tm_list) =
  15.376    let
  15.377 @@ -606,7 +598,7 @@
  15.378  (*Extract TFree constraints from context to include as conjecture clauses*)
  15.379  fun init_tfrees ctxt =
  15.380    let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
  15.381 -  in  SFC.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
  15.382 +  in  add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
  15.383  
  15.384  (*transform isabelle type / arity clause to metis clause *)
  15.385  fun add_type_thm [] lmap = lmap
  15.386 @@ -643,12 +635,12 @@
  15.387        val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
  15.388        fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
  15.389        (*Now check for the existence of certain combinators*)
  15.390 -      val thI  = if used "c_COMBI" then [comb_I] else []
  15.391 -      val thK  = if used "c_COMBK" then [comb_K] else []
  15.392 -      val thB   = if used "c_COMBB" then [comb_B] else []
  15.393 -      val thC   = if used "c_COMBC" then [comb_C] else []
  15.394 -      val thS   = if used "c_COMBS" then [comb_S] else []
  15.395 -      val thEQ  = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
  15.396 +      val thI  = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else []
  15.397 +      val thK  = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else []
  15.398 +      val thB   = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else []
  15.399 +      val thC   = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
  15.400 +      val thS   = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
  15.401 +      val thEQ  = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
  15.402        val lmap' = if mode=FO then lmap
  15.403                    else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
  15.404    in
  15.405 @@ -668,7 +660,7 @@
  15.406  fun FOL_SOLVE mode ctxt cls ths0 =
  15.407    let val thy = ProofContext.theory_of ctxt
  15.408        val th_cls_pairs =
  15.409 -        map (fn th => (Thm.get_name_hint th, Sledgehammer_Fact_Preprocessor.cnf_axiom thy th)) ths0
  15.410 +        map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
  15.411        val ths = maps #2 th_cls_pairs
  15.412        val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
  15.413        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
  15.414 @@ -677,7 +669,7 @@
  15.415        val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
  15.416        val _ = if null tfrees then ()
  15.417                else (trace_msg (fn () => "TFREE CLAUSES");
  15.418 -                    app (fn tf => trace_msg (fn _ => SFC.tptp_of_typeLit true tf)) tfrees)
  15.419 +                    app (fn tf => trace_msg (fn _ => tptp_of_typeLit true tf)) tfrees)
  15.420        val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
  15.421        val thms = map #1 axioms
  15.422        val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
  15.423 @@ -719,12 +711,12 @@
  15.424    let val _ = trace_msg (fn () =>
  15.425          "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
  15.426    in
  15.427 -    if exists_type Sledgehammer_Fact_Preprocessor.type_has_topsort (prop_of st0)
  15.428 +    if exists_type type_has_topsort (prop_of st0)
  15.429      then raise METIS "Metis: Proof state contains the universal sort {}"
  15.430      else
  15.431 -      (Meson.MESON Sledgehammer_Fact_Preprocessor.neg_clausify
  15.432 +      (Meson.MESON neg_clausify
  15.433          (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
  15.434 -          THEN Sledgehammer_Fact_Preprocessor.expand_defs_tac st0) st0
  15.435 +          THEN Meson_Tactic.expand_defs_tac st0) st0
  15.436    end
  15.437    handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
  15.438  
  15.439 @@ -737,11 +729,11 @@
  15.440  
  15.441  val setup =
  15.442    type_lits_setup #>
  15.443 -  method @{binding metis} HO "METIS for FOL & HOL problems" #>
  15.444 +  method @{binding metis} HO "METIS for FOL and HOL problems" #>
  15.445    method @{binding metisF} FO "METIS for FOL problems" #>
  15.446    method @{binding metisFT} FT "METIS with fully-typed translation" #>
  15.447    Method.setup @{binding finish_clausify}
  15.448 -    (Scan.succeed (K (SIMPLE_METHOD (Sledgehammer_Fact_Preprocessor.expand_defs_tac refl))))
  15.449 +    (Scan.succeed (K (SIMPLE_METHOD (Meson_Tactic.expand_defs_tac refl))))
  15.450      "cleanup after conversion to clauses";
  15.451  
  15.452  end;
    16.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Mar 22 08:30:13 2010 +0100
    16.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Mar 22 13:48:15 2010 +0100
    16.3 @@ -4,47 +4,45 @@
    16.4  
    16.5  signature SLEDGEHAMMER_FACT_FILTER =
    16.6  sig
    16.7 -  type classrelClause = Sledgehammer_FOL_Clause.classrelClause
    16.8 -  type arityClause = Sledgehammer_FOL_Clause.arityClause
    16.9 +  type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
   16.10 +  type arity_clause = Sledgehammer_FOL_Clause.arity_clause
   16.11    type axiom_name = Sledgehammer_HOL_Clause.axiom_name
   16.12 -  type clause = Sledgehammer_HOL_Clause.clause
   16.13 -  type clause_id = Sledgehammer_HOL_Clause.clause_id
   16.14 -  datatype mode = Auto | Fol | Hol
   16.15 +  type hol_clause = Sledgehammer_HOL_Clause.hol_clause
   16.16 +  type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
   16.17    val tvar_classes_of_terms : term list -> string list
   16.18    val tfree_classes_of_terms : term list -> string list
   16.19    val type_consts_of_terms : theory -> term list -> string list
   16.20 -  val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
   16.21 +  val get_relevant_facts : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
   16.22      (thm * (string * int)) list
   16.23    val prepare_clauses : bool -> thm list -> thm list ->
   16.24 -    (thm * (axiom_name * clause_id)) list ->
   16.25 -    (thm * (axiom_name * clause_id)) list -> theory ->
   16.26 +    (thm * (axiom_name * hol_clause_id)) list ->
   16.27 +    (thm * (axiom_name * hol_clause_id)) list -> theory ->
   16.28      axiom_name vector *
   16.29 -      (clause list * clause list * clause list *
   16.30 -      clause list * classrelClause list * arityClause list)
   16.31 +      (hol_clause list * hol_clause list * hol_clause list *
   16.32 +      hol_clause list * classrel_clause list * arity_clause list)
   16.33  end;
   16.34  
   16.35  structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
   16.36  struct
   16.37  
   16.38 -structure SFC = Sledgehammer_FOL_Clause
   16.39 -structure SFP = Sledgehammer_Fact_Preprocessor
   16.40 -structure SHC = Sledgehammer_HOL_Clause
   16.41 +open Sledgehammer_FOL_Clause
   16.42 +open Sledgehammer_Fact_Preprocessor
   16.43 +open Sledgehammer_HOL_Clause
   16.44  
   16.45 -type classrelClause = SFC.classrelClause
   16.46 -type arityClause = SFC.arityClause
   16.47 -type axiom_name = SHC.axiom_name
   16.48 -type clause = SHC.clause
   16.49 -type clause_id = SHC.clause_id
   16.50 +type axiom_name = axiom_name
   16.51 +type hol_clause = hol_clause
   16.52 +type hol_clause_id = hol_clause_id
   16.53  
   16.54  (********************************************************************)
   16.55  (* some settings for both background automatic ATP calling procedure*)
   16.56  (* and also explicit ATP invocation methods                         *)
   16.57  (********************************************************************)
   16.58  
   16.59 -(*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
   16.60 +(* Translation mode can be auto-detected, or forced to be first-order or
   16.61 +   higher-order *)
   16.62  datatype mode = Auto | Fol | Hol;
   16.63  
   16.64 -val linkup_logic_mode = Auto;
   16.65 +val translation_mode = Auto;
   16.66  
   16.67  (*** background linkup ***)
   16.68  val run_blacklist_filter = true;
   16.69 @@ -59,7 +57,7 @@
   16.70  (* Relevance Filtering                                         *)
   16.71  (***************************************************************)
   16.72  
   16.73 -fun strip_Trueprop (Const("Trueprop",_) $ t) = t
   16.74 +fun strip_Trueprop (@{const Trueprop} $ t) = t
   16.75    | strip_Trueprop t = t;
   16.76  
   16.77  (*A surprising number of theorems contain only a few significant constants.
   16.78 @@ -79,7 +77,10 @@
   16.79    being chosen, but for some reason filtering works better with them listed. The
   16.80    logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
   16.81    must be within comprehensions.*)
   16.82 -val standard_consts = ["Trueprop","==>","all","==","op |","Not","op ="];
   16.83 +val standard_consts =
   16.84 +  [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
   16.85 +   @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
   16.86 +   @{const_name "op ="}];
   16.87  
   16.88  
   16.89  (*** constants with types ***)
   16.90 @@ -233,7 +234,7 @@
   16.91              end
   16.92              handle ConstFree => false
   16.93      in    
   16.94 -        case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
   16.95 +        case tm of @{const Trueprop} $ (Const(@{const_name "op ="}, _) $ lhs $ rhs) => 
   16.96                     defs lhs rhs 
   16.97                   | _ => false
   16.98      end;
   16.99 @@ -252,10 +253,10 @@
  16.100        let val cls = sort compare_pairs newpairs
  16.101            val accepted = List.take (cls, max_new)
  16.102        in
  16.103 -        SFP.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
  16.104 +        trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
  16.105                         ", exceeds the limit of " ^ Int.toString (max_new)));
  16.106 -        SFP.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
  16.107 -        SFP.trace_msg (fn () => "Actually passed: " ^
  16.108 +        trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
  16.109 +        trace_msg (fn () => "Actually passed: " ^
  16.110            space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
  16.111  
  16.112          (map #1 accepted, map #1 (List.drop (cls, max_new)))
  16.113 @@ -270,7 +271,7 @@
  16.114                  val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
  16.115                  val newp = p + (1.0-p) / convergence
  16.116              in
  16.117 -              SFP.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
  16.118 +              trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
  16.119                 (map #1 newrels) @ 
  16.120                 (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
  16.121              end
  16.122 @@ -278,12 +279,12 @@
  16.123              let val weight = clause_weight ctab rel_consts consts_typs
  16.124              in
  16.125                if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
  16.126 -              then (SFP.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ 
  16.127 +              then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ 
  16.128                                              " passes: " ^ Real.toString weight));
  16.129                      relevant ((ax,weight)::newrels, rejects) axs)
  16.130                else relevant (newrels, ax::rejects) axs
  16.131              end
  16.132 -    in  SFP.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
  16.133 +    in  trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
  16.134          relevant ([],[]) 
  16.135      end;
  16.136          
  16.137 @@ -292,12 +293,12 @@
  16.138   then
  16.139    let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
  16.140        val goal_const_tab = get_goal_consts_typs thy goals
  16.141 -      val _ = SFP.trace_msg (fn () => ("Initial constants: " ^
  16.142 +      val _ = trace_msg (fn () => ("Initial constants: " ^
  16.143                                   space_implode ", " (Symtab.keys goal_const_tab)));
  16.144        val rels = relevant_clauses max_new thy const_tab (pass_mark) 
  16.145                     goal_const_tab  (map (pair_consts_typs_axiom theory_const thy) axioms)
  16.146    in
  16.147 -      SFP.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
  16.148 +      trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
  16.149        rels
  16.150    end
  16.151   else axioms;
  16.152 @@ -332,7 +333,7 @@
  16.153    | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
  16.154    | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
  16.155  
  16.156 -fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
  16.157 +fun hash_literal (@{const Not} $ P) = Word.notb(hashw_term(P,0w0))
  16.158    | hash_literal P = hashw_term(P,0w0);
  16.159  
  16.160  fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t))));
  16.161 @@ -351,7 +352,7 @@
  16.162  fun make_unique xs =
  16.163    let val ht = mk_clause_table 7000
  16.164    in
  16.165 -      SFP.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
  16.166 +      trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
  16.167        app (ignore o Polyhash.peekInsert ht) xs;
  16.168        Polyhash.listItems ht
  16.169    end;
  16.170 @@ -383,7 +384,7 @@
  16.171  
  16.172            val name1 = Facts.extern facts name;
  16.173            val name2 = Name_Space.extern full_space name;
  16.174 -          val ths = filter_out SFP.bad_for_atp ths0;
  16.175 +          val ths = filter_out bad_for_atp ths0;
  16.176          in
  16.177            if Facts.is_concealed facts name orelse null ths orelse
  16.178              run_blacklist_filter andalso is_package_def name then I
  16.179 @@ -403,7 +404,7 @@
  16.180  
  16.181  (*Ignore blacklisted basenames*)
  16.182  fun add_multi_names (a, ths) pairs =
  16.183 -  if (Long_Name.base_name a) mem_string SFP.multi_base_blacklist then pairs
  16.184 +  if (Long_Name.base_name a) mem_string multi_base_blacklist then pairs
  16.185    else add_single_names (a, ths) pairs;
  16.186  
  16.187  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
  16.188 @@ -412,12 +413,17 @@
  16.189  fun name_thm_pairs ctxt =
  16.190    let
  16.191      val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
  16.192 -    val blacklist =
  16.193 -      if run_blacklist_filter then No_ATPs.get ctxt |> map Thm.prop_of else []
  16.194 -    fun is_blacklisted (_, th) = member (op =) blacklist (Thm.prop_of th)
  16.195 +    val ps = [] |> fold add_multi_names mults
  16.196 +                |> fold add_single_names singles
  16.197    in
  16.198 -    filter_out is_blacklisted
  16.199 -      (fold add_single_names singles (fold add_multi_names mults []))
  16.200 +    if run_blacklist_filter then
  16.201 +      let
  16.202 +        val blacklist = No_ATPs.get ctxt
  16.203 +                        |> map (`Thm.full_prop_of) |> Termtab.make
  16.204 +        val is_blacklisted = Termtab.defined blacklist o Thm.full_prop_of o snd
  16.205 +      in ps |> filter_out is_blacklisted end
  16.206 +    else
  16.207 +      ps
  16.208    end;
  16.209  
  16.210  fun check_named ("", th) =
  16.211 @@ -426,7 +432,7 @@
  16.212  
  16.213  fun get_all_lemmas ctxt =
  16.214    let val included_thms =
  16.215 -        tap (fn ths => SFP.trace_msg
  16.216 +        tap (fn ths => trace_msg
  16.217                       (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
  16.218              (name_thm_pairs ctxt)
  16.219    in
  16.220 @@ -440,7 +446,7 @@
  16.221  fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts);
  16.222  
  16.223  (*Remove this trivial type class*)
  16.224 -fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
  16.225 +fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
  16.226  
  16.227  fun tvar_classes_of_terms ts =
  16.228    let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
  16.229 @@ -499,14 +505,10 @@
  16.230  fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
  16.231    | too_general_eqterms _ = false;
  16.232  
  16.233 -fun too_general_equality (Const ("op =", _) $ x $ y) =
  16.234 +fun too_general_equality (Const (@{const_name "op ="}, _) $ x $ y) =
  16.235        too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
  16.236    | too_general_equality _ = false;
  16.237  
  16.238 -(* tautologous? *)
  16.239 -fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
  16.240 -  | is_taut _ = false;
  16.241 -
  16.242  fun has_typed_var tycons = exists_subterm
  16.243    (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
  16.244  
  16.245 @@ -514,28 +516,29 @@
  16.246    they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
  16.247    The resulting clause will have no type constraint, yielding false proofs. Even "bool"
  16.248    leads to many unsound proofs, though (obviously) only for higher-order problems.*)
  16.249 -val unwanted_types = ["Product_Type.unit","bool"];
  16.250 +val unwanted_types = [@{type_name unit}, @{type_name bool}];
  16.251  
  16.252  fun unwanted t =
  16.253 -  is_taut t orelse has_typed_var unwanted_types t orelse
  16.254 +  t = @{prop True} orelse has_typed_var unwanted_types t orelse
  16.255    forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
  16.256  
  16.257  (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
  16.258    likely to lead to unsound proofs.*)
  16.259  fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
  16.260  
  16.261 -fun isFO thy goal_cls = case linkup_logic_mode of
  16.262 -      Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
  16.263 -    | Fol => true
  16.264 -    | Hol => false
  16.265 +fun is_first_order thy goal_cls =
  16.266 +  case translation_mode of
  16.267 +    Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
  16.268 +  | Fol => true
  16.269 +  | Hol => false
  16.270  
  16.271 -fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
  16.272 +fun get_relevant_facts max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
  16.273    let
  16.274      val thy = ProofContext.theory_of ctxt
  16.275 -    val isFO = isFO thy goal_cls
  16.276 +    val is_FO = is_first_order thy goal_cls
  16.277      val included_cls = get_all_lemmas ctxt
  16.278 -      |> SFP.cnf_rules_pairs thy |> make_unique
  16.279 -      |> restrict_to_logic thy isFO
  16.280 +      |> cnf_rules_pairs thy |> make_unique
  16.281 +      |> restrict_to_logic thy is_FO
  16.282        |> remove_unwanted_clauses
  16.283    in
  16.284      relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) 
  16.285 @@ -547,28 +550,27 @@
  16.286    let
  16.287      (* add chain thms *)
  16.288      val chain_cls =
  16.289 -      SFP.cnf_rules_pairs thy (filter check_named (map SFP.pairname chain_ths))
  16.290 +      cnf_rules_pairs thy (filter check_named (map pairname chain_ths))
  16.291      val axcls = chain_cls @ axcls
  16.292      val extra_cls = chain_cls @ extra_cls
  16.293 -    val isFO = isFO thy goal_cls
  16.294 +    val is_FO = is_first_order thy goal_cls
  16.295      val ccls = subtract_cls goal_cls extra_cls
  16.296 -    val _ = app (fn th => SFP.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
  16.297 +    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
  16.298      val ccltms = map prop_of ccls
  16.299      and axtms = map (prop_of o #1) extra_cls
  16.300      val subs = tfree_classes_of_terms ccltms
  16.301      and supers = tvar_classes_of_terms axtms
  16.302 -    and tycons = type_consts_of_terms thy (ccltms@axtms)
  16.303 +    and tycons = type_consts_of_terms thy (ccltms @ axtms)
  16.304      (*TFrees in conjecture clauses; TVars in axiom clauses*)
  16.305 -    val conjectures = SHC.make_conjecture_clauses dfg thy ccls
  16.306 -    val (_, extra_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy extra_cls)
  16.307 -    val (clnames,axiom_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy axcls)
  16.308 -    val helper_clauses = SHC.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
  16.309 -    val (supers',arity_clauses) = SFC.make_arity_clauses_dfg dfg thy tycons supers
  16.310 -    val classrel_clauses = SFC.make_classrel_clauses thy subs supers'
  16.311 +    val conjectures = make_conjecture_clauses dfg thy ccls
  16.312 +    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls)
  16.313 +    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls)
  16.314 +    val helper_clauses = get_helper_clauses dfg thy is_FO (conjectures, extra_cls, [])
  16.315 +    val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers
  16.316 +    val classrel_clauses = make_classrel_clauses thy subs supers'
  16.317    in
  16.318      (Vector.fromList clnames,
  16.319        (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
  16.320    end
  16.321  
  16.322  end;
  16.323 -
    17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Mar 22 08:30:13 2010 +0100
    17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Mar 22 13:48:15 2010 +0100
    17.3 @@ -8,6 +8,7 @@
    17.4  sig
    17.5    val trace: bool Unsynchronized.ref
    17.6    val trace_msg: (unit -> string) -> unit
    17.7 +  val skolem_prefix: string
    17.8    val cnf_axiom: theory -> thm -> thm list
    17.9    val pairname: thm -> string * thm
   17.10    val multi_base_blacklist: string list
   17.11 @@ -15,7 +16,6 @@
   17.12    val type_has_topsort: typ -> bool
   17.13    val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
   17.14    val neg_clausify: thm list -> thm list
   17.15 -  val expand_defs_tac: thm -> tactic
   17.16    val combinators: thm -> thm
   17.17    val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
   17.18    val suppress_endtheory: bool Unsynchronized.ref
   17.19 @@ -26,8 +26,12 @@
   17.20  structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR =
   17.21  struct
   17.22  
   17.23 +open Sledgehammer_FOL_Clause
   17.24 +
   17.25  val trace = Unsynchronized.ref false;
   17.26 -fun trace_msg msg = if ! trace then tracing (msg ()) else ();
   17.27 +fun trace_msg msg = if !trace then tracing (msg ()) else ();
   17.28 +
   17.29 +val skolem_prefix = "sko_"
   17.30  
   17.31  fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
   17.32  
   17.33 @@ -75,7 +79,7 @@
   17.34      fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
   17.35            (*Existential: declare a Skolem function, then insert into body and continue*)
   17.36            let
   17.37 -            val cname = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
   17.38 +            val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
   17.39              val args0 = OldTerm.term_frees xtp  (*get the formal parameter list*)
   17.40              val Ts = map type_of args0
   17.41              val extraTs = rhs_extra_types (Ts ---> T) xtp
   17.42 @@ -110,7 +114,7 @@
   17.43                  val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
   17.44                  val Ts = map type_of args
   17.45                  val cT = Ts ---> T
   17.46 -                val id = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
   17.47 +                val id = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
   17.48                  val c = Free (id, cT)
   17.49                  val rhs = list_abs_free (map dest_Free args,
   17.50                                           HOLogic.choice_const T $ xtp)
   17.51 @@ -386,15 +390,14 @@
   17.52    | cnf_rules_pairs_aux thy pairs ((name,th)::ths) =
   17.53        let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs
   17.54                         handle THM _ => pairs |
   17.55 -                              Sledgehammer_FOL_Clause.CLAUSE _ => pairs
   17.56 +                              CLAUSE _ => pairs
   17.57        in  cnf_rules_pairs_aux thy pairs' ths  end;
   17.58  
   17.59  (*The combination of rev and tail recursion preserves the original order*)
   17.60  fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
   17.61  
   17.62  
   17.63 -(**** Convert all facts of the theory into clauses
   17.64 -      (Sledgehammer_FOL_Clause.clause, or Sledgehammer_HOL_Clause.clause) ****)
   17.65 +(**** Convert all facts of the theory into FOL or HOL clauses ****)
   17.66  
   17.67  local
   17.68  
   17.69 @@ -455,49 +458,13 @@
   17.70    lambda_free, but then the individual theory caches become much bigger.*)
   17.71  
   17.72  
   17.73 -(*** meson proof methods ***)
   17.74 -
   17.75 -(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
   17.76 -fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a
   17.77 -  | is_absko _ = false;
   17.78 -
   17.79 -fun is_okdef xs (Const ("==", _) $ t $ u) =   (*Definition of Free, not in certain terms*)
   17.80 -      is_Free t andalso not (member (op aconv) xs t)
   17.81 -  | is_okdef _ _ = false
   17.82 -
   17.83 -(*This function tries to cope with open locales, which introduce hypotheses of the form
   17.84 -  Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
   17.85 -  of sko_ functions. *)
   17.86 -fun expand_defs_tac st0 st =
   17.87 -  let val hyps0 = #hyps (rep_thm st0)
   17.88 -      val hyps = #hyps (crep_thm st)
   17.89 -      val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
   17.90 -      val defs = filter (is_absko o Thm.term_of) newhyps
   17.91 -      val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
   17.92 -                                      (map Thm.term_of hyps)
   17.93 -      val fixed = OldTerm.term_frees (concl_of st) @
   17.94 -                  fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
   17.95 -  in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
   17.96 -
   17.97 -
   17.98 -fun meson_general_tac ctxt ths i st0 =
   17.99 -  let
  17.100 -    val thy = ProofContext.theory_of ctxt
  17.101 -    val ctxt0 = Classical.put_claset HOL_cs ctxt
  17.102 -  in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
  17.103 -
  17.104 -val meson_method_setup =
  17.105 -  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
  17.106 -    SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
  17.107 -    "MESON resolution proof procedure";
  17.108 -
  17.109 -
  17.110  (*** Converting a subgoal into negated conjecture clauses. ***)
  17.111  
  17.112  fun neg_skolemize_tac ctxt =
  17.113    EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
  17.114  
  17.115 -val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
  17.116 +val neg_clausify =
  17.117 +  Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf;
  17.118  
  17.119  fun neg_conjecture_clauses ctxt st0 n =
  17.120    let
  17.121 @@ -534,11 +501,9 @@
  17.122    "conversion of theorem to clauses";
  17.123  
  17.124  
  17.125 -
  17.126  (** setup **)
  17.127  
  17.128  val setup =
  17.129 -  meson_method_setup #>
  17.130    neg_clausify_setup #>
  17.131    clausify_setup #>
  17.132    perhaps saturate_skolem_cache #>
    18.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Mar 22 08:30:13 2010 +0100
    18.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Mar 22 13:48:15 2010 +0100
    18.3 @@ -44,19 +44,19 @@
    18.4    datatype arLit =
    18.5        TConsLit of class * string * string list
    18.6      | TVarLit of class * string
    18.7 -  datatype arityClause = ArityClause of
    18.8 +  datatype arity_clause = ArityClause of
    18.9     {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list}
   18.10 -  datatype classrelClause = ClassrelClause of
   18.11 +  datatype classrel_clause = ClassrelClause of
   18.12     {axiom_name: axiom_name, subclass: class, superclass: class}
   18.13 -  val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
   18.14 -  val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arityClause list
   18.15 -  val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
   18.16 +  val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
   18.17 +  val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list
   18.18 +  val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
   18.19    val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table
   18.20 -  val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table
   18.21 +  val add_classrel_clause_preds : classrel_clause * int Symtab.table -> int Symtab.table
   18.22    val class_of_arityLit: arLit -> class
   18.23 -  val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table
   18.24 +  val add_arity_clause_preds: arity_clause * int Symtab.table -> int Symtab.table
   18.25    val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
   18.26 -  val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table
   18.27 +  val add_arity_clause_funcs: arity_clause * int Symtab.table -> int Symtab.table
   18.28    val init_functab: int Symtab.table
   18.29    val dfg_sign: bool -> string -> string
   18.30    val dfg_of_typeLit: bool -> type_literal -> string
   18.31 @@ -67,14 +67,14 @@
   18.32    val string_of_start: string -> string
   18.33    val string_of_descrip : string -> string
   18.34    val dfg_tfree_clause : string -> string
   18.35 -  val dfg_classrelClause: classrelClause -> string
   18.36 -  val dfg_arity_clause: arityClause -> string
   18.37 +  val dfg_classrel_clause: classrel_clause -> string
   18.38 +  val dfg_arity_clause: arity_clause -> string
   18.39    val tptp_sign: bool -> string -> string
   18.40    val tptp_of_typeLit : bool -> type_literal -> string
   18.41    val gen_tptp_cls : int * string * kind * string list * string list -> string
   18.42    val tptp_tfree_clause : string -> string
   18.43 -  val tptp_arity_clause : arityClause -> string
   18.44 -  val tptp_classrelClause : classrelClause -> string
   18.45 +  val tptp_arity_clause : arity_clause -> string
   18.46 +  val tptp_classrel_clause : classrel_clause -> string
   18.47  end
   18.48  
   18.49  structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
   18.50 @@ -96,28 +96,23 @@
   18.51  
   18.52  fun union_all xss = List.foldl (uncurry (union (op =))) [] xss;
   18.53  
   18.54 -(*Provide readable names for the more common symbolic functions*)
   18.55 +(* Provide readable names for the more common symbolic functions *)
   18.56  val const_trans_table =
   18.57 -      Symtab.make [(@{const_name "op ="}, "equal"),
   18.58 -                   (@{const_name Orderings.less_eq}, "lessequals"),
   18.59 -                   (@{const_name "op &"}, "and"),
   18.60 -                   (@{const_name "op |"}, "or"),
   18.61 -                   (@{const_name "op -->"}, "implies"),
   18.62 -                   (@{const_name "op :"}, "in"),
   18.63 -                   ("Sledgehammer.fequal", "fequal"),
   18.64 -                   ("Sledgehammer.COMBI", "COMBI"),
   18.65 -                   ("Sledgehammer.COMBK", "COMBK"),
   18.66 -                   ("Sledgehammer.COMBB", "COMBB"),
   18.67 -                   ("Sledgehammer.COMBC", "COMBC"),
   18.68 -                   ("Sledgehammer.COMBS", "COMBS"),
   18.69 -                   ("Sledgehammer.COMBB'", "COMBB_e"),
   18.70 -                   ("Sledgehammer.COMBC'", "COMBC_e"),
   18.71 -                   ("Sledgehammer.COMBS'", "COMBS_e")];
   18.72 +  Symtab.make [(@{const_name "op ="}, "equal"),
   18.73 +               (@{const_name Orderings.less_eq}, "lessequals"),
   18.74 +               (@{const_name "op &"}, "and"),
   18.75 +               (@{const_name "op |"}, "or"),
   18.76 +               (@{const_name "op -->"}, "implies"),
   18.77 +               (@{const_name "op :"}, "in"),
   18.78 +               (@{const_name fequal}, "fequal"),
   18.79 +               (@{const_name COMBI}, "COMBI"),
   18.80 +               (@{const_name COMBK}, "COMBK"),
   18.81 +               (@{const_name COMBB}, "COMBB"),
   18.82 +               (@{const_name COMBC}, "COMBC"),
   18.83 +               (@{const_name COMBS}, "COMBS")];
   18.84  
   18.85  val type_const_trans_table =
   18.86 -      Symtab.make [("*", "prod"),
   18.87 -                   ("+", "sum"),
   18.88 -                   ("~=>", "map")];
   18.89 +  Symtab.make [("*", "prod"), ("+", "sum"), ("~=>", "map")];
   18.90  
   18.91  (*Escaping of special characters.
   18.92    Alphanumeric characters are left unchanged.
   18.93 @@ -290,7 +285,7 @@
   18.94  datatype arLit = TConsLit of class * string * string list
   18.95                 | TVarLit of class * string;
   18.96  
   18.97 -datatype arityClause =
   18.98 +datatype arity_clause =
   18.99           ArityClause of {axiom_name: axiom_name,
  18.100                           conclLit: arLit,
  18.101                           premLits: arLit list};
  18.102 @@ -316,7 +311,7 @@
  18.103  
  18.104  (**** Isabelle class relations ****)
  18.105  
  18.106 -datatype classrelClause =
  18.107 +datatype classrel_clause =
  18.108           ClassrelClause of {axiom_name: axiom_name,
  18.109                              subclass: class,
  18.110                              superclass: class};
  18.111 @@ -330,13 +325,13 @@
  18.112            fun add_supers (sub,pairs) = List.foldl (add_super sub) pairs supers
  18.113        in  List.foldl add_supers [] subs  end;
  18.114  
  18.115 -fun make_classrelClause (sub,super) =
  18.116 +fun make_classrel_clause (sub,super) =
  18.117    ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
  18.118                    subclass = make_type_class sub,
  18.119                    superclass = make_type_class super};
  18.120  
  18.121  fun make_classrel_clauses thy subs supers =
  18.122 -  map make_classrelClause (class_pairs thy subs supers);
  18.123 +  map make_classrel_clause (class_pairs thy subs supers);
  18.124  
  18.125  
  18.126  (** Isabelle arities **)
  18.127 @@ -391,13 +386,13 @@
  18.128  fun add_type_sort_preds (T, preds) =
  18.129        update_many (preds, map pred_of_sort (sorts_on_typs T));
  18.130  
  18.131 -fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
  18.132 +fun add_classrel_clause_preds (ClassrelClause {subclass,superclass,...}, preds) =
  18.133    Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
  18.134  
  18.135  fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass
  18.136    | class_of_arityLit (TVarLit (tclass, _)) = tclass;
  18.137  
  18.138 -fun add_arityClause_preds (ArityClause {conclLit,premLits,...}, preds) =
  18.139 +fun add_arity_clause_preds (ArityClause {conclLit,premLits,...}, preds) =
  18.140    let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits)
  18.141        fun upd (class,preds) = Symtab.update (class,1) preds
  18.142    in  List.foldl upd preds classes  end;
  18.143 @@ -414,7 +409,7 @@
  18.144    | add_type_sort_funcs (TFree (a, _), funcs) =
  18.145        Symtab.update (make_fixed_type_var a, 0) funcs
  18.146  
  18.147 -fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) =
  18.148 +fun add_arity_clause_funcs (ArityClause {conclLit,...}, funcs) =
  18.149    let val TConsLit (_, tcons, tvars) = conclLit
  18.150    in  Symtab.update (tcons, length tvars) funcs  end;
  18.151  
  18.152 @@ -480,7 +475,7 @@
  18.153  
  18.154  fun dfg_classrelLits sub sup =  "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)";
  18.155  
  18.156 -fun dfg_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
  18.157 +fun dfg_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
  18.158    "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^
  18.159    axiom_name ^ ").\n\n";
  18.160  
  18.161 @@ -528,7 +523,7 @@
  18.162    let val tvar = "(T)"
  18.163    in  tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
  18.164  
  18.165 -fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
  18.166 +fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
  18.167    "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n"
  18.168  
  18.169  end;
    19.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Mar 22 08:30:13 2010 +0100
    19.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Mar 22 13:48:15 2010 +0100
    19.3 @@ -6,67 +6,54 @@
    19.4  
    19.5  signature SLEDGEHAMMER_HOL_CLAUSE =
    19.6  sig
    19.7 -  val ext: thm
    19.8 -  val comb_I: thm
    19.9 -  val comb_K: thm
   19.10 -  val comb_B: thm
   19.11 -  val comb_C: thm
   19.12 -  val comb_S: thm
   19.13 -  val minimize_applies: bool
   19.14 +  type kind = Sledgehammer_FOL_Clause.kind
   19.15 +  type fol_type = Sledgehammer_FOL_Clause.fol_type
   19.16 +  type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
   19.17 +  type arity_clause = Sledgehammer_FOL_Clause.arity_clause
   19.18    type axiom_name = string
   19.19    type polarity = bool
   19.20 -  type clause_id = int
   19.21 +  type hol_clause_id = int
   19.22 +
   19.23    datatype combterm =
   19.24 -      CombConst of string * Sledgehammer_FOL_Clause.fol_type * Sledgehammer_FOL_Clause.fol_type list (*Const and Free*)
   19.25 -    | CombVar of string * Sledgehammer_FOL_Clause.fol_type
   19.26 -    | CombApp of combterm * combterm
   19.27 +    CombConst of string * fol_type * fol_type list (* Const and Free *) |
   19.28 +    CombVar of string * fol_type |
   19.29 +    CombApp of combterm * combterm
   19.30    datatype literal = Literal of polarity * combterm
   19.31 -  datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
   19.32 -                    kind: Sledgehammer_FOL_Clause.kind,literals: literal list, ctypes_sorts: typ list}
   19.33 -  val type_of_combterm: combterm -> Sledgehammer_FOL_Clause.fol_type
   19.34 -  val strip_comb: combterm -> combterm * combterm list
   19.35 -  val literals_of_term: theory -> term -> literal list * typ list
   19.36 -  exception TOO_TRIVIAL
   19.37 -  val make_conjecture_clauses:  bool -> theory -> thm list -> clause list
   19.38 -  val make_axiom_clauses: bool ->
   19.39 -       theory ->
   19.40 -       (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list
   19.41 -  val get_helper_clauses: bool ->
   19.42 -       theory ->
   19.43 -       bool ->
   19.44 -       clause list * (thm * (axiom_name * clause_id)) list * string list ->
   19.45 -       clause list
   19.46 -  val tptp_write_file: bool -> Path.T ->
   19.47 -    clause list * clause list * clause list * clause list *
   19.48 -    Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
   19.49 +  datatype hol_clause =
   19.50 +    HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
   19.51 +                  kind: kind, literals: literal list, ctypes_sorts: typ list}
   19.52 +
   19.53 +  val type_of_combterm : combterm -> fol_type
   19.54 +  val strip_combterm_comb : combterm -> combterm * combterm list
   19.55 +  val literals_of_term : theory -> term -> literal list * typ list
   19.56 +  exception TRIVIAL
   19.57 +  val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
   19.58 +  val make_axiom_clauses : bool -> theory ->
   19.59 +       (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
   19.60 +  val get_helper_clauses : bool -> theory -> bool ->
   19.61 +       hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
   19.62 +       hol_clause list
   19.63 +  val write_tptp_file : bool -> Path.T ->
   19.64 +    hol_clause list * hol_clause list * hol_clause list * hol_clause list *
   19.65 +    classrel_clause list * arity_clause list ->
   19.66      int * int
   19.67 -  val dfg_write_file: bool -> Path.T ->
   19.68 -    clause list * clause list * clause list * clause list *
   19.69 -    Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
   19.70 -    int * int
   19.71 +  val write_dfg_file : bool -> Path.T ->
   19.72 +    hol_clause list * hol_clause list * hol_clause list * hol_clause list *
   19.73 +    classrel_clause list * arity_clause list -> int * int
   19.74  end
   19.75  
   19.76  structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
   19.77  struct
   19.78  
   19.79 -structure SFC = Sledgehammer_FOL_Clause;
   19.80 -
   19.81 -(* theorems for combinators and function extensionality *)
   19.82 -val ext = thm "HOL.ext";
   19.83 -val comb_I = thm "Sledgehammer.COMBI_def";
   19.84 -val comb_K = thm "Sledgehammer.COMBK_def";
   19.85 -val comb_B = thm "Sledgehammer.COMBB_def";
   19.86 -val comb_C = thm "Sledgehammer.COMBC_def";
   19.87 -val comb_S = thm "Sledgehammer.COMBS_def";
   19.88 -val fequal_imp_equal = thm "Sledgehammer.fequal_imp_equal";
   19.89 -val equal_imp_fequal = thm "Sledgehammer.equal_imp_fequal";
   19.90 -
   19.91 +open Sledgehammer_FOL_Clause
   19.92 +open Sledgehammer_Fact_Preprocessor
   19.93  
   19.94  (* Parameter t_full below indicates that full type information is to be
   19.95  exported *)
   19.96  
   19.97 -(*If true, each function will be directly applied to as many arguments as possible, avoiding
   19.98 -  use of the "apply" operator. Use of hBOOL is also minimized.*)
   19.99 +(* If true, each function will be directly applied to as many arguments as
  19.100 +   possible, avoiding use of the "apply" operator. Use of hBOOL is also
  19.101 +   minimized. *)
  19.102  val minimize_applies = true;
  19.103  
  19.104  fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
  19.105 @@ -84,21 +71,18 @@
  19.106  
  19.107  type axiom_name = string;
  19.108  type polarity = bool;
  19.109 -type clause_id = int;
  19.110 +type hol_clause_id = int;
  19.111  
  19.112 -datatype combterm = CombConst of string * SFC.fol_type * SFC.fol_type list (*Const and Free*)
  19.113 -                  | CombVar of string * SFC.fol_type
  19.114 -                  | CombApp of combterm * combterm
  19.115 +datatype combterm =
  19.116 +  CombConst of string * fol_type * fol_type list (* Const and Free *) |
  19.117 +  CombVar of string * fol_type |
  19.118 +  CombApp of combterm * combterm
  19.119  
  19.120  datatype literal = Literal of polarity * combterm;
  19.121  
  19.122 -datatype clause =
  19.123 -         Clause of {clause_id: clause_id,
  19.124 -                    axiom_name: axiom_name,
  19.125 -                    th: thm,
  19.126 -                    kind: SFC.kind,
  19.127 -                    literals: literal list,
  19.128 -                    ctypes_sorts: typ list};
  19.129 +datatype hol_clause =
  19.130 +  HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
  19.131 +                kind: kind, literals: literal list, ctypes_sorts: typ list};
  19.132  
  19.133  
  19.134  (*********************************************************************)
  19.135 @@ -106,8 +90,7 @@
  19.136  (*********************************************************************)
  19.137  
  19.138  fun isFalse (Literal(pol, CombConst(c,_,_))) =
  19.139 -      (pol andalso c = "c_False") orelse
  19.140 -      (not pol andalso c = "c_True")
  19.141 +      (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
  19.142    | isFalse _ = false;
  19.143  
  19.144  fun isTrue (Literal (pol, CombConst(c,_,_))) =
  19.145 @@ -115,24 +98,22 @@
  19.146        (not pol andalso c = "c_False")
  19.147    | isTrue _ = false;
  19.148  
  19.149 -fun isTaut (Clause {literals,...}) = exists isTrue literals;
  19.150 +fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
  19.151  
  19.152  fun type_of dfg (Type (a, Ts)) =
  19.153        let val (folTypes,ts) = types_of dfg Ts
  19.154 -      in  (SFC.Comp(SFC.make_fixed_type_const dfg a, folTypes), ts)  end
  19.155 -  | type_of _ (tp as TFree (a, _)) =
  19.156 -      (SFC.AtomF (SFC.make_fixed_type_var a), [tp])
  19.157 -  | type_of _ (tp as TVar (v, _)) =
  19.158 -      (SFC.AtomV (SFC.make_schematic_type_var v), [tp])
  19.159 +      in  (Comp(make_fixed_type_const dfg a, folTypes), ts)  end
  19.160 +  | type_of _ (tp as TFree (a, _)) = (AtomF (make_fixed_type_var a), [tp])
  19.161 +  | type_of _ (tp as TVar (v, _)) = (AtomV (make_schematic_type_var v), [tp])
  19.162  and types_of dfg Ts =
  19.163        let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
  19.164 -      in  (folTyps, SFC.union_all ts)  end;
  19.165 +      in  (folTyps, union_all ts)  end;
  19.166  
  19.167  (* same as above, but no gathering of sort information *)
  19.168  fun simp_type_of dfg (Type (a, Ts)) =
  19.169 -      SFC.Comp(SFC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
  19.170 -  | simp_type_of _ (TFree (a, _)) = SFC.AtomF(SFC.make_fixed_type_var a)
  19.171 -  | simp_type_of _ (TVar (v, _)) = SFC.AtomV(SFC.make_schematic_type_var v);
  19.172 +      Comp(make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
  19.173 +  | simp_type_of _ (TFree (a, _)) = AtomF (make_fixed_type_var a)
  19.174 +  | simp_type_of _ (TVar (v, _)) = AtomV (make_schematic_type_var v);
  19.175  
  19.176  
  19.177  fun const_type_of dfg thy (c,t) =
  19.178 @@ -142,27 +123,27 @@
  19.179  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
  19.180  fun combterm_of dfg thy (Const(c,t)) =
  19.181        let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
  19.182 -          val c' = CombConst(SFC.make_fixed_const dfg c, tp, tvar_list)
  19.183 +          val c' = CombConst(make_fixed_const dfg c, tp, tvar_list)
  19.184        in  (c',ts)  end
  19.185    | combterm_of dfg _ (Free(v,t)) =
  19.186        let val (tp,ts) = type_of dfg t
  19.187 -          val v' = CombConst(SFC.make_fixed_var v, tp, [])
  19.188 +          val v' = CombConst(make_fixed_var v, tp, [])
  19.189        in  (v',ts)  end
  19.190    | combterm_of dfg _ (Var(v,t)) =
  19.191        let val (tp,ts) = type_of dfg t
  19.192 -          val v' = CombVar(SFC.make_schematic_var v,tp)
  19.193 +          val v' = CombVar(make_schematic_var v,tp)
  19.194        in  (v',ts)  end
  19.195    | combterm_of dfg thy (P $ Q) =
  19.196        let val (P',tsP) = combterm_of dfg thy P
  19.197            val (Q',tsQ) = combterm_of dfg thy Q
  19.198        in  (CombApp(P',Q'), union (op =) tsP tsQ)  end
  19.199 -  | combterm_of _ _ (t as Abs _) = raise SFC.CLAUSE ("HOL CLAUSE", t);
  19.200 +  | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t);
  19.201  
  19.202 -fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
  19.203 +fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
  19.204    | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
  19.205  
  19.206 -fun literals_of_term1 dfg thy args (Const("Trueprop",_) $ P) = literals_of_term1 dfg thy args P
  19.207 -  | literals_of_term1 dfg thy args (Const("op |",_) $ P $ Q) =
  19.208 +fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P
  19.209 +  | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) =
  19.210        literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
  19.211    | literals_of_term1 dfg thy (lits,ts) P =
  19.212        let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
  19.213 @@ -173,23 +154,23 @@
  19.214  fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
  19.215  val literals_of_term = literals_of_term_dfg false;
  19.216  
  19.217 -(* Problem too trivial for resolution (empty clause) *)
  19.218 -exception TOO_TRIVIAL;
  19.219 +(* Trivial problem, which resolution cannot handle (empty clause) *)
  19.220 +exception TRIVIAL;
  19.221  
  19.222  (* making axiom and conjecture clauses *)
  19.223 -fun make_clause dfg thy (clause_id,axiom_name,kind,th) =
  19.224 +fun make_clause dfg thy (clause_id, axiom_name, kind, th) =
  19.225      let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
  19.226      in
  19.227 -        if forall isFalse lits
  19.228 -        then raise TOO_TRIVIAL
  19.229 +        if forall isFalse lits then
  19.230 +            raise TRIVIAL
  19.231          else
  19.232 -            Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
  19.233 -                    literals = lits, ctypes_sorts = ctypes_sorts}
  19.234 +            HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
  19.235 +                       kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}
  19.236      end;
  19.237  
  19.238  
  19.239  fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
  19.240 -  let val cls = make_clause dfg thy (id, name, SFC.Axiom, th)
  19.241 +  let val cls = make_clause dfg thy (id, name, Axiom, th)
  19.242    in
  19.243        if isTaut cls then pairs else (name,cls)::pairs
  19.244    end;
  19.245 @@ -198,7 +179,7 @@
  19.246  
  19.247  fun make_conjecture_clauses_aux _ _ _ [] = []
  19.248    | make_conjecture_clauses_aux dfg thy n (th::ths) =
  19.249 -      make_clause dfg thy (n,"conjecture", SFC.Conjecture, th) ::
  19.250 +      make_clause dfg thy (n,"conjecture", Conjecture, th) ::
  19.251        make_conjecture_clauses_aux dfg thy (n+1) ths;
  19.252  
  19.253  fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
  19.254 @@ -211,7 +192,7 @@
  19.255  (**********************************************************************)
  19.256  
  19.257  (*Result of a function type; no need to check that the argument type matches.*)
  19.258 -fun result_type (SFC.Comp ("tc_fun", [_, tp2])) = tp2
  19.259 +fun result_type (Comp ("tc_fun", [_, tp2])) = tp2
  19.260    | result_type _ = error "result_type"
  19.261  
  19.262  fun type_of_combterm (CombConst (_, tp, _)) = tp
  19.263 @@ -219,7 +200,7 @@
  19.264    | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
  19.265  
  19.266  (*gets the head of a combinator application, along with the list of arguments*)
  19.267 -fun strip_comb u =
  19.268 +fun strip_combterm_comb u =
  19.269      let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
  19.270          |   stripc  x =  x
  19.271      in  stripc(u,[])  end;
  19.272 @@ -231,10 +212,10 @@
  19.273  
  19.274  fun wrap_type t_full (s, tp) =
  19.275    if t_full then
  19.276 -      type_wrapper ^ SFC.paren_pack [s, SFC.string_of_fol_type tp]
  19.277 +      type_wrapper ^ paren_pack [s, string_of_fol_type tp]
  19.278    else s;
  19.279  
  19.280 -fun apply ss = "hAPP" ^ SFC.paren_pack ss;
  19.281 +fun apply ss = "hAPP" ^ paren_pack ss;
  19.282  
  19.283  fun rev_apply (v, []) = v
  19.284    | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
  19.285 @@ -251,10 +232,9 @@
  19.286                                           Int.toString nargs ^ " but is applied to " ^
  19.287                                           space_implode ", " args)
  19.288            val args2 = List.drop(args, nargs)
  19.289 -          val targs = if not t_full then map SFC.string_of_fol_type tvars
  19.290 -                      else []
  19.291 +          val targs = if not t_full then map string_of_fol_type tvars else []
  19.292        in
  19.293 -          string_apply (c ^ SFC.paren_pack (args1@targs), args2)
  19.294 +          string_apply (c ^ paren_pack (args1@targs), args2)
  19.295        end
  19.296    | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
  19.297    | string_of_applic _ _ _ = error "string_of_applic";
  19.298 @@ -263,7 +243,7 @@
  19.299    if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
  19.300  
  19.301  fun string_of_combterm (params as (t_full, cma, cnh)) t =
  19.302 -  let val (head, args) = strip_comb t
  19.303 +  let val (head, args) = strip_combterm_comb t
  19.304    in  wrap_type_if t_full cnh (head,
  19.305                      string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
  19.306                      type_of_combterm t)
  19.307 @@ -271,15 +251,15 @@
  19.308  
  19.309  (*Boolean-valued terms are here converted to literals.*)
  19.310  fun boolify params t =
  19.311 -  "hBOOL" ^ SFC.paren_pack [string_of_combterm params t];
  19.312 +  "hBOOL" ^ paren_pack [string_of_combterm params t];
  19.313  
  19.314  fun string_of_predicate (params as (_,_,cnh)) t =
  19.315    case t of
  19.316        (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
  19.317            (*DFG only: new TPTP prefers infix equality*)
  19.318 -          ("equal" ^ SFC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
  19.319 +          ("equal" ^ paren_pack [string_of_combterm params t1, string_of_combterm params t2])
  19.320      | _ =>
  19.321 -          case #1 (strip_comb t) of
  19.322 +          case #1 (strip_combterm_comb t) of
  19.323                CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
  19.324              | _ => boolify params t;
  19.325  
  19.326 @@ -290,31 +270,31 @@
  19.327    let val eqop = if pol then " = " else " != "
  19.328    in  string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2  end;
  19.329  
  19.330 -fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
  19.331 +fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal", _, _), t1), t2))) =
  19.332        tptp_of_equality params pol (t1,t2)
  19.333    | tptp_literal params (Literal(pol,pred)) =
  19.334 -      SFC.tptp_sign pol (string_of_predicate params pred);
  19.335 +      tptp_sign pol (string_of_predicate params pred);
  19.336  
  19.337  (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
  19.338    the latter should only occur in conjecture clauses.*)
  19.339 -fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
  19.340 +fun tptp_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
  19.341        (map (tptp_literal params) literals, 
  19.342 -       map (SFC.tptp_of_typeLit pos) (SFC.add_typs ctypes_sorts));
  19.343 +       map (tptp_of_typeLit pos) (add_typs ctypes_sorts));
  19.344  
  19.345 -fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) =
  19.346 -  let val (lits,tylits) = tptp_type_lits params (kind = SFC.Conjecture) cls
  19.347 +fun clause2tptp params (cls as HOLClause {axiom_name, clause_id, kind, ...}) =
  19.348 +  let val (lits,tylits) = tptp_type_lits params (kind = Conjecture) cls
  19.349    in
  19.350 -      (SFC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
  19.351 +      (gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits)
  19.352    end;
  19.353  
  19.354  
  19.355  (*** dfg format ***)
  19.356  
  19.357 -fun dfg_literal params (Literal(pol,pred)) = SFC.dfg_sign pol (string_of_predicate params pred);
  19.358 +fun dfg_literal params (Literal(pol,pred)) = dfg_sign pol (string_of_predicate params pred);
  19.359  
  19.360 -fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
  19.361 +fun dfg_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
  19.362        (map (dfg_literal params) literals, 
  19.363 -       map (SFC.dfg_of_typeLit pos) (SFC.add_typs ctypes_sorts));
  19.364 +       map (dfg_of_typeLit pos) (add_typs ctypes_sorts));
  19.365  
  19.366  fun get_uvars (CombConst _) vars = vars
  19.367    | get_uvars (CombVar(v,_)) vars = (v::vars)
  19.368 @@ -322,20 +302,21 @@
  19.369  
  19.370  fun get_uvars_l (Literal(_,c)) = get_uvars c [];
  19.371  
  19.372 -fun dfg_vars (Clause {literals,...}) = SFC.union_all (map get_uvars_l literals);
  19.373 +fun dfg_vars (HOLClause {literals,...}) = union_all (map get_uvars_l literals);
  19.374  
  19.375 -fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
  19.376 -  let val (lits,tylits) = dfg_type_lits params (kind = SFC.Conjecture) cls
  19.377 +fun clause2dfg params (cls as HOLClause {axiom_name, clause_id, kind,
  19.378 +                                         ctypes_sorts, ...}) =
  19.379 +  let val (lits,tylits) = dfg_type_lits params (kind = Conjecture) cls
  19.380        val vars = dfg_vars cls
  19.381 -      val tvars = SFC.get_tvar_strs ctypes_sorts
  19.382 +      val tvars = get_tvar_strs ctypes_sorts
  19.383    in
  19.384 -      (SFC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
  19.385 +      (gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
  19.386    end;
  19.387  
  19.388  
  19.389  (** For DFG format: accumulate function and predicate declarations **)
  19.390  
  19.391 -fun addtypes tvars tab = List.foldl SFC.add_foltype_funcs tab tvars;
  19.392 +fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
  19.393  
  19.394  fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
  19.395        if c = "equal" then (addtypes tvars funcs, preds)
  19.396 @@ -348,33 +329,33 @@
  19.397              else (addtypes tvars funcs, addit preds)
  19.398          end
  19.399    | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
  19.400 -      (SFC.add_foltype_funcs (ctp,funcs), preds)
  19.401 +      (add_foltype_funcs (ctp,funcs), preds)
  19.402    | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
  19.403  
  19.404 -fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls);
  19.405 +fun add_literal_decls params (Literal (_,c), decls) = add_decls params (c,decls);
  19.406  
  19.407 -fun add_clause_decls params (Clause {literals, ...}, decls) =
  19.408 +fun add_clause_decls params (HOLClause {literals, ...}, decls) =
  19.409      List.foldl (add_literal_decls params) decls literals
  19.410      handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
  19.411  
  19.412  fun decls_of_clauses params clauses arity_clauses =
  19.413 -  let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) SFC.init_functab)
  19.414 +  let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) init_functab)
  19.415        val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
  19.416        val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
  19.417    in
  19.418 -      (Symtab.dest (List.foldl SFC.add_arityClause_funcs functab arity_clauses),
  19.419 +      (Symtab.dest (List.foldl add_arity_clause_funcs functab arity_clauses),
  19.420         Symtab.dest predtab)
  19.421    end;
  19.422  
  19.423 -fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
  19.424 -  List.foldl SFC.add_type_sort_preds preds ctypes_sorts
  19.425 +fun add_clause_preds (HOLClause {ctypes_sorts, ...}, preds) =
  19.426 +  List.foldl add_type_sort_preds preds ctypes_sorts
  19.427    handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
  19.428  
  19.429  (*Higher-order clauses have only the predicates hBOOL and type classes.*)
  19.430  fun preds_of_clauses clauses clsrel_clauses arity_clauses =
  19.431      Symtab.dest
  19.432 -        (List.foldl SFC.add_classrelClause_preds
  19.433 -               (List.foldl SFC.add_arityClause_preds
  19.434 +        (List.foldl add_classrel_clause_preds
  19.435 +               (List.foldl add_arity_clause_preds
  19.436                        (List.foldl add_clause_preds Symtab.empty clauses)
  19.437                        arity_clauses)
  19.438                 clsrel_clauses)
  19.439 @@ -385,9 +366,8 @@
  19.440  (**********************************************************************)
  19.441  
  19.442  val init_counters =
  19.443 -    Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
  19.444 -                 ("c_COMBB", 0), ("c_COMBC", 0),
  19.445 -                 ("c_COMBS", 0)];
  19.446 +  Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
  19.447 +               ("c_COMBS", 0)];
  19.448  
  19.449  fun count_combterm (CombConst (c, _, _), ct) =
  19.450       (case Symtab.lookup ct c of NONE => ct  (*no counter*)
  19.451 @@ -397,18 +377,18 @@
  19.452  
  19.453  fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
  19.454  
  19.455 -fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals;
  19.456 +fun count_clause (HOLClause {literals, ...}, ct) =
  19.457 +  List.foldl count_literal ct literals;
  19.458  
  19.459 -fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
  19.460 +fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}, ct) =
  19.461    if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
  19.462    else ct;
  19.463  
  19.464 -fun cnf_helper_thms thy =
  19.465 -  Sledgehammer_Fact_Preprocessor.cnf_rules_pairs thy
  19.466 -  o map Sledgehammer_Fact_Preprocessor.pairname
  19.467 +fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname
  19.468  
  19.469  fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
  19.470 -  if isFO then []  (*first-order*)
  19.471 +  if isFO then
  19.472 +    []
  19.473    else
  19.474      let
  19.475          val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
  19.476 @@ -416,15 +396,15 @@
  19.477          val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
  19.478          fun needed c = the (Symtab.lookup ct c) > 0
  19.479          val IK = if needed "c_COMBI" orelse needed "c_COMBK"
  19.480 -                 then cnf_helper_thms thy [comb_I,comb_K]
  19.481 +                 then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
  19.482                   else []
  19.483          val BC = if needed "c_COMBB" orelse needed "c_COMBC"
  19.484 -                 then cnf_helper_thms thy [comb_B,comb_C]
  19.485 +                 then cnf_helper_thms thy [@{thm COMBB_def}, @{thm COMBC_def}]
  19.486                   else []
  19.487 -        val S = if needed "c_COMBS"
  19.488 -                then cnf_helper_thms thy [comb_S]
  19.489 +        val S = if needed "c_COMBS" then cnf_helper_thms thy [@{thm COMBS_def}]
  19.490                  else []
  19.491 -        val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
  19.492 +        val other = cnf_helper_thms thy [@{thm fequal_imp_equal},
  19.493 +                                         @{thm equal_imp_fequal}]
  19.494      in
  19.495          map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
  19.496      end;
  19.497 @@ -432,7 +412,7 @@
  19.498  (*Find the minimal arity of each function mentioned in the term. Also, note which uses
  19.499    are not at top level, to see if hBOOL is needed.*)
  19.500  fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
  19.501 -  let val (head, args) = strip_comb t
  19.502 +  let val (head, args) = strip_combterm_comb t
  19.503        val n = length args
  19.504        val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
  19.505    in
  19.506 @@ -451,11 +431,12 @@
  19.507  fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
  19.508    count_constants_term true t (const_min_arity, const_needs_hBOOL);
  19.509  
  19.510 -fun count_constants_clause (Clause{literals,...}) (const_min_arity, const_needs_hBOOL) =
  19.511 +fun count_constants_clause (HOLClause {literals, ...})
  19.512 +                           (const_min_arity, const_needs_hBOOL) =
  19.513    fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
  19.514  
  19.515  fun display_arity const_needs_hBOOL (c,n) =
  19.516 -  Sledgehammer_Fact_Preprocessor.trace_msg (fn () => "Constant: " ^ c ^
  19.517 +  trace_msg (fn () => "Constant: " ^ c ^
  19.518                  " arity:\t" ^ Int.toString n ^
  19.519                  (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
  19.520  
  19.521 @@ -469,31 +450,31 @@
  19.522       in (const_min_arity, const_needs_hBOOL) end
  19.523    else (Symtab.empty, Symtab.empty);
  19.524  
  19.525 -(* tptp format *)
  19.526 +(* TPTP format *)
  19.527  
  19.528 -fun tptp_write_file t_full file clauses =
  19.529 +fun write_tptp_file t_full file clauses =
  19.530    let
  19.531      val (conjectures, axclauses, _, helper_clauses,
  19.532        classrel_clauses, arity_clauses) = clauses
  19.533      val (cma, cnh) = count_constants clauses
  19.534      val params = (t_full, cma, cnh)
  19.535      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
  19.536 -    val tfree_clss = map SFC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
  19.537 +    val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
  19.538      val _ =
  19.539        File.write_list file (
  19.540          map (#1 o (clause2tptp params)) axclauses @
  19.541          tfree_clss @
  19.542          tptp_clss @
  19.543 -        map SFC.tptp_classrelClause classrel_clauses @
  19.544 -        map SFC.tptp_arity_clause arity_clauses @
  19.545 +        map tptp_classrel_clause classrel_clauses @
  19.546 +        map tptp_arity_clause arity_clauses @
  19.547          map (#1 o (clause2tptp params)) helper_clauses)
  19.548      in (length axclauses + 1, length tfree_clss + length tptp_clss)
  19.549    end;
  19.550  
  19.551  
  19.552 -(* dfg format *)
  19.553 +(* DFG format *)
  19.554  
  19.555 -fun dfg_write_file t_full file clauses =
  19.556 +fun write_dfg_file t_full file clauses =
  19.557    let
  19.558      val (conjectures, axclauses, _, helper_clauses,
  19.559        classrel_clauses, arity_clauses) = clauses
  19.560 @@ -502,20 +483,20 @@
  19.561      val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
  19.562      and probname = Path.implode (Path.base file)
  19.563      val axstrs = map (#1 o (clause2dfg params)) axclauses
  19.564 -    val tfree_clss = map SFC.dfg_tfree_clause (SFC.union_all tfree_litss)
  19.565 +    val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
  19.566      val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
  19.567      val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
  19.568      and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
  19.569      val _ =
  19.570        File.write_list file (
  19.571 -        SFC.string_of_start probname ::
  19.572 -        SFC.string_of_descrip probname ::
  19.573 -        SFC.string_of_symbols (SFC.string_of_funcs funcs)
  19.574 -          (SFC.string_of_preds (cl_preds @ ty_preds)) ::
  19.575 +        string_of_start probname ::
  19.576 +        string_of_descrip probname ::
  19.577 +        string_of_symbols (string_of_funcs funcs)
  19.578 +          (string_of_preds (cl_preds @ ty_preds)) ::
  19.579          "list_of_clauses(axioms,cnf).\n" ::
  19.580          axstrs @
  19.581 -        map SFC.dfg_classrelClause classrel_clauses @
  19.582 -        map SFC.dfg_arity_clause arity_clauses @
  19.583 +        map dfg_classrel_clause classrel_clauses @
  19.584 +        map dfg_arity_clause arity_clauses @
  19.585          helper_clauses_strs @
  19.586          ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
  19.587          tfree_clss @
  19.588 @@ -530,4 +511,3 @@
  19.589    end;
  19.590  
  19.591  end;
  19.592 -
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 22 13:48:15 2010 +0100
    20.3 @@ -0,0 +1,87 @@
    20.4 +(*  Title:      HOL/Sledgehammer/sledgehammer_isar.ML
    20.5 +    Author:     Jasmin Blanchette, TU Muenchen
    20.6 +
    20.7 +Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
    20.8 +*)
    20.9 +
   20.10 +structure Sledgehammer_Isar : sig end =
   20.11 +struct
   20.12 +
   20.13 +open ATP_Manager
   20.14 +open ATP_Minimal
   20.15 +
   20.16 +structure K = OuterKeyword and P = OuterParse
   20.17 +
   20.18 +val _ =
   20.19 +  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
   20.20 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
   20.21 +
   20.22 +val _ =
   20.23 +  OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
   20.24 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
   20.25 +
   20.26 +val _ =
   20.27 +  OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
   20.28 +    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
   20.29 +      (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
   20.30 +
   20.31 +val _ =
   20.32 +  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
   20.33 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
   20.34 +      Toplevel.keep (print_provers o Toplevel.theory_of)));
   20.35 +
   20.36 +val _ =
   20.37 +  OuterSyntax.command "sledgehammer"
   20.38 +    "search for first-order proof using automatic theorem provers" K.diag
   20.39 +    (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
   20.40 +      Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
   20.41 +
   20.42 +val default_minimize_prover = "remote_vampire"
   20.43 +val default_minimize_time_limit = 5
   20.44 +
   20.45 +fun atp_minimize_command args thm_names state =
   20.46 +  let
   20.47 +    fun theorems_from_names ctxt =
   20.48 +      map (fn (name, interval) =>
   20.49 +              let
   20.50 +                val thmref = Facts.Named ((name, Position.none), interval)
   20.51 +                val ths = ProofContext.get_fact ctxt thmref
   20.52 +                val name' = Facts.string_of_ref thmref
   20.53 +              in (name', ths) end)
   20.54 +    fun get_time_limit_arg time_string =
   20.55 +      (case Int.fromString time_string of
   20.56 +        SOME t => t
   20.57 +      | NONE => error ("Invalid time limit: " ^ quote time_string))
   20.58 +    fun get_opt (name, a) (p, t) =
   20.59 +      (case name of
   20.60 +        "time" => (p, get_time_limit_arg a)
   20.61 +      | "atp" => (a, t)
   20.62 +      | n => error ("Invalid argument: " ^ n))
   20.63 +    fun get_options args =
   20.64 +      fold get_opt args (default_minimize_prover, default_minimize_time_limit)
   20.65 +    val (prover_name, time_limit) = get_options args
   20.66 +    val prover =
   20.67 +      (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
   20.68 +        SOME prover => prover
   20.69 +      | NONE => error ("Unknown prover: " ^ quote prover_name))
   20.70 +    val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
   20.71 +  in
   20.72 +    writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
   20.73 +                                   state name_thms_pairs))
   20.74 +  end
   20.75 +
   20.76 +local structure K = OuterKeyword and P = OuterParse in
   20.77 +
   20.78 +val parse_args =
   20.79 +  Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
   20.80 +val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
   20.81 +
   20.82 +val _ =
   20.83 +  OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
   20.84 +    (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
   20.85 +      Toplevel.no_timing o Toplevel.unknown_proof o
   20.86 +        Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
   20.87 +
   20.88 +end
   20.89 +
   20.90 +end;
    21.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 22 08:30:13 2010 +0100
    21.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 22 13:48:15 2010 +0100
    21.3 @@ -7,33 +7,29 @@
    21.4  signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
    21.5  sig
    21.6    val chained_hint: string
    21.7 -
    21.8 -  val fix_sorts: sort Vartab.table -> term -> term
    21.9    val invert_const: string -> string
   21.10    val invert_type_const: string -> string
   21.11    val num_typargs: theory -> string -> int
   21.12    val make_tvar: string -> typ
   21.13    val strip_prefix: string -> string -> string option
   21.14    val setup: theory -> theory
   21.15 -  (* extracting lemma list*)
   21.16 -  val find_failure: string -> string option
   21.17 -  val lemma_list: bool -> string ->
   21.18 +  val is_proof_well_formed: string -> bool
   21.19 +  val metis_lemma_list: bool -> string ->
   21.20      string * string vector * (int * int) * Proof.context * thm * int -> string * string list
   21.21 -  (* structured proofs *)
   21.22 -  val structured_proof: string ->
   21.23 +  val structured_isar_proof: string ->
   21.24      string * string vector * (int * int) * Proof.context * thm * int -> string * string list
   21.25  end;
   21.26  
   21.27  structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
   21.28  struct
   21.29  
   21.30 -structure SFC = Sledgehammer_FOL_Clause
   21.31 -
   21.32 -val trace_path = Path.basic "atp_trace";
   21.33 +open Sledgehammer_FOL_Clause
   21.34 +open Sledgehammer_Fact_Preprocessor
   21.35  
   21.36 -fun trace s =
   21.37 -  if ! Sledgehammer_Fact_Preprocessor.trace then File.append (File.tmp_path trace_path) s
   21.38 -  else ();
   21.39 +val trace_proof_path = Path.basic "atp_trace";
   21.40 +
   21.41 +fun trace_proof_msg f =
   21.42 +  if !trace then File.append (File.tmp_path trace_proof_path) (f ()) else ();
   21.43  
   21.44  fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
   21.45  
   21.46 @@ -43,9 +39,6 @@
   21.47  (*Indicates whether to include sort information in generated proofs*)
   21.48  val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true;
   21.49  
   21.50 -(*Indicated whether to generate full proofs or just lemma lists - now via setup of atps*)
   21.51 -(* val (full_proofs, full_proofs_setup) = Attrib.config_bool "sledgehammer_full" false; *)
   21.52 -
   21.53  val setup = modulus_setup #> recon_sorts_setup;
   21.54  
   21.55  (**** PARSING OF TSTP FORMAT ****)
   21.56 @@ -109,12 +102,12 @@
   21.57  (*If string s has the prefix s1, return the result of deleting it.*)
   21.58  fun strip_prefix s1 s =
   21.59    if String.isPrefix s1 s
   21.60 -  then SOME (SFC.undo_ascii_of (String.extract (s, size s1, NONE)))
   21.61 +  then SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
   21.62    else NONE;
   21.63  
   21.64  (*Invert the table of translations between Isabelle and ATPs*)
   21.65  val type_const_trans_table_inv =
   21.66 -      Symtab.make (map swap (Symtab.dest SFC.type_const_trans_table));
   21.67 +      Symtab.make (map swap (Symtab.dest type_const_trans_table));
   21.68  
   21.69  fun invert_type_const c =
   21.70      case Symtab.lookup type_const_trans_table_inv c of
   21.71 @@ -132,15 +125,15 @@
   21.72      | Br (a,ts) =>
   21.73          let val Ts = map type_of_stree ts
   21.74          in
   21.75 -          case strip_prefix SFC.tconst_prefix a of
   21.76 +          case strip_prefix tconst_prefix a of
   21.77                SOME b => Type(invert_type_const b, Ts)
   21.78              | NONE =>
   21.79                  if not (null ts) then raise STREE t  (*only tconsts have type arguments*)
   21.80                  else
   21.81 -                case strip_prefix SFC.tfree_prefix a of
   21.82 +                case strip_prefix tfree_prefix a of
   21.83                      SOME b => TFree("'" ^ b, HOLogic.typeS)
   21.84                    | NONE =>
   21.85 -                case strip_prefix SFC.tvar_prefix a of
   21.86 +                case strip_prefix tvar_prefix a of
   21.87                      SOME b => make_tvar b
   21.88                    | NONE => make_tvar a   (*Variable from the ATP, say X1*)
   21.89          end;
   21.90 @@ -148,7 +141,7 @@
   21.91  (*Invert the table of translations between Isabelle and ATPs*)
   21.92  val const_trans_table_inv =
   21.93        Symtab.update ("fequal", "op =")
   21.94 -        (Symtab.make (map swap (Symtab.dest SFC.const_trans_table)));
   21.95 +        (Symtab.make (map swap (Symtab.dest const_trans_table)));
   21.96  
   21.97  fun invert_const c =
   21.98      case Symtab.lookup const_trans_table_inv c of
   21.99 @@ -169,9 +162,9 @@
  21.100      | Br ("hBOOL",[t]) => term_of_stree [] thy t  (*ignore hBOOL*)
  21.101      | Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t
  21.102      | Br (a,ts) =>
  21.103 -        case strip_prefix SFC.const_prefix a of
  21.104 +        case strip_prefix const_prefix a of
  21.105              SOME "equal" =>
  21.106 -              list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
  21.107 +              list_comb(Const (@{const_name "op ="}, HOLogic.typeT), List.map (term_of_stree [] thy) ts)
  21.108            | SOME b =>
  21.109                let val c = invert_const b
  21.110                    val nterms = length ts - num_typargs thy c
  21.111 @@ -183,10 +176,10 @@
  21.112            | NONE => (*a variable, not a constant*)
  21.113                let val T = HOLogic.typeT
  21.114                    val opr = (*a Free variable is typically a Skolem function*)
  21.115 -                    case strip_prefix SFC.fixed_var_prefix a of
  21.116 +                    case strip_prefix fixed_var_prefix a of
  21.117                          SOME b => Free(b,T)
  21.118                        | NONE =>
  21.119 -                    case strip_prefix SFC.schematic_var_prefix a of
  21.120 +                    case strip_prefix schematic_var_prefix a of
  21.121                          SOME b => make_var (b,T)
  21.122                        | NONE => make_var (a,T)    (*Variable from the ATP, say X1*)
  21.123                in  list_comb (opr, List.map (term_of_stree [] thy) (ts@args))  end;
  21.124 @@ -196,7 +189,7 @@
  21.125    | constraint_of_stree pol t = case t of
  21.126          Int _ => raise STREE t
  21.127        | Br (a,ts) =>
  21.128 -            (case (strip_prefix SFC.class_prefix a, map type_of_stree ts) of
  21.129 +            (case (strip_prefix class_prefix a, map type_of_stree ts) of
  21.130                   (SOME b, [T]) => (pol, b, T)
  21.131                 | _ => raise STREE t);
  21.132  
  21.133 @@ -286,7 +279,7 @@
  21.134      may disagree. We have to try all combinations of literals (quadratic!) and
  21.135      match up the variable names consistently. **)
  21.136  
  21.137 -fun strip_alls_aux n (Const("all",_)$Abs(a,T,t))  =
  21.138 +fun strip_alls_aux n (Const(@{const_name all}, _)$Abs(a,T,t))  =
  21.139        strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t))
  21.140    | strip_alls_aux _ t  =  t;
  21.141  
  21.142 @@ -340,26 +333,30 @@
  21.143              then SOME ctm else perm ctms
  21.144    in perm end;
  21.145  
  21.146 -fun have_or_show "show " _ = "show \""
  21.147 -  | have_or_show have lname = have ^ lname ^ ": \""
  21.148 -
  21.149  (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
  21.150    ATP may have their literals reordered.*)
  21.151 -fun isar_lines ctxt ctms =
  21.152 -  let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term)
  21.153 -      val _ = trace ("\n\nisar_lines: start\n")
  21.154 -      fun doline _ (lname, t, []) =  (*No deps: it's a conjecture clause, with no proof.*)
  21.155 -           (case permuted_clause t ctms of
  21.156 -                SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
  21.157 -              | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n")  (*no match!!*)
  21.158 -        | doline have (lname, t, deps) =
  21.159 -            have_or_show have lname ^ string_of (gen_all_vars (HOLogic.mk_Trueprop t)) ^
  21.160 -            "\"\n  by (metis " ^ space_implode " " deps ^ ")\n"
  21.161 -      fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
  21.162 -        | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
  21.163 -  in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) dolines end;
  21.164 +fun isar_proof_body ctxt ctms =
  21.165 +  let
  21.166 +    val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
  21.167 +    val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt)
  21.168 +    fun have_or_show "show" _ = "show \""
  21.169 +      | have_or_show have lname = have ^ " " ^ lname ^ ": \""
  21.170 +    fun do_line _ (lname, t, []) =
  21.171 +       (* No deps: it's a conjecture clause, with no proof. *)
  21.172 +       (case permuted_clause t ctms of
  21.173 +          SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
  21.174 +        | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
  21.175 +                              [t]))
  21.176 +      | do_line have (lname, t, deps) =
  21.177 +        have_or_show have lname ^
  21.178 +        string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^
  21.179 +        "\"\n  by (metis " ^ space_implode " " deps ^ ")\n"
  21.180 +    fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
  21.181 +      | do_lines ((lname, t, deps) :: lines) =
  21.182 +        do_line "have" (lname, t, deps) :: do_lines lines
  21.183 +  in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) do_lines end;
  21.184  
  21.185 -fun notequal t (_,t',_) = not (t aconv t');
  21.186 +fun unequal t (_, t', _) = not (t aconv t');
  21.187  
  21.188  (*No "real" literals means only type information*)
  21.189  fun eq_types t = t aconv HOLogic.true_const;
  21.190 @@ -375,7 +372,7 @@
  21.191        if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*)
  21.192        then map (replace_deps (lno, [])) lines
  21.193        else
  21.194 -       (case take_prefix (notequal t) lines of
  21.195 +       (case take_prefix (unequal t) lines of
  21.196             (_,[]) => lines                  (*no repetition of proof line*)
  21.197           | (pre, (lno', _, _) :: post) =>   (*repetition: replace later line by earlier one*)
  21.198               pre @ map (replace_deps (lno', [lno])) post)
  21.199 @@ -385,7 +382,7 @@
  21.200        if eq_types t then (lno, t, deps) :: lines
  21.201        (*Type information will be deleted later; skip repetition test.*)
  21.202        else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
  21.203 -      case take_prefix (notequal t) lines of
  21.204 +      case take_prefix (unequal t) lines of
  21.205           (_,[]) => (lno, t, deps) :: lines  (*no repetition of proof line*)
  21.206         | (pre, (lno', t', _) :: post) =>
  21.207             (lno, t', deps) ::               (*repetition: replace later line by earlier one*)
  21.208 @@ -399,7 +396,7 @@
  21.209    | add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines
  21.210  and delete_dep lno lines = List.foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines);
  21.211  
  21.212 -fun bad_free (Free (a,_)) = String.isPrefix "sko_" a
  21.213 +fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a
  21.214    | bad_free _ = false;
  21.215  
  21.216  (*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies.
  21.217 @@ -435,39 +432,42 @@
  21.218  fun isar_header [] = proofstart
  21.219    | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
  21.220  
  21.221 -fun decode_tstp_file cnfs ctxt th sgno thm_names =
  21.222 -  let val _ = trace "\ndecode_tstp_file: start\n"
  21.223 -      val tuples = map (dest_tstp o tstp_line o explode) cnfs
  21.224 -      val _ = trace (Int.toString (length tuples) ^ " tuples extracted\n")
  21.225 -      val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
  21.226 -      val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
  21.227 -      val _ = trace (Int.toString (length raw_lines) ^ " raw_lines extracted\n")
  21.228 -      val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
  21.229 -      val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
  21.230 -      val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
  21.231 -      val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
  21.232 -      val (ccls,fixes) = Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th sgno
  21.233 -      val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
  21.234 -      val ccls = map forall_intr_vars ccls
  21.235 -      val _ =
  21.236 -        if ! Sledgehammer_Fact_Preprocessor.trace then
  21.237 -          app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
  21.238 -        else
  21.239 -          ()
  21.240 -      val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
  21.241 -      val _ = trace "\ndecode_tstp_file: finishing\n"
  21.242 -  in
  21.243 -    isar_header (map #1 fixes) ^ implode ilines ^ "qed\n"
  21.244 -  end handle STREE _ => error "Could not extract proof (ATP output malformed?)";
  21.245 +fun isar_proof_from_tstp_file cnfs ctxt th sgno thm_names =
  21.246 +  let
  21.247 +    val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n")
  21.248 +    val tuples = map (dest_tstp o tstp_line o explode) cnfs
  21.249 +    val _ = trace_proof_msg (fn () =>
  21.250 +      Int.toString (length tuples) ^ " tuples extracted\n")
  21.251 +    val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
  21.252 +    val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
  21.253 +    val _ = trace_proof_msg (fn () =>
  21.254 +      Int.toString (length raw_lines) ^ " raw_lines extracted\n")
  21.255 +    val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
  21.256 +    val _ = trace_proof_msg (fn () =>
  21.257 +      Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
  21.258 +    val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
  21.259 +    val _ = trace_proof_msg (fn () =>
  21.260 +      Int.toString (length lines) ^ " lines extracted\n")
  21.261 +    val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno
  21.262 +    val _ = trace_proof_msg (fn () =>
  21.263 +      Int.toString (length ccls) ^ " conjecture clauses\n")
  21.264 +    val ccls = map forall_intr_vars ccls
  21.265 +    val _ = app (fn th => trace_proof_msg
  21.266 +                              (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
  21.267 +    val body = isar_proof_body ctxt (map prop_of ccls)
  21.268 +                               (stringify_deps thm_names [] lines)
  21.269 +    val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
  21.270 +  in isar_header (map #1 fixes) ^ implode body ^ "qed\n" end
  21.271 +  handle STREE _ => error "Could not extract proof (ATP output malformed?)";
  21.272  
  21.273  
  21.274  (*=== EXTRACTING PROOF-TEXT === *)
  21.275  
  21.276 -val begin_proof_strings = ["# SZS output start CNFRefutation.",
  21.277 +val begin_proof_strs = ["# SZS output start CNFRefutation.",
  21.278    "=========== Refutation ==========",
  21.279    "Here is a proof"];
  21.280  
  21.281 -val end_proof_strings = ["# SZS output end CNFRefutation",
  21.282 +val end_proof_strs = ["# SZS output end CNFRefutation",
  21.283    "======= End of refutation =======",
  21.284    "Formulae used in the proof"];
  21.285  
  21.286 @@ -475,8 +475,8 @@
  21.287    let
  21.288      (*splits to_split by the first possible of a list of splitters*)
  21.289      val (begin_string, end_string) =
  21.290 -      (find_first (fn s => String.isSubstring s proof) begin_proof_strings,
  21.291 -      find_first (fn s => String.isSubstring s proof) end_proof_strings)
  21.292 +      (find_first (fn s => String.isSubstring s proof) begin_proof_strs,
  21.293 +      find_first (fn s => String.isSubstring s proof) end_proof_strs)
  21.294    in
  21.295      if is_none begin_string orelse is_none end_string
  21.296      then error "Could not extract proof (no substring indicating a proof)"
  21.297 @@ -484,36 +484,24 @@
  21.298                 |> first_field (the end_string) |> the |> fst
  21.299    end;
  21.300  
  21.301 -(* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
  21.302 +(* ==== CHECK IF PROOF WAS SUCCESSFUL === *)
  21.303  
  21.304 -val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
  21.305 -  "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
  21.306 -val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
  21.307 -val failure_strings_SPASS = ["SPASS beiseite: Completion found.",
  21.308 -  "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."];
  21.309 -val failure_strings_remote = ["Remote-script could not extract proof"];
  21.310 -fun find_failure proof =
  21.311 -  let val failures =
  21.312 -    map_filter (fn s => if String.isSubstring s proof then SOME s else NONE)
  21.313 -      (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
  21.314 -  val correct = null failures andalso
  21.315 -    exists (fn s => String.isSubstring s proof) begin_proof_strings andalso
  21.316 -    exists (fn s => String.isSubstring s proof) end_proof_strings
  21.317 -  in
  21.318 -    if correct then NONE
  21.319 -    else if null failures then SOME "Output of ATP not in proper format"
  21.320 -    else SOME (hd failures) end;
  21.321 +fun is_proof_well_formed proof =
  21.322 +  exists (fn s => String.isSubstring s proof) begin_proof_strs andalso
  21.323 +  exists (fn s => String.isSubstring s proof) end_proof_strs
  21.324  
  21.325  (* === EXTRACTING LEMMAS === *)
  21.326  (* lines have the form "cnf(108, axiom, ...",
  21.327  the number (108) has to be extracted)*)
  21.328 -fun get_step_nums false proofextract =
  21.329 -  let val toks = String.tokens (not o Char.isAlphaNum)
  21.330 -  fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
  21.331 -    | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok
  21.332 -    | inputno _ = NONE
  21.333 -  val lines = split_lines proofextract
  21.334 -  in  map_filter (inputno o toks) lines  end
  21.335 +fun get_step_nums false extract =
  21.336 +  let
  21.337 +    val toks = String.tokens (not o Char.isAlphaNum)
  21.338 +    fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok
  21.339 +      | inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) =
  21.340 +        Int.fromString ntok
  21.341 +      | inputno _ = NONE
  21.342 +    val lines = split_lines extract
  21.343 +  in map_filter (inputno o toks) lines end
  21.344  (*String contains multiple lines. We want those of the form
  21.345    "253[0:Inp] et cetera..."
  21.346    A list consisting of the first number in each line is returned. *)
  21.347 @@ -527,27 +515,25 @@
  21.348  (*extracting lemmas from tstp-output between the lines from above*)
  21.349  fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
  21.350    let
  21.351 -  (* get the names of axioms from their numbers*)
  21.352 -  fun get_axiom_names thm_names step_nums =
  21.353 -    let
  21.354 -    val last_axiom = Vector.length thm_names
  21.355 -    fun is_axiom n = n <= last_axiom
  21.356 -    fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count
  21.357 -    fun getname i = Vector.sub(thm_names, i-1)
  21.358 -    in
  21.359 -      (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
  21.360 -        (map getname (filter is_axiom step_nums))),
  21.361 -      exists is_conj step_nums)
  21.362 -    end
  21.363 -  val proofextract = get_proof_extract proof
  21.364 -  in
  21.365 -    get_axiom_names thm_names (get_step_nums proofextract)
  21.366 -  end;
  21.367 +    (* get the names of axioms from their numbers*)
  21.368 +    fun get_axiom_names thm_names step_nums =
  21.369 +      let
  21.370 +        val last_axiom = Vector.length thm_names
  21.371 +        fun is_axiom n = n <= last_axiom
  21.372 +        fun is_conj n = n >= fst conj_count andalso
  21.373 +                        n < fst conj_count + snd conj_count
  21.374 +        fun getname i = Vector.sub(thm_names, i-1)
  21.375 +      in
  21.376 +        (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
  21.377 +          (map getname (filter is_axiom step_nums))),
  21.378 +        exists is_conj step_nums)
  21.379 +      end
  21.380 +  in get_axiom_names thm_names (get_step_nums (get_proof_extract proof)) end;
  21.381  
  21.382  (*Used to label theorems chained into the sledgehammer call*)
  21.383  val chained_hint = "CHAINED";
  21.384 -val nochained = filter_out (fn y => y = chained_hint)
  21.385 -  
  21.386 +val kill_chained = filter_out (curry (op =) chained_hint)
  21.387 +
  21.388  (* metis-command *)
  21.389  fun metis_line [] = "apply metis"
  21.390    | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
  21.391 @@ -555,34 +541,37 @@
  21.392  (* atp_minimize [atp=<prover>] <lemmas> *)
  21.393  fun minimize_line _ [] = ""
  21.394    | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
  21.395 -        (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^
  21.396 -                                         space_implode " " (nochained lemmas))
  21.397 -
  21.398 -fun sendback_metis_nochained lemmas =
  21.399 -  (Markup.markup Markup.sendback o metis_line) (nochained lemmas)
  21.400 +        Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
  21.401 +                                       space_implode " " (kill_chained lemmas))
  21.402  
  21.403 -fun lemma_list dfg name result =
  21.404 -  let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
  21.405 -  in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
  21.406 -    (if used_conj then ""
  21.407 -     else "\nWarning: Goal is provable because context is inconsistent."),
  21.408 -     nochained lemmas)
  21.409 +fun metis_lemma_list dfg name result =
  21.410 +  let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
  21.411 +    (Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^
  21.412 +     minimize_line name lemmas ^
  21.413 +     (if used_conj then
  21.414 +        ""
  21.415 +      else
  21.416 +        "\nWarning: The goal is provable because the context is inconsistent."),
  21.417 +     kill_chained lemmas)
  21.418    end;
  21.419  
  21.420 -(* === Extracting structured Isar-proof === *)
  21.421 -fun structured_proof name (result as (proof, thm_names, conj_count, ctxt, goal, subgoalno)) =
  21.422 +fun structured_isar_proof name (result as (proof, thm_names, conj_count, ctxt,
  21.423 +                                           goal, subgoalno)) =
  21.424    let
  21.425 -  (*Could use split_lines, but it can return blank lines...*)
  21.426 -  val lines = String.tokens (equal #"\n");
  21.427 -  val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
  21.428 -  val proofextract = get_proof_extract proof
  21.429 -  val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
  21.430 -  val (one_line_proof, lemma_names) = lemma_list false name result
  21.431 -  val structured =
  21.432 -    if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
  21.433 -    else decode_tstp_file cnfs ctxt goal subgoalno thm_names
  21.434 +    (* Could use "split_lines", but it can return blank lines *)
  21.435 +    val lines = String.tokens (equal #"\n");
  21.436 +    val kill_spaces =
  21.437 +      String.translate (fn c => if Char.isSpace c then "" else str c)
  21.438 +    val extract = get_proof_extract proof
  21.439 +    val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
  21.440 +    val (one_line_proof, lemma_names) = metis_lemma_list false name result
  21.441 +    val tokens = String.tokens (fn c => c = #" ") one_line_proof
  21.442 +    val isar_proof =
  21.443 +      if member (op =) tokens chained_hint then ""
  21.444 +      else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
  21.445    in
  21.446 -  (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured, lemma_names)
  21.447 -end
  21.448 +    (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback isar_proof,
  21.449 +     lemma_names)
  21.450 +  end
  21.451  
  21.452  end;
    22.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Mar 22 08:30:13 2010 +0100
    22.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Mar 22 13:48:15 2010 +0100
    22.3 @@ -22,7 +22,6 @@
    22.4    val global_setup: theory -> theory
    22.5    val split_limit: int Config.T
    22.6    val neq_limit: int Config.T
    22.7 -  val warning_count: int Unsynchronized.ref
    22.8    val trace: bool Unsynchronized.ref
    22.9  end;
   22.10  
   22.11 @@ -797,7 +796,6 @@
   22.12  fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
   22.13  val lin_arith_tac = Fast_Arith.lin_arith_tac;
   22.14  val trace = Fast_Arith.trace;
   22.15 -val warning_count = Fast_Arith.warning_count;
   22.16  
   22.17  (* reduce contradictory <= to False.
   22.18     Most of the work is done by the cancel tactics. *)
    23.1 --- a/src/HOL/Tools/meson.ML	Mon Mar 22 08:30:13 2010 +0100
    23.2 +++ b/src/HOL/Tools/meson.ML	Mon Mar 22 13:48:15 2010 +0100
    23.3 @@ -18,6 +18,7 @@
    23.4    val make_nnf: Proof.context -> thm -> thm
    23.5    val skolemize: Proof.context -> thm -> thm
    23.6    val is_fol_term: theory -> term -> bool
    23.7 +  val make_clauses_unsorted: thm list -> thm list
    23.8    val make_clauses: thm list -> thm list
    23.9    val make_horns: thm list -> thm list
   23.10    val best_prolog_tac: (thm -> int) -> thm list -> tactic
   23.11 @@ -560,7 +561,8 @@
   23.12  
   23.13  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   23.14    The resulting clauses are HOL disjunctions.*)
   23.15 -fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []);
   23.16 +fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
   23.17 +val make_clauses = sort_clauses o make_clauses_unsorted;
   23.18  
   23.19  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   23.20  fun make_horns ths =
    24.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 22 08:30:13 2010 +0100
    24.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 22 13:48:15 2010 +0100
    24.3 @@ -96,7 +96,6 @@
    24.4                       number_of : serial * (theory -> typ -> int -> cterm)})
    24.5                  -> Context.generic -> Context.generic
    24.6    val trace: bool Unsynchronized.ref
    24.7 -  val warning_count: int Unsynchronized.ref;
    24.8  end;
    24.9  
   24.10  functor Fast_Lin_Arith
   24.11 @@ -426,9 +425,6 @@
   24.12  fun trace_msg msg =
   24.13    if !trace then tracing msg else ();
   24.14  
   24.15 -val warning_count = Unsynchronized.ref 0;
   24.16 -val warning_count_max = 10;
   24.17 -
   24.18  val union_term = union Pattern.aeconv;
   24.19  val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'));
   24.20  
   24.21 @@ -532,17 +528,11 @@
   24.22        val _ =
   24.23          if LA_Logic.is_False fls then ()
   24.24          else
   24.25 -          let val count = CRITICAL (fn () => Unsynchronized.inc warning_count) in
   24.26 -            if count > warning_count_max then ()
   24.27 -            else
   24.28 -              (tracing (cat_lines
   24.29 -                (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
   24.30 -                 ["Proved:", Display.string_of_thm ctxt fls, ""] @
   24.31 -                 (if count <> warning_count_max then []
   24.32 -                  else ["\n(Reached maximal message count -- disabling future warnings)"])));
   24.33 -                warning "Linear arithmetic should have refuted the assumptions.\n\
   24.34 -                  \Please inform Tobias Nipkow (nipkow@in.tum.de).")
   24.35 -          end;
   24.36 +         (tracing (cat_lines
   24.37 +           (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
   24.38 +            ["Proved:", Display.string_of_thm ctxt fls, ""]));
   24.39 +          warning "Linear arithmetic should have refuted the assumptions.\n\
   24.40 +            \Please inform Tobias Nipkow.")
   24.41      in fls end
   24.42      handle FalseE thm => trace_thm ctxt "False reached early:" thm
   24.43    end;
    25.1 --- a/src/Pure/Isar/class_target.ML	Mon Mar 22 08:30:13 2010 +0100
    25.2 +++ b/src/Pure/Isar/class_target.ML	Mon Mar 22 13:48:15 2010 +0100
    25.3 @@ -16,12 +16,13 @@
    25.4    val rules: theory -> class -> thm option * thm
    25.5    val these_params: theory -> sort -> (string * (class * (string * typ))) list
    25.6    val these_defs: theory -> sort -> thm list
    25.7 -  val these_operations: theory -> sort -> (string * (class * (typ * term))) list
    25.8 +  val these_operations: theory -> sort
    25.9 +    -> (string * (class * (typ * term))) list
   25.10    val print_classes: theory -> unit
   25.11  
   25.12    val begin: class list -> sort -> Proof.context -> Proof.context
   25.13    val init: class -> theory -> Proof.context
   25.14 -  val declare: class -> (binding * mixfix) * term -> theory -> theory
   25.15 +  val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory
   25.16    val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
   25.17    val class_prefix: string -> string
   25.18    val refresh_syntax: class -> Proof.context -> Proof.context
   25.19 @@ -253,8 +254,8 @@
   25.20  
   25.21  (* class context syntax *)
   25.22  
   25.23 -fun these_unchecks thy =
   25.24 -  map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
   25.25 +fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
   25.26 +  o these_operations thy;
   25.27  
   25.28  fun redeclare_const thy c =
   25.29    let val b = Long_Name.base_name c
   25.30 @@ -317,15 +318,15 @@
   25.31  
   25.32  val class_prefix = Logic.const_of_class o Long_Name.base_name;
   25.33  
   25.34 -fun declare class ((c, mx), dict) thy =
   25.35 +fun declare class ((c, mx), (type_params, dict)) thy =
   25.36    let
   25.37      val morph = morphism thy class;
   25.38      val b = Morphism.binding morph c;
   25.39      val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b);
   25.40      val c' = Sign.full_name thy b;
   25.41      val dict' = Morphism.term morph dict;
   25.42 -    val ty' = Term.fastype_of dict';
   25.43 -    val def_eq = Logic.mk_equals (Const (c', ty'), dict')
   25.44 +    val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict';
   25.45 +    val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict')
   25.46        |> map_types Type.strip_sorts;
   25.47    in
   25.48      thy
   25.49 @@ -335,7 +336,7 @@
   25.50      |>> Thm.varifyT_global
   25.51      |-> (fn def_thm => PureThy.store_thm (b_def, def_thm)
   25.52        #> snd
   25.53 -      #> register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
   25.54 +      #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
   25.55      |> Sign.add_const_constraint (c', SOME ty')
   25.56    end;
   25.57  
    26.1 --- a/src/Pure/Isar/overloading.ML	Mon Mar 22 08:30:13 2010 +0100
    26.2 +++ b/src/Pure/Isar/overloading.ML	Mon Mar 22 13:48:15 2010 +0100
    26.3 @@ -13,7 +13,7 @@
    26.4    val define: bool -> binding -> string * term -> theory -> thm * theory
    26.5    val operation: Proof.context -> binding -> (string * bool) option
    26.6    val pretty: Proof.context -> Pretty.T
    26.7 -  
    26.8 +
    26.9    type improvable_syntax
   26.10    val add_improvable_syntax: Proof.context -> Proof.context
   26.11    val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
    27.1 --- a/src/Pure/Isar/theory_target.ML	Mon Mar 22 08:30:13 2010 +0100
    27.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Mar 22 13:48:15 2010 +0100
    27.3 @@ -277,7 +277,7 @@
    27.4    in
    27.5      lthy'
    27.6      |> is_locale ? syntax_declaration ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
    27.7 -    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
    27.8 +    |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), (type_params, t)))
    27.9      |> Local_Defs.add_def ((b, NoSyn), t)
   27.10    end;
   27.11