src/Provers/hypsubst.ML
author paulson
Tue Dec 23 11:39:03 1997 +0100 (1997-12-23 ago)
changeset 4466 305390f23734
parent 4299 22596d62ce0b
child 9532 36b9bc6eb454
permissions -rw-r--r--
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
clasohm@0
     1
(*  Title: 	Provers/hypsubst
clasohm@0
     2
    ID:         $Id$
lcp@1011
     3
    Authors: 	Martin D Coen, Tobias Nipkow and Lawrence C Paulson
lcp@1011
     4
    Copyright   1995  University of Cambridge
lcp@1011
     5
oheimb@4223
     6
Tactic to substitute using (at least) the assumption x=t in the rest of the 
oheimb@4223
     7
subgoal, and to delete (at least) that assumption. 
oheimb@4223
     8
Original version due to Martin Coen.
lcp@1011
     9
lcp@1011
    10
This version uses the simplifier, and requires it to be already present.
lcp@1011
    11
lcp@1011
    12
Test data:
clasohm@0
    13
lcp@1011
    14
goal thy "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
lcp@1011
    15
goal thy "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
lcp@1011
    16
goal thy "!!y. [| ?x=y; P(?x) |] ==> y = a";
lcp@1011
    17
goal thy "!!z. [| ?x=y; P(?x) |] ==> y = a";
lcp@1011
    18
lcp@1011
    19
by (hyp_subst_tac 1);
lcp@1011
    20
by (bound_hyp_subst_tac 1);
lcp@1011
    21
lcp@1011
    22
Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
lcp@1011
    23
goal thy "P(a) --> (EX y. a=y --> P(f(a)))";
paulson@4466
    24
paulson@4466
    25
goal thy "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
paulson@4466
    26
\                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
paulson@4466
    27
by (blast_hyp_subst_tac (ref true) 1);
clasohm@0
    28
*)
clasohm@0
    29
clasohm@0
    30
signature HYPSUBST_DATA =
clasohm@0
    31
  sig
lcp@1011
    32
  structure Simplifier : SIMPLIFIER
paulson@4466
    33
  val dest_Trueprop    : term -> term
paulson@4179
    34
  val dest_eq	       : term -> term*term*typ
paulson@4466
    35
  val dest_imp	       : term -> term*term
lcp@1011
    36
  val eq_reflection    : thm		   (* a=b ==> a==b *)
lcp@1011
    37
  val imp_intr	       : thm		   (* (P ==> Q) ==> P-->Q *)
lcp@1011
    38
  val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
lcp@1011
    39
  val subst	       : thm		   (* [| a=b;  P(a) |] ==> P(b) *)
lcp@1011
    40
  val sym	       : thm		   (* a=b ==> b=a *)
oheimb@4223
    41
  val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
paulson@4466
    42
  end;
clasohm@0
    43
lcp@1011
    44
clasohm@0
    45
signature HYPSUBST =
clasohm@0
    46
  sig
lcp@1011
    47
  val bound_hyp_subst_tac    : int -> tactic
lcp@1011
    48
  val hyp_subst_tac          : int -> tactic
paulson@4466
    49
  val blast_hyp_subst_tac    : bool ref -> int -> tactic
clasohm@0
    50
    (*exported purely for debugging purposes*)
lcp@1011
    51
  val gen_hyp_subst_tac      : bool -> int -> tactic
lcp@1011
    52
  val vars_gen_hyp_subst_tac : bool -> int -> tactic
lcp@1011
    53
  val eq_var                 : bool -> bool -> term -> int * bool
paulson@4179
    54
  val inspect_pair           : bool -> bool -> term * term * typ -> bool
lcp@1011
    55
  val mk_eqs                 : thm -> thm list
lcp@1011
    56
  val thin_leading_eqs_tac   : bool -> int -> int -> tactic
clasohm@0
    57
  end;
clasohm@0
    58
paulson@2722
    59
paulson@2722
    60
clasohm@0
    61
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
clasohm@0
    62
struct
clasohm@0
    63
clasohm@0
    64
exception EQ_VAR;
clasohm@0
    65
paulson@2174
    66
fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
clasohm@0
    67
lcp@1011
    68
local val odot = ord"."
lcp@1011
    69
in
lcp@1011
    70
(*Simplifier turns Bound variables to dotted Free variables: 
lcp@1011
    71
  change it back (any Bound variable will do)
lcp@1011
    72
*)
lcp@1011
    73
fun contract t =
paulson@2722
    74
    case Pattern.eta_contract_atom t of
lcp@1011
    75
	Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T)
lcp@1011
    76
      | t'        => t'
lcp@1011
    77
end;
lcp@1011
    78
lcp@1011
    79
fun has_vars t = maxidx_of_term t <> ~1;
lcp@1011
    80
lcp@1011
    81
