David,

Of course, how to make a rule depends on what rule you are trying to make.

¬_∨_thm is an equivalence, i.e. a boolean equation, and the most common way of using equations is by rewriting. If you are doing forward proof then you can rewrite using rewrite_rule, so to use this theorem you might rewrite with it as follows:

val new_thm = rewrite_rule [¬_∨_thm] old_thm;

The effect would be to push in negation over any disjunctions to which it is applied in the old_thm and return the resulting theorem,

If you wanted a special rule to achieve that effect then:

val ¬_∨_rule = rewrite_rule [¬_∨_thm];

which you would use thus:

val new_thm = ¬_∨_rule old_thm;

Roger

On 07/02/2017 05:29, David Topham wrote:
I have made some more progress in applying ProofPower to forward proofs in discrete math. e.g. I can prove DeMorgan's theorem successful (propositional calculus). I would like to use the newly proved theorem in other proofs now. What is the best strategy to do that? Is it to create an SML function that takes an argument of type TERM and returns a THM? Could you give an example of a proved THM intended to be used as a new rule of inference?

I also discovered the not_or_thm in the zed theory, which is DeMorgan's Law, but that does not seem to be a function, so I am not sure how to apply it in a forward proof.

I appreciate any pointers in the right direction (or reference to which manual might enlighten me). Thanks, Dave

