Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step



On 27.02.2013 10:33, Gottfried Barrow wrote:
Hi,

I've set up a bunch of simp rules, and I'm getting lots of 1 step proofs
with "by(simp)".

However, there's one common proof which I can't figure out how to get in
1 step, which is set equality for the case where I have to prove "A is a
subset of B and B is a subset of A", which I have to do because the auto
provers can't prove "A = B" directly.

The problem is that my "A is a subset of B and B is a subset of A" is my
main equality "A=B", so I'm blank on how I can automate the connection
between the two.

You could a conditional rewrite rule "A <= B; B <= A ==> A = B".

BTW: Having one of your central operators be an abbreviation (especially one which is likely to be modified by simp/auto) will probably do more harm than good, as automated tactics will often modify your goal in a way, where your Lemmas do not apply directly anymore.

BTW2: Having (minimal, working) theory files instead of PDFs makes it often easier to come up with good suggestions.

  -- Lars





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