author  lcp 
Fri, 11 Nov 1994 10:42:55 +0100  
changeset 704  b71b6be59354 
parent 680  f9e24455bbd1 
child 1011  5c9654e2e3de 
permissions  rwrr 
0  1 
(* Title: Provers/hypsubst 
2 
ID: $Id$ 

646  3 
Author: Martin D Coen, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

6 
Martin Coen's tactic for substitution in the hypotheses 

7 
*) 

8 

9 
signature HYPSUBST_DATA = 

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  16 
end; 
17 

18 
signature HYPSUBST = 

19 
sig 

20 
val bound_hyp_subst_tac : int > tactic 

21 
val hyp_subst_tac : int > tactic 

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  25 
end; 
26 

27 
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 

28 
struct 

29 

30 
local open Data in 

31 

32 
exception EQ_VAR; 

33 

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

35 

36 
(*It's not safe to substitute for a constant; consider 0=1. 

37 
It's not safe to substitute for x=t[x] since x is not eliminated. 

646  38 
It's not safe to substitute for a Var; what if it appears in other goals? 
0  39 
It's not safe to substitute for a variable free in the premises, 
40 
but how could we check for this?*) 

41 
fun inspect_pair bnd (t,u) = 

42 
case (Pattern.eta_contract t, Pattern.eta_contract u) of 

43 
(Bound i, _) => if loose(i,u) then raise Match 

680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

44 
else sym (*eliminates t*) 
0  45 
 (_, Bound i) => if loose(i,t) then raise Match 
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

46 
else asm_rl (*eliminates u*) 
0  47 
 (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

48 
else sym (*eliminates t*) 
0  49 
 (_, 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

50 
else asm_rl (*eliminates u*) 
0  51 
 _ => raise Match; 
52 

680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

53 
(*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

54 
assumption. Returns the number of intervening assumptions, paried with 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

55 
the rule asm_rl (resp. sym). *) 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

56 
fun eq_var bnd = 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

57 
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

58 
 eq_var_aux k (Const("==>",_) $ A $ B) = 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

59 
((k, inspect_pair bnd (dest_eq A)) 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

60 
(*Exception Match comes from inspect_pair or dest_eq*) 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

61 
handle Match => eq_var_aux (k+1) B) 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

62 
 eq_var_aux k _ = raise EQ_VAR 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

63 
in eq_var_aux 0 end; 
0  64 

65 
(*Select a suitable equality assumption and substitute throughout the subgoal 

66 
Replaces only Bound variables if bnd is true*) 

67 
fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => 

68 
let val (_,_,Bi,_) = dest_state(state,i) 

69 
val n = length(Logic.strip_assums_hyp Bi)  1 

680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

70 
val (k,symopt) = eq_var bnd Bi 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

71 
in 
704
b71b6be59354
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
lcp
parents:
680
diff
changeset

72 
EVERY [REPEAT_DETERM_N k (etac rev_mp i), 
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

73 
etac revcut_rl i, 
704
b71b6be59354
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
lcp
parents:
680
diff
changeset

74 
REPEAT_DETERM_N (nk) (etac rev_mp i), 
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

75 
etac (symopt RS subst) i, 
704
b71b6be59354
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
lcp
parents:
680
diff
changeset

76 
REPEAT_DETERM_N n (rtac imp_intr i)] 
0  77 
end 
78 
handle THM _ => no_tac  EQ_VAR => no_tac)); 

79 

80 
(*Substitutes for Free or Bound variables*) 

81 
val hyp_subst_tac = gen_hyp_subst_tac false; 

82 

83 
(*Substitutes for Bound variables only  this is always safe*) 

84 
val bound_hyp_subst_tac = gen_hyp_subst_tac true; 

85 

86 
end 

87 
end; 

88 