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

```Can't you prove "(A seO B) ==> (A = B)" and then use that theorem as a rule?

On Wed, Feb 27, 2013 at 5:57 PM, Gottfried Barrow
<gottfried.barrow at gmx.com>wrote:

> I guess the answer might be in the The Isabelle Cookbook.
>
> http://www.inf.kcl.ac.uk/**staff/urbanc/Cookbook/<http://www.inf.kcl.ac.uk/staff/urbanc/Cookbook/>
>
> Maybe in chapter 6, Tactical Reasoning.
>
> So far, I've enjoyed only needing a bare bones structured proof, or only a
> "by(metis...)" proof that Sledgehammer found for me.
>
> But having to frequently have 7 lines for a proof, which is really only
> about 4 or 5 lines of proof, that's weighing heavy on me.
>
> If someone wants to give me the ML to implement the 7 lines of proof
> below, that would be good, but then, maybe to automate it, tactics are
> needed. I wouldn't know anything about tactics.
>
> Regards,
> GB
>
>
>
> On 2/27/2013 9:49 AM, Gottfried Barrow wrote:
>
>> 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.