--- a/src/FOL/FOL.thy Sat May 14 18:26:25 2011 +0200
+++ b/src/FOL/FOL.thy Sat May 14 22:00:24 2011 +0200
@@ -167,7 +167,7 @@
section {* Classical Reasoner *}
ML {*
-structure Cla = ClassicalFun
+structure Cla = Classical
(
val imp_elim = @{thm imp_elim}
val not_elim = @{thm notE}
@@ -201,7 +201,7 @@
structure Blast = Blast
(
structure Classical = Cla
- val thy = @{theory}
+ val Trueprop_const = dest_Const @{const Trueprop}
val equality_name = @{const_name eq}
val not_name = @{const_name Not}
val notE = @{thm notE}
--- a/src/FOL/IFOL.thy Sat May 14 18:26:25 2011 +0200
+++ b/src/FOL/IFOL.thy Sat May 14 22:00:24 2011 +0200
@@ -19,7 +19,6 @@
"~~/src/Tools/project_rule.ML"
"~~/src/Tools/atomize_elim.ML"
("fologic.ML")
- ("hypsubstdata.ML")
("intprover.ML")
begin
@@ -592,7 +591,23 @@
lemma thin_refl: "[|x=x; PROP W|] ==> PROP W" .
-use "hypsubstdata.ML"
+ML {*
+structure Hypsubst = Hypsubst
+(
+ val dest_eq = FOLogic.dest_eq
+ val dest_Trueprop = FOLogic.dest_Trueprop
+ val dest_imp = FOLogic.dest_imp
+ val eq_reflection = @{thm eq_reflection}
+ val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
+ val imp_intr = @{thm impI}
+ val rev_mp = @{thm rev_mp}
+ val subst = @{thm subst}
+ val sym = @{thm sym}
+ val thin_refl = @{thm thin_refl}
+);
+open Hypsubst;
+*}
+
setup hypsubst_setup
use "intprover.ML"
--- a/src/FOL/IsaMakefile Sat May 14 18:26:25 2011 +0200
+++ b/src/FOL/IsaMakefile Sat May 14 22:00:24 2011 +0200
@@ -36,8 +36,7 @@
$(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \
$(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML \
- document/root.tex fologic.ML hypsubstdata.ML intprover.ML \
- simpdata.ML
+ document/root.tex fologic.ML intprover.ML simpdata.ML
@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
--- a/src/FOL/hypsubstdata.ML Sat May 14 18:26:25 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-
-(** Applying HypsubstFun to generate hyp_subst_tac **)
-structure Hypsubst_Data =
-struct
- structure Simplifier = Simplifier
- val dest_eq = FOLogic.dest_eq
- val dest_Trueprop = FOLogic.dest_Trueprop
- val dest_imp = FOLogic.dest_imp
- val eq_reflection = @{thm eq_reflection}
- val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
- val imp_intr = @{thm impI}
- val rev_mp = @{thm rev_mp}
- val subst = @{thm subst}
- val sym = @{thm sym}
- val thin_refl = @{thm thin_refl}
-end;
-
-structure Hypsubst = HypsubstFun(Hypsubst_Data);
-open Hypsubst;
--- a/src/FOLP/FOLP.thy Sat May 14 18:26:25 2011 +0200
+++ b/src/FOLP/FOLP.thy Sat May 14 22:00:24 2011 +0200
@@ -103,17 +103,14 @@
use "simp.ML" (* Patched 'cos matching won't instantiate proof *)
ML {*
-(*** Applying ClassicalFun to create a classical prover ***)
-structure Classical_Data =
-struct
+structure Cla = Classical
+(
val sizef = size_of_thm
val mp = @{thm mp}
val not_elim = @{thm notE}
val swap = @{thm swap}
val hyp_subst_tacs = [hyp_subst_tac]
-end;
-
-structure Cla = ClassicalFun(Classical_Data);
+);
open Cla;
(*Propositional rules
--- a/src/FOLP/IFOLP.thy Sat May 14 18:26:25 2011 +0200
+++ b/src/FOLP/IFOLP.thy Sat May 14 22:00:24 2011 +0200
@@ -587,11 +587,8 @@
use "hypsubst.ML"
ML {*
-
-(*** Applying HypsubstFun to generate hyp_subst_tac ***)
-
-structure Hypsubst_Data =
-struct
+structure Hypsubst = Hypsubst
+(
(*Take apart an equality judgement; otherwise raise Match!*)
fun dest_eq (Const (@{const_name Proof}, _) $
(Const (@{const_name eq}, _) $ t $ u) $ _) = (t, u);
@@ -605,9 +602,7 @@
val subst = @{thm subst}
val sym = @{thm sym}
val thin_refl = @{thm thin_refl}
-end;
-
-structure Hypsubst = HypsubstFun(Hypsubst_Data);
+);
open Hypsubst;
*}
--- a/src/FOLP/classical.ML Sat May 14 18:26:25 2011 +0200
+++ b/src/FOLP/classical.ML Sat May 14 22:00:24 2011 +0200
@@ -60,7 +60,7 @@
end;
-functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =
+functor Classical(Data: CLASSICAL_DATA): CLASSICAL =
struct
local open Data in
--- a/src/FOLP/hypsubst.ML Sat May 14 18:26:25 2011 +0200
+++ b/src/FOLP/hypsubst.ML Sat May 14 22:00:24 2011 +0200
@@ -26,7 +26,7 @@
val inspect_pair : bool -> term * term -> thm
end;
-functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
+functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
struct
local open Data in
--- a/src/HOL/HOL.thy Sat May 14 18:26:25 2011 +0200
+++ b/src/HOL/HOL.thy Sat May 14 22:00:24 2011 +0200
@@ -826,9 +826,8 @@
"\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
ML {*
-structure Hypsubst = HypsubstFun(
-struct
- structure Simplifier = Simplifier
+structure Hypsubst = Hypsubst
+(
val dest_eq = HOLogic.dest_eq
val dest_Trueprop = HOLogic.dest_Trueprop
val dest_imp = HOLogic.dest_imp
@@ -839,18 +838,18 @@
val subst = @{thm subst}
val sym = @{thm sym}
val thin_refl = @{thm thin_refl};
-end);
+);
open Hypsubst;
-structure Classical = ClassicalFun(
-struct
+structure Classical = Classical
+(
val imp_elim = @{thm imp_elim}
val not_elim = @{thm notE}
val swap = @{thm swap}
val classical = @{thm classical}
val sizef = Drule.size_of_thm
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
-end);
+);
structure Basic_Classical: BASIC_CLASSICAL = Classical;
open Basic_Classical;
@@ -930,7 +929,7 @@
structure Blast = Blast
(
structure Classical = Classical
- val thy = @{theory}
+ val Trueprop_const = dest_Const @{const Trueprop}
val equality_name = @{const_name HOL.eq}
val not_name = @{const_name Not}
val notE = @{thm notE}
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Sat May 14 18:26:25 2011 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sat May 14 22:00:24 2011 +0200
@@ -34,7 +34,7 @@
gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
fun cut_inst_tac_term' tinst th =
- res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th);
+ res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve th);
fun get_dyn_thm thy name atom_name =
Global_Theory.get_thm thy name handle ERROR _ =>
--- a/src/HOL/TLA/TLA.thy Sat May 14 18:26:25 2011 +0200
+++ b/src/HOL/TLA/TLA.thy Sat May 14 22:00:24 2011 +0200
@@ -597,11 +597,11 @@
auto-tactic, which applies too much propositional logic and simplifies
too late.
*)
-fun auto_inv_tac ss =
+fun auto_inv_tac ctxt =
SELECT_GOAL
- (inv_tac (map_simpset (K ss) @{context}) 1 THEN
+ (inv_tac ctxt 1 THEN
(TRYALL (action_simp_tac
- (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
+ (simpset_of ctxt addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
*}
method_setup invariant = {*
@@ -609,8 +609,7 @@
*} ""
method_setup auto_invariant = {*
- Method.sections Clasimp.clasimp_modifiers
- >> (K (SIMPLE_METHOD' o auto_inv_tac o simpset_of))
+ Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
*} ""
lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat May 14 18:26:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat May 14 22:00:24 2011 +0200
@@ -799,8 +799,8 @@
fun clasimpset_rules_of ctxt =
let
val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> rep_cs
- val intros = safeIs @ hazIs
- val elims = map Classical.classical_rule (safeEs @ hazEs)
+ val intros = Item_Net.content safeIs @ Item_Net.content hazIs
+ val elims = map Classical.classical_rule (Item_Net.content safeEs @ Item_Net.content hazEs)
val simps = ctxt |> simpset_of |> dest_ss |> #simps
in
(mk_fact_table I I intros,
--- a/src/HOL/ex/CASC_Setup.thy Sat May 14 18:26:25 2011 +0200
+++ b/src/HOL/ex/CASC_Setup.thy Sat May 14 22:00:24 2011 +0200
@@ -38,28 +38,28 @@
*}
ML {*
-fun isabellep_tac ctxt cs ss css max_secs =
+fun isabellep_tac ctxt max_secs =
SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
ORELSE
SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
(ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac ss))
+ SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
ORELSE
- SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac cs))
+ SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac css
+ SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac ctxt []))
ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac cs))
+ SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac cs))
+ SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt))
ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac css))
+ SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt))
ORELSE
- SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac css))
+ SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt))
*}
end
--- a/src/Provers/blast.ML Sat May 14 18:26:25 2011 +0200
+++ b/src/Provers/blast.ML Sat May 14 22:00:24 2011 +0200
@@ -41,7 +41,7 @@
signature BLAST_DATA =
sig
structure Classical: CLASSICAL
- val thy: theory
+ val Trueprop_const: string * typ
val equality_name: string
val not_name: string
val notE: thm (* [| ~P; P |] ==> R *)
@@ -66,9 +66,8 @@
val setup: theory -> theory
(*debugging tools*)
type branch
- val stats: bool Unsynchronized.ref
- val trace: bool Unsynchronized.ref
- val fullTrace: branch list list Unsynchronized.ref
+ val stats: bool Config.T
+ val trace: bool Config.T
val fromType: (indexname * term) list Unsynchronized.ref -> Term.typ -> term
val fromTerm: theory -> Term.term -> term
val fromSubgoal: theory -> Term.term -> term
@@ -76,7 +75,8 @@
val toTerm: int -> term -> Term.term
val readGoal: Proof.context -> string -> term
val tryIt: Proof.context -> int -> string ->
- (int -> tactic) list * branch list list * (int * int * exn) list
+ {fullTrace: branch list list,
+ result: ((int -> tactic) list * branch list list * (int * int * exn) list)}
val normBr: branch -> branch
end;
@@ -85,8 +85,9 @@
structure Classical = Data.Classical;
-val trace = Unsynchronized.ref false
-and stats = Unsynchronized.ref false; (*for runtime and search statistics*)
+val trace = Config.bool (Config.declare "Blast.trace" (K (Config.Bool false)));
+val stats = Config.bool (Config.declare "Blast.stats" (K (Config.Bool false)));
+(*for runtime and search statistics*)
datatype term =
Const of string * term list (*typargs constant--as a terms!*)
@@ -109,7 +110,7 @@
(* global state information *)
datatype state = State of
- {thy: theory,
+ {ctxt: Proof.context,
fullTrace: branch list list Unsynchronized.ref,
trail: term option Unsynchronized.ref list Unsynchronized.ref,
ntrail: int Unsynchronized.ref,
@@ -120,16 +121,20 @@
is_some (Sign.const_type thy c) andalso
error ("blast: theory contains illegal constant " ^ quote c);
-fun initialize thy =
- (reject_const thy "*Goal*";
- reject_const thy "*False*";
- State
- {thy = thy,
- fullTrace = Unsynchronized.ref [],
- trail = Unsynchronized.ref [],
- ntrail = Unsynchronized.ref 0,
- nclosed = Unsynchronized.ref 0, (*branches closed: number of branches closed during the search*)
- ntried = Unsynchronized.ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*)
+fun initialize ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val _ = reject_const thy "*Goal*";
+ val _ = reject_const thy "*False*";
+ in
+ State
+ {ctxt = ctxt,
+ fullTrace = Unsynchronized.ref [],
+ trail = Unsynchronized.ref [],
+ ntrail = Unsynchronized.ref 0,
+ nclosed = Unsynchronized.ref 0, (*number of branches closed during the search*)
+ ntried = Unsynchronized.ref 1} (*number of branches created by splitting (counting from 1)*)
+ end;
@@ -168,8 +173,7 @@
fun isGoal (Const ("*Goal*", _) $ _) = true
| isGoal _ = false;
-val TruepropC = Object_Logic.judgment_name Data.thy;
-val TruepropT = Sign.the_const_type Data.thy TruepropC;
+val (TruepropC, TruepropT) = Data.Trueprop_const;
fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
@@ -479,33 +483,34 @@
end;
-fun TRACE rl tac st i =
- if !trace then (writeln (Display.string_of_thm_without_context rl); tac st i)
- else tac st i;
+fun TRACE ctxt rl tac i st =
+ if Config.get ctxt trace then (writeln (Display.string_of_thm ctxt rl); tac i st)
+ else tac i st;
(*Resolution/matching tactics: if upd then the proof state may be updated.
Matching makes the tactics more deterministic in the presence of Vars.*)
-fun emtac upd rl = TRACE rl (if upd then etac rl else ematch_tac [rl]);
-fun rmtac upd rl = TRACE rl (if upd then rtac rl else match_tac [rl]);
+fun emtac ctxt upd rl = TRACE ctxt rl (if upd then etac rl else ematch_tac [rl]);
+fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then rtac rl else match_tac [rl]);
(*Tableau rule from elimination rule.
Flag "upd" says that the inference updated the branch.
Flag "dup" requests duplication of the affected formula.*)
-fun fromRule thy vars rl =
- let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars
+fun fromRule ctxt vars rl =
+ let val thy = Proof_Context.theory_of ctxt
+ val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars
fun tac (upd, dup,rot) i =
- emtac upd (if dup then rev_dup_elim rl else rl) i
+ emtac ctxt upd (if dup then rev_dup_elim rl else rl) i
THEN
rot_subgoals_tac (rot, #2 trl) i
in Option.SOME (trl, tac) end
handle
ElimBadPrem => (*reject: prems don't preserve conclusion*)
- (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm_global thy rl);
+ (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl);
Option.NONE)
| ElimBadConcl => (*ignore: conclusion is not just a variable*)
- (if !trace then
+ (if Config.get ctxt trace then
(warning ("Ignoring ill-formed elimination rule:\n" ^
- "conclusion should be a variable\n" ^ Display.string_of_thm_global thy rl))
+ "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl))
else ();
Option.NONE);
@@ -525,10 +530,11 @@
Flag "dup" requests duplication of the affected formula.
Since haz rules are now delayed, "dup" is always FALSE for
introduction rules.*)
-fun fromIntrRule thy vars rl =
- let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars
+fun fromIntrRule ctxt vars rl =
+ let val thy = Proof_Context.theory_of ctxt
+ val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars
fun tac (upd,dup,rot) i =
- rmtac upd (if dup then Classical.dup_intr rl else rl) i
+ rmtac ctxt upd (if dup then Classical.dup_intr rl else rl) i
THEN
rot_subgoals_tac (rot, #2 trl) i
in (trl, tac) end;
@@ -548,16 +554,16 @@
| toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u);
-fun netMkRules thy P vars (nps: netpair list) =
+fun netMkRules ctxt P vars (nps: netpair list) =
case P of
(Const ("*Goal*", _) $ G) =>
let val pG = mk_Trueprop (toTerm 2 G)
val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
- in map (fromIntrRule thy vars o #2) (order_list intrs) end
+ in map (fromIntrRule ctxt vars o #2) (order_list intrs) end
| _ =>
let val pP = mk_Trueprop (toTerm 3 P)
val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
- in map_filter (fromRule thy vars o #2) (order_list elims) end;
+ in map_filter (fromRule ctxt vars o #2) (order_list elims) end;
(*Normalize a branch--for tracing*)
@@ -602,7 +608,7 @@
| showTerm d (f $ u) = if d=0 then dummyVar
else Term.$ (showTerm d f, showTerm (d-1) u);
-fun string_of thy d t = Syntax.string_of_term_global thy (showTerm d t);
+fun string_of ctxt d t = Syntax.string_of_term ctxt (showTerm d t);
(*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like
Ex(P) is duplicated as the assumption ~Ex(P). *)
@@ -617,23 +623,24 @@
fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;
(*Tactic. Convert *Goal* to negated assumption in FIRST position*)
-fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN
- rotate_tac ~1 i;
+fun negOfGoal_tac ctxt i =
+ TRACE ctxt Data.ccontr (rtac Data.ccontr) i THEN rotate_tac ~1 i;
-fun traceTerm thy t =
- let val t' = norm (negOfGoal t)
- val stm = string_of thy 8 t'
+fun traceTerm ctxt t =
+ let val thy = Proof_Context.theory_of ctxt
+ val t' = norm (negOfGoal t)
+ val stm = string_of ctxt 8 t'
in
case topType thy t' of
NONE => stm (*no type to attach*)
- | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ_global thy T
+ | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ ctxt T
end;
(*Print tracing information at each iteration of prover*)
-fun tracing (State {thy, fullTrace, ...}) brs =
- let fun printPairs (((G,_)::_,_)::_) = Output.tracing (traceTerm thy G)
- | printPairs (([],(H,_)::_)::_) = Output.tracing (traceTerm thy H ^ "\t (Unsafe)")
+fun tracing (State {ctxt, fullTrace, ...}) brs =
+ let fun printPairs (((G,_)::_,_)::_) = Output.tracing (traceTerm ctxt G)
+ | printPairs (([],(H,_)::_)::_) = Output.tracing (traceTerm ctxt H ^ "\t (Unsafe)")
| printPairs _ = ()
fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
(fullTrace := brs0 :: !fullTrace;
@@ -641,32 +648,31 @@
Output.tracing (" [" ^ string_of_int lim ^ "] ");
printPairs pairs;
writeln"")
- in if !trace then printBrs (map normBr brs) else ()
- end;
+ in if Config.get ctxt trace then printBrs (map normBr brs) else () end;
-fun traceMsg s = if !trace then writeln s else ();
+fun traceMsg true s = writeln s
+ | traceMsg false _ = ();
(*Tracing: variables updated in the last branch operation?*)
-fun traceVars (State {thy, ntrail, trail, ...}) ntrl =
- if !trace then
+fun traceVars (State {ctxt, ntrail, trail, ...}) ntrl =
+ if Config.get ctxt trace then
(case !ntrail-ntrl of
0 => ()
| 1 => Output.tracing "\t1 variable UPDATED:"
| n => Output.tracing ("\t" ^ string_of_int n ^ " variables UPDATED:");
(*display the instantiations themselves, though no variable names*)
- List.app (fn v => Output.tracing (" " ^ string_of thy 4 (the (!v))))
+ List.app (fn v => Output.tracing (" " ^ string_of ctxt 4 (the (!v))))
(List.take(!trail, !ntrail-ntrl));
- writeln"")
+ writeln "")
else ();
(*Tracing: how many new branches are created?*)
-fun traceNew prems =
- if !trace then
- case length prems of
- 0 => Output.tracing "branch closed by rule"
- | 1 => Output.tracing "branch extended (1 new subgoal)"
- | n => Output.tracing ("branch split: "^ string_of_int n ^ " new subgoals")
- else ();
+fun traceNew true prems =
+ (case length prems of
+ 0 => Output.tracing "branch closed by rule"
+ | 1 => Output.tracing "branch extended (1 new subgoal)"
+ | n => Output.tracing ("branch split: "^ string_of_int n ^ " new subgoals"))
+ | traceNew _ _ = ();
@@ -740,7 +746,7 @@
(*Substitute through the branch if an equality goal (else raise DEST_EQ).
Moves affected literals back into the branch, but it is not clear where
they should go: this could make proofs fail.*)
-fun equalSubst thy (G, {pairs, lits, vars, lim}) =
+fun equalSubst ctxt (G, {pairs, lits, vars, lim}) =
let val (t,u) = orientGoal(dest_eq G)
val subst = subst_atomic (t,u)
fun subst2(G,md) = (subst G, md)
@@ -763,8 +769,8 @@
end
val (changed, lits') = List.foldr subLit ([], []) lits
val (changed', pairs') = List.foldr subFrame (changed, []) pairs
- in if !trace then writeln ("Substituting " ^ traceTerm thy u ^
- " for " ^ traceTerm thy t ^ " in branch" )
+ in if Config.get ctxt trace then writeln ("Substituting " ^ traceTerm ctxt u ^
+ " for " ^ traceTerm ctxt t ^ " in branch" )
else ();
{pairs = (changed',[])::pairs', (*affected formulas, and others*)
lits = lits', (*unaffected literals*)
@@ -781,12 +787,12 @@
val contr_tac = ematch_tac [Data.notE] THEN'
(eq_assume_tac ORELSE' assume_tac);
-val eContr_tac = TRACE Data.notE contr_tac;
-val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac);
-
(*Try to unify complementary literals and return the corresponding tactic. *)
fun tryClose state (G, L) =
let
+ val State {ctxt, ...} = state;
+ val eContr_tac = TRACE ctxt Data.notE contr_tac;
+ val eAssume_tac = TRACE ctxt asm_rl (eq_assume_tac ORELSE' assume_tac);
fun close t u tac = if unify state ([], t, u) then SOME tac else NONE;
fun arg (_ $ t) = t;
in
@@ -800,7 +806,7 @@
(*Were there Skolem terms in the premise? Must NOT chase Vars*)
fun hasSkolem (Skolem _) = true
| hasSkolem (Abs (_,body)) = hasSkolem body
- | hasSkolem (f$t) = hasSkolem f orelse hasSkolem t
+ | hasSkolem (f$t) = hasSkolem f orelse hasSkolem t
| hasSkolem _ = false;
(*Attach the right "may duplicate" flag to new formulae: if they contain
@@ -826,11 +832,11 @@
next branch have been updated.*)
fun prune _ (1, nxtVars, choices) = choices (*DON'T prune at very end: allow
backtracking over bad proofs*)
- | prune (State {ntrail, trail, ...}) (nbrs: int, nxtVars, choices) =
+ | prune (State {ctxt, ntrail, trail, ...}) (nbrs: int, nxtVars, choices) =
let fun traceIt last =
let val ll = length last
and lc = length choices
- in if !trace andalso ll<lc then
+ in if Config.get ctxt trace andalso ll<lc then
(writeln("Pruning " ^ string_of_int(lc-ll) ^ " levels");
last)
else last
@@ -850,12 +856,11 @@
fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars
| nextVars [] = [];
-fun backtrack (choices as (ntrl, nbrs, exn)::_) =
- (if !trace then (writeln ("Backtracking; now there are " ^
- string_of_int nbrs ^ " branches"))
- else ();
+fun backtrack trace (choices as (ntrl, nbrs, exn)::_) =
+ (if trace then (writeln ("Backtracking; now there are " ^ string_of_int nbrs ^ " branches"))
+ else ();
raise exn)
- | backtrack _ = raise PROVE;
+ | backtrack _ _ = raise PROVE;
(*Add the literal G, handling *Goal* and detecting duplicates.*)
fun addLit (Const ("*Goal*", _) $ G, lits) =
@@ -913,14 +918,16 @@
bound on unsafe expansions.
"start" is CPU time at start, for printing search time
*)
-fun prove (state, start, ctxt, brs, cont) =
- let val State {thy, ntrail, nclosed, ntried, ...} = state;
+fun prove (state, start, brs, cont) =
+ let val State {ctxt, ntrail, nclosed, ntried, ...} = state;
+ val trace = Config.get ctxt trace;
+ val stats = Config.get ctxt stats;
val {safe0_netpair, safep_netpair, haz_netpair, ...} =
Classical.rep_cs (Classical.claset_of ctxt);
val safeList = [safe0_netpair, safep_netpair]
and hazList = [haz_netpair]
fun prv (tacs, trs, choices, []) =
- (printStats state (!trace orelse !stats, start, tacs);
+ (printStats state (trace orelse stats, start, tacs);
cont (tacs, trs, choices)) (*all branches closed!*)
| prv (tacs, trs, choices,
brs0 as {pairs = ((G,md)::br, haz)::pairs,
@@ -932,7 +939,7 @@
val nbrs = length brs0
val nxtVars = nextVars brs
val G = norm G
- val rules = netMkRules thy G vars safeList
+ val rules = netMkRules ctxt G vars safeList
(*Make a new branch, decrementing "lim" if instantiations occur*)
fun newBr (vars',lim') prems =
map (fn prem =>
@@ -965,7 +972,7 @@
val tacs' = (tac(updated,false,true))
:: tacs (*no duplication; rotate*)
in
- traceNew prems; traceVars state ntrl;
+ traceNew trace prems; traceVars state ntrl;
(if null prems then (*closed the branch: prune!*)
(nclosed := !nclosed + 1;
prv(tacs', brs0::trs,
@@ -973,7 +980,7 @@
brs))
else (*prems non-null*)
if lim'<0 (*faster to kill ALL the alternatives*)
- then (traceMsg"Excessive branching: KILLED";
+ then (traceMsg trace "Excessive branching: KILLED";
clearTo state ntrl; raise NEWBRANCHES)
else
(ntried := !ntried + length prems - 1;
@@ -985,7 +992,7 @@
Reset Vars and try another rule*)
(clearTo state ntrl; deeper grls)
else (*backtrack to previous level*)
- backtrack choices
+ backtrack trace choices
end
else deeper grls
(*Try to close branch by unifying with head goal*)
@@ -995,7 +1002,7 @@
NONE => closeF Ls
| SOME tac =>
let val choices' =
- (if !trace then (Output.tracing "branch closed";
+ (if trace then (Output.tracing "branch closed";
traceVars state ntrl)
else ();
prune state (nbrs, nxtVars,
@@ -1014,11 +1021,11 @@
handle CLOSEF => closeF (map fst haz)
handle CLOSEF => closeFl pairs
in tracing state brs0;
- if lim<0 then (traceMsg "Limit reached. "; backtrack choices)
+ if lim<0 then (traceMsg trace "Limit reached. "; backtrack trace choices)
else
- prv (Data.hyp_subst_tac (!trace) :: tacs,
+ prv (Data.hyp_subst_tac trace :: tacs,
brs0::trs, choices,
- equalSubst thy
+ equalSubst ctxt
(G, {pairs = (br,haz)::pairs,
lits = lits, vars = vars, lim = lim})
:: brs)
@@ -1026,17 +1033,17 @@
handle CLOSEF => closeFl ((br,haz)::pairs)
handle CLOSEF => deeper rules
handle NEWBRANCHES =>
- (case netMkRules thy G vars hazList of
+ (case netMkRules ctxt G vars hazList of
[] => (*there are no plausible haz rules*)
- (traceMsg "moving formula to literals";
+ (traceMsg trace "moving formula to literals";
prv (tacs, brs0::trs, choices,
{pairs = (br,haz)::pairs,
lits = addLit(G,lits),
vars = vars,
lim = lim} :: brs))
| _ => (*G admits some haz rules: try later*)
- (traceMsg "moving formula to haz list";
- prv (if isGoal G then negOfGoal_tac :: tacs
+ (traceMsg trace "moving formula to haz list";
+ prv (if isGoal G then negOfGoal_tac ctxt :: tacs
else tacs,
brs0::trs,
choices,
@@ -1060,7 +1067,7 @@
let exception PRV (*backtrack to precisely this recursion!*)
val H = norm H
val ntrl = !ntrail
- val rules = netMkRules thy H vars hazList
+ val rules = netMkRules ctxt H vars hazList
(*new premises of haz rules may NOT be duplicated*)
fun newPrem (vars,P,dup,lim') prem =
let val Gs' = map (fn Q => (Q,false)) prem
@@ -1122,14 +1129,12 @@
in
if lim'<0 andalso not (null prems)
then (*it's faster to kill ALL the alternatives*)
- (traceMsg"Excessive branching: KILLED";
+ (traceMsg trace "Excessive branching: KILLED";
clearTo state ntrl; raise NEWBRANCHES)
else
- traceNew prems;
- if !trace andalso dup then Output.tracing " (duplicating)"
- else ();
- if !trace andalso recur then Output.tracing " (recursive)"
- else ();
+ traceNew trace prems;
+ if trace andalso dup then Output.tracing " (duplicating)" else ();
+ if trace andalso recur then Output.tracing " (recursive)" else ();
traceVars state ntrl;
if null prems then nclosed := !nclosed + 1
else ntried := !ntried + length prems - 1;
@@ -1142,11 +1147,11 @@
then (*reset Vars and try another rule*)
(clearTo state ntrl; deeper grls)
else (*backtrack to previous level*)
- backtrack choices
+ backtrack trace choices
end
else deeper grls
in tracing state brs0;
- if lim<1 then (traceMsg "Limit reached. "; backtrack choices)
+ if lim<1 then (traceMsg trace "Limit reached. "; backtrack trace choices)
else deeper rules
handle NEWBRANCHES =>
(*cannot close branch: move H to literals*)
@@ -1156,7 +1161,7 @@
vars = vars,
lim = lim} :: brs)
end
- | prv (tacs, trs, choices, _ :: brs) = backtrack choices
+ | prv (tacs, trs, choices, _ :: brs) = backtrack trace choices
in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end;
@@ -1237,8 +1242,10 @@
(also prints reconstruction time)
"lim" is depth limit.*)
fun timing_depth_tac start ctxt lim i st0 =
- let val thy = Thm.theory_of_thm st0
- val state = initialize thy
+ let val thy = Proof_Context.theory_of ctxt
+ val state = initialize ctxt
+ val trace = Config.get ctxt trace;
+ val stats = Config.get ctxt stats;
val st = st0
|> rotate_prems (i - 1)
|> Conv.gconv_rule Object_Logic.atomize_prems 1
@@ -1251,16 +1258,16 @@
case Seq.pull(EVERY' (rev tacs) 1 st) of
NONE => (writeln ("PROOF FAILED for depth " ^
string_of_int lim);
- if !trace then error "************************\n"
+ if trace then error "************************\n"
else ();
- backtrack choices)
- | cell => (if (!trace orelse !stats)
+ backtrack trace choices)
+ | cell => (if (trace orelse stats)
then writeln (Timing.message (Timing.result start) ^ " for reconstruction")
else ();
Seq.make(fn()=> cell))
end
in
- prove (state, start, ctxt, [initBranch (mkGoal concl :: hyps, lim)], cont)
+ prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont)
|> Seq.map (rotate_prems (1 - i))
end
handle PROVE => Seq.empty;
@@ -1269,35 +1276,27 @@
fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st;
val (depth_limit, setup_depth_limit) =
- Attrib.config_int_global @{binding blast_depth_limit} (K 20);
+ Attrib.config_int @{binding blast_depth_limit} (K 20);
fun blast_tac ctxt i st =
- ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
- (timing_depth_tac (Timing.start ()) ctxt) 0) i
- THEN flexflex_tac) st
- handle TRANS s =>
- ((if !trace then warning ("blast: " ^ s) else ());
- Seq.empty);
+ ((DEEPEN (1, Config.get ctxt depth_limit) (timing_depth_tac (Timing.start ()) ctxt) 0) i
+ THEN flexflex_tac) st
+ handle TRANS s => (if Config.get ctxt trace then warning ("blast: " ^ s) else (); Seq.empty);
(*** For debugging: these apply the prover to a subgoal and return
the resulting tactics, trace, etc. ***)
-val fullTrace = Unsynchronized.ref ([]: branch list list);
-
(*Read a string to make an initial, singleton branch*)
fun readGoal ctxt s =
Syntax.read_prop ctxt s |> fromTerm (Proof_Context.theory_of ctxt) |> rand |> mkGoal;
fun tryIt ctxt lim s =
let
- val thy = Proof_Context.theory_of ctxt;
- val state as State {fullTrace = ft, ...} = initialize thy;
- val res = timeap prove
- (state, Timing.start (), ctxt, [initBranch ([readGoal ctxt s], lim)], I);
- val _ = fullTrace := !ft;
- in res end;
+ val state as State {fullTrace, ...} = initialize ctxt;
+ val res = timeap prove (state, Timing.start (), [initBranch ([readGoal ctxt s], lim)], I);
+ in {fullTrace = !fullTrace, result = res} end;
(** method setup **)
--- a/src/Provers/clasimp.ML Sat May 14 18:26:25 2011 +0200
+++ b/src/Provers/clasimp.ML Sat May 14 22:00:24 2011 +0200
@@ -19,7 +19,6 @@
sig
val addSss: Proof.context -> Proof.context
val addss: Proof.context -> Proof.context
- val addss': Proof.context -> Proof.context
val clarsimp_tac: Proof.context -> int -> tactic
val mk_auto_tac: Proof.context -> int -> int -> tactic
val auto_tac: Proof.context -> tactic
@@ -55,8 +54,6 @@
(*Caution: only one simpset added can be added by each of addSss and addss*)
val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" safe_asm_full_simp_tac;
val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
-(* FIXME "asm_lr_simp_tac" !? *)
-val addss' = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_lr_simp_tac;
(* iffs: addition of rules to simpsets and clasets simultaneously *)
--- a/src/Provers/classical.ML Sat May 14 18:26:25 2011 +0200
+++ b/src/Provers/classical.ML Sat May 14 22:00:24 2011 +0200
@@ -37,11 +37,12 @@
sig
type claset
val empty_cs: claset
+ val merge_cs: claset * claset -> claset
val rep_cs: claset ->
- {safeIs: thm list,
- safeEs: thm list,
- hazIs: thm list,
- hazEs: thm list,
+ {safeIs: thm Item_Net.T,
+ safeEs: thm Item_Net.T,
+ hazIs: thm Item_Net.T,
+ hazEs: thm Item_Net.T,
swrappers: (string * (Proof.context -> wrapper)) list,
uwrappers: (string * (Proof.context -> wrapper)) list,
safe0_netpair: netpair,
@@ -131,7 +132,7 @@
end;
-functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =
+functor Classical(Data: CLASSICAL_DATA): CLASSICAL =
struct
(** classical elimination rules **)
@@ -214,10 +215,10 @@
datatype claset =
CS of
- {safeIs : thm list, (*safe introduction rules*)
- safeEs : thm list, (*safe elimination rules*)
- hazIs : thm list, (*unsafe introduction rules*)
- hazEs : thm list, (*unsafe elimination rules*)
+ {safeIs : thm Item_Net.T, (*safe introduction rules*)
+ safeEs : thm Item_Net.T, (*safe elimination rules*)
+ hazIs : thm Item_Net.T, (*unsafe introduction rules*)
+ hazEs : thm Item_Net.T, (*unsafe elimination rules*)
swrappers : (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*)
uwrappers : (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*)
safe0_netpair : netpair, (*nets for trivial cases*)
@@ -244,10 +245,10 @@
val empty_cs =
CS
- {safeIs = [],
- safeEs = [],
- hazIs = [],
- hazEs = [],
+ {safeIs = Thm.full_rules,
+ safeEs = Thm.full_rules,
+ hazIs = Thm.full_rules,
+ hazEs = Thm.full_rules,
swrappers = [],
uwrappers = [],
safe0_netpair = empty_netpair,
@@ -294,9 +295,6 @@
fun delete x = delete_tagged_list (joinrules x);
fun delete' x = delete_tagged_list (joinrules' x);
-val mem_thm = member Thm.eq_thm_prop
-and rem_thm = remove Thm.eq_thm_prop;
-
fun string_of_thm NONE = Display.string_of_thm_without_context
| string_of_thm (SOME context) =
Display.string_of_thm (Context.cases Syntax.init_pretty_global I context);
@@ -306,14 +304,19 @@
error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
else Tactic.make_elim th;
-fun warn context msg rules th =
- mem_thm rules th andalso (warning (msg ^ string_of_thm context th); true);
+fun warn_thm context msg th =
+ if (case context of SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt | _ => false)
+ then warning (msg ^ string_of_thm context th)
+ else ();
-fun warn_other context th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
- warn context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
- warn context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
- warn context "Rule already declared as introduction (intro)\n" hazIs th orelse
- warn context "Rule already declared as elimination (elim)\n" hazEs th;
+fun warn_rules context msg rules th =
+ Item_Net.member rules th andalso (warn_thm context msg th; true);
+
+fun warn_claset context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
+ warn_rules context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
+ warn_rules context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
+ warn_rules context "Rule already declared as introduction (intro)\n" hazIs th orelse
+ warn_rules context "Rule already declared as elimination (elim)\n" hazEs th;
(*** Safe rules ***)
@@ -321,18 +324,18 @@
fun addSI w context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if warn context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
+ if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
else
let
val th' = flat_rule th;
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
List.partition Thm.no_prems [th'];
- val nI = length safeIs + 1;
- val nE = length safeEs;
- val _ = warn_other context th cs;
+ val nI = Item_Net.length safeIs + 1;
+ val nE = Item_Net.length safeEs;
+ val _ = warn_claset context th cs;
in
CS
- {safeIs = th::safeIs,
+ {safeIs = Item_Net.update th safeIs,
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
safeEs = safeEs,
@@ -348,7 +351,7 @@
fun addSE w context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if warn context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
+ if warn_rules context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
else if has_fewer_prems 1 th then
error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
else
@@ -356,12 +359,12 @@
val th' = classical_rule (flat_rule th);
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
List.partition (fn rl => nprems_of rl=1) [th'];
- val nI = length safeIs;
- val nE = length safeEs + 1;
- val _ = warn_other context th cs;
+ val nI = Item_Net.length safeIs;
+ val nE = Item_Net.length safeEs + 1;
+ val _ = warn_claset context th cs;
in
CS
- {safeEs = th::safeEs,
+ {safeEs = Item_Net.update th safeEs,
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
safeIs = safeIs,
@@ -382,16 +385,16 @@
fun addI w context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if warn context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
+ if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
else
let
val th' = flat_rule th;
- val nI = length hazIs + 1;
- val nE = length hazEs;
- val _ = warn_other context th cs;
+ val nI = Item_Net.length hazIs + 1;
+ val nE = Item_Net.length hazEs;
+ val _ = warn_claset context th cs;
in
CS
- {hazIs = th :: hazIs,
+ {hazIs = Item_Net.update th hazIs,
haz_netpair = insert (nI, nE) ([th'], []) haz_netpair,
dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair,
safeIs = safeIs,
@@ -409,18 +412,18 @@
fun addE w context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if warn context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
+ if warn_rules context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
else if has_fewer_prems 1 th then
error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
else
let
val th' = classical_rule (flat_rule th);
- val nI = length hazIs;
- val nE = length hazEs + 1;
- val _ = warn_other context th cs;
+ val nI = Item_Net.length hazIs;
+ val nE = Item_Net.length hazEs + 1;
+ val _ = warn_claset context th cs;
in
CS
- {hazEs = th :: hazEs,
+ {hazEs = Item_Net.update th hazEs,
haz_netpair = insert (nI, nE) ([], [th']) haz_netpair,
dup_netpair = insert (nI, nE) ([], [dup_elim th']) dup_netpair,
safeIs = safeIs,
@@ -445,7 +448,7 @@
fun delSI th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if mem_thm safeIs th then
+ if Item_Net.member safeIs th then
let
val th' = flat_rule th;
val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
@@ -453,7 +456,7 @@
CS
{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
safep_netpair = delete (safep_rls, []) safep_netpair,
- safeIs = rem_thm th safeIs,
+ safeIs = Item_Net.remove th safeIs,
safeEs = safeEs,
hazIs = hazIs,
hazEs = hazEs,
@@ -468,7 +471,7 @@
fun delSE th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if mem_thm safeEs th then
+ if Item_Net.member safeEs th then
let
val th' = classical_rule (flat_rule th);
val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th'];
@@ -477,7 +480,7 @@
{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
safep_netpair = delete ([], safep_rls) safep_netpair,
safeIs = safeIs,
- safeEs = rem_thm th safeEs,
+ safeEs = Item_Net.remove th safeEs,
hazIs = hazIs,
hazEs = hazEs,
swrappers = swrappers,
@@ -491,14 +494,14 @@
fun delI context th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if mem_thm hazIs th then
+ if Item_Net.member hazIs th then
let val th' = flat_rule th in
CS
{haz_netpair = delete ([th'], []) haz_netpair,
dup_netpair = delete ([dup_intr th'], []) dup_netpair,
safeIs = safeIs,
safeEs = safeEs,
- hazIs = rem_thm th hazIs,
+ hazIs = Item_Net.remove th hazIs,
hazEs = hazEs,
swrappers = swrappers,
uwrappers = uwrappers,
@@ -513,7 +516,7 @@
fun delE th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
- if mem_thm hazEs th then
+ if Item_Net.member hazEs th then
let val th' = classical_rule (flat_rule th) in
CS
{haz_netpair = delete ([], [th']) haz_netpair,
@@ -521,7 +524,7 @@
safeIs = safeIs,
safeEs = safeEs,
hazIs = hazIs,
- hazEs = rem_thm th hazEs,
+ hazEs = Item_Net.remove th hazEs,
swrappers = swrappers,
uwrappers = uwrappers,
safe0_netpair = safe0_netpair,
@@ -533,11 +536,11 @@
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
let val th' = Tactic.make_elim th in
- if mem_thm safeIs th orelse mem_thm safeEs th orelse
- mem_thm hazIs th orelse mem_thm hazEs th orelse
- mem_thm safeEs th' orelse mem_thm hazEs th'
+ if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse
+ Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse
+ Item_Net.member safeEs th' orelse Item_Net.member hazEs th'
then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
- else (warning ("Undeclared classical rule\n" ^ string_of_thm context th); cs)
+ else (warn_thm context "Undeclared classical rule\n" th; cs)
end;
@@ -565,28 +568,24 @@
(* merge_cs *)
-(*Merge works by adding all new rules of the 2nd claset into the 1st claset.
- Merging the term nets may look more efficient, but the rather delicate
- treatment of priority might get muddled up.*)
+(*Merge works by adding all new rules of the 2nd claset into the 1st claset,
+ in order to preserve priorities reliably.*)
+
+fun merge_thms add thms1 thms2 =
+ fold_rev (fn thm => if Item_Net.member thms1 thm then I else add thm) (Item_Net.content thms2);
+
fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...},
cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
swrappers, uwrappers, ...}) =
if pointer_eq (cs, cs') then cs
else
- let
- val safeIs' = fold rem_thm safeIs safeIs2;
- val safeEs' = fold rem_thm safeEs safeEs2;
- val hazIs' = fold rem_thm hazIs hazIs2;
- val hazEs' = fold rem_thm hazEs hazEs2;
- in
- cs
- |> fold_rev (addSI NONE NONE) safeIs'
- |> fold_rev (addSE NONE NONE) safeEs'
- |> fold_rev (addI NONE NONE) hazIs'
- |> fold_rev (addE NONE NONE) hazEs'
- |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers))
- |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers))
- end;
+ cs
+ |> merge_thms (addSI NONE NONE) safeIs safeIs2
+ |> merge_thms (addSE NONE NONE) safeEs safeEs2
+ |> merge_thms (addI NONE NONE) hazIs hazIs2
+ |> merge_thms (addE NONE NONE) hazEs hazEs2
+ |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers))
+ |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers));
(* data *)
@@ -612,7 +611,7 @@
fun print_claset ctxt =
let
val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
- val pretty_thms = map (Display.pretty_thm ctxt);
+ val pretty_thms = map (Display.pretty_thm ctxt) o Item_Net.content;
in
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
--- a/src/Provers/hypsubst.ML Sat May 14 18:26:25 2011 +0200
+++ b/src/Provers/hypsubst.ML Sat May 14 22:00:24 2011 +0200
@@ -53,7 +53,7 @@
val hypsubst_setup : theory -> theory
end;
-functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
+functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
struct
exception EQ_VAR;
--- a/src/Pure/Isar/attrib.ML Sat May 14 18:26:25 2011 +0200
+++ b/src/Pure/Isar/attrib.ML Sat May 14 22:00:24 2011 +0200
@@ -44,14 +44,6 @@
(Context.generic -> real) -> real Config.T * (theory -> theory)
val config_string: Binding.binding ->
(Context.generic -> string) -> string Config.T * (theory -> theory)
- val config_bool_global: Binding.binding ->
- (Context.generic -> bool) -> bool Config.T * (theory -> theory)
- val config_int_global: Binding.binding ->
- (Context.generic -> int) -> int Config.T * (theory -> theory)
- val config_real_global: Binding.binding ->
- (Context.generic -> real) -> real Config.T * (theory -> theory)
- val config_string_global: Binding.binding ->
- (Context.generic -> string) -> string Config.T * (theory -> theory)
val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T
val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
@@ -384,24 +376,19 @@
|> Configs.map (Symtab.update (name, config))
end;
-fun declare make coerce global binding default =
+fun declare make coerce binding default =
let
val name = Binding.name_of binding;
- val config_value = Config.declare_generic {global = global} name (make o default);
+ val config_value = Config.declare_generic {global = false} name (make o default);
val config = coerce config_value;
in (config, register binding config_value) end;
in
-val config_bool = declare Config.Bool Config.bool false;
-val config_int = declare Config.Int Config.int false;
-val config_real = declare Config.Real Config.real false;
-val config_string = declare Config.String Config.string false;
-
-val config_bool_global = declare Config.Bool Config.bool true;
-val config_int_global = declare Config.Int Config.int true;
-val config_real_global = declare Config.Real Config.real true;
-val config_string_global = declare Config.String Config.string true;
+val config_bool = declare Config.Bool Config.bool;
+val config_int = declare Config.Int Config.int;
+val config_real = declare Config.Real Config.real;
+val config_string = declare Config.String Config.string;
fun register_config config = register (Binding.name (Config.name_of config)) config;
--- a/src/Pure/Isar/rule_insts.ML Sat May 14 18:26:25 2011 +0200
+++ b/src/Pure/Isar/rule_insts.ML Sat May 14 22:00:24 2011 +0200
@@ -26,7 +26,7 @@
val make_elim_preserve: thm -> thm
end;
-structure RuleInsts: RULE_INSTS =
+structure Rule_Insts: RULE_INSTS =
struct
(** reading instantiations **)
@@ -422,5 +422,5 @@
end;
-structure Basic_Rule_Insts: BASIC_RULE_INSTS = RuleInsts;
+structure Basic_Rule_Insts: BASIC_RULE_INSTS = Rule_Insts;
open Basic_Rule_Insts;
--- a/src/Pure/item_net.ML Sat May 14 18:26:25 2011 +0200
+++ b/src/Pure/item_net.ML Sat May 14 22:00:24 2011 +0200
@@ -10,6 +10,7 @@
type 'a T
val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
val content: 'a T -> 'a list
+ val length: 'a T -> int
val retrieve: 'a T -> term -> 'a list
val member: 'a T -> 'a -> bool
val merge: 'a T * 'a T -> 'a T
@@ -36,6 +37,7 @@
fun init eq index = mk_items eq index [] ~1 Net.empty;
fun content (Items {content, ...}) = content;
+fun length items = List.length (content items);
fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;