src/Provers/classical.ML
author lcp
Thu Mar 30 13:44:34 1995 +0200 (1995-03-30 ago)
changeset 982 4fe0b642b7d5
parent 747 bdc066781063
child 1010 a7693f30065d
permissions -rw-r--r--
Addition of wrappers for integration with the simplifier.
New infixes setwrapper compwrapper addbefore addafter. New function
getwrapper. The wrapper is a tactical that is applied to the step tactic. By
default it is the identity. Using THEN one can cause other tactics to be
tried before or after the step tactic. Other effects are possible using
ORELSE, etc.
clasohm@0
     1
(*  Title: 	Provers/classical
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Theorem prover for classical reasoning, including predicate calculus, set
clasohm@0
     7
theory, etc.
clasohm@0
     8
clasohm@0
     9
Rules must be classified as intr, elim, safe, hazardous.
clasohm@0
    10
clasohm@0
    11
A rule is unsafe unless it can be applied blindly without harmful results.
clasohm@0
    12
For a rule to be safe, its premises and conclusion should be logically
clasohm@0
    13
equivalent.  There should be no variables in the premises that are not in
clasohm@0
    14
the conclusion.
clasohm@0
    15
*)
clasohm@0
    16
lcp@982
    17
infix 1 THEN_MAYBE;
lcp@982
    18
clasohm@0
    19
signature CLASSICAL_DATA =
clasohm@0
    20
  sig
lcp@681
    21
  val mp	: thm    	(* [| P-->Q;  P |] ==> Q *)
lcp@681
    22
  val not_elim	: thm		(* [| ~P;  P |] ==> R *)
lcp@681
    23
  val classical	: thm		(* (~P ==> P) ==> P *)
lcp@681
    24
  val sizef 	: thm -> int	(* size function for BEST_FIRST *)
clasohm@0
    25
  val hyp_subst_tacs: (int -> tactic) list
clasohm@0
    26
  end;
clasohm@0
    27
clasohm@0
    28
(*Higher precedence than := facilitates use of references*)
lcp@982
    29
infix 4 addSIs addSEs addSDs addIs addEs addDs 
lcp@982
    30
        setwrapper compwrapper addbefore addafter;
clasohm@0
    31
clasohm@0
    32
clasohm@0
    33
signature CLASSICAL =
clasohm@0
    34
  sig
clasohm@0
    35
  type claset
lcp@681
    36
  val empty_cs		: claset
lcp@681
    37
  val addDs 		: claset * thm list -> claset
lcp@681
    38
  val addEs 		: claset * thm list -> claset
lcp@681
    39
  val addIs 		: claset * thm list -> claset
lcp@681
    40
  val addSDs		: claset * thm list -> claset
lcp@681
    41
  val addSEs		: claset * thm list -> claset
lcp@681
    42
  val addSIs		: claset * thm list -> claset
lcp@982
    43
  val setwrapper 	: claset * (tactic->tactic) -> claset
lcp@982
    44
  val compwrapper 	: claset * (tactic->tactic) -> claset
lcp@982
    45
  val addbefore 	: claset * tactic -> claset
lcp@982
    46
  val addafter 		: claset * tactic -> claset
lcp@982
    47
lcp@681
    48
  val print_cs		: claset -> unit
lcp@681
    49
  val rep_claset	: claset -> {safeIs: thm list, safeEs: thm list, 
lcp@982
    50
				     hazIs: thm list, hazEs: thm list,
lcp@982
    51
				     wrapper: tactic -> tactic}
lcp@982
    52
  val getwrapper	: claset -> tactic -> tactic
lcp@982
    53
  val THEN_MAYBE	: tactic * tactic -> tactic
lcp@982
    54
lcp@681
    55
  val best_tac 		: claset -> int -> tactic
lcp@681
    56
  val contr_tac 	: int -> tactic
lcp@681
    57
  val depth_tac		: claset -> int -> int -> tactic
lcp@681
    58
  val deepen_tac	: claset -> int -> int -> tactic
