When defining an inductive predicate, Isabelle turns rules of the form
a: A ⟹ B ⟹ C
A ∧ B ⟹ C
which is inconvenient when trying to typeset the rules with the antiquotation
since the assumptions are connected by a conjunction.
How can I control that behaviour or change the shape of the rule before typesetting?
Inductive should normally not do this. When does this happen to you?
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" ...
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
I just noticed that
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.
assm[OF conjI] results in an ML exception because there are no unifiers.
Ah, I found the culprit, it was my bad. I included OptionalSugar.thy which performs this syntax translation.
Last updated: Aug 15 2022 at 02:13 UTC