# Re: [ProofPower] Trying to Prove my Zed Specifications

```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?
```

```
```
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
```