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