Re: [ProofPower] "Unicode" vs. UTF8

[Roger Bishop Jones]

On 07/11/2023 10:09, Makarius wrote:
I first heard of "Unicode" approx. 1990. Everybody was talking about 
"wide charaters" (16bit) and made moves to support them (e.g. major 
Unix vendors and MicroSoft). That was the time of now obsolete UCS16: 
"16bit should be sufficient for everyone, i.e. every imaginable 
character on the planet".
We began working (at ICL) with Cambridge HOL in 1986, using a modified 
version for an important secure hardware verification 88-9 before 
starting the project which first developed ProofPower in 90-93.
The emphasis was on verification of systems specified in Z, and so at 
first we had done small things to make HOL look more like Z, and one of 
those was simply to use the extended character set.

At that time we were on Sun workstations, and Linux didn't exist.
Sun had a font editor, so I just added extra characters in the empty 
spaces in the existing character sets and edited the font myself; things 
were way simpler in those days.


There are of course things we would have used if they had been on our 
radar.  UTF would have been a good idea, and it would have been better 
perhaps to have started out with an open source project, but we were 
scuppered by the commercialisation by Cambridge University of the Poly 
ML system which had been chosen as the best base for ProofPower (before 
that happened).


Roger


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

Re: [ProofPower] Existential Elimination

[Roger Bishop Jones]

David,

Something odd about your message which confuses my mail tool and doesn't 
quote it properly, so this is hand cranked (your text in italics)

/
//What is confusing is the 3 parameters.  e.g. In this partial proof, 
there is only one premise, but you mention 2?


/I'm afraid I'm confused by your question.
When I talked of two premises I presume I was talking of the two 
theorems which are required by ∃_elim, i.e. L1 and L2 in your simpler 
example.

//

/val L1 = asm_rule ⌜∃x⦁W(x)⌝;/
/val L2 = asm_rule ⌜W(b):BOOL⌝;/
/val L3 = ∃_elim ⌜x⌝ L1 L2;/
Good idea to look at the reference manual entry for ∃_elim, which, in 
the version I am looking at, is on page 333.

The first premise must have an existential conclusion.
The second premise must have an assumption which is obtained from that 
conclusion by removing the existential quantifier, but the variable over 
which is quantifies must not be present anywhere else in the second premise.
You can change the name (as you have done) but you must use a name which 
has no other free occurrences in that premise.
In L2 W(b) appears with b free both in the assumptions and in the 
conclusion, so the rule will fail to eliminate W(b) from the assumptions.


Apart from the one assumption matching the existential premise which is 
supposed to be remove (but wasn't in this case), all the assumptions in 
the two premises appear in the conclusion.

So that's why /∃x⦁W(x)⌝ /appears in the assumptions of your conclusion.

A better explanation of what /∃_elim/ is doing has now occurred to me.
The turnstile in HOL is purely truth functional,
so you may think of A1, A2..., An ⊢ C as being similar to A1 ∧ A2 ... An ⇒ C
and we know that P is provable iff ∀x⦁P x//is provable./
/So A1, P x..., An ⊢ C is provable iff ∀x⦁A1 ∧ P x ... An ⇒ C is provable
and if x appears free nowhere else we can push in the universal to:
A1 ∧ (∃x⦁P x) ... An ⇒ C

i.e. a conjecture with an assumption with a unique free variable is provable
iff the conjecture with that assumption existentially quantified is 
provable.
This is reflected in the effect of stripping an existential into the 
assumptions

in a goal oriented proof, which results in the existential being dropped.

I say all this just to explain the naming of /∃_elim//.
/The existential eliminated by the rule is not an explicit existential
but rather what we might call an implicit existential in the assumptions
of the second premise, which is eliminated using a theorem (the first
premise) which has that existential as its conclusion.
If that existential is proven using certain assumptions, then of course
those assumptions must appear on the resulting theorem.
If the existential in the first premise does not match an assumption
in the second in which the existentially quatified variable is replaced by
a unique free variable, then the rule will not fail, but it will not 
eliminate

any assumption, and you will still get the extra assumptions added.
This is what happened in your simpler example.

good luck,
Roger
//

/

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

Re: [ProofPower] ∃_elim

[Roger Bishop Jones]

David,

The existential rule most closely analogous to universal instantiation 
is existential introduction.

The ∃_elim rule is more complex, and the name perhaps misleading.
The conclusion is always exactly the conclusion of the second premise.
The existential "eliminated" is the conclusion of the first premise.
But its probably clearer to think of the first premise being used to 
eliminate an assumption in the second premise which is a witness to the 
existential in the first premise.


In your proof, the effect realised is to introduce an existential in the 
assumptions (in both cases).


Roger


On 31/03/2020 17:10, David Topham wrote:
I was restudying this proof suggested by Rob a few years ago and still 
have a nagging question I am trying to resolve:

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 *)
I know when we do Universal elimination the quantifier is no longer 
there, but here for Existential elimination the quantifier remains.  
Is there a reason for that?

