|
68630
|
1 |
signature INST_EXISTENTIALS =
|
|
|
2 |
sig
|
|
|
3 |
val tac : Proof.context -> term list -> int -> tactic
|
|
|
4 |
end
|
|
|
5 |
|
|
|
6 |
structure Inst_Existentials : INST_EXISTENTIALS =
|
|
|
7 |
struct
|
|
|
8 |
|
|
|
9 |
fun tac ctxt [] = TRY o REPEAT_ALL_NEW (resolve_tac ctxt @{thms HOL.conjI})
|
|
|
10 |
| tac ctxt (t :: ts) =
|
|
|
11 |
(TRY o REPEAT_ALL_NEW (resolve_tac ctxt @{thms HOL.conjI}))
|
|
|
12 |
THEN_ALL_NEW (TRY o (
|
|
|
13 |
let
|
|
|
14 |
val thm = Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt t)] @{thm HOL.exI}
|
|
|
15 |
in
|
|
|
16 |
resolve_tac ctxt [thm] THEN' tac ctxt ts
|
|
|
17 |
end))
|
|
|
18 |
|
|
|
19 |
end |