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"
"A seO B"
"A = B"
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