Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Adding lemmas to fact collections

Email Gateway (Aug 18 2022 at 12:28):

From: David Trachtenherz <trachten@in.tum.de>
Hello,

in Isabelle 2005 it was possible to successively add lemmas to a
collection of lemmas in a way like:
lemmas some_lemmas = lemma1 lemma2
lemmas some_lemmas = some_lemmas lemma3
lemmas some_lemmas = some_lemmas lemma4
...

In Isabelle 2008 this method yields the error message "Duplicate fact".
Is there a way to add new facts to an already declared fact collection?

Thank You in advance!

David

Email Gateway (Aug 18 2022 at 12:28):

From: Makarius <makarius@sketis.net>
Overwriting existing fact names in older versions of Isabelle did not
really achieve the effect of "adding facts to a collection", and had many
other problems (there was also a warning). For example, merging theories
did not merge these pseudo-containers, but select one from some branch
(via the name space).

This is how to do named collections of facts properly in Isabelle2008:

ML {* structure Foo = NamedThmsFun(val name = "foo" val description = "foo rules") *}
setup Foo.setup

declare refl [foo]
declare sym [foo]
declare trans [foo]

thm foo

declare refl [foo del]

thm foo

Makarius

Last updated: May 03 2024 at 08:18 UTC