Re: [isabelle] Adding lemmas to HOL?



I was thinking along those lines as well. Moreover, it makes sense on any set of lists:

"GREATEST ps WRT length. âxs â L. prefix ps xs"

Of course that one is not executable. I'll put something suitable together.

Tobias

On 27/05/2016 13:36, Joachim Breitner wrote:
Hi,

so much â quantifiers. Given that for any two lists, the maximal common
prefix is unique, wouldnât it make sense to give this a name, define it
straight-forwardly using fun, and then possibly add lemmas?

Greetings,
Joachim

Am Freitag, den 27.05.2016, 12:05 +0200 schrieb Christoph Dittmann:
Hi,

I am looking for lemmas that show that from every pair of lists you
can
split off a maximal common prefix or suffix. I am looking for this:

lemma maximal_common_prefix:
  shows "âps xs' ys'. xs = ps @ xs' â ys = ps @ ys'
         â (xs' = [] â ys' = [] â hd xs' â hd ys')"
  by (induct xs ys rule: list_induct2', blast, blast, blast)
     (metis (no_types, hide_lams) append_Cons append_Nil list.sel(1))

corollary maximal_common_suffix:
  shows "âss xs' ys'. xs = xs' @ ss â ys = ys' @ ss
         â (xs' = Nil â ys' = Nil â last xs' â last ys')"
  using maximal_common_prefix[of "rev xs" "rev ys"]
  unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)

The proofs work, but I would have expected that these statements
already
exist somewhere in src/HOL/List.thy.  Unfortunately, I couldn't find
these or something similar.  I would be glad if someone corrected me.

These two lemmas look to me like they could be useful for many proofs
because they give a general way to decompose two lists.

So my question is, what is the process to propose new lemmas for HOL?
Do these two lemmas look reasonable enough (assuming they don't
already
exist)?

Thanks,
Christoph




Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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