Re: [isabelle] Adding lemmas to HOL?


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?


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
Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter

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

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