Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
On 2/28/2013 8:41 PM, Thomas Sewell wrote:
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.
Thanks for the input.
Extraordinarily simple stuff can be a real show stopper for the novice.
I tried "A <= B; B <= A ==> A = B" after Lar's comment, and it gave me a
syntax error, and after searching for documentation on how to use
conditional rewrite rule syntax, particularly how to use the semicolon,
I couldn't find any, so I gave up.
This time I tried a little harder, doing searches and stuff, looking for
that semicolon, and finally I decided it must be an operator, so I
finally tried \<and>, which got me to the next step.
As an aside, the syntax for two other operators that have never worked
for me in jEdit are "/\" and "\/", but they're listed in the symbols panel.
I could talk about Stackexchange more also, about whether this comment
would have gotten made if the replies were split up.
Anyway, the conditional rewrite rule looked a little promising, because
it might be onerous to have to type "(rule)" if I knew I could set
things up without having to do that.
However, the performance of either of "A <= B; B <= A ==> A = B" or "A
<= B; B <= A ==> (A = B) == True" is very slow.
I have some examples of sets which are nested about 11 levels deep. It's
obvious now that Ramana gave me the same formula, but with my own
notation. I told him it was creating some non-termination, but that's
not the case. It's just that it takes forever for simp to simplify these
nested sets. Each level of nesting adds at least twice the time to
At 7 levels it takes about 15 to 20 seconds, where without this
conditional simp rule in, it takes no time, and those examples don't
even need that rule.
Conditional rewriting will come in handy now that I've made the
connection between "conditional" and the conditional "==>". That wasn't
an easy connection to make. Information overload or just a lack of the
necessary amount of hand holding.
Thanks for the suggestion,
This archive was generated by a fusion of
Pipermail (Mailman edition) and