src/HOL/TLA/hypsubst.ML

uses BasisLibrary for Int.min

(*  Title: 	~/projects/isabelle/TLA/hypsubst.ML
    Authors: 	Martin D Coen, Tobias Nipkow and Lawrence C Paulson
    Copyright   1995  University of Cambridge

Tactic to substitute using the assumption x=t in the rest of the subgoal,
and to delete that assumption.  Original version due to Martin Coen.

This version uses the simplifier, and requires it to be already present.

Local changes for TLA (Stephan Merz):
  Simplify equations like f(x) = g(y) if x,y are bound variables.
  This is useful for TLA if f and g are state variables. f and g may be
  free or bound variables, or even constants. (This may be unsafe, but
  we do some type checking to restrict this to state variables!)



Test data:

Goal "[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
Goal "[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
Goal "[| ?x=y; P(?x) |] ==> y = a";
Goal "[| ?x=y; P(?x) |] ==> y = a";

by (hyp_subst_tac 1);
by (bound_hyp_subst_tac 1);

Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
Goal "P(a) --> (EX y. a=y --> P(f(a)))";
*)

(*** Signatures unchanged (but renamed) from the original hypsubst.ML ***)

signature ACTHYPSUBST_DATA =
  sig
  structure Simplifier : SIMPLIFIER
  val dest_eq	       : term -> term*term
  val eq_reflection    : thm		   (* a=b ==> a==b *)
  val imp_intr	       : thm		   (* (P ==> Q) ==> P-->Q *)
  val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
  val subst	       : thm		   (* [| a=b;  P(a) |] ==> P(b) *)
  val sym	       : thm		   (* a=b ==> b=a *)
  end;


signature ACTHYPSUBST =
  sig
  val action_bound_hyp_subst_tac    : int -> tactic
  val action_hyp_subst_tac          : int -> tactic
    (*exported purely for debugging purposes*)
  val gen_hyp_subst_tac      : bool -> int -> tactic
  val vars_gen_hyp_subst_tac : bool -> int -> tactic
  val eq_var                 : bool -> bool -> term -> int * bool
  val inspect_pair           : bool -> bool -> term * term -> bool
  val mk_eqs                 : thm -> thm list
  val thin_leading_eqs_tac   : bool -> int -> int -> tactic
  end;


functor ActHypsubstFun(Data: ACTHYPSUBST_DATA): ACTHYPSUBST = 
struct

fun STATE tacfun st = tacfun st st;


local open Data 
           BasisLibrary  (*for Int, List, ...*)
in

exception EQ_VAR;

fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);

local val odot = ord"."
in
(*Simplifier turns Bound variables to dotted Free variables: 
  change it back (any Bound variable will do)
*)
fun contract t =
    case Pattern.eta_contract t of
	Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T)
      | Free at $ Free(b,T) => Free at $
                               (if ord b = odot then Bound 0 else Free(b,T))
      | t'        => t'
end;

fun has_vars t = maxidx_of_term t <> ~1;

(* Added for TLA version.
   Is type ty the type of a state variable? Only then do we substitute
   in applications. This function either returns true or raises Match.
*)
fun is_stvar (Type("fun", Type("Stfun.state",[])::_)) = true;


(*If novars then we forbid Vars in the equality.
  If bnd then we only look for Bound (or dotted Free) variables to eliminate. 
  When can we safely delete the equality?
    Not if it equates two constants; consider 0=1.
    Not if it resembles x=t[x], since substitution does not eliminate x.
    Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
    Not if it involves a variable free in the premises, 
        but we can't check for this -- hence bnd and bound_hyp_subst_tac
  Prefer to eliminate Bound variables if possible.
  Result:  true = use as is,  false = reorient first *)
