src/FOLP/classical.ML
changeset 58963 26bf09b95dda
parent 58957 c9e744ea8a38
child 59498 50b60f501b05
     1.1 --- a/src/FOLP/classical.ML	Sun Nov 09 20:49:28 2014 +0100
     1.2 +++ b/src/FOLP/classical.ML	Mon Nov 10 21:49:48 2014 +0100
     1.3 @@ -45,17 +45,17 @@
     1.4         safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
     1.5         haz_brls: (bool*thm)list}
     1.6    val best_tac : Proof.context -> claset -> int -> tactic
     1.7 -  val contr_tac : int -> tactic
     1.8 +  val contr_tac : Proof.context -> int -> tactic
     1.9    val fast_tac : Proof.context -> claset -> int -> tactic
    1.10 -  val inst_step_tac : int -> tactic
    1.11 +  val inst_step_tac : Proof.context -> int -> tactic
    1.12    val joinrules : thm list * thm list -> (bool * thm) list
    1.13 -  val mp_tac: int -> tactic
    1.14 +  val mp_tac: Proof.context -> int -> tactic
    1.15    val safe_tac : Proof.context -> claset -> tactic
    1.16    val safe_step_tac : Proof.context -> claset -> int -> tactic
    1.17    val slow_step_tac : Proof.context -> claset -> int -> tactic
    1.18    val step_tac : Proof.context -> claset -> int -> tactic
    1.19    val swapify : thm list -> thm list
    1.20 -  val swap_res_tac : thm list -> int -> tactic
    1.21 +  val swap_res_tac : Proof.context -> thm list -> int -> tactic
    1.22    val uniq_mp_tac: Proof.context -> int -> tactic
    1.23    end;
    1.24  
    1.25 @@ -70,22 +70,22 @@
    1.26  val imp_elim = make_elim mp;
    1.27  
    1.28  (*Solve goal that assumes both P and ~P. *)
    1.29 -val contr_tac = etac not_elim THEN'  assume_tac;
    1.30 +fun contr_tac ctxt = etac not_elim THEN'  assume_tac ctxt;
    1.31  
    1.32  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
    1.33 -fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac i;
    1.34 +fun mp_tac ctxt i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac ctxt i;
    1.35  
    1.36  (*Like mp_tac but instantiates no variables*)
    1.37 -fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i  THEN  uniq_assume_tac i;
    1.38 +fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i  THEN  uniq_assume_tac ctxt i;
    1.39  
    1.40  (*Creates rules to eliminate ~A, from rules to introduce A*)
    1.41  fun swapify intrs = intrs RLN (2, [swap]);
    1.42  
    1.43  (*Uses introduction rules in the normal way, or on negated assumptions,
    1.44    trying rules in order. *)
    1.45 -fun swap_res_tac rls = 
    1.46 +fun swap_res_tac ctxt rls = 
    1.47      let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap))
    1.48 -    in  assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls)
    1.49 +    in  assume_tac ctxt ORELSE' contr_tac ctxt ORELSE' FIRST' (map tacf rls)
    1.50      end;
    1.51  
    1.52  
    1.53 @@ -149,7 +149,7 @@
    1.54  
    1.55  (*Attack subgoals using safe inferences*)
    1.56  fun safe_step_tac ctxt (CS{safe0_brls,safep_brls,...}) = 
    1.57 -  FIRST' [uniq_assume_tac,
    1.58 +  FIRST' [uniq_assume_tac ctxt,
    1.59            uniq_mp_tac ctxt,
    1.60            biresolve_tac safe0_brls,
    1.61            FIRST' hyp_subst_tacs,
    1.62 @@ -159,12 +159,12 @@
    1.63  fun safe_tac ctxt cs = DETERM (REPEAT_FIRST (safe_step_tac ctxt cs));
    1.64  
    1.65  (*These steps could instantiate variables and are therefore unsafe.*)
    1.66 -val inst_step_tac = assume_tac APPEND' contr_tac;
    1.67 +fun inst_step_tac ctxt = assume_tac ctxt APPEND' contr_tac ctxt;
    1.68  
    1.69  (*Single step for the prover.  FAILS unless it makes progress. *)
    1.70  fun step_tac ctxt (cs as (CS{haz_brls,...})) i = 
    1.71    FIRST [safe_tac ctxt cs,
    1.72 -         inst_step_tac i,
    1.73 +         inst_step_tac ctxt i,
    1.74           biresolve_tac haz_brls i];
    1.75  
    1.76  (*** The following tactics all fail unless they solve one goal ***)
    1.77 @@ -179,7 +179,7 @@
    1.78  (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
    1.79    allows backtracking from "safe" rules to "unsafe" rules here.*)
    1.80  fun slow_step_tac ctxt (cs as (CS{haz_brls,...})) i = 
    1.81 -    safe_tac ctxt cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);
    1.82 +    safe_tac ctxt cs ORELSE (assume_tac ctxt i APPEND biresolve_tac haz_brls i);
    1.83  
    1.84  end; 
    1.85  end;