Email Gateway (Aug 18 2022 at 13:45): Email Gateway (Aug 18 2022 at 13:45):From: Jesper Bengtson <jesperb@it.uu.se>
Greetings all.
I am currently trying to typeset my thesis with the very nice latex
generation capabilities that Isabelle provides. I have a few questions.
Firstly, when printing proofs, Isabelle does a very nice job of
typesetting the keywords and indentations of the proof scripts, but
the actual object logic terms keep their x-symbol syntax and not the
nice latex sugar that I have defined for them. Is there any flag to
set which would translate them in the same manner as is done when
using the @{term...} antiquotation?
Secondly, I have some very large induction rules which I would like to
present and every case of these rules have all of their parameters
meta-quantified. Is there a mode which removes the actual meta-
quantification? It takes up a lot of space, and the absence of the
quantifiers can be explained in figure captions in stead. What I would
like to do is an equivalent of @{thm_style [mode=Rule] premxx
myInductionRule}, but without the preceeding /\x y z ... . I'm
guessing either a new style or mode is required.
I have been reading through the reference manual, but not found a way
to do these things although I'm sure at least the second one is
possible.
Many thanks.
/Jesper
Email Gateway (Aug 18 2022 at 13:47):From: Tobias Nipkow <nipkow@in.tum.de>
You can add your own styles for printing terms or theorems. Add the
following to your theory. It declares your own styles "no_all_prem1" and
"no_all_prem2" - you can add more if you like.
setup {*
let
fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
strip_assums_all ((a,T)::params, t)
| strip_assums_all (params, B) = (params, B);
fun style_parm_premise i ctxt t =
let val prems = Logic.strip_imp_prems t in
if i <= length prems
then let val (params,t) = strip_assums_all([], nth prems (i - 1))
in subst_bounds(map Free params, t) end
else error ("Not enough premises for prem" ^ string_of_int i ^
" in propositon: " ^ Syntax.string_of_term ctxt t)
end;
in
TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>
TermStyle.add_style "no_all_prem2" (style_parm_premise 2)
end
*}
Now you can go @{thm_style no_all_prem1 my_induction_thm}
Warning: I have hardly tested this!
Tobias
Jesper Bengtson wrote:
Email Gateway (Aug 18 2022 at 13:48):From: Norbert Schirmer <schirmer@in.tum.de>
No there is not. You can only access the full power of syntax print
translations through antiquotations.
Typically there are two kinds of documents typeset with Isabelle:
1) present the pure theory (or an Isabelle tutorial): mainly Isabelle
proof text with documenting @{text } quotations and antiquotations.
2) write a document (like a thesis) about your theories: mainly a big
@{text } quotation with heaps of antiquotations.
Cheers,
Norbert
Last updated: May 03 2024 at 08:18 UTC