Mark,
> On 11 Mar 2016, at 14:06, m...@proof-technologies.com 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
g...@github.com:RobArthan/pp-contrib,
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:
http://lemma-one.com/pipermail/proofpower_lemma-one.com/2016-February/001113.html
<http://lemma-one.com/pipermail/proofpower_lemma-one.com/2016-February/001113.html>
Regards,
Rob.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
