src/Provers/blast.ML
author paulson
Tue, 12 Jul 2005 12:49:46 +0200
changeset 16774 515b6020cf5d
parent 15786 81e9f17823ea
child 16859 8ac6d4902b56
permissions -rw-r--r--
experimental code to reduce the amount of type information in blast
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4078
c107ab1c7626 adapted to new implicit claset mechanism;
wenzelm
parents: 4065
diff changeset
     1
(*  Title: 	Provers/blast.ML
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     2
    ID:         $Id$
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
     4
    Copyright   1997  University of Cambridge
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     5
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     6
Generic tableau prover with proof reconstruction
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     7
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
     8
  SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules??
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     9
  Needs explicit instantiation of assumptions?
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    10
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    11
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    12
Blast_tac is often more powerful than fast_tac, but has some limitations.
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    13
Blast_tac...
4651
70dd492a1698 changed wrapper mechanism of classical reasoner
oheimb
parents: 4511
diff changeset
    14
  * ignores wrappers (addss, addbefore, addafter, addWrapper, ...); 
70dd492a1698 changed wrapper mechanism of classical reasoner
oheimb
parents: 4511
diff changeset
    15
    this restriction is intrinsic
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    16
  * ignores elimination rules that don't have the correct format
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    17
	(conclusion must be a formula variable)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    18
  * ignores types, which can make HOL proofs fail
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    19
  * rules must not require higher-order unification, e.g. apply_type in ZF
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    20
    + message "Function Var's argument not a bound variable" relates to this
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    21
  * its proof strategy is more general but can actually be slower
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    22
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    23
Known problems:
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
    24
  "Recursive" chains of rules can sometimes exclude other unsafe formulae
3021
39806db47be9 Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents: 2999
diff changeset
    25
	from expansion.  This happens because newly-created formulae always
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
    26
	have priority over existing ones.  But obviously recursive rules 
15661
9ef583b08647 reverted renaming of Some/None in comments and strings;
wenzelm
parents: 15574
diff changeset
    27
	such as transitivity are treated specially to prevent this.  Sometimes
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
    28
	the formulae get into the wrong order (see WRONG below).
3021
39806db47be9 Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents: 2999
diff changeset
    29
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    30
  With substition for equalities (hyp_subst_tac):
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
    31
        When substitution affects a haz formula or literal, it is moved
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    32
        back to the list of safe formulae.
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    33
        But there's no way of putting it in the right place.  A "moved" or
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    34
        "no DETERM" flag would prevent proofs failing here.
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    35
*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    36
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    37
(*Should be a type abbreviation?*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    38
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    39
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    40
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    41
(*Assumptions about constants:
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    42
  --The negation symbol is "Not"
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    43
  --The equality symbol is "op ="
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    44
  --The is-true judgement symbol is "Trueprop"
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    45
  --There are no constants named "*Goal* or "*False*"
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    46
*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    47
signature BLAST_DATA =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    48
  sig
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    49
  type claset
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    50
  val notE		: thm		(* [| ~P;  P |] ==> R *)
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
    51
  val is_hol    : bool      (*Is this HOL or FOL/ZF?*)	
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    52
  val ccontr		: thm		
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    53
  val contr_tac 	: int -> tactic
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    54
  val dup_intr		: thm -> thm
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
    55
  val hyp_subst_tac     : bool ref -> int -> tactic
4078
c107ab1c7626 adapted to new implicit claset mechanism;
wenzelm
parents: 4065
diff changeset
    56
  val claset		: unit -> claset
4653
d60f76680bf4 renamed rep_claset to rep_cs
oheimb
parents: 4651
diff changeset
    57
  val rep_cs	: (* dependent on classical.ML *)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    58
      claset -> {safeIs: thm list, safeEs: thm list, 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    59
		 hazIs: thm list, hazEs: thm list,
4651
70dd492a1698 changed wrapper mechanism of classical reasoner
oheimb
parents: 4511
diff changeset
    60
		 swrappers: (string * wrapper) list, 
70dd492a1698 changed wrapper mechanism of classical reasoner
oheimb
parents: 4511
diff changeset
    61
		 uwrappers: (string * wrapper) list,
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    62
		 safe0_netpair: netpair, safep_netpair: netpair,
12403
3e3bd3d449b5 tuned xtra_netpair;
wenzelm
parents: 12371
diff changeset
    63
		 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
7272
d20f51e43909 Method.modifier;
wenzelm
parents: 7155
diff changeset
    64
  val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
7559
1d2c099e98f7 setup for refined facts handling;
wenzelm
parents: 7272
diff changeset
    65
  val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    66
  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    67
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    68
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    69
signature BLAST =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    70
  sig
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    71
  type claset 
4233
85d004a96b98 Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
paulson
parents: 4196
diff changeset
    72
  exception TRANS of string    (*reports translation errors*)
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    73
  datatype term = 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    74
      Const of string
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
    75
    | TConst of string * term
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    76
    | Skolem of string * term option ref list
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    77
    | Free  of string
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    78
    | Var   of term option ref
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    79
    | Bound of int
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    80
    | Abs   of string*term
15786
81e9f17823ea Added op in front of constructor for better parsing.
gagern
parents: 15661
diff changeset
    81
    | op $  of term*term;
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    82
  type branch
2883
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
    83
  val depth_tac 	: claset -> int -> int -> tactic
15162
670ab8497818 depth limit (previously hard-coded with a value of 20) made a reference
webertj
parents: 14984
diff changeset
    84
  val depth_limit : int ref
2883
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
    85
  val blast_tac 	: claset -> int -> tactic
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
    86
  val Blast_tac 	: int -> tactic
5926
58f9ca06b76b method setup;
wenzelm
parents: 5734
diff changeset
    87
  val setup		: (theory -> theory) list
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    88
  (*debugging tools*)
4323
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
    89
  val stats	        : bool ref
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    90
  val trace	        : bool ref
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    91
  val fullTrace	        : branch list list ref
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
    92
  val fromType	        : (indexname * term) list ref -> Term.typ -> term
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
    93
  val fromTerm	        : Term.term -> term
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
    94
  val fromSubgoal       : Term.term -> term
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
    95
  val instVars          : term -> (unit -> unit)
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    96
  val toTerm	        : int -> term -> Term.term
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    97
  val readGoal          : Sign.sg -> string -> term
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    98
  val tryInThy		: theory -> int -> string ->
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
    99
		  (int->tactic) list * branch list list * (int*int*exn) list
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   100
  val trygl		: claset -> int -> int ->
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   101
		  (int->tactic) list * branch list list * (int*int*exn) list
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   102
  val Trygl		: int -> int -> 
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   103
                  (int->tactic) list * branch list list * (int*int*exn) list
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   104
  val normBr		: branch -> branch
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   105
  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   106
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   107
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   108
functor BlastFun(Data: BLAST_DATA) : BLAST = 
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   109
struct
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   110
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   111
type claset = Data.claset;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   112
4323
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
   113
val trace = ref false
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
   114
and stats = ref false;   (*for runtime and search statistics*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   115
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   116
datatype term = 
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   117
    Const  of string
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   118
  | TConst of string * term    (*type of overloaded constant--as a term!*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   119
  | Skolem of string * term option ref list
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   120
  | Free   of string
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   121
  | Var    of term option ref
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   122
  | Bound  of int
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   123
  | Abs    of string*term
5613
5cb6129566e7 MLWorks demands the "op" before $
paulson
parents: 5481
diff changeset
   124
  | op $   of term*term;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   125
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   126
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   127
(** Basic syntactic operations **)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   128
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   129
fun is_Var (Var _) = true
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   130
  | is_Var _ = false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   131
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   132
fun dest_Var (Var x) =  x;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   133
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   134
fun rand (f$x) = x;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   135
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   136
(* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   137
val list_comb : term * term list -> term = Library.foldl (op $);
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   138
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   139
(* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   140
fun strip_comb u : term * term list = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   141
    let fun stripc (f$t, ts) = stripc (f, t::ts)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   142
        |   stripc  x =  x 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   143
    in  stripc(u,[])  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   144
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   145
(* maps   f(t1,...,tn)  to  f , which is never a combination *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   146
fun head_of (f$t) = head_of f
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   147
  | head_of u = u;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   148
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   149
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   150
(** Particular constants **)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   151
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   152
fun negate P = Const"Not" $ P;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   153
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   154
fun mkGoal P = Const"*Goal*" $ P;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   155
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   156
fun isGoal (Const"*Goal*" $ _) = true
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   157
  | isGoal _                   = false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   158
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   159
val boolT = if Data.is_hol then "bool" else "o";
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   160
val Trueprop = Term.Const("Trueprop", Type(boolT,[])-->propT);
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   161
fun mk_tprop P = Term.$ (Trueprop, P);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   162
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   163
fun isTrueprop (Term.Const("Trueprop",_)) = true
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   164
  | isTrueprop _                          = false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   165
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   166
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   167
(*** Dealing with overloaded constants ***)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   168
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   169
(*alist is a map from TVar names to Vars.  We need to unify the TVars
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   170
  faithfully in order to track overloading*)
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   171
fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a, map (fromType alist) Ts)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   172
  | fromType alist (Term.TFree(a,_)) = Free a
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   173
  | fromType alist (Term.TVar (ixn,_)) =
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   174
	      (case (assoc_string_int(!alist,ixn)) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   175
		   NONE => let val t' = Var(ref NONE)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   176
		           in  alist := (ixn, t') :: !alist;  t'
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   177
			   end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   178
		 | SOME v => v)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   179
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   180
(*Definitions of the theory in which blast is initialized.*)
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   181
val curr_defs = ref Defs.empty;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   182
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   183
(*Types aren't needed if the constant has at most one definition and is monomorphic*)
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   184
fun no_types_needed s =
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   185
  (case Defs.overloading_info (!curr_defs) s of
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   186
      NONE => true
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   187
    | SOME (T,defs,_) => length defs <= 1 andalso null (typ_tvars T))
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   188
  handle Option => (warning ("Defs.overloading_info failed for " ^ s); false);
11119
2d92ab19747b new function get_overloads
paulson
parents: 10400
diff changeset
   189
13550
5a176b8dda84 removal of blast.overloaded
paulson
parents: 12902
diff changeset
   190
(*Convert a Term.Const to a Blast.Const or Blast.TConst,
5a176b8dda84 removal of blast.overloaded
paulson
parents: 12902
diff changeset
   191
  converting its type to a Blast.term in the latter case.
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   192
  For efficiency, Const is used for FOL and for the logical constants.
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   193
  We can't use it for all non-overloaded operators because some preservation
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   194
  of type information is necessary to prevent PROOF FAILED elsewhere.*)
13550
5a176b8dda84 removal of blast.overloaded
paulson
parents: 12902
diff changeset
   195
fun fromConst alist (a,T) = 
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   196
    if not Data.is_hol orelse a mem_string ["All","Ex","all"] orelse no_types_needed a 
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   197
	then Const a 
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   198
	else TConst(a, fromType alist T);
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   199
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   200
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   201
(*Tests whether 2 terms are alpha-convertible; chases instantiations*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   202
fun (Const a)      aconv (Const b)      = a=b
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   203
  | (TConst (a,ta)) aconv (TConst (b,tb)) = a=b andalso ta aconv tb
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   204
  | (Skolem (a,_)) aconv (Skolem (b,_)) = a=b  (*arglists must then be equal*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   205
  | (Free a)       aconv (Free b)       = a=b
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   206
  | (Var(ref(SOME t))) aconv u          = t aconv u
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   207
  | t          aconv (Var(ref(SOME u))) = t aconv u
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   208
  | (Var v)        aconv (Var w)        = v=w	(*both Vars are un-assigned*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   209
  | (Bound i)      aconv (Bound j)      = i=j
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   210
  | (Abs(_,t))     aconv (Abs(_,u))     = t aconv u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   211
  | (f$t)          aconv (g$u)          = (f aconv g) andalso (t aconv u)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   212
  | _ aconv _  =  false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   213
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   214
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   215
fun mem_term (_, [])     = false
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   216
  | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   217
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   218
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   219
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   220
fun mem_var (v: term option ref, []) = false
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   221
  | mem_var (v, v'::vs)              = v=v' orelse mem_var(v,vs);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   222
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   223
fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   224
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   225
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   226
(** Vars **)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   227
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   228
(*Accumulates the Vars in the term, suppressing duplicates*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   229
fun add_term_vars (Skolem(a,args),	vars) = add_vars_vars(args,vars)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   230
  | add_term_vars (Var (v as ref NONE),	vars) = ins_var (v, vars)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   231
  | add_term_vars (Var (ref (SOME u)), vars)  = add_term_vars(u,vars)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   232
  | add_term_vars (TConst (_,t),	vars) = add_term_vars(t,vars)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   233
  | add_term_vars (Abs (_,body),	vars) = add_term_vars(body,vars)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   234
  | add_term_vars (f$t,	vars) =  add_term_vars (f, add_term_vars(t, vars))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   235
  | add_term_vars (_,	vars) = vars
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   236
(*Term list version.  [The fold functionals are slow]*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   237
and add_terms_vars ([],    vars) = vars
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   238
  | add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   239
(*Var list version.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   240
and add_vars_vars ([],    vars) = vars
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   241
  | add_vars_vars (ref (SOME u) :: vs, vars) = 
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   242
	add_vars_vars (vs, add_term_vars(u,vars))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   243
  | add_vars_vars (v::vs, vars) =   (*v must be a ref NONE*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   244
	add_vars_vars (vs, ins_var (v, vars));
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   245
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   246
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   247
(*Chase assignments in "vars"; return a list of unassigned variables*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   248
fun vars_in_vars vars = add_vars_vars(vars,[]);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   249
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   250
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   251
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   252
(*increment a term's non-local bound variables
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   253
     inc is  increment for bound variables
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   254
     lev is  level at which a bound variable is considered 'loose'*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   255
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   256
  | incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   257
  | incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   258
  | incr_bv (inc, lev, u) = u;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   259
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   260
fun incr_boundvars  0  t = t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   261
  | incr_boundvars inc t = incr_bv(inc,0,t);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   262
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   263
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   264
(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   265
   (Bound 0) is loose at level 0 *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   266
fun add_loose_bnos (Bound i, lev, js)   = if i<lev then js  
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   267
					  else  (i-lev) ins_int js
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   268
  | add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   269
  | add_loose_bnos (f$t, lev, js)       =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   270
	        add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   271
  | add_loose_bnos (_, _, js)           = js;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   272
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   273
fun loose_bnos t = add_loose_bnos (t, 0, []);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   274
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   275
fun subst_bound (arg, t) : term = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   276
  let fun subst (t as Bound i, lev) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   277
 	    if i<lev then  t    (*var is locally bound*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   278
	    else  if i=lev then incr_boundvars lev arg
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   279
		           else Bound(i-1)  (*loose: change it*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   280
	| subst (Abs(a,body), lev) = Abs(a, subst(body,lev+1))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   281
	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   282
	| subst (t,lev)    = t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   283
  in  subst (t,0)  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   284
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   285
3101
e8a92f497295 Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents: 3092
diff changeset
   286
(*Normalize...but not the bodies of ABSTRACTIONS*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   287
fun norm t = case t of
2952
ea834e8fac1b Changed penalty from log2 to log3
paulson
parents: 2924
diff changeset
   288
    Skolem (a,args)      => Skolem(a, vars_in_vars args)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   289
  | TConst(a,aT)         => TConst(a, norm aT)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   290
  | (Var (ref NONE))     => t
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   291
  | (Var (ref (SOME u))) => norm u
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   292
  | (f $ u) => (case norm f of
3101
e8a92f497295 Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents: 3092
diff changeset
   293
                    Abs(_,body) => norm (subst_bound (u, body))
e8a92f497295 Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents: 3092
diff changeset
   294
                  | nf => nf $ norm u)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   295
  | _ => t;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   296
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   297
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   298
(*Weak (one-level) normalize for use in unification*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   299
fun wkNormAux t = case t of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   300
    (Var v) => (case !v of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   301
		    SOME u => wkNorm u
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   302
		  | NONE   => t)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   303
  | (f $ u) => (case wkNormAux f of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   304
		    Abs(_,body) => wkNorm (subst_bound (u, body))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   305
		  | nf          => nf $ u)
2952
ea834e8fac1b Changed penalty from log2 to log3
paulson
parents: 2924
diff changeset
   306
  | Abs (a,body) =>	(*eta-contract if possible*)
ea834e8fac1b Changed penalty from log2 to log3
paulson
parents: 2924
diff changeset
   307
	(case wkNormAux body of
ea834e8fac1b Changed penalty from log2 to log3
paulson
parents: 2924
diff changeset
   308
	     nb as (f $ t) => 
ea834e8fac1b Changed penalty from log2 to log3
paulson
parents: 2924
diff changeset
   309
		 if (0 mem_int loose_bnos f) orelse wkNorm t <> Bound 0
ea834e8fac1b Changed penalty from log2 to log3
paulson
parents: 2924
diff changeset
   310
		 then Abs(a,nb)
ea834e8fac1b Changed penalty from log2 to log3
paulson
parents: 2924
diff changeset
   311
		 else wkNorm (incr_boundvars ~1 f)
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   312
	   | nb => Abs (a,nb))
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   313
  | _ => t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   314
and wkNorm t = case head_of t of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   315
    Const _        => t
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   316
  | TConst _       => t
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   317
  | Skolem(a,args) => t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   318
  | Free _         => t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   319
  | _              => wkNormAux t;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   320
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   321
5734
bebd10cb7a8d occurs check now handles Bound variables (for soundness)
paulson
parents: 5613
diff changeset
   322
(*Does variable v occur in u?  For unification.  
bebd10cb7a8d occurs check now handles Bound variables (for soundness)
paulson
parents: 5613
diff changeset
   323
  Dangling bound vars are also forbidden.*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   324
fun varOccur v = 
5734
bebd10cb7a8d occurs check now handles Bound variables (for soundness)
paulson
parents: 5613
diff changeset
   325
  let fun occL lev [] = false	(*same as (exists occ), but faster*)
bebd10cb7a8d occurs check now handles Bound variables (for soundness)
paulson
parents: 5613
diff changeset
   326
	| occL lev (u::us) = occ lev u orelse occL lev us
bebd10cb7a8d occurs check now handles Bound variables (for soundness)
paulson
parents: 5613
diff changeset
   327
      and occ lev (Var w) = 
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   328
	      v=w orelse
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   329
              (case !w of NONE   => false
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   330
	                | SOME u => occ lev u)
5734
bebd10cb7a8d occurs check now handles Bound variables (for soundness)
paulson
parents: 5613
diff changeset
   331
        | occ lev (Skolem(_,args)) = occL lev (map Var args)
bebd10cb7a8d occurs check now handles Bound variables (for soundness)
paulson
parents: 5613
diff changeset
   332
            (*ignore TConst, since term variables can't occur in types (?) *)
bebd10cb7a8d occurs check now handles Bound variables (for soundness)
paulson
parents: 5613
diff changeset
   333
        | occ lev (Bound i)  = lev <= i
bebd10cb7a8d occurs check now handles Bound variables (for soundness)
paulson
parents: 5613
diff changeset
   334
        | occ lev (Abs(_,u)) = occ (lev+1) u
bebd10cb7a8d occurs check now handles Bound variables (for soundness)
paulson
parents: 5613
diff changeset
   335
        | occ lev (f$u)      = occ lev u  orelse  occ lev f
bebd10cb7a8d occurs check now handles Bound variables (for soundness)
paulson
parents: 5613
diff changeset
   336
        | occ lev _          = false;
bebd10cb7a8d occurs check now handles Bound variables (for soundness)
paulson
parents: 5613
diff changeset
   337
  in  occ 0  end;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   338
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   339
exception UNIFY;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   340
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   341
val trail = ref [] : term option ref list ref;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   342
val ntrail = ref 0;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   343
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   344
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   345
(*Restore the trail to some previous state: for backtracking*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   346
fun clearTo n =
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   347
    while !ntrail<>n do
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   348
	(hd(!trail) := NONE;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   349
	 trail := tl (!trail);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   350
	 ntrail := !ntrail - 1);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   351
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   352
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   353
(*First-order unification with bound variables.  
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   354
  "vars" is a list of variables local to the rule and NOT to be put
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   355
	on the trail (no point in doing so)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   356
*)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   357
fun unify(vars,t,u) =
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   358
    let val n = !ntrail 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   359
	fun update (t as Var v, u) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   360
	    if t aconv u then ()
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   361
	    else if varOccur v u then raise UNIFY 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   362
	    else if mem_var(v, vars) then v := SOME u
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   363
		 else (*avoid updating Vars in the branch if possible!*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   364
		      if is_Var u andalso mem_var(dest_Var u, vars)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   365
		      then dest_Var u := SOME t
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   366
		      else (v := SOME u;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   367
			    trail := v :: !trail;  ntrail := !ntrail + 1)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   368
	fun unifyAux (t,u) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   369
	    case (wkNorm t,  wkNorm u) of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   370
		(nt as Var v,  nu) => update(nt,nu)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   371
	      | (nu,  nt as Var v) => update(nt,nu)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   372
	      | (TConst(a,at), TConst(b,bt)) => if a=b then unifyAux(at,bt)
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   373
		                                else raise UNIFY
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   374
	      | (Abs(_,t'),  Abs(_,u')) => unifyAux(t',u')
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   375
		    (*NB: can yield unifiers having dangling Bound vars!*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   376
	      | (f$t',  g$u') => (unifyAux(f,g); unifyAux(t',u'))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   377
	      | (nt,  nu)    => if nt aconv nu then () else raise UNIFY
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   378
    in  (unifyAux(t,u); true) handle UNIFY => (clearTo n; false)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   379
    end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   380
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   381
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   382
(*Convert from "real" terms to prototerms; eta-contract.
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   383
  Code is similar to fromSubgoal.*)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   384
fun fromTerm t =
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   385
  let val alistVar = ref []
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   386
      and alistTVar = ref []
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   387
      fun from (Term.Const aT) = fromConst alistTVar aT
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   388
	| from (Term.Free  (a,_)) = Free a
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   389
	| from (Term.Bound i)     = Bound i
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   390
	| from (Term.Var (ixn,T)) = 
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   391
	      (case (assoc_string_int(!alistVar,ixn)) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   392
		   NONE => let val t' = Var(ref NONE)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   393
		           in  alistVar := (ixn, t') :: !alistVar;  t'
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   394
			   end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   395
		 | SOME v => v)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   396
	| from (Term.Abs (a,_,u)) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   397
	      (case  from u  of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   398
		u' as (f $ Bound 0) => 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   399
		  if (0 mem_int loose_bnos f) then Abs(a,u')
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   400
		  else incr_boundvars ~1 f 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   401
	      | u' => Abs(a,u'))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   402
	| from (Term.$ (f,u)) = from f $ from u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   403
  in  from t  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   404
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   405
(*A debugging function: replaces all Vars by dummy Frees for visual inspection
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   406
  of whether they are distinct.  Function revert undoes the assignments.*)
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   407
fun instVars t =
12902
a23dc0b7566f Symbol.bump_string;
wenzelm
parents: 12403
diff changeset
   408
  let val name = ref "a"
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   409
      val updated = ref []
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   410
      fun inst (TConst(a,t)) = inst t
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   411
	| inst (Var(v as ref NONE)) = (updated := v :: (!updated);
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   412
				       v       := SOME (Free ("?" ^ !name)); 
12902
a23dc0b7566f Symbol.bump_string;
wenzelm
parents: 12403
diff changeset
   413
				       name    := Symbol.bump_string (!name))
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   414
	| inst (Abs(a,t))    = inst t
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   415
	| inst (f $ u)       = (inst f; inst u)
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   416
	| inst _             = ()
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   417
      fun revert() = List.app (fn v => v:=NONE) (!updated)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   418
  in  inst t; revert  end;
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   419
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   420
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   421
(* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   422
fun strip_imp_prems (Const"==>" $ (Const"Trueprop" $ A) $ B) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   423
           A :: strip_imp_prems B
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   424
  | strip_imp_prems (Const"==>" $ A $ B) = A :: strip_imp_prems B
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   425
  | strip_imp_prems _ = [];
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   426
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   427
(* A1==>...An==>B  goes to B, where B is not an implication *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   428
fun strip_imp_concl (Const"==>" $ A $ B) = strip_imp_concl B
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   429
  | strip_imp_concl (Const"Trueprop" $ A) = A
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   430
  | strip_imp_concl A = A : term;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   431
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   432
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   433
(*** Conversion of Elimination Rules to Tableau Operations ***)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   434
9170
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   435
exception ElimBadConcl and ElimBadPrem;
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   436
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   437
(*The conclusion becomes the goal/negated assumption *False*: delete it!
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   438
  If we don't find it then the premise is ill-formed and could cause 
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   439
  PROOF FAILED*)
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   440
fun delete_concl [] = raise ElimBadPrem
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   441
  | delete_concl (Const "*Goal*" $ (Var (ref (SOME (Const"*False*")))) :: Ps) =
9170
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   442
	Ps
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   443
  | delete_concl (Const "Not" $ (Var (ref (SOME (Const"*False*")))) :: Ps) =
9170
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   444
	Ps
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   445
  | delete_concl (P::Ps) = P :: delete_concl Ps;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   446
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   447
fun skoPrem vars (Const "all" $ Abs (_, P)) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   448
        skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   449
  | skoPrem vars P = P;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   450
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   451
fun convertPrem t = 
9170
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   452
    delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t);
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   453
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   454
(*Expects elimination rules to have a formula variable as conclusion*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   455
fun convertRule vars t =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   456
  let val (P::Ps) = strip_imp_prems t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   457
      val Var v   = strip_imp_concl t
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   458
  in  v := SOME (Const"*False*");
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   459
      (P, map (convertPrem o skoPrem vars) Ps) 
9170
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   460
  end
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   461
  handle Bind => raise ElimBadConcl;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   462
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   463
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   464
(*Like dup_elim, but puts the duplicated major premise FIRST*)
4271
3a82492e70c5 changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents: 4240
diff changeset
   465
fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   466
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   467
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   468
(*Rotate the assumptions in all new subgoals for the LIFO discipline*)
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   469
local
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   470
  (*Count new hyps so that they can be rotated*)
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   471
  fun nNewHyps []                         = 0
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   472
    | nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   473
    | nNewHyps (P::Ps)                    = 1 + nNewHyps Ps;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   474
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   475
  fun rot_tac [] i st      = Seq.single st
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   476
    | rot_tac (0::ks) i st = rot_tac ks (i+1) st
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   477
    | rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st);
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   478
in
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   479
fun rot_subgoals_tac (rot, rl) =
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   480
     rot_tac (if rot then map nNewHyps rl else []) 
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   481
end;
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   482
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   483
2999
fad7cc426242 Penalty for branching instantiations reduced from log3 to log4.
paulson
parents: 2952
diff changeset
   484
fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   485
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   486
(*Resolution/matching tactics: if upd then the proof state may be updated.
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   487
  Matching makes the tactics more deterministic in the presence of Vars.*)
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   488
fun emtac upd rl = TRACE rl (if upd then etac rl else ematch_tac [rl]);
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   489
fun rmtac upd rl = TRACE rl (if upd then rtac rl else match_tac [rl]);
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   490
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   491
(*Tableau rule from elimination rule.  
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   492
  Flag "upd" says that the inference updated the branch.
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   493
  Flag "dup" requests duplication of the affected formula.*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   494
fun fromRule vars rl = 
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   495
  let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertRule vars
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   496
      fun tac (upd, dup,rot) i = 
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   497
	emtac upd (if dup then rev_dup_elim rl else rl) i
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   498
	THEN
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   499
	rot_subgoals_tac (rot, #2 trl) i
3244
71b760618f30 Basis library version of type "option" now resides in its own structure Option
paulson
parents: 3101
diff changeset
   500
  in Option.SOME (trl, tac) end
9170
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   501
  handle ElimBadPrem => (*reject: prems don't preserve conclusion*)
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   502
	    (warning("Ignoring weak elimination rule\n" ^ string_of_thm rl);
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   503
	     Option.NONE)
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   504
       | ElimBadConcl => (*ignore: conclusion is not just a variable*)
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   505
	   (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   506
       	               "conclusion should be a variable\n" ^ string_of_thm rl))
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   507
	    else ();
0bfe5354d5e7 warns of weak elim rules and ignores them
paulson
parents: 7607
diff changeset
   508
	    Option.NONE);
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   509
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   510
3101
e8a92f497295 Again "norm" DOES NOT normalize bodies of abstractions
paulson
parents: 3092
diff changeset
   511
(*** Conversion of Introduction Rules ***)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   512
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   513
fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   514
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   515
fun convertIntrRule vars t =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   516
  let val Ps = strip_imp_prems t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   517
      val P  = strip_imp_concl t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   518
  in  (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps) 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   519
  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   520
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   521
(*Tableau rule from introduction rule.  
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   522
  Flag "upd" says that the inference updated the branch.
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   523
  Flag "dup" requests duplication of the affected formula.
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   524
  Since haz rules are now delayed, "dup" is always FALSE for
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   525
  introduction rules.*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   526
fun fromIntrRule vars rl = 
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   527
  let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertIntrRule vars
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   528
      fun tac (upd,dup,rot) i = 
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   529
	 rmtac upd (if dup then Data.dup_intr rl else rl) i
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   530
	 THEN
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   531
	 rot_subgoals_tac (rot, #2 trl) i
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   532
  in (trl, tac) end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   533
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   534
3030
04e3359921a8 Addition of printed tracing. Also some tidying
paulson
parents: 3021
diff changeset
   535
val dummyVar = Term.Var (("etc",0), dummyT);
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   536
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   537
(*Convert from prototerms to ordinary terms with dummy types
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   538
  Ignore abstractions; identify all Vars; STOP at given depth*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   539
fun toTerm 0 _             = dummyVar
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   540
  | toTerm d (Const a)     = Term.Const (a,dummyT)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   541
  | toTerm d (TConst(a,_)) = Term.Const (a,dummyT)  (*no need to convert type*)
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   542
  | toTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   543
  | toTerm d (Free a)      = Term.Free  (a,dummyT)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   544
  | toTerm d (Bound i)     = Term.Bound i
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   545
  | toTerm d (Var _)       = dummyVar
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   546
  | toTerm d (Abs(a,_))    = dummyVar
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   547
  | toTerm d (f $ u)       = Term.$ (toTerm d f, toTerm (d-1) u);
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   548
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   549
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   550
fun netMkRules P vars (nps: netpair list) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   551
  case P of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   552
      (Const "*Goal*" $ G) =>
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   553
	let val pG = mk_tprop (toTerm 2 G)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   554
	    val intrs = List.concat 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   555
		             (map (fn (inet,_) => Net.unify_term inet pG) 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   556
			      nps)
11783
aee100a086b1 Tactic.orderlist;
wenzelm
parents: 11754
diff changeset
   557
	in  map (fromIntrRule vars o #2) (Tactic.orderlist intrs)  end
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   558
    | _ =>
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   559
	let val pP = mk_tprop (toTerm 3 P)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   560
	    val elims = List.concat 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   561
		             (map (fn (_,enet) => Net.unify_term enet pP) 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   562
			      nps)
11783
aee100a086b1 Tactic.orderlist;
wenzelm
parents: 11754
diff changeset
   563
	in  List.mapPartial (fromRule vars o #2) (Tactic.orderlist elims)  end;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   564
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   565
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   566
(*Pending formulae carry md (may duplicate) flags*)
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   567
type branch = 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   568
    {pairs: ((term*bool) list *	(*safe formulae on this level*)
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   569
               (term*bool) list) list,  (*haz formulae  on this level*)
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   570
     lits:   term list,                 (*literals: irreducible formulae*)
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   571
     vars:   term option ref list,      (*variables occurring in branch*)
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   572
     lim:    int};                      (*resource limit*)
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   573
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   574
val fullTrace = ref[] : branch list list ref;
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   575
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   576
(*Normalize a branch--for tracing*)
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   577
fun norm2 (G,md) = (norm G, md);
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   578
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   579
fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs);
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   580
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   581
fun normBr {pairs, lits, vars, lim} =
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   582
     {pairs = map normLev pairs, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   583
      lits  = map norm lits, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   584
      vars  = vars, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   585
      lim   = lim};
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   586
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   587
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   588
val dummyTVar = Term.TVar(("a",0), []);
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   589
val dummyVar2 = Term.Var(("var",0), dummyT);
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   590
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   591
(*convert Blast_tac's type representation to real types for tracing*)
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   592
fun showType (Free a)  = Term.TFree (a,[])
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   593
  | showType (Var _)   = dummyTVar
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   594
  | showType t         =
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   595
      (case strip_comb t of
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   596
	   (Const a, us) => Term.Type(a, map showType us)
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   597
	 | _ => dummyT);
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   598
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   599
(*Display top-level overloading if any*)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   600
fun topType (TConst(a,t)) = SOME (showType t)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   601
  | topType (Abs(a,t))    = topType t
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
   602
  | topType (f $ u)       = (case topType f of NONE => topType u | some => some)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   603
  | topType _             = NONE;
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   604
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   605
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   606
(*Convert from prototerms to ordinary terms with dummy types for tracing*)
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   607
fun showTerm d (Const a)     = Term.Const (a,dummyT)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   608
  | showTerm d (TConst(a,_)) = Term.Const (a,dummyT)
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   609
  | showTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   610
  | showTerm d (Free a)      = Term.Free  (a,dummyT)
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   611
  | showTerm d (Bound i)     = Term.Bound i
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   612
  | showTerm d (Var(ref(SOME u))) = showTerm d u
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   613
  | showTerm d (Var(ref NONE))    = dummyVar2
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   614
  | showTerm d (Abs(a,t))    = if d=0 then dummyVar
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   615
			       else Term.Abs(a, dummyT, showTerm (d-1) t)
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   616
  | showTerm d (f $ u)       = if d=0 then dummyVar
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   617
			       else Term.$ (showTerm d f, showTerm (d-1) u);
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   618
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   619
fun string_of sign d t = Sign.string_of_term sign (showTerm d t);
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   620
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   621
fun traceTerm sign t = 
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   622
  let val t' = norm t
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   623
      val stm = string_of sign 8 t'
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   624
  in  
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   625
      case topType t' of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   626
	  NONE   => stm   (*no type to attach*)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   627
	| SOME T => stm ^ "\t:: " ^ Sign.string_of_typ sign T
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   628
  end;
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   629
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   630
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   631
(*Print tracing information at each iteration of prover*)
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   632
fun tracing sign brs = 
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14913
diff changeset
   633
  let fun printPairs (((G,_)::_,_)::_)  = immediate_output(traceTerm sign G)
edbc81e60809 immediate_output;
wenzelm
parents: 14913
diff changeset
   634
	| printPairs (([],(H,_)::_)::_) = immediate_output(traceTerm sign H ^ "\t (Unsafe)")
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   635
	| printPairs _                 = ()
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   636
      fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   637
	    (fullTrace := brs0 :: !fullTrace;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   638
	     List.app (fn _ => immediate_output "+") brs;
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14913
diff changeset
   639
	     immediate_output (" [" ^ Int.toString lim ^ "] ");
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   640
	     printPairs pairs;
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   641
	     writeln"")
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   642
  in if !trace then printBrs (map normBr brs) else ()
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   643
  end;
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   644
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   645
fun traceMsg s = if !trace then writeln s else ();
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   646
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   647
(*Tracing: variables updated in the last branch operation?*)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   648
fun traceVars sign ntrl =
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   649
  if !trace then 
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   650
      (case !ntrail-ntrl of
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   651
	    0 => ()
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14913
diff changeset
   652
	  | 1 => immediate_output"\t1 variable UPDATED:"
edbc81e60809 immediate_output;
wenzelm
parents: 14913
diff changeset
   653
	  | n => immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   654
       (*display the instantiations themselves, though no variable names*)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   655
       List.app (fn v => immediate_output("   " ^ string_of sign 4 (valOf (!v))))
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   656
           (List.take(!trail, !ntrail-ntrl));
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   657
       writeln"")
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   658
    else ();
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   659
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   660
(*Tracing: how many new branches are created?*)
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   661
fun traceNew prems =
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   662
    if !trace then 
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   663
        case length prems of
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14913
diff changeset
   664
	    0 => immediate_output"branch closed by rule"
edbc81e60809 immediate_output;
wenzelm
parents: 14913
diff changeset
   665
	  | 1 => immediate_output"branch extended (1 new subgoal)"
edbc81e60809 immediate_output;
wenzelm
parents: 14913
diff changeset
   666
	  | n => immediate_output("branch split: "^ Int.toString n ^ " new subgoals")
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   667
    else ();
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   668
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   669
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   670
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   671
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   672
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   673
(*Replace the ATOMIC term "old" by "new" in t*)  
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   674
fun subst_atomic (old,new) t =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   675
    let fun subst (Var(ref(SOME u))) = subst u
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   676
	  | subst (Abs(a,body))      = Abs(a, subst body)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   677
	  | subst (f$t)              = subst f $ subst t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   678
	  | subst t                  = if t aconv old then new else t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   679
    in  subst t  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   680
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   681
(*Eta-contract a term from outside: just enough to reduce it to an atom*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   682
fun eta_contract_atom (t0 as Abs(a, body)) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   683
      (case  eta_contract2 body  of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   684
        f $ Bound 0 => if (0 mem_int loose_bnos f) then t0
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   685
		       else eta_contract_atom (incr_boundvars ~1 f)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   686
      | _ => t0)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   687
  | eta_contract_atom t = t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   688
and eta_contract2 (f$t) = f $ eta_contract_atom t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   689
  | eta_contract2 t     = eta_contract_atom t;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   690
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   691
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   692
(*When can we safely delete the equality?
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   693
    Not if it equates two constants; consider 0=1.
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   694
    Not if it resembles x=t[x], since substitution does not eliminate x.
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   695
    Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   696
  Prefer to eliminate Bound variables if possible.
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   697
  Result:  true = use as is,  false = reorient first *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   698
4354
7f4da01bdf0e Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents: 4323
diff changeset
   699
(*Can t occur in u?  For substitution.  
7f4da01bdf0e Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents: 4323
diff changeset
   700
  Does NOT examine the args of Skolem terms: substitution does not affect them.
4196
9953c0995b79 Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents: 4149
diff changeset
   701
  REFLEXIVE because hyp_subst_tac fails on x=x.*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   702
fun substOccur t = 
4354
7f4da01bdf0e Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents: 4323
diff changeset
   703
  let (*NO vars are permitted in u except the arguments of t, if it is 
7f4da01bdf0e Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents: 4323
diff changeset
   704
        a Skolem term.  This ensures that no equations are deleted that could
7f4da01bdf0e Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents: 4323
diff changeset
   705
        be instantiated to a cycle.  For example, x=?a is rejected because ?a
7f4da01bdf0e Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents: 4323
diff changeset
   706
	could be instantiated to Suc(x).*)
7f4da01bdf0e Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents: 4323
diff changeset
   707
      val vars = case t of
7f4da01bdf0e Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents: 4323
diff changeset
   708
                     Skolem(_,vars) => vars
7f4da01bdf0e Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents: 4323
diff changeset
   709
		   | _ => []
7f4da01bdf0e Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents: 4323
diff changeset
   710
      fun occEq u = (t aconv u) orelse occ u
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   711
      and occ (Var(ref(SOME u))) = occEq u
4354
7f4da01bdf0e Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents: 4323
diff changeset
   712
        | occ (Var v)            = not (mem_var (v, vars))
7f4da01bdf0e Fixed the treatment of substitution for equations, restricting occurrences of
paulson
parents: 4323
diff changeset
   713
	| occ (Abs(_,u))         = occEq u
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   714
        | occ (f$u)              = occEq u  orelse  occEq f
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   715
        | occ (_)                = false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   716
  in  occEq  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   717
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   718
exception DEST_EQ;
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   719
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   720
(*Take apart an equality (plain or overloaded).  NO constant Trueprop*)
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   721
fun dest_eq (Const  "op ="     $ t $ u) = 
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   722
		(eta_contract_atom t, eta_contract_atom u)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   723
  | dest_eq (TConst("op =",_)  $ t $ u) = 
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   724
		(eta_contract_atom t, eta_contract_atom u)
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   725
  | dest_eq _                           = raise DEST_EQ;
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   726
4196
9953c0995b79 Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents: 4149
diff changeset
   727
(*Reject the equality if u occurs in (or equals!) t*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   728
fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   729
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   730
(*IF the goal is an equality with a substitutable variable 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   731
  THEN orient that equality ELSE raise exception DEST_EQ*)
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   732
fun orientGoal (t,u) = case (t,u) of
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   733
       (Skolem _, _) => check(t,u,(t,u))	(*eliminates t*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   734
     | (_, Skolem _) => check(u,t,(u,t))	(*eliminates u*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   735
     | (Free _, _)   => check(t,u,(t,u))	(*eliminates t*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   736
     | (_, Free _)   => check(u,t,(u,t))	(*eliminates u*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   737
     | _             => raise DEST_EQ;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   738
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   739
(*Substitute through the branch if an equality goal (else raise DEST_EQ).
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   740
  Moves affected literals back into the branch, but it is not clear where
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   741
  they should go: this could make proofs fail.*)
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   742
fun equalSubst sign (G, {pairs, lits, vars, lim}) = 
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   743
  let val (t,u) = orientGoal(dest_eq G)
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   744
      val subst = subst_atomic (t,u)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   745
      fun subst2(G,md) = (subst G, md)
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
   746
      (*substitute throughout list; extract affected formulae*)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
   747
      fun subForm ((G,md), (changed, pairs)) =
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
   748
	    let val nG = subst G
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
   749
	    in  if nG aconv G then (changed, (G,md)::pairs)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
   750
		              else ((nG,md)::changed, pairs)
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   751
            end
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
   752
      (*substitute throughout "stack frame"; extract affected formulae*)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
   753
      fun subFrame ((Gs,Hs), (changed, frames)) =
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   754
	    let val (changed', Gs') = foldr subForm (changed, []) Gs
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   755
                val (changed'', Hs') = foldr subForm (changed', []) Hs
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
   756
            in  (changed'', (Gs',Hs')::frames)  end
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
   757
      (*substitute throughout literals; extract affected ones*)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
   758
      fun subLit (lit, (changed, nlits)) =
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   759
	    let val nlit = subst lit
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
   760
	    in  if nlit aconv lit then (changed, nlit::nlits)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
   761
		                  else ((nlit,true)::changed, nlits)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   762
            end
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   763
      val (changed, lits') = foldr subLit ([], []) lits
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   764
      val (changed', pairs') = foldr subFrame (changed, []) pairs
3092
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   765
  in  if !trace then writeln ("Substituting " ^ traceTerm sign u ^
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   766
			      " for " ^ traceTerm sign t ^ " in branch" )
b92a1b50b16b More tracing. hyp_subst_tac allowed to fail
paulson
parents: 3083
diff changeset
   767
      else ();
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   768
      {pairs = (changed',[])::pairs',	(*affected formulas, and others*)
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   769
       lits  = lits',			(*unaffected literals*)
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   770
       vars  = vars, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   771
       lim   = lim}
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   772
  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   773
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   774
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   775
exception NEWBRANCHES and CLOSEF;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   776
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   777
exception PROVE;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   778
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   779
(*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   780
val contr_tac = ematch_tac [Data.notE] THEN' 
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   781
                (eq_assume_tac ORELSE' assume_tac);
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   782
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   783
val eContr_tac  = TRACE Data.notE contr_tac;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   784
val eAssume_tac = TRACE asm_rl   (eq_assume_tac ORELSE' assume_tac);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   785
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   786
(*Try to unify complementary literals and return the corresponding tactic. *) 
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   787
fun tryClose (Const"*Goal*" $ G,  L) = 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   788
	if unify([],G,L) then SOME eAssume_tac else NONE
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   789
  | tryClose (G,  Const"*Goal*" $ L) = 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   790
	if unify([],G,L) then SOME eAssume_tac else NONE
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   791
  | tryClose (Const"Not" $ G,  L)    = 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   792
	if unify([],G,L) then SOME eContr_tac else NONE
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   793
  | tryClose (G,  Const"Not" $ L)    = 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   794
	if unify([],G,L) then SOME eContr_tac else NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
   795
  | tryClose _                       = NONE;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   796
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   797
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   798
(*Were there Skolem terms in the premise?  Must NOT chase Vars*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   799
fun hasSkolem (Skolem _)     = true
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   800
  | hasSkolem (Abs (_,body)) = hasSkolem body 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   801
  | hasSkolem (f$t)          =  hasSkolem f orelse hasSkolem t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   802
  | hasSkolem _              = false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   803
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   804
(*Attach the right "may duplicate" flag to new formulae: if they contain
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   805
  Skolem terms then allow duplication.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   806
fun joinMd md [] = []
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   807
  | joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   808
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   809
(*Convert a Goal to an ordinary Not.  Used also in dup_intr, where a goal like
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   810
  Ex(P) is duplicated as the assumption ~Ex(P). *)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   811
fun negOfGoal (Const"*Goal*" $ G) = negate G
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   812
  | negOfGoal G                   = G;
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   813
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   814
fun negOfGoal2 (G,md) = (negOfGoal G, md);
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   815
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   816
(*Converts all Goals to Nots in the safe parts of a branch.  They could
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   817
  have been moved there from the literals list after substitution (equalSubst).
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   818
  There can be at most one--this function could be made more efficient.*)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   819
fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   820
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   821
(*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   822
fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   823
                      rotate_tac ~1 i;
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   824
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   825
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   826
(** Backtracking and Pruning **)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   827
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   828
(*clashVar vars (n,trail) determines whether any of the last n elements
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   829
  of "trail" occur in "vars" OR in their instantiations*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   830
fun clashVar [] = (fn _ => false)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   831
  | clashVar vars =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   832
      let fun clash (0, _)     = false
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   833
	    | clash (_, [])    = false
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   834
	    | clash (n, v::vs) = exists (varOccur v) vars orelse clash(n-1,vs)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   835
      in  clash  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   836
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   837
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   838
(*nbrs = # of branches just prior to closing this one.  Delete choice points
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   839
  for goals proved by the latest inference, provided NO variables in the
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   840
  next branch have been updated.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   841
fun prune (1, nxtVars, choices) = choices  (*DON'T prune at very end: allow 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   842
					     backtracking over bad proofs*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   843
  | prune (nbrs, nxtVars, choices) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   844
      let fun traceIt last =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   845
		let val ll = length last
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   846
		    and lc = length choices
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   847
		in if !trace andalso ll<lc then
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   848
		    (writeln("Pruning " ^ Int.toString(lc-ll) ^ " levels"); 
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   849
		     last)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   850
		   else last
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   851
		end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   852
	  fun pruneAux (last, _, _, []) = last
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   853
	    | pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) =
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   854
		if nbrs' < nbrs 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   855
		then last  (*don't backtrack beyond first solution of goal*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   856
		else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   857
		else (* nbrs'=nbrs *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   858
		     if clashVar nxtVars (ntrl-ntrl', trl) then last
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   859
		     else (*no clashes: can go back at least this far!*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   860
			  pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'), 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   861
				   choices)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   862
  in  traceIt (pruneAux (choices, !ntrail, !trail, choices))  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   863
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   864
fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   865
  | nextVars []                              = [];
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   866
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   867
fun backtrack (choices as (ntrl, nbrs, exn)::_) = 
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   868
      (if !trace then (writeln ("Backtracking; now there are " ^ 
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   869
				Int.toString nbrs ^ " branches"))
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   870
                 else (); 
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   871
       raise exn)
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   872
  | backtrack _ = raise PROVE;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   873
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   874
(*Add the literal G, handling *Goal* and detecting duplicates.*)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   875
fun addLit (Const "*Goal*" $ G, lits) = 
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   876
      (*New literal is a *Goal*, so change all other Goals to Nots*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   877
      let fun bad (Const"*Goal*" $ _) = true
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   878
	    | bad (Const"Not" $ G')   = G aconv G'
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   879
	    | bad _                   = false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   880
	  fun change [] = []
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   881
	    | change (Const"*Goal*" $ G' :: lits) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   882
		  if G aconv G' then change lits
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   883
		  else Const"Not" $ G' :: change lits
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   884
	    | change (Const"Not" $ G' :: lits)    = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   885
		  if G aconv G' then change lits
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   886
		  else Const"Not" $ G' :: change lits
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   887
	    | change (lit::lits) = lit :: change lits
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   888
      in
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   889
	Const "*Goal*" $ G :: (if exists bad lits then change lits else lits)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   890
      end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   891
  | addLit (G,lits) = ins_term(G, lits)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   892
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   893
2952
ea834e8fac1b Changed penalty from log2 to log3
paulson
parents: 2924
diff changeset
   894
(*For calculating the "penalty" to assess on a branching factor of n
ea834e8fac1b Changed penalty from log2 to log3
paulson
parents: 2924
diff changeset
   895
  log2 seems a little too severe*)
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   896
fun log n = if n<4 then 0 else 1 + log(n div 4);
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   897
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   898
3021
39806db47be9 Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents: 2999
diff changeset
   899
(*match(t,u) says whether the term u might be an instance of the pattern t
39806db47be9 Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents: 2999
diff changeset
   900
  Used to detect "recursive" rules such as transitivity*)
39806db47be9 Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents: 2999
diff changeset
   901
fun match (Var _) u   = true
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   902
  | match (Const"*Goal*") (Const"Not")    = true
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   903
  | match (Const"Not")    (Const"*Goal*") = true
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   904
  | match (Const a)       (Const b)       = (a=b)
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   905
  | match (TConst (a,ta)) (TConst (b,tb)) = a=b andalso match ta tb
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   906
  | match (Free a)        (Free b)        = (a=b)
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   907
  | match (Bound i)       (Bound j)       = (i=j)
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   908
  | match (Abs(_,t))      (Abs(_,u))      = match t u
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   909
  | match (f$t)           (g$u)           = match f g andalso match t u
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   910
  | match t               u   = false;
3021
39806db47be9 Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents: 2999
diff changeset
   911
39806db47be9 Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents: 2999
diff changeset
   912
4300
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   913
(*Branches closed: number of branches closed during the search
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   914
  Branches tried:  number of branches created by splitting (counting from 1)*)
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   915
val nclosed = ref 0
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   916
and ntried  = ref 1;
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   917
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   918
fun printStats (b, start, tacs) =
4323
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
   919
  if b then
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
   920
    writeln (endTiming start ^ " for search.  Closed: " 
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
   921
	     ^ Int.toString (!nclosed) ^
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   922
             " tried: " ^ Int.toString (!ntried) ^
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   923
             " tactics: " ^ Int.toString (length tacs))
4323
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
   924
  else ();
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
   925
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
   926
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   927
(*Tableau prover based on leanTaP.  Argument is a list of branches.  Each 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   928
  branch contains a list of unexpanded formulae, a list of literals, and a 
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   929
  bound on unsafe expansions.
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   930
 "start" is CPU time at start, for printing search time
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   931
*)
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   932
fun prove (sign, start, cs, brs, cont) =
4653
d60f76680bf4 renamed rep_claset to rep_cs
oheimb
parents: 4651
diff changeset
   933
 let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   934
     val safeList = [safe0_netpair, safep_netpair]
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   935
     and hazList  = [haz_netpair]
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   936
     fun prv (tacs, trs, choices, []) = 
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
   937
	        (printStats (!trace orelse !stats, start, tacs); 
4323
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
   938
		 cont (tacs, trs, choices))   (*all branches closed!*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   939
       | prv (tacs, trs, choices, 
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   940
	      brs0 as {pairs = ((G,md)::br, haz)::pairs, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   941
		       lits, vars, lim} :: brs) =
3917
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
   942
   	     (*apply a safe rule only (possibly allowing instantiation);
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
   943
               defer any haz formulae*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   944
	  let exception PRV (*backtrack to precisely this recursion!*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   945
	      val ntrl = !ntrail 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   946
	      val nbrs = length brs0
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   947
              val nxtVars = nextVars brs
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   948
	      val G = norm G
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   949
	      val rules = netMkRules G vars safeList
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   950
	      (*Make a new branch, decrementing "lim" if instantiations occur*)
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   951
	      fun newBr (vars',lim') prems =
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   952
		  map (fn prem => 
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   953
		       if (exists isGoal prem) 
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   954
		       then {pairs = ((joinMd md prem, []) :: 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   955
				      negOfGoals ((br, haz)::pairs)),
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   956
			     lits  = map negOfGoal lits, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   957
			     vars  = vars', 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   958
			     lim   = lim'}
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   959
		       else {pairs = ((joinMd md prem, []) :: 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   960
				      (br, haz) :: pairs),
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   961
			     lits = lits, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   962
			     vars = vars', 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   963
			     lim  = lim'})
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   964
		  prems @
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   965
		  brs		  
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   966
	      (*Seek a matching rule.  If unifiable then add new premises
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   967
                to branch.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   968
	      fun deeper [] = raise NEWBRANCHES
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   969
		| deeper (((P,prems),tac)::grls) =
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   970
		    if unify(add_term_vars(P,[]), P, G) 
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   971
		    then  (*P comes from the rule; G comes from the branch.*)
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   972
		     let val updated = ntrl < !ntrail (*branch updated*)
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   973
			 val lim' = if updated
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   974
				    then lim - (1+log(length rules))
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   975
				    else lim   (*discourage branching updates*)
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   976
			 val vars  = vars_in_vars vars
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   977
			 val vars' = foldr add_terms_vars vars prems
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   978
			 val choices' = (ntrl, nbrs, PRV) :: choices
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
   979
			 val tacs' = (tac(updated,false,true)) 
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   980
                                     :: tacs  (*no duplication; rotate*)
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   981
		     in
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   982
			 traceNew prems;  traceVars sign ntrl;
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   983
			 (if null prems then (*closed the branch: prune!*)
4300
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   984
			    (nclosed := !nclosed + 1;
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   985
			     prv(tacs',  brs0::trs, 
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   986
				 prune (nbrs, nxtVars, choices'),
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   987
				 brs))
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   988
			  else (*prems non-null*)
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   989
			  if lim'<0 (*faster to kill ALL the alternatives*)
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   990
			  then (traceMsg"Excessive branching: KILLED";
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
   991
			        clearTo ntrl;  raise NEWBRANCHES)
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   992
			  else
4300
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   993
			    (ntried := !ntried + length prems - 1;
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   994
			     prv(tacs',  brs0::trs, choices',
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
   995
				 newBr (vars',lim') prems)))
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   996
                         handle PRV => 
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
   997
			   if updated then
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   998
				(*Backtrack at this level.
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
   999
				  Reset Vars and try another rule*)
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1000
				(clearTo ntrl;  deeper grls)
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1001
			   else (*backtrack to previous level*)
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1002
				backtrack choices
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1003
		     end
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1004
		    else deeper grls
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1005
	      (*Try to close branch by unifying with head goal*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1006
	      fun closeF [] = raise CLOSEF
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1007
		| closeF (L::Ls) = 
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1008
		    case tryClose(G,L) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
  1009
			NONE     => closeF Ls
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
  1010
		      | SOME tac => 
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1011
			    let val choices' = 
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14913
diff changeset
  1012
				    (if !trace then (immediate_output"branch closed";
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1013
						     traceVars sign ntrl)
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1014
				               else ();
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1015
				     prune (nbrs, nxtVars, 
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1016
					    (ntrl, nbrs, PRV) :: choices))
4300
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
  1017
			    in  nclosed := !nclosed + 1;
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
  1018
				prv (tac::tacs, brs0::trs, choices', brs)  
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1019
				handle PRV => 
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1020
				    (*reset Vars and try another literal
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1021
				      [this handler is pruned if possible!]*)
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1022
				 (clearTo ntrl;  closeF Ls)
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1023
			    end
11152
32d002362005 Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents: 11119
diff changeset
  1024
	      (*Try to unify a queued formula (safe or haz) with head goal*)
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
  1025
	      fun closeFl [] = raise CLOSEF
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
  1026
		| closeFl ((br, haz)::pairs) =
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
  1027
		    closeF (map fst br)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
  1028
		      handle CLOSEF => closeF (map fst haz)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
  1029
			handle CLOSEF => closeFl pairs
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1030
	  in tracing sign brs0; 
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1031
	     if lim<0 then (traceMsg "Limit reached.  "; backtrack choices)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1032
	     else
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
  1033
	     prv (Data.hyp_subst_tac trace :: tacs, 
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1034
		  brs0::trs,  choices,
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1035
		  equalSubst sign
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1036
		    (G, {pairs = (br,haz)::pairs, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1037
			 lits  = lits, vars  = vars, lim   = lim}) 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1038
		    :: brs)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1039
	     handle DEST_EQ =>   closeF lits
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1040
	      handle CLOSEF =>   closeFl ((br,haz)::pairs)
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1041
	        handle CLOSEF => deeper rules
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
  1042
		  handle NEWBRANCHES => 
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
  1043
		   (case netMkRules G vars hazList of
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
  1044
		       [] => (*there are no plausible haz rules*)
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1045
			     (traceMsg "moving formula to literals";
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1046
			      prv (tacs, brs0::trs, choices,
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1047
				   {pairs = (br,haz)::pairs, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1048
				    lits  = addLit(G,lits), 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1049
				    vars  = vars, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1050
				    lim   = lim}  :: brs))
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
  1051
		    | _ => (*G admits some haz rules: try later*)
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1052
			   (traceMsg "moving formula to haz list";
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4391
diff changeset
  1053
			    prv (if isGoal G then negOfGoal_tac :: tacs
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1054
				             else tacs, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1055
				 brs0::trs,  
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1056
				 choices,
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1057
				 {pairs = (br, haz@[(negOfGoal G, md)])::pairs,
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1058
				  lits  = lits,
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1059
				  vars  = vars, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1060
				  lim   = lim}  :: brs)))
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1061
	  end
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1062
       | prv (tacs, trs, choices, 
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1063
	      {pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) =
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
  1064
	     (*no more "safe" formulae: transfer haz down a level*)
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1065
	   prv (tacs, trs, choices, 
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1066
		{pairs = (Gs,haz@haz')::pairs, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1067
		 lits  = lits, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1068
		 vars  = vars, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1069
		 lim    = lim} :: brs)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1070
       | prv (tacs, trs, choices, 
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1071
	      brs0 as {pairs = [([], (H,md)::Hs)],
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1072
		       lits, vars, lim} :: brs) =
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
  1073
   	     (*no safe steps possible at any level: apply a haz rule*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1074
	  let exception PRV (*backtrack to precisely this recursion!*)
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
  1075
	      val H = norm H
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1076
	      val ntrl = !ntrail
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1077
	      val rules = netMkRules H vars hazList
3021
39806db47be9 Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents: 2999
diff changeset
  1078
	      (*new premises of haz rules may NOT be duplicated*)
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1079
	      fun newPrem (vars,P,dup,lim') prem = 
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1080
		  let val Gs' = map (fn Q => (Q,false)) prem
3021
39806db47be9 Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents: 2999
diff changeset
  1081
		      and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs
4196
9953c0995b79 Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents: 4149
diff changeset
  1082
		      and lits' = if (exists isGoal prem) 
9953c0995b79 Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents: 4149
diff changeset
  1083
			          then map negOfGoal lits
9953c0995b79 Now applies "map negOfGoal" to lits when expanding haz rules.
paulson
parents: 4149
diff changeset
  1084
				  else lits
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1085
                  in  {pairs = if exists (match P) prem then [(Gs',Hs')] 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1086
			       (*Recursive in this premise.  Don't make new
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1087
				 "stack frame".  New haz premises will end up
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1088
				 at the BACK of the queue, preventing
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1089
				 exclusion of others*)
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1090
			    else [(Gs',[]), ([],Hs')], 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1091
		       lits = lits', 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1092
		       vars = vars, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1093
		       lim  = lim'}
3021
39806db47be9 Loop detection: before expanding a haz formula, see whether it is a duplicate
paulson
parents: 2999
diff changeset
  1094
		  end
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1095
	      fun newBr x prems = map (newPrem x) prems  @  brs
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1096
	      (*Seek a matching rule.  If unifiable then add new premises
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1097
                to branch.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1098
	      fun deeper [] = raise NEWBRANCHES
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1099
		| deeper (((P,prems),tac)::grls) =
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1100
		    if unify(add_term_vars(P,[]), P, H)
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1101
		    then
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
  1102
		     let val updated = ntrl < !ntrail (*branch updated*)
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1103
			 val vars  = vars_in_vars vars
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
  1104
			 val vars' = foldr add_terms_vars vars prems
11152
32d002362005 Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents: 11119
diff changeset
  1105
			    (*duplicate H if md permits*)
32d002362005 Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents: 11119
diff changeset
  1106
			 val dup = md (*earlier had "andalso vars' <> vars":
32d002362005 Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents: 11119
diff changeset
  1107
                                  duplicate only if the subgoal has new vars*)
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1108
			     (*any instances of P in the subgoals?
11152
32d002362005 Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents: 11119
diff changeset
  1109
			       NB: boolean "recur" affects tracing only!*)
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1110
			 and recur = exists (exists (match P)) prems
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1111
			 val lim' = (*Decrement "lim" extra if updates occur*)
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
  1112
			     if updated then lim - (1+log(length rules))
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1113
			     else lim-1 
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1114
				 (*It is tempting to leave "lim" UNCHANGED if
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1115
				   both dup and recur are false.  Proofs are
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1116
				   found at shallower depths, but looping
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1117
				   occurs too often...*)
3917
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
  1118
			 val mayUndo = 
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
  1119
			     (*Allowing backtracking from a rule application
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
  1120
			       if other matching rules exist, if the rule
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
  1121
			       updated variables, or if the rule did not
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
  1122
			       introduce new variables.  This latter condition
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
  1123
			       means it is not a standard "gamma-rule" but
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
  1124
			       some other form of unsafe rule.  Aim is to
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
  1125
			       emulate Fast_tac, which allows all unsafe steps
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
  1126
			       to be undone.*)
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
  1127
			     not(null grls)   (*other rules to try?*)
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
  1128
			     orelse updated
3917
6ea5f9101c3e A lot of new comments
paulson
parents: 3533
diff changeset
  1129
			     orelse vars=vars'   (*no new Vars?*)
5481
c41956742c2e Less deterministic reconstruction: now more robust but perhaps slower
paulson
parents: 5463
diff changeset
  1130
			 val tac' = tac(updated, dup, true)
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1131
		       (*if recur then perhaps shouldn't call rotate_tac: new
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1132
                         formulae should be last, but that's WRONG if the new
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1133
                         formulae are Goals, since they remain in the first
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1134
                         position*)
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1135
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1136
		     in
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1137
		       if lim'<0 andalso not (null prems)
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1138
		       then (*it's faster to kill ALL the alternatives*)
5343
871b77df79a0 new version, more resistant to PROOF FAILED. Now it distinguishes between
paulson
parents: 4653
diff changeset
  1139
			   (traceMsg"Excessive branching: KILLED";
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1140
			    clearTo ntrl;  raise NEWBRANCHES)
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1141
		       else 
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1142
			 traceNew prems;  
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14913
diff changeset
  1143
			 if !trace andalso dup then immediate_output" (duplicating)"
11152
32d002362005 Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents: 11119
diff changeset
  1144
					         else ();
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14913
diff changeset
  1145
			 if !trace andalso recur then immediate_output" (recursive)"
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1146
					         else ();
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1147
			 traceVars sign ntrl;
4300
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
  1148
			 if null prems then nclosed := !nclosed + 1
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
  1149
			 else ntried := !ntried + length prems - 1;
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1150
			 prv(tac' :: tacs, 
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1151
			     brs0::trs, 
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1152
			     (ntrl, length brs0, PRV) :: choices, 
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1153
			     newBr (vars', P, dup, lim') prems)
3083
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1154
			  handle PRV => 
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1155
			      if mayUndo
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1156
			      then (*reset Vars and try another rule*)
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1157
				   (clearTo ntrl;  deeper grls)
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1158
			      else (*backtrack to previous level*)
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1159
				   backtrack choices
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1160
		     end
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1161
		    else deeper grls
1a7edbd7f55a More tracing; less exception handling
paulson
parents: 3049
diff changeset
  1162
	  in tracing sign brs0; 
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1163
	     if lim<1 then (traceMsg "Limit reached.  "; backtrack choices)
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1164
	     else deeper rules
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1165
	     handle NEWBRANCHES => 
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
  1166
		 (*cannot close branch: move H to literals*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1167
		 prv (tacs,  brs0::trs,  choices,
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1168
		      {pairs = [([], Hs)], 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1169
		       lits  = H::lits, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1170
		       vars  = vars, 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1171
		       lim   = lim}  :: brs)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1172
	  end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1173
       | prv (tacs, trs, choices, _ :: brs) = backtrack choices
12346
e7b1956f4eae removed questionable init_gensym;
wenzelm
parents: 11783
diff changeset
  1174
 in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1175
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1176
2883
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
  1177
(*Construct an initial branch.*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1178
fun initBranch (ts,lim) = 
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1179
    {pairs = [(map (fn t => (t,true)) ts, [])],
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1180
     lits  = [], 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1181
     vars  = add_terms_vars (ts,[]), 
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1182
     lim   = lim};
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1183
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1184
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1185
(*** Conversion & Skolemization of the Isabelle proof state ***)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1186
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1187
(*Make a list of all the parameters in a subgoal, even if nested*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1188
local open Term 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1189
in
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1190
fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1191
  | discard_foralls t = t;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1192
end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1193
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1194
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1195
(*List of variables not appearing as arguments to the given parameter*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1196
fun getVars []                  i = []
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1197
  | getVars ((_,(v,is))::alist) i =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1198
	if i mem is then getVars alist i
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1199
	else v :: getVars alist i;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1200
4233
85d004a96b98 Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
paulson
parents: 4196
diff changeset
  1201
exception TRANS of string;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1202
4233
85d004a96b98 Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
paulson
parents: 4196
diff changeset
  1203
(*Translation of a subgoal: Skolemize all parameters*)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1204
fun fromSubgoal t =
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1205
  let val alistVar = ref []
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1206
      and alistTVar = ref []
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1207
      fun hdvar ((ix,(v,is))::_) = v
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1208
      fun from lev t =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1209
	let val (ht,ts) = Term.strip_comb t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1210
	    fun apply u = list_comb (u, map (from lev) ts)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1211
	    fun bounds [] = []
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1212
	      | bounds (Term.Bound i::ts) = 
4233
85d004a96b98 Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
paulson
parents: 4196
diff changeset
  1213
		  if i<lev then raise TRANS
85d004a96b98 Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
paulson
parents: 4196
diff changeset
  1214
		      "Function unknown's argument not a parameter"
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1215
		  else i-lev :: bounds ts
4233
85d004a96b98 Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
paulson
parents: 4196
diff changeset
  1216
	      | bounds ts = raise TRANS
85d004a96b98 Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
paulson
parents: 4196
diff changeset
  1217
		      "Function unknown's argument not a bound variable"
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1218
        in
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1219
	  case ht of 
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1220
	      Term.Const aT    => apply (fromConst alistTVar aT)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1221
	    | Term.Free  (a,_) => apply (Free a)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1222
	    | Term.Bound i     => apply (Bound i)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1223
	    | Term.Var (ix,_) => 
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1224
		  (case (assoc_string_int(!alistVar,ix)) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
  1225
		       NONE => (alistVar := (ix, (ref NONE, bounds ts))
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1226
					  :: !alistVar;
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1227
				Var (hdvar(!alistVar)))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
  1228
		     | SOME(v,is) => if is=bounds ts then Var v
4233
85d004a96b98 Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
paulson
parents: 4196
diff changeset
  1229
			    else raise TRANS
5411
7a43b484f6d2 fixed error msg
paulson
parents: 5343
diff changeset
  1230
				("Discrepancy among occurrences of "
4233
85d004a96b98 Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
paulson
parents: 4196
diff changeset
  1231
				 ^ Syntax.string_of_vname ix))
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1232
	    | Term.Abs (a,_,body) => 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1233
		  if null ts then Abs(a, from (lev+1) body)
4233
85d004a96b98 Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
paulson
parents: 4196
diff changeset
  1234
		  else raise TRANS "argument not in normal form"
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1235
        end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1236
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1237
      val npars = length (Logic.strip_params t)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1238
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1239
      (*Skolemize a subgoal from a proof state*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1240
      fun skoSubgoal i t =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1241
	  if i<npars then 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1242
	      skoSubgoal (i+1)
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1243
		(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1244
			      t))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1245
	  else t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1246
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1247
  in  skoSubgoal 0 (from 0 (discard_foralls t))  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1248
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1249
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1250
fun initialize thy = 
4300
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
  1251
    (fullTrace:=[];  trail := [];  ntrail := 0;
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1252
     nclosed := 0;  ntried := 1;  curr_defs := Theory.defs_of thy);
4300
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
  1253
451ae21dca28 Statistics
paulson
parents: 4271
diff changeset
  1254
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1255
(*Tactic using tableau engine and proof reconstruction.  
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1256
 "start" is CPU time at start, for printing SEARCH time
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1257
	(also prints reconstruction time)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1258
 "lim" is depth limit.*)
9486
2df511ebb956 handle actual object-logic rules by atomizing the goal;
wenzelm
parents: 9170
diff changeset
  1259
fun timing_depth_tac start cs lim i st0 = 
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1260
  let val st = (initialize (theory_of_thm st0); ObjectLogic.atomize_goal i st0);
9486
2df511ebb956 handle actual object-logic rules by atomizing the goal;
wenzelm
parents: 9170
diff changeset
  1261
      val {sign,...} = rep_thm st
4323
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1262
      val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1263
      val hyps  = strip_imp_prems skoprem
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1264
      and concl = strip_imp_concl skoprem
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1265
      fun cont (tacs,_,choices) = 
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1266
	  let val start = startTiming()
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1267
	  in
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1268
	  case Seq.pull(EVERY' (rev tacs) i st) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
  1269
	      NONE => (writeln ("PROOF FAILED for depth " ^
4323
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1270
				Int.toString lim);
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1271
		       if !trace then error "************************\n"
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1272
		       else ();
4323
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1273
		       backtrack choices)
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1274
	    | cell => (if (!trace orelse !stats)
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1275
		       then writeln (endTiming start ^ " for reconstruction")
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1276
		       else ();
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1277
		       Seq.make(fn()=> cell))
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1278
          end
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1279
  in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) 
4323
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1280
  end
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1281
  handle PROVE     => Seq.empty;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1282
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1283
(*Public version with fixed depth*)
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1284
fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st;
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1285
15162
670ab8497818 depth limit (previously hard-coded with a value of 20) made a reference
webertj
parents: 14984
diff changeset
  1286
val depth_limit = ref 20;
670ab8497818 depth limit (previously hard-coded with a value of 20) made a reference
webertj
parents: 14984
diff changeset
  1287
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1288
fun blast_tac cs i st = 
15162
670ab8497818 depth limit (previously hard-coded with a value of 20) made a reference
webertj
parents: 14984
diff changeset
  1289
    ((DEEPEN (1, !depth_limit) (timing_depth_tac (startTiming()) cs) 0) i 
5463
a5479f5cd482 Allows more backtracking in proof reconstruction, making it slower but more
paulson
parents: 5411
diff changeset
  1290
     THEN flexflex_tac) st
14466
b737e523fc6c more up-to-date error msg
paulson
parents: 13550
diff changeset
  1291
    handle TRANS s =>
b737e523fc6c more up-to-date error msg
paulson
parents: 13550
diff changeset
  1292
      ((if !trace then warning ("blast: " ^ s) else ()); 
b737e523fc6c more up-to-date error msg
paulson
parents: 13550
diff changeset
  1293
       Seq.empty);
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1294
4078
c107ab1c7626 adapted to new implicit claset mechanism;
wenzelm
parents: 4065
diff changeset
  1295
fun Blast_tac i = blast_tac (Data.claset()) i;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1296
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1297
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1298
(*** For debugging: these apply the prover to a subgoal and return 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1299
     the resulting tactics, trace, etc.                            ***)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1300
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1301
(*Translate subgoal i from a proof state*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1302
fun trygl cs lim i = 
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1303
	let val st = topthm()
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1304
		val {sign,...} = rep_thm st
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1305
		val skoprem = (initialize (theory_of_thm st); 
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1306
		               fromSubgoal (List.nth(prems_of st, i-1)))
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1307
		val hyps  = strip_imp_prems skoprem
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1308
		and concl = strip_imp_concl skoprem
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1309
	in timeap prove (sign, startTiming(), cs, 
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1310
			 [initBranch (mkGoal concl :: hyps, lim)], I)
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1311
	end
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1312
	handle Subscript => error("There is no subgoal " ^ Int.toString i);
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1313
4078
c107ab1c7626 adapted to new implicit claset mechanism;
wenzelm
parents: 4065
diff changeset
  1314
fun Trygl lim i = trygl (Data.claset()) lim i;
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1315
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1316
(*Read a string to make an initial, singleton branch*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1317
fun readGoal sign s = read_cterm sign (s,propT) |>
4065
8862fcb5d44a New treatment of overloading\!
paulson
parents: 3917
diff changeset
  1318
                      term_of |> fromTerm |> rand |> mkGoal;
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1319
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1320
fun tryInThy thy lim s = 
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 15786
diff changeset
  1321
    (initialize thy;
6391
0da748358eff Theory.sign_of;
wenzelm
parents: 5961
diff changeset
  1322
     timeap prove (Theory.sign_of thy, 
4391
cc3e8453d7f0 More deterministic and therefore faster (sometimes) proof reconstruction
paulson
parents: 4354
diff changeset
  1323
		   startTiming(), 
4323
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1324
		   Data.claset(), 
6391
0da748358eff Theory.sign_of;
wenzelm
parents: 5961
diff changeset
  1325
		   [initBranch ([readGoal (Theory.sign_of thy) s], lim)], 
4323
561242f8606b Printing of statistics including time for search & reconstruction
paulson
parents: 4300
diff changeset
  1326
		   I));
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1327
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1328
5926
58f9ca06b76b method setup;
wenzelm
parents: 5734
diff changeset
  1329
(** method setup **)
58f9ca06b76b method setup;
wenzelm
parents: 5734
diff changeset
  1330
7559
1d2c099e98f7 setup for refined facts handling;
wenzelm
parents: 7272
diff changeset
  1331
fun blast_args m =
11152
32d002362005 Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents: 11119
diff changeset
  1332
  Method.bang_sectioned_args' 
32d002362005 Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents: 11119
diff changeset
  1333
      Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m;
7155
70ba7d640bfe blast method: optional depth argument;
wenzelm
parents: 7003
diff changeset
  1334
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
  1335
fun blast_meth NONE = Data.cla_meth' blast_tac
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15162
diff changeset
  1336
  | blast_meth (SOME lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
7155
70ba7d640bfe blast method: optional depth argument;
wenzelm
parents: 7003
diff changeset
  1337
11152
32d002362005 Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents: 11119
diff changeset
  1338
val setup = [Method.add_methods [("blast", blast_args blast_meth, 
32d002362005 Blast bug fix: now always duplicates when applying a haz rule,
paulson
parents: 11119
diff changeset
  1339
				  "tableau prover")]];
5926
58f9ca06b76b method setup;
wenzelm
parents: 5734
diff changeset
  1340
58f9ca06b76b method setup;
wenzelm
parents: 5734
diff changeset
  1341
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1342
end;