[isabelle] problem with opening proof



OK, I gave Isar another try and I'm making some progress with it. Anyway.

I have some statements like

fix ...
assume ... and ...
thus "EX x y. ..."
proof

The "proof" line fails, with "empty result sequence", unless I change
it to "proof -" or change "thus" to "show", hence taking the
assumptions out of "this". Why are my assumptions getting in the way
of what should be a simple application of exI? This makes no sense to
me, as exI only cares about the conclusion. Let me know if I need to
send an example.

On a completely different note, it would be cool if abbreviations
could be made that are local to proofs. Often I have expressions
repeated several times throughout a goal that make it quite large,
when it would be manageable with some abbreviations. Let statements
are nice, but they're expanded in the goal display. Such a command
might not semantically differ from the let command.

Chris Capel
-- 
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)





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