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



On Sat, Aug 4, 2012 at 2:06 PM, Yannick Duchêne (Hibou57)
<yannick_duchene at yahoo.fr> wrote:
> 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.

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.

- Brian





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