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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
