Stream: Beginner Questions

Topic: Copying theorem output into e-mail


view this post on Zulip Gergely Buday (Jan 05 2021 at 08:52):

I would like to copy theorem output into e-mail. I tried two ways, none of them worked properly.

First: copy from the generated pdf:

[x1 ⇒ x2;
V s. P (SKIP, s) s; V x a s. P (x ::= a, s) (s(x := aval a s));
V c
1 s 1 s 2 c 2 s 3 .

Here and in Thunderbird the meta universal quantifier appears as a capital form of disjunction.

Second: copy from Isabelle/JEdit Output window:

?x1.0 ⇒ ?x2.0 ⟹
(⋀s. ?P (SKIP, s) s) ⟹
(⋀x a s. ?P (x ::= a, s) (s(x := aval a s))) ⟹
(⋀c⇩1 s⇩1 s⇩2 c⇩2 s⇩3. (c⇩1, s⇩1) ⇒ s⇩2 ⟹ ?P (c⇩1, s⇩1) s⇩2 ⟹ (c⇩2, s⇩2) ⇒ s⇩3 ⟹ ?P (c⇩2, s⇩2) s⇩3 ⟹ ?P (c⇩1;; c⇩2, s⇩1) s⇩3) ⟹

instead of $c_1$, c⇩1 appears. Also, x1 becomes ?x1.0 .

Is there a panacea for this?

view this post on Zulip Mathias Fleury (Jan 05 2021 at 09:19):

IIRC, copy-pasting from the HTML preview works

view this post on Zulip Gergely Buday (Jan 05 2021 at 09:27):

This is a generated theorem that is not present in the HTML preview.

view this post on Zulip Gergely Buday (Jan 05 2021 at 13:18):

#!/bin/bash

sed -e $'s/⇩1/\u2081/g' <$1 | \
sed -e $'s/⇩2/\u2082/g' | \
sed -e $'s/⇩3/\u2083/g' | \
sed -e $'s/⇩4/\u2084/g' | \
sed -e $'s/⇩5/\u2085/g' | \
sed -e 's/?//'g

Creates proper subscript numbers up to 5 and removes question marks for schematic variables. This processes theorems in the Output window of Isabelle/JEdit.

Notice the leading $ that enables shell escapes for unicode characters:

https://stackoverflow.com/questions/27140408/bash-replacing-a-number-with-unicode-character-using-sed/27141959#27141959

view this post on Zulip Manuel Eberl (Jan 05 2021 at 13:40):

you can also do thm [no_vars] to get rid of schematic variables.

view this post on Zulip Gergely Buday (Jan 05 2021 at 13:51):

@Manuel Eberl Does that work only in document preparation's @{thm } sequence or also in Isabelle/JEdit Output window?

I could not add [no_vars] anyhow into

lemmas big_step_induct = big_step.induct [split_format(complete)]

view this post on Zulip Manuel Eberl (Jan 05 2021 at 13:55):

Well you should only use this for presentation, really. You know, when you want to copy-paste stuff into an email or something.

view this post on Zulip Manuel Eberl (Jan 05 2021 at 13:55):

But yes, no_vars is just an attribute. You can do thm foo[no_avsrs] or lemmas bar = foo[no_vars].


Last updated: Sep 25 2021 at 09:17 UTC