Roger, Thank you so much! I had not come across rewrite_rule in my reading.
It works exactly as I need.  -Dave

On Tue, Feb 7, 2017 at 5:01 AM, Roger Bishop Jones <> wrote:

> 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 <> 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 <> 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 <> 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
>>>  (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 <>
>>> 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  or (510) 659-7333
>>>> <%28510%29%20659-7333>.
>>> _______________________________________________
>>> Proofpower mailing list
Proofpower mailing list

Reply via email to