author  lcp 
Wed, 02 Nov 1994 12:44:03 +0100  
changeset 680  f9e24455bbd1 
parent 646  7928c9760667 
child 704  b71b6be59354 
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 
fun REPEATN 0 tac = all_tac 

33 
 REPEATN n tac = Tactic(fn state => 

34 
tapply(tac THEN REPEATN (n1) tac, state)); 

35 

36 
exception EQ_VAR; 

37 

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

39 

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

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

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

45 
fun inspect_pair bnd (t,u) = 

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

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  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  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  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  55 
 _ => raise Match; 
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  68 

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

70 
Replaces only Bound variables if bnd is true*) 

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

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

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 (nk) (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  81 
end 
82 
handle THM _ => no_tac  EQ_VAR => no_tac)); 

83 

84 
(*Substitutes for Free or Bound variables*) 

85 
val hyp_subst_tac = gen_hyp_subst_tac false; 

86 

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

88 
val bound_hyp_subst_tac = gen_hyp_subst_tac true; 

89 

90 
end 

91 
end; 

92 