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