Re: [isabelle] proving a class instantiation.



On Tue, 9 Nov 2010, Brian Huffman wrote:

<viorel.preoteasa at abo.fi> wrote:
fix a b c::"'a N" show "a * b = a * c ==> b = c"  by (rule
cancel_times_left, simp) next;

I cannot get rid of the first suboal. The first subgoal changes to:

1. /\ a b c . a * b = a * c ==> ?a12 a b c * b =?a12 a b c * c
2. /\ b a c . b * a = c * a ==> b = c

The quick fix is to avoid using this:

fix a b c::"'a N" show "a * b = a * c ==> b = c"

and instead use explicit 'assume' commands:

fix a b c::"'a N" assume "a * b = a * c" thus "b = c"

Hopefully this strange behavior can be changed in a future release of Isabelle,

users seem to get stuck on the same problem on a regular basis.

This is mainly due to the historic goal state output: when the system prints a subgoal "!!x. A x ==> B x" it means "for arbitrary but fixed x you may now assume A x and then have to show B x", but this is not immediately clear. Since the post-Proof-General model is less centered around goal states anyway, the confusion might disappear by itself at some point. There are also other reforms in the pipeline (for many years already) that did not make it into the light of reality yet.


because using 'show' with meta-implications is useful sometimes

Can you give an example for that?  I.e. where show "!!x. A x ==> B x"
is needed as such, instead of something that is equivalent to
{ fix x assume "A x" then show "B x" ... } ?


	Makarius


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