Re: [isabelle] introducing local names in proofs

The right way is to use a structured proof, where you have elements such as

  def a \<equiv> "x+y+z"


  let ?a = "x+y+z"

The former must be expanded explicitly, while the latter are mere abbreviations and expand automatically.

Larry Paulson

On 3 Mar 2011, at 10:17, Viorel Preoteasa wrote:

> Hello,
> In a proof I need to introduce some local names.
> something like: a = x+y+z, b = a + x, ...
> apply (subgoal_tac "\<exists> a b: a = x+y+z /\ b = a + x")
> but this is simplified away by simp or safe.
> Is there a way to achieve this goal?
> Best regards,
> Viorel

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