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



On Sat, 9 Jul 2011, Matej Urbas wrote:

I want to 'replace' the current subgoal sg1 with sg2. Therefore I make a
meta-implication and prove it with 'Goal.prove':

       val intert = Logic.mk_implies (sg2, sg1)
       val interThm = Goal.prove ctxt [] [] inter1 (K ((auto_tac
       (clasimpset_of ctxt)) THEN (ALLGOALS (Intuitionistic.prover_tac
       ctxt NONE))))

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.

This is all a bit indirect -- working against the natural flow of reasoning in Isabelle/Pure. Note that compose_tac is outside the normal rule composition paradigm, i.e. you are standing naked in the cold rain.

When you have a structured goal with its own !! and ==> the canonical proof enters that context and establishes the conclusion, e.g. see SUBGOAL.FOCUS and similar (which are mentioned in the "implementation" manual).

There are sometimes reasons to bypass the primary structure, but it should be only done if there are explicit reasons for it. My favourite internal operation for that is Thm.compose_no_flatten, but that is not for the faint-hearted.


	Makarius





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