Email Gateway (Aug 19 2022 at 08:29): Email Gateway (Aug 19 2022 at 08:29):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi people out there,
Sorry for an other rather beginner's question, but here is: I favor
explicit proof over automated one, except for some simplifications group.
That works, but this often lead to repeated subexpressions in multiple
“have”, and that bloats the proof text, which in turn, does not help
readability. I wondered if there is a way to have shorthands for common
expression appearing at multiple places. I tried with a “def E ≡
"my-expression"” and then an “have "blah E blah"”, but it does not work,
seems E is not replaced with the corresponding expression as I expected,
and proofs by simp which succeed with the literal subexpression, fails
when I replace the literal subexpression with E. I also tried a naive
“write "my-expression" ("E")”, but that's even worse, Isabelle complains
the expression is an unknown constant.
You see that's not a question about proving, but a question about style in
writing proofs.
I have another in the same vein, for which I don't wish to open a new
thread. I don't know about LaTex, and wondered if there a way, to do the
same with plain text comments. That is, I would write a comment somewhere,
and either include it at another place or else add a reference to it from
that other place.
I may also have a question about the different way to invoke the
simplifier, but I leave that for later; that's enough for that thread.
Have a nice day all
Email Gateway (Aug 19 2022 at 08:30):From: Brian Huffman <huffman@in.tum.de>
When you use "def E == expression", the definition of E must be
unfolded explicity (using something like "apply (simp add: E_def)" or
"unfolding E_def").
The alternative is to use "let" to define a new schematic variable:
"let ?E = expression". Then "?E" is really just an input abbreviation,
no explicit unfolding necessary.
Email Gateway (Aug 19 2022 at 08:30):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Yannick,
Brian already answered your question, which is good information for me
also, but for myself, I worked up how to use "abbreviation" to
abbreviate a formula, which is probably not best for your situation, but
which may come in handy for me, though I notice that in prog-prove.pdf,
it tells me that abbreviations should be used sparingly.
On 8/4/2012 7:06 AM, Yannick Duchêne (Hibou57) wrote:
Sorry for an other rather beginner's question, but here is: I favor
explicit proof over automated one, except for some simplifications group.
For an interesting discussion of an explicit proof example using
introduction and elimination rules, scroll down to Wenzel's PhD thesis
on the page below, and have a look at pages 77 to 92 where he takes a
simple example and starts with a very abbreviated form and keeps
expanding it into more explicit forms.
http://www4.in.tum.de/~wenzelm/papers/
<http://www4.in.tum.de/%7Ewenzelm/papers/>
I tried with a “def E ≡ "my-expression"” and then an “have "blah E
blah"”, but it does not work, seems E is not replaced with the
corresponding expression as I expected, and proofs by simp which
succeed with the literal subexpression, fails when I replace the
literal subexpression with E.
Here's what I get with a simple example:
theory z0_i_Scratch imports Main begin
typedecl sT
consts inS::"sT => sT => bool" (infixl "IN" 55)
consts emS::sT
axiomatization where
eeA_that_would_have_hard_to_type_name: "!x. ~(x IN emS)"
lemma eeA_ASCI_name1: "!x. ~(x IN emS)"
by(metis eeA_that_would_have_hard_to_type_name)
abbreviation
eeA_exp_name::"bool" where "eeA_exp_name == (!x. ~(x IN emS))"
lemma eeA_ASCI_name2: "!x. ~(x IN emS)"
by(metis eeA_ASCI_name1)
end
When I put the cursor at "eeA_ASCI_name2" in the output panel, "(!x. ¬(x
IN emS))" gets replaced with "eeA_exp_name", unlike at "eeA_ASCI_name1".
As far as getting something like "(!x. ¬(x IN emS))" replaced with
another formula (that's not a named identifier), I don't know about that.
Abbreviation is syntactic sugar (page 14 of prog-prove.pdf).
I have another in the same vein, for which I don't wish to open a new
thread. I don't know about LaTex, and wondered if there a way, to do
the same with plain text comments. That is, I would write a comment
somewhere, and either include it at another place or else add a
reference to it from that other place.
I guess you're talking about defining a "macro command" as in Latex, and
then using the macro, where it gets expanded when the PDF document is built.
That would be the use of antiquotations inside of "text{...}",
"section{...}", etc., and lots of other places; I don't use
antiquotations yet. Learning the details of how to use antiquotations
would be on the level of learning how to use Latex, but if you were
going to learn one first, then you'd probably want to learn
antiquotations first (page 64 isar-ref.pdf).
What you eventually end up doing is using antiquotations with Latex;
Isabelle uses Latex rather than duplicate it.
Whether or not you take advantage of additional Latex commands, if you
specify the document to be built with something like "usedir", Latex is
used to create the PDF.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:30):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Currently on the page 77 you mentioned, looking at “is” and “concl is”.
Looks even shorter and straighter than using “let”. That's what I like
with my discovery of Isabelle: as I go, I understand it's intentionally
designed to author concise and readable proof, and to balance both
(conciseness and verbosity) as you see fits.
Email Gateway (Aug 19 2022 at 08:30):From: Gottfried Barrow <gottfried.barrow@gmx.com>
The page 77 you're talking about is the absolute page number, which
would be the printed page number of 63.
The example I'm talking about is sections 4.2.3 and 4.2.4, printed page
numbers 77 to 92.
It goes to show that there are lots more examples and explanations in
that document on Isar. For each keyword described in Wenzel's document,
if you look the keyword up in isar-ref.pdf, then you learn even more.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:31):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I finally go with both Brian's suggestion to use “let” and Markus's thesis
suggestion to use “"…" (is "…")”. I ended to the test files attached to
that message. Please note that's nothing exiting, just intended to
beginners like me, and to be opened to comments (comments are easier on
simple things). It's based on something from a function tutorial in
Isabelle's documentation directory. I'm not so much happy with the PDF
rendering, but I don't know enough about (La)Tex, that may be the reason
why (I also wonder why the document weight more than expected, but that's
another story).
Thanks for your tips, to both of you
Isa_Test.thy
Isa_Test.pdf
Last updated: Apr 25 2024 at 20:15 UTC