src/Provers/blast.ML
author paulson
Wed, 09 Apr 1997 12:36:52 +0200
changeset 2924 af506c35b4ed
parent 2894 d2ffee4f811b
child 2952 ea834e8fac1b
permissions -rw-r--r--
Control over excessive branching by applying a log2 penalty Incorporation of debugging features Allows backtracking over haz rules if alternatives exist Subsitution for equality may more a rule from the haz to the safe part
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     1
(*  Title: 	Provers/blast
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     2
    ID:         $Id$
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     4
    Copyright   1992  University of Cambridge
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     5
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     6
Generic tableau prover with proof reconstruction
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     7
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
     8
  SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules??
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
     9
  Needs explicit instantiation of assumptions?
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    10
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    11
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    12
Blast_tac is often more powerful than fast_tac, but has some limitations.
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    13
Blast_tac...
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    14
  * ignores addss, addbefore, addafter; this restriction is intrinsic
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    15
  * ignores elimination rules that don't have the correct format
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    16
	(conclusion must be a formula variable)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    17
  * ignores types, which can make HOL proofs fail
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    18
  * 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
    19
    + 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
    20
  * 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
    21
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    22
Known problems:
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    23
  With substition for equalities (hyp_subst_tac):
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    24
    1.  Sometimes hyp_subst_tac will fail due to occurrence of the parameter
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
    25
        as the argument of a function variable
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    26
    2.  When substitution affects a haz formula or literal, it is moved
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    27
        back to the list of safe formulae.
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    28
        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
    29
        "no DETERM" flag would prevent proofs failing here.
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    30
*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    31
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    32
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    33
(*Should be a type abbreviation?*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    34
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    35
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    36
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    37
(*Assumptions about constants:
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    38
  --The negation symbol is "Not"
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    39
  --The equality symbol is "op ="
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    40
  --The is-true judgement symbol is "Trueprop"
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    41
  --There are no constants named "*Goal* or "*False*"
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    42
*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    43
signature BLAST_DATA =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    44
  sig
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    45
  type claset
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    46
  val notE		: thm		(* [| ~P;  P |] ==> R *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    47
  val ccontr		: thm		
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    48
  val contr_tac 	: int -> tactic
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    49
  val dup_intr		: thm -> thm
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    50
  val vars_gen_hyp_subst_tac : bool -> int -> tactic
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    51
  val claset		: claset ref
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    52
  val rep_claset	: 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    53
      claset -> {safeIs: thm list, safeEs: thm list, 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    54
		 hazIs: thm list, hazEs: thm list,
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    55
		 uwrapper: (int -> tactic) -> (int -> tactic),
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    56
		 swrapper: (int -> tactic) -> (int -> tactic),
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    57
		 safe0_netpair: netpair, safep_netpair: netpair,
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    58
		 haz_netpair: netpair, dup_netpair: netpair}
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    59
  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    60
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    61
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    62
signature BLAST =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    63
  sig
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    64
  type claset 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    65
  datatype term = 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    66
      Const of string
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    67
    | OConst of string * int
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    68
    | Skolem of string * term option ref list
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    69
    | Free  of string
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    70
    | Var   of term option ref
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    71
    | Bound of int
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    72
    | Abs   of string*term
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    73
    | op $  of term*term;
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    74
  type branch
2883
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
    75
  val depth_tac 	: claset -> int -> int -> tactic
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
    76
  val blast_tac 	: claset -> int -> tactic
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
    77
  val Blast_tac 	: int -> tactic
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
    78
  val declConsts 	: string list * thm list -> unit
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    79
  (*debugging tools*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    80
  val trace	        : bool ref
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    81
  val fullTrace	        : branch list list ref
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    82
  val fromTerm	        : Type.type_sig -> Term.term -> term
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    83
  val fromSubgoal       : Type.type_sig -> Term.term -> term
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    84
  val toTerm	        : int -> term -> Term.term
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    85
  val readGoal          : Sign.sg -> string -> term
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    86
  val tryInThy		: theory -> int -> string ->
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    87
		branch list list * (int*int*exn) list * (int -> tactic) list
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    88
  val trygl		: claset -> int -> int ->
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    89
		branch list list * (int*int*exn) list * (int -> tactic) list
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    90
  val Trygl		: int -> int ->
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    91
		branch list list * (int*int*exn) list * (int -> tactic) list
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    92
  val normBr		: branch -> branch
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    93
  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    94
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    95
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
    96
functor BlastFun(Data: BLAST_DATA): BLAST = 
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    97
struct
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    98
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
    99
type claset = Data.claset;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   100
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   101
val trace = ref false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   102
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   103
datatype term = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   104
    Const of string
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   105
  | OConst of string * int
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   106
  | Skolem of string * term option ref list
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   107
  | Free  of string
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   108
  | Var   of term option ref
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   109
  | Bound of int
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   110
  | Abs   of string*term
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   111
  | op $  of term*term;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   112
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   113
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   114
exception DEST_EQ;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   115
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   116
  (*Take apart an equality (plain or overloaded).  NO constant Trueprop*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   117
  fun dest_eq (Const  "op ="     $ t $ u) = (t,u)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   118
    | dest_eq (OConst("op =",_)  $ t $ u) = (t,u)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   119
    | dest_eq _                      = raise DEST_EQ;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   120
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   121
(** Basic syntactic operations **)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   122
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   123
fun is_Var (Var _) = true
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   124
  | is_Var _ = false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   125
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   126
fun dest_Var (Var x) =  x;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   127
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   128
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   129
fun rand (f$x) = x;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   130
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   131
(* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   132
val list_comb : term * term list -> term = foldl (op $);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   133
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   134
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   135
(* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   136
fun strip_comb u : term * term list = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   137
    let fun stripc (f$t, ts) = stripc (f, t::ts)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   138
        |   stripc  x =  x 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   139
    in  stripc(u,[])  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   140
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   141
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   142
(* maps   f(t1,...,tn)  to  f , which is never a combination *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   143
fun head_of (f$t) = head_of f
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   144
  | head_of u = u;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   145
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
(** Particular constants **)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   148
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   149
fun negate P = Const"Not" $ P;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   150
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   151
fun mkGoal P = Const"*Goal*" $ P;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   152
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   153
fun isGoal (Const"*Goal*" $ _) = true
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   154
  | isGoal _                   = false;
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
val Trueprop = Term.Const("Trueprop", Type("o",[])-->propT);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   157
fun mk_tprop P = Term.$ (Trueprop, P);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   158
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   159
fun isTrueprop (Term.Const("Trueprop",_)) = true
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   160
  | isTrueprop _                          = false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   161
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   162
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   163
(** Dealing with overloaded constants **)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   164
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   165
(*Result is a symbol table, indexed by names of overloaded constants.
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   166
  Each constant maps to a list of (pattern,Blast.Const) pairs.
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   167
  Any Term.Const that matches a pattern gets replaced by the Blast.Const.
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   168
*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   169
fun addConsts (t as Term.Const(a,_), tab) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   170
     (case Symtab.lookup (tab,a) of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   171
	  None    => tab  (*ignore: not a constant that we are looking for*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   172
	| Some patList => 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   173
	      (case gen_assoc (op aconv) (patList, t) of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   174
		  None => Symtab.update
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   175
		           ((a, (t, OConst (a, length patList)) :: patList), 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   176
			    tab)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   177
		 | _    => tab))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   178
  | addConsts (Term.Abs(_,_,body), tab) = addConsts (body, tab)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   179
  | addConsts (Term.$ (t,u), tab) = addConsts (t, addConsts (u, tab))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   180
  | addConsts (_,            tab) = tab (*ignore others*);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   181
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   182
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   183
fun addRules (rls,tab) = foldr addConsts (map (#prop o rep_thm) rls, tab);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   184
2883
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
   185
fun declConst (a,tab) = 
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
   186
    case Symtab.lookup (tab,a) of
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
   187
	None   => Symtab.update((a,[]), tab)	(*create a brand new entry*)
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
   188
      | Some _ => tab				(*preserve old entry*);
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   189
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   190
(*maps the name of each overloaded constant to a list of archetypal constants,
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   191
  which may be polymorphic.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   192
local
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   193
val overLoadTab = ref (Symtab.null : (Term.term * term) list Symtab.table)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   194
    (*The alists in this table should only be increased*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   195
in
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   196
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   197
fun declConsts (names, rls) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   198
    overLoadTab := addRules (rls, foldr declConst (names, !overLoadTab));
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   199
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   200
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   201
(*Convert a possibly overloaded Term.Const to a Blast.Const*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   202
fun fromConst tsig (t as Term.Const (a,_)) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   203
  let fun find []                  = Const a
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   204
	| find ((pat,t')::patList) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   205
		if Pattern.matches tsig (pat,t) then t' 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   206
		else find patList
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   207
  in  case Symtab.lookup(!overLoadTab, a) of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   208
	   None         => Const a
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   209
	 | Some patList => find patList
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   210
  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   211
end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   212
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
(*Tests whether 2 terms are alpha-convertible; chases instantiations*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   215
fun (Const a)      aconv (Const b)      = a=b
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   216
  | (OConst ai)    aconv (OConst bj)    = ai=bj
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   217
  | (Skolem (a,_)) aconv (Skolem (b,_)) = a=b  (*arglists must then be equal*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   218
  | (Free a)       aconv (Free b)       = a=b
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   219
  | (Var(ref(Some t))) aconv u          = t aconv u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   220
  | t aconv (Var(ref(Some u)))          = t aconv u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   221
  | (Var v)        aconv (Var w)        = v=w	(*both Vars are un-assigned*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   222
  | (Bound i)      aconv (Bound j)      = i=j
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   223
  | (Abs(_,t))     aconv (Abs(_,u))     = t aconv u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   224
  | (f$t)          aconv (g$u)          = (f aconv g) andalso (t aconv u)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   225
  | _ aconv _  =  false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   226
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
fun mem_term (_, [])     = false
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   229
  | 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
   230
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   231
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
   232
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   233
fun mem_var (v: term option ref, []) = false
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   234
  | mem_var (v, v'::vs)              = v=v' orelse mem_var(v,vs);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   235
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   236
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
   237
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   238
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   239
(** Vars **)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   240
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   241
(*Accumulates the Vars in the term, suppressing duplicates*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   242
fun add_term_vars (Skolem(a,args),	vars) = add_vars_vars(args,vars)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   243
  | add_term_vars (Var (v as ref None),	vars) = ins_var (v, vars)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   244
  | add_term_vars (Var (ref (Some u)), vars)  = add_term_vars(u,vars)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   245
  | add_term_vars (Abs (_,body),	vars) = add_term_vars(body,vars)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   246
  | add_term_vars (f$t,	vars) =  add_term_vars (f, add_term_vars(t, vars))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   247
  | add_term_vars (_,	vars) = vars
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   248
(*Term list version.  [The fold functionals are slow]*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   249
and add_terms_vars ([],    vars) = vars
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   250
  | 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
   251
(*Var list version.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   252
and add_vars_vars ([],    vars) = vars
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   253
  | add_vars_vars (ref (Some u) :: vs, vars) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   254
	add_vars_vars (vs, add_term_vars(u,vars))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   255
  | add_vars_vars (v::vs, vars) =   (*v must be a ref None*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   256
	add_vars_vars (vs, ins_var (v, vars));
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   257
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   258
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   259
(*Chase assignments in "vars"; return a list of unassigned variables*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   260
fun vars_in_vars vars = add_vars_vars(vars,[]);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   261
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
(*increment a term's non-local bound variables
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   265
     inc is  increment for bound variables
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   266
     lev is  level at which a bound variable is considered 'loose'*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   267
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   268
  | 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
   269
  | 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
   270
  | incr_bv (inc, lev, u) = u;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   271
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   272
fun incr_boundvars  0  t = t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   273
  | incr_boundvars inc t = incr_bv(inc,0,t);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   274
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   275
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   276
(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   277
   (Bound 0) is loose at level 0 *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   278
fun add_loose_bnos (Bound i, lev, js)   = if i<lev then js  
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   279
					  else  (i-lev) ins_int js
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   280
  | 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
   281
  | add_loose_bnos (f$t, lev, js)       =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   282
	        add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   283
  | add_loose_bnos (_, _, js)           = js;
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
fun loose_bnos t = add_loose_bnos (t, 0, []);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   286
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   287
fun subst_bound (arg, t) : term = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   288
  let fun subst (t as Bound i, lev) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   289
 	    if i<lev then  t    (*var is locally bound*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   290
	    else  if i=lev then incr_boundvars lev arg
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   291
		           else Bound(i-1)  (*loose: change it*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   292
	| subst (Abs(a,body), lev) = Abs(a, subst(body,lev+1))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   293
	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   294
	| subst (t,lev)    = t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   295
  in  subst (t,0)  end;
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
(*Normalize...but not the bodies of ABSTRACTIONS*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   299
fun norm t = case t of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   300
    Skolem(a,args)       => Skolem(a, vars_in_vars args)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   301
  | (Var (ref None))     => t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   302
  | (Var (ref (Some u))) => norm u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   303
  | (f $ u) => (case norm f of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   304
		    Abs(_,body) => norm (subst_bound (u, body))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   305
		  | nf => nf $ norm u)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   306
  | _ => t;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   307
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   308
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   309
(*Weak (one-level) normalize for use in unification*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   310
fun wkNormAux t = case t of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   311
    (Var v) => (case !v of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   312
		    Some u => wkNorm u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   313
		  | None   => t)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   314
  | (f $ u) => (case wkNormAux f of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   315
		    Abs(_,body) => wkNorm (subst_bound (u, body))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   316
		  | nf          => nf $ u)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   317
  | _ => t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   318
and wkNorm t = case head_of t of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   319
    Const _        => t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   320
  | OConst _       => t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   321
  | Skolem(a,args) => t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   322
  | Free _         => t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   323
  | _              => wkNormAux t;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   324
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   325
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   326
(*Does variable v occur in u?  For unification.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   327
fun varOccur v = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   328
  let fun occL [] = false	(*same as (exists occ), but faster*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   329
	| occL (u::us) = occ u orelse occL us
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   330
      and occ (Var w) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   331
	      v=w orelse
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   332
              (case !w of None   => false
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   333
	                | Some u => occ u)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   334
        | occ (Skolem(_,args)) = occL (map Var args)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   335
        | occ (Abs(_,u)) = occ u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   336
        | occ (f$u)      = occ u  orelse  occ f
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   337
        | occ (_)        = false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   338
  in  occ  end;
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
exception UNIFY;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   341
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   342
val trail = ref [] : term option ref list ref;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   343
val ntrail = ref 0;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   344
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   345
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   346
(*Restore the trail to some previous state: for backtracking*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   347
fun clearTo n =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   348
    while !ntrail>n do
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   349
	(hd(!trail) := None;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   350
	 trail := tl (!trail);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   351
	 ntrail := !ntrail - 1);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   352
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   353
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   354
(*First-order unification with bound variables.  
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   355
  "vars" is a list of variables local to the rule and NOT to be put
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   356
	on the trail (no point in doing so)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   357
*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   358
fun unify(vars,t,u) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   359
    let val n = !ntrail 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   360
	fun update (t as Var v, u) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   361
	    if t aconv u then ()
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   362
	    else if varOccur v u then raise UNIFY 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   363
	    else if mem_var(v, vars) then v := Some u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   364
		 else (*avoid updating Vars in the branch if possible!*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   365
		      if is_Var u andalso mem_var(dest_Var u, vars)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   366
		      then dest_Var u := Some t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   367
		      else (v := Some u;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   368
			    trail := v :: !trail;  ntrail := !ntrail + 1)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   369
	fun unifyAux (t,u) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   370
	    case (wkNorm t,  wkNorm u) of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   371
		(nt as Var v,  nu) => update(nt,nu)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   372
	      | (nu,  nt as Var v) => update(nt,nu)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   373
	      | (Abs(_,t'),  Abs(_,u')) => unifyAux(t',u')
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   374
		    (*NB: can yield unifiers having dangling Bound vars!*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   375
	      | (f$t',  g$u') => (unifyAux(f,g); unifyAux(t',u'))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   376
	      | (nt,  nu)    => if nt aconv nu then () else raise UNIFY
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   377
    in  unifyAux(t,u) handle UNIFY => (clearTo n; raise UNIFY)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   378
    end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   379
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
(*Convert from "real" terms to prototerms; eta-contract*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   382
fun fromTerm tsig t =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   383
  let val alist = ref []
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   384
      fun from (t as Term.Const _) = fromConst tsig t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   385
	| from (Term.Free  (a,_)) = Free a
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   386
	| from (Term.Bound i)     = Bound i
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   387
	| from (Term.Var (ixn,T)) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   388
	      (case (assoc_string_int(!alist,ixn)) of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   389
		   None => let val t' = Var(ref None)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   390
		           in  alist := (ixn, (t', T)) :: !alist;  t'
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   391
			   end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   392
		 | Some (v,_) => v)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   393
	| from (Term.Abs (a,_,u)) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   394
	      (case  from u  of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   395
		u' as (f $ Bound 0) => 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   396
		  if (0 mem_int loose_bnos f) then Abs(a,u')
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   397
		  else incr_boundvars ~1 f 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   398
	      | u' => Abs(a,u'))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   399
	| from (Term.$ (f,u)) = from f $ from u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   400
  in  from t  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   401
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   402
(* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   403
fun strip_imp_prems (Const"==>" $ (Const"Trueprop" $ A) $ B) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   404
           A :: strip_imp_prems B
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   405
  | strip_imp_prems (Const"==>" $ A $ B) = A :: strip_imp_prems B
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   406
  | strip_imp_prems _ = [];
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   407
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   408
(* A1==>...An==>B  goes to B, where B is not an implication *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   409
fun strip_imp_concl (Const"==>" $ A $ B) = strip_imp_concl B
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   410
  | strip_imp_concl (Const"Trueprop" $ A) = A
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   411
  | strip_imp_concl A = A : term;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   412
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   413
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   414
(*** Conversion of Elimination Rules to Tableau Operations ***)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   415
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   416
(*The conclusion becomes the goal/negated assumption *False*: delete it!*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   417
fun squash_nots [] = []
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   418
  | squash_nots (Const "*Goal*" $ (Var (ref (Some (Const"*False*")))) :: Ps) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   419
	squash_nots Ps
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   420
  | squash_nots (Const "Not" $ (Var (ref (Some (Const"*False*")))) :: Ps) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   421
	squash_nots Ps
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   422
  | squash_nots (P::Ps) = P :: squash_nots Ps;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   423
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   424
fun skoPrem vars (Const "all" $ Abs (_, P)) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   425
        skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   426
  | skoPrem vars P = P;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   427
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   428
fun convertPrem t = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   429
    squash_nots (mkGoal (strip_imp_concl t) :: strip_imp_prems t);
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
(*Expects elimination rules to have a formula variable as conclusion*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   432
fun convertRule vars t =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   433
  let val (P::Ps) = strip_imp_prems t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   434
      val Var v   = strip_imp_concl t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   435
  in  v := Some (Const"*False*");
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   436
      (P, map (convertPrem o skoPrem vars) Ps) 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   437
  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   438
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   439
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   440
(*Like dup_elim, but puts the duplicated major premise FIRST*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   441
fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   442
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   443
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   444
(*Count new hyps so that they can be rotated*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   445
fun nNewHyps []                         = 0
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   446
  | nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   447
  | nNewHyps (P::Ps)                    = 1 + nNewHyps Ps;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   448
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   449
fun rot_subgoals_tac [] i st      = Sequence.single st
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   450
  | rot_subgoals_tac (k::ks) i st =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   451
      rot_subgoals_tac ks (i+1) (Sequence.hd (rotate_tac (~k) i st))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   452
      handle OPTION _ => Sequence.null;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   453
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   454
fun TRACE rl tac st = if !trace then (prth rl; tac st) else tac st;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   455
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   456
(*Tableau rule from elimination rule.  Flag "dup" requests duplication of the
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   457
  affected formula.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   458
fun fromRule vars rl = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   459
  let val {tsig,...} = Sign.rep_sg (#sign (rep_thm rl))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   460
      val trl = rl |> rep_thm |> #prop |> fromTerm tsig |> convertRule vars
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   461
      fun tac dup i = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   462
	  TRACE rl
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   463
	  (etac (if dup then rev_dup_elim rl else rl) i)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   464
	  THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i
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
  in General.SOME (trl, tac) end
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   467
  handle Bind => (*reject: conclusion is not just a variable*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   468
   (if !trace then (writeln"Warning: ignoring ill-formed elimination rule";
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   469
		    print_thm rl)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   470
    else ();
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   471
    General.NONE);
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   472
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   473
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   474
(*** Conversion of Introduction Rules (needed for efficiency in 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   475
               proof reconstruction) ***)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   476
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   477
fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   478
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   479
fun convertIntrRule vars t =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   480
  let val Ps = strip_imp_prems t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   481
      val P  = strip_imp_concl t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   482
  in  (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps) 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   483
  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   484
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   485
(*Tableau rule from introduction rule.  Since haz rules are now delayed, 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   486
  "dup" is always FALSE for introduction rules.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   487
fun fromIntrRule vars rl = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   488
  let val {tsig,...} = Sign.rep_sg (#sign (rep_thm rl))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   489
      val trl = rl |> rep_thm |> #prop |> fromTerm tsig |> convertIntrRule vars
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   490
      fun tac dup i = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   491
	  TRACE rl (DETERM (rtac (if dup then Data.dup_intr rl else rl) i))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   492
	  THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   493
  in (trl, tac) end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   494
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   495
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   496
val dummyVar = Term.Var (("Doom",666), dummyT);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   497
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   498
(*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
   499
  Ignore abstractions; identify all Vars; STOP at given depth*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   500
fun toTerm 0 _             = dummyVar
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   501
  | toTerm d (Const a)     = Term.Const (a,dummyT)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   502
  | toTerm d (OConst(a,_)) = Term.Const (a,dummyT)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   503
  | toTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   504
  | toTerm d (Free a)      = Term.Free  (a,dummyT)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   505
  | toTerm d (Bound i)     = Term.Bound i
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   506
  | toTerm d (Var _)       = dummyVar
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   507
  | toTerm d (Abs(a,_))    = dummyVar
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   508
  | 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
   509
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   510
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   511
fun netMkRules P vars (nps: netpair list) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   512
  case P of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   513
      (Const "*Goal*" $ G) =>
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   514
	let val pG = mk_tprop (toTerm 2 G)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   515
	    val intrs = List.concat 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   516
		             (map (fn (inet,_) => Net.unify_term inet pG) 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   517
			      nps)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   518
	in  map (fromIntrRule vars o #2) (orderlist intrs)  end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   519
    | _ =>
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   520
	let val pP = mk_tprop (toTerm 3 P)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   521
	    val elims = List.concat 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   522
		             (map (fn (_,enet) => Net.unify_term enet pP) 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   523
			      nps)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   524
	in  List.mapPartial (fromRule vars o #2) (orderlist elims)  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   525
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   526
(**
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   527
end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   528
**)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   529
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   530
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   531
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   532
(*Replace the ATOMIC term "old" by "new" in t*)  
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   533
fun subst_atomic (old,new) t =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   534
    let fun subst (Var(ref(Some u))) = subst u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   535
	  | subst (Abs(a,body))      = Abs(a, subst body)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   536
	  | subst (f$t)              = subst f $ subst t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   537
	  | subst t                  = if t aconv old then new else t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   538
    in  subst t  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   539
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   540
(*Eta-contract a term from outside: just enough to reduce it to an atom*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   541
fun eta_contract_atom (t0 as Abs(a, body)) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   542
      (case  eta_contract2 body  of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   543
        f $ Bound 0 => if (0 mem_int loose_bnos f) then t0
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   544
		       else eta_contract_atom (incr_boundvars ~1 f)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   545
      | _ => t0)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   546
  | eta_contract_atom t = t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   547
and eta_contract2 (f$t) = f $ eta_contract_atom t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   548
  | eta_contract2 t     = eta_contract_atom t;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   549
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   550
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   551
(*When can we safely delete the equality?
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   552
    Not if it equates two constants; consider 0=1.
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   553
    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
   554
    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
   555
  Prefer to eliminate Bound variables if possible.
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   556
  Result:  true = use as is,  false = reorient first *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   557
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   558
(*Does t occur in u?  For substitution.  
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   559
  Does NOT check args of Skolem terms: substitution does not affect them.
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   560
  NOT reflexive since hyp_subst_tac fails on x=x.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   561
fun substOccur t = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   562
  let fun occEq u = (t aconv u) orelse occ u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   563
      and occ (Var(ref None))    = false
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   564
	| occ (Var(ref(Some u))) = occEq u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   565
        | occ (Abs(_,u))         = occEq u
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   566
        | occ (f$u)              = occEq u  orelse  occEq f
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   567
        | occ (_)                = false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   568
  in  occEq  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   569
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   570
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
   571
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   572
(*IF the goal is an equality with a substitutable variable 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   573
  THEN orient that equality ELSE raise exception DEST_EQ*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   574
fun orientGoal (t,u) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   575
  case (eta_contract_atom t, eta_contract_atom u) of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   576
       (Skolem _, _) => check(t,u,(t,u))	(*eliminates t*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   577
     | (_, Skolem _) => check(u,t,(u,t))	(*eliminates u*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   578
     | (Free _, _)   => check(t,u,(t,u))	(*eliminates t*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   579
     | (_, Free _)   => check(u,t,(u,t))	(*eliminates u*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   580
     | _             => raise DEST_EQ;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   581
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   582
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   583
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   584
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   585
(*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
   586
  Moves affected literals back into the branch, but it is not clear where
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   587
  they should go: this could make proofs fail.  ??? *)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   588
fun equalSubst (G, pairs, lits, vars, lim) = 
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   589
  let val subst = subst_atomic (orientGoal(dest_eq G))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   590
      fun subst2(G,md) = (subst G, md)
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   591
      (*substitute throughout Haz list; move affected ones to Safe part*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   592
      fun subHazs ([], Gs, nHs)         = (Gs,nHs)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   593
	| subHazs ((H,md)::Hs, Gs, nHs) =
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   594
	    let val nH = subst H
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   595
	    in  if nH aconv H then subHazs (Hs, Gs, (H,md)::nHs)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   596
		              else subHazs (Hs, (nH,md)::Gs, nHs)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   597
            end
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   598
      val pairs' = map (fn(Gs,Hs) => subHazs(rev Hs, map subst2 Gs, [])) pairs
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   599
      (*substitute throughout literals; move affected ones to Safe part*)
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   600
      fun subLits ([], [], nlits) =          (pairs', nlits, vars, lim)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   601
	| subLits ([], Gs, nlits) = ((Gs,[])::pairs', nlits, vars, lim)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   602
	| subLits (lit::lits, Gs, nlits) =
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   603
	    let val nlit = subst lit
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   604
	    in  if nlit aconv lit then subLits (lits, Gs, nlit::nlits)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   605
		                  else subLits (lits, (nlit,true)::Gs, nlits)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   606
            end
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   607
  in  subLits (rev lits, [], [])  
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   608
  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   609
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   610
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   611
exception NEWBRANCHES and CLOSEF;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   612
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   613
(*Pending formulae carry md (may duplicate) flags*)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   614
type branch = ((term*bool) list *	(*safe formulae on this level*)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   615
               (term*bool) list) list * (*haz formulae  on this level*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   616
	      term list *               (*literals: irreducible formulae*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   617
	      term option ref list *    (*variables occurring in branch*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   618
	      int;                      (*resource limit*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   619
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   620
val fullTrace = ref[] : branch list list ref;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   621
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   622
(*Normalize a branch--for tracing*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   623
local
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   624
    fun norm2 (G,md) = (norm G, md);
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   625
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   626
    fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs);
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   627
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   628
in
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   629
fun normBr (br, lits, vars, lim) =
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   630
     (map normLev br, map norm lits, vars, lim);
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   631
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   632
fun tracing brs = if !trace then fullTrace := map normBr brs :: !fullTrace 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   633
		else ()
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   634
end;
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   635
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   636
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   637
exception PROVE;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   638
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   639
val eq_contr_tac = eresolve_tac [Data.notE]  THEN'  eq_assume_tac;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   640
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   641
val eContr_tac  = TRACE Data.notE (eq_contr_tac ORELSE' Data.contr_tac);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   642
val eAssume_tac = TRACE asm_rl   (eq_assume_tac ORELSE' assume_tac);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   643
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   644
(*Try to unify complementary literals and return the corresponding tactic. *) 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   645
fun tryClose (Const"*Goal*" $ G,  L) = (unify([],G,L); eAssume_tac)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   646
  | tryClose (G,  Const"*Goal*" $ L) = (unify([],G,L); eAssume_tac)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   647
  | tryClose (Const"Not" $ G,  L)    = (unify([],G,L); eContr_tac)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   648
  | tryClose (G,  Const"Not" $ L)    = (unify([],G,L); eContr_tac)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   649
  | tryClose _                       = raise UNIFY;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   650
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   651
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   652
(*Were there Skolem terms in the premise?  Must NOT chase Vars*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   653
fun hasSkolem (Skolem _)     = true
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   654
  | hasSkolem (Abs (_,body)) = hasSkolem body 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   655
  | hasSkolem (f$t)          =  hasSkolem f orelse hasSkolem t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   656
  | hasSkolem _              = false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   657
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   658
(*Attach the right "may duplicate" flag to new formulae: if they contain
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   659
  Skolem terms then allow duplication.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   660
fun joinMd md [] = []
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   661
  | joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   662
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   663
(*Convert a Goal to an ordinary Not.  Used also in dup_intr, where a goal like
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   664
  Ex(P) is duplicated as the assumption ~Ex(P). *)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   665
fun negOfGoal (Const"*Goal*" $ G) = negate G
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   666
  | negOfGoal G                   = G;
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   667
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   668
fun negOfGoal2 (G,md) = (negOfGoal G, md);
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   669
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   670
(*Converts all Goals to Nots in the safe parts of a branch.  They could
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   671
  have been moved there from the literals list after substitution (equalSubst).
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   672
  There can be at most one--this function could be made more efficient.*)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   673
fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   674
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   675
(*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   676
val negOfGoal_tac = rtac Data.ccontr THEN' rotate_tac ~1;
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   677
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   678
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   679
(** Backtracking and Pruning **)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   680
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   681
(*clashVar vars (n,trail) determines whether any of the last n elements
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   682
  of "trail" occur in "vars" OR in their instantiations*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   683
fun clashVar [] = (fn _ => false)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   684
  | clashVar vars =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   685
      let fun clash (0, _)     = false
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   686
	    | clash (_, [])    = false
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   687
	    | clash (n, v::vs) = exists (varOccur v) vars orelse clash(n-1,vs)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   688
      in  clash  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   689
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   690
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   691
(*nbrs = # of branches just prior to closing this one.  Delete choice points
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   692
  for goals proved by the latest inference, provided NO variables in the
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   693
  next branch have been updated.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   694
fun prune (1, nxtVars, choices) = choices  (*DON'T prune at very end: allow 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   695
					     backtracking over bad proofs*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   696
  | prune (nbrs, nxtVars, choices) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   697
      let fun traceIt last =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   698
		let val ll = length last
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   699
		    and lc = length choices
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   700
		in if !trace andalso ll<lc then
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   701
		    (writeln("PRUNING " ^ Int.toString(lc-ll) ^ " LEVELS"); 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   702
		     last)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   703
		   else last
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   704
		end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   705
	  fun pruneAux (last, _, _, []) = last
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   706
	    | pruneAux (last, ntrl, trl, ch' as (ntrl',nbrs',exn) :: choices) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   707
		if nbrs' < nbrs 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   708
		then last  (*don't backtrack beyond first solution of goal*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   709
		else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   710
		else (* nbrs'=nbrs *)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   711
		     if clashVar nxtVars (ntrl-ntrl', trl) then last
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   712
		     else (*no clashes: can go back at least this far!*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   713
			  pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'), 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   714
				   choices)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   715
  in  traceIt (pruneAux (choices, !ntrail, !trail, choices))  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   716
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   717
fun nextVars ((br, lits, vars, lim) :: _) = map Var vars
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   718
  | nextVars []                                 = [];
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   719
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   720
fun backtrack ((_, _, exn)::_) = raise exn
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   721
  | backtrack _                = raise PROVE;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   722
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   723
(*Add the literal G, handling *Goal* and detecting duplicates.*)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   724
fun addLit (Const "*Goal*" $ G, lits) = 
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   725
      (*New literal is a *Goal*, so change all other Goals to Nots*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   726
      let fun bad (Const"*Goal*" $ _) = true
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   727
	    | bad (Const"Not" $ G')   = G aconv G'
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   728
	    | bad _                   = false;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   729
	  fun change [] = []
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   730
	    | change (Const"*Goal*" $ G' :: lits) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   731
		  if G aconv G' then change lits
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   732
		  else Const"Not" $ G' :: change lits
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   733
	    | change (Const"Not" $ G' :: lits)    = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   734
		  if G aconv G' then change lits
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   735
		  else Const"Not" $ G' :: change lits
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   736
	    | change (lit::lits) = lit :: change lits
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   737
      in
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   738
	Const "*Goal*" $ G :: (if exists bad lits then change lits else lits)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   739
      end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   740
  | addLit (G,lits) = ins_term(G, lits)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   741
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   742
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   743
(*For calculating the "penalty" to assess on a branching factor of n*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   744
fun log2 1 = 0
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   745
  | log2 n = 1 + log2(n div 2);
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   746
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   747
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   748
(*Tableau prover based on leanTaP.  Argument is a list of branches.  Each 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   749
  branch contains a list of unexpanded formulae, a list of literals, and a 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   750
  bound on unsafe expansions.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   751
fun prove (cs, brs, cont) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   752
 let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   753
     val safeList = [safe0_netpair, safep_netpair]
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   754
     and hazList  = [haz_netpair]
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   755
     fun prv (tacs, trs, choices, []) = (cont (trs,choices,tacs))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   756
       | prv (tacs, trs, choices, 
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   757
	      brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) =
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   758
	  let exception PRV (*backtrack to precisely this recursion!*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   759
	      val ntrl = !ntrail 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   760
	      val nbrs = length brs0
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   761
              val nxtVars = nextVars brs
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   762
	      val G = norm G
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   763
	      val rules = netMkRules G vars safeList
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   764
	      (*Make a new branch, decrementing "lim" if instantiations occur*)
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   765
	      fun newBr (vars',lim') prems =
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   766
		  map (fn prem => 
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   767
		       if (exists isGoal prem) 
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   768
		       then (((joinMd md prem, []) :: 
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   769
			      negOfGoals ((br, haz)::pairs)),
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   770
			     map negOfGoal lits, 
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   771
			     vars', lim') 
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   772
		       else (((joinMd md prem, []) :: (br, haz) :: pairs),
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   773
			     lits, vars', lim'))
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   774
		  prems @
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   775
		  brs		  
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   776
	      (*Seek a matching rule.  If unifiable then add new premises
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   777
                to branch.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   778
	      fun deeper [] = raise NEWBRANCHES
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   779
		| deeper (((P,prems),tac)::grls) =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   780
		    let val dummy = unify(add_term_vars(P,[]), P, G)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   781
			    (*P comes from the rule; G comes from the branch.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   782
                        val ntrl' = !ntrail
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   783
			val lim' = if ntrl < !ntrail 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   784
				   then lim - (1+log2(length rules))
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   785
				   else lim   (*discourage branching updates*)
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   786
                        val vars  = vars_in_vars vars
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   787
                        val vars' = foldr add_terms_vars (prems, vars)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   788
			val choices' = (ntrl, nbrs, PRV) :: choices
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   789
                        val tacs' = (DETERM o (tac false)) :: tacs 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   790
		                        (*no duplication*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   791
                    in
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   792
			if null prems then (*closed the branch: prune!*)
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   793
			  prv(tacs',  brs0::trs, 
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   794
			      prune (nbrs, nxtVars, choices'),
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   795
			      brs)
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   796
			  handle PRV => (*reset Vars and try another rule*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   797
			      (clearTo ntrl;  deeper grls)
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   798
		        else (*can we kill all the alternatives??*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   799
			if lim'<0 then raise NEWBRANCHES
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   800
			else
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   801
			  prv(tacs',  brs0::trs, choices',
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   802
			      newBr (vars',lim') prems)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   803
			  handle PRV => 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   804
			      if ntrl < ntrl' then
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   805
				   (*Vars have been updated: must backtrack
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   806
				     even if not mentioned in other goals!
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   807
				     Reset Vars and try another rule*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   808
				   (clearTo ntrl;  deeper grls)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   809
			      else (*backtrack to previous level*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   810
				   backtrack choices
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   811
		    end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   812
		    handle UNIFY => deeper grls
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   813
	      (*Try to close branch by unifying with head goal*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   814
	      fun closeF [] = raise CLOSEF
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   815
		| closeF (L::Ls) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   816
		    let val tacs' = tryClose(G,L)::tacs
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   817
			val choices' = prune (nbrs, nxtVars, 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   818
					      (ntrl, nbrs, PRV) :: choices)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   819
		    in  prv (tacs', brs0::trs, choices', brs)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   820
			handle PRV => 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   821
			    (*reset Vars and try another literal
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   822
			      [this handler is pruned if possible!]*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   823
			 (clearTo ntrl;  closeF Ls)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   824
                    end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   825
		    handle UNIFY => closeF Ls
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   826
	      fun closeFl [] = raise CLOSEF
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   827
		| closeFl ((br, haz)::pairs) =
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   828
		    closeF (map fst br)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   829
		      handle CLOSEF => closeF (map fst haz)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   830
			handle CLOSEF => closeFl pairs
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   831
	  in tracing brs0;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   832
	     if lim<0 then backtrack choices
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   833
	     else
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   834
	     prv (Data.vars_gen_hyp_subst_tac false :: tacs, 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   835
		  brs0::trs,  choices,
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   836
		  equalSubst (G, (br,haz)::pairs, lits, vars, lim) :: brs)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   837
	     handle DEST_EQ => closeF lits
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   838
	      handle CLOSEF => closeFl ((br,haz)::pairs)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   839
	        handle CLOSEF => 
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   840
		 deeper rules
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   841
		  handle NEWBRANCHES => 
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   842
		   (case netMkRules G vars hazList of
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   843
		       [] => (*no plausible rules: move G to literals*)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   844
			   prv (tacs, brs0::trs, choices,
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   845
				((br,haz)::pairs, addLit(G,lits), vars, lim)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   846
				::brs)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   847
		    | _ => (*G admits some haz rules: try later*)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   848
			   prv (if isGoal G then negOfGoal_tac :: tacs
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   849
				else tacs, 
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   850
				brs0::trs,  choices,
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   851
				((br, haz@[(negOfGoal G, md)])::pairs,
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   852
				 lits, vars, lim)  ::  brs))
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   853
	  end
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   854
       | prv (tacs, trs, choices, 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   855
	      (([],haz)::(Gs,haz')::pairs, lits, vars, lim) :: brs) =
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   856
	     (*no more "safe" formulae: transfer haz down a level*)
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   857
	   prv (tacs, trs, choices, 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   858
		((Gs,haz@haz')::pairs, lits, vars, lim) :: brs)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   859
       | prv (tacs, trs, choices, 
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   860
	      brs0 as ([([], (H,md)::Hs)], lits, vars, lim) :: brs) =
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   861
   	     (*no safe steps possible at any level: apply a haz rule*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   862
	  let exception PRV (*backtrack to precisely this recursion!*)
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   863
	      val H = norm H
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   864
	      val ntrl = !ntrail
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   865
	      val rules = netMkRules H vars hazList
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   866
	      fun newPrem (vars,dup,lim') prem = 
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   867
		  ([(map (fn P => (P,false)) prem, []), (*may NOT duplicate*)
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   868
		    ([], if dup then Hs @ [(negOfGoal H, md)] else Hs)],  
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   869
		   lits, vars, lim')
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   870
	      fun newBr x prems = map (newPrem x) prems  @  brs
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   871
	      (*Seek a matching rule.  If unifiable then add new premises
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   872
                to branch.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   873
	      fun deeper [] = raise NEWBRANCHES
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   874
		| deeper (((P,prems),tac)::grls) =
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   875
		    let val dummy = unify(add_term_vars(P,[]), P, H)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   876
			val ntrl' = !ntrail
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   877
                        val vars  = vars_in_vars vars
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   878
                        val vars' = foldr add_terms_vars (prems, vars)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   879
                        val dup = md andalso vars' <> vars
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   880
			(*duplicate H only if md and the premise has new vars*)
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   881
			val lim' = (*Decrement "lim" extra if updates occur*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   882
			    if ntrl < !ntrail then lim - (1+log2(length rules))
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   883
			    else lim-1
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   884
			    (*NB: if the formula is duplicated, 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   885
			      then it seems plausible to leave lim alone.  
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   886
			      But then transitivity laws loop.*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   887
                        val mayUndo = not (null grls)   (*other rules to try?*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   888
				    orelse ntrl < ntrl'  (*variables updated?*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   889
				    orelse vars=vars'    (*no new Vars?*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   890
                        val tac' = if mayUndo then tac dup
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   891
                                   else DETERM o (tac dup) 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   892
		    in
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   893
		      (*can we kill all the alternatives??*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   894
		      if lim'<0 andalso not (null prems)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   895
		      then raise NEWBRANCHES
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   896
		      else 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   897
			prv(tac dup :: tacs, 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   898
			    brs0::trs, 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   899
			    (ntrl, length brs0, PRV) :: choices, 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   900
			    newBr (vars', dup, lim') prems)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   901
			 handle PRV => 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   902
			     if mayUndo
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   903
			     then (*reset Vars and try another rule*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   904
				  (clearTo ntrl;  deeper grls)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   905
			     else (*backtrack to previous level*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   906
				  backtrack choices
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   907
		    end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   908
		    handle UNIFY => deeper grls
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   909
	  in tracing brs0;
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   910
	     if lim<1 then backtrack choices
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
   911
	     else deeper rules
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   912
	     handle NEWBRANCHES => 
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   913
		 (*cannot close branch: move H to literals*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   914
		 prv (tacs,  brs0::trs,  choices,
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   915
		      ([([], Hs)], H::lits, vars, lim)::brs)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   916
	  end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   917
       | prv (tacs, trs, choices, _ :: brs) = backtrack choices
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   918
 in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   919
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   920
2883
fd1c0b8e9b61 Now exports declConsts!
paulson
parents: 2854
diff changeset
   921
(*Construct an initial branch.*)
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   922
fun initBranch (ts,lim) = 
2894
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   923
    ([(map (fn t => (t,true)) ts, [])],
d2ffee4f811b Re-organization of the order of haz rules
paulson
parents: 2883
diff changeset
   924
     [], add_terms_vars (ts,[]), lim);
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   925
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   926
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   927
(*** Conversion & Skolemization of the Isabelle proof state ***)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   928
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   929
(*Make a list of all the parameters in a subgoal, even if nested*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   930
local open Term 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   931
in
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   932
fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   933
  | discard_foralls t = t;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   934
end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   935
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   936
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   937
(*List of variables not appearing as arguments to the given parameter*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   938
fun getVars []                  i = []
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   939
  | getVars ((_,(v,is))::alist) i =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   940
	if i mem is then getVars alist i
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   941
	else v :: getVars alist i;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   942
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   943
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   944
(*Conversion of a subgoal: Skolemize all parameters*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   945
fun fromSubgoal tsig t =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   946
  let val alist = ref []
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   947
      fun hdvar ((ix,(v,is))::_) = v
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   948
      fun from lev t =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   949
	let val (ht,ts) = Term.strip_comb t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   950
	    fun apply u = list_comb (u, map (from lev) ts)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   951
	    fun bounds [] = []
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   952
	      | bounds (Term.Bound i::ts) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   953
		  if i<lev then error"Function Var's argument not a parameter"
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   954
		  else i-lev :: bounds ts
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   955
	      | bounds ts = error"Function Var's argument not a bound variable"
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   956
        in
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   957
	  case ht of 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   958
	      t as Term.Const _ => apply (fromConst tsig t)	    
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   959
	    | Term.Free  (a,_) => apply (Free a)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   960
	    | Term.Bound i     => apply (Bound i)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   961
	    | Term.Var (ix,_) => 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   962
		  (case (assoc_string_int(!alist,ix)) of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   963
		       None => (alist := (ix, (ref None, bounds ts))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   964
					  :: !alist;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   965
				Var (hdvar(!alist)))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   966
		     | Some(v,is) => if is=bounds ts then Var v
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   967
			    else error("Discrepancy among occurrences of ?"
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   968
				       ^ Syntax.string_of_vname ix))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   969
	    | Term.Abs (a,_,body) => 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   970
		  if null ts then Abs(a, from (lev+1) body)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   971
		  else error "fromSubgoal: argument not in normal form"
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   972
        end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   973
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   974
      val npars = length (Logic.strip_params t)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   975
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   976
      (*Skolemize a subgoal from a proof state*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   977
      fun skoSubgoal i t =
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   978
	  if i<npars then 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   979
	      skoSubgoal (i+1)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   980
		(subst_bound (Skolem (gensym "SG_", getVars (!alist) i), 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   981
			      t))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   982
	  else t
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   983
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   984
  in  skoSubgoal 0 (from 0 (discard_foralls t))  end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   985
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   986
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   987
(*Tactic using tableau engine and proof reconstruction.  
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   988
 "lim" is depth limit.*)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   989
fun depth_tac cs lim i st = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   990
    (fullTrace:=[];  trail := [];  ntrail := 0;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   991
     let val {tsig,...} = Sign.rep_sg (#sign (rep_thm st))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   992
	 val skoprem = fromSubgoal tsig (List.nth(prems_of st, i-1))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   993
         val hyps  = strip_imp_prems skoprem
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   994
         and concl = strip_imp_concl skoprem
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   995
         fun cont (_,choices,tacs) = 
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   996
	     (case Sequence.pull(EVERY' (rev tacs) i st) of
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   997
		  None => (writeln ("PROOF FAILED for depth " ^
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   998
				    Int.toString lim);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
   999
			   backtrack choices)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1000
		| cell => Sequence.seqof(fn()=> cell))
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1001
     in prove (cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1002
     end
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1003
     handle Subscript => Sequence.null
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1004
	  | PROVE     => Sequence.null);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1005
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1006
fun blast_tac cs = (DEEPEN (1,20) (depth_tac cs) 0);
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1007
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1008
fun Blast_tac i = blast_tac (!Data.claset) i;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1009
2924
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1010
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1011
(*** For debugging: these apply the prover to a subgoal and return 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1012
     the resulting tactics, trace, etc.                            ***)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1013
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1014
(*Translate subgoal i from a proof state*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1015
fun trygl cs lim i = 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1016
    (fullTrace:=[];  trail := [];  ntrail := 0;
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1017
     let val st = topthm()
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1018
         val {tsig,...} = Sign.rep_sg (#sign (rep_thm st))
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1019
	 val skoprem = fromSubgoal tsig (List.nth(prems_of st, i-1))
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1020
         val hyps  = strip_imp_prems skoprem
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1021
         and concl = strip_imp_concl skoprem
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1022
     in timeap prove
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1023
	 (cs, [initBranch (mkGoal concl :: hyps, lim)], I)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1024
     end
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1025
     handle Subscript => error("There is no subgoal " ^ Int.toString i));
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1026
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1027
fun Trygl lim i = trygl (!Data.claset) lim i;
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1028
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1029
(*Read a string to make an initial, singleton branch*)
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1030
fun readGoal sign s = read_cterm sign (s,propT) |>
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1031
                      term_of |> fromTerm (#tsig(Sign.rep_sg sign)) |> 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1032
		      rand |> mkGoal;
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1033
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1034
fun tryInThy thy lim s = 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1035
    (fullTrace:=[];  trail := [];  ntrail := 0;
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1036
     timeap prove (!Data.claset, 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1037
		   [initBranch ([readGoal (sign_of thy) s], lim)], 
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1038
		   I));
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1039
af506c35b4ed Control over excessive branching by applying a log2 penalty
paulson
parents: 2894
diff changeset
  1040
2854
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1041
end;
f03b1652fc6a Implementation of blast_tac: fast tableau prover
paulson
parents:
diff changeset
  1042