src/Provers/hypsubst.ML
author lcp
Fri Nov 11 10:42:55 1994 +0100 (1994-11-11 ago)
changeset 704 b71b6be59354
parent 680 f9e24455bbd1
child 1011 5c9654e2e3de
permissions -rw-r--r--
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
clasohm@0
     1
(*  Title: 	Provers/hypsubst
clasohm@0
     2
    ID:         $Id$
lcp@646
     3
    Author: 	Martin D Coen, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Martin Coen's tactic for substitution in the hypotheses
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
signature HYPSUBST_DATA =
clasohm@0
    10
  sig
lcp@680
    11
  val dest_eq	: term -> term*term
lcp@680
    12
  val imp_intr	: thm		(* (P ==> Q) ==> P-->Q *)
lcp@680
    13
  val rev_mp	: thm		(* [| P;  P-->Q |] ==> Q *)
lcp@680
    14
  val subst	: thm		(* [| a=b;  P(a) |] ==> P(b) *)
lcp@680
    15
  val sym	: thm		(* a=b ==> b=a *)
clasohm@0
    16
  end;
clasohm@0
    17
clasohm@0
    18
signature HYPSUBST =
clasohm@0
    19
  sig
clasohm@0
    20
  val bound_hyp_subst_tac : int -> tactic
clasohm@0
    21
  val hyp_subst_tac       : int -> tactic
clasohm@0
    22
    (*exported purely for debugging purposes*)
lcp@680
    23
  val eq_var              : bool -> term -> int * thm
lcp@680
    24
  val inspect_pair        : bool -> term * term -> thm
clasohm@0
    25
  end;
clasohm@0
    26
clasohm@0
    27
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
clasohm@0
    28
struct
clasohm@0
    29
clasohm@0
    30
local open Data in
clasohm@0
    31
clasohm@0
    32
exception EQ_VAR;
clasohm@0
    33
clasohm@0
    34
fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
clasohm@0
    35
clasohm@0
    36
(*It's not safe to substitute for a constant; consider 0=1.
clasohm@0
    37
  It's not safe to substitute for x=t[x] since x is not eliminated.
lcp@646
    38
  It's not safe to substitute for a Var; what if it appears in other goals?
clasohm@0
    39
  It's not safe to substitute for a variable free in the premises,
clasohm@0
    40
    but how could we check for this?*)
clasohm@0
    41
fun inspect_pair bnd (t,u) =
clasohm@0
    42
  case (Pattern.eta_contract t, Pattern.eta_contract u) of
clasohm@0
    43
       (Bound i, _) => if loose(i,u) then raise Match 
lcp@680
    44
		       else sym		(*eliminates t*)
clasohm@0
    45
     | (_, Bound i) => if loose(i,t) then raise Match 
lcp@680
    46
		       else asm_rl	(*eliminates u*)
clasohm@0
    47
     | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match 
lcp@680
    48
		      else sym		(*eliminates t*)
clasohm@0
    49
     | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match 
lcp@680
    50
		      else asm_rl	(*eliminates u*)
clasohm@0
    51
     | _ => raise Match;
clasohm@0
    52
lcp@680
    53
(*Locates a substitutable variable on the left (resp. right) of an equality
lcp@680
    54
   assumption.  Returns the number of intervening assumptions, paried with
lcp@680
    55
   the rule asm_rl (resp. sym). *)
lcp@680
    56
fun eq_var bnd =
lcp@680
    57
  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
lcp@680
    58
	| eq_var_aux k (Const("==>",_) $ A $ B) = 
lcp@680
    59
	      ((k, inspect_pair bnd (dest_eq A))
lcp@680
    60
		      (*Exception Match comes from inspect_pair or dest_eq*)
lcp@680
    61
	       handle Match => eq_var_aux (k+1) B)
lcp@680
    62
	| eq_var_aux k _ = raise EQ_VAR
lcp@680
    63
  in  eq_var_aux 0  end;
clasohm@0
    64
clasohm@0
    65
(*Select a suitable equality assumption and substitute throughout the subgoal
clasohm@0
    66
  Replaces only Bound variables if bnd is true*)
clasohm@0
    67
fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
clasohm@0
    68
      let val (_,_,Bi,_) = dest_state(state,i)
clasohm@0
    69
	  val n = length(Logic.strip_assums_hyp Bi) - 1
lcp@680
    70
	  val (k,symopt) = eq_var bnd Bi
lcp@680
    71
      in 
lcp@704
    72
	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
lcp@680
    73
		etac revcut_rl i,
lcp@704
    74
		REPEAT_DETERM_N (n-k) (etac rev_mp i),
lcp@680
    75
		etac (symopt RS subst) i,
lcp@704
    76
		REPEAT_DETERM_N n (rtac imp_intr i)]
clasohm@0
    77
      end
clasohm@0
    78
      handle THM _ => no_tac | EQ_VAR => no_tac));
clasohm@0
    79
clasohm@0
    80
(*Substitutes for Free or Bound variables*)
clasohm@0
    81
val hyp_subst_tac = gen_hyp_subst_tac false;
clasohm@0
    82
clasohm@0
    83
(*Substitutes for Bound variables only -- this is always safe*)
clasohm@0
    84
val bound_hyp_subst_tac = gen_hyp_subst_tac true;
clasohm@0
    85
clasohm@0
    86
end
clasohm@0
    87
end;
clasohm@0
    88