(*If novars then we forbid Vars in the equality.
lcp@1011
    82
  If bnd then we only look for Bound (or dotted Free) variables to eliminate. 
lcp@1011
    83
  When can we safely delete the equality?
lcp@1011
    84
    Not if it equates two constants; consider 0=1.
lcp@1011
    85
    Not if it resembles x=t[x], since substitution does not eliminate x.
paulson@4299
    86
    Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
lcp@1011
    87
    Not if it involves a variable free in the premises, 
lcp@1011
    88
        but we can't check for this -- hence bnd and bound_hyp_subst_tac
lcp@1011
    89
  Prefer to eliminate Bound variables if possible.
lcp@1011
    90
  Result:  true = use as is,  false = reorient first *)
paulson@4179
    91
fun inspect_pair bnd novars (t,u,T) =
paulson@4179
    92
  if novars andalso maxidx_of_typ T <> ~1 
paulson@4179
    93
  then raise Match   (*variables in the type!*)
paulson@4179
    94
  else
lcp@1011
    95
  case (contract t, contract u) of
lcp@1011
    96
       (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
lcp@1011
    97
		       then raise Match 
lcp@1011
    98
		       else true		(*eliminates t*)
lcp@1011
    99
     | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t  
lcp@1011
   100
		       then raise Match 
lcp@1011
   101
		       else false		(*eliminates u*)
lcp@1011
   102
     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse  
lcp@1011
   103
		          novars andalso has_vars u  
lcp@1011
   104
		       then raise Match 
lcp@1011
   105
		       else true		(*eliminates t*)
lcp@1011
   106
     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse  
lcp@1011
   107
		          novars andalso has_vars t 
lcp@1011
   108
		       then raise Match 
lcp@1011
   109
		       else false		(*eliminates u*)
clasohm@0
   110
     | _ => raise Match;
clasohm@0
   111
lcp@680
   112
(*Locates a substitutable variable on the left (resp. right) of an equality
lcp@1011
   113
   assumption.  Returns the number of intervening assumptions. *)
lcp@1011
   114
fun eq_var bnd novars =
lcp@680
   115
  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
lcp@680
   116
	| eq_var_aux k (Const("==>",_) $ A $ B) = 
paulson@4466
   117
	      ((k, inspect_pair bnd novars 
paulson@4466
   118
		    (Data.dest_eq (Data.dest_Trueprop A)))
lcp@1011
   119
		      (*Exception comes from inspect_pair or dest_eq*)
paulson@4466
   120
	       handle _ => eq_var_aux (k+1) B)
lcp@680
   121
	| eq_var_aux k _ = raise EQ_VAR
lcp@680
   122
  in  eq_var_aux 0  end;
clasohm@0
   123
lcp@1011
   124
(*We do not try to delete ALL equality assumptions at once.  But
lcp@1011
   125
  it is easy to handle several consecutive equality assumptions in a row.
lcp@1011
   126
  Note that we have to inspect the proof state after doing the rewriting,
lcp@1011
   127
  since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality
lcp@1011
   128
  must NOT be deleted.  Tactic must rotate or delete m assumptions.
lcp@1011
   129
*)
paulson@3537
   130
fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>
lcp@1011
   131
    let fun count []      = 0
paulson@4466
   132
	  | count (A::Bs) = ((inspect_pair bnd true 
paulson@4466
   133
			      (Data.dest_eq (Data.dest_Trueprop A));  
lcp@1011
   134
			      1 + count Bs)
paulson@4466
   135
                             handle _ => 0)
paulson@2143
   136
        val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
paulson@2722
   137
    in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
lcp@1011
   138
    end);
lcp@1011
   139
lcp@1011
   140
(*For the simpset.  Adds ALL suitable equalities, even if not first!
lcp@1011
   141
  No vars are allowed here, as simpsets are built from meta-assumptions*)
lcp@1011
   142
