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