src/Provers/classical.ML
changeset 58957 c9e744ea8a38
parent 58950 d07464875dd4
child 58958 114255dce178
     1.1 --- a/src/Provers/classical.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/Provers/classical.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4    val dup_elim: thm -> thm
     1.5    val dup_intr: thm -> thm
     1.6    val dup_step_tac: Proof.context -> int -> tactic
     1.7 -  val eq_mp_tac: int -> tactic
     1.8 +  val eq_mp_tac: Proof.context -> int -> tactic
     1.9    val haz_step_tac: Proof.context -> int -> tactic
    1.10    val joinrules: thm list * thm list -> (bool * thm) list
    1.11    val mp_tac: int -> tactic
    1.12 @@ -187,7 +187,7 @@
    1.13  fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i;
    1.14  
    1.15  (*Like mp_tac but instantiates no variables*)
    1.16 -fun eq_mp_tac i = ematch_tac [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
    1.17 +fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
    1.18  
    1.19  (*Creates rules to eliminate ~A, from rules to introduce A*)
    1.20  fun swapify intrs = intrs RLN (2, [Data.swap]);
    1.21 @@ -689,10 +689,14 @@
    1.22  fun ctxt addafter (name, tac2) =
    1.23    ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt);
    1.24  
    1.25 -fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
    1.26 -fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
    1.27 -fun ctxt addSD2 (name, thm) = ctxt addSafter (name, fn _ => dmatch_tac [thm] THEN' eq_assume_tac);
    1.28 -fun ctxt addSE2 (name, thm) = ctxt addSafter (name, fn _ => ematch_tac [thm] THEN' eq_assume_tac);
    1.29 +fun ctxt addD2 (name, thm) =
    1.30 +  ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
    1.31 +fun ctxt addE2 (name, thm) =
    1.32 +  ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
    1.33 +fun ctxt addSD2 (name, thm) =
    1.34 +  ctxt addSafter (name, fn ctxt' => dmatch_tac ctxt' [thm] THEN' eq_assume_tac);
    1.35 +fun ctxt addSE2 (name, thm) =
    1.36 +  ctxt addSafter (name, fn ctxt' => ematch_tac ctxt' [thm] THEN' eq_assume_tac);
    1.37  
    1.38  
    1.39  
    1.40 @@ -704,7 +708,7 @@
    1.41      appSWrappers ctxt
    1.42        (FIRST'
    1.43         [eq_assume_tac,
    1.44 -        eq_mp_tac,
    1.45 +        eq_mp_tac ctxt,
    1.46          bimatch_from_nets_tac safe0_netpair,
    1.47          FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
    1.48          bimatch_from_nets_tac safep_netpair])
    1.49 @@ -727,24 +731,24 @@
    1.50  fun n_bimatch_from_nets_tac n =
    1.51    biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
    1.52  
    1.53 -fun eq_contr_tac i = ematch_tac [Data.not_elim] i THEN eq_assume_tac i;
    1.54 -val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
    1.55 +fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i;
    1.56 +fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt;
    1.57  
    1.58  (*Two-way branching is allowed only if one of the branches immediately closes*)
    1.59 -fun bimatch2_tac netpair i =
    1.60 +fun bimatch2_tac ctxt netpair i =
    1.61    n_bimatch_from_nets_tac 2 netpair i THEN
    1.62 -  (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1));
    1.63 +  (eq_assume_contr_tac ctxt i ORELSE eq_assume_contr_tac ctxt (i + 1));
    1.64  
    1.65  (*Attack subgoals using safe inferences -- matching, not resolution*)
    1.66  fun clarify_step_tac ctxt =
    1.67    let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
    1.68      appSWrappers ctxt
    1.69       (FIRST'
    1.70 -       [eq_assume_contr_tac,
    1.71 +       [eq_assume_contr_tac ctxt,
    1.72          bimatch_from_nets_tac safe0_netpair,
    1.73          FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
    1.74          n_bimatch_from_nets_tac 1 safep_netpair,
    1.75 -        bimatch2_tac safep_netpair])
    1.76 +        bimatch2_tac ctxt safep_netpair])
    1.77    end;
    1.78  
    1.79  fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1));