Re: [isabelle] primrec on nested mutually-recursive datatype



Greg Bronevetsky wrote:
I've finally gotten the the point where I need to use the measure function to recdef a type. However, Isabelle wants me to prove that (ALL asOp. 0 < AppSrcOpSize asOp). Unfortunately, I don't know how to prove it. The most obvious proof is by structural induction but I'm too new to Isabelle to know how to specify that. Doing something as simple as "proof (induct asOp)" does not work since Isabelle says "*** Unable to figure out induct rule". What else can I do?

You can only do induction on *free* variables. In your example, induction
is actually overkill, since you can prove the above goal by a sequence
of case distinctions followed by simplification:

lemma "0 < AppSrcOpSize asOp"
  apply (case_tac asOp)
  apply (case_tac x)
  apply (case_tac b)
  apply (case_tac ba)
  apply simp_all
  done

By the way, why don't you use the standard "size" funtion already provided
by the datatype package?

Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





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