|
1 (* Title: ZF/UNITY/UNITY.thy |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 The basic UNITY theory (revised version, based upon the "co" operator) |
|
7 From Misra, "A Logic for Concurrent Programming", 1994 |
|
8 |
|
9 Theory ported from HOL. |
|
10 *) |
|
11 |
|
12 UNITY = State + UNITYMisc + |
|
13 consts |
|
14 constrains :: "[i, i] => i" (infixl "co" 60) |
|
15 op_unless :: "[i, i] => i" (infixl "unless" 60) |
|
16 |
|
17 constdefs |
|
18 program :: i |
|
19 "program == {<init, acts, allowed>:condition*actionSet*actionSet. |
|
20 Id:acts & Id:allowed}" |
|
21 |
|
22 mk_program :: [i,i,i]=>i |
|
23 "mk_program(init, acts, allowed) == |
|
24 <init Int state, cons(Id, acts Int action), cons(Id, allowed Int action)>" |
|
25 |
|
26 SKIP :: i |
|
27 "SKIP == mk_program(state, 0, action)" |
|
28 |
|
29 (** Coercion from anything to program **) |
|
30 programify :: i=>i |
|
31 "programify(F) == if F:program then F else SKIP" |
|
32 |
|
33 RawInit :: i=>i |
|
34 "RawInit(F) == fst(F)" |
|
35 |
|
36 Init :: i=>i |
|
37 "Init(F) == RawInit(programify(F))" |
|
38 |
|
39 RawActs :: i=>i |
|
40 "RawActs(F) == cons(Id, fst(snd(F)))" |
|
41 |
|
42 Acts :: i=>i |
|
43 "Acts(F) == RawActs(programify(F))" |
|
44 |
|
45 RawAllowedActs :: i=>i |
|
46 "RawAllowedActs(F) == cons(Id, snd(snd(F)))" |
|
47 |
|
48 AllowedActs :: i=>i |
|
49 "AllowedActs(F) == RawAllowedActs(programify(F))" |
|
50 |
|
51 |
|
52 Allowed :: i =>i |
|
53 "Allowed(F) == {G:program. Acts(G) <= AllowedActs(F)}" |
|
54 |
|
55 (* initially property, used by some UNITY authors *) |
|
56 initially :: i => i |
|
57 "initially(A) == {F:program. Init(F)<= A & A:condition}" |
|
58 |
|
59 stable :: i=>i |
|
60 "stable(A) == A co A" |
|
61 |
|
62 strongest_rhs :: [i, i] => i |
|
63 "strongest_rhs(F, A) == Inter({B:Pow(state). F:A co B})" |
|
64 |
|
65 invariant :: i => i |
|
66 "invariant(A) == {F:program. Init(F)<=A} Int stable(A)" |
|
67 |
|
68 part_order :: [i, i] => o |
|
69 "part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)" |
|
70 |
|
71 nat_order :: i |
|
72 "nat_order == {<i,j>:nat*nat. i le j}" |
|
73 |
|
74 (* |
|
75 The constant increasing_on defines the Charpentier's increasing notion. |
|
76 It should not be confused with the ZF's increasing constant |
|
77 which have a different meaning. |
|
78 Increasing_on's parameters: a state function f, a domain A and |
|
79 a order relation r over the domain A |
|
80 Should f be a meta function instead ? |
|
81 *) |
|
82 increasing_on :: [i,i, i] => i ("increasing[_]'(_,_')") |
|
83 "increasing[A](f, r) == |
|
84 {F:program. f:state->A & part_order(A,r) & F: |
|
85 (INT z:A. stable({s:state. <z, f`s>:r}))}" |
|
86 |
|
87 defs |
|
88 (* The typing requirements `A:condition & B:condition' |
|
89 make the definition stronger than the original ones in HOL. *) |
|
90 |
|
91 constrains_def "A co B == |
|
92 {F:program. (ALL act:Acts(F). act``A <= B) |
|
93 & A:condition & B:condition}" |
|
94 |
|
95 unless_def "A unless B == (A - B) co (A Un B)" |
|
96 |
|
97 end |
|
98 |