# HG changeset patch # User wenzelm # Date 1248888982 -7200 # Node ID b10cbf4d3f55239ee80c5bef7123a628cd393300 # Parent e7f275d203bc414898e1e87fd132e465903484bd# Parent 73cd8f74cf2a89b256c1db0cccaecc9fd688ce2c merged diff -r e7f275d203bc -r b10cbf4d3f55 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Wed Jul 29 16:43:02 2009 +0200 +++ b/src/FOL/FOL.thy Wed Jul 29 19:36:22 2009 +0200 @@ -168,7 +168,7 @@ use "cladata.ML" setup Cla.setup -setup cla_setup +ML {* Context.>> (Cla.map_cs (K FOL_cs)) *} ML {* structure Blast = Blast diff -r e7f275d203bc -r b10cbf4d3f55 src/FOL/cladata.ML --- a/src/FOL/cladata.ML Wed Jul 29 16:43:02 2009 +0200 +++ b/src/FOL/cladata.ML Wed Jul 29 19:36:22 2009 +0200 @@ -32,4 +32,3 @@ val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}] addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}]; -val cla_setup = Cla.map_claset (K FOL_cs); diff -r e7f275d203bc -r b10cbf4d3f55 src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Wed Jul 29 16:43:02 2009 +0200 +++ b/src/HOL/Prolog/prolog.ML Wed Jul 29 19:36:22 2009 +0200 @@ -67,8 +67,8 @@ imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *) imp_all]; (* "((!x. D) :- G) = (!x. D :- G)" *) -(*val hyp_resolve_tac = METAHYPS (fn prems => - resolve_tac (List.concat (map atomizeD prems)) 1); +(*val hyp_resolve_tac = FOCUS (fn {prems, ...} => + resolve_tac (maps atomizeD prems) 1); -- is nice, but cannot instantiate unknowns in the assumptions *) fun hyp_resolve_tac i st = let fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t)) diff -r e7f275d203bc -r b10cbf4d3f55 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Wed Jul 29 16:43:02 2009 +0200 +++ b/src/HOL/Tools/meson.ML Wed Jul 29 19:36:22 2009 +0200 @@ -14,30 +14,29 @@ val too_many_clauses: Proof.context option -> term -> bool val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context val finish_cnf: thm list -> thm list - val make_nnf: thm -> thm - val skolemize: thm -> thm + val make_nnf: Proof.context -> thm -> thm + val skolemize: Proof.context -> thm -> thm val is_fol_term: theory -> term -> bool val make_clauses: thm list -> thm list val make_horns: thm list -> thm list val best_prolog_tac: (thm -> int) -> thm list -> tactic val depth_prolog_tac: thm list -> tactic val gocls: thm list -> thm list - val skolemize_prems_tac: thm list -> int -> tactic - val MESON: (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic - val best_meson_tac: (thm -> int) -> int -> tactic - val safe_best_meson_tac: claset -> int -> tactic - val depth_meson_tac: int -> tactic + val skolemize_prems_tac: Proof.context -> thm list -> int -> tactic + val MESON: (thm list -> thm list) -> (thm list -> tactic) -> Proof.context -> int -> tactic + val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic + val safe_best_meson_tac: Proof.context -> int -> tactic + val depth_meson_tac: Proof.context -> int -> tactic val prolog_step_tac': thm list -> int -> tactic val iter_deepen_prolog_tac: thm list -> tactic - val iter_deepen_meson_tac: thm list -> int -> tactic + val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic val make_meta_clause: thm -> thm val make_meta_clauses: thm list -> thm list - val meson_claset_tac: thm list -> claset -> int -> tactic - val meson_tac: claset -> int -> tactic + val meson_tac: Proof.context -> thm list -> int -> tactic val negate_head: thm -> thm val select_literal: int -> thm -> thm - val skolemize_tac: int -> tactic - val setup: Context.theory -> Context.theory + val skolemize_tac: Proof.context -> int -> tactic + val setup: theory -> theory end structure Meson: MESON = @@ -89,13 +88,16 @@ (*FIXME: currently does not "rename variables apart"*) fun first_order_resolve thA thB = - let val thy = theory_of_thm thA - val tmA = concl_of thA - val Const("==>",_) $ tmB $ _ = prop_of thB - val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty) - val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) - in thA RS (cterm_instantiate ct_pairs thB) end - handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); (* FIXME avoid handle _ *) + (case + try (fn () => + let val thy = theory_of_thm thA + val tmA = concl_of thA + val Const("==>",_) $ tmB $ _ = prop_of thB + val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty) + val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) + in thA RS (cterm_instantiate ct_pairs thB) end) () of + SOME th => th + | NONE => raise THM ("first_order_resolve", 0, [thA, thB])); fun flexflex_first_order th = case (tpairs_of th) of @@ -124,13 +126,13 @@ e.g. from conj_forward, should have the form "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q" and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*) -fun forward_res nf st = +fun forward_res ctxt nf st = let fun forward_tacf [prem] = rtac (nf prem) 1 | forward_tacf prems = error (cat_lines ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" :: - Display.string_of_thm_without_context st :: - "Premises:" :: map Display.string_of_thm_without_context prems)) + Display.string_of_thm ctxt st :: + "Premises:" :: map (Display.string_of_thm ctxt) prems)) in case Seq.pull (ALLGOALS (OldGoals.METAHYPS forward_tacf) st) of SOME(th,_) => th @@ -223,7 +225,7 @@ (*** Removal of duplicate literals ***) (*Forward proof, passing extra assumptions as theorems to the tactic*) -fun forward_res2 nf hyps st = +fun forward_res2 ctxt nf hyps st = case Seq.pull (REPEAT (OldGoals.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) @@ -233,16 +235,16 @@ (*Remove duplicates in P|Q by assuming ~P in Q rls (initially []) accumulates assumptions of the form P==>False*) -fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc) +fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc) handle THM _ => tryres(th,rls) - handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2), + handle THM _ => tryres(forward_res2 ctxt (nodups_aux ctxt) rls (th RS disj_forward2), [disj_FalseD1, disj_FalseD2, asm_rl]) handle THM _ => th; (*Remove duplicate literals, if there are any*) -fun nodups th = +fun nodups ctxt th = if has_duplicates (op =) (literals (prop_of th)) - then nodups_aux [] th + then nodups_aux ctxt [] th else th; @@ -321,7 +323,7 @@ fun cnf_aux (th,ths) = if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*) else if not (has_conns ["All","Ex","op &"] (prop_of th)) - then nodups th :: ths (*no work to do, terminate*) + then nodups ctxt th :: ths (*no work to do, terminate*) else case head_of (HOLogic.dest_Trueprop (concl_of th)) of Const ("op &", _) => (*conjunction*) cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) @@ -335,10 +337,10 @@ (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using all combinations of converting P, Q to CNF.*) let val tac = - (OldGoals.METAHYPS (resop cnf_nil) 1) THEN + OldGoals.METAHYPS (resop cnf_nil) 1 THEN (fn st' => st' |> OldGoals.METAHYPS (resop cnf_nil) 1) in Seq.list_of (tac (th RS disj_forward)) @ ths end - | _ => nodups th :: ths (*no work to do*) + | _ => nodups ctxt th :: ths (*no work to do*) and cnf_nil th = cnf_aux (th,[]) val cls = if too_many_clauses (SOME ctxt) (concl_of th) @@ -499,11 +501,11 @@ | ok4nnf (Const ("Trueprop",_) $ t) = rigid t | ok4nnf _ = false; -fun make_nnf1 th = +fun make_nnf1 ctxt th = if ok4nnf (concl_of th) - then make_nnf1 (tryres(th, nnf_rls)) + then make_nnf1 ctxt (tryres(th, nnf_rls)) handle THM ("tryres", _, _) => - forward_res make_nnf1 + forward_res ctxt (make_nnf1 ctxt) (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) handle THM ("tryres", _, _) => th else th; @@ -521,32 +523,32 @@ HOL_basic_ss addsimps nnf_extra_simps addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; -fun make_nnf th = case prems_of th of +fun make_nnf ctxt th = case prems_of th of [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps) |> simplify nnf_ss - |> make_nnf1 + |> make_nnf1 ctxt | _ => raise THM ("make_nnf: premises in argument", 0, [th]); (*Pull existential quantifiers to front. This accomplishes Skolemization for clauses that arise from a subgoal.*) -fun skolemize1 th = +fun skolemize1 ctxt th = if not (has_conns ["Ex"] (prop_of th)) then th - else (skolemize1 (tryres(th, [choice, conj_exD1, conj_exD2, + else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2]))) handle THM ("tryres", _, _) => - skolemize1 (forward_res skolemize1 + skolemize1 ctxt (forward_res ctxt (skolemize1 ctxt) (tryres (th, [conj_forward, disj_forward, all_forward]))) handle THM ("tryres", _, _) => - forward_res skolemize1 (rename_bvs_RS th ex_forward); + forward_res ctxt (skolemize1 ctxt) (rename_bvs_RS th ex_forward); -fun skolemize th = skolemize1 (make_nnf th); +fun skolemize ctxt th = skolemize1 ctxt (make_nnf ctxt th); -fun skolemize_nnf_list [] = [] - | skolemize_nnf_list (th::ths) = - skolemize th :: skolemize_nnf_list ths +fun skolemize_nnf_list _ [] = [] + | skolemize_nnf_list ctxt (th::ths) = + skolemize ctxt th :: skolemize_nnf_list ctxt ths handle THM _ => (*RS can fail if Unify.search_bound is too small*) - (warning ("Failed to Skolemize " ^ Display.string_of_thm_without_context th); - skolemize_nnf_list ths); + (warning ("Failed to Skolemize " ^ Display.string_of_thm ctxt th); + skolemize_nnf_list ctxt ths); fun add_clauses (th,cls) = let val ctxt0 = Variable.thm_context th @@ -574,19 +576,19 @@ (*Return all negative clauses, as possible goal clauses*) fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); -fun skolemize_prems_tac prems = - cut_facts_tac (skolemize_nnf_list prems) THEN' +fun skolemize_prems_tac ctxt prems = + cut_facts_tac (skolemize_nnf_list ctxt prems) THEN' REPEAT o (etac exE); (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. Function mkcl converts theorems to clauses.*) -fun MESON mkcl cltac i st = +fun MESON mkcl cltac ctxt i st = SELECT_GOAL (EVERY [ObjectLogic.atomize_prems_tac 1, rtac ccontr 1, - OldGoals.METAHYPS (fn negs => - EVERY1 [skolemize_prems_tac negs, - OldGoals.METAHYPS (cltac o mkcl)]) 1]) i st + FOCUS (fn {context = ctxt', prems = negs, ...} => + EVERY1 [skolemize_prems_tac ctxt negs, + FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) (** Best-first search versions **) @@ -600,9 +602,9 @@ (prolog_step_tac (make_horns cls) 1)); (*First, breaks the goal into independent units*) -fun safe_best_meson_tac cs = - SELECT_GOAL (TRY (safe_tac cs) THEN - TRYALL (best_meson_tac size_of_subgoals)); +fun safe_best_meson_tac ctxt = + SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN + TRYALL (best_meson_tac size_of_subgoals ctxt)); (** Depth-first search version **) @@ -627,7 +629,7 @@ fun iter_deepen_prolog_tac horns = ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns); -fun iter_deepen_meson_tac ths = MESON make_clauses +fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses (fn cls => (case (gocls (cls @ ths)) of [] => no_tac (*no goal clauses*) @@ -636,14 +638,12 @@ val horns = make_horns (cls @ ths) val _ = Output.debug (fn () => cat_lines ("meson method called:" :: - map Display.string_of_thm_without_context (cls @ ths) @ - ["clauses:"] @ map Display.string_of_thm_without_context horns)) + map (Display.string_of_thm ctxt) (cls @ ths) @ + ["clauses:"] @ map (Display.string_of_thm ctxt) horns)) in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end)); -fun meson_claset_tac ths cs = - SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths)); - -val meson_tac = meson_claset_tac []; +fun meson_tac ctxt ths = + SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths)); (**** Code to support ordinary resolution, rather than Model Elimination ****) @@ -695,14 +695,14 @@ leaving !!-quantified variables. Perhaps Safe_tac should follow, but it might generate many subgoals.*) -fun skolemize_tac i st = - let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1)) +fun skolemize_tac ctxt = SUBGOAL (fn (goal, i) => + let val ts = Logic.strip_assums_hyp goal in - EVERY' [OldGoals.METAHYPS - (fn hyps => (cut_facts_tac (skolemize_nnf_list hyps) 1 - THEN REPEAT (etac exE 1))), - REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st - end - handle Subscript => Seq.empty; + EVERY' + [OldGoals.METAHYPS (fn hyps => + (cut_facts_tac (skolemize_nnf_list ctxt hyps) 1 + THEN REPEAT (etac exE 1))), + REPEAT_DETERM_N (length ts) o (etac thin_rl)] i + end); end; diff -r e7f275d203bc -r b10cbf4d3f55 src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Wed Jul 29 16:43:02 2009 +0200 +++ b/src/HOL/Tools/metis_tools.ML Wed Jul 29 19:36:22 2009 +0200 @@ -628,7 +628,8 @@ if exists_type ResAxioms.type_has_empty_sort (prop_of st0) then (warning "Proof state contains the empty sort"; Seq.empty) else - (Meson.MESON ResAxioms.neg_clausify (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) i + (Meson.MESON ResAxioms.neg_clausify + (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i THEN ResAxioms.expand_defs_tac st0) st0 end handle METIS s => (warning ("Metis: " ^ s); Seq.empty); diff -r e7f275d203bc -r b10cbf4d3f55 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Wed Jul 29 16:43:02 2009 +0200 +++ b/src/HOL/Tools/res_axioms.ML Wed Jul 29 19:36:22 2009 +0200 @@ -270,8 +270,10 @@ (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*) fun to_nnf th ctxt0 = let val th1 = th |> transform_elim |> zero_var_indexes - val ((_,[th2]),ctxt) = Variable.import true [th1] ctxt0 - val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1 + val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 + val th3 = th2 + |> Conv.fconv_rule ObjectLogic.atomize + |> Meson.make_nnf ctxt |> strip_lambdas ~1 in (th3, ctxt) end; (*Generate Skolem functions for a theorem supplied in nnf*) @@ -483,33 +485,35 @@ in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end; -fun meson_general_tac ths i st0 = +fun meson_general_tac ctxt ths i st0 = let - val thy = Thm.theory_of_thm st0 - in (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end; + val thy = ProofContext.theory_of ctxt + val ctxt0 = Classical.put_claset HOL_cs ctxt + in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end; val meson_method_setup = - Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn _ => - SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths))) + Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => + SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) "MESON resolution proof procedure"; (*** Converting a subgoal into negated conjecture clauses. ***) -val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac]; +fun neg_skolemize_tac ctxt = + EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac ctxt]; val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf; fun neg_conjecture_clauses ctxt st0 n = let - val st = Seq.hd (neg_skolemize_tac n st0) + val st = Seq.hd (neg_skolemize_tac ctxt n st0) val ({params, prems, ...}, _) = Subgoal.focus (Variable.set_body false ctxt) n st in (neg_clausify prems, map (Term.dest_Free o Thm.term_of o #2) params) end; (*Conversion of a subgoal to conjecture clauses. Each clause has leading !!-bound universal variables, to express generality. *) fun neg_clausify_tac ctxt = - neg_skolemize_tac THEN' + neg_skolemize_tac ctxt THEN' SUBGOAL (fn (prop, i) => let val ts = Logic.strip_assums_hyp prop in EVERY' diff -r e7f275d203bc -r b10cbf4d3f55 src/HOL/ex/Classical.thy --- a/src/HOL/ex/Classical.thy Wed Jul 29 16:43:02 2009 +0200 +++ b/src/HOL/ex/Classical.thy Wed Jul 29 19:36:22 2009 +0200 @@ -429,7 +429,7 @@ lemma "(\x y z. R(x,y) & R(y,z) --> R(x,z)) & (\x. \y. R(x,y)) --> ~ (\x. P x = (\y. R(x,y) --> ~ P y))" -by (tactic{*Meson.safe_best_meson_tac @{claset} 1*}) +by (tactic{*Meson.safe_best_meson_tac @{context} 1*}) --{*In contrast, @{text meson} is SLOW: 7.6s on griffon*} @@ -723,7 +723,7 @@ (\x y. bird x & snail y \ ~eats x y) & (\x. (caterpillar x \ snail x) \ (\y. plant y & eats x y)) \ (\x y. animal x & animal y & (\z. grain z & eats y z & eats x y))" -by (tactic{*Meson.safe_best_meson_tac @{claset} 1*}) +by (tactic{*Meson.safe_best_meson_tac @{context} 1*}) --{*Nearly twice as fast as @{text meson}, which performs iterative deepening rather than best-first search*} diff -r e7f275d203bc -r b10cbf4d3f55 src/HOL/ex/Meson_Test.thy --- a/src/HOL/ex/Meson_Test.thy Wed Jul 29 16:43:02 2009 +0200 +++ b/src/HOL/ex/Meson_Test.thy Wed Jul 29 19:36:22 2009 +0200 @@ -31,8 +31,8 @@ Goal "(\x. P x) & (\x. L x --> ~ (M x & R x)) & (\x. P x --> (M x & L x)) & ((\x. P x --> Q x) | (\x. P x & R x)) --> (\x. Q x & P x)"; by (rtac ccontr 1); val [prem25] = gethyps 1; -val nnf25 = Meson.make_nnf prem25; -val xsko25 = Meson.skolemize nnf25; +val nnf25 = Meson.make_nnf @{context} prem25; +val xsko25 = Meson.skolemize @{context} nnf25; by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1)); val [_,sko25] = gethyps 1; val clauses25 = Meson.make_clauses [sko25]; (*7 clauses*) @@ -51,8 +51,8 @@ Goal "((\x. p x) = (\x. q x)) & (\x. \y. p x & q y --> (r x = s y)) --> ((\x. p x --> r x) = (\x. q x --> s x))"; by (rtac ccontr 1); val [prem26] = gethyps 1; -val nnf26 = Meson.make_nnf prem26; -val xsko26 = Meson.skolemize nnf26; +val nnf26 = Meson.make_nnf @{context} prem26; +val xsko26 = Meson.skolemize @{context} nnf26; by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1)); val [_,sko26] = gethyps 1; val clauses26 = Meson.make_clauses [sko26]; (*9 clauses*) @@ -72,8 +72,8 @@ Goal "(\x. \y. q x y = (\z. p z x = (p z y::bool))) --> (\x. (\y. q x y = (q y x::bool)))"; by (rtac ccontr 1); val [prem43] = gethyps 1; -val nnf43 = Meson.make_nnf prem43; -val xsko43 = Meson.skolemize nnf43; +val nnf43 = Meson.make_nnf @{context} prem43; +val xsko43 = Meson.skolemize @{context} nnf43; by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1)); val [_,sko43] = gethyps 1; val clauses43 = Meson.make_clauses [sko43]; (*6*) diff -r e7f275d203bc -r b10cbf4d3f55 src/Provers/classical.ML --- a/src/Provers/classical.ML Wed Jul 29 16:43:02 2009 +0200 +++ b/src/Provers/classical.ML Wed Jul 29 19:36:22 2009 +0200 @@ -113,8 +113,8 @@ val del_context_safe_wrapper: string -> theory -> theory val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory val del_context_unsafe_wrapper: string -> theory -> theory - val get_claset: theory -> claset - val map_claset: (claset -> claset) -> theory -> theory + val get_claset: Proof.context -> claset + val put_claset: claset -> Proof.context -> Proof.context val get_cs: Context.generic -> claset val map_cs: (claset -> claset) -> Context.generic -> Context.generic val safe_dest: int option -> attribute @@ -845,8 +845,8 @@ (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2)); ); -val get_claset = #1 o GlobalClaset.get; -val map_claset = GlobalClaset.map o apfst; +val get_global_claset = #1 o GlobalClaset.get; +val map_global_claset = GlobalClaset.map o apfst; val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of; fun map_context_cs f = GlobalClaset.map (apsnd @@ -871,9 +871,12 @@ structure LocalClaset = ProofDataFun ( type T = claset; - val init = get_claset; + val init = get_global_claset; ); +val get_claset = LocalClaset.get; +val put_claset = LocalClaset.put; + fun claset_of ctxt = context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt); @@ -881,13 +884,13 @@ (* generic clasets *) val get_cs = Context.cases global_claset_of claset_of; -fun map_cs f = Context.mapping (map_claset f) (LocalClaset.map f); +fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f); (* attributes *) fun attrib f = Thm.declaration_attribute (fn th => - Context.mapping (map_claset (f th)) (LocalClaset.map (f th))); + Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th))); fun safe_dest w = attrib (addSE w o make_elim); val safe_elim = attrib o addSE;