Stream: Beginner Questions

Topic: how to import "HOL-Lattice.Orders"

david streader (Nov 24 2021 at 04:41):

Hi I am very much a beginer!
In Jedit
**theory PreGalois
imports HOL.Lattices "HOL-Lattice.Orders" begin
**
works. But when I run isabelle build it objects to the second import

dstr@D Gal % isabelle build -D PreGalois
*** Cannot load theory "HOL-Lattice.Orders"

Any ideas much appreciated

Mathias Fleury (Nov 24 2021 at 05:34):

Given the ROOT file, only the import HOL_Lattice.CompleteLattice should work

Mathias Fleury (Nov 24 2021 at 05:36):

(Orders is transitively included)

Mathias Fleury (Nov 24 2021 at 05:37):

The ROOT file includes only one file and this is the only one you should (and can) import:

session "HOL-Lattice" in Lattice = HOL +
  description "
    Author:     Markus Wenzel, TU Muenchen

    Basic theory of lattices and orders.
  "
  theories CompleteLattice
  document_files "root.tex"

Mathias Fleury (Nov 24 2021 at 05:38):

(jEdit is less strict on those things for some reason)

david streader (Nov 24 2021 at 07:58):

Thanks Mathias
I am getting their slowly. As Lattice imports Bounds and that imports Orders all I need is
theory PreGalois
imports "HOL.Lattices" begin
This import works (JEdit) but now the reference to quasi_order that was working (its a class in Orders) breaks
interpretation "abs" : quasi_order "(⊑a) :: 'a ⇒ 'a ⇒ bool"
I have tried Orders_quasi_order , Orders.quasi_order and adding " " but can not find how to reference something thats in a nested import.

Mathias Fleury (Nov 24 2021 at 08:00):

HOL.Lattices and HOL-Lattice.CompleteLattice are not the same

Mathias Fleury (Nov 24 2021 at 08:00):

Import Main instead of only HOL.Lattices

Mathias Fleury (Nov 24 2021 at 08:02):

Mathias Fleury said:

HOL.Lattices and HOL-Lattice.CompleteLattice are not the same

To be clear: quasi_order is defined in "~~src/HOL/Lattice/Orders.thy", so you have to import that theory with HOL-Lattice.CompleteLattice and not HOL.Lattices

Mathias Fleury (Nov 24 2021 at 08:03):

HOL.Lattices refers to "~ ~src/HOL/Lattices.thy", not "~ ~src/HOL/Lattice/<some_theory_here>"

Last updated: Jul 15 2022 at 23:21 UTC