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


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.


Attachment: sTs_doc.pdf
Description: Adobe PDF document

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