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



Ramana,

Thanks for the tip. I proved something like this:

theorem name [simp]:
"(A seO B) ==> (A = B)"
by(metis foo)

It then caused some non-terminating things to start happening.

However, doing all of that helped me realize that it has to be a two step proof. The flow has to be

(A = B) ====> (A seO B) --> (A = B),

where "====>" means I have to convert (A=B) into the form (A seO B) before anything can be proved, and I can't get the simplifier to convert (A=B) to something like (A seO B), which I suppose is for good reason, since "=" is used everywhere. (In a manner of speaking, I manually convert (A=B) to (A seO B) as the first step in the proof.)

My simp rule expands "seO" into the formula

  "(x IN A --> x IN B) & (x IN B --> x IN A)".

The simp rules then expand formulas like "x IN {a,b}" into the formula "(x = a | x = b)".

With all the expansion, lexicographic ordering, and other simp rules, things get simplified and proved. All the work is done in the processing of the statement

  "(A seO B)" apply(simp).

Unless someone tells me the way to do it, I'll someday check into how to program tactics, and see if that's the way to do it. Whatever the case, the simp or auto methods have to be used, as far I can tell. I don't see how the simplifier could be replaced.

Thanks,
GB



On 2/27/2013 12:26 PM, Ramana Kumar wrote:
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 <mailto: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/

    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.