On Wed, Aug 17, 2016 at 11:06 AM, David Topham <dtop...@ohlone.edu <mailto:dtop...@ohlone.edu>> wrote:

    Thank you both (Rob and Roger) for your "above and beyond the call
    of duty" help in getting me through my attempts to approach using
    ProofPower to teach Discrete Math. I understand your comments that
    backward proof is more economical than forward proof. Yet, I don't
    think the students will learn how to formulate proof thinking
    skills if ProofPower does it for them! True, that learning how to
    use the mechanized assistance is practical, but we (students) need
    to understand what constitutes valid reasoning so have to see the
    tedious steps one-at-a-time.  (e.g. I tried "a (prove_tac[]);" and
    it works perfectly, but does not show me all the steps that were
    used (is there a way for it to do that?))

    I believe the majority of courses teaching DM don't even try to go
    beyond the paper and pencil proofs--maybe that is good enough, but
    I can't help but think that exposure to professional tools (i.e.
    ProofPower) that force us to think carefully about what we are
    doing and to have the computer not allow us to proceed on shaky
    grounds is beneficial.

    Even though ProofPower is designed for math pros and is difficult
    to approach as beginning math novices, it is very well designed in
    its interface and ease of use. I am drawn to it by integration of
    "literate" approaches to documentation, ability to enter math
    notation, support for SML, and Z too (which is my next goal once
    basic Prop/Pred Calc is under our belts). Overall we should be
    able to derive correct programs and/or prove algorithms.

    My idea is that application of proofs to software design is the
    main goal of a Discrete Math course (recently changed to Discrete
    Structures by the powers that be).  I do recognize the value of
    your time, and will resist asking each time I get stuck unless I
    am unable to continue.
    -Dave


    On Wed, Aug 17, 2016 at 3:02 AM, Rob Arthan <r...@lemma-one.com
    <mailto:r...@lemma-one.com>> wrote:

        David,

        I endorse what Roger said about forward v. backwards proof.
        There is definitely a tension between teaching proof theory
        and teaching practical mechanised proof.

        For the record, the problem was that you had the two theorem
        arguments of ∃_elim the wrong way round and you seemed
        to have misunderstood the role of the term argument: it is
        the variable that is free in the assumption of the second theorem
        that is going to be discharged by the first theorem (the one
        with the existential conclusion). Here is the complete proof
        with the output you should see in the comments.

        val L1 = asm_rule ⌜p(x,y):BOOL⌝;
        (* val L1 = p (x, y) ⊢ p (x, y): THM *)
        val L2 = ⌜∃x:'a⦁p(x,y)⌝;
        (* val L2 = ⌜∃ x⦁ p (x, y)⌝: TERM *)
        val L3 = ∃_intro L2 L1;
        (* val L3 = p (x, y) ⊢ ∃ x⦁ p (x, y): THM *)
        val L4 = ⌜∃y:'b⦁∃x:'a⦁p(x,y)⌝;
        (* val L4 = ⌜∃ y x⦁ p (x, y)⌝: TERM *)
        val L5 = ∃_intro L4 L3;
        (* val L5 = p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
        val L6 = asm_rule ⌜∃y:'b⦁p(x,y)⌝;
        (* val L6 = ∃ y⦁ p (x, y) ⊢ ∃ y⦁ p (x, y): THM *)
        val L7 = ∃_elim ⌜y:'b⌝ L6 L5;
        (* val L7 = ∃ y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
        val L8 = asm_rule ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝;
        (* val L8 = ∃ x y⦁ p (x, y) ⊢ ∃ x y⦁ p (x, y): THM *)
        val L9 = ∃_elim ⌜x:'a⌝ L8 L7;
        (* val L9 = ∃ x y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
        val L10 = ⇒_intro ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝ L9;
        (* val L10 = ⊢ (∃ x y⦁ p (x, y)) ⇒ (∃ y x⦁ p (x, y)): THM *)

        The documentation and the error messages talk about varstructs
        meaning either variables or  things formed from variables
        using pairing
        (like ∃_elim will work on theorems with conclusions like ∃(x,
        y)⦁ p (x, y)).
        You can just read “variable” for “varstruct” in simple examples.

        Regards,

        Rob.

        On 16 Aug 2016, at 21:24, David Topham <dtop...@ohlone.edu
        <mailto:dtop...@ohlone.edu>> wrote:

        Since the slides for this book use slightly different
        notation, I am back to trying to implement the proofs in the
        main book:  UsingZ from
        www.usingz.com <http://www.usingz.com/>  (in text link, it is
        zedbook)

        On page 42, the proof is using nested existentials, and I am
        trying
        to get past my lack of understanding in applying E-elim
        (Roger already helped me with E-intro)

        Here are two of my attempts (using ASCII since I can't attach
        pdf here)
        val L1 = asm_rule %<%p(x,y):BOOL%>%;
        val L2 = %<%%exists%x:'a%spot%p(x,y)%>%;
        val L3 = %exists%_intro L2 L1;
        val L4 = %<%%exists%y:'b%spot%%exists%x:'a%spot%p(x,y)%>%;
        val L5 = %exists%_intro L4 L3;
        val L6 = asm_rule %<%%exists%y:'b%spot%p(x,y)%>%;
        val L7 = %exists%_elim L4 L5 L6;

        val L1 = asm_rule %<%p:BOOL%>%;
        val L2 = %<%%exists%x:'a%spot%p%>%;
        val L3 = %exists%_intro L2 L1;
        val L4 = %<%%exists%y:'b%spot%%exists%x:'a%spot%p%>%;
        val L5 = %exists%_intro L4 L3;
        val L6 = asm_rule %<%%exists%y:'b%spot%p%>%;
        val L7 = %exists%_elim L4 L5 L6;

        The error I get is "does not match the bound varstruct"

        Does anyone have a suggestion to get me past this roadblock?

        -Dave

        On Sun, Aug 14, 2016 at 2:21 AM, Roger Bishop Jones
        <r...@rbjones.com <mailto:r...@rbjones.com>> wrote:


            On 14/08/2016 08:44, David Topham wrote:

                Thanks Roger, I am using slides he distributes.  He
                has false introduction rules starting on page 24
                (attached).
                Sorry about my poor example, please ignore that since
                is a confused use of this technique anyway!  -Dave

            Looks like he changed the name.

            In fact the original name (the one he uses in the book)
            is good in ProofPower.
            ¬_elim is available in ProofPower and does what you want
            (though it is sligftly more general, it proves anything
            from a contradiction so you have to tell it what result
            you are after).
            Details in reference manual.

            Roger


            This message did not originate from Ohlone College and
            must be viewed with caution. Viruses and phishing
            attempts can be transmitted via email.
            E-mail transmission cannot be guaranteed to be secure or
            error-free as information could be intercepted,
            corrupted, lost, destroyed, arrive late or incomplete, or
            contain viruses.

            If you have any concerns, please contact the Ohlone
            College IT Service Desk at itserviced...@ohlone.edu
            <mailto:itserviced...@ohlone.edu> or (510) 659-7333
            <tel:%28510%29%20659-7333>.


        _______________________________________________
        Proofpower mailing list
        Proofpower@lemma-one.com <mailto:Proofpower@lemma-one.com>
        http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
        <http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com>




_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to