Stream: General

Topic: OptionalSugar

Lukas Stevens (Aug 12 2019 at 12:17):

When defining an inductive predicate, Isabelle turns rules of the form

a: A ⟹ B ⟹ C

into

A ∧ B ⟹ C

which is inconvenient when trying to typeset the rules with the antiquotation

@{thm[mode=Rule] a}

since the assumptions are connected by a conjunction.
How can I control that behaviour or change the shape of the rule before typesetting?

Alexander Krauss (Aug 12 2019 at 12:42):

Inductive should normally not do this. When does this happen to you?

Lukas Stevens (Aug 12 2019 at 12:46):

I am not doing anything special. Isabelle version is August 2018. My inductive predicate looks like follows:

inductive proves :: "literal set ⇒ literal ⇒ bool" (infix "⊢⇩P" 60) where
assm: "⟦ l ∈ A; is_EQ_or_LEQ l ⟧ ⟹ A ⊢⇩P l"
...

Alexander Krauss (Aug 12 2019 at 12:52):

And now assm comes out with a conjunction? This is unexpected as far as I know. Can you produce a self-contained runnable example?

As a workaround/hack for presentation, you might try assm[OF conjI].

Lukas Stevens (Aug 12 2019 at 12:58):

I just noticed that

thm "proves.assm"

gives the correct output when used directly after the definition, but not in Thesis.thy which I use for writing the document.
This is my setup:
The root directory contains the directory src and the directory thesis.
In src, I have all my theory files that constitute my proofs. It has the following ROOT file:

session Order = HOL +
  theories
    Order_Semantics
    Partial_Order
    Partial_Order_Proofs
    Partial_Order_Impl
    Total_Order

In thesis, I have a file Thesis.thy with which I typeset my thesis. The ROOT file looks like follows:

session Thesis_Base = HOL +
  sessions
    "HOL-Library"
    Order
  theories
    "HOL-Library.LaTeXsugar"

session Thesis = Thesis_Base +
  options [document = pdf, show_question_marks = false, names_short = true,
    document_output = "build"]
  theories
    Thesis
  document_files
    "root.tex"
    "settings.tex"
    "sources.bib"
    "pages/abstract.tex"
    "pages/acknowledgements.tex"
    "pages/cover.tex"
    "pages/disclaimer.tex"
    "pages/title.tex"
    "build"

I open the file Thesis.thy with the command isabelle jedit -d ../src Thesis.thy & in the directory thesis.
When I type thm proves.assm, the output has the conjunction.

Lukas Stevens (Aug 12 2019 at 13:01):

assm[OF conjI] results in an ML exception because there are no unifiers.

Lukas Stevens (Aug 12 2019 at 13:12):

Ah, I found the culprit, it was my bad. I included OptionalSugar.thy which performs this syntax translation.

Last updated: Apr 20 2024 at 04:19 UTC