Re: [isabelle] Isabelle2013-1-RC2 available for testing



Dear all,

some (mostly unimportant) comments and questions on the extended documentation of the function package (nice to have the new elim/cases rules!):

- "A definition of function f" -> "The definition of a function f" (Otherwise it sounds like only "f", and no other function, gives rise to the new rules.)

- "also tell us" -> "also tells us" (Since "the rule", independent of its name, is singular.)

- "elim rules above" -> "elims rule above" (?) (Why is "elim" typeset as it is? Should this refer to the name of the fact, or the "elim" attribute?)

- In the example lemma, how about the more "canonical"

  lemma
    assumes "list_to_option xs = y"
    shows "P"
  using assms
  proof (rule list_to_option.elims)
    fix x
    assume "xs = [x]" and "y = Some x"
    then show "P" sorry
  next
    assume "xs = []" and "y = None"
    then show "P" sorry
  next
    fix a b xs'
    assume "xs = a # b # xs'" and "y = None"
    then show "P" sorry
  qed

instead of using the old-school "erule"?

- In general, why is the name "f.elims" (rather than "f.elim")? Won't this be a single rule in most cases? Only for mutually recursive functions there are more? Or do I miss something? (Sorry if this was discussed before.)

- Btw: A few words on what happens for mutually recursive functions might be helpful (e.g., with the "standard" definition of "even"/"odd" I end up with 3 rules in each of "even.elims" and "odd.elims").

cheers

chris





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