--- a/src/FOL/simpdata.ML Fri Apr 30 08:47:07 2010 -0700
+++ b/src/FOL/simpdata.ML Fri Apr 30 09:54:04 2010 -0700
@@ -21,13 +21,13 @@
| _ => th RS @{thm iff_reflection_T};
(*Replace premises x=y, X<->Y by X==Y*)
-val mk_meta_prems =
- rule_by_tactic
+fun mk_meta_prems ctxt =
+ rule_by_tactic ctxt
(REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
(*Congruence rules for = or <-> (instead of ==)*)
-fun mk_meta_cong (_: simpset) rl =
- Drule.export_without_context (mk_meta_eq (mk_meta_prems rl))
+fun mk_meta_cong ss rl =
+ Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must use =-equality or <->");
--- a/src/HOL/Metis_Examples/Message.thy Fri Apr 30 08:47:07 2010 -0700
+++ b/src/HOL/Metis_Examples/Message.thy Fri Apr 30 09:54:04 2010 -0700
@@ -711,7 +711,7 @@
lemma Fake_parts_insert:
"X \<in> synth (analz H) ==>
parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
-sledgehammer
+(*sledgehammer*)
proof -
assume A1: "X \<in> synth (analz H)"
have F1: "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth (analz x\<^isub>1) = analz (synth (analz x\<^isub>1))"
--- a/src/HOL/Tools/TFL/post.ML Fri Apr 30 08:47:07 2010 -0700
+++ b/src/HOL/Tools/TFL/post.ML Fri Apr 30 09:54:04 2010 -0700
@@ -128,9 +128,9 @@
Split_Rule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
-val meta_outer =
+fun meta_outer ctxt =
curry_rule o Drule.export_without_context o
- rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
+ rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
(*Strip off the outer !P*)
val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
@@ -139,7 +139,9 @@
| tracing false msg = writeln msg;
fun simplify_defn strict thy cs ss congs wfs id pats def0 =
- let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
+ let
+ val ctxt = ProofContext.init thy
+ val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
val {rules,rows,TCs,full_pats_TCs} =
Prim.post_definition congs (thy, (def,pats))
val {lhs=f,rhs} = S.dest_eq (concl def)
@@ -153,7 +155,7 @@
TCs = TCs}
val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
(R.CONJUNCTS rules)
- in {induct = meta_outer (Object_Logic.rulify_no_asm (induction RS spec')),
+ in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')),
rules = ListPair.zip(rules', rows),
tcs = (termination_goals rules') @ tcs}
end
--- a/src/HOL/Tools/inductive.ML Fri Apr 30 08:47:07 2010 -0700
+++ b/src/HOL/Tools/inductive.ML Fri Apr 30 09:54:04 2010 -0700
@@ -446,7 +446,7 @@
val cprop = Thm.cterm_of thy prop;
val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
fun mk_elim rl =
- Thm.implies_intr cprop (Tactic.rule_by_tactic tac (Thm.assume cprop RS rl))
+ Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
|> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
in
(case get_first (try mk_elim) elims of
--- a/src/HOL/Tools/split_rule.ML Fri Apr 30 08:47:07 2010 -0700
+++ b/src/HOL/Tools/split_rule.ML Fri Apr 30 09:54:04 2010 -0700
@@ -116,7 +116,7 @@
fun split_rule_goal ctxt xss rl =
let
- fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i);
+ fun one_split i s = Tactic.rule_by_tactic ctxt (pair_tac ctxt s i);
fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
in
rl
--- a/src/Provers/classical.ML Fri Apr 30 08:47:07 2010 -0700
+++ b/src/Provers/classical.ML Fri Apr 30 09:54:04 2010 -0700
@@ -208,8 +208,11 @@
fun dup_intr th = zero_var_indexes (th RS classical);
fun dup_elim th =
- rule_by_tactic (TRYALL (etac revcut_rl))
- ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd);
+ let
+ val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
+ val ctxt = ProofContext.init (Thm.theory_of_thm rl);
+ in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
+
(**** Classical rule sets ****)
--- a/src/Pure/meta_simplifier.ML Fri Apr 30 08:47:07 2010 -0700
+++ b/src/Pure/meta_simplifier.ML Fri Apr 30 09:54:04 2010 -0700
@@ -115,6 +115,7 @@
val the_context: simpset -> Proof.context
val context: Proof.context -> simpset -> simpset
val global_context: theory -> simpset -> simpset
+ val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
val debug_bounds: bool Unsynchronized.ref
val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
val set_solvers: solver list -> simpset -> simpset
@@ -326,7 +327,8 @@
print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
fun cond_warn_thm a (ss as Simpset ({context, ...}, _)) th =
- if is_some context then () else warn_thm a ss th;
+ if (case context of NONE => true | SOME ctxt => Context_Position.is_visible ctxt)
+ then warn_thm a ss th else ();
end;
@@ -358,9 +360,13 @@
fun activate_context thy ss =
let
val ctxt = the_context ss;
- val ctxt' = Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt;
+ val ctxt' = ctxt
+ |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt))
+ |> Context_Position.set_visible false;
in context ctxt' ss end;
+fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss));
+
(* maintain simp rules *)
--- a/src/Pure/simplifier.ML Fri Apr 30 08:47:07 2010 -0700
+++ b/src/Pure/simplifier.ML Fri Apr 30 09:54:04 2010 -0700
@@ -108,7 +108,7 @@
);
val get_ss = SimpsetData.get;
-val map_ss = SimpsetData.map;
+fun map_ss f context = SimpsetData.map (with_context (Context.proof_of context) f) context;
(* attributes *)
--- a/src/Pure/tactic.ML Fri Apr 30 08:47:07 2010 -0700
+++ b/src/Pure/tactic.ML Fri Apr 30 09:54:04 2010 -0700
@@ -7,7 +7,7 @@
signature BASIC_TACTIC =
sig
val trace_goalno_tac: (int -> tactic) -> int -> tactic
- val rule_by_tactic: tactic -> thm -> thm
+ val rule_by_tactic: Proof.context -> tactic -> thm -> thm
val assume_tac: int -> tactic
val eq_assume_tac: int -> tactic
val compose_tac: (bool * thm * int) -> int -> tactic
@@ -86,14 +86,14 @@
Seq.make(fn()=> seqcell));
(*Makes a rule by applying a tactic to an existing rule*)
-fun rule_by_tactic tac rl =
+fun rule_by_tactic ctxt tac rl =
let
- val ctxt = Variable.thm_context rl;
- val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
+ val ctxt' = Variable.declare_thm rl ctxt;
+ val ((_, [st]), ctxt'') = Variable.import true [rl] ctxt';
in
(case Seq.pull (tac st) of
NONE => raise THM ("rule_by_tactic", 0, [rl])
- | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
+ | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt'' ctxt') st'))
end;
--- a/src/Sequents/simpdata.ML Fri Apr 30 08:47:07 2010 -0700
+++ b/src/Sequents/simpdata.ML Fri Apr 30 09:54:04 2010 -0700
@@ -42,13 +42,13 @@
Display.string_of_thm_without_context th));
(*Replace premises x=y, X<->Y by X==Y*)
-val mk_meta_prems =
- rule_by_tactic
+fun mk_meta_prems ctxt =
+ rule_by_tactic ctxt
(REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
(*Congruence rules for = or <-> (instead of ==)*)
-fun mk_meta_cong (_: simpset) rl =
- Drule.export_without_context(mk_meta_eq (mk_meta_prems rl))
+fun mk_meta_cong ss rl =
+ Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
handle THM _ =>
error("Premises and conclusion of congruence rules must use =-equality or <->");
--- a/src/Tools/Code/code_haskell.ML Fri Apr 30 08:47:07 2010 -0700
+++ b/src/Tools/Code/code_haskell.ML Fri Apr 30 09:54:04 2010 -0700
@@ -109,10 +109,9 @@
let
val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
- in brackify_block fxy
- (concat [str "case", print_term tyvars some_thm vars NOBR t, str "of", str "{"])
+ in Pretty.block_enclose
+ (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
(map print_select clauses)
- (str "}")
end
| print_case tyvars some_thm vars fxy ((_, []), _) =
(brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
--- a/src/ZF/Tools/inductive_package.ML Fri Apr 30 08:47:07 2010 -0700
+++ b/src/ZF/Tools/inductive_package.ML Fri Apr 30 09:54:04 2010 -0700
@@ -261,7 +261,7 @@
THEN (PRIMITIVE (fold_rule part_rec_defs));
(*Elimination*)
- val elim = rule_by_tactic basic_elim_tac
+ val elim = rule_by_tactic (ProofContext.init thy1) basic_elim_tac
(unfold RS Ind_Syntax.equals_CollectD)
(*Applies freeness of the given constructors, which *must* be unfolded by
@@ -269,7 +269,7 @@
con_defs=[] for inference systems.
Proposition A should have the form t:Si where Si is an inductive set*)
fun make_cases ctxt A =
- rule_by_tactic
+ rule_by_tactic ctxt
(basic_elim_tac THEN ALLGOALS (asm_full_simp_tac (simpset_of ctxt)) THEN basic_elim_tac)
(Thm.assume A RS elim)
|> Drule.export_without_context_open;