> On 11 Mar 2016, at 14:06, wrote:
> Hi Dave,
> With this rule, the theorems need to precisely match up with how they are 
> described in the manual, so you need to have the conclusion of the 2nd 
> theorem as the logical negation of the LHS of the "or" in the 1st thm (not 
> vice versa).  So just use the double logical negation introduction rule on 
> the 2nd theorem, and then it works.
Quite so. 
> Perhaps using good old ASCII versions of the logical symbols a good idea.  
> This is what the HOL4 and HOL Light use.  So there's:
>   disjunction:  \/
>   conjuntion: /\
>  ...

[Aside: actually HOL4 supports UTF-8-encoded Unicode maths symbols if you throw
the right switches.]

ProofPower now has support for UTF-8-encoded Unicode, but there isn’t any
support for it in xpp yet. There is a program pputf8 that will translate 
ProofPower source
into UTF-8.

You can get pputf8 by taking a clone of the git repository,
navigating to pp-contrib/src/pputf8 and running:

        make -f pputf8.mkf bad

Then copy the programs pputf8 (and utf8pp if you like) to somewhere convenient 
(e.g., $HOME/bin
or the bin directory in your ProofPower installation). pputf8 is a filter, 
i.e., it reads standard input
and writes standard output.

Here is the result of running pputf8 on my recreation of David’s problem and 
Mark’s solution:

val L1 = asm_rule ⌜p:BOOL⌝;
val L2 = asm_rule ⌜p ⇒ q⌝;
val L3 = undisch_rule L2;
val L4 = asm_rule ⌜¬ q ∨ r ⌝;

val L5 = ∨_cancel_rule L4 L3;

(* Above fails with:
Exception Fail * ¬ q ∨ r ⊢ ¬ q ∨ r and p ⇒ q, p ⊢ q are not of the form: `𝛤1 ⊢ 
t1 ∨ t2' and `𝛤2 ⊢ ¬t3' where ⌜t3⌝ is
 𝛼-convertible to ⌜t1⌝ or ⌜t2⌝ [∨_cancel_rule.7050] * raised

val L3' = ¬_¬_intro L3;

val L5 = ∨_cancel_rule L4 L3';

(* Above works giving:
val L5 = ¬ q ∨ r, p ⇒ q, p ⊢ r: THM

If you run pp -d hol in a terminal window and then do:

        set_flag("input_in_utf8", true);
        set_flag("output_in_utf8", true);

you should be able to execute the above commands by copying and pasting them
into the terminal window. Alternatively, you can paste them into utf8pp >XYZ.ML
and then work with XYZ.ML using xpp.

I hope to do more work on UTF-8 presently. See the following post for more info:



Proofpower mailing list

Reply via email to