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