src/Provers/classical.ML
author paulson
Fri Aug 18 15:20:02 1995 +0200 (1995-08-18)
changeset 1231 91d2c1bb5803
parent 1073 b3f190995bc9
child 1524 524879632d88
permissions -rw-r--r--
clarified comment
     1 (*  Title: 	Provers/classical
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Theorem prover for classical reasoning, including predicate calculus, set
     7 theory, etc.
     8 
     9 Rules must be classified as intr, elim, safe, hazardous.
    10 
    11 A rule is unsafe unless it can be applied blindly without harmful results.
    12 For a rule to be safe, its premises and conclusion should be logically
    13 equivalent.  There should be no variables in the premises that are not in
    14 the conclusion.
    15 *)
    16 
    17 infix 1 THEN_MAYBE;
    18 
    19 signature CLASSICAL_DATA =
    20   sig
    21   val mp	: thm    	(* [| P-->Q;  P |] ==> Q *)
    22   val not_elim	: thm		(* [| ~P;  P |] ==> R *)
    23   val classical	: thm		(* (~P ==> P) ==> P *)
    24   val sizef 	: thm -> int	(* size function for BEST_FIRST *)
    25   val hyp_subst_tacs: (int -> tactic) list
    26   end;
    27 
    28 (*Higher precedence than := facilitates use of references*)
    29 infix 4 addSIs addSEs addSDs addIs addEs addDs 
    30         setwrapper compwrapper addbefore addafter;
    31 
    32 
    33 signature CLASSICAL =
    34   sig
    35   type claset
    36   type netpair
    37   val empty_cs		: claset
    38   val addDs 		: claset * thm list -> claset
    39   val addEs 		: claset * thm list -> claset
    40   val addIs 		: claset * thm list -> claset
    41   val addSDs		: claset * thm list -> claset
    42   val addSEs		: claset * thm list -> claset
    43   val addSIs		: claset * thm list -> claset
    44   val setwrapper 	: claset * (tactic->tactic) -> claset
    45   val compwrapper 	: claset * (tactic->tactic) -> claset
    46   val addbefore 	: claset * tactic -> claset
    47   val addafter 		: claset * tactic -> claset
    48 
    49   val print_cs		: claset -> unit
    50   val rep_claset	: 
    51       claset -> {safeIs: thm list, safeEs: thm list, 
    52 		 hazIs: thm list, hazEs: thm list,
    53 		 wrapper: tactic -> tactic,
    54 		 safe0_netpair: netpair, safep_netpair: netpair,
    55 		 haz_netpair: netpair, dup_netpair: netpair}
    56   val getwrapper	: claset -> tactic -> tactic
    57   val THEN_MAYBE	: tactic * tactic -> tactic
    58 
    59   val best_tac 		: claset -> int -> tactic
    60   val contr_tac 	: int -> tactic
    61   val depth_tac		: claset -> int -> int -> tactic
    62   val deepen_tac	: claset -> int -> int -> tactic
    63   val dup_elim		: thm -> thm
    64   val dup_intr		: thm -> thm
    65   val dup_step_tac	: claset -> int -> tactic
    66   val eq_mp_tac		: int -> tactic
    67   val fast_tac 		: claset -> int -> tactic
    68   val haz_step_tac 	: claset -> int -> tactic
    69   val joinrules 	: thm list * thm list -> (bool * thm) list
    70   val mp_tac		: int -> tactic
    71   val safe_tac 		: claset -> tactic
    72   val safe_step_tac 	: claset -> int -> tactic
    73   val slow_step_tac 	: claset -> int -> tactic
    74   val slow_best_tac 	: claset -> int -> tactic
    75   val slow_tac 		: claset -> int -> tactic
    76   val step_tac 		: claset -> int -> tactic
    77   val swap		: thm                 (* ~P ==> (~Q ==> P) ==> Q *)
    78   val swapify 		: thm list -> thm list
    79   val swap_res_tac 	: thm list -> int -> tactic
    80   val inst_step_tac 	: claset -> int -> tactic
    81   val inst0_step_tac 	: claset -> int -> tactic
    82   val instp_step_tac 	: claset -> int -> tactic
    83   end;
    84 
    85 
    86 functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
    87 struct
    88 
    89 local open Data in
    90 
    91 (** Useful tactics for classical reasoning **)
    92 
    93 val imp_elim = make_elim mp;
    94 
    95 (*Solve goal that assumes both P and ~P. *)
    96 val contr_tac = eresolve_tac [not_elim]  THEN'  assume_tac;
    97 
    98 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
    99   Could do the same thing for P<->Q and P... *)
   100 fun mp_tac i = eresolve_tac [not_elim, imp_elim] i  THEN  assume_tac i;
   101 
   102 (*Like mp_tac but instantiates no variables*)
   103 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
   104 
   105 val swap = rule_by_tactic (etac thin_rl 1) (not_elim RS classical);
   106 
   107 (*Creates rules to eliminate ~A, from rules to introduce A*)
   108 fun swapify intrs = intrs RLN (2, [swap]);
   109 
   110 (*Uses introduction rules in the normal way, or on negated assumptions,
   111   trying rules in order. *)
   112 fun swap_res_tac rls = 
   113     let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
   114     in  assume_tac 	ORELSE' 
   115 	contr_tac 	ORELSE' 
   116         biresolve_tac (foldr addrl (rls,[]))
   117     end;
   118 
   119 (*Duplication of hazardous rules, for complete provers*)
   120 fun dup_intr th = standard (th RS classical);
   121 
   122 fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd |> 
   123                   rule_by_tactic (TRYALL (etac revcut_rl));
   124 
   125 
   126 (*** Classical rule sets ***)
   127 
   128 type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
   129 
   130 datatype claset =
   131   CS of {safeIs		: thm list,		(*safe introduction rules*)
   132 	 safeEs		: thm list,		(*safe elimination rules*)
   133 	 hazIs		: thm list,		(*unsafe introduction rules*)
   134 	 hazEs		: thm list,		(*unsafe elimination rules*)
   135 	 wrapper	: tactic->tactic,	(*for transforming step_tac*)
   136 	 safe0_netpair	: netpair,		(*nets for trivial cases*)
   137 	 safep_netpair	: netpair,		(*nets for >0 subgoals*)
   138 	 haz_netpair  	: netpair,		(*nets for unsafe rules*)
   139 	 dup_netpair	: netpair};		(*nets for duplication*)
   140 
   141 (*Desired invariants are
   142 	safe0_netpair = build safe0_brls,
   143 	safep_netpair = build safep_brls,
   144 	haz_netpair = build (joinrules(hazIs, hazEs)),
   145 	dup_netpair = build (joinrules(map dup_intr hazIs, 
   146 				       map dup_elim hazEs))}
   147 
   148 where build = build_netpair(Net.empty,Net.empty), 
   149       safe0_brls contains all brules that solve the subgoal, and
   150       safep_brls contains all brules that generate 1 or more new subgoals.
   151 Nets must be built incrementally, to save space and time.
   152 *)
   153 
   154 val empty_cs = 
   155   CS{safeIs	= [],
   156      safeEs	= [],
   157      hazIs	= [],
   158      hazEs	= [],
   159      wrapper 	= I,
   160      safe0_netpair = (Net.empty,Net.empty),
   161      safep_netpair = (Net.empty,Net.empty),
   162      haz_netpair   = (Net.empty,Net.empty),
   163      dup_netpair   = (Net.empty,Net.empty)};
   164 
   165 fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
   166  (writeln"Introduction rules";  	prths hazIs;
   167   writeln"Safe introduction rules";  	prths safeIs;
   168   writeln"Elimination rules";  		prths hazEs;
   169   writeln"Safe elimination rules";  	prths safeEs;
   170   ());
   171 
   172 fun rep_claset (CS args) = args;
   173 
   174 fun getwrapper (CS{wrapper,...}) = wrapper;
   175 
   176 
   177 (** Adding (un)safe introduction or elimination rules.
   178 
   179     In case of overlap, new rules are tried BEFORE old ones!!
   180 **)
   181 
   182 (*For use with biresolve_tac.  Combines intr rules with swap to handle negated
   183   assumptions.  Pairs elim rules with true. *)
   184 fun joinrules (intrs,elims) =  
   185     (map (pair true) (elims @ swapify intrs)  @
   186      map (pair false) intrs);
   187 
   188 (*Priority: prefer rules with fewest subgoals, 
   189   then rules added most recently (preferring the head of the list).*)
   190 fun tag_brls k [] = []
   191   | tag_brls k (brl::brls) =
   192       (1000000*subgoals_of_brl brl + k, brl) :: 
   193       tag_brls (k+1) brls;
   194 
   195 fun insert_tagged_list kbrls np = foldr insert_tagged_brl (kbrls, np);
   196 
   197 (*Insert into netpair that already has nI intr rules and nE elim rules.
   198   Count the intr rules double (to account for swapify).  Negate to give the
   199   new insertions the lowest priority.*)
   200 fun insert (nI,nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
   201 
   202 
   203 (** Safe rules **)
   204 
   205 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   206 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
   207     addSIs  ths  =
   208   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   209           take_prefix (fn rl => nprems_of rl=0) ths
   210       val nI = length safeIs + length ths
   211       and nE = length safeEs
   212   in CS{safeIs	= ths@safeIs,
   213         safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
   214 	safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
   215 	safeEs	= safeEs,
   216 	hazIs	= hazIs,
   217 	hazEs	= hazEs,
   218 	wrapper = wrapper,
   219 	haz_netpair = haz_netpair,
   220 	dup_netpair = dup_netpair}
   221   end;
   222 
   223 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   224 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
   225     addSEs  ths  =
   226   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   227           take_prefix (fn rl => nprems_of rl=1) ths
   228       val nI = length safeIs
   229       and nE = length safeEs + length ths
   230   in 
   231      CS{safeEs	= ths@safeEs,
   232         safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
   233 	safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   234 	safeIs	= safeIs,
   235 	hazIs	= hazIs,
   236 	hazEs	= hazEs,
   237 	wrapper = wrapper,
   238 	haz_netpair = haz_netpair,
   239 	dup_netpair = dup_netpair}
   240   end;
   241 
   242 fun cs addSDs ths = cs addSEs (map make_elim ths);
   243 
   244 
   245 (** Hazardous (unsafe) rules **)
   246 
   247 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   248 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
   249     addIs  ths  =
   250   let val nI = length hazIs + length ths
   251       and nE = length hazEs
   252   in 
   253      CS{hazIs	= ths@hazIs,
   254 	haz_netpair = insert (nI,nE) (ths, []) haz_netpair,
   255 	dup_netpair = insert (nI,nE) (map dup_intr ths, []) dup_netpair,
   256 	safeIs 	= safeIs, 
   257 	safeEs	= safeEs,
   258 	hazEs	= hazEs,
   259 	wrapper 	= wrapper,
   260 	safe0_netpair = safe0_netpair,
   261 	safep_netpair = safep_netpair}
   262   end;
   263 
   264 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   265 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
   266     addEs  ths  =
   267   let val nI = length hazIs 
   268       and nE = length hazEs + length ths
   269   in 
   270      CS{hazEs	= ths@hazEs,
   271 	haz_netpair = insert (nI,nE) ([], ths) haz_netpair,
   272 	dup_netpair = insert (nI,nE) ([], map dup_elim ths) dup_netpair,
   273 	safeIs	= safeIs, 
   274 	safeEs	= safeEs,
   275 	hazIs	= hazIs,
   276 	wrapper	= wrapper,
   277 	safe0_netpair = safe0_netpair,
   278 	safep_netpair = safep_netpair}
   279   end;
   280 
   281 fun cs addDs ths = cs addEs (map make_elim ths);
   282 
   283 
   284 (** Setting or modifying the wrapper tactical **)
   285 
   286 (*Set a new wrapper*)
   287 fun (CS{safeIs, safeEs, hazIs, hazEs, 
   288 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
   289     setwrapper new_wrapper  =
   290   CS{wrapper 	= new_wrapper,
   291      safeIs	= safeIs,
   292      safeEs	= safeEs,
   293      hazIs	= hazIs,
   294      hazEs	= hazEs,
   295      safe0_netpair = safe0_netpair,
   296      safep_netpair = safep_netpair,
   297      haz_netpair = haz_netpair,
   298      dup_netpair = dup_netpair};
   299 
   300 (*Compose a tactical with the existing wrapper*)
   301 fun cs compwrapper wrapper' = cs setwrapper (wrapper' o getwrapper cs);
   302 
   303 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
   304   as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
   305 fun tac1 THEN_MAYBE tac2 = 
   306   STATE (fn state =>
   307 	 tac1  THEN  
   308 	 COND (has_fewer_prems (nprems_of state)) all_tac tac2);
   309 
   310 (*Cause a tactic to be executed before/after the step tactic*)
   311 fun cs addbefore tac2 = cs compwrapper (fn tac1 => tac2 THEN_MAYBE tac1);
   312 fun cs addafter tac2  = cs compwrapper (fn tac1 => tac1 THEN_MAYBE tac2);
   313 
   314 
   315 
   316 (*** Simple tactics for theorem proving ***)
   317 
   318 (*Attack subgoals using safe inferences -- matching, not resolution*)
   319 fun safe_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
   320   FIRST' [eq_assume_tac,
   321 	  eq_mp_tac,
   322 	  bimatch_from_nets_tac safe0_netpair,
   323 	  FIRST' hyp_subst_tacs,
   324 	  bimatch_from_nets_tac safep_netpair] ;
   325 
   326 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   327 fun safe_tac cs = REPEAT_DETERM_FIRST (safe_step_tac cs);
   328 
   329 (*But these unsafe steps at least solve a subgoal!*)
   330 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   331   assume_tac 			  APPEND' 
   332   contr_tac 			  APPEND' 
   333   biresolve_from_nets_tac safe0_netpair;
   334 
   335 (*These are much worse since they could generate more and more subgoals*)
   336 fun instp_step_tac (CS{safep_netpair,...}) =
   337   biresolve_from_nets_tac safep_netpair;
   338 
   339 (*These steps could instantiate variables and are therefore unsafe.*)
   340 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
   341 
   342 fun haz_step_tac (CS{haz_netpair,...}) = 
   343   biresolve_from_nets_tac haz_netpair;
   344 
   345 (*Single step for the prover.  FAILS unless it makes progress. *)
   346 fun step_tac cs i = 
   347   getwrapper cs 
   348     (FIRST [safe_tac cs, inst_step_tac cs i, haz_step_tac cs i]);
   349 
   350 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   351   allows backtracking from "safe" rules to "unsafe" rules here.*)
   352 fun slow_step_tac cs i = 
   353   getwrapper cs 
   354     (safe_tac cs ORELSE (inst_step_tac cs i APPEND haz_step_tac cs i));
   355 
   356 (*** The following tactics all fail unless they solve one goal ***)
   357 
   358 (*Dumb but fast*)
   359 fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   360 
   361 (*Slower but smarter than fast_tac*)
   362 fun best_tac cs = 
   363   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
   364 
   365 fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   366 
   367 fun slow_best_tac cs = 
   368   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
   369 
   370 
   371 (*** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   372   of much experimentation!  Changing APPEND to ORELSE below would prove
   373   easy theorems faster, but loses completeness -- and many of the harder
   374   theorems such as 43. ***)
   375 
   376 (*Non-deterministic!  Could always expand the first unsafe connective.
   377   That's hard to implement and did not perform better in experiments, due to
   378   greater search depth required.*)
   379 fun dup_step_tac (cs as (CS{dup_netpair,...})) = 
   380   biresolve_from_nets_tac dup_netpair;
   381 
   382 (*Searching to depth m.*)
   383 fun depth_tac cs m i = STATE(fn state => 
   384   SELECT_GOAL 
   385     (REPEAT_DETERM1 (safe_step_tac cs 1) THEN_ELSE
   386      (DEPTH_SOLVE (depth_tac cs m 1),
   387       inst0_step_tac cs 1  APPEND
   388       COND (K(m=0)) no_tac
   389         ((instp_step_tac cs 1 APPEND dup_step_tac cs 1)
   390 	 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))))
   391   i);
   392 
   393 (*Iterative deepening tactical.  Allows us to "deepen" any search tactic*)
   394 fun DEEPEN tacf m i = STATE(fn state => 
   395    if has_fewer_prems i state then no_tac
   396    else (writeln ("Depth = " ^ string_of_int m);
   397 	 tacf m i  ORELSE  DEEPEN tacf (m+2) i));
   398 
   399 fun safe_depth_tac cs m = 
   400   SUBGOAL 
   401     (fn (prem,i) =>
   402       let val deti =
   403 	  (*No Vars in the goal?  No need to backtrack between goals.*)
   404 	  case term_vars prem of
   405 	      []	=> DETERM 
   406 	    | _::_	=> I
   407       in  SELECT_GOAL (TRY (safe_tac cs) THEN 
   408 		       DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   409       end);
   410 
   411 fun deepen_tac cs = DEEPEN (safe_depth_tac cs);
   412 
   413 end; 
   414 end;