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