Re: [Hol-info] working proof that shouldn't need to be so complicated

2018-01-05 Thread Jeremy Dawson
Sorry if I've missed your point (just a quick reply) but On 01/06/2018 05:18 AM, Michael Beeson wrote: SIMP isn't a conversion SIMP_CONV is a conversion, which may give what you want And if RHS_CONV would do what you want, no need to use PAT_CONV Jeremy

Re: [Hol-info] working proof that shouldn't need to be so complicated

2018-01-05 Thread Petros Papapanagiotou
Dear Michael, On 05/01/2018 18:18, Michael Beeson wrote: But, we have to rewrite ONLY that term, and not the other tarea terms. We can do that kind of thing with PAT_CONV,  but it only works on conversions, and SIMP isn't a conversion,  hence the convoluted code above that makes REWRITE into a

[Hol-info] working proof that shouldn't need to be so complicated

2018-01-05 Thread Michael Beeson
Here is a fragment of working code (but depending on some previous stuff not shown, so you can't just run this code). Since the code works, you don't need to run it--I'm just asking if it really needs to be this complicated. Details below. let tapermutation = MATCH_MP ta3 ta2;; # tarea(c,a,b)