proper context for rule_by_tactic;
authorwenzelm
Fri Apr 30 18:06:29 2010 +0200 (2010-04-30)
changeset 36546a9873318fe30
parent 36545 5c5b5c7f1157
child 36579 04dd306fdb3c
proper context for rule_by_tactic;
src/FOL/simpdata.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/split_rule.ML
src/Provers/classical.ML
src/Pure/tactic.ML
src/Sequents/simpdata.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/FOL/simpdata.ML	Fri Apr 30 17:18:29 2010 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Fri Apr 30 18:06:29 2010 +0200
     1.3 @@ -21,13 +21,13 @@
     1.4    | _                           => th RS @{thm iff_reflection_T};
     1.5  
     1.6  (*Replace premises x=y, X<->Y by X==Y*)
     1.7 -val mk_meta_prems =
     1.8 -    rule_by_tactic
     1.9 +fun mk_meta_prems ctxt =
    1.10 +    rule_by_tactic ctxt
    1.11        (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
    1.12  
    1.13  (*Congruence rules for = or <-> (instead of ==)*)
    1.14 -fun mk_meta_cong (_: simpset) rl =
    1.15 -  Drule.export_without_context (mk_meta_eq (mk_meta_prems rl))
    1.16 +fun mk_meta_cong ss rl =
    1.17 +  Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
    1.18      handle THM _ =>
    1.19        error("Premises and conclusion of congruence rules must use =-equality or <->");
    1.20  
     2.1 --- a/src/HOL/Tools/TFL/post.ML	Fri Apr 30 17:18:29 2010 +0200
     2.2 +++ b/src/HOL/Tools/TFL/post.ML	Fri Apr 30 18:06:29 2010 +0200
     2.3 @@ -128,9 +128,9 @@
     2.4    Split_Rule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
     2.5  
     2.6  (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
     2.7 -val meta_outer =
     2.8 +fun meta_outer ctxt =
     2.9    curry_rule o Drule.export_without_context o
    2.10 -  rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
    2.11 +  rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
    2.12  
    2.13  (*Strip off the outer !P*)
    2.14  val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
    2.15 @@ -139,7 +139,9 @@
    2.16    | tracing false msg = writeln msg;
    2.17  
    2.18  fun simplify_defn strict thy cs ss congs wfs id pats def0 =
    2.19 -   let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
    2.20 +   let
    2.21 +       val ctxt = ProofContext.init thy
    2.22 +       val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
    2.23         val {rules,rows,TCs,full_pats_TCs} =
    2.24             Prim.post_definition congs (thy, (def,pats))
    2.25         val {lhs=f,rhs} = S.dest_eq (concl def)
    2.26 @@ -153,7 +155,7 @@
    2.27                  TCs = TCs}
    2.28         val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
    2.29                          (R.CONJUNCTS rules)
    2.30 -         in  {induct = meta_outer (Object_Logic.rulify_no_asm (induction RS spec')),
    2.31 +         in  {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')),
    2.32          rules = ListPair.zip(rules', rows),
    2.33          tcs = (termination_goals rules') @ tcs}
    2.34     end
     3.1 --- a/src/HOL/Tools/inductive.ML	Fri Apr 30 17:18:29 2010 +0200
     3.2 +++ b/src/HOL/Tools/inductive.ML	Fri Apr 30 18:06:29 2010 +0200
     3.3 @@ -446,7 +446,7 @@
     3.4      val cprop = Thm.cterm_of thy prop;
     3.5      val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
     3.6      fun mk_elim rl =
     3.7 -      Thm.implies_intr cprop (Tactic.rule_by_tactic tac (Thm.assume cprop RS rl))
     3.8 +      Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
     3.9        |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
    3.10    in
    3.11      (case get_first (try mk_elim) elims of
     4.1 --- a/src/HOL/Tools/split_rule.ML	Fri Apr 30 17:18:29 2010 +0200
     4.2 +++ b/src/HOL/Tools/split_rule.ML	Fri Apr 30 18:06:29 2010 +0200
     4.3 @@ -116,7 +116,7 @@
     4.4  
     4.5  fun split_rule_goal ctxt xss rl =
     4.6    let
     4.7 -    fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i);
     4.8 +    fun one_split i s = Tactic.rule_by_tactic ctxt (pair_tac ctxt s i);
     4.9      fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
    4.10    in
    4.11      rl
     5.1 --- a/src/Provers/classical.ML	Fri Apr 30 17:18:29 2010 +0200
     5.2 +++ b/src/Provers/classical.ML	Fri Apr 30 18:06:29 2010 +0200
     5.3 @@ -208,8 +208,11 @@
     5.4  fun dup_intr th = zero_var_indexes (th RS classical);
     5.5  
     5.6  fun dup_elim th =
     5.7 -    rule_by_tactic (TRYALL (etac revcut_rl))
     5.8 -      ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd);
     5.9 +  let
    5.10 +    val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
    5.11 +    val ctxt = ProofContext.init (Thm.theory_of_thm rl);
    5.12 +  in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
    5.13 +
    5.14  
    5.15  (**** Classical rule sets ****)
    5.16  
     6.1 --- a/src/Pure/tactic.ML	Fri Apr 30 17:18:29 2010 +0200
     6.2 +++ b/src/Pure/tactic.ML	Fri Apr 30 18:06:29 2010 +0200
     6.3 @@ -7,7 +7,7 @@
     6.4  signature BASIC_TACTIC =
     6.5  sig
     6.6    val trace_goalno_tac: (int -> tactic) -> int -> tactic
     6.7 -  val rule_by_tactic: tactic -> thm -> thm
     6.8 +  val rule_by_tactic: Proof.context -> tactic -> thm -> thm
     6.9    val assume_tac: int -> tactic
    6.10    val eq_assume_tac: int -> tactic
    6.11    val compose_tac: (bool * thm * int) -> int -> tactic
    6.12 @@ -86,14 +86,14 @@
    6.13                           Seq.make(fn()=> seqcell));
    6.14  
    6.15  (*Makes a rule by applying a tactic to an existing rule*)
    6.16 -fun rule_by_tactic tac rl =
    6.17 +fun rule_by_tactic ctxt tac rl =
    6.18    let
    6.19 -    val ctxt = Variable.thm_context rl;
    6.20 -    val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
    6.21 +    val ctxt' = Variable.declare_thm rl ctxt;
    6.22 +    val ((_, [st]), ctxt'') = Variable.import true [rl] ctxt';
    6.23    in
    6.24      (case Seq.pull (tac st) of
    6.25        NONE => raise THM ("rule_by_tactic", 0, [rl])
    6.26 -    | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
    6.27 +    | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt'' ctxt') st'))
    6.28    end;
    6.29  
    6.30  
     7.1 --- a/src/Sequents/simpdata.ML	Fri Apr 30 17:18:29 2010 +0200
     7.2 +++ b/src/Sequents/simpdata.ML	Fri Apr 30 18:06:29 2010 +0200
     7.3 @@ -42,13 +42,13 @@
     7.4                           Display.string_of_thm_without_context th));
     7.5  
     7.6  (*Replace premises x=y, X<->Y by X==Y*)
     7.7 -val mk_meta_prems =
     7.8 -    rule_by_tactic
     7.9 +fun mk_meta_prems ctxt =
    7.10 +    rule_by_tactic ctxt
    7.11        (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
    7.12  
    7.13  (*Congruence rules for = or <-> (instead of ==)*)
    7.14 -fun mk_meta_cong (_: simpset) rl =
    7.15 -  Drule.export_without_context(mk_meta_eq (mk_meta_prems rl))
    7.16 +fun mk_meta_cong ss rl =
    7.17 +  Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
    7.18      handle THM _ =>
    7.19        error("Premises and conclusion of congruence rules must use =-equality or <->");
    7.20  
     8.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Apr 30 17:18:29 2010 +0200
     8.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Apr 30 18:06:29 2010 +0200
     8.3 @@ -261,7 +261,7 @@
     8.4        THEN (PRIMITIVE (fold_rule part_rec_defs));
     8.5  
     8.6    (*Elimination*)
     8.7 -  val elim = rule_by_tactic basic_elim_tac
     8.8 +  val elim = rule_by_tactic (ProofContext.init thy1) basic_elim_tac
     8.9                   (unfold RS Ind_Syntax.equals_CollectD)
    8.10  
    8.11    (*Applies freeness of the given constructors, which *must* be unfolded by
    8.12 @@ -269,7 +269,7 @@
    8.13        con_defs=[] for inference systems.
    8.14      Proposition A should have the form t:Si where Si is an inductive set*)
    8.15    fun make_cases ctxt A =
    8.16 -    rule_by_tactic
    8.17 +    rule_by_tactic ctxt
    8.18        (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac (simpset_of ctxt)) THEN basic_elim_tac)
    8.19        (Thm.assume A RS elim)
    8.20        |> Drule.export_without_context_open;