lcp@681
    59
  val dup_elim		: thm -> thm
lcp@681
    60
  val dup_intr		: thm -> thm
lcp@681
    61
  val dup_step_tac	: claset -> int -> tactic
lcp@681
    62
  val eq_mp_tac		: int -> tactic
lcp@681
    63
  val fast_tac 		: claset -> int -> tactic
lcp@681
    64
  val haz_step_tac 	: claset -> int -> tactic
lcp@681
    65
  val joinrules 	: thm list * thm list -> (bool * thm) list
lcp@681
    66
  val mp_tac		: int -> tactic
lcp@681
    67
  val safe_tac 		: claset -> tactic
lcp@681
    68
  val safe_step_tac 	: claset -> int -> tactic
lcp@681
    69
  val slow_step_tac 	: claset -> int -> tactic
lcp@681
    70
  val slow_best_tac 	: claset -> int -> tactic
lcp@681
    71
  val slow_tac 		: claset -> int -> tactic
lcp@681
    72
  val step_tac 		: claset -> int -> tactic
lcp@681
    73
  val swap		: thm                 (* ~P ==> (~Q ==> P) ==> Q *)
lcp@681
    74
  val swapify 		: thm list -> thm list
lcp@681
    75
  val swap_res_tac 	: thm list -> int -> tactic
lcp@681
    76
  val inst_step_tac 	: claset -> int -> tactic
lcp@747
    77
  val inst0_step_tac 	: claset -> int -> tactic
lcp@747
    78
  val instp_step_tac 	: claset -> int -> tactic
clasohm@0
    79
  end;
clasohm@0
    80
clasohm@0
    81
clasohm@0
    82
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
clasohm@0
    83
struct
clasohm@0
    84
clasohm@0
    85
local open Data in
clasohm@0
    86
clasohm@0
    87
(** Useful tactics for classical reasoning **)
clasohm@0
    88
clasohm@0
    89
val imp_elim = make_elim mp;
clasohm@0
    90
clasohm@0
    91
(*Solve goal that assumes both P and ~P. *)
clasohm@0
    92
val contr_tac = eresolve_tac [not_elim]  THEN'  assume_tac;
clasohm@0
    93
lcp@681
    94
(*Finds P-->Q and P in the assumptions, replaces implication by Q.
lcp@681
    95
  Could do the same thing for P<->Q and P... *)
lcp@681
    96
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i  THEN  assume_tac i;
clasohm@0
    97
clasohm@0
    98
(*Like mp_tac but instantiates no variables*)
lcp@681
    99
fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
lcp@681
   100
lcp@681
   101
val swap = rule_by_tactic (etac thin_rl 1) (not_elim RS classical);
clasohm@0
   102
clasohm@0
   103
(*Creates rules to eliminate ~A, from rules to introduce A*)
clasohm@0
   104
fun swapify intrs = intrs RLN (2, [swap]);
clasohm@0
   105
clasohm@0
   106
(*Uses introduction rules in the normal way, or on negated assumptions,
clasohm@0
   107
  trying rules in order. *)
clasohm@0
   108
fun swap_res_tac rls = 
lcp@54
   109
    let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
lcp@54
   110
    in  assume_tac 	ORELSE' 
lcp@54
   111
	contr_tac 	ORELSE' 
lcp@54
   112
        biresolve_tac (foldr addrl (rls,[]))
clasohm@0
   113
    end;
clasohm@0
   114
lcp@681
   115
(*Duplication of hazardous rules, for complete provers*)
lcp@681
   116
fun dup_intr th = standard (th RS classical);
lcp@681
   117
lcp@681
   118
fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd |> 
lcp@681
   119
                  rule_by_tactic (TRYALL (etac revcut_rl));
clasohm@0
   120
clasohm@0
   121
(*** Classical rule sets ***)
clasohm@0
   122
clasohm@0
   123
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
clasohm@0
   124
clasohm@0
   125
