Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] HOL-Eisbach brings in Pure and confusion

Email Gateway (Feb 11 2022 at 11:11):

From: Peter Lammich <lammich@in.tum.de>
The theory named HOL-Eisbach.Eisbach, actually depends on Pure, not on
HOL.
The Eisbach manual just mentions that HOL-Eisbach.Eisbach "needs to be
imported by all Eisbach applications". It does not mention the
following:

It seems that Eisbach has to be imported AFTER Main, see minimal
example attached.

Email Gateway (Feb 11 2022 at 11:46):

From: Dominique Unruh <unruh@ut.ee>
Maybe it would be great (for the next release) to have an Eisbach theory
that already imports HOL.Main, and one based on Pure? Then one does not
have to be careful with the ordering in user-level.

Best wishes,
Dominique.

Email Gateway (Feb 11 2022 at 12:39):

From: Peter Lammich <lammich@in.tum.de>
On Fri, 2022-02-11 at 13:45 +0200, Dominique Unruh wrote:

Maybe it would be great (for the next release) to have an Eisbach
theory
that already imports HOL.Main, and one based on Pure? Then one does
not
have to be careful with the ordering in user-level.

yes, in particular for a theory with HOL in its name ...

Best wishes,
Dominique.

On 2/11/22 1:11 PM, Peter Lammich wrote:

The theory named HOL-Eisbach.Eisbach, actually depends on Pure, not
on
HOL.
The Eisbach manual just mentions that HOL-Eisbach.Eisbach "needs to
be
imported by all Eisbach applications". It does not mention the
following:

It seems that Eisbach has to be imported AFTER Main, see minimal
example attached.

--
Peter

imports "HOL-Eisbach.Eisbach" Main
begin
lemma "fun_ord (≤) (λx. 0) (λx. Suc x)" by (simp add:
fun_ord_def)
(** Fails *)

imports Main "HOL-Eisbach.Eisbach"
begin
lemma "fun_ord (≤) (λx. 0)
(λx. Suc x)" by (simp add: fun_ord_def)
(** Works *)

Last updated: Jul 15 2022 at 23:21 UTC