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"

and

  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.