16 Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)"; |
16 Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)"; |
17 Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)"; |
17 Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)"; |
18 Goal "!!y. [| ?x=y; P(?x) |] ==> y = a"; |
18 Goal "!!y. [| ?x=y; P(?x) |] ==> y = a"; |
19 Goal "!!z. [| ?x=y; P(?x) |] ==> y = a"; |
19 Goal "!!z. [| ?x=y; P(?x) |] ==> y = a"; |
20 |
20 |
|
21 Goal "!!x a. [| x = f(b); g(a) = b |] ==> P(x)"; |
|
22 |
|
23 by (bound_hyp_subst_tac 1); |
21 by (hyp_subst_tac 1); |
24 by (hyp_subst_tac 1); |
22 by (bound_hyp_subst_tac 1); |
|
23 |
25 |
24 Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) |
26 Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) |
25 Goal "P(a) --> (EX y. a=y --> P(f(a)))"; |
27 Goal "P(a) --> (EX y. a=y --> P(f(a)))"; |
26 |
28 |
27 Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \ |
29 Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \ |
53 (*exported purely for debugging purposes*) |
55 (*exported purely for debugging purposes*) |
54 val gen_hyp_subst_tac : bool -> int -> tactic |
56 val gen_hyp_subst_tac : bool -> int -> tactic |
55 val vars_gen_hyp_subst_tac : bool -> int -> tactic |
57 val vars_gen_hyp_subst_tac : bool -> int -> tactic |
56 val eq_var : bool -> bool -> term -> int * bool |
58 val eq_var : bool -> bool -> term -> int * bool |
57 val inspect_pair : bool -> bool -> term * term * typ -> bool |
59 val inspect_pair : bool -> bool -> term * term * typ -> bool |
58 val mk_eqs : thm -> thm list |
60 val mk_eqs : bool -> thm -> thm list |
59 val stac : thm -> int -> tactic |
61 val stac : thm -> int -> tactic |
60 val hypsubst_setup : (theory -> theory) list |
62 val hypsubst_setup : (theory -> theory) list |
61 end; |
63 end; |
62 |
64 |
63 |
65 |
125 | eq_var_aux k _ = raise EQ_VAR |
127 | eq_var_aux k _ = raise EQ_VAR |
126 in eq_var_aux 0 end; |
128 in eq_var_aux 0 end; |
127 |
129 |
128 (*For the simpset. Adds ALL suitable equalities, even if not first! |
130 (*For the simpset. Adds ALL suitable equalities, even if not first! |
129 No vars are allowed here, as simpsets are built from meta-assumptions*) |
131 No vars are allowed here, as simpsets are built from meta-assumptions*) |
130 fun mk_eqs th = |
132 fun mk_eqs bnd th = |
131 [ if inspect_pair false false (Data.dest_eq |
133 [ if inspect_pair bnd false (Data.dest_eq |
132 (Data.dest_Trueprop (#prop (rep_thm th)))) |
134 (Data.dest_Trueprop (#prop (rep_thm th)))) |
133 then th RS Data.eq_reflection |
135 then th RS Data.eq_reflection |
134 else symmetric(th RS Data.eq_reflection) (*reorient*) ] |
136 else symmetric(th RS Data.eq_reflection) (*reorient*) ] |
135 handle _ => []; (*Exception comes from inspect_pair or dest_eq*) |
137 handle _ => []; (*Exception comes from inspect_pair or dest_eq*) |
136 |
138 |
137 local open Simplifier |
139 local open Simplifier |
138 in |
140 in |
139 |
141 |
140 val hyp_subst_ss = empty_ss setmksimps mk_eqs |
142 (*Select a suitable equality assumption; substitute throughout the subgoal |
141 |
143 If bnd is true, then it replaces Bound variables only. *) |
142 (*Select a suitable equality assumption and substitute throughout the subgoal |
|
143 Replaces only Bound variables if bnd is true*) |
|
144 fun gen_hyp_subst_tac bnd = |
144 fun gen_hyp_subst_tac bnd = |
145 let val tac = SUBGOAL (fn (Bi, i) => |
145 let val tac = SUBGOAL (fn (Bi, i) => |
146 let val (k, _) = eq_var bnd true Bi |
146 let val (k, _) = eq_var bnd true Bi |
|
147 val hyp_subst_ss = empty_ss setmksimps (mk_eqs bnd) |
147 in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i, |
148 in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i, |
148 etac thin_rl i, rotate_tac (~k) i] |
149 etac thin_rl i, rotate_tac (~k) i] |
149 end handle THM _ => no_tac | EQ_VAR => no_tac) |
150 end handle THM _ => no_tac | EQ_VAR => no_tac) |
150 in REPEAT_DETERM1 o tac end; |
151 in REPEAT_DETERM1 o tac end; |
151 |
152 |