--- a/src/ZF/UNITY/UNITY.thy Wed Nov 14 23:22:43 2001 +0100
+++ b/src/ZF/UNITY/UNITY.thy Thu Nov 15 15:07:16 2001 +0100
@@ -9,27 +9,31 @@
Theory ported from HOL.
*)
-UNITY = State + UNITYMisc +
+UNITY = State +
consts
constrains :: "[i, i] => i" (infixl "co" 60)
op_unless :: "[i, i] => i" (infixl "unless" 60)
constdefs
program :: i
- "program == {<init, acts, allowed>:condition*actionSet*actionSet.
- Id:acts & Id:allowed}"
+ "program == {<init, acts, allowed>:
+ Pow(state)*Pow(Pow(state*state))*Pow(Pow(state*state)).
+ id(state):acts & id(state):allowed}"
+ (* The definition below yields a program thanks to the coercions
+ init Int state, acts Int Pow(state*state), etc. *)
mk_program :: [i,i,i]=>i
"mk_program(init, acts, allowed) ==
- <init Int state, cons(Id, acts Int action), cons(Id, allowed Int action)>"
+ <init Int state, cons(id(state), acts Int Pow(state*state)),
+ cons(id(state), allowed Int Pow(state*state))>"
SKIP :: i
- "SKIP == mk_program(state, 0, action)"
+ "SKIP == mk_program(state, 0, Pow(state*state))"
- (** Coercion from anything to program **)
+ (* Coercion from anything to program *)
programify :: i=>i
"programify(F) == if F:program then F else SKIP"
-
+
RawInit :: i=>i
"RawInit(F) == fst(F)"
@@ -37,13 +41,13 @@
"Init(F) == RawInit(programify(F))"
RawActs :: i=>i
- "RawActs(F) == cons(Id, fst(snd(F)))"
+ "RawActs(F) == cons(id(state), fst(snd(F)))"
Acts :: i=>i
"Acts(F) == RawActs(programify(F))"
RawAllowedActs :: i=>i
- "RawAllowedActs(F) == cons(Id, snd(snd(F)))"
+ "RawAllowedActs(F) == cons(id(state), snd(snd(F)))"
AllowedActs :: i=>i
"AllowedActs(F) == RawAllowedActs(programify(F))"
@@ -52,9 +56,8 @@
Allowed :: i =>i
"Allowed(F) == {G:program. Acts(G) <= AllowedActs(F)}"
- (* initially property, used by some UNITY authors *)
- initially :: i => i
- "initially(A) == {F:program. Init(F)<= A & A:condition}"
+ initially :: i=>i
+ "initially(A) == {F:program. Init(F)<=A}"
stable :: i=>i
"stable(A) == A co A"
@@ -63,36 +66,24 @@
"strongest_rhs(F, A) == Inter({B:Pow(state). F:A co B})"
invariant :: i => i
- "invariant(A) == {F:program. Init(F)<=A} Int stable(A)"
+ "invariant(A) == initially(A) Int stable(A)"
+
+ (* The `increasing' relation of Charpentier. Increasing's parameters are:
+ a state function f, a domain A and an order relation r over the domain A. *)
+
+ increasing :: [i,i, i] => i
+ "increasing(A, r, f) == INT a:A. stable({s:state. <a, f`s>:r})"
+ (* The definition of a partial order in ZF (predicate part_ord in theory Order)
+ describes a strict order: irreflexive and transitive.
+ However, the order used in association with Charpentier's increasing
+ relation is not, hence the definition below: *)
part_order :: [i, i] => o
"part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)"
- nat_order :: i
- "nat_order == {<i,j>:nat*nat. i le j}"
-
- (*
- The constant increasing_on defines the Charpentier's increasing notion.
- It should not be confused with the ZF's increasing constant
- which have a different meaning.
- Increasing_on's parameters: a state function f, a domain A and
- a order relation r over the domain A
- Should f be a meta function instead ?
- *)
- increasing_on :: [i,i, i] => i ("increasing[_]'(_,_')")
- "increasing[A](f, r) ==
- {F:program. f:state->A & part_order(A,r) & F:
- (INT z:A. stable({s:state. <z, f`s>:r}))}"
-
defs
- (* The typing requirements `A:condition & B:condition'
- make the definition stronger than the original ones in HOL. *)
-
- constrains_def "A co B ==
- {F:program. (ALL act:Acts(F). act``A <= B)
- & A:condition & B:condition}"
-
+ (* Condition `st_set(A)' makes the definition slightly stronger than the HOL one *)
+ constrains_def "A co B == {F:program. (ALL act:Acts(F). act``A<=B) & st_set(A)}"
unless_def "A unless B == (A - B) co (A Un B)"
-
end