e.g.
Why is
val L7 = ∃_elim ⌜y:'b⌝ L6 L5;
(* val L7 = ∃ y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
not
val L7 = ∃_elim ⌜y:'b⌝ L6 L5;
(* val L7 = ∃ y⦁ p (x, y) ⊢ p (x, y): THM *)
Aren't we selecting y to be witness or example of a y that satisfies p?
Like
(∃y)Py Py ∃_elimNeed to make assumption based on the existentially quantified 
proposition

___
Proofpower mailing list
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

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

[Roger Bishop Jones]

On 04/11/2019 02:01, David Topham wrote:
Those two don't seem to get along!  Probably my error and sorry to be 
burdening you with debugging due to partial understanding on my part.



you need ⌜sum (pow r)⌝ and now you are in the reals, / instead of Div, so:

⌜λ n⦁ ∀ r⦁ sum (pow r) n = 1.0 - pow r (n + 1) / (1.0 - r)⌝;
Roger
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

[Roger Bishop Jones]

David,

Good to see you are making some progress.

For the examples in 9.2 you best course is probably to have a power 
function with type:


    ℝ→ℕ→ℝ

ⓈHOLCONST
│ pow:ℝ→ℕ→ℝ
├──
│ ∀b e⦁ (pow b 0) = 1. ∧
│       (pow b (e + 1)) = b * (pow b e)
■

This will fit with Rob's suggestion for modelling sequences:

    Sequences are modeled as functions ℕ → ℝ.

Which allows you to use mathematical induction over ℕ for reasoning 
about ℝ valued sequences. Roger





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

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

[Roger Bishop Jones]

On 02/11/2019 19:10, Rob Arthan wrote:

If I need to work with the rationals I just treat
them as a subset of the reals.
Though I think for these examples even that is an unnecessary 
complication, since the proof over the reals as a whole will be closest 
(apart from the actual types) to what a proof for the rationals would 
look like.

And the original seems ambiguous about types.

Roger

PS: my 0 < r < 1 suggestion seems unnecessary.

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

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

[Roger Bishop Jones]

David,

Thanks for the reference to the text you are working from, it makes it 
much clearer what you are trying to do.


In example 9.2 I think he should stipulate 0 < r < 1 not just r not= 1.

I think strictly speaking if you work with real numbers you are not 
doing discrete maths, but I don't know how much that matters to you.
( /"Discrete mathematics/is the study of/mathematical/structures that 
are countable or otherwise distinct and separable."

This seems the most popular definition.)

However, the examples in 9.2 don't require real numbers, since he is 
only dealing with finite sums, not taking limits, so the numbers here 
could be the rational numbers ℚ, and the induction is over the natural 
numbers.
How about working in theory "ℚ"? (that's still discrete by the above 
criterion).


As to utf8, it is likely that the next release of ProofPower will work 
with utf8, and in the interim there is a ProofPower contrib which 
contains programs for converting between ProofPower ext character set 
and utf8.


I can't see anywhere that pputf8 can be downloaded, so you might have to 
clone the github depository at:


https://github.com/RobArthan/pp-contrib

Then look for build instructions in src/pputf8.

Alternatively, look here for Rob's previous advice:

http://lemma-one.com/pipermail/proofpower_lemma-one.com/2016-August/002345.html

Roger

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

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

[Roger Bishop Jones]

David

The ascii may not be readable, but it can be converted back to ext, or 
to utf8:


ⓈHOLCONST
│ sum:ℕ→ℕ
├──
│ ∀n⦁ sum 0 = 0 ∧ sum (n) = n + (sum n-1)
■
ⓈHOLCONST
│ pow:ℕ→ℕ→ℕ
├──
│ ∀b e⦁ (pow b 0) = 1 ∧ (pow b e) = b * (pow b (e - 1))
■
=SML
val ex92 = ⌜λ n r⦁ sum (pow r n) = (1 - (pow r (n - 1)) Div (1 - r))⌝;
val UI = ∀_elim ex92 induction_thm;
val lemma1 = rewrite_rule [] UI;

putting in utf8 would be better, but you probably wouldn't find that easy.
(the next release of ProofPower will make it easier)

To understand why your definitions don't work, consider what they say 
when you instantiate n or e to 0.

You get conflicting and nonsensical assertions about sum 0 and pow b 0.
When you use similar definitions in SML its OK because execution is 
sequential and the second reading is never reached (for the zero 
argument), but in logic you can reach the second clause and you can 
derive a contradiction.


Also, it is now clear (even though you don't actually state your goal), 
that you are trying to reason about the sum of a segment of series, but 
the function "sum" you have (almost) defined gives the sum of an initial 
segment of the natural numbers, not of an arbitrary series.

The "sum" you want takes a function as well as a number, so it has type:

sum:(ℕ→ℕ) → ℕ → ℕ

When it comes to doing induction, apart from the need to chose the 
proposition carefully which I mentioned earlier, you obtain the required 
property by eliminating only the outermost universal, so you would have:


val ex92 = ⌜λ n⦁  ∀r⦁ sum (pow r n) = (1 - (pow r (n - 1)) Div (1 - r))⌝;

Then you would have a term of the right type to instantiate induction thm.

Roger





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

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

[Roger Bishop Jones]

David,

I missed a pair of brackets in my last.

Should be:

ⓈHOLCONST
│    tri : ℕ → ℕ
├──
│    ∀n⦁    tri 0 = 0
│    ∧    tri (n+1) = (tri n)+n+1
■

⌜∀n⦁ tri n = (n*(n+1)) Div 2⌝;

val tri_p = ⌜λn⦁ tri n = (n*(n+1)) Div 2⌝;

∀_elim tri_p induction_thm;

val lemma1 = rewrite_rule [] it;

and of course, rewriting with the definition of "tri" helps:

val lemma2 = rewrite_rule [get_spec ⌜tri⌝] lemma1;

giving:

val lemma2 =
   ⊢ 0 = 0 Div 2
 ∧ (∀ m
 ⦁ tri m = (m * (m + 1)) Div 2
 ⇒ tri m + m + 1 = ((m + 1) * ((m + 1) + 1)) Div 2)
   ⇒ (∀ n⦁ tri n = (n * (n + 1)) Div 2): THM

and then you need to do some arithmetic!

Roger


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

Re: [ProofPower] ProofPower and Discrete Math

[Roger Bishop Jones]

David,

On 28/10/2019 02:39, David Topham wrote:
Hello Rob,Roger, et al. Hope you are doing well. I am still trying to 
apply ProofPower to forward proofs.

Glad to hear that.

I am working on proof by induction and came across this:

induction_thm

In the notes, there is an intriguing statement that we could use 
"forall_elim" to do forward proofs using the thm, but no specific example.


e.g. I would like to show the sum of the integers from 1...n = n(n+1)/2

but not sure how to notate the "infinite sequence" or to
remove the implied "forall" using
rewrite_rule (or prove_rule)

Do you have a sample of that technique somewhere?

There are not so many examples in general of forward proof methods, 
because in practice it is usually easier and faster to use the goal 
package to obtain proofs, even though an understanding of forward proof 
is pretty essential and bits of forward proof are often handy within a 
larger goal-oriented proof or when programming new proof automation.


So I'm not able to point you to an example of forward induction.

However, I can give you some clues about how to go about it.

There are examples of backwards inductive proofs in the HOL Tutorial 
Notes, which it would be worthwhile you looking at first.
You could look at those proofs and ask "how would I do this as a forward 
proof?"
They have the advantage that they are about concepts which are already 
defined in the theory of list, particularly concatenation of lists.


Typically inductive proofs involve inductively defined concepts or 
functions.
The one you want to prove is about natural numbers (which are 
inductively defined) and the function "sum of the numbers up to n" (you 
don't need to do anything with /infinite/ sequences) which needs to be 
defined inductively, but has not been defined in the theory of natural 
numbers.
So to address that inductive proof, you must first master inductive 
definitions, and define the sum of a finite sequence.
There are examples of inductive definitions, for example plus_def and 
times_def, in the HOL theories.
Then you need to identify the property of natural numbers which you are 
trying to show, by induction, is true of all natural numbers.
This is the thing with which you must instantiate induction_thm using 
forall_elim.


Do you think you could define the summation op you need to get to a 
formal statement of the theorem you wish to prove, and then use this in 
formally stating the property you want to prove of all numbers?


Roger

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

Re: [ProofPower] ProofPower and Discrete Math

[Roger Bishop Jones]

> David,

Good to hear you are still moving forward.

If the transformation you seek is a propositional tautology, the following 
general prescription should work.

1. Formulate the transformation as an equivalence using propositional (Boolean) 
variables, with the starting point on the left of the equivalence and the 
desired form on the right, and universally quantify the equivalence over all 
the Boolean variables.

2. Prove this sentence using “prove_rule[]”.

3. Use rewrite_rule with the resulting theorem to effect the transformation in 
a forward proof.

I’m not in a position to check any specific examples at the moment, but if you 
have any difficulties I will be better placed later in the week.

Roger Jones

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

Re: [ProofPower] Font for SML

[Roger Bishop Jones]

David,

Looks like one problem for you is the way you are processing the latex 
files.


There is a ProofPower manual, USR001, called:ProofPower - Document 
Preparation 
which tells you how to process ProofPower files for printing (or to .dvi 
files).
Rather than converting to .tex and then running latex on the tex file, 
you should be
using docdvi, which will extract the .tex file and run it through LaTeX 
for you.


I could not check this out for you because I was still short of a style 
file pstricks.sty
so I can't be sure that would work for your document, but you should try 
it yourself

and see how it goes.

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

Re: [ProofPower] file conversion

[Roger Bishop Jones]

Thanks for the help with UTF8 Rob.

That went through without hitch for me, apart from my discovering that 
my OS X ProofPower installation didn't work properly.
It turned out that on OS X, as on Ubuntu 16.04, I needed to put in a 
softlink to app-defaults in my home directory.


Roger Jones

On 18/08/2016 21:15, Rob Arthan wrote:

Roger,


On 17 Aug 2016, at 11:41, Roger Bishop Jones <r...@rbjones.com> wrote:

Rob,

It would be helpful for intelligible email discussions about ProofPower if you 
could tell us all the slickest way to get a proofpower script into a form in 
which it can be pasted into an email (UTF8 presumably), and vice-versa.

I hope this will be quite a bit slicker in the not too distant future.
For now, you need to build the pputf8 and utf8pp programs,
which you can do by cloning the pp-contrib git repo at:

https://github.com/RobArthan/pp-contrib

Then navigate to pp-contrib/src/pputf8 and do:

make -f pputf8.mkf bld

Now (unless you want to type the  full path names when you run the programs)
copy the pputf8 and utf8pp executables to some convenient
directory on your PATH, e.g., $HOME/bin or /usr/local/pp/bin.

pputf8 and utf8pp are filters (programs that read standard input and
write standard output) and convert from the ProofPower encoding
to UTF-8 and vice versa.

To get some UTF-8 to include in an e-mail, copy the ProofPower
text into a file, say mystuff-pp.txt, and do

pputtf8 < mystuff-pp.txt > mystuff-utf8.txt

and then use a text editor on mystuff-utf8.txt to copy-and-paste
your stuff, now encoded as UTF-8, into an e-mail.

On Mac OS, there is a handy program called pbcopy that lets
you bypass the text editor step:

pputf8 < mystyff-pp.txt | pbcopy

will put the UTF-8 onto the Mac OS pasteboard directly.
I think there are Linux/Cygwin equivalents for pbcopy
(xclip?) but I don't have any experience with them.

To extract ProofPower encoded stuff from a UTF-8
encoded snippet in an e-mail, copy the snippet into
a text editor, save it, and then use utf8pp to get
the ProofPower encoding. Again, you could use
pbpaste or Linux/Cygwin equivalent to bypass
the text editor step.

Regards,

Rob.








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

Re: [ProofPower] ProofPower and Discrete Math

[Roger Bishop Jones]

David,

There is a reason why the ProofPower tutorials don't say much about the 
forward proof tools you are trying to use.
I have given courses on ProofPower HOL and on ProofPower Z and wrote the 
tutorials.
What I did in the courses was to teach just enough about forward proof 
for the students to understand the basics of how proof in ProofPower 
works, before teaching them how to use the goal package to accomplish 
proofs.
Goal oriented proof is much easier in virtually all applications (though 
it does often involve small fragments of forward proof).
Compared with using the goal package, contruction of forward proofs is 
like pulling teeth.


The example given by Woodcock on page 42 can be proven using the goal 
package by the following script:


set_goal([], %<%(%exists%x:'a%spot% %exists%y:'b%spot% P(x,y)) ´ 
(%exists%y:'b%spot% %exists%x:'a%spot% P(x,y))%>%);

a (REPEAT strip_tac);
a (%exists%_tac %<%y%>% THEN %exists%_tac %<%x%>% THEN strip_tac);

or just (not quite so easy to understand):

a (contr_tac THEN asm_fc_tac[]);

or even:

a (prove_tac[]);

(in a reasonable proof context such as "hol")

You might consider pointing your students to the Woodcock forward proof 
and then showing them a ProofPower goal oriented proof, then they will 
be learning a more intelligible and economic method of proof.


I could look closely at how to do this by forward proof and debug your 
attempts, but I have never myself had occasion to do this kind of 
forward proof, its not a necessary skill.
Of course, the forward proof facilities are used, but in rather 
different ways, by the people who programmed the goal package, and by 
people writing higher level proof facilities such as tactics, tacticals 
etc., but for applications, the goal package makes things simpler both 
to understand and to execute.


By way of further comment on why your proofs are not working, the term 
required as a parameter to exists elim is one which matches just the 
variable over which the existential quantifies, and so not a predicate.
It will only work one quantifier at a time (and %exists% x y %spot% is 
two nested quantifiers), so you would have to do the proof in two stages 
one for each of the quantified variables, unless you put them together 
in the theorem as in %exists% (x,y) %spot%, which of course, is not 
quite the same theorem.

So it really is a lot more complicated to do this by forward proof.

Roger


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

Re: [ProofPower] ProofPower and Discrete Math

[Roger Bishop Jones]

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

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

Re: [ProofPower] ProofPower on Ubuntu 16.04

[Roger Bishop Jones]

Thanks Rob for sorting this out for me.
I now have ProofPower running on Ubuntu 16.04 (under VirtualBox on my 
macbook).
(also under OS X, but I have other things which I can't get to work on 
OS X).
16.04 works on the 12" macbook under VirtualBox but not native, though 
it will boot from a flash drive but doesn't then understand the keyboard 
or touchpad.


The install prescription should probably be:

libmotif-dev
polyml
libpolyml-dev
texlive-generic-recommended

but I already had texlive-full installed so I can't confirm that 
texlive-generic-recommended suffices.

Roger

On 22/07/2016 12:30, Rob Arthan wrote:

Roger,

I have now had time to build ProofPower on ubuntu 16.04. I needed to do the 
following:

1) Install the following packages:

libmotif-dev
poly
libpoly-dev
texlive-recommended

2) Change configure so that it doesn’t fail if libpolymain is in a subdirectory 
of /usr/lib (see below)

3) Change src/xpp/xpp.mkf so that it doesn’t use -lXext or -lXp (see below)

4) Copy the app-defaults directory to my home directory (xpp wouldn’t use the 
fonts otherwise)

For (2) and (3) I’ve attached a patch. If you build poly yourself, rather than 
install the package you
might not need to do (2), but the patch does not harm.

Regards,

Rob.





On 21 Jul 2016, at 11:15, Rob Arthan <r...@lemma-one.com> wrote:

Roger,


On 18 Jul 2016, at 22:15, Roger Bishop Jones <r...@rbjones.com> wrote:

I have been trying to install ProofPower on Ubuntu 16.04, without success.

The stumbling block comes early, in the prerequisites for installing OpenMotif, 
since some of these are not available in the usual repositories.

Do you need any more than libmotif-dev?  I have a kubuntu 16.04 VM but 
unfortunately it’s not convenient for me to install all the prerequisites for 
ProofPower on it just now. However, I installed libmotif-dev and was able to 
build a simple motif programme and I can’t see any reason why xpp would need 
anything more.


If anyone figures out how to get ProofPower installed on Ubuntu 16.04 I should 
be pleased to know how it can be done.

I’ll try a full installation on kubuntu 16.04 when I get a moment.

Regards,

Rob.
___
Proofpower mailing list
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

[ProofPower] Installing ProofPower on OS X El Capitain

[Roger Bishop Jones]

Here is my reconstruction of the method I used to get ProofPower running 
on OS X 10.11.4, which is an adaptation of a recipe posted by Rob for an 
earlier version of OS X.


From the App Store install Xcode.

The rest of the process is done on the command line, so you either need 
to use terminal or you can use emacs (once installed).


Install Xcode command line executables by:

xcode-select --install
(and select "install" when prompted)

install XQuartz from XQuartz.org
install macports from macports.org

You need in your PATH /opt/local/bin:/opt/local/sbin
The MacPorts installation edits your .profile to make that happen, which 
has the desired effect if you are using Terminal.
If you are using emacs it doesn't (not with the out-of-the-box emacs), 
but if you copy .profile to .emacs_bash that does it).


To install openmotif you have to re-install xorg-libnXt because it needs 
the flat_namespace option.


sudo port install xorg-libXt +flat_namespace

sudo port install openmotif
sudo port install polyml
sudo port install texlive

Get ProoPower from Lemma-one.com and unpack tarball.

In the main directory of the unpacked ProofPower distribution:

PPPOLYLINKFLAGS=" " ./configure
./install

(you may wish to read the README file and set other environment vatiables)

and Bob's your uncle.


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

Re: [ProofPower] ProofPower build on OS X

