Re: [isabelle] subst question



On Wed, 12 Oct 2005, Jeremy Dawson wrote:

> Reto Kramer wrote:
> > I find myself with the following subgoal:
> > 
> >    !! a b. a = ?y31 (a,b)
> > 
> > How do I tell Isabelle to replace ?y31 with "fst" so that simp will  solve
> > the goal?

> Actually I've found you get a less flaky proof by the following
> which removes the 31 (which is particularly likely to vary after minor changes
> in your preceding proof steps)
> 
> by (PRIMITIVE standard) ;
> by (instantiate_tac [("y", "fst")]) ;

Just note that using standard within a proof is a very bad idea -- its
purpose is to conclude a sequence of reasoning, producing a certain normal
form with some internal rearrangements.  Even worse, standard only works
properly in a top-level theory context, but messes up the proof state in
the presence of local assumptions, locales etc.

Functions like prove_goal, prove_goalw_cterm are of the same category, and
are better avoided.


> see the reference manual s3.5.1 and s3.1.4

The reference manual is slightly outdated, and will be replaced 
eventually.


	Makarius





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