src/Provers/hypsubst.ML
author lcp
Wed Oct 19 09:48:13 1994 +0100 (1994-10-19 ago)
changeset 646 7928c9760667
parent 231 cb6a24451544
child 680 f9e24455bbd1
permissions -rw-r--r--
new comments explaining abandoned change
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
clasohm@0
    11
  val dest_eq: term -> term*term
clasohm@0
    12
  val imp_intr: thm	(* (P ==> Q) ==> P-->Q *)
clasohm@0
    13
  val rev_cut_eq: thm	(* [| a=b;  a=b ==> R |] ==> R *)
clasohm@0
    14
  val rev_mp: thm	(* [| P;  P-->Q |] ==> Q *)
clasohm@0
    15
  val subst: thm	(* [| a=b;  P(a) |] ==> P(b) *)
clasohm@0
    16
  val sym: thm		(* a=b ==> b=a *)
clasohm@0
    17
  end;
clasohm@0
    18
clasohm@0
    19
signature HYPSUBST =
clasohm@0
    20
  sig
clasohm@0
    21
  val bound_hyp_subst_tac : int -> tactic
clasohm@0
    22
  val hyp_subst_tac       : int -> tactic
clasohm@0
    23
    (*exported purely for debugging purposes*)
clasohm@0
    24
  val eq_var              : bool -> term -> term * thm
clasohm@0
    25
  val inspect_pair        : bool -> term * term -> term * thm
clasohm@0
    26
  val liftvar             : int -> typ list -> term
clasohm@0
    27
  end;
clasohm@0
    28
clasohm@0
    29
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
clasohm@0
    30
struct
clasohm@0
    31
clasohm@0
    32
local open Data in
clasohm@0
    33
clasohm@0
    34
fun REPEATN 0 tac = all_tac
clasohm@0
    35
  | REPEATN n tac = Tactic(fn state =>
clasohm@0
    36
                           tapply(tac THEN REPEATN (n-1) tac,  state));
clasohm@0
    37
clasohm@0
    38
local
clasohm@0
    39
  val T = case #1 (types_sorts rev_cut_eq) ("a",0) of
clasohm@0
    40
	      Some T => T
clasohm@0
    41
   	    | None   => error"No such variable in rev_cut_eq"
clasohm@0
    42
in
clasohm@0
    43
  fun liftvar inc paramTs = Var(("a",inc), paramTs ---> incr_tvar inc T);
clasohm@0
    44
end;
clasohm@0
    45
clasohm@0
    46
exception EQ_VAR;
clasohm@0
    47
clasohm@0
    48
fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
clasohm@0
    49
clasohm@0
    50
(*It's not safe to substitute for a constant; consider 0=1.
clasohm@0
    51
  It's not safe to substitute for x=t[x] since x is not eliminated.
lcp@646
    52
  It's not safe to substitute for a Var; what if it appears in other goals?
clasohm@0
    53
  It's not safe to substitute for a variable free in the premises,
clasohm@0
    54
    but how could we check for this?*)
clasohm@0
    55
fun inspect_pair bnd (t,u) =
clasohm@0
    56
  case (Pattern.eta_contract t, Pattern.eta_contract u) of
clasohm@0
    57
       (Bound i, _) => if loose(i,u) then raise Match 
clasohm@0
    58
		       else (t, asm_rl)
clasohm@0
    59
     | (_, Bound i) => if loose(i,t) then raise Match 
clasohm@0
    60
		       else (u, sym)
clasohm@0
    61
     | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match 
clasohm@0
    62
		      else (t, asm_rl)
clasohm@0
    63
     | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match 
clasohm@0
    64
		      else (u, sym) 
clasohm@0
    65
     | _ => raise Match;
clasohm@0
    66
clasohm@0
    67
 (* Extracts the name of the variable on the left (resp. right) of an equality
clasohm@0
    68
   assumption.  Returns the rule asm_rl (resp. sym). *)
clasohm@0
    69
fun eq_var bnd (Const("all",_) $ Abs(_,_,t)) = eq_var bnd t
clasohm@0
    70
  | eq_var bnd (Const("==>",_) $ A $ B) = 
clasohm@0
    71
	(inspect_pair bnd (dest_eq A) 
clasohm@0
    72
	        (*Match comes from inspect_pair or dest_eq*)
clasohm@0
    73
	 handle Match => eq_var bnd B)
clasohm@0
    74
  | eq_var bnd _ = raise EQ_VAR;
clasohm@0
    75
clasohm@0
    76
(*Lift and instantiate a rule wrt the given state and subgoal number *)
clasohm@0
    77
fun lift_instpair (state, i, t, rule) =
clasohm@0
    78
  let val {maxidx,sign,...} = rep_thm state
clasohm@0
    79
      val (_, _, Bi, _) = dest_state(state,i)
clasohm@0
    80
      val params = Logic.strip_params Bi
clasohm@0
    81
      val var = liftvar (maxidx+1) (map #2 params)
clasohm@0
    82
      and u   = Unify.rlist_abs(rev params, t)
lcp@231
    83
      and cterm = cterm_of sign
clasohm@0
    84
  in cterm_instantiate [(cterm var, cterm u)] (lift_rule (state,i) rule)
clasohm@0
    85
  end;
clasohm@0
    86
clasohm@0
    87
fun eres_instpair_tac t rule i = STATE (fn state => 
clasohm@0
    88
	   compose_tac (true, lift_instpair (state, i, t, rule),
clasohm@0
    89
			length(prems_of rule)) i);
clasohm@0
    90
clasohm@0
    91
val ssubst = sym RS subst;
clasohm@0
    92
clasohm@0
    93
(*Select a suitable equality assumption and substitute throughout the subgoal
clasohm@0
    94
  Replaces only Bound variables if bnd is true*)
clasohm@0
    95
fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
clasohm@0
    96
      let val (_,_,Bi,_) = dest_state(state,i)
clasohm@0
    97
	  val n = length(Logic.strip_assums_hyp Bi) - 1
clasohm@0
    98
	  val (t,symopt) = eq_var bnd Bi
clasohm@0
    99
      in eres_instpair_tac t (symopt RS rev_cut_eq) i  THEN
clasohm@0
   100
         REPEATN n (etac rev_mp i) THEN
clasohm@0
   101
	 etac ssubst i THEN REPEATN n (rtac imp_intr i)
clasohm@0
   102
      end
clasohm@0
   103
      handle THM _ => no_tac | EQ_VAR => no_tac));
clasohm@0
   104
clasohm@0
   105
(*Substitutes for Free or Bound variables*)
clasohm@0
   106
val hyp_subst_tac = gen_hyp_subst_tac false;
clasohm@0
   107
clasohm@0
   108
(*Substitutes for Bound variables only -- this is always safe*)
clasohm@0
   109
val bound_hyp_subst_tac = gen_hyp_subst_tac true;
clasohm@0
   110
clasohm@0
   111
end
clasohm@0
   112
end;
clasohm@0
   113