datatype claset =
lcp@982
   126
  CS of {safeIs		: thm list,		(*safe introduction rules*)
lcp@982
   127
	 safeEs		: thm list,		(*safe elimination rules*)
lcp@982
   128
	 hazIs		: thm list,		(*unsafe introduction rules*)
lcp@982
   129
	 hazEs		: thm list,		(*unsafe elimination rules*)
lcp@982
   130
	 wrapper	: tactic->tactic,	(*for transforming step_tac*)
lcp@982
   131
	 safe0_netpair	: netpair,		(*nets for trivial cases*)
lcp@982
   132
	 safep_netpair	: netpair,		(*nets for >0 subgoals*)
lcp@982
   133
	 haz_netpair  	: netpair,		(*nets for unsafe rules*)
lcp@982
   134
	 dup_netpair	: netpair};		(*nets for duplication*)
clasohm@0
   135
lcp@982
   136
fun rep_claset (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) = 
lcp@982
   137
    {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper};
clasohm@0
   138
lcp@982
   139
fun getwrapper (CS{wrapper,...}) = wrapper;
lcp@982
   140
lcp@982
   141
(*For use with biresolve_tac.  Combines intr rules with swap to handle negated
lcp@982
   142
  assumptions.  Pairs elim rules with true.  Sorts the list of pairs by 
lcp@982
   143
  the number of new subgoals generated. *)
clasohm@0
   144
fun joinrules (intrs,elims) =  
clasohm@0
   145
  sort lessb 
clasohm@0
   146
    (map (pair true) (elims @ swapify intrs)  @
clasohm@0
   147
     map (pair false) intrs);
clasohm@0
   148
lcp@681
   149
val build = build_netpair(Net.empty,Net.empty);
lcp@681
   150
clasohm@0
   151
(*Make a claset from the four kinds of rules*)
lcp@982
   152
fun make_cs {safeIs,safeEs,hazIs,hazEs,wrapper} =
clasohm@0
   153
  let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)
clasohm@0
   154
          take_prefix (fn brl => subgoals_of_brl brl=0)
clasohm@0
   155
             (joinrules(safeIs, safeEs))
clasohm@0
   156
  in CS{safeIs = safeIs, 
clasohm@0
   157
        safeEs = safeEs,
clasohm@0
   158
	hazIs = hazIs,
clasohm@0
   159
	hazEs = hazEs,
lcp@982
   160
	wrapper = wrapper,
lcp@681
   161
	safe0_netpair = build safe0_brls,
lcp@681
   162
	safep_netpair = build safep_brls,
lcp@681
   163
	haz_netpair = build (joinrules(hazIs, hazEs)),
lcp@681
   164
	dup_netpair = build (joinrules(map dup_intr hazIs, 
lcp@681
   165
				       map dup_elim hazEs))}
clasohm@0
   166
  end;
clasohm@0
   167
clasohm@0
   168
(*** Manipulation of clasets ***)
clasohm@0
   169
lcp@982
   170
val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[], wrapper=I};
clasohm@0
   171
clasohm@0
   172
fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
clasohm@0
   173
 (writeln"Introduction rules";  prths hazIs;
clasohm@0
   174
  writeln"Safe introduction rules";  prths safeIs;
clasohm@0
   175
  writeln"Elimination rules";  prths hazEs;
clasohm@0
   176
  writeln"Safe elimination rules";  prths safeEs;
clasohm@0
   177
  ());
clasohm@0
   178
lcp@982
   179
(** Adding new (un)safe introduction or elimination rules **)
clasohm@0
   180
lcp@982
   181
fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addSIs ths =
lcp@982
   182
  make_cs {safeIs=ths@safeIs, 
lcp@982
   183
	   safeEs=safeEs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper};
lcp@982
   184
lcp@982
   185
fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addSEs ths =
lcp@982
   186
  make_cs {safeEs=ths@safeEs, 
lcp@982
   187
	   safeIs=safeIs, hazIs=hazIs, hazEs=hazEs, wrapper=wrapper};
clasohm@0
   188
clasohm@0
   189
fun cs addSDs ths = cs addSEs (map make_elim ths);
clasohm@0
   190
