src/Pure/raw_simplifier.ML
changeset 54742 7a86358a3c0b
parent 54731 384ac33802b0
child 54883 dd04a8b654fc
     1.1 --- a/src/Pure/raw_simplifier.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -57,13 +57,13 @@
     1.4    val setSolver: Proof.context * solver -> Proof.context
     1.5    val addSolver: Proof.context * solver -> Proof.context
     1.6  
     1.7 -  val rewrite_rule: thm list -> thm -> thm
     1.8 -  val rewrite_goals_rule: thm list -> thm -> thm
     1.9 -  val rewrite_goals_tac: thm list -> tactic
    1.10 -  val rewrite_goal_tac: thm list -> int -> tactic
    1.11 -  val prune_params_tac: tactic
    1.12 -  val fold_rule: thm list -> thm -> thm
    1.13 -  val fold_goals_tac: thm list -> tactic
    1.14 +  val rewrite_rule: Proof.context -> thm list -> thm -> thm
    1.15 +  val rewrite_goals_rule: Proof.context -> thm list -> thm -> thm
    1.16 +  val rewrite_goals_tac: Proof.context -> thm list -> tactic
    1.17 +  val rewrite_goal_tac: Proof.context -> thm list -> int -> tactic
    1.18 +  val prune_params_tac: Proof.context -> tactic
    1.19 +  val fold_rule: Proof.context -> thm list -> thm -> thm
    1.20 +  val fold_goals_tac: Proof.context -> thm list -> tactic
    1.21    val norm_hhf: thm -> thm
    1.22    val norm_hhf_protect: thm -> thm
    1.23  end;
    1.24 @@ -126,7 +126,7 @@
    1.25      (Proof.context -> thm -> thm option) -> Proof.context -> thm -> thm
    1.26    val generic_rewrite_goal_tac: bool * bool * bool ->
    1.27      (Proof.context -> tactic) -> Proof.context -> int -> tactic
    1.28 -  val rewrite: bool -> thm list -> conv
    1.29 +  val rewrite: Proof.context -> bool -> thm list -> conv
    1.30  end;
    1.31  
    1.32  structure Raw_Simplifier: RAW_SIMPLIFIER =
    1.33 @@ -1366,12 +1366,12 @@
    1.34  val simple_prover =
    1.35    SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));
    1.36  
    1.37 -fun rewrite _ [] ct = Thm.reflexive ct
    1.38 -  | rewrite full thms ct =
    1.39 +fun rewrite _ _ [] = Thm.reflexive
    1.40 +  | rewrite ctxt full thms =
    1.41        rewrite_cterm (full, false, false) simple_prover
    1.42 -        (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
    1.43 +        (empty_simpset ctxt addsimps thms);
    1.44  
    1.45 -val rewrite_rule = Conv.fconv_rule o rewrite true;
    1.46 +fun rewrite_rule ctxt = Conv.fconv_rule o rewrite ctxt true;
    1.47  
    1.48  (*simple term rewriting -- no proof*)
    1.49  fun rewrite_term thy rules procs =
    1.50 @@ -1380,15 +1380,15 @@
    1.51  fun rewrite_thm mode prover ctxt = Conv.fconv_rule (rewrite_cterm mode prover ctxt);
    1.52  
    1.53  (*Rewrite the subgoals of a proof state (represented by a theorem)*)
    1.54 -fun rewrite_goals_rule thms th =
    1.55 +fun rewrite_goals_rule ctxt thms th =
    1.56    Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
    1.57 -    (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
    1.58 +    (empty_simpset ctxt addsimps thms))) th;
    1.59  
    1.60  
    1.61  (** meta-rewriting tactics **)
    1.62  
    1.63  (*Rewrite all subgoals*)
    1.64 -fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
    1.65 +fun rewrite_goals_tac ctxt defs = PRIMITIVE (rewrite_goals_rule ctxt defs);
    1.66  
    1.67  (*Rewrite one subgoal*)
    1.68  fun generic_rewrite_goal_tac mode prover_tac ctxt i thm =
    1.69 @@ -1396,12 +1396,12 @@
    1.70      Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ctxt) i thm)
    1.71    else Seq.empty;
    1.72  
    1.73 -fun rewrite_goal_tac rews i st =
    1.74 +fun rewrite_goal_tac ctxt rews =
    1.75    generic_rewrite_goal_tac (true, false, false) (K no_tac)
    1.76 -    (global_context (Thm.theory_of_thm st) empty_ss addsimps rews) i st;
    1.77 +    (empty_simpset ctxt addsimps rews);
    1.78  
    1.79  (*Prunes all redundant parameters from the proof state by rewriting.*)
    1.80 -val prune_params_tac = rewrite_goals_tac [Drule.triv_forall_equality];
    1.81 +fun prune_params_tac ctxt = rewrite_goals_tac ctxt [Drule.triv_forall_equality];
    1.82  
    1.83  
    1.84  (* for folding definitions, handling critical pairs *)
    1.85 @@ -1422,8 +1422,8 @@
    1.86  
    1.87  val rev_defs = sort_lhs_depths o map Thm.symmetric;
    1.88  
    1.89 -fun fold_rule defs = fold rewrite_rule (rev_defs defs);
    1.90 -fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
    1.91 +fun fold_rule ctxt defs = fold (rewrite_rule ctxt) (rev_defs defs);
    1.92 +fun fold_goals_tac ctxt defs = EVERY (map (rewrite_goals_tac ctxt) (rev_defs defs));
    1.93  
    1.94  
    1.95  (* HHF normal form: !! before ==>, outermost !! generalized *)