src/FOLP/classical.ML
changeset 58957 c9e744ea8a38
parent 42799 4e33894aec6d
child 58963 26bf09b95dda
     1.1 --- a/src/FOLP/classical.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/FOLP/classical.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -44,19 +44,19 @@
     1.4        {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, 
     1.5         safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
     1.6         haz_brls: (bool*thm)list}
     1.7 -  val best_tac : claset -> int -> tactic
     1.8 +  val best_tac : Proof.context -> claset -> int -> tactic
     1.9    val contr_tac : int -> tactic
    1.10 -  val fast_tac : claset -> int -> tactic
    1.11 +  val fast_tac : Proof.context -> claset -> int -> tactic
    1.12    val inst_step_tac : int -> tactic
    1.13    val joinrules : thm list * thm list -> (bool * thm) list
    1.14    val mp_tac: int -> tactic
    1.15 -  val safe_tac : claset -> tactic
    1.16 -  val safe_step_tac : claset -> int -> tactic
    1.17 -  val slow_step_tac : claset -> int -> tactic
    1.18 -  val step_tac : claset -> int -> tactic
    1.19 +  val safe_tac : Proof.context -> claset -> tactic
    1.20 +  val safe_step_tac : Proof.context -> claset -> int -> tactic
    1.21 +  val slow_step_tac : Proof.context -> claset -> int -> tactic
    1.22 +  val step_tac : Proof.context -> claset -> int -> tactic
    1.23    val swapify : thm list -> thm list
    1.24    val swap_res_tac : thm list -> int -> tactic
    1.25 -  val uniq_mp_tac: int -> tactic
    1.26 +  val uniq_mp_tac: Proof.context -> int -> tactic
    1.27    end;
    1.28  
    1.29  
    1.30 @@ -76,7 +76,7 @@
    1.31  fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac i;
    1.32  
    1.33  (*Like mp_tac but instantiates no variables*)
    1.34 -fun uniq_mp_tac i = ematch_tac ([not_elim,imp_elim]) i  THEN  uniq_assume_tac i;
    1.35 +fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i  THEN  uniq_assume_tac i;
    1.36  
    1.37  (*Creates rules to eliminate ~A, from rules to introduce A*)
    1.38  fun swapify intrs = intrs RLN (2, [swap]);
    1.39 @@ -148,38 +148,38 @@
    1.40  (*** Simple tactics for theorem proving ***)
    1.41  
    1.42  (*Attack subgoals using safe inferences*)
    1.43 -fun safe_step_tac (CS{safe0_brls,safep_brls,...}) = 
    1.44 +fun safe_step_tac ctxt (CS{safe0_brls,safep_brls,...}) = 
    1.45    FIRST' [uniq_assume_tac,
    1.46 -          uniq_mp_tac,
    1.47 +          uniq_mp_tac ctxt,
    1.48            biresolve_tac safe0_brls,
    1.49            FIRST' hyp_subst_tacs,
    1.50            biresolve_tac safep_brls] ;
    1.51  
    1.52  (*Repeatedly attack subgoals using safe inferences*)
    1.53 -fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs));
    1.54 +fun safe_tac ctxt cs = DETERM (REPEAT_FIRST (safe_step_tac ctxt cs));
    1.55  
    1.56  (*These steps could instantiate variables and are therefore unsafe.*)
    1.57  val inst_step_tac = assume_tac APPEND' contr_tac;
    1.58  
    1.59  (*Single step for the prover.  FAILS unless it makes progress. *)
    1.60 -fun step_tac (cs as (CS{haz_brls,...})) i = 
    1.61 -  FIRST [safe_tac cs,
    1.62 +fun step_tac ctxt (cs as (CS{haz_brls,...})) i = 
    1.63 +  FIRST [safe_tac ctxt cs,
    1.64           inst_step_tac i,
    1.65           biresolve_tac haz_brls i];
    1.66  
    1.67  (*** The following tactics all fail unless they solve one goal ***)
    1.68  
    1.69  (*Dumb but fast*)
    1.70 -fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
    1.71 +fun fast_tac ctxt cs = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt cs 1));
    1.72  
    1.73  (*Slower but smarter than fast_tac*)
    1.74 -fun best_tac cs = 
    1.75 -  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
    1.76 +fun best_tac ctxt cs = 
    1.77 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac ctxt cs 1));
    1.78  
    1.79  (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
    1.80    allows backtracking from "safe" rules to "unsafe" rules here.*)
    1.81 -fun slow_step_tac (cs as (CS{haz_brls,...})) i = 
    1.82 -    safe_tac cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);
    1.83 +fun slow_step_tac ctxt (cs as (CS{haz_brls,...})) i = 
    1.84 +    safe_tac ctxt cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);
    1.85  
    1.86  end; 
    1.87  end;