Stream: Beginner Questions

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

view this post on Zulip 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

view this post on Zulip Mathias Fleury (Nov 24 2021 at 05:34):

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

view this post on Zulip Mathias Fleury (Nov 24 2021 at 05:36):

(Orders is transitively included)

view this post on Zulip 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"

view this post on Zulip Mathias Fleury (Nov 24 2021 at 05:38):

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

view this post on Zulip 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.

view this post on Zulip Mathias Fleury (Nov 24 2021 at 08:00):

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

view this post on Zulip Mathias Fleury (Nov 24 2021 at 08:00):

Import Main instead of only HOL.Lattices

view this post on Zulip 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

view this post on Zulip Mathias Fleury (Nov 24 2021 at 08:03):

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

view this post on Zulip david streader (Nov 24 2021 at 16:05):

B

Sorry I am so painfully slow
imports "HOL-Lattice.Lattice" begin works just fine in JEdit
But isabelle build still can not find the theory to import. Do I need to set something to tell isabelle build where to look?

dstr@D NEW % more PreGalois/ROOT
session Test = HOL +
options [document = pdf, document_output = "output"]
theories
PreGalois
document_files
"root.tex"
dstr@D NEW %
dstr@D NEW % isabelle build -D PreGalois
*** Cannot load theory "HOL-Lattice.CompleteLattice"
*** The error(s) above occurred in session "Test" (line 1 of "/Users/dstr/IsabelleWork/NEW/PreGalois/ROOT")
dstr@D NEW %

view this post on Zulip Mathias Fleury (Nov 24 2021 at 16:35):

You want:

imports "HOL-Lattice.CompleteLattice"

view this post on Zulip Mathias Fleury (Nov 24 2021 at 16:35):

in the root file:

session Test = HOL +
options [document = pdf, document_output = "output"]
sessions
   HOL-Lattice
theories
   PreGalois
document_files
    "root.tex"

view this post on Zulip david streader (Nov 24 2021 at 17:11):

Many Thanks it works.

view this post on Zulip Notification Bot (Nov 24 2021 at 17:12):

david streader has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC