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