src/Provers/hypsubst.ML
author nipkow
Fri, 09 Oct 1998 14:19:13 +0200
changeset 5633 fb7fa1b154c4
parent 4466 305390f23734
child 9532 36b9bc6eb454
permissions -rw-r--r--
Added a few breaks in error text.
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
4223
f60e3d2c81d3 added thin_refl to hyp_subst_tac
oheimb
parents: 4179
diff changeset
     6
Tactic to substitute using (at least) the assumption x=t in the rest of the 
f60e3d2c81d3 added thin_refl to hyp_subst_tac
oheimb
parents: 4179
diff changeset
     7
subgoal, and to delete (at least) that assumption. 
f60e3d2c81d3 added thin_refl to hyp_subst_tac
oheimb
parents: 4179
diff changeset
     8
Original version due to Martin Coen.
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
     9
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    10
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
    11
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    12
Test data:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
1011
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); 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
    15
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
    16
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
    17
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
    18
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    19
by (hyp_subst_tac 1);
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    20
by (bound_hyp_subst_tac 1);
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    21
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    22
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
    23
goal thy "P(a) --> (EX y. a=y --> P(f(a)))";
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    24
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    25
goal thy "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    26
\                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    27
by (blast_hyp_subst_tac (ref true) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
signature HYPSUBST_DATA =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  sig
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    32
  structure Simplifier : SIMPLIFIER
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    33
  val dest_Trueprop    : term -> term
4179
cc4b6791d5dc hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents: 3537
diff changeset
    34
  val dest_eq	       : term -> term*term*typ
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    35
  val dest_imp	       : term -> term*term
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    36
  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
    37
  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
    38
  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
    39
  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
    40
  val sym	       : thm		   (* a=b ==> b=a *)
4223
f60e3d2c81d3 added thin_refl to hyp_subst_tac
oheimb
parents: 4179
diff changeset
    41
  val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    42
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    44
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
signature HYPSUBST =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  sig
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    47
  val bound_hyp_subst_tac    : int -> tactic
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    48
  val hyp_subst_tac          : int -> tactic
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
    49
  val blast_hyp_subst_tac    : bool ref -> int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
    (*exported purely for debugging purposes*)
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    51
  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
    52
  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
    53
  val eq_var                 : bool -> bool -> term -> int * bool
4179
cc4b6791d5dc hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents: 3537
diff changeset
    54
  val inspect_pair           : bool -> bool -> term * term * typ -> bool
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    55
  val mk_eqs                 : thm -> thm list
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    56
  val thin_leading_eqs_tac   : bool -> int -> int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
2722
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
    59
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
    60
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
exception EQ_VAR;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
2174
0829b7b632c5 Removed a call to polymorphic mem
paulson
parents: 2143
diff changeset
    66
fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    68
local val odot = ord"."
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    69
in
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    70
(*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
    71
  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
    72
*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    73
fun contract t =
2722
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
    74
    case Pattern.eta_contract_atom t of
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    75
	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
    76
      | t'        => t'
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    77
end;
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    78
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    79
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
    80
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    81
(*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
    82
  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
    83
  When can we safely delete the equality?
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    84
    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
    85
    Not if it resembles x=t[x], since substitution does not eliminate x.
4299
22596d62ce0b updated comment
paulson
parents: 4223
diff changeset
    86
    Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    87
    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
    88
        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
    89
  Prefer to eliminate Bound variables if possible.
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    90
  Result:  true = use as is,  false = reorient first *)
4179
cc4b6791d5dc hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents: 3537
diff changeset
    91
fun inspect_pair bnd novars (t,u,T) =
cc4b6791d5dc hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents: 3537
diff changeset
    92
  if novars andalso maxidx_of_typ T <> ~1 
cc4b6791d5dc hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents: 3537
diff changeset
    93
  then raise Match   (*variables in the type!*)
cc4b6791d5dc hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents: 3537
diff changeset
    94
  else
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    95
  case (contract t, contract u) of
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    96
       (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
    97
		       then raise Match 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    98
		       else true		(*eliminates t*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
    99
     | (_, 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
   100
		       then raise Match 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   101
		       else false		(*eliminates u*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   102
     | (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
   103
		          novars andalso has_vars u  
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   104
		       then raise Match 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   105
		       else true		(*eliminates t*)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   106
     | (_, 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
   107
		          novars andalso has_vars t 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   108
		       then raise Match 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   109
		       else false		(*eliminates u*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
     | _ => raise Match;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   112
(*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
   113
   assumption.  Returns the number of intervening assumptions. *)
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   114
fun eq_var bnd novars =
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   115
  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
   116
	| eq_var_aux k (Const("==>",_) $ A $ B) = 
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   117
	      ((k, inspect_pair bnd novars 
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   118
		    (Data.dest_eq (Data.dest_Trueprop A)))
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   119
		      (*Exception comes from inspect_pair or dest_eq*)
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   120
	       handle _ => eq_var_aux (k+1) B)
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   121
	| eq_var_aux k _ = raise EQ_VAR
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   122
  in  eq_var_aux 0  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   124
(*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
   125
  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
   126
  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
   127
  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
   128
  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
   129
*)
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   130
fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   131
    let fun count []      = 0
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   132
	  | count (A::Bs) = ((inspect_pair bnd true 
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   133
			      (Data.dest_eq (Data.dest_Trueprop A));  
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   134
			      1 + count Bs)
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   135
                             handle _ => 0)
2143
093bbe6d333b Replaced min by Int.min
paulson
parents: 1011
diff changeset
   136
        val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
2722
3e07c20b967c Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents: 2174
diff changeset
   137
    in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   138
    end);
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   139
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   140
(*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
   141
  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
   142
fun mk_eqs th = 
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   143
    [ if inspect_pair false false (Data.dest_eq 
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   144
				   (Data.dest_Trueprop (#prop (rep_thm th))))
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   145
      then th RS Data.eq_reflection
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   146
      else symmetric(th RS Data.eq_reflection) (*reorient*) ] 
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   147
    handle _ => [];  (*Exception comes from inspect_pair or dest_eq*)
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   148
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   149
local open Simplifier 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   150
in
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   151
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   152
  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
   153
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   154
  (*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
   155
    Replaces only Bound variables if bnd is true*)
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   156
  fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   157
	let 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
   158
	    val (k,_) = eq_var bnd true Bi
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   159
	in 
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   160
	   DETERM (EVERY [rotate_tac k i,
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   161
			  asm_full_simp_tac hyp_subst_ss i,
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   162
			  etac thin_rl i,
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   163
			  thin_leading_eqs_tac bnd (n-k) i])
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   164
	end
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   165
	handle THM _ => no_tac | EQ_VAR => no_tac);
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   166
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   167
end;
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   168
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   169
val ssubst = standard (Data.sym RS Data.subst);
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   170
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   171
val imp_intr_tac = rtac Data.imp_intr;
1011
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   172
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   173
(*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
   174
  to handle equalities containing Vars.*)
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   175
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   176
      let 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
   177
	  val (k,symopt) = eq_var bnd false Bi
680
f9e24455bbd1 Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents: 646
diff changeset
   178
      in 
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   179
	 DETERM
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   180
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   181
		   rotate_tac 1 i,
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   182
		   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   183
		   etac (if symopt then ssubst else Data.subst) i,
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   184
		   REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
      end
3537
79ac9b475621 Removal of the tactical STATE
paulson
parents: 2750
diff changeset
   186
      handle THM _ => no_tac | EQ_VAR => no_tac);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
(*Substitutes for Free or Bound variables*)
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   189
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
4223
f60e3d2c81d3 added thin_refl to hyp_subst_tac
oheimb
parents: 4179
diff changeset
   190
        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
(*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
   193
val bound_hyp_subst_tac = 
5c9654e2e3de Recoded with help from Toby to use rewriting instead of the
lcp
parents: 704
diff changeset
   194
    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
4466
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   196
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   197
(** Version for Blast_tac.  Hyps that are affected by the substitution are 
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   198
    moved to the front.  Defect: even trivial changes are noticed, such as
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   199
    substitutions in the arguments of a function Var. **)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   200
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   201
(*final re-reversal of the changed assumptions*)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   202
fun reverse_n_tac 0 i = all_tac
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   203
  | reverse_n_tac 1 i = rotate_tac ~1 i
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   204
  | reverse_n_tac n i = 
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   205
      REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   206
      REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   207
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   208
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   209
fun all_imp_intr_tac hyps i = 
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   210
  let fun imptac (r, [])    st = reverse_n_tac r i st
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   211
	| imptac (r, hyp::hyps) st =
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   212
	   let val (hyp',_) = List.nth (prems_of st, i-1) |>
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   213
			      Logic.strip_assums_concl    |> 
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   214
			      Data.dest_Trueprop          |> Data.dest_imp
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   215
	       val (r',tac) = if Pattern.aeconv (hyp,hyp')
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   216
			      then (r, imp_intr_tac i THEN rotate_tac ~1 i)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   217
			      else (*leave affected hyps at end*)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   218
				   (r+1, imp_intr_tac i) 
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   219
	   in
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   220
	       case Seq.pull(tac st) of
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   221
		   None       => Seq.single(st)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   222
		 | Some(st',_) => imptac (r',hyps) st'
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   223
	   end handle _ => error "?? in blast_hyp_subst_tac"
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   224
  in  imptac (0, rev hyps)  end;
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   225
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   226
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   227
fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   228
      let val (k,symopt) = eq_var false false Bi
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   229
	  val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   230
          (*omit selected equality, returning other hyps*)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   231
	  val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   232
	  val n = length hyps
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   233
      in 
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   234
	 if !trace then writeln "Substituting an equality" else ();
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   235
	 DETERM
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   236
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   237
		   rotate_tac 1 i,
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   238
		   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   239
		   etac (if symopt then ssubst else Data.subst) i,
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   240
		   all_imp_intr_tac hyps i])
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   241
      end
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   242
      handle THM _ => no_tac | EQ_VAR => no_tac);
305390f23734 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents: 4299
diff changeset
   243
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245