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.
The short answer is: If you use Goal.prove_internal instead of Goal.prove,
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.