src/Provers/hypsubst.ML
author clasohm
Tue, 24 Oct 1995 14:45:35 +0100
changeset 1294 1358dc040edb
parent 1011 5c9654e2e3de
child 2143 093bbe6d333b
permissions -rw-r--r--
added calls of init_html and make_chart; added usage of qed
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	Provers/hypsubst
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
     3
    Authors: 	Martin D Coen, Tobias Nipkow and Lawrence C Paulson
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
     4
    Copyright   1995  University of Cambridge
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
     5
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
     6
Tactic to substitute using the assumption x=t in the rest of the subgoal,
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
     7
and to delete that assumption.  Original version due to Martin Coen.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
     8
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
     9
This version uses the simplifier, and requires it to be already present.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    10
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    11
Test data:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    13
goal thy "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    14
goal thy "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    15
goal thy "!!y. [| ?x=y; P(?x) |] ==> y = a";
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    16
goal thy "!!z. [| ?x=y; P(?x) |] ==> y = a";
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    17
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    18
by (hyp_subst_tac 1);
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    19
by (bound_hyp_subst_tac 1);
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    20
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    21
Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    22
goal thy "P(a) --> (EX y. a=y --> P(f(a)))";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
signature HYPSUBST_DATA =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  sig
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    27
  structure Simplifier : SIMPLIFIER
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    28
  val dest_eq	       : term -> term*term
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    29
  val eq_reflection    : thm		   (* a=b ==> a==b *)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    30
  val imp_intr	       : thm		   (* (P ==> Q) ==> P-->Q *)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    31
  val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    32
  val subst	       : thm		   (* [| a=b;  P(a) |] ==> P(b) *)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    33
  val sym	       : thm		   (* a=b ==> b=a *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    36
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
signature HYPSUBST =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  sig
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    39
  val bound_hyp_subst_tac    : int -> tactic
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    40
  val hyp_subst_tac          : int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
    (*exported purely for debugging purposes*)
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    42
  val gen_hyp_subst_tac      : bool -> int -> tactic
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    43
  val vars_gen_hyp_subst_tac : bool -> int -> tactic
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    44
  val eq_var                 : bool -> bool -> term -> int * bool
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    45
  val inspect_pair           : bool -> bool -> term * term -> bool
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    46
  val mk_eqs                 : thm -> thm list
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    47
  val thin_leading_eqs_tac   : bool -> int -> int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
local open Data in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
exception EQ_VAR;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    59
local val odot = ord"."
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    60
in
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    61
(*Simplifier turns Bound variables to dotted Free variables: 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    62
  change it back (any Bound variable will do)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    63
*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    64
fun contract t =
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    65
    case Pattern.eta_contract t of
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    66
	Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    67
      | t'        => t'
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    68
end;
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    69
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    70
fun has_vars t = maxidx_of_term t <> ~1;
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    71
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    72
(*If novars then we forbid Vars in the equality.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    73
  If bnd then we only look for Bound (or dotted Free) variables to eliminate. 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    74
  When can we safely delete the equality?
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    75
    Not if it equates two constants; consider 0=1.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    76
    Not if it resembles x=t[x], since substitution does not eliminate x.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    77
    Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    78
    Not if it involves a variable free in the premises, 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    79
        but we can't check for this -- hence bnd and bound_hyp_subst_tac
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    80
  Prefer to eliminate Bound variables if possible.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    81
  Result:  true = use as is,  false = reorient first *)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    82
fun inspect_pair bnd novars (t,u) =
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    83
  case (contract t, contract u) of
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    84
       (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    85
		       then raise Match 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    86
		       else true		(*eliminates t*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    87
     | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t  
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    88
		       then raise Match 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    89
		       else false		(*eliminates u*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    90
     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse  
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    91
		          novars andalso has_vars u  
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    92
		       then raise Match 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    93
		       else true		(*eliminates t*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    94
     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse  
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    95
		          novars andalso has_vars t 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    96
		       then raise Match 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    97
		       else false		(*eliminates u*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
     | _ => raise Match;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   100
(*Locates a substitutable variable on the left (resp. right) of an equality
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   101
   assumption.  Returns the number of intervening assumptions. *)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   102
fun eq_var bnd novars =
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   103
  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   104
	| eq_var_aux k (Const("==>",_) $ A $ B) = 
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   105
	      ((k, inspect_pair bnd novars (dest_eq A))
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   106
		      (*Exception comes from inspect_pair or dest_eq*)
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   107
	       handle Match => eq_var_aux (k+1) B)
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   108
	| eq_var_aux k _ = raise EQ_VAR
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   109
  in  eq_var_aux 0  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   111
(*We do not try to delete ALL equality assumptions at once.  But
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   112
  it is easy to handle several consecutive equality assumptions in a row.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   113
  Note that we have to inspect the proof state after doing the rewriting,
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   114
  since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   115
  must NOT be deleted.  Tactic must rotate or delete m assumptions.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   116
*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   117
fun thin_leading_eqs_tac bnd m i = STATE(fn state =>
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   118
    let fun count []      = 0
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   119
	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);  
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   120
			      1 + count Bs)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   121
                             handle Match => 0)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   122
	val (_,_,Bi,_) = dest_state(state,i)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   123
        val j = min [m, count (Logic.strip_assums_hyp Bi)]
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   124
    in  REPEAT_DETERM_N j     (etac thin_rl i)   THEN
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   125
        REPEAT_DETERM_N (m-j) (etac revcut_rl i)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   126
    end);
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   127
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   128
(*For the simpset.  Adds ALL suitable equalities, even if not first!
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   129
  No vars are allowed here, as simpsets are built from meta-assumptions*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   130
fun mk_eqs th = 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   131
    [ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th)))
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   132
      then th RS Data.eq_reflection
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   133
      else symmetric(th RS Data.eq_reflection) (*reorient*) ] 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   134
    handle Match => [];  (*Exception comes from inspect_pair or dest_eq*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   135
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   136
local open Simplifier 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   137
in
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   138
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   139
  val hyp_subst_ss = empty_ss setmksimps mk_eqs
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   140
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   141
  (*Select a suitable equality assumption and substitute throughout the subgoal
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   142
    Replaces only Bound variables if bnd is true*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   143
  fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   144
	let val (_,_,Bi,_) = dest_state(state,i)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   145
	    val n = length(Logic.strip_assums_hyp Bi) - 1
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   146
	    val (k,_) = eq_var bnd true Bi
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   147
	in 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   148
	   EVERY [REPEAT_DETERM_N k (etac revcut_rl i),
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   149
		  asm_full_simp_tac hyp_subst_ss i,
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   150
		  etac thin_rl i,
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   151
		  thin_leading_eqs_tac bnd (n-k) i]
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   152
	end
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   153
	handle THM _ => no_tac | EQ_VAR => no_tac));
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   154
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   155
end;
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   156
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   157
val ssubst = standard (sym RS subst);
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   158
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   159
(*Old version of the tactic above -- slower but the only way
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   160
  to handle equalities containing Vars.*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   161
fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
      let val (_,_,Bi,_) = dest_state(state,i)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
	  val n = length(Logic.strip_assums_hyp Bi) - 1
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   164
	  val (k,symopt) = eq_var bnd false Bi
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   165
      in 
704
b71b6be59354 Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
lcp
parents: 680
diff changeset
   166
	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   167
		etac revcut_rl i,
704
b71b6be59354 Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
lcp
parents: 680
diff changeset
   168
		REPEAT_DETERM_N (n-k) (etac rev_mp i),
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   169
		etac (if symopt then ssubst else subst) i,
704
b71b6be59354 Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
lcp
parents: 680
diff changeset
   170
		REPEAT_DETERM_N n (rtac imp_intr i)]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
      end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
      handle THM _ => no_tac | EQ_VAR => no_tac));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
(*Substitutes for Free or Bound variables*)
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   175
val hyp_subst_tac = 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   176
    gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
(*Substitutes for Bound variables only -- this is always safe*)
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   179
val bound_hyp_subst_tac = 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   180
    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184