Jon, On 13/09/12 04:16, Jon Lockhart wrote:

Are you saying then for the Boolean block I have to just replace it with the one that you have provided in the email?

## Advertising

`Not only would you have to replace the Boolean block but also remove the`

`integer comparison around the references to Boolean global variables.`

`For example, the predicate`

masterStop = 0 must be changed to either ¬ masterStop or masterStop = False

Seems odd to be to just through True and False in there like that where I am describing sets but if it works, then I am all for it, I just need to see or understand how to use it properly.

`To use this is very simple for the most part. In a predicate context,`

`just treat Boolean expressions as though they were predicates. In an`

`expression context, Boolean expressions can be combined to give other`

`Boolean expressions as you would expect, e.g. a ∧ b. However, to create`

`a Boolean expression from a predicate p, you need to write`

[ | p]

`It is probably worth understanding what is going on at least once. It`

`is easiest to think in terms of sets. A schema is just a set of`

`bindings. The empty schema [], which is the same as [ | true], is a set`

`containing just the empty binding, i.e. {()}. So [] is much like the`

`SML type 'unit', a type that has only one value. Thus Boolean is the`

`set {{}, {()}} where {} represents false and {()} represents true, hence`

`our definition of True and False. So an expression of type Boolean is a`

`schema. When a schema S is used as a predicate, the predicate is θS ∈`

`S. For one of our Boolean expressions B as a predicate, the predicate`

`is θB ∈ B which is equivalent to () ∈ B. So you can see how the`

`corresponding predicate is derived.`

As for the version of ProofPower, I have version 2.9.1w2, which is what you were saying does not support ==. Looks like I might have to update here when the latest stable version is released on the site.

If you feel inclined to try the latest patch, it is here, with instructions: http://www.lemma-one.com/ProofPower/patches/patches.html

`I'm fairly familiar with the installation process, so it only takes me a`

`few minutes to build a patched version. However, a new release may be`

`around the corner - I don't know what Rob's plans are there.`

What I was saying on the masterStop / masterReset axiom, along with the minNumberFloors, maxNumberFloors, etc axioms, since I am using those as global variables essentially, is how do I prove them and preconditions on them like I have down for my States so far? Is is necessary too, or if I just get the spec of them they are already shown to be theorems?

`I see what you mean. Yes, for an axiomatic description, one wants to be`

`sure that it is not introducing a contradiction into the theory, making`

`the theory inconsistent. ProofPower has a mode of operation where it`

`does not assume such axioms are consistent until they have been proved`

`consistent. This works by showing that each axiom is a conservative`

`extension to the theory, i.e. does not introduce an inconsistency.`

For Z, at the start of your theory, you would do set_flag ("z_use_axioms", false);

`Note, then, that z_get_spec does not simply give you the axiom as a`

`theorem. After an axiomatic description paragraph, start a consistency`

`proof with e.g.`

z_push_consistency_goal %SZT%minNumberFloors%>%; See section 5.3, page 93, of usr011.dvi for examples. Phil _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com