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

```I'll simplify my question.

```
I have a very common theorem and proof pattern which uses "=", a binary operator "seO", and a theorem "ssO":
```
theorem "A = B"
proof- have
"A seO B"
by(simp)
thus
"A = B"
by(metis ssO_eq)
qed

```
I'm learning proof techniques on an as-need basis, where Sledgehammer and metis have dramatically reduced the "need" in "as-need".
```
Is there some way I can automate that specific proof template?

```
Can I do that in ML? Is there an example somewhere that will show me how to do it?
```
```
I can't set up a simp rule for the formula "(A seO B) = (A = B)" because it's exactly "(A seO B)" that I have to prove to get "(A = B)".
```
Thanks,
GB

On 2/27/2013 3:33 AM, 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.
```
```
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

```
```

```

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