# HG changeset patch # User wenzelm # Date 1305403224 -7200 # Node ID c5146d5fc54c15df4cc4a256024b9d82edc5e3bc # Parent 5b45125b15bad5edaf02d456cf19e60d8613606d# Parent 2425068fe13ac9808ad2f1211b757c36b1e5ca55 merged diff -r 5b45125b15ba -r c5146d5fc54c src/FOL/FOL.thy --- 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} diff -r 5b45125b15ba -r c5146d5fc54c src/FOL/IFOL.thy --- 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" diff -r 5b45125b15ba -r c5146d5fc54c src/FOL/IsaMakefile --- 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 diff -r 5b45125b15ba -r c5146d5fc54c src/FOL/hypsubstdata.ML --- 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; diff -r 5b45125b15ba -r c5146d5fc54c src/FOLP/FOLP.thy --- 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 diff -r 5b45125b15ba -r c5146d5fc54c src/FOLP/IFOLP.thy --- 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; *} diff -r 5b45125b15ba -r c5146d5fc54c src/FOLP/classical.ML --- 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 diff -r 5b45125b15ba -r c5146d5fc54c src/FOLP/hypsubst.ML --- 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 diff -r 5b45125b15ba -r c5146d5fc54c src/HOL/HOL.thy --- 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 @@ "\X. \ x=x; PROP W \ \ 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} diff -r 5b45125b15ba -r c5146d5fc54c src/HOL/Nominal/nominal_fresh_fun.ML --- 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 _ => diff -r 5b45125b15ba -r c5146d5fc54c src/HOL/TLA/TLA.thy --- 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" diff -r 5b45125b15ba -r c5146d5fc54c src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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, diff -r 5b45125b15ba -r c5146d5fc54c src/HOL/ex/CASC_Setup.thy --- 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 diff -r 5b45125b15ba -r c5146d5fc54c src/Provers/blast.ML --- 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 @@ -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 **) diff -r 5b45125b15ba -r c5146d5fc54c src/Provers/clasimp.ML --- 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 *) diff -r 5b45125b15ba -r c5146d5fc54c src/Provers/classical.ML --- 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), diff -r 5b45125b15ba -r c5146d5fc54c src/Provers/hypsubst.ML --- 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; diff -r 5b45125b15ba -r c5146d5fc54c src/Pure/Isar/attrib.ML --- 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; diff -r 5b45125b15ba -r c5146d5fc54c src/Pure/Isar/rule_insts.ML --- 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; diff -r 5b45125b15ba -r c5146d5fc54c src/Pure/item_net.ML --- 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;