Re: [isabelle] Question on hypothesis



On Fri, 3 Dec 2010, olfa mraihi wrote:

1)how to represent hypothesis in isabelle? is it with the keyword "assume"?

2)how to tell isabelle to simplify a set of hypothesis under the use of the adequate theory?  (remark:there is no goal to prove,only hypothesis to simplify)

Here are some examples that illustrate goal-free experimentation in Isabelle2009-2:

  theory Scratch
  imports Main
  begin

  example_proof
    assume "P (xs @ [])"
    thm this [simplified]

    have "xs @ [] = xxx" apply simp
      oops


	Makarius


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