fun mk_eqs th = 
paulson@4466
   143
    [ if inspect_pair false false (Data.dest_eq 
paulson@4466
   144
				   (Data.dest_Trueprop (#prop (rep_thm th))))
lcp@1011
   145
      then th RS Data.eq_reflection
lcp@1011
   146
      else symmetric(th RS Data.eq_reflection) (*reorient*) ] 
paulson@4466
   147
    handle _ => [];  (*Exception comes from inspect_pair or dest_eq*)
lcp@1011
   148
lcp@1011
   149
local open Simplifier 
lcp@1011
   150
in
lcp@1011
   151
lcp@1011
   152
  val hyp_subst_ss = empty_ss setmksimps mk_eqs
lcp@1011
   153
lcp@1011
   154
  (*Select a suitable equality assumption and substitute throughout the subgoal
lcp@1011
   155
    Replaces only Bound variables if bnd is true*)
paulson@3537
   156
  fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
paulson@3537
   157
	let val n = length(Logic.strip_assums_hyp Bi) - 1
lcp@1011
   158
	    val (k,_) = eq_var bnd true Bi
lcp@1011
   159
	in 
paulson@3537
   160
	   DETERM (EVERY [rotate_tac k i,
paulson@3537
   161
			  asm_full_simp_tac hyp_subst_ss i,
paulson@3537
   162
			  etac thin_rl i,
paulson@3537
   163
			  thin_leading_eqs_tac bnd (n-k) i])
lcp@1011
   164
	end
paulson@3537
   165
	handle THM _ => no_tac | EQ_VAR => no_tac);
lcp@1011
   166
lcp@1011
   167
end;
lcp@1011
   168
paulson@4466
   169
val ssubst = standard (Data.sym RS Data.subst);
paulson@4466
   170
paulson@4466
   171
val imp_intr_tac = rtac Data.imp_intr;
lcp@1011
   172
lcp@1011
   173
(*Old version of the tactic above -- slower but the only way
lcp@1011
   174
  to handle equalities containing Vars.*)
paulson@3537
   175
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
paulson@3537
   176
      let val n = length(Logic.strip_assums_hyp Bi) - 1
lcp@1011
   177
	  val (k,symopt) = eq_var bnd false Bi
lcp@680
   178
      in 
paulson@3537
   179
	 DETERM
paulson@4466
   180
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
paulson@4466
   181
		   rotate_tac 1 i,
paulson@4466
   182
		   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
paulson@4466
   183
		   etac (if symopt then ssubst else Data.subst) i,
paulson@4466
   184
		   REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
clasohm@0
   185
      end
paulson@3537
   186
      handle THM _ => no_tac | EQ_VAR => no_tac);
clasohm@0
   187
clasohm@0
   188
(*Substitutes for Free or Bound variables*)
paulson@4466
   189
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
oheimb@4223
   190
        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
clasohm@0
   191
clasohm@0
   192
(*Substitutes for Bound variables only -- this is always safe*)
lcp@1011
   193
val bound_hyp_subst_tac = 
lcp@1011
   194
    gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
clasohm@0
   195
paulson@4466
   196
paulson@4466
   197
(** Version for Blast_tac.  Hyps that are affected by the substitution are 
paulson@4466
   198
    moved to the front.  Defect: even trivial changes are noticed, such as
paulson@4466
   199
    substitutions in the arguments of a function Var. **)
paulson@4466
   200
paulson@4466
   201
(*final re-reversal of the changed assumptions*)
paulson@4466
   202
fun reverse_n_tac 0 i = all_tac
paulson@4466
   203
  | reverse_n_tac 1 i = rotate_tac ~1 i
paulson@4466
   204
  | reverse_n_tac n i = 
paulson@4466
   205
      REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
paulson@4466
   206
      REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
paulson@4466
   207
paulson@4466
   208
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
paulson@4466
   209
fun all_imp_intr_tac hyps i = 
paulson@4466
   210
  let fun imptac (r, [])    st = reverse_n_tac r i st
paulson@4466
   211
	| imptac (r, hyp::hyps) st =
paulson@4466
   212
	   let val (hyp',_) = List.nth (prems_of st, i-1) |>
paulson@4466
   213
			      Logic.strip_assums_concl    |> 
paulson@4466
   214
			      Data.dest_Trueprop          |> Data.dest_imp
paulson@4466
   215
	       val (r',tac) = if Pattern.aeconv (hyp,hyp')
paulson@4466
   216
			      then (r, imp_intr_tac i THEN rotate_tac ~1 i)
paulson@4466
   217
			      else (*leave affected hyps at end*)
paulson@4466
   218
				   (r+1, imp_intr_tac i) 
paulson@4466
   219
	   in
paulson@4466
   220
	       case Seq.pull(tac st) of
paulson@4466
   221
		   None       => Seq.single(st)
paulson@4466
   222
		 | Some(st',_) => imptac (r',hyps) st'
paulson@4466
   223
	   end handle _ => error "?? in blast_hyp_subst_tac"
paulson@4466
   224
  in  imptac (0, rev hyps)  end;
paulson@4466
   225
paulson@4466
   226
paulson@4466
   227
fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
paulson@4466
   228
      let val (k,symopt) = eq_var false false Bi
paulson@4466
   229
	  val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
paulson@4466
   230
          (*omit selected equality, returning other hyps*)
paulson@4466
   231
	  val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
paulson@4466
   232
	  val n = length hyps
paulson@4466
   233
      in 
paulson@4466
   234
	 if !trace then writeln "Substituting an equality" else ();
paulson@4466
   235
	 DETERM
paulson@4466
   236
           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
paulson@4466
   237
		   rotate_tac 1 i,
paulson@4466
   238
		   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
paulson@4466
   239
		   etac (if symopt then ssubst else Data.subst) i,
paulson@4466
   240
		   all_imp_intr_tac hyps i])
paulson@4466
   241
      end
paulson@4466
   242
      handle THM _ => no_tac | EQ_VAR => no_tac);
paulson@4466
   243
clasohm@0
   244
end;
clasohm@0
   245