Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
- From: Thomas Sewell <Thomas.Sewell at nicta.com.au>
- Date: Fri, 01 Mar 2013 13:41:47 +1100
- In-reply-to: <512F2933.firstname.lastname@example.org>
- References: <512DD2E4.email@example.com> <512F2933.firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120410 Thunderbird/11.0.1
I think that the problem with providing "A <= B; B <= A ==> A = B" as a
conditional rewrite rule is that the simplifier will (probably) see this
as a rule for rewriting A into B rather than a rule for rewriting "A =
B" into True. This is too general, it will be applied anywhere there is
an A with an appropriate type.
One solution is to resolve your rule with Eq_TrueI, for instance, "thm
equalityI[THEN Eq_TrueI]". Your rule should then look like "A <= B; B <=
A ==> (A = B) == True", which strongly suggests to the simplifier that
it should be used only for rewriting actual equalities.
For some reason the system seems to figure this out by itself when given
the equalityI rule from HOL, which may invalidate this comment.
This archive was generated by a fusion of
Pipermail (Mailman edition) and