|
1 (* Title: HOL/UNITY/State.thy |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 Formalizes UNITY-program states using dependent types: |
|
7 - variables are typed. |
|
8 - the state space is uniform, common to all defined programs. |
|
9 - variables can be quantified over. |
|
10 |
|
11 *) |
|
12 |
|
13 State = UNITYMisc + |
|
14 |
|
15 consts |
|
16 variable :: i |
|
17 |
|
18 (** |
|
19 Variables are better represented using integers, but at the moment |
|
20 there is a problem with integer translations like "uu" == "Var(#0)", which |
|
21 are needed to give names to variables. |
|
22 So for the time being we are using lists of naturals to index variables. |
|
23 **) |
|
24 |
|
25 datatype variable = Var("i:list(nat)") |
|
26 type_intrs "[list_nat_into_univ]" |
|
27 |
|
28 consts |
|
29 state, action, some ::i |
|
30 type_of :: i=>i |
|
31 |
|
32 translations |
|
33 (* The state space is a dependent type *) |
|
34 "state" == "Pi(variable, type_of)" |
|
35 |
|
36 (* Commands are relations over states *) |
|
37 "action" == "Pow(state*state)" |
|
38 |
|
39 rules |
|
40 (** We might have defined the state space in a such way that it is already |
|
41 not empty by formation: for example "state==PROD x:variable. type_of(x) Un {0}" |
|
42 which contains the function (lam x:variable. 0) is a possible choice. |
|
43 However, we prefer the following way for simpler proofs by avoiding |
|
44 case splitting resulting from type_of(x) Un {0}. **) |
|
45 |
|
46 some_in_state "some:state" |
|
47 |
|
48 constdefs |
|
49 (* State conditions/predicates are sets of states *) |
|
50 condition :: i |
|
51 "condition == Pow(state)" |
|
52 |
|
53 actionSet :: i |
|
54 "actionSet == Pow(action)" |
|
55 |
|
56 consts |
|
57 Id :: i |
|
58 translations |
|
59 "Id" == "Identity(state)" |
|
60 end |