Re: [isabelle] Ways to use expression shorthands in proof?



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








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.