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

I guess the answer might be in the The Isabelle 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.


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"
  "A = B"
  by(metis ssO_eq)

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)".


On 2/27/2013 3:33 AM, Gottfried Barrow wrote:

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.


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