lcp@982
   191
fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addIs ths =
lcp@982
   192
  make_cs {hazIs=ths@hazIs, 
lcp@982
   193
	   safeIs=safeIs, safeEs=safeEs, hazEs=hazEs, wrapper=wrapper};
clasohm@0
   194
lcp@982
   195
fun (CS{safeIs,safeEs,hazIs,hazEs,wrapper,...}) addEs ths =
lcp@982
   196
  make_cs {hazEs=ths@hazEs,
lcp@982
   197
	   safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, wrapper=wrapper};
clasohm@0
   198
clasohm@0
   199
fun cs addDs ths = cs addEs (map make_elim ths);
clasohm@0
   200
lcp@982
   201
(** Setting or modifying the wrapper tactical **)
lcp@982
   202
lcp@982
   203
(*Set a new wrapper*)
lcp@982
   204
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) setwrapper wrapper =
lcp@982
   205
  make_cs {wrapper=wrapper,
lcp@982
   206
	   safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
lcp@982
   207
lcp@982
   208
(*Compose a tactical with the existing wrapper*)
lcp@982
   209
fun cs compwrapper wrapper' = cs setwrapper (wrapper' o getwrapper cs);
lcp@982
   210
lcp@982
   211
(*Execute tac1, but only execute tac2 if there are at least as many subgoals
lcp@982
   212
  as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
lcp@982
   213
fun tac1 THEN_MAYBE tac2 = 
lcp@982
   214
  STATE (fn state =>
lcp@982
   215
	 tac1  THEN  
lcp@982
   216
	 COND (has_fewer_prems (nprems_of state)) all_tac tac2);
lcp@982
   217
lcp@982
   218
(*Cause a tactic to be executed before/after the step tactic*)
lcp@982
   219
fun cs addbefore tac2 = cs compwrapper (fn tac1 => tac2 THEN_MAYBE tac1);
lcp@982
   220
fun cs addafter tac2  = cs compwrapper (fn tac1 => tac1 THEN_MAYBE tac2);
lcp@982
   221
lcp@982
   222
lcp@982
   223
clasohm@0
   224
(*** Simple tactics for theorem proving ***)
clasohm@0
   225
clasohm@0
   226
(*Attack subgoals using safe inferences -- matching, not resolution*)
clasohm@0
   227
fun safe_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
clasohm@0
   228
  FIRST' [eq_assume_tac,
clasohm@0
   229
	  eq_mp_tac,
clasohm@0
   230
	  bimatch_from_nets_tac safe0_netpair,
clasohm@0
   231
	  FIRST' hyp_subst_tacs,
clasohm@0
   232
	  bimatch_from_nets_tac safep_netpair] ;
clasohm@0
   233
clasohm@0
   234
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
lcp@747
   235
fun safe_tac cs = REPEAT_DETERM_FIRST (safe_step_tac cs);
lcp@747
   236
lcp@747
   237
(*But these unsafe steps at least solve a subgoal!*)
lcp@747
   238
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
lcp@747
   239
  assume_tac 			  APPEND' 
lcp@747
   240
  contr_tac 			  APPEND' 
lcp@747
   241
  biresolve_from_nets_tac safe0_netpair;
lcp@747
   242
lcp@747
   243
(*These are much worse since they could generate more and more subgoals*)
lcp@747
   244
fun instp_step_tac (CS{safep_netpair,...}) =
lcp@747
   245
  biresolve_from_nets_tac safep_netpair;
clasohm@0
   246
clasohm@0
   247
(*These steps could instantiate variables and are therefore unsafe.*)
lcp@747
   248
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
clasohm@0
   249
lcp@982
   250
fun haz_step_tac (CS{haz_netpair,...}) = 
lcp@681
   251
  biresolve_from_nets_tac haz_netpair;
lcp@681
   252
clasohm@0
   253
(*Single step for the prover.  FAILS unless it makes progress. *)
lcp@681
   254
fun step_tac cs i = 
lcp@982
   255
  getwrapper cs 
