src/Provers/classical.ML
changeset 42792 85fb70b0c5e8
parent 42791 36f787ae5f70
child 42793 88bee9f6eec7
     1.1 --- a/src/Provers/classical.ML	Fri May 13 15:55:32 2011 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri May 13 16:03:03 2011 +0200
     1.3 @@ -139,8 +139,6 @@
     1.4  functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =
     1.5  struct
     1.6  
     1.7 -local open Data in
     1.8 -
     1.9  (** classical elimination rules **)
    1.10  
    1.11  (*
    1.12 @@ -158,7 +156,7 @@
    1.13  fun classical_rule rule =
    1.14    if is_some (Object_Logic.elim_concl rule) then
    1.15      let
    1.16 -      val rule' = rule RS classical;
    1.17 +      val rule' = rule RS Data.classical;
    1.18        val concl' = Thm.concl_of rule';
    1.19        fun redundant_hyp goal =
    1.20          concl' aconv Logic.strip_assums_concl goal orelse
    1.21 @@ -184,15 +182,15 @@
    1.22  (*Prove goal that assumes both P and ~P.
    1.23    No backtracking if it finds an equal assumption.  Perhaps should call
    1.24    ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
    1.25 -val contr_tac = eresolve_tac [not_elim]  THEN'
    1.26 -                (eq_assume_tac ORELSE' assume_tac);
    1.27 +val contr_tac =
    1.28 +  eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac);
    1.29  
    1.30  (*Finds P-->Q and P in the assumptions, replaces implication by Q.
    1.31    Could do the same thing for P<->Q and P... *)
    1.32 -fun mp_tac i = eresolve_tac [not_elim, Data.imp_elim] i  THEN  assume_tac i;
    1.33 +fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i;
    1.34  
    1.35  (*Like mp_tac but instantiates no variables*)
    1.36 -fun eq_mp_tac i = ematch_tac [not_elim, Data.imp_elim] i  THEN  eq_assume_tac i;
    1.37 +fun eq_mp_tac i = ematch_tac [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
    1.38  
    1.39  (*Creates rules to eliminate ~A, from rules to introduce A*)
    1.40  fun swapify intrs = intrs RLN (2, [Data.swap]);
    1.41 @@ -201,14 +199,14 @@
    1.42  (*Uses introduction rules in the normal way, or on negated assumptions,
    1.43    trying rules in order. *)
    1.44  fun swap_res_tac rls =
    1.45 -    let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
    1.46 -    in  assume_tac      ORELSE'
    1.47 -        contr_tac       ORELSE'
    1.48 -        biresolve_tac (fold_rev addrl rls [])
    1.49 -    end;
    1.50 +  let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in
    1.51 +    assume_tac ORELSE'
    1.52 +    contr_tac ORELSE'
    1.53 +    biresolve_tac (fold_rev addrl rls [])
    1.54 +  end;
    1.55  
    1.56  (*Duplication of hazardous rules, for complete provers*)
    1.57 -fun dup_intr th = zero_var_indexes (th RS classical);
    1.58 +fun dup_intr th = zero_var_indexes (th RS Data.classical);
    1.59  
    1.60  fun dup_elim th =
    1.61    let
    1.62 @@ -642,7 +640,7 @@
    1.63          eq_assume_tac,
    1.64          eq_mp_tac,
    1.65          bimatch_from_nets_tac safe0_netpair,
    1.66 -        FIRST' hyp_subst_tacs,
    1.67 +        FIRST' Data.hyp_subst_tacs,
    1.68          bimatch_from_nets_tac safep_netpair]);
    1.69  
    1.70  (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
    1.71 @@ -662,7 +660,7 @@
    1.72  fun n_bimatch_from_nets_tac n =
    1.73    biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
    1.74  
    1.75 -fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
    1.76 +fun eq_contr_tac i = ematch_tac [Data.not_elim] i THEN eq_assume_tac i;
    1.77  val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
    1.78  
    1.79  (*Two-way branching is allowed only if one of the branches immediately closes*)
    1.80 @@ -675,7 +673,7 @@
    1.81    appSWrappers cs (FIRST' [
    1.82          eq_assume_contr_tac,
    1.83          bimatch_from_nets_tac safe0_netpair,
    1.84 -        FIRST' hyp_subst_tacs,
    1.85 +        FIRST' Data.hyp_subst_tacs,
    1.86          n_bimatch_from_nets_tac 1 safep_netpair,
    1.87          bimatch2_tac safep_netpair]);
    1.88  
    1.89 @@ -720,12 +718,12 @@
    1.90  (*Slower but smarter than fast_tac*)
    1.91  fun best_tac cs =
    1.92    Object_Logic.atomize_prems_tac THEN'
    1.93 -  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
    1.94 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac cs 1));
    1.95  
    1.96  (*even a bit smarter than best_tac*)
    1.97  fun first_best_tac cs =
    1.98    Object_Logic.atomize_prems_tac THEN'
    1.99 -  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
   1.100 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac cs)));
   1.101  
   1.102  fun slow_tac cs =
   1.103    Object_Logic.atomize_prems_tac THEN'
   1.104 @@ -733,7 +731,7 @@
   1.105  
   1.106  fun slow_best_tac cs =
   1.107    Object_Logic.atomize_prems_tac THEN'
   1.108 -  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
   1.109 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac cs 1));
   1.110  
   1.111  
   1.112  (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
   1.113 @@ -890,9 +888,6 @@
   1.114  val rule_del = attrib delrule o Context_Rules.rule_del;
   1.115  
   1.116  
   1.117 -end;
   1.118 -
   1.119 -
   1.120  
   1.121  (** concrete syntax of attributes **)
   1.122