author | wenzelm |
Wed, 03 Feb 1999 17:28:02 +0100 | |
changeset 6208 | ea009b75b74e |
parent 4466 | 305390f23734 |
child 9532 | 36b9bc6eb454 |
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)))"; |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
24 |
|
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
25 |
goal thy "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \ |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
26 |
\ P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)"; |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
27 |
by (blast_hyp_subst_tac (ref true) 1); |
0 | 28 |
*) |
29 |
||
30 |
signature HYPSUBST_DATA = |
|
31 |
sig |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
32 |
structure Simplifier : SIMPLIFIER |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
33 |
val dest_Trueprop : term -> term |
4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset
|
34 |
val dest_eq : term -> term*term*typ |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
35 |
val dest_imp : term -> term*term |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
36 |
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
|
37 |
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
|
38 |
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
|
39 |
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
|
40 |
val sym : thm (* a=b ==> b=a *) |
4223 | 41 |
val thin_refl : thm (* [|x=x; PROP W|] ==> PROP W *) |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
42 |
end; |
0 | 43 |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
44 |
|
0 | 45 |
signature HYPSUBST = |
46 |
sig |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
47 |
val bound_hyp_subst_tac : int -> tactic |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
48 |
val hyp_subst_tac : int -> tactic |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
49 |
val blast_hyp_subst_tac : bool ref -> int -> tactic |
0 | 50 |
(*exported purely for debugging purposes*) |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
51 |
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
|
52 |
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
|
53 |
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
|
54 |
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
|
55 |
val mk_eqs : thm -> thm list |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
56 |
val thin_leading_eqs_tac : bool -> int -> int -> tactic |
0 | 57 |
end; |
58 |
||
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset
|
59 |
|
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset
|
60 |
|
0 | 61 |
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = |
62 |
struct |
|
63 |
||
64 |
exception EQ_VAR; |
|
65 |
||
2174 | 66 |
fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]); |
0 | 67 |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
68 |
local val odot = ord"." |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
69 |
in |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
70 |
(*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
|
71 |
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
|
72 |
*) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
73 |
fun contract t = |
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset
|
74 |
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
|
75 |
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
|
76 |
| t' => t' |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
77 |
end; |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
78 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
79 |
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
|
80 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
81 |
(*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
|
82 |
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
|
83 |
When can we safely delete the equality? |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
84 |
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
|
85 |
Not if it resembles x=t[x], since substitution does not eliminate x. |
4299 | 86 |
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
|
87 |
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
|
88 |
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
|
89 |
Prefer to eliminate Bound variables if possible. |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
90 |
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
|
91 |
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
|
92 |
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
|
93 |
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
|
94 |
else |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
95 |
case (contract t, contract u) of |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
96 |
(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
|
97 |
then raise Match |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
98 |
else true (*eliminates t*) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
99 |
| (_, 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
|
100 |
then raise Match |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
101 |
else false (*eliminates u*) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
102 |
| (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
|
103 |
novars andalso has_vars u |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
104 |
then raise Match |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
105 |
else true (*eliminates t*) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
106 |
| (_, 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
|
107 |
novars andalso has_vars t |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
108 |
then raise Match |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
109 |
else false (*eliminates u*) |
0 | 110 |
| _ => raise Match; |
111 |
||
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset
|
112 |
(*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
|
113 |
assumption. Returns the number of intervening assumptions. *) |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
114 |
fun eq_var bnd novars = |
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset
|
115 |
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
|
116 |
| eq_var_aux k (Const("==>",_) $ A $ B) = |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
117 |
((k, inspect_pair bnd novars |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
118 |
(Data.dest_eq (Data.dest_Trueprop A))) |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
119 |
(*Exception comes from inspect_pair or dest_eq*) |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
120 |
handle _ => eq_var_aux (k+1) B) |
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset
|
121 |
| eq_var_aux k _ = raise EQ_VAR |
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset
|
122 |
in eq_var_aux 0 end; |
0 | 123 |
|
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
124 |
(*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
|
125 |
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
|
126 |
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
|
127 |
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
|
128 |
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
|
129 |
*) |
3537 | 130 |
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
|
131 |
let fun count [] = 0 |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
132 |
| count (A::Bs) = ((inspect_pair bnd true |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
133 |
(Data.dest_eq (Data.dest_Trueprop A)); |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
134 |
1 + count Bs) |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
135 |
handle _ => 0) |
2143 | 136 |
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
|
137 |
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
|
138 |
end); |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
139 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
140 |
(*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
|
141 |
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
|
142 |
fun mk_eqs th = |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
143 |
[ if inspect_pair false false (Data.dest_eq |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
144 |
(Data.dest_Trueprop (#prop (rep_thm th)))) |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
145 |
then th RS Data.eq_reflection |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
146 |
else symmetric(th RS Data.eq_reflection) (*reorient*) ] |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
147 |
handle _ => []; (*Exception comes from inspect_pair or dest_eq*) |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
148 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
149 |
local open Simplifier |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
150 |
in |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
151 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
152 |
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
|
153 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
154 |
(*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
|
155 |
Replaces only Bound variables if bnd is true*) |
3537 | 156 |
fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => |
157 |
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
|
158 |
val (k,_) = eq_var bnd true Bi |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
159 |
in |
3537 | 160 |
DETERM (EVERY [rotate_tac k i, |
161 |
asm_full_simp_tac hyp_subst_ss i, |
|
162 |
etac thin_rl i, |
|
163 |
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
|
164 |
end |
3537 | 165 |
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
|
166 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
167 |
end; |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
168 |
|
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
169 |
val ssubst = standard (Data.sym RS Data.subst); |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
170 |
|
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
171 |
val imp_intr_tac = rtac Data.imp_intr; |
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
172 |
|
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
173 |
(*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
|
174 |
to handle equalities containing Vars.*) |
3537 | 175 |
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => |
176 |
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
|
177 |
val (k,symopt) = eq_var bnd false Bi |
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset
|
178 |
in |
3537 | 179 |
DETERM |
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
180 |
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
181 |
rotate_tac 1 i, |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
182 |
REPEAT_DETERM_N (n-k) (etac Data.rev_mp i), |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
183 |
etac (if symopt then ssubst else Data.subst) i, |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
184 |
REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)]) |
0 | 185 |
end |
3537 | 186 |
handle THM _ => no_tac | EQ_VAR => no_tac); |
0 | 187 |
|
188 |
(*Substitutes for Free or Bound variables*) |
|
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
189 |
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl], |
4223 | 190 |
gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false]; |
0 | 191 |
|
192 |
(*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
|
193 |
val bound_hyp_subst_tac = |
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset
|
194 |
gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; |
0 | 195 |
|
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
196 |
|
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
197 |
(** Version for Blast_tac. Hyps that are affected by the substitution are |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
198 |
moved to the front. Defect: even trivial changes are noticed, such as |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
199 |
substitutions in the arguments of a function Var. **) |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
200 |
|
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
201 |
(*final re-reversal of the changed assumptions*) |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
202 |
fun reverse_n_tac 0 i = all_tac |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
203 |
| reverse_n_tac 1 i = rotate_tac ~1 i |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
204 |
| reverse_n_tac n i = |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
205 |
REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
206 |
REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i); |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
207 |
|
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
208 |
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*) |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
209 |
fun all_imp_intr_tac hyps i = |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
210 |
let fun imptac (r, []) st = reverse_n_tac r i st |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
211 |
| imptac (r, hyp::hyps) st = |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
212 |
let val (hyp',_) = List.nth (prems_of st, i-1) |> |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
213 |
Logic.strip_assums_concl |> |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
214 |
Data.dest_Trueprop |> Data.dest_imp |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
215 |
val (r',tac) = if Pattern.aeconv (hyp,hyp') |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
216 |
then (r, imp_intr_tac i THEN rotate_tac ~1 i) |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
217 |
else (*leave affected hyps at end*) |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
218 |
(r+1, imp_intr_tac i) |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
219 |
in |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
220 |
case Seq.pull(tac st) of |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
221 |
None => Seq.single(st) |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
222 |
| Some(st',_) => imptac (r',hyps) st' |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
223 |
end handle _ => error "?? in blast_hyp_subst_tac" |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
224 |
in imptac (0, rev hyps) end; |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
225 |
|
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
226 |
|
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
227 |
fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) => |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
228 |
let val (k,symopt) = eq_var false false Bi |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
229 |
val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi) |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
230 |
(*omit selected equality, returning other hyps*) |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
231 |
val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1) |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
232 |
val n = length hyps |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
233 |
in |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
234 |
if !trace then writeln "Substituting an equality" else (); |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
235 |
DETERM |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
236 |
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
237 |
rotate_tac 1 i, |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
238 |
REPEAT_DETERM_N (n-k) (etac Data.rev_mp i), |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
239 |
etac (if symopt then ssubst else Data.subst) i, |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
240 |
all_imp_intr_tac hyps i]) |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
241 |
end |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
242 |
handle THM _ => no_tac | EQ_VAR => no_tac); |
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset
|
243 |
|
0 | 244 |
end; |
245 |