# Re: [isabelle] Problems with Logic.mk_implies + compose_tac

```Hi Matej,

> I am having a bit of problems using 'compose_tac' with an intermediate
> theorem (produced with mk_implies + Goal.prove). I hope you do not mind
> if I ask for a hint.
> [...]
> The next step is to use interThm in 'compose_tac', which is applied on
> the original goal sg1:
>
>         compose_tac (false, interThm, 1) i
>
> which fails.
your approach works just fine. (See the code below.)

The function Goal.prove_internal is merely a wrapper for Goal.init /
Goal.conclude (+ introducing & discharging assumptions), and init/conclude
perform the internal fiddling with the invisible protect constant for you.
A quick grep over the sources shows that prove_internal and compose_tac are
used by tools and internal code, presumably to do similar low-level goal
manipulations.

I'm sure this solution is not entirely orthodox, but since it worked
for me in many similar situations where I needed precise control over
the entire subgoal structure, I thought I'd share it none the less.

Holger

lemma sg1:
"⋀s1 s2. ⟦distinct [s1, s2]; s1 ∈ A; s1 ∈ B; s2 ∈ A; s2 ∉ B⟧ ⟹
∃s1 s2. distinct [s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B"
apply (tactic {*
SUBGOAL
(fn (sg1,i) =>
let val ctxt = @{context}
val sg2 = @{term "⋀s1 s2. ⟦distinct[s1, s2]; s1 ∈ A ∩ B; s2 ∈ A - B⟧
⟹ (∃s1 s2.
distinct[s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B)"}
val intert = Logic.mk_implies (sg2, sg1)
val intert_cterm = Thm.cterm_of (ProofContext.theory_of ctxt) intert
val _ = tracing ("Have "^Syntax.string_of_term @{context} intert)
val interThm = Goal.prove_internal [] intert_cterm
(K ((auto_tac (clasimpset_of ctxt)) THEN (ALLGOALS
(Intuitionistic.prover_tac
ctxt NONE))))
val _ = tracing ("Interm: "^Display.string_of_thm @{context} interThm)
in
compose_tac (false, interThm, 1) i
end) 1
*})

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.