lcp@982
   256
    (FIRST [safe_tac cs, inst_step_tac cs i, haz_step_tac cs i]);
clasohm@0
   257
clasohm@0
   258
(*Using a "safe" rule to instantiate variables is unsafe.  This tactic
clasohm@0
   259
  allows backtracking from "safe" rules to "unsafe" rules here.*)
lcp@681
   260
fun slow_step_tac cs i = 
lcp@982
   261
  getwrapper cs 
lcp@982
   262
    (safe_tac cs ORELSE (inst_step_tac cs i APPEND haz_step_tac cs i));
clasohm@0
   263
clasohm@0
   264
(*** The following tactics all fail unless they solve one goal ***)
clasohm@0
   265
clasohm@0
   266
(*Dumb but fast*)
clasohm@0
   267
fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
clasohm@0
   268
clasohm@0
   269
(*Slower but smarter than fast_tac*)
clasohm@0
   270
fun best_tac cs = 
clasohm@0
   271
  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
clasohm@0
   272
clasohm@0
   273
fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
clasohm@0
   274
clasohm@0
   275
fun slow_best_tac cs = 
clasohm@0
   276
  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
clasohm@0
   277
lcp@681
   278
lcp@982
   279
(*** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
lcp@747
   280
  of much experimentation!  Changing APPEND to ORELSE below would prove
lcp@747
   281
  easy theorems faster, but loses completeness -- and many of the harder
lcp@747
   282
  theorems such as 43. ***)
lcp@681
   283
lcp@747
   284
(*Non-deterministic!  Could always expand the first unsafe connective.
lcp@747
   285
  That's hard to implement and did not perform better in experiments, due to
lcp@747
   286
  greater search depth required.*)
lcp@681
   287
fun dup_step_tac (cs as (CS{dup_netpair,...})) = 
lcp@681
   288
  biresolve_from_nets_tac dup_netpair;
lcp@681
   289
lcp@747
   290
(*Searching to depth m.*)
lcp@747
   291
fun depth_tac cs m i = STATE(fn state => 
lcp@747
   292
  SELECT_GOAL 
lcp@747
   293
    (REPEAT_DETERM1 (safe_step_tac cs 1) THEN_ELSE
lcp@747
   294
     (DEPTH_SOLVE (depth_tac cs m 1),
lcp@747
   295
      inst0_step_tac cs 1  APPEND
lcp@747
   296
      COND (K(m=0)) no_tac
lcp@747
   297
        ((instp_step_tac cs 1 APPEND dup_step_tac cs 1)
lcp@747
   298
	 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))))
lcp@747
   299
  i);
lcp@747
   300
lcp@747
   301
(*Iterative deepening tactical.  Allows us to "deepen" any search tactic*)
lcp@747
   302
fun DEEPEN tacf m i = STATE(fn state => 
lcp@747
   303
   if has_fewer_prems i state then no_tac
lcp@747
   304
   else (writeln ("Depth = " ^ string_of_int m);
lcp@747
   305
	 tacf m i  ORELSE  DEEPEN tacf (m+2) i));
lcp@747
   306
lcp@747
   307
fun safe_depth_tac cs m = 
lcp@681
   308
  SUBGOAL 
lcp@681
   309
    (fn (prem,i) =>
lcp@681
   310
      let val deti =
lcp@681
   311
	  (*No Vars in the goal?  No need to backtrack between goals.*)
lcp@681
   312
	  case term_vars prem of
lcp@681
   313
	      []	=> DETERM 
lcp@681
   314
	    | _::_	=> I
lcp@681
   315
      in  SELECT_GOAL (TRY (safe_tac cs) THEN 
lcp@747
   316
		       DEPTH_SOLVE (deti (depth_tac cs m 1))) i
lcp@747
   317
      end);
lcp@681
   318
lcp@747
   319
fun deepen_tac cs = DEEPEN (safe_depth_tac cs);
lcp@681
   320
clasohm@0
   321
end; 
clasohm@0
   322
end;