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