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