author | paulson |
Wed, 26 Nov 1997 16:49:07 +0100 | |
changeset 4299 | 22596d62ce0b |
parent 4223 | f60e3d2c81d3 |
child 4466 | 305390f23734 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: Provers/hypsubst |
2 |
ID: $Id$ |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
3 |
Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
4 |
Copyright 1995 University of Cambridge |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
5 |
|
4223 | 6 |
Tactic to substitute using (at least) the assumption x=t in the rest of the |
7 |
subgoal, and to delete (at least) that assumption. |
|
8 |
Original version due to Martin Coen. |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
9 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
10 |
This version uses the simplifier, and requires it to be already present. |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
11 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
12 |
Test data: |
0 | 13 |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
14 |
goal thy "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)"; |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
15 |
goal thy "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)"; |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
16 |
goal thy "!!y. [| ?x=y; P(?x) |] ==> y = a"; |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
17 |
goal thy "!!z. [| ?x=y; P(?x) |] ==> y = a"; |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
18 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
19 |
by (hyp_subst_tac 1); |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
20 |
by (bound_hyp_subst_tac 1); |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
21 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
22 |
Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
23 |
goal thy "P(a) --> (EX y. a=y --> P(f(a)))"; |
0 | 24 |
*) |
25 |
||
26 |
signature HYPSUBST_DATA = |
|
27 |
sig |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
28 |
structure Simplifier : SIMPLIFIER |
4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset
|
29 |
val dest_eq : term -> term*term*typ |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
30 |
val eq_reflection : thm (* a=b ==> a==b *) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
31 |
val imp_intr : thm (* (P ==> Q) ==> P-->Q *) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
32 |
val rev_mp : thm (* [| P; P-->Q |] ==> Q *) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
33 |
val subst : thm (* [| a=b; P(a) |] ==> P(b) *) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
34 |
val sym : thm (* a=b ==> b=a *) |
4223 | 35 |
val thin_refl : thm (* [|x=x; PROP W|] ==> PROP W *) |
36 |
end; |
|
0 | 37 |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
38 |
|
0 | 39 |
signature HYPSUBST = |
40 |
sig |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
41 |
val bound_hyp_subst_tac : int -> tactic |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
42 |
val hyp_subst_tac : int -> tactic |
0 | 43 |
(*exported purely for debugging purposes*) |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
44 |
val gen_hyp_subst_tac : bool -> int -> tactic |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
45 |
val vars_gen_hyp_subst_tac : bool -> int -> tactic |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
46 |
val eq_var : bool -> bool -> term -> int * bool |
4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset
|
47 |
val inspect_pair : bool -> bool -> term * term * typ -> bool |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
48 |
val mk_eqs : thm -> thm list |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
49 |
val thin_leading_eqs_tac : bool -> int -> int -> tactic |
0 | 50 |
end; |
51 |
||
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset
|
52 |
|
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset
|
53 |
|
0 | 54 |
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = |
55 |
struct |
|
56 |
||
57 |
local open Data in |
|
58 |
||
59 |
exception EQ_VAR; |
|
60 |
||
2174 | 61 |
fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]); |
0 | 62 |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
63 |
local val odot = ord"." |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
64 |
in |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
65 |
(*Simplifier turns Bound variables to dotted Free variables: |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
66 |
change it back (any Bound variable will do) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
67 |
*) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
68 |
fun contract t = |
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset
|
69 |
case Pattern.eta_contract_atom t of |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
70 |
Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
71 |
| t' => t' |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
72 |
end; |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
73 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
74 |
fun has_vars t = maxidx_of_term t <> ~1; |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
75 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
76 |
(*If novars then we forbid Vars in the equality. |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
77 |
If bnd then we only look for Bound (or dotted Free) variables to eliminate. |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
78 |
When can we safely delete the equality? |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
79 |
Not if it equates two constants; consider 0=1. |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
80 |
Not if it resembles x=t[x], since substitution does not eliminate x. |
4299 | 81 |
Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
82 |
Not if it involves a variable free in the premises, |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
83 |
but we can't check for this -- hence bnd and bound_hyp_subst_tac |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
84 |
Prefer to eliminate Bound variables if possible. |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
85 |
Result: true = use as is, false = reorient first *) |
4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset
|
86 |
fun inspect_pair bnd novars (t,u,T) = |
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset
|
87 |
if novars andalso maxidx_of_typ T <> ~1 |
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset
|
88 |
then raise Match (*variables in the type!*) |
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset
|
89 |
else |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
90 |
case (contract t, contract u) of |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
91 |
(Bound i, _) => if loose(i,u) orelse novars andalso has_vars u |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
92 |
then raise Match |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
93 |
else true (*eliminates t*) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
94 |
| (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
95 |
then raise Match |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
96 |
else false (*eliminates u*) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
97 |
| (Free _, _) => if bnd orelse Logic.occs(t,u) orelse |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
98 |
novars andalso has_vars u |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
99 |
then raise Match |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
100 |
else true (*eliminates t*) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
101 |
| (_, Free _) => if bnd orelse Logic.occs(u,t) orelse |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
102 |
novars andalso has_vars t |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
103 |
then raise Match |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
104 |
else false (*eliminates u*) |
0 | 105 |
| _ => raise Match; |
106 |
||
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset
|
107 |
(*Locates a substitutable variable on the left (resp. right) of an equality |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
108 |
assumption. Returns the number of intervening assumptions. *) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
109 |
fun eq_var bnd novars = |
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset
|
110 |
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
|
111 |
| eq_var_aux k (Const("==>",_) $ A $ B) = |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
112 |
((k, inspect_pair bnd novars (dest_eq A)) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
113 |
(*Exception comes from inspect_pair or dest_eq*) |
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset
|
114 |
handle Match => eq_var_aux (k+1) B) |
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset
|
115 |
| eq_var_aux k _ = raise EQ_VAR |
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset
|
116 |
in eq_var_aux 0 end; |
0 | 117 |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
118 |
(*We do not try to delete ALL equality assumptions at once. But |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
119 |
it is easy to handle several consecutive equality assumptions in a row. |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
120 |
Note that we have to inspect the proof state after doing the rewriting, |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
121 |
since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
122 |
must NOT be deleted. Tactic must rotate or delete m assumptions. |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
123 |
*) |
3537 | 124 |
fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) => |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
125 |
let fun count [] = 0 |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
126 |
| count (A::Bs) = ((inspect_pair bnd true (dest_eq A); |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
127 |
1 + count Bs) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
128 |
handle Match => 0) |
2143 | 129 |
val j = Int.min(m, count (Logic.strip_assums_hyp Bi)) |
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset
|
130 |
in REPEAT_DETERM_N j (etac thin_rl i) THEN rotate_tac (m-j) i |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
131 |
end); |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
132 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
133 |
(*For the simpset. Adds ALL suitable equalities, even if not first! |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
134 |
No vars are allowed here, as simpsets are built from meta-assumptions*) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
135 |
fun mk_eqs th = |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
136 |
[ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th))) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
137 |
then th RS Data.eq_reflection |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
138 |
else symmetric(th RS Data.eq_reflection) (*reorient*) ] |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
139 |
handle Match => []; (*Exception comes from inspect_pair or dest_eq*) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
140 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
141 |
local open Simplifier |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
142 |
in |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
143 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
144 |
val hyp_subst_ss = empty_ss setmksimps mk_eqs |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
145 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
146 |
(*Select a suitable equality assumption and substitute throughout the subgoal |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
147 |
Replaces only Bound variables if bnd is true*) |
3537 | 148 |
fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => |
149 |
let val n = length(Logic.strip_assums_hyp Bi) - 1 |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
150 |
val (k,_) = eq_var bnd true Bi |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
151 |
in |
3537 | 152 |
DETERM (EVERY [rotate_tac k i, |
153 |
asm_full_simp_tac hyp_subst_ss i, |
|
154 |
etac thin_rl i, |
|
155 |
thin_leading_eqs_tac bnd (n-k) i]) |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
156 |
end |
3537 | 157 |
handle THM _ => no_tac | EQ_VAR => no_tac); |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
158 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
159 |
end; |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
160 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
161 |
val ssubst = standard (sym RS subst); |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
162 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
163 |
(*Old version of the tactic above -- slower but the only way |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
164 |
to handle equalities containing Vars.*) |
3537 | 165 |
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => |
166 |
let val n = length(Logic.strip_assums_hyp Bi) - 1 |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
167 |
val (k,symopt) = eq_var bnd false Bi |
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset
|
168 |
in |
3537 | 169 |
DETERM |
170 |
(EVERY [REPEAT_DETERM_N k (etac rev_mp i), |
|
171 |
etac revcut_rl i, |
|
172 |
REPEAT_DETERM_N (n-k) (etac rev_mp i), |
|
173 |
etac (if symopt then ssubst else subst) i, |
|
174 |
REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]) |
|
0 | 175 |
end |
3537 | 176 |
handle THM _ => no_tac | EQ_VAR => no_tac); |
0 | 177 |
|
178 |
(*Substitutes for Free or Bound variables*) |
|
4223 | 179 |
val hyp_subst_tac = FIRST' [ematch_tac [thin_refl], |
180 |
gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false]; |
|
0 | 181 |
|
182 |
(*Substitutes for Bound variables only -- this is always safe*) |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
183 |
val bound_hyp_subst_tac = |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
184 |
gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; |
0 | 185 |
|
186 |
end |
|
187 |
end; |
|
188 |