Passing the theorem EQ_SYM_EQ will normalise this sort of thing:
> EQ_SYM_EQ;
val it =
|- ∀x y. x = y ⇔ y = x:
thm
> SIMP_CONV (srw_ss()) [EQ_SYM_EQ] “a = b ∧ x = z ⇔ b = a ∧ x = z”;
<<HOL message: inventing new type variable names: 'a, 'b>>
val it =
|- (a = b ∧ x = z ⇔ b = a ∧ x = z) ⇔ T:
thm
Michael
On 29/10/17, 02:58, "Mario Castelán Castro" <marioxcc...@yandex.com> wrote:
Sometimes I have a goal of the form “P = Q” where P and Q are terms that
are the same except for the order of the arguments of a symmetric
relation, e.g. (in this case equality): “a = b ∧ x = z ⇔ b = a ∧ x = z”.
Can these sub-terms be normalized by SIMP_TAC analogous to how it can
normalize associative and commutative functions?.
Thanks.
--
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