fun inspect_pair bnd novars (t,u) =
  case (contract t, contract u) of
       (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
		       then raise Match 
		       else true		(*eliminates t*)
     | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t  
		       then raise Match 
		       else false		(*eliminates u*)
     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse  
		          novars andalso has_vars u  
		       then raise Match 
		       else true		(*eliminates t*)
     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse  
		          novars andalso has_vars t 
		       then raise Match 
		       else false		(*eliminates u*)
     | (Free(_,ty) $ (Bound _), _) => 
                       if bnd orelse 
                          novars andalso has_vars u
                       then raise Match 
                       else is_stvar(ty)        (* changed for TLA *)
     | (_, Free(_,ty) $ (Bound _)) => 
                       if bnd orelse 
                          novars andalso has_vars t
                       then raise Match 
                       else not(is_stvar(ty))   (* changed for TLA *)
     | ((Bound _) $ (Bound _), _) => (* can't check for types here *)
                       if bnd orelse 
                          novars andalso has_vars u
                       then raise Match 
                       else true
     | (_, (Bound _) $ (Bound _)) => (* can't check for types here *)
                       if bnd orelse 
                          novars andalso has_vars t
                       then raise Match 
                       else false
     | (Const(_,ty) $ (Bound _), _) => 
                       if bnd orelse 
                          novars andalso has_vars u
                       then raise Match 
                       else is_stvar(ty)        (* changed for TLA *)
     | (_, Const(_,ty) $ (Bound _)) => 
                       if bnd orelse
                          novars andalso has_vars t
                       then raise Match 
                       else not(is_stvar(ty))   (* changed for TLA *)
     | _ => raise Match;

(*Locates a substitutable variable on the left (resp. right) of an equality
   assumption.  Returns the number of intervening assumptions. *)
fun eq_var bnd novars =
  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
	| eq_var_aux k (Const("==>",_) $ A $ B) = 
	      ((k, inspect_pair bnd novars (dest_eq A))
		      (*Exception comes from inspect_pair or dest_eq*)
	       handle Match => eq_var_aux (k+1) B)
	| eq_var_aux k _ = raise EQ_VAR
  in  eq_var_aux 0  end;

(*We do not try to delete ALL equality assumptions at once.  But
  it is easy to handle several consecutive equality assumptions in a row.
  Note that we have to inspect the proof state after doing the rewriting,
  since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality
  must NOT be deleted.  Tactic must rotate or delete m assumptions.
*)
fun thin_leading_eqs_tac bnd m i = STATE(fn state =>
    let fun count []      = 0
	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);  
			      1 + count Bs)
                             handle Match => 0)
	val (_,_,Bi,_) = dest_state(state,i)
        val j = Int.min (m, count (Logic.strip_assums_hyp Bi))
    in  REPEAT_DETERM_N j     (etac thin_rl i)   THEN
        REPEAT_DETERM_N (m-j) (etac revcut_rl i)
    end);

(*For the simpset.  Adds ALL suitable equalities, even if not first!
  No vars are allowed here, as simpsets are built from meta-assumptions*)
fun mk_eqs th = 
    [ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th)))
      then th RS Data.eq_reflection
      else symmetric(th RS Data.eq_reflection) (*reorient*) ] 
    handle Match => [];  (*Exception comes from inspect_pair or dest_eq*)

local open Simplifier 
in

  val hyp_subst_ss = empty_ss setmksimps mk_eqs

  (*Select a suitable equality assumption and substitute throughout the subgoal
    Replaces only Bound variables if bnd is true*)
  fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
	let val (_,_,Bi,_) = dest_state(state,i)
	    val n = length(Logic.strip_assums_hyp Bi) - 1
	    val (k,_) = eq_var bnd true Bi
	in 
	   EVERY [REPEAT_DETERM_N k (etac revcut_rl i),
		  asm_full_simp_tac hyp_subst_ss i,
		  etac thin_rl i,
		  thin_leading_eqs_tac bnd (n-k) i]
	end
	handle THM _ => no_tac | EQ_VAR => no_tac));

end;

val ssubst = standard (sym RS subst);

(*Old version of the tactic above -- slower but the only way
  to handle equalities containing Vars.*)
fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
      let val (_,_,Bi,_) = dest_state(state,i)
	  val n = length(Logic.strip_assums_hyp Bi) - 1
	  val (k,symopt) = eq_var bnd false Bi
      in 
	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
		etac revcut_rl i,
		REPEAT_DETERM_N (n-k) (etac rev_mp i),
		etac (if symopt then ssubst else subst) i,
		REPEAT_DETERM_N n (rtac imp_intr i)]
      end
      handle THM _ => no_tac | EQ_VAR => no_tac));

(*Substitutes for Free or Bound variables*)
val action_hyp_subst_tac = 
    (* gen_hyp_subst_tac false ORELSE' *) vars_gen_hyp_subst_tac false;

(*Substitutes for Bound variables only -- this is always safe*)
val action_bound_hyp_subst_tac = 
    (* gen_hyp_subst_tac true ORELSE' *) vars_gen_hyp_subst_tac true;

end
end;