# HG changeset patch # User blanchet # Date 1327607394 -3600 # Node ID cac402c486b029ed2bb415011a5da7091f698281 # Parent 6268c5b3efdc012419fa44a5a795b39ec7ab9c39 separate orthogonal components diff -r 6268c5b3efdc -r cac402c486b0 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 = diff -r 6268c5b3efdc -r cac402c486b0 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 diff -r 6268c5b3efdc -r cac402c486b0 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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, diff -r 6268c5b3efdc -r cac402c486b0 src/HOL/Tools/Metis/metis_generate.ML --- 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) => diff -r 6268c5b3efdc -r cac402c486b0 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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) diff -r 6268c5b3efdc -r cac402c486b0 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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 diff -r 6268c5b3efdc -r cac402c486b0 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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, diff -r 6268c5b3efdc -r cac402c486b0 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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,