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



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.

I attach a PDF. On page 7, Notation 3.1.10, I create an abbreviation for "A is a subset of B and B is a subset of A". On page 8 is my Theorem 3.1.12 which shows that "A is a subset of B and B is a subset of A" is equivalent to "A=B".

My theory is filling up with proofs to theorems in which I state a proof step with my "equal subsets" operator, prove it with "by(simp)", and then have to finish it off with the Theorem 3.1.12.

Starting on page 37, there's 6 out of 7 theorems where I do that. Then on page 39, there's the examples that show how I can get equality with my "equal subsets" operator, but not with the normal "=".

That's related to the main reason I care, which is that I'd like to show finite set equality using only one automatic proof method command.

If anyone can tell me how to do that, I'd appreciate it.

Regards,
GB


Attachment: sTs_doc.pdf
Description: Adobe PDF document



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