--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 26 20:49:54 2012 +0100
@@ -336,7 +336,7 @@
| NONE => get_prover (default_prover_name ()))
end
-type locality = ATP_Problem_Generate.locality
+type stature = ATP_Problem_Generate.stature
(* hack *)
fun reconstructor_from_msg args msg =
@@ -357,7 +357,7 @@
local
datatype sh_result =
- SH_OK of int * int * (string * locality) list |
+ SH_OK of int * int * (string * stature) list |
SH_FAIL of int * int |
SH_ERROR
@@ -486,8 +486,8 @@
case result of
SH_OK (time_isa, time_prover, names) =>
let
- fun get_thms (name, loc) =
- SOME ((name, loc), thms_of_name (Proof.context_of st) name)
+ fun get_thms (name, stature) =
+ SOME ((name, stature), thms_of_name (Proof.context_of st) name)
in
change_data id inc_sh_success;
if trivial then () else change_data id inc_sh_nontriv_success;
@@ -654,7 +654,7 @@
let
val reconstructor = Unsynchronized.ref ""
val named_thms =
- Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
+ Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
val minimize = AList.defined (op =) args minimizeK
val metis_ft = AList.defined (op =) args metis_ftK
val trivial =
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jan 26 20:49:54 2012 +0100
@@ -15,8 +15,9 @@
type formula_kind = ATP_Problem.formula_kind
type 'a problem = 'a ATP_Problem.problem
- datatype locality =
- General | Induction | Intro | Elim | Simp | Local | Assum | Chained
+ datatype scope = Global | Local | Assum | Chained
+ datatype status = General | Induct | Intro | Elim | Simp
+ type stature = scope * status
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype strictness = Strict | Non_Strict
@@ -101,8 +102,8 @@
val prepare_atp_problem :
Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
-> bool -> string -> bool -> bool -> term list -> term
- -> ((string * locality) * term) list
- -> string problem * string Symtab.table * (string * locality) list vector
+ -> ((string * stature) * term) list
+ -> string problem * string Symtab.table * (string * stature) list vector
* (string * term) list * int Symtab.table
val atp_problem_weights : string problem -> (string * real) list
end;
@@ -541,8 +542,9 @@
val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
-datatype locality =
- General | Induction | Intro | Elim | Simp | Local | Assum | Chained
+datatype scope = Global | Local | Assum | Chained
+datatype status = General | Induct | Intro | Elim | Simp
+type stature = scope * status
datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
@@ -720,14 +722,14 @@
type translated_formula =
{name : string,
- locality : locality,
+ stature : stature,
kind : formula_kind,
iformula : (name, typ, iterm) formula,
atomic_types : typ list}
-fun update_iformula f ({name, locality, kind, iformula, atomic_types}
+fun update_iformula f ({name, stature, kind, iformula, atomic_types}
: translated_formula) =
- {name = name, locality = locality, kind = kind, iformula = f iformula,
+ {name = name, stature = stature, kind = kind, iformula = f iformula,
atomic_types = atomic_types} : translated_formula
fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
@@ -1180,7 +1182,8 @@
|>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
val lam_facts =
map2 (fn t => fn j =>
- ((lam_fact_prefix ^ Int.toString j, General), (Axiom, t)))
+ ((lam_fact_prefix ^ Int.toString j, (Global, General)),
+ (Axiom, t)))
lambda_ts (1 upto length lambda_ts)
in (facts, lam_facts) end
@@ -1211,20 +1214,20 @@
handle TERM _ => if role = Conjecture then @{term False} else @{term True})
|> pair role
-fun make_formula ctxt format type_enc eq_as_iff name loc kind t =
+fun make_formula ctxt format type_enc eq_as_iff name stature kind t =
let
val (iformula, atomic_Ts) =
iformula_from_prop ctxt format type_enc eq_as_iff
(SOME (kind <> Conjecture)) t []
|>> close_iformula_universally
in
- {name = name, locality = loc, kind = kind, iformula = iformula,
+ {name = name, stature = stature, kind = kind, iformula = iformula,
atomic_types = atomic_Ts}
end
-fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
+fun make_fact ctxt format type_enc eq_as_iff ((name, stature), t) =
case t |> make_formula ctxt format type_enc (eq_as_iff andalso format <> CNF)
- name loc Axiom of
+ name stature Axiom of
formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
if s = tptp_true then NONE else SOME formula
| formula => SOME formula
@@ -1234,9 +1237,10 @@
if fastype_of t = @{typ bool} then s_not t else @{prop False} (* too meta *)
fun make_conjecture ctxt format type_enc =
- map (fn ((name, loc), (kind, t)) =>
+ map (fn ((name, stature), (kind, t)) =>
t |> kind = Conjecture ? s_not_trueprop
- |> make_formula ctxt format type_enc (format <> CNF) name loc kind)
+ |> make_formula ctxt format type_enc (format <> CNF) name stature
+ kind)
(** Finite and infinite type inference **)
@@ -1618,7 +1622,7 @@
[t]
end
|> tag_list 1
- |> map (fn (k, t) => ((dub needs_fairly_sound j k, Simp), t))
+ |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Simp)), t))
val make_facts = map_filter (make_fact ctxt format type_enc false)
val fairly_sound = is_type_enc_fairly_sound type_enc
in
@@ -1717,7 +1721,8 @@
val conjs =
map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
|> map (apsnd freeze_term)
- |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
+ |> map2 (pair o rpair (Local, General) o string_of_int)
+ (0 upto length hyp_ts)
val ((conjs, facts), lam_facts) =
(conjs, facts)
|> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt))))
@@ -1892,7 +1897,7 @@
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos
- mono type_enc (j, {name, locality, kind, iformula, atomic_types}) =
+ mono type_enc (j, {name, stature, kind, iformula, atomic_types}) =
(prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
iformula
|> formula_from_iformula ctxt polym_constrs format mono type_enc
@@ -1900,7 +1905,7 @@
|> close_formula_universally
|> bound_tvars type_enc true atomic_types,
NONE,
- case locality of
+ case snd stature of
Intro => isabelle_info format introN
| Elim => isabelle_info format elimN
| Simp => isabelle_info format simpN
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Jan 26 20:49:54 2012 +0100
@@ -11,7 +11,7 @@
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
type 'a proof = 'a ATP_Proof.proof
- type locality = ATP_Problem_Generate.locality
+ type stature = ATP_Problem_Generate.stature
datatype reconstructor =
Metis of string * string |
@@ -24,9 +24,9 @@
type minimize_command = string list -> string
type one_line_params =
- play * string * (string * locality) list * minimize_command * int * int
+ play * string * (string * stature) list * minimize_command * int * int
type isar_params =
- bool * int * string Symtab.table * (string * locality) list vector
+ bool * int * string Symtab.table * (string * stature) list vector
* int Symtab.table * string proof * thm
val metisN : string
@@ -44,12 +44,12 @@
val metis_call : string -> string -> string
val string_for_reconstructor : reconstructor -> string
val used_facts_in_atp_proof :
- Proof.context -> (string * locality) list vector -> string proof
- -> (string * locality) list
+ Proof.context -> (string * stature) list vector -> string proof
+ -> (string * stature) list
val lam_trans_from_atp_proof : string proof -> string -> string
val is_typed_helper_used_in_atp_proof : string proof -> bool
val used_facts_in_unsound_atp_proof :
- Proof.context -> (string * locality) list vector -> 'a proof
+ Proof.context -> (string * stature) list vector -> 'a proof
-> string list option
val unalias_type_enc : string -> string list
val one_line_proof_text : one_line_params -> string
@@ -93,9 +93,9 @@
type minimize_command = string list -> string
type one_line_params =
- play * string * (string * locality) list * minimize_command * int * int
+ play * string * (string * stature) list * minimize_command * int * int
type isar_params =
- bool * int * string Symtab.table * (string * locality) list vector
+ bool * int * string Symtab.table * (string * stature) list vector
* int Symtab.table * string proof * thm
val metisN = "metis"
@@ -198,25 +198,20 @@
fun add_fact _ fact_names (Inference ((_, ss), _, _, [])) =
union (op =) (resolve_fact fact_names ss)
| add_fact ctxt _ (Inference (_, _, rule, _)) =
- if rule = leo2_ext then insert (op =) (ext_name ctxt, General) else I
+ if rule = leo2_ext then insert (op =) (ext_name ctxt, (Global, General))
+ else I
| add_fact _ _ _ = I
fun used_facts_in_atp_proof ctxt fact_names atp_proof =
if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
else fold (add_fact ctxt fact_names) atp_proof []
-(* (quasi-)underapproximation of the truth *)
-fun is_locality_global Local = false
- | is_locality_global Assum = false
- | is_locality_global Chained = false
- | is_locality_global _ = true
-
fun used_facts_in_unsound_atp_proof _ _ [] = NONE
| used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
let
val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
in
- if forall (is_locality_global o snd) used_facts andalso
+ if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then
SOME (map fst used_facts)
else
@@ -250,10 +245,11 @@
| minimize_line minimize_command ss =
case minimize_command ss of
"" => ""
- | command => "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
+ | command =>
+ "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
val split_used_facts =
- List.partition (curry (op =) Chained o snd)
+ List.partition (fn (_, (sc, _)) => sc = Chained)
#> pairself (sort_distinct (string_ord o pairself fst))
fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
--- a/src/HOL/Tools/Metis/metis_generate.ML Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML Thu Jan 26 20:49:54 2012 +0100
@@ -222,10 +222,9 @@
|> pairself (maps (map (zero_var_indexes o snd)))
val num_conjs = length conj_clauses
val clauses =
- map2 (fn j => pair (Int.toString j, Local))
+ map2 (fn j => pair (Int.toString j, (Local, General)))
(0 upto num_conjs - 1) conj_clauses @
- (* "General" below isn't quite correct; the fact could be local. *)
- map2 (fn j => pair (Int.toString (num_conjs + j), General))
+ map2 (fn j => pair (Int.toString (num_conjs + j), (Local, General)))
(0 upto length fact_clauses - 1) fact_clauses
val (old_skolems, props) =
fold_rev (fn (name, th) => fn (old_skolems, props) =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jan 26 20:49:54 2012 +0100
@@ -7,7 +7,7 @@
signature SLEDGEHAMMER_FILTER =
sig
- type locality = ATP_Problem_Generate.locality
+ type stature = ATP_Problem_Generate.stature
type relevance_fudge =
{local_const_multiplier : real,
@@ -44,19 +44,19 @@
-> string list
val fact_from_ref :
Proof.context -> unit Symtab.table -> thm list
- -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
+ -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
val all_facts :
Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list
- -> (((unit -> string) * locality) * thm) list
+ -> (((unit -> string) * stature) * thm) list
val nearly_all_facts :
Proof.context -> bool -> relevance_override -> thm list -> term list -> term
- -> (((unit -> string) * locality) * thm) list
+ -> (((unit -> string) * stature) * thm) list
val relevant_facts :
Proof.context -> real * real -> int
-> (string * typ -> term list -> bool * term list) -> relevance_fudge
-> relevance_override -> thm list -> term list -> term
- -> (((unit -> string) * locality) * thm) list
- -> ((string * locality) * thm) list
+ -> (((unit -> string) * stature) * thm) list
+ -> ((string * stature) * thm) list
end;
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
@@ -144,8 +144,8 @@
|-> fold (fn th => fn (j, rest) =>
(j + 1,
((nth_name j,
- if member Thm.eq_thm_prop chained_ths th then Chained
- else General), th) :: rest))
+ (if member Thm.eq_thm_prop chained_ths th then Chained
+ else Local (* just in case *), General)), th) :: rest))
|> snd
end
@@ -190,7 +190,7 @@
NONE
| _ => NONE
-fun instantiate_induct_rule ctxt concl_prop p_name ((name, loc), th) ind_x =
+fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
let
fun varify_noninducts (t as Free (s, T)) =
if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
@@ -200,8 +200,8 @@
|> lambda (Free ind_x)
|> string_for_term ctxt
in
- ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", loc),
- th |> read_instantiate ctxt [((p_name, 0), p_inst)])
+ ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
+ stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
end
fun type_match thy (T1, T2) =
@@ -467,19 +467,21 @@
chained_const_irrel_weight (irrel_weight_for fudge) swap
const_tab chained_const_tab
-fun locality_bonus ({intro_bonus, ...} : relevance_fudge) Intro = intro_bonus
- | locality_bonus {elim_bonus, ...} Elim = elim_bonus
- | locality_bonus {simp_bonus, ...} Simp = simp_bonus
- | locality_bonus {local_bonus, ...} Local = local_bonus
- | locality_bonus {assum_bonus, ...} Assum = assum_bonus
- | locality_bonus {chained_bonus, ...} Chained = chained_bonus
- | locality_bonus _ _ = 0.0
+fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
+ intro_bonus
+ | stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus
+ | stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus
+ | stature_bonus {local_bonus, ...} (Local, _) = local_bonus
+ | stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus
+ | stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus
+ | stature_bonus _ _ = 0.0
fun is_odd_const_name s =
s = abs_name orelse String.isPrefix skolem_prefix s orelse
String.isSuffix theory_const_suffix s
-fun fact_weight fudge loc const_tab relevant_consts chained_consts fact_consts =
+fun fact_weight fudge stature const_tab relevant_consts chained_consts
+ fact_consts =
case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
||> filter_out (pconst_hyper_mem swap relevant_consts) of
([], _) => 0.0
@@ -492,7 +494,7 @@
val rel_weight =
0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
val irrel_weight =
- ~ (locality_bonus fudge loc)
+ ~ (stature_bonus fudge stature)
|> fold (curry (op +)
o irrel_pconst_weight fudge const_tab chained_consts) irrel
val res = rel_weight / (rel_weight + irrel_weight)
@@ -512,7 +514,7 @@
val const_names_in_fact = map fst ooo pconsts_in_fact
type annotated_thm =
- (((unit -> string) * locality) * thm) * (string * ptype) list
+ (((unit -> string) * stature) * thm) * (string * ptype) list
fun take_most_relevant ctxt max_relevant remaining_max
({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
@@ -537,13 +539,12 @@
(accepts, more_rejects @ rejects)
end
-fun if_empty_replace_with_locality thy is_built_in_const facts loc tab =
+fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
if Symtab.is_empty tab then
Symtab.empty
|> fold (add_pconsts_in_term thy is_built_in_const false (SOME false))
- (map_filter (fn ((_, loc'), th) =>
- if loc' = loc then SOME (prop_of th) else NONE)
- facts)
+ (map_filter (fn ((_, (sc', _)), th) =>
+ if sc' = sc then SOME (prop_of th) else NONE) facts)
else
tab
@@ -584,7 +585,7 @@
Symtab.empty |> fold (add_pconsts true) hyp_ts
|> add_pconsts false concl_t
|> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
- |> fold (if_empty_replace_with_locality thy is_built_in_const facts)
+ |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
[Chained, Assum, Local]
val add_ths = Attrib.eval_thms ctxt add
val del_ths = Attrib.eval_thms ctxt del
@@ -637,13 +638,13 @@
hopeless_rejects hopeful_rejects)
end
| relevant candidates rejects
- (((ax as (((_, loc), _), fact_consts)), cached_weight)
+ (((ax as (((_, stature), _), fact_consts)), cached_weight)
:: hopeful) =
let
val weight =
case cached_weight of
SOME w => w
- | NONE => fact_weight fudge loc const_tab rel_const_tab
+ | NONE => fact_weight fudge stature const_tab rel_const_tab
chained_const_tab fact_consts
in
if weight >= threshold then
@@ -783,8 +784,8 @@
let
val thy = Proof_Context.theory_of ctxt
val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
- fun add loc g f =
- fold (Termtab.update o rpair loc o g o crude_zero_vars o prop_of o f)
+ fun add stature g f =
+ fold (Termtab.update o rpair stature o g o crude_zero_vars o prop_of o f)
val {safeIs, safeEs, hazIs, hazEs, ...} =
ctxt |> claset_of |> Classical.rep_cs
val intros = Item_Net.content safeIs @ Item_Net.content hazIs
@@ -809,20 +810,19 @@
fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
val is_chained = member Thm.eq_thm_prop chained_ths
val clasimpset_table = clasimpset_rule_table_of ctxt
- fun locality_of_theorem global name th =
- if String.isSubstring ".induct" name orelse (*FIXME: use structured name*)
+ fun scope_of_thm global th =
+ if is_chained th then Chained
+ else if global then Global
+ else if is_assum th then Assum
+ else Local
+ fun status_of_thm name th =
+ (* FIXME: use structured name *)
+ if String.isSubstring ".induct" name orelse
String.isSubstring ".inducts" name then
- Induction
- else if is_chained th then
- Chained
- else if global then
- case Termtab.lookup clasimpset_table (prop_of th) of
- SOME loc => loc
- | NONE => General
- else if is_assum th then
- Assum
- else
- Local
+ Induct
+ else case Termtab.lookup clasimpset_table (prop_of th) of
+ SOME status => status
+ | NONE => General
fun is_good_unnamed_local th =
not (Thm.has_name_hint th) andalso
forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
@@ -872,7 +872,8 @@
|> (fn SOME name =>
make_name reserved multi j name
| NONE => "")),
- locality_of_theorem global name0 th), th)
+ (scope_of_thm global th,
+ status_of_thm name0 th)), th)
in
if multi then (new :: multis, unis)
else (multis, new :: unis)
@@ -902,7 +903,7 @@
val ind_stmt_xs = external_frees ind_stmt
in
(if only then
- maps (map (fn ((name, loc), th) => ((K name, loc), th))
+ maps (map (fn ((name, stature), th) => ((K name, stature), th))
o fact_from_ref ctxt reserved chained_ths) add
else
all_facts ctxt ho_atp reserved false add_ths chained_ths)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 26 20:49:54 2012 +0100
@@ -7,15 +7,15 @@
signature SLEDGEHAMMER_MINIMIZE =
sig
- type locality = ATP_Problem_Generate.locality
+ type stature = ATP_Problem_Generate.stature
type play = ATP_Proof_Reconstruct.play
type params = Sledgehammer_Provers.params
val binary_min_facts : int Config.T
val minimize_facts :
string -> params -> bool -> int -> int -> Proof.state
- -> ((string * locality) * thm list) list
- -> ((string * locality) * thm list) list option
+ -> ((string * stature) * thm list) list
+ -> ((string * stature) * thm list) list option
* ((unit -> play) * (play -> string) * string)
val run_minimize :
params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
@@ -192,7 +192,8 @@
min test (new_timeout timeout run_time) result facts
val _ = print silent (fn () => cat_lines
["Minimized to " ^ n_facts (map fst min_facts)] ^
- (case length (filter (curry (op =) Chained o snd o fst) min_facts) of
+ (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
+ |> length of
0 => ""
| n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".")
in (SOME min_facts, (preplay, message, message_tail)) end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 26 20:49:54 2012 +0100
@@ -9,7 +9,7 @@
signature SLEDGEHAMMER_PROVERS =
sig
type failure = ATP_Proof.failure
- type locality = ATP_Problem_Generate.locality
+ type stature = ATP_Problem_Generate.stature
type type_enc = ATP_Problem_Generate.type_enc
type reconstructor = ATP_Proof_Reconstruct.reconstructor
type play = ATP_Proof_Reconstruct.play
@@ -40,8 +40,8 @@
expect: string}
datatype prover_fact =
- Untranslated_Fact of (string * locality) * thm |
- SMT_Weighted_Fact of (string * locality) * (int option * thm)
+ Untranslated_Fact of (string * stature) * thm |
+ SMT_Weighted_Fact of (string * stature) * (int option * thm)
type prover_problem =
{state: Proof.state,
@@ -49,11 +49,11 @@
subgoal: int,
subgoal_count: int,
facts: prover_fact list,
- smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
+ smt_filter: (string * stature) SMT_Solver.smt_filter_data option}
type prover_result =
{outcome: failure option,
- used_facts: (string * locality) list,
+ used_facts: (string * stature) list,
run_time: Time.time,
preplay: unit -> play,
message: play -> string,
@@ -98,12 +98,12 @@
val smt_relevance_fudge : relevance_fudge
val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
val weight_smt_fact :
- Proof.context -> int -> ((string * locality) * thm) * int
- -> (string * locality) * (int option * thm)
- val untranslated_fact : prover_fact -> (string * locality) * thm
+ Proof.context -> int -> ((string * stature) * thm) * int
+ -> (string * stature) * (int option * thm)
+ val untranslated_fact : prover_fact -> (string * stature) * thm
val smt_weighted_fact :
Proof.context -> int -> prover_fact * int
- -> (string * locality) * (int option * thm)
+ -> (string * stature) * (int option * thm)
val supported_provers : Proof.context -> unit
val kill_provers : unit -> unit
val running_provers : unit -> unit
@@ -304,8 +304,8 @@
expect: string}
datatype prover_fact =
- Untranslated_Fact of (string * locality) * thm |
- SMT_Weighted_Fact of (string * locality) * (int option * thm)
+ Untranslated_Fact of (string * stature) * thm |
+ SMT_Weighted_Fact of (string * stature) * (int option * thm)
type prover_problem =
{state: Proof.state,
@@ -313,11 +313,11 @@
subgoal: int,
subgoal_count: int,
facts: prover_fact list,
- smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
+ smt_filter: (string * stature) SMT_Solver.smt_filter_data option}
type prover_result =
{outcome: failure option,
- used_facts: (string * locality) list,
+ used_facts: (string * stature) list,
run_time: Time.time,
preplay: unit -> play,
message: play -> string,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 26 20:49:54 2012 +0100
@@ -172,7 +172,7 @@
get_prover ctxt mode name params minimize_command problem
|> minimize ctxt mode name params problem
-fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true
+fun is_induction_fact (Untranslated_Fact ((_, (_, Induct)), _)) = true
| is_induction_fact _ = false
fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,