Re: [isabelle] fixrec’s demand for continuity proofs



Dear Brian,

thanks for your detailed response, I’m having a much clearer picture now
and also managed to define my function using HOLCF.


I had some problems with the cont2cont_Let' rule in the cont2cont rule
set. Here is a minimal example:
______________________________________________________
lemma "cont (λx. x⋅(Discr True))"
by (intro cont2cont)
______________________________________________________
works as expected. But
______________________________________________________
lemma "cont (λx. let y = True in x⋅(Discr y))"
by (intro cont2cont)
______________________________________________________
does not. The goal that it is stuck on is
"cont (λp. Discr (snd p))".

It works after I added this lemma to the cont2cont set, which works for
let expressions where the variable x does not appear in the bound
expression:
______________________________________________________
lemma cont2cont_Let_simple[simp,cont2cont]:
  assumes "cont (λx. g x t)"
  shows "cont (λx. let y = t in g x y)"
unfolding Let_def using assms .
______________________________________________________

I’m not sure if this is a general solution and or it would somehow
conflict with cont2cont_Let'. If it is a general solution, feel free to
add it to HOLCF.



Furthermore, I had to add these lemmas:
______________________________________________________
lemma cont2cont_list_case [simp, cont2cont]:
  assumes "⋀y. cont (λx. f1 x)"
     and  "⋀y z. cont (λx. f2 x y z)"
  shows "cont (λx. list_case (f1 x) (f2 x) l)"
using assms
by (cases l) auto

lemma cont2cont_prod_case [simp, cont2cont]:
  assumes "⋀y z. cont (λx. f x y z)"
  shows "cont (λx. prod_case (f x) p)"
using assms
by (cases p) auto
______________________________________________________
plus similar ones for each algebraic data types that I am using. The
form of these lemmas is very static – do you think this can be
generalized somehow? I did not yet write any ML scripts in Isabelle, but
I’m eager to learn if there is a worthwhile goal.


Thanks,
Joachim

PS: I wrote a "list :: cpo(cpo)" instance, relating lists of equal
length piecewise and not relating lists of different lengths, at
http://git.nomeata.de/?p=funcCF.git;a=blob;f=CFGraph/HOLCFList.thy;hb=HEAD
If you think this is generally useful and know where to put it I’d
happily share it (after make the proofs prettier).


-- 
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.