author | lcp |
Fri, 11 Nov 1994 10:42:55 +0100 | |
changeset 704 | b71b6be59354 |
parent 680 | f9e24455bbd1 |
child 1011 | 5c9654e2e3de |
permissions | -rw-r--r-- |
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 (n-k) (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 |