[Roger Bishop Jones]

Magic.

Build complete.
I just had to change the path.

xpp seems to come up ok.

Thanks, I’ll post a resume.
Roger
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower build on OS X

[Roger Bishop Jones]

Rob,

Now failing to find mkfontdir.

PATH=/opt/local/bin:/opt/local/sbin:/usr/bin:/bin:/usr/sbin:/sbin:/Applications/Emacs.app/Contents/MacOS/bin-x86_64-10_9:/Applications/Emacs.app/Contents/MacOS/libexec-x86_64-10_9

Am I missing something from the PATH or do I need to install something else?

Roger


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

Re: [ProofPower] ProofPower build on OS X

[Roger Bishop Jones]

Rob,

Thanks for you continuing support.

> On 30 Apr 2016, at 10:16, Rob Arthan  wrote:
> 
> 

...

> Try it in in src/dev. I think it will fail. If so, try it without the 
> obsolete options:
> 
>   polyc -o pp-ml pp-ml.o
> 

Here are the results:

bash-3.2$ polyc -segprot POLY rwx rwx -o pp-ml pp-ml.o
Only one source file name allowed
Usage: polyc [OPTION]... [SOURCEFILE]
bash-3.2$ polyc -o pp-ml pp-ml.o
ld: warning: could not create compact unwind for _ffi_call_unix64: does not use 
RBP or RSP based frame

So I need to build my own?

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

[ProofPower] ProofPower build on OS X

[Roger Bishop Jones]

Rob,

OK, so now I am through to the ProofPower build, which fails pretty fast, just 
after compiling dtd108.

Here’s the tail of the log:

rm -f hol.polydb
Compiling dtd108.sml and imp108.sml
{   { echo "val system_version : string = \"3.1w7\"; val build_date : 
Date.date = Date.fromTimeLocal(Time.now()); use\"dtd108.sml\"; 
use\"imp108.sml\";" | poly ; } && { polyc -segprot POLY rwx rwx -o pp-ml 
pp-ml.o || LD_RUN_PATH=/opt/local/lib c++ -segprot POLY rwx rwx -o pp-ml 
pp-ml.o -L/opt/local/lib -lpolymain -lpolyml ; } && { echo "PPBuild.pp'save 
();" | pp-ml ; } } > dtd108.ldd0
ld: warning: could not create compact unwind for _ffi_call_unix64: does not use 
RBP or RSP based frame
Undefined symbols for architecture x86_64:
  "___gmpn_add_n", referenced from:
  add_unsigned_long(TaskData*, SaveVecEntry*, SaveVecEntry*, int) in 
libpolyml.a(arb.o)
  "___gmpn_gcd", referenced from:
  gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*) in 
libpolyml.a(arb.o)
  "___gmpn_gcd_1", referenced from:
  gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*) in 
libpolyml.a(arb.o)
  "___gmpn_lshift", referenced from:
  gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*) in 
libpolyml.a(arb.o)
  "___gmpn_mul", referenced from:
  mult_longc(TaskData*, SaveVecEntry*, SaveVecEntry*) in libpolyml.a(arb.o)
  "___gmpn_rshift", referenced from:
  gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*) in 
libpolyml.a(arb.o)
  "___gmpn_sub_n", referenced from:
  sub_unsigned_long(TaskData*, SaveVecEntry*, SaveVecEntry*, int) in 
