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
```