[isabelle] adm and fixrec’s induct rules

Dear Brian,

I have been working some more with HOLCF (although my supervisers warned
me that I might run into difficulties or make life harder for me...),
and I have some suggestions and some questions. I hope you don’t mind me
accosting them to you, and remember that these really are only
suggestions, not requests :-)

First I noticed that I tend to have a lot of admissibility statements to
proof. With the lemmas provided in Adm.thy, this is usually not a big
problem. I wonder if it would be sensible to take a similar approach
than taken with cont2cont: I.e. have a ruleset adm2adm that I can amend,
so that I can just use "apply (intros adm2adm)" without listing all my
custon adm rules, and be done in most cases. Or possibly "apply (intros
adm2adm cont2cont)", if some rules involve continuity claims, such as
this one I wrote:
lemma adm_single_valued:
 assumes "cont (λx. f x)"
 shows "adm (λx. single_valued (f x))"
using assms
unfolding single_valued_def
by (intro adm_lemmas adm_not_mem cont2cont adm_subst[of f])

My next question is about pattern matching in fixrec equations. At the
moment, fixrec only supports very few constructors in patterns, and the
Discr constructor is not supported. Therefore, I have only one equation
with a large case expression then, which makes the .induct rule
relatively unpleasant to work with (compared with, e.g., the function
package). I’d be glad if I could use the Discr constructor in patterns,
and I’d be even more pleased if arbitrary patterns can be used inside
the Discr constructor. 

And finaly, I’d like to have some advice. I tried to proof a statement
"P f" about the function f defined by fixrec, using f.induct. I noticed
that it would be easier if I know "Q f", so I proved that (again using
f.induct). Turning back to the proof of "P f", I found out that the
lemma "Q f" is useless, as in the inductive proof of "P f" I am not
working with f, but rather an approximation.

I worked around it by proving P and Q simultaneously in one induction,
but the proof is becoming illegibly convoluted.

Is there maybe a cleaner and more idiomatic way of handing such a case?
I’m afraid that if I continue this way, in the end all statements of my
projects will be proven in one huge induct rule. And Isabelle is already
moving slowly inside the induct proof.

Thanks for your support,

Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de

Attachment: signature.asc
Description: This is a digitally signed message part

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