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