libpolyml.a(arb.o)
  "___gmpn_tdiv_qr", referenced from:
  quotRem(TaskData*, SaveVecEntry*, SaveVecEntry*, SaveVecEntry*&, 
SaveVecEntry*&) in libpolyml.a(arb.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make: *** [hol.ldd] Error 1

Any idea what the problem is here?

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

Re: [ProofPower] tactic in backward reasoning for rewrite rules with conditions

[Roger Bishop Jones]

On 28/09/15 11:05, Lin, Yuhui wrote:
> Thank you very much. Your solution works perfectly for me. Just be a little 
> curious, what dose the following promoted message means when applying the 
> tactic
>
>   'Tactics proof introduced the subgoal 2 but did not request it as a 
> subgoal"
>
>
That's because the tactic doesn't really work properly, and the goal
package had
to intervene to patch up the proof.
I mentioned in my description of a suggested method that if a conversion
produces
an equation with extra assumptions, then if you use it as a tactic those
assumptions
will get subgoaled.
This is true, and it works, but the tactic is not really doing what it
should and the
subgoal package is fixing the problem,

I thought that was a bit off, and also I wasn't sure that the subgoal
created by
the goal package would always have the right assumptions so I did it
properly,
and include the result, for the record, below,

Its still very crude, some of the choices are arbitrary and not thought out
(like the parameters to prim_rewrite_conv, also the canon could do more)
But it does what was asked for.

(I did it in theory real because there was a nice conditional equation
available there for testing it, it doesn't really need to be there)

Roger


open_theory "%bbR%";

fun thm_eqn_cxt1 (thm : THM) : TERM * CONV = (
letval cnv = simple_eq_match_conv thm
val lhs = fst(dest_eq(snd(strip_%forall% (concl thm;
in
(lhs, cnv)
end);

fun cond_rewrite_canon thm = [strip_%implies%_rule (all_%forall%_elim thm)];

val cond_rewrite_conv = prim_rewrite_conv
empty_net
cond_rewrite_canon
(Value thm_eqn_cxt1)
MAP_C
[];

cond_rewrite_conv [%bbR%_over_times_over_thm] %<%2./3.*4./5.%>%;

fun cond_rewrite_tac thm (asml, conc) =
let val thm2 = cond_rewrite_conv [thm] conc
in  MAP_EVERY (fn p => (LEMMA_T p
(fn q => MAP_EVERY asm_tac (forward_chain_rule [thm] [q]
(asms thm2)
(asml, conc)
end;

set_goal ([%<%H1:BOOL%>%, %<%H2:BOOL%>%], %<%2./3.*4./5. = 0.%>%);
a(cond_rewrite_tac %bbR%_over_times_over_thm);


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

Re: [ProofPower] tactic in backward reasoning for rewrite rules with conditions

[Roger Bishop Jones]

Further to my last on this topic, I now see that simple_eq_match_conv
already does what is needed for the solution of the first approximation
to the requirement.

If you take a theorem of the form:

forall x, y. P(x,y) ==> A(x,y) = B(x,y)


and infer:

P(x,y) |- A(x,y) = B(x,y)

then supply this to simple_eq_match_conv you get
a conversion which will rewrite using the equation
and instantiate the assumption P(x,y) appropriately.
If you use that in a tactic the assumptions will get
subgoaled.

If you have a conversion which does that you can
apply it to get the relevant conditions (Ps), use that
to infer the corresponding equations (A=Bs) and add them
into the assumptions.
i.e. you get instances of:

P(x,y) |- A(x,y) = B(x,y)

which you asm_tac causing the equations to go into the
assumptions and the conditions to be subgoaled.

That's reasonably simple!

Probably not very intelligible, but I can fill out the details if necessary.

Roger


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

[ProofPower] Hard copy manuals

[Roger Bishop Jones]

From version 3.1w6 most of the ProofPower manuals are available
as paperback books from amazon websites.

A search on a US or European amazon website for ProofPower Manuals
brings them up, or you can use the links provided at the top of the
ProofPower documentation page which is created when version
3.1w6 is installed.

They are reasonably priced, prices range from £2.75($4.30) for
ProofPower Description (64 pages) to £15 ($18) for ProofPower Z
Reference Manual (674 pages, free delivery in UK).
The interiors of the manuals are exactly the same as the PDFs
issued with v3.1w6  of ProofPower except for some resizing
to fit in the available trim sizes.

Roger Jones



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

Re: [ProofPower] apply conditional rewriting

[Roger Bishop Jones]

On 04/06/15 10:30, YuHui Lin wrote:
 Hi,

 How can I apply a conditional rewrite rule in proof power. For example, 
 applying the following thm:

 forall x,y, z | x  y  dot  x - y  + z = x + z -y

 where  x  y is the condition, to generate the following two subgoals:
 1) x  y
 2) goal [x - y  + z / x + z -y]

There is no comprehensive support for conditional rewriting in ProofPower.
but the simpler cases can be accomplished by forward chaining on the
assumptions and rewriting with the result.

In this case you can use lemma_tac to get two goals then
forward chain using your conditional equation and rewrite
with the result, e.g. FC_T rewrite_tac [conditional_equation].

There is some help in describing the available rewriting
and forward chaining facilities in the HOL Tutorial chapter 7,
and all the facilities can be found in the reference manual
by looking for fc or rewrite in the KWIC index.


 Also, I wonder is there any interface of this mail list for searching, so 
 that i can find possible solutions from previous questions of the mail list 
 achieve ?x - y  + z = x + z -y

Mailman doesn't provide for search.

You can search using google by including:

site:lemma-one.com

in your search expression.

Roger Jones

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

Re: [ProofPower] Compiling OpenProofPower-2.9.1w5 under Ubuntu 12.04 (64bit)

[Roger Bishop Jones]

On 09/05/13 23:03, Piotr Trojanek wrote:

Thank you for your reply. I have groff installed, so this is not the reason.

As far as I understand, the build workflow is .doc-.sml-.err. With
my experience in SML I can only attach the files with indication of
the problem and kindly ask for your assistance.

The version of Poly/ML, as given by 'poly -v' is
Poly/ML 5.2 ReleaseRTS version: X86_64-5.2.1


Sorry, I should have spotted this first time.

You need PolyML 5.3 or later.
You might as well use 5.4 that worked for me on Ubuntu 12.04.

Since that version isn't available on the Ubuntu repository
you will need to download the tarfile (from PolyML.org)
and build it yourself.

Roger Jones

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

Re: [ProofPower] Compiling OpenProofPower-2.9.1w5 under Ubuntu 12.04 (64bit)

[Roger Bishop Jones]

Further to my last, this is what I did before building on Ubuntu 12.04

sudo apt-get install texlive-latex-extra texlive-fonts-extra
sudo apt-get install libXp-dev libXext-dev \
 libXmu-dev libXt-dev \
 libxft-dev libjpeg-dev libpng12-dev
sudo apt-get install libmotif4 libmotif-dev libmotif4-dbg
sudo apt-get install splint groff
sudo apt-get install autoconf
sudo apt-get install g++

You don't need all that for PolyML and ProofPower (probably not the
texlive extra stuff, but that's probably the only large item you don't 
need).

Sorry I can't be more definite, I found it hard to figure out what I
needed for PolyML, the configure script tells you a lot about what is there
and what isn't but its not so clear which items are actually necessary.

Roger Jones


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

Re: [ProofPower] Compiling OpenProofPower-2.9.1w5 under Ubuntu 12.04 (64bit)

[Roger Bishop Jones]

On 09/05/13 15:16, Piotr Trojanek wrote:

Dear ProofPower experts,

I triy to install the latest OpenProofPower under Ubuntu 12.04, but it
fails with the (somewhat cryptic) tail of build.log:

docsml -f hol.svf imp001
Compiling (code) imp001.sml
make[1]: *** [imp001.ldd] Error 1

My setup details: polyml, libpolyml1, libpolyml-dev from the standard
Ubuntu repository (5.2.1-1). GCC 4.7.3 (ppa:ubuntu-toolchain-r/test).

Any advice?


You need also to install groff, that might be your problem.

To get more info on the cause of the failure you should look
at the file imp001.err.

Roger Jones

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

Re: [ProofPower] directory path

[Roger Bishop Jones]

Sarah,

The reason why you had problems after setting the PATH variable to point 
to the ProofPower binary directory is because you set it to include only 
that one directory, so xpp was found, but lots of other necessary 
binaries were no longer in the search path.


As recommended by Phil, the correct procedure is to add the ProofPower 
directory into the default PATH value so that all the original 
directories remain.

This is what Phil recommended:

PATH=/home/sarah/pp/bin:$PATH

in which the original value of the $PATH variable is included in the new 
value.


This is very basic linux stuff, if possible you should find someone 
local to help you with this kind of thing until you get better 
acquainted with how to use linux, since resolving problems at this level 
through the ProofPower list will be very slow and tortuous.


Roger



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

Re: [ProofPower] (no subject)

[Roger Bishop Jones]

On 19/02/13 00:55, Phil Clayton wrote:



Easy - by doing exactly that before you run xpp, e.g.

  PATH=/home/sarah/pp/bin:$PATH

Put this in

  /home/sarah/.bash_profile

to have this done automatically when you log in.  (That's for Fedora, 
at leats.  For other Linux distributions, it may go elsewhere e.g. 
.bashrc - I don't know.)

I think Sarah said she was on ubuntu 12.10.

According to the bash manual page, .bash_profile is run when you start a 
login shell and .bashrc is run on any bash shell.


I always used to put things like this in bash_profile and this seemed to 
work OK for shell scripts started in emacs until I upgraded from ubuntu 
10.02 to 12.02 and then it stopped working.


Then I decided to use .bash_aliases and made sure that .bashrc loads 
bash_aliases (I can't remember if it came that way now).


Roger

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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

Jon,

Your file does not show what you were trying to do with 
LEMMA_T, or what you actually did, so its hard to offer much 
help.

lemma_tac is easier to understand that LEMMA_T, so you 
could try doing it with lemma_tac first.
(you can always collapse it down to an application of 
LEMMA_T once you have succeeded in proving the lemma using 
lemma_tac).

Roger

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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

Jon,

I should have mentioned that the problem goal you are 
looking at can be solved by linear arithmetic so you don't 
need any lemma at all.
Linear arithmetic is not covered by the tutorlal but this is 
one way to prove the goal:

a (PC_T1 z_lin_arith asm_prove_tac[]);

Roger

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

[ProofPower] Recursion theorems without constructors

[Roger Bishop Jones]

I make quite a lot of use of recursion theorems to enable 
various kinds of recursive definitions to be proven 
consistent automatically.

The facilities provided in ProofPower are designed to 
support recursive definitions over recursive datatypes, in 
which every element of the type is obtained using some 
constructor and functions are defined using pattern matching.

Because I work in set theory (in HOL) there are recursion 
principles I use for defining functions over arbitrary sets 
not obtained using any constructor.
If I produce a corresponding recursion theorem, in the 
required format except for the lack of a constructor, this 
is accepted by the system (by add_%exists%_cd_thms, and by 
evaluate_%exists%_cd_thm) without complaint, but the 
consistency proofs for corresponding  recursive definitions 
don't happen.
This can be fixed by putting in a fake constructor, CombI 
will do, so the definitions then go though so long as you put 
CombI in the definition.

I'm curious to know whether this is the intended behaviour 
(I don't remember anything about this at the time it was 
being implemented) and if there is any obvious way I can 
avoid having to put CombI in my recursive definitions.

Roger Jones

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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

On Thursday 18 Oct 2012 21:14, Jon Lockhart wrote:

 After fixing the correction you pointed out, I was able
 to get the existance proofs completed and I removed the
 precondition proofs for those init operations. You can
 see this in the attached specification file.

You are now using after states for initial conditions, so an 
existential is the best way to express the consistency of 
these conditions.

However, you are including extra undecorated components in 
some of the initial state schemas, and I am not aware of a 
precedent for this.
Its not clear what this is intended to mean.
I suspect that these names might possibly be better as 
global variables than as local to the initial state schemas, 
but it depends what you are intending to say here.

 Now this
 brings up a previous question again, along with a new
 one. 1) Is it necessary to have the precondtion proofs
 with the exsistance proofs in the specification? If not
 necessary is it wise to use both, or are both redundant
 in terms of what they are showing and not necessary?

Not necessary for the initial state.

 2)
 I am now on to the first main operation of the
 specification, and I have a precondition proof outlined,
 albeit some changes are required of it, to begin proving
 properties of said operation. Should I stick with the
 precondition proof for this and the other opertations or
 is there another proof I should be using? What other
 proofs just on the operations should I be looking to
 use?

Precondition proofs are simply a consistency check.
They tell you when the operations have a result.

I have already made some suggestions about what other kinds 
of thing you might want to prove.

Generally proofs may be used either to validate your 
specification (ideally against some other more abstract 
specification), or to validate code against the specification, 
or to validate refinement steps which add more detail or move 
the spec closer to the code.
Which of these you do is up to you or to you customers.

Roger







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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

Jon,

On Tuesday 16 Oct 2012 01:12, Jon Lockhart wrote:

 I guess I didn't quite understand or comprehend properly
 the second point you were trying to make. I inserted an
 existance proof like I had done for the state schemas
 and I unfortunately get a very interesting goal after
 the rewrite, as seen in the error zip attached.

The point I was making was very elementary, so you probably 
already understood it.
I didn't have a specific issue to address and you had already 
made a mistake in choice of witness so I thought I would 
start there.

Your present example illustrates what happens when you 
rewrite with the definition of a schema.
The first thing that happens is that the schema name is 
replaced by the horizontal schema corresponding to the 
definition.
Often the context allows this to be eliminated, typically in 
favour of the predicate obtained from the declaration and 
body parts of the schema, but in some cases as in the 
declaration part of your existential, this is not possible.

It is better when you have an existential goal to supply a 
witness before you rewrite.
When you supply the witness the declaration part disappears 
and the witness is asserted to belong to the schema. In this 
context when you rewrite with the schema definition it is 
possible to eliminate the horizontal schema.

It is not essential to supply the witness first, but if you 
don't you are likely to see these unfamiliar expressions in 
which horizontal schemas are used.

I see that you are using operations for initial conditions 
rather than following either Spivey or Woodcock with a 
before or an after state respectively.
(I don't know a reason why not, except that you are more 
likely to get comments along the lines that's not how you 
specify initial conditions).

 This
 makes me wonder if it would be better to attempt to use
 the precondition proof code found underneath the start
 of the existance proof for trying to prove properties
 about the init operations, and then further of course
 into the system opertaions.

If you are using an operation to specify the initial 
conditions, then the consistency of your initial conditions 
is equivalent to the assertionj that the precondition of the 
operation is the before state, in this case

pre Button_Init = Button_State

The existential form was recommended for the case that you 
were specifying the initial condition not as an operation
(a delta Button_state) but as a before state (a 
Button_State) or an after state (a Button_State').
However, the existential proof you have started is perfectly 
OK, you just have to carry it through without being phased 
by horizontal schemas.

 The second question I have is a more general one, and
 this may be difficult to answer since I am still green
 at proving properties of formal specifications. Say for
 example I do the precondition proofs and those all work
 out. What else can we say about the operations in this
 system before we exhaust the possibilities and I move on
 to coding, and verification there.

Before proceeding to implementation you would want to verify 
that the system as specified has the most important of the 
properties which you would expect of it.

Think of the difference between a specification of the system, 
and a specification of the requirements which the system must 
meet.

You don't have what I would call a requirements 
specification, you have a functional specification.
The kind of thing a requirements specification might say is 
that every request for a lift is eventually honoured, and 
that when you get in the lift you are eventually let out on 
the floor you requested.
Can you see how to state and prove such claims?

Roger Jones







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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

Jon,

On Friday 12 Oct 2012 20:35, Jon Lockhart wrote:
 
 I got back to the specification today, and moved on to
 proving the elevator state schema, Elevator_State, and I
 moved the static component elevator to an axiom, similar
 to the static components of button. Unfortunately I get
 a weird sub goal pop up that says {} = elevator after
 I work on the existence proof. Is this b/c I used the
 empty set as the witness to the elevator axiom proof?

No, its because you set both moving and stopped to the empty 
set, and this can only be the case if there are no 
elevators.
Your spec doesn't say there are no elevators, so you can't 
prove it.

You need to supply a witness for which the union of moving 
and stopped can be proven to be elevators, even though 
you don't know what elevators is.
One way to do that is to use the state in which everything 
is stopped, i.e. in which moving = {} and stopped = 
elevators.

I haven't checked that that satisfies the rest of the 
predicate, but I guess that's probable.

Roger


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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

Jon,

On Tuesday 09 Oct 2012 20:22, Jon Lockhart wrote:

 I am having a little trouble getting the axioms created,
 moving the static portions of the Button_State to an
 axiom from the schema. I can't seem to get the proof to
 operate properly. Any suggestions?

The problem is that the existential goal you are trying to 
prove has decorations on the names of the variables, but the 
witness you have supplied does not.

This is a point of difference between proving the non-
emptyness of a schema and the consistency of an axiomatic 
specification.

Because the names in the signature of the axiomatic spec 
have already been introduced as global variables (aka 
constants), they cannot be used as the names in the 
existential which must be proven to establish the 
consistency of the axiomatic specification.
So they get primed.

When z exists tac complains that it can't match the witness 
against the signature of the existential, first check that 
the names you have used in the binding are exactly those in 
the existential you are trying to prove, then check that the 
expressions have the right type.

regards,
Roger Jones


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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

On Friday 28 Sep 2012 22:26, Jon Lockhart wrote:

 I have two questions on that then. First, from a since
 and style standpoint, if I wanted to make everything
 neat in the spec I would place the no changing sets in
 the axiom after the state schema, but for functionality
 standpoint, if I wanted to use them in the predicate
 section of the schema they would need to go before it.
 So what would you see as being the better option? The
 second is would I prove their consistency just like I
 did the global variables?

First I should repeat my caveat. This is not a style of 
specification which I have used or studied, so my views on 
this may be eccentric.

If you are using ProofPower you have to present the 
specification so that every global variable is specified 
before it is used.  There may be tools which can reorder the 
specification for you, but ProofPower doesn't.
I'm not entirely sure what you meant by in the axiom after 
the state schema, I hope you didn't mean in the predicate 
of the state schema!

Yes, consistency proofs are the same as the ones you have 
been doing.
When you say just like the global variables, you do them 
like global variables because they will actually be global 
variables.

 I do see a problem though in that I don't want those sets
 to be accessed by anyone, only if the schema is included
 in the beginning of the operation.

It won't be possible to change them, but they will be global 
variables so any part of the specification after they have 
been introduced could access them.

 Could we resolve this
 matter by using the schema paragraphs? So we would
 create two schema descriptions of Button_State for
 example and then the first contains the static and the
 second the dynamic sets.

I think that is a good way of organising this material.
But the nub of the original suggestion was that they might 
be taken out of the signature of the operations, and in 
order for them to be accessible in defining the operations on 
the state they would have to be made into global variables 
(which is appropriate for something the specification regards 
as fixed in value).

So if you did define a schema containing what one might 
consider configuration data, you would have to use that 
schema to introduce the names in its signature as global 
variables so that they could then be accessed in you 
operation specifications (or in your definition of state).

 Then when accessing an
 operation the static or does not change symbol is placed
 in front of the static Button_State schema, allowing
 access to the sets, but not allowing change, and this
 way only when the name is provided in the description is
 the information accessible. Would that work to
 accomplish the same goal?

You could do something like this, though its not what I 
intended to suggest.
If I understand you correctly you are suggesting that the 
signature of the operation contains certain fixed data as 
well as the components  which are subject to change (and any 
input or output values).

I have never seen this done, and so I imagine this is a 
larger departure from normal practice than I was advocating.
It has some disadvantages relative to the method I intended 
to suggest.

Generally it is a good idea to try and structure the 
specification so that the size of signatures does not get 
very large.
It is a disadvantage of Z that the syle of specification 
encourages all the state of the system to be represented in 
the flat signature of a single state schema,
You can split this up into many parts and use schema 
inclusion to make this seem better structured in the 
specification, but when you come to reasoning with it you 
will be reasoning with objects which have very large 
signatures, and this make comprehension of what's going on 
more difficult.
In ProofPower is can lead to performance problems, and may 
lead to hard to understand diagnostics from the type 
inference system.

Another problem which may arise is in the schema calculus.
I have not looked into it, but operations like composition 
may not do the right thing with the extra components in the 
schema.

You could of course put the configuration variables in the 
state with an equivalence operator, then you would be back 
with something more standard (perhaps that's what you 
intended).  Schema composition would then do the right 
thing.

I suspect that this conversation is a little to intricate to 
work very well by email, since the misunderstandings which 
arise in such a discussion take to long to resolve.
If you want to talk about this we could have a Skype 
conversation, you can find me on skype from my email address.
(we would have to agree a time by email).

Roger






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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

Jon,

On Tuesday 25 Sep 2012 22:05, Jon Lockhart wrote:

 I started doing the There Exist proofs, and as you said
 they seem quite trivial indeed, but I seem to be stuck
 after the first two lines. So I have the goal, and it
 has been rewritten, now I am not sure what is the right
 question to ask. Do I do the z_There Exist_tac or
 something else? What constitutes a witness for some of
 the predicate declarations.

Ideally you would say prove_∃_tac and it would do it for 
you, but at present automation for existential goals in Z is 
not strong, so you normally have to supply the witness 
yourself and should use z_∃_tac.

You have to ask yourself what are the objects which belong 
to the schema (ButtonState in this case) and chose a simple 
one to use as a witness.
You then have to prove that the witness does indeed have the 
required properties.
So the question is, what's a simple binding which satisifies
the ButtonState predicate?, i.e. what are the acceptable 
states of the buttons.
The components of ButtonState are all sets.
You have said nothing which requires any of them to be non-
empty, and the specified relationships all hold if they are 
all empty.
So the binding in which every component is the empty set 
will be your simplest witness.
If you supply that witness and then rewrite that should 
solve the goal.

At this point you might ask yourself whether ButtonState 
does not allow more things to vary than might be thought 
acceptable.
Do you really want your system to allow all the buttons to 
disappear, or even to allow that the set of buttons might 
change, or to allow that a floor button become a lift button?
I don't know your application, but I would have thought that 
the set of buttons would be fixed and only the pushed bit 
was actually part of the state.
In that case you could have buttons, floorButtons and 
elevatorButtons as loosely specified by an axiomatic 
paragraph, so that they are fixed in any implementation of 
the spec but not fixed by the spec, and then you would have 
only one component in ButtonState, i.e. pushed, 
constrained to be a subset of the available buttons.

Roger


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

Re: [ProofPower] Initialisation convention

[Roger Bishop Jones]

Phil,

On Sunday 23 Sep 2012 21:11, Phil Clayton wrote:

 By making initialization an operation without a before
 state, the initialization can be used with schema
 operators such as composition and pre, e.g.
 
Init ⨟ Op
 
pre Init
 
 the latter being another way to write the following:
∃ Init ∙ true
∃ State' ∙ Init

That had occurred to me.
But it didn't seem to me a particularly good idea.

One could generally state the non-emptyness of some schema S 
as pre S', but surely its clearer to say ∃ S ∙ true.
(and Init /\ Op does the same under Spivey's convention as  
Init ⨟ Op under the other).

There doesn't seem to be much to chose between them.

Roger

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

[ProofPower] Initialisation convention

[Roger Bishop Jones]

I see that Potter Sinclair and Till An Introduction to 
Formal Specification Using Z 1991 use the primed version of 
the convention, and offer the following rationale (p43):

Here we use Vocab' as the variable to suggest that 
initialisation is like an operation which produces after 
objects which are acceptable as starting values for the 
persistent objects of the system.
Admittedly in this very simple case this seems a complicated 
way of saying that the system must start with an empty 
vocabulary.

(but note that they did not actually use an operation, the 
initial state is defined as a bare after-state).

Possibly the priming of initial state began here.
But 

Roger

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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

Jon,

I had a brief look at the last spec that you posted.
I also had a problem unzipping it, but despite a failure 
message got a decompression by opening the file in emacs.

The file decompressed in this way had two issues in it.
The first was that it terminated mid paragraph.
The second was that there were lower case beta signs 
systematically appearing throughout.

I used a repetitive edit to remove the betas and partially 
processed the result.

Some issues arising were:

1. Semicolons are needed between declarations but not after 
tha last one in the declaration part.

2. You used the same name (Elevator_State) twice for schemas 
(perhaps there was a significant beta there or some other 
problem with the decompression. The second occurence is for 
an operation over the first so presumably it was decorated in 
some way).

3. Not all uses of BOOLEAN values have been translated to 
use True and False instead of 0 and 1, so the remainder give 
type errors.

You may will find it hard work proving the consistency of 
your specification, even where it looks pretty obvious, and 
so there might be better value for you in using axiomatic 
mode (which amounts to assuming consistency) and working on 
more interesting proofs.  You can always go back later and 
prove the consistency results.
On the other hand, consistency proofs will be simpler than 
proving significant properties of the spec as a whole so it 
is a place to start learning proof.

Its not clear what consistency goal you were attempting, but 
I'm guessing it was masterStop, in which case using 
masterStop as a witness won't work. You could use True.
And then you will have to rewrite with the definition of True 
and that of BOOLEAN.

Roger


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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

On Friday 14 Sep 2012 10:36, Phil Clayton wrote:
 On 14/09/12 10:05, Roger Bishop Jones wrote:
  I had a brief look at the last spec that you posted.
  I also had a problem unzipping it, ...
 
 This doesn't surprise me because the attachment was byte
 for byte the same as the previous attachment that didn't
 unzip!  I guess Jon sent the wrong file or else
 something very strange is occurring.

Possibly somewhere en-route has a problem with binary 
attachments.  That used to happen a long time ago, but its 
not something I have seen recently.

Perhaps a good idea to attach the ascii version, Jon.

Do conv_ascii on your .doc file and attach the result.

Roger

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

Re: [ProofPower] Best platform for ProofPower?

[Roger Bishop Jones]

On Thursday 13 Sep 2012 19:37, Phil Clayton wrote:
 On 12/09/12 21:05, Roger Bishop Jones wrote:

  So far I'm not having much success on Ubuntu 12.04 (the
  PolyML build doesn't seem to work for me).
 
 What error message do you get?  I ask because David
 Matthews is about to release 5.5 so it would be worth
 resolving any issue there.

The build seemed to have gone through OK, though I couldn't 
actually find any instructions so who knows whether I did the 
right thing!

I ran ./configure a few times, installing whatever it 
complained of the absence of, and the ran make.

When I invoked poly it complained that it couldn't find some 
libraries.

Unfortunately I am now building Debian so Ubuntu 12.04 is 
history and I can't check exactly what the complaint was.

  I'm interested to know what people are actually running
  ProofPower on these days?
 
 I'm using Fedora 16.  Generally I've had no issue
 installing on the Fedora series of Linux provided that
 all the prerequisite packages are installed - achieved
 with the following yum/rpm commands:

Thanks for the info about Fedora 16 I will give that a go if 
I don't get on with Debian. (which was suggested by jon).

Roger


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

Re: [ProofPower] ProofPower Update

[Roger Bishop Jones]

Rob,

Sorry for the slow response.
I have thought quite a bit about this, but these days such 
cogitations don't always go anywhere useful.

On Thursday 30 Aug 2012 21:58, Rob Arthan wrote:
 On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote:

  and a number of cases where identifiers which I had
  been using are now used in MathsEgs theories which are
  in my ancestry these include Tree TREE Pair
 
 Were you using these names for things of your own?

Yes.

 If so,
 then perhaps this would be solved if the underlying
 names of constants were prefixed with the theory name.
 What I am considering in this area is an option
 controlled by a flag (say structured_HOL_namespace),
 which I would turn on towards the end of the HOL build,
 whereby the HOL parser would do this for you. When you
 define constant xyz in theory abc, the underlying
 name would be xyz.abc and abc would be introduced as
 an alias for that. And likewise for types. This
 behaviour would be optional and language-specific (e.g.,
 you wouldn't want it for Z, and you might not want it in
 HOL). Would that have saved you any trouble?

I don't think my problems with the new version of maths_egs 
are of any concern, and don't for me motivate changes.

I do think changes in this area are desirable but I would 
say that my own prime motivation would be to move to a 
situation in which proof tools can make use of results 
obtained in other proof tools, i.e. the motivations for 
OpenTheory and my X-Logic.
I think being able to eliminate junk from theories is 
something which would help in that enterprise, and as it 
happens it would probably would also help to mange the above 
kind of problem.

I think that probably would involve using compound constant 
names, at least behind the scenes, not necessarily in front 
of the children.
But I'm not keen on the use of the ProofPower aliasing 
mechanism to manage the use of simple names.

A key feature I think is simply to be able to hide names, or 
project a theory according to a signature, but also it would 
be nice to be able to rename on import.
I am inclined now to think that it might have been a mistake 
to automatically inherit all the ancestry when adding a 
parent.

This connects with the discussion about conservative 
extension, since it represents an alternative way of 
obtaining the kind of abstraction which new_specification 
provides, and possibly somewhat superior in that the details 
are all there, but not actually exported.

Putting it in that context, the idea that the structured 
namespace is something you opt into at some point seems to 
me doubtfull, though you might want it to default to 
behaviour which is backward compatible, i.e. if the local 
names are all globally unique then they will all get 
correctly resolved as at present.
However, once you put it in this context, then you are 
really looking at a bigger problem in which concensus across 
theorem provers is essential.

Personally, I think that shouldn't just be HOL provers, and 
as you know I advocate importing results even if proofs 
cannot be imported.
As an example of what ideally might be possible, classical 
arithmetic is standard, no two provers should disagree about 
what is true (though they will differ about what they can 
prove), so exchange across any tool which is sound for first 
order arithmetic should be possible in that domain.

All that of course is much more than you wanted to get into, 
and for my money you can safely do nothing here if your 
concern is just the occasional rework that people might have 
to do when you change maths_egs.

  (probably the most
  disruptive) and some identifiers consisting of or
  starting with subscripted D.
 
 Really -  I can't find any identifiers that start with a
 subscripted character in the MathsEgs theories.

The theory is topology which now contains some names which 
are the same as names you put into a bit of differential 
geometry you did for me way back.
 
  I have not yet considered a new way of building
  contribs. I feel that making MathsEgs build OK on the
  development system would not be productive in the
  absence of a little more clarity about how a contrib
  system would be expected to work.
 
 I had a discussion with Anthony Fox about how they do
 things in HOL4 and that has given me some more ideas on
 this. I think it is actually completely orthogonal to
 how the ProofPower code is organised.

Yes.
I got confused when you issues the trial reorganisation and 
tried to build maths_egs out of the RCS, which didn't work,
but it did build in the normal way of course.

 In HOL4, the contents of a theory are exported to and
 imported from text files. So if you have code associated
 with a theory that you want to export to users of the
 theory, you put that in a separate file and let users
 load that file. As ML doesn't have separate compilation,
 such code has to be provided as source. To  make things
 easier for the user, HOL4 has its own make function,
 HOLmake

[ProofPower] Best platform for ProofPower?

[Roger Bishop Jones]

I'm having bad luck lately getting suitable environments for 
running ProofPower.

My laptop is on Ubuntu 10.4, and that is fine for ProofPower, 
but is now so out of date that I can't upgrade it, I would 
have to install a more recent version of Ubuntu from 
scratch.

So I revived an old server to try out a more up-to-date 
context for running ProofPower.
(my efforts in the amazon cloud ran into the buffers some time 
ago).

So far I'm not having much success on Ubuntu 12.04 (the 
PolyML build doesn't seem to work for me).

I'm interested to know what people are actually running 
ProofPower on these days?

Roger Jones

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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

On Monday 03 Sep 2012 21:03, Jon Lockhart wrote:

 Most of the tactics return the
 exact same goal and the comment printed with the goal is
 that it is alpha-convertible to its goal.

The significance of this is simply that the proof step you 
have just done has not moved you forward.
i.e. it says that what you ended up with is essentially the 
same as what you started with.

 I am assuming
 it is saying that this subgoal is alpha-convertible to
 the main goal I am trying to prove.

Just the alpha-equivalent to the goal or subgoal from which 
it was obtained.

 Now I looked at the
 reference manual and there appears to be some commands
 that I can use to eliminate alpha-convertible components
 and that this is what I should use for simplifying the
 sub goal and thus proving it and the main goal.

No this is a red herring.

You are not reasoning from your subgoal to the main goal.
You have to prove the subgoal independently of the main 
goal, and when you have proved them all you have a proved 
the main goal.

 So based on the scenario above and where I am at does
 anyone have any suggestions on what commands I should
 use to handle the alpha-conversion and completing the
 proof of the subgoal?

Normally you would not need to do anything about alpha 
conversion, if you were within alpha conversion of the 
target then the system would sort that out for you 
automatically.

So your problem here is that you have misunderstood the 
significance of the alpha conversion message.
Forget about alpha conversion.

No-one can help you at this point, because we don't know 
anything at all about what you are trying to prove.
If you want help you should show us the problem you are 
working on.

Roger Jones













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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

On Saturday 25 Aug 2012 20:47, Jon Lockhart wrote:

 I did have a question on some of the outputs from the
 tutorial document. Currently I am on user013C and when I
 have placed some of the commands into the terminal, via
 the execute line command, the ProofPower output is not
 the same as is reported in the document. Is this due to
 some changes that have been made since this document was
 published in 2002? Also a few of the rewrite commands
 that were in the document threw exceptions.

On my system usr013A-C all load OK (in fact if they didn't 
the build would have failed since I think they are loaded in 
creating the examples database).

That is to say, if you start with a clean HOL database and 
do docsml on each of usr013A-C and then load file on each, 
they go through fine.

So the possible reasons for your failures are:

1. You are starting with the wrong database

or

2. you are copy and pasting something for which some prior 
script is essential but has not been executed.

or

3. you are trying to execute something which is in the 
document for explanation but is not there to be executed in 
that context.
(e.g. something in a GFT section rather than an SML 
section).

If you can't figure it out from that then you will need to 
post exactly what you have done and what the result was.


Roger Jones


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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

Jon,

You are right that Rob is the man to answer your technical
problem, but in the meantime I might be able to help you 
round it.

save_and_quit(); is something that I never use.

If your system otherwise seems OK then you should go right 
ahead and work through the tutorial.

Why don't I use it?

Well, whenever I am working interactively with ProofPower I 
just don't save the database.
I always have a make system in the background ready to build 
in batch mode, and this uses proofpower with the -f option 
to run a script and then save it.
So when I have a working script I create a new database 
using make.
This must be possible with your system otherwise you would 
not have completed the build of ProofPower.

When I resume work on an incomplete development I will enter 
the current document with xpp picking the database with all 
prior documents loaded, and then I use use_file to run the 
current script through to the point of failure where I was 
last working (and I force failure by just putting stop; in 
the script at the point I am working).
Then I continue my interactive work.
When I have a clean document I save it and then do a make to 
create a new database.

You probably don't want to set up a makefile for working 
through the tutorial, but you can still work in a similar 
manner, i.e. instead of saving the database when you pause 
in the tutorial, just put stop here; in your script, save 
it, and quit xpp.
When you come back use use_file to run your script through 
to your current position in the tutorial.
(you will need to use docsml on the file first if it is not 
pure SML, but for the tutorial you can just work with an SML 
script).

I presume you are looking at usr004, which is the gentlest 
introduction to ProofPower-HOL.
Alternatively you could work through the ProofPower HOL 
course usr022 with its accompanying tutorial notes usr013, 
which is less gentle but I think, more systematic and has 
greater coverage (but doesn't actually mention 
save_and_quit())

Roger Jones

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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

On Monday 13 Aug 2012 03:24, Jon Lockhart wrote:

 I have already written the specifications in Word using Z
 Word Tools, and they are already saved in a variety of
 formats. I have them transferred over to my linux image.
 What format do they need to be in for me to get to
 import them into XPP so I can begin the proof
 development.

ProofPower and Word don't really go together.
ProofPower works with LaTeX documents using a special 
encoding for non-ascii characters.
There are no automatic conversions available from Word to 
this format, though there is an alternative fully ascii 
source format using keywords instead of special characters.

The place to look for full details of ProofPower documents 
and the facilities associated with them is usr001 
ProofPower - Document Preparation which is part of the 
PPTex option when building ProofPower.

The ProofPower documentation is in directory doc of the 
installation, see index.html in that directory.

 My second question is once you get those specifications
 into XPP and the ProofPower tools, then how do you start
 writing the proofs on the Zed specs? Is it supposed to
 be in Zed terminology or in HOL?

Look at the ProofPower documentation page and you will find 
tutorials on proof in HOL and in Z.
Proofs of Z theorems will ideally stick to Z and not stray 
into HOL, but it doesn't always work out that way.
It is generally recommended to learn how to do proofs in HOL 
first and then move on to Z, and the tutorial materials for Z 
assume that the student already knows about proof in HOL,

If you don't know LaTeX or HOL then there is a pretty steep 
learning curve ahead to get into a position to do Z proofs 
in ProofPower.

It is possible to cut out the LaTeX, but without the LaTeX 
your ProofPower-Z source files would not be printable 
documents and you would be maintaining two parallel sets of 
documents, a printable set in Word and sources for 
ProofPower in a different set of documents.

Roger Jones

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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

On Monday 13 Aug 2012 13:12, Rob Arthan wrote:

 Jon is using Anthony Hall's Z Word Tools, which actually
 go quite a long way to bridging this gap. Z Word Tools
 allows you to prepare a Z specification inside a Word
 document and project out the Z in a format suitable for
 processing by other tools such as Fuzz or CZT.  Anthony
 and I have talked about adding ProofPower as a list of
 targets, but it got deferred pending some work I was
 doing on getting ProofPower to support UTF-8. I have a
 prototype converter from a UTF-8 format to the
 ProofPower formats, but it would require a bit of
 handcranking to get it to convert CZT input into
 ProofPower input. I don't know how much work would be
 involved in getting Z Word Tools to output something
 that ProofPower can eat (e.g., my UTF-8 format).

That's all very interesting, and it would be good to get 
ProofPower into a less eccentric position on document 
formats.

I have myself recently found myself using utf8 in LaTeX 
documents (when I wanted to get some Greek in), and may find 
myself wanting to prepare documents which have both Greek 
and ProofPower as a result of furthering my modelling of 
aspects of Aristotle's Organon and Metaphysics.

I see from reading a little about this in either or both of 
emacs and PERL that the support of arbitary encodings rather 
than specifically of one or more of the UTF variants seems to 
be thought desirable (and is realised I think in emacs).
From this point of view one might consider making the 
ProofPower encoding respectable by doing whatever is 
needed for it to be supported by such generic software.
It might then be possible to convert between ProofPower's 
encoding and others using some standard generic utility 
(perhaps emacs does this).
[On further grubbing around I think the generic facilities 
support a fixed, if perhaps long, list of encodings.
I haven't found anything which appears to work from a soft 
definition of an encoding.]

Somewhere in this maze I think there are ways of telling 
that the greek alphabet does consist of alphabetic 
characters and hence perhaps should be admitted in 
ProofPower identifiers.

When you speak of my UTF8 format, presumably you are 
talking about the mapping between the ProofPower extended 
characters and the unicode character codes (which wouldn't 
be specific to UTF8).

Incidentally, my hacks for making HTML from ProofPower 
sources, though they once translated into image references, 
were switched a while back to use unicode entities (not UTF 
but ascii things like #;) so I do have a mapping 
between the two (though incomplete).
Not good enough to be of any help to you, but I would fall 
in line with whatever mapping you have come up with if I 
ever find myself augmenting or fixing it.

Roger

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

Re: [ProofPower] ProofPower Update

[Roger Bishop Jones]

I have now managed to build my theories on the new 
ProofPower and MathsEgs.

I had to modify 13 source files to get them through.

It seems probable that the changes all resulted from the new 
MathsEgs, and primarily were changes to names.
These include the changes to theorems plus = additive 
and a number of cases where identifiers which I had been 
using are now used in MathsEgs theories which are in my 
ancestry these include Tree TREE Pair (probably the most 
disruptive) and some identifiers consisting of or starting 
with subscripted D.

There was only one broken proof (for reasons other than 
naming), and I am guessing that the reason was a change in 
the behaviour of R_top_anf_tac which now introduces powers 
in place of products where possible (it doesn't look like 
that was happening before) but I just repaired the proof and 
didn't go into detail on what had broken it.

I have not yet considered a new way of building contribs.
I feel that making MathsEgs build OK on the development 
system would not be productive in the absence of a little 
more clarity about how a contrib system would be expected to 
work.
The first issue in relation to this seems to me to be the 
localisation of namespaces.
A contrib system presumably would not work with a single RCS 
directory.
I don't actually understand why you could not have separate 
RCS directories for each product, together with one for files 
common to more than one product.
I suppose the problem is that make would not know where to 
go to for the files (and I suppose expects the RCS directory 
to be called RCS).

So the situation at the moment is that I don't feel there is 
enough clarity about where we are going to actually do 
anything at present, though I am more keen than I was last 
time we talked about this to make a fresh start on my own 
material, so I would like to move this forward so that I 
don't have to change twice to fit in.

Roger









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

Re: [ProofPower] ProofPower Update

[Roger Bishop Jones]

Rob,

On Thursday 09 Aug 2012 10:26, Rob Arthan wrote:

 I plan to make a new ProofPower release shortly. In the
 meantime, if you want the state of the art, I uploaded
 an experimental version built from the latest source.
 You can find this here:
 
 http://www.lemma-one.com/ProofPower/getting/experimental/

It that any different from what you get building from the RCS 
archive in your dropbox?

Can I build MathsEgs from that RCS?

[actually, I just tried but I see that the makefile for 
maths_egs isn't compliant with the pattern used in that 
system (no inst target, and the bld target fails).

VERY MINOR COMMENT

Seems odd that the directory in which one builds is called 
pp and the one in which one installs is ppdev.
Shouldn't it be the other way round?

Roger

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

Re: [ProofPower] ProofPower Update

[Roger Bishop Jones]

Rob,

My theories fail to build on the latest version of maths_egs 
because I have been using R_plus_ops_thm and 
R_plus_group_thm which were in wrk068 but are no longer.

Looks like you have just changed some names, is that right?

Roger Jones

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

Re: [ProofPower] ProofPower RCS Repository

[Roger Bishop Jones]

On Sunday 05 Aug 2012 15:36, Rob Arthan wrote:

 If anyone feels minded to look at this and advise how it
 could be adapted to work with Mercurial or Git, I would
 be very grateful. My ideal would be to be able to map
 between Mercurial or Git and RCS. Any feedback on this
 would be gratefully received.

I tried it but failed to build xpp.
Lots of undefined references:

/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(TextIn.o): In function 
`SelfInsert':
(.text+0x6fa6): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(TextOut.o): In function 
`FindWidth':
(.text+0x34f): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(TextOut.o): In function 
`FindWidth':
(.text+0x425): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(TextOut.o): In function 
`FindHeight':
(.text+0xbfd): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(TextOut.o): In function 
`FindHeight':
(.text+0xcfb): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmString.o):
(.text+0x2a46): more undefined references to 
`XftTextExtentsUtf8' follow
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmString.o): In function 
`SubStringPosition':
(.text+0x8625): undefined reference to `XftTextExtents16'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmString.o): In function 
`SubStringPosition':
(.text+0x893c): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmString.o): In function 
`SubStringPosition':
(.text+0x8bbb): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmString.o): In function 
`SubStringPosition':
(.text+0x8c3f): undefined reference to `XftTextExtents16'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(TextF.o): In function 
`FindPixelLength':
(.text+0x682): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(TextF.o): In function 
`FindPixelLength':
(.text+0x852): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(TextF.o): In function 
`FindPixelLength':
(.text+0x8d8): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(TextF.o): In function 
`PrintableString':
(.text+0x2f7e): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(TextF.o): In function 
`TextFieldResetIC':
(.text+0xb733): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftFontAverageWidth':
(.text+0x549): undefined reference to `XftTextExtents8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftDrawCreate':
(.text+0xabb): undefined reference to `XftDrawCreate'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftDrawCreate':
(.text+0xba2): undefined reference to `XftDrawCreateBitmap'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftDrawString':
(.text+0xd05): undefined reference to `XftDrawRect'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftDrawString':
(.text+0xd90): undefined reference to `XftDrawStringUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftDrawString':
(.text+0xdd8): undefined reference to `XftDrawString32'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftDrawString':
(.text+0xe20): undefined reference to `XftDrawString16'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftDrawString':
(.text+0xe56): undefined reference to `XftTextExtents16'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftDrawString':
(.text+0xe8e): undefined reference to `XftTextExtentsUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftDrawString':
(.text+0xf4e): undefined reference to `XftTextExtents32'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftDrawString2':
(.text+0x1106): undefined reference to `XftDrawStringUtf8'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftDrawString2':
(.text+0x114e): undefined reference to `XftDrawString32'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`_XmXftDrawString2':
(.text+0x1196): undefined reference to `XftDrawString16'
/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(XmRenderT.o): In function 
`ValidateAndLoadFont':

Re: [ProofPower] ProofPower RCS Repository

[Roger Bishop Jones]

On Monday 06 Aug 2012 19:40, Rob Arthan wrote:
 Could you try again with
 PPMOTIFLINKING=dynamic ?

That worked fine.

I'm afraid I can't help with mercurial or git, but I am due 
for a new development regime so I will be following you 
closely.

Roger


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

[ProofPower] ProofPower on AWS EC2

[Roger Bishop Jones]

Thanks to Phil, Rob and Wolfram for help so far.
I was completely distracted yesterday by the delivery of a 
new keyboard (7-octave variety), but seem to have made some 
progress.

Phil's Yum prescription was helpful.
The amazon repositories don't have SML, but do contain a 
satisfactory openmotif.
As it happens there is lots of other development software 
not installed so I added Development tools and 
Development Libraries groups, though most of what they 
provide I don't need.

As to what I am trying to do, certainly there is no intent 
to provide a service of any kind, just to use the cloud for 
my own development work, if that proved satisfactory.
ProofPower is in my mind a development tool, and as such 
would not be deployed in anything which looked like an 
application.
The most useful thing one could do in the cloud to support 
ProofPower users would probably be to provide an AMI (Amazon 
Machine Interface) with ProofPower already installed so that 
anyone wanting to run ProofPower in the cloud could pick up 
a working environment and then add to it whatever else he 
wanted to work with.
In theory Rob could make that into a product for which 
they could charge (by the hour), but presumably that would 
only be for the extra bits like DAZ which don't come in the 
opensource distribution.

As far as collaborative projects are concerned, I would have 
thought that a collaboration would center around a common 
source repository (in the cloud perhaps) rather than on 
trying to share a ProofPower database, which surely wouldn't 
work.

Anyway, as one would hope, installing ProofPower on AWS 
presents no special problems.

Running it interactively is not quite so simple but the 
simplest method mentioned by Rob really is simple and does 
actually work for xpp.
(that is: just add -X to the ssh command for connecting to 
the remote image and then invoke xpp on the remote as 
normal).
As Phil remarks, this picks up both the source files and the 
ProofPower databases in the cloud, which is what I was 
looking for.

For some reason it doesn't work for emacs, which complains 
of being on a dumb terminal and cops out.
If anyone knows how to persuade emacs to use the X-server 
that would be nice (just telling it the display doesn't do 
the trick).

Xpp seems to run OK, though the performance is very 
variable.
Some of this will be due to running in the AWS free layer, 
which presumably gets lesser priority than anything which is 
actually paid for.
As it is one would not want to use it for real.

Following Wolfram's advice I have been trying to get vnc 
running, which sounds like the right thing to do to get best 
performance interactively.

I had a bit of difficulty finding and chosing VNC software (a 
lot of it seems to be windows only).
The first problem was that tightVNC is now Windows only, but 
I eventually realised that TigerVNC is a split off tightVNC 
and is the linux version.
Part of my dismay about the complexity arose from looking at 
some software which was just libraries for developers of VNC 
servers and clients and not realising that it was not 
actually supplying any servers or clients and was just 
targeted at the developers.

Anyway I have tigerVNC up and running on the (AWS) server 
but can't get the client to work.
Wolfram's scripts, though I installed them all, seem 
unlikely to work because of the changes from tightvnc to 
tigerVNC.

Right now I'm wondering whether I have the client and server 
software in the right places.
Should it be the TigerVNC server out there in the cloud and 
the client here on earth, or the other way round?
I guess I'm running clients up there which use an X11 server 
down here?

Roger






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

Re: [ProofPower] Trouble Installing in cloud

[Roger Bishop Jones]

On Thursday 02 Aug 2012 00:33, you wrote:
 On 01/08/12 14:35, Roger Bishop Jones wrote:
  The real challenge (for me at least) is to get xpp
  and/or emacs to run in the cloud with a display here
  on earth, I don't have much clue how to do that.
 
 I've been thinking about this.  To me, it seems
 conceptually wrong to be running Xpp remotely.

Mm.
I don't know about conceptually, but there is a question 
here about what problem I am trying to solve.

 Would it
 not make more sense to run a local (earth-based) Xpp
 whose journal window contains a remote ProofPower shell
 (up in the cloud) via e.g. ssh?

If I were just interested in running ProofPower in the cloud 
then that would be correct. And this something that one 
might like to investigate.  However, my own primary interest 
is in whether I could export my entire development 
environment into the cloud so that I don't have to worry 
when I buy a device whether it will support LINUX and I get 
continuity of my development environment independently of 
what bits of kit I am buying or disposing of.

 Initially I tried
 testing
 
xpp -c ssh -Y user@host
 
 but is seems that the capabilities of Xpp's pseudo
 terminal aren't up to ssh login interaction.  However,
 if you can automatically log in then all is fine.  I
 used the instructions here:
 http://docs.fedoraproject.org/en-US/Fedora/17/html/System
 _Administrators_Guide/s2-ssh-configuration-keypairs.html
 to create .ssh/authorized_keys on the remote account to
 allow automatic log in.

Aren't you heading for a situation in which the source files 
being edited by Xpp are local but the ProofPower database 
which you are augmenting is remote?

I don't see how that would make sense.

I am really looking for a complete X11 framebuffer (is that 
what they call it?) which  is is remote, so that not only 
Xpp but also other tools like emacs run remotely.
There does seem to be software which does that (e.g. using 
VNC), but the documentation seems to assume you know a lot 
more than I do.
Alternatively X11 forwarding over SSH looks like it allows 
any applications you open on the remote host to operate 
windows on the local machine (but this is not supposed to 
perform very well or to provide robust connections).  These 
are the two scenarios I am investigating at the moment, 
along with a third which I'm not sure where it fits but which 
might be what amazon best supports (because I can see it in 
their yum depositories. which seem light on X11 package 
groups) viz. Xephyr.

Roger



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

[ProofPower] ProofPower in the cloud?

[Roger Bishop Jones]

Has anyone tried, or even considered, running ProoPower in 
the Amazon cloud (AWS they call it Amazon Web Services)?

They offer a number of Linux images which might be used as 
starting points.
Presumably one could run ProofPower and xpp in the cloud and 
access it using an X-client on cygwin on MS windows, in 
theory.

(I had a poke around but didn't spend enough time to get 
anywhere).

Roger Jones

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

Re: [ProofPower] Writing Z schema predicates with decorations

[Roger Bishop Jones]

On Wednesday 28 Sep 2011 13:52, Phil Clayton wrote:

  I wondered whether the original design intended to map
  decoration differently for predicates and expressions?
  Then the user could determine the mapping of e.g. S'
  as either
  mk_z_schema_pred (S, ')
  mk_z_schema_pred (mk_z_decor%down%s (S, '), )
  by controlling predicate/expression parsing modes as
  usual. (As Rob points out, the second is always used
  currently.)
 
 To answer my own question: from what Roger is saying,
 this must have been the intention as Z'SchemaPred can
 only occur in a predicate and Z'Decor only in an
 expression.

The rationale is specific to schemas as predicates, in other 
contexts I don't see how to avoid decorating the schema.

I see that the account I gave is pretty much the same as 
what Spivey says about decoration of schemas as predicates 
on page 72 of the second edition of The Z notation.
He gives the expansion as decorated theta term isin schema
(not in words of course) and I guess we decided to go 
straight to the explicit binding display because we knew we 
had to have those things and might as well go straight 
there, whereas Spivey seemed content to do without them.
Their absence from The Z notation explains why we ended up 
with a non-standard syntax for binding displays, since we 
had to make one up and the standards committee chose not to 
follow our lead  (Rob might know why, I think I had left the 
committee before that decision).

Roger

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

Re: [ProofPower] Writing Z schema predicates with decorations

[Roger Bishop Jones]

On Sunday 25 Sep 2011 16:20, Phil Clayton wrote:

 Although the Z'SchemaPred semantic constant enables
 renaming to be avoided, Z'SchemaPred HOL terms are not
 Z when the schema components are decorated
 inconsistently.  So perhaps renaming is useful?

I'm sure it is.

But I doubt that it is sensible in the mapping of a 
decorated schema reference.
In this case the same decoration is applied to all 
components.

As to the merits of the design of z_schema_pred, it seems to 
me that the mapping is not only simpler but works more as 
one would expect if a decorated schema reference uses the 
decoration parameter as intended.

In that case, simply rewriting with the definition of 
Z'SchemaPred (which is just membership) yields the statement 
that the binding with decorated variable names (but 
undecorated component names) is a member of the schema 
(undecorated).
This is as close as you get to asserting that the decorated 
theta term is a member of the schema (which might possibly 
have been even better in some ways, though less efficient).

My guess is that it probably was done that way in the 
prototype embedding of Z into the prototype ICL HOL (I did 
the specifications and explained them to Geoff Scullard who 
implemented them), but that when this was all re-implemented 
for the product version, the implementation fell out 
without using it (I don't think either Geoff or myself had 
much involvement at that stage, so the reason for using it 
got lost).

Roger

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

Re: [ProofPower] Writing Z schema predicates with decorations

[Roger Bishop Jones]

On Saturday 24 Sep 2011 22:53, Roger Bishop Jones wrote:
 On Saturday 24 Sep 2011 13:09, Rob Arthan wrote:
  The quick answer is no - the term generator
  (imp063.doc) never calls mk_z_schema_pred with
  non-empty decoration. I need to remind myself exactly
  what the decoration in mk_z_schema_pred is for (I know
  what the semantics is intended to be but I can't
  recall why we have it). Perhaps Roger can cast his
  mind back to this.
 
 My memory is pretty bad on the history.
 
 I expect that I started out with the syntax in Spivey's
 The Z Notation (It was the only game in town at the
 time). But then you might expect to see gen actuals
 and renaming! there.

A better answer is as follows.

We were making the Spivey syntax more orthogonal by 
allowing schema expressions in places where only schemas 
were previously allowed, and in that context there was no 
benefit in putting actual parameters or renamings into the 
predication operation, since they could be implemented 
using the normal schema expression operations.

However, decoration is another matter.
Decoration during schema-predication requires only that the 
free variables in the covert theta term be decorated.
Decorating the schema(expression) is a more horrible 
operation and is unnecessary.
So the parameter would enable a more efficient mapping of the 
Z into HOL, if it had actually been used!
Presumably the implementation (of z_schema_pred) does just 
decorate the theta term not the schema expression.

Roger



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

Re: [ProofPower] Writing Z schema predicates with decorations

[Roger Bishop Jones]

On Saturday 24 Sep 2011 13:09, Rob Arthan wrote:

 The quick answer is no - the term generator (imp063.doc)
 never calls mk_z_schema_pred with non-empty decoration.
 I need to remind myself exactly what the decoration in
 mk_z_schema_pred is for (I know what the semantics is
 intended to be but I can't recall why we have it).
 Perhaps Roger can cast his mind back to this.

My memory is pretty bad on the history.

I expect that I started out with the syntax in Spivey's The 
Z Notation (It was the only game in town at the time).
But then you might expect to see gen actuals and 
renaming! there.

To unravel it one would need to look at the very early 
editions of the specification.
Do the SCCS files have the full history in them?

 This reminds me that I always meant to make the Z
 specifications of the Z to HOL mapping available. As a
 quick fix, I have put the documents here:
 
 http://dl.dropbox.com/u/34693999/zed002.pdf
 http://dl.dropbox.com/u/34693999/zed003.pdf
 http://dl.dropbox.com/u/34693999/zed005.pdf
 
 I will make sure they typecheck presently and include
 them in the doc directory in future builds.

FIrst time I clicked on those links it worked OK but every 
subsequent attempt to access the documents has come up with 
something Acrobat could not process.

Roger

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

Re: [ProofPower] Printing of \not\in

[Roger Bishop Jones]

Rob,

I just made something like your document to exhibit the 
problem and I see that it doesn't.

In a sample document exhibiting the problem I have:

\usepackage{latexsym}
\usepackage{rbj}

and rbj.sty has in it:

\RequirePackage{Proofpower}
\RequirePackage{mathabx}

However, adding these two font packages to the simplest 
example does not create the problem.

I will get back to you when I have managed to reproduce the 
problem in a minimal context.

Roger













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

Re: [ProofPower] Printing of \not\in

[Roger Bishop Jones]

On Sunday 10 Jul 2011 12:22, Rob Arthan wrote:
 Roger,
 
 I had put this on my list of things to fix by changing
 \not\in in the style file to \notin, but I get exactly
 the opposite problem: \not\in work but \notin fails. Are
 you still having this problem? I am suspecting that you
 are using a style file that redefines both \not and
 \notin to something different from what LaTeX gives you
 out of the box. Note that \notin is not in the standard
 list of mathematical symbols in the LaTeX User's Guide.

I have the following in those of my documents which use the 
character:

\def\PrIO{\MMM{\notin}}

I don't understand how you get the opposite problem.

Roger

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

Re: [ProofPower] Printing of \not\in

[Roger Bishop Jones]

Rob,

On Sunday 10 Jul 2011 15:59, you wrote:
 
 What happens if you just run doctex and then texdvi on
 this file:
 
 http://dl.dropbox.com/u/34693999/ProofPower/rbj-not-in.te
 x
 
 For me it fails on the second GFT section, when the
 %notmem% character is expanded to \notin rather than
 \not\in.

You just asked me to run doctex on a tex file, so I skipped 
that step.

When I ran texdvi I got:

! Illegal parameter number in definition of \Temp.
to be read again 
   \crcr 
l.14 ...ng \Backslash{}notin : \PrNL{}\PrIO{}\PrNN
  {}\\


What I normally do is run docpdf which is my own lash up 
(using makeindex).

Roger

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

Re: [ProofPower] Printing of \not\in

[Roger Bishop Jones]

On Tuesday 29 Mar 2011 16:48, Rob Arthan wrote:

 It works fine for me. What goes wrong?

The failing occurrences are either in index brackets or in 
theory listings (probably also in index brackets).

The actual error message is:

! Undefined control sequence.
\not #1-\let \@@not 
 =\not \let \@@n =\n \let \not =\relax 
\let \n =\relax \...
l.849 ...M{} \$\PrNL{}\PrIO{}\PrIJ{m}\PrIJ{p}\PrNN
  {}: S 
\PrKN{} S \PrKN{} PR...

Unfortunately I don't know how to read these things and 
hence don't know exactly what it is complaining about,
but the odds are it is the double at signs.

Also I should say that I am using hyperref and makeindex 
rather than the standard indexing arrangements, which I 
would be inclined to blame if the failure was in the index, 
but I don't see how it (makeindex) affects these occurrences.

Roger


 

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

[ProofPower] Error on set_merge_pcs after add_cs_E_thm

[Roger Bishop Jones]

Here is a sequence of actions with ProofPower which is 
causing me puzzlement.

:) set_merge_pcs [unalg, 'latt2];

val it = () : unit

:) add_%exists%_cd_thms [MkLat_recursion_lemma] 'latt2;

val it = () : unit

:) set_merge_pcs [unalg, 'latt2];
Exception Fail * Element cannot be found in list [find.1004] 
* raised

So 'latt2 now seems to be in a mess.

The theorem I used was like this (something similar worked 
previously).

MkLat_recursion_lemma ;
val it = %turnstile% %forall% cf C a b· %exists% f· f (MkLat 
C a b) = cf C a b
: THM

(it isn't really a recursion theorem, I just want to be able 
to write function definitions by pattern matching on MkLat).

Any ideas on what is going on here?

Roger Jones

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

Re: [ProofPower] Cut and Paste problem

[Roger Bishop Jones]

On Thursday 08 Jul 2010 11:21, m...@proof-technologies.com 
wrote:
 In fact, Roger, could you confirm that you are using
  OpenMotif 2.3.0?

No. 2.2.3-4.
I'm on Ubuntu 9.04 so I think I will have to go up to 9.10.

Roger

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

Re: [ProofPower] help

[Roger Bishop Jones]

On Monday 09 November 2009 19:48:04 Igorj V wrote:

 may be some one could explain me such error when installing proofpower?!

 troff: fatal error: can't find macro file s

I had that problem, and the question has been asked and answered.
The answer is in the archive here:

http://lemma-one.com/pipermail/proofpower_lemma-one.com/2009-
October/000576.html

Roger Jones

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

Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus

[Roger Bishop Jones]

On Tuesday 24 March 2009 05:07:09 Artur Oliveira Gomes wrote:

I'm having hard times to achieve some proofs of preciondition
and initialization using ProofPower.
The file attached contains 3 examples that I still can not prove.
If anyone could help me out with those proofs, I will be thankful.

These are all existential conjectures.

ProofPower is sometimes quite dumb about these things
(sometimes quite smart), it only really knows about
the kinds of existential proofs which are necessary
for proving consistency of things like recursive
definitions (and that stuff only really works for HOL
its not so good in Z).  So usually you will have to
come up with a witness for the existential goal
yourself.

In the case of an existential with a schema as the
signature the witness will usually be a binding
display.  So for each of your proofs you must
come up with the binding display of a witness
for your conjecture, i.e. a binding which satisfies
the body of the existential, and then offer it up
using exists-tac.  Then you have to prove that
your witness does satisfy the predicate.

(I didn't check whether you are trying to prove
the right thing!)

regards,
Roger Jones


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

Re: [ProofPower] Schemas and Operations

[Roger Bishop Jones]

Artur,

After my last post I remembered the previous conversation
and realised that you were reducing the width of your
schemas and then having a problem translating the
theta expressions in the original.

I've been a bit busier than usual so I didn't get
back. In fact I forgot.

To use a theta term you have to contrive to get the
required signature variables into scope.
One way to do this is to use a quantifier.

Here's one way to do this how for your original example:

=TEX

=SML
open_theory z_reals;
new_theory temp;
=TEX

%SZS% State %BH%%BH%%BH%%BH%
%BV% a: %bbR%;
%BV% b: %bbB%
%EZ%%BH%%BH%%BH%%BH%%BH%

%SZS% OpState %BH%%BH%%BH%%BH%
%BV% %Delta%State
%BT%%BH%%BH%%BH%%BH%
%BV% a = real 0;
%BV% %theta%(State \%down%s (a))' = %theta%(State \%down%s (a))
%EZ%%BH%%BH%%BH%%BH%%BH%

%SFT%Z
%BV% NewState %def% [OldState : State]
%EFT%

%SZS% OpNewState %BH%%BH%%BH%%BH%
%BV% %Delta%NewState
%BT%%BH%%BH%%BH%%BH%
%BV% %exists%OpState%spot% %theta%(State) = OldState %and% %theta%(State)' = 
OldState'
%EZ%%BH%%BH%%BH%%BH%%BH%

=TEX

regards,
Rpger






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