5111
|
1 |
(* Title: HOL/UNITY/Traces
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1998 University of Cambridge
|
|
5 |
|
|
6 |
Inductive definitions of
|
|
7 |
* traces: the possible execution traces
|
|
8 |
* reachable: the set of reachable states
|
|
9 |
*)
|
|
10 |
|
5648
|
11 |
Traces = LessThan +
|
4776
|
12 |
|
5111
|
13 |
consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
|
4776
|
14 |
|
5111
|
15 |
(*Initial states and program => (final state, reversed trace to it)...
|
|
16 |
Arguments MUST be curried in an inductive definition*)
|
|
17 |
|
|
18 |
inductive "traces Init Acts"
|
4776
|
19 |
intrs
|
|
20 |
(*Initial trace is empty*)
|
5111
|
21 |
Init "s: Init ==> (s,[]) : traces Init Acts"
|
4776
|
22 |
|
5111
|
23 |
Acts "[| act: Acts; (s,evs) : traces Init Acts; (s,s'): act |]
|
|
24 |
==> (s', s#evs) : traces Init Acts"
|
4776
|
25 |
|
|
26 |
|
5596
|
27 |
typedef (Program)
|
5608
|
28 |
'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
|
5584
|
29 |
|
|
30 |
constdefs
|
5596
|
31 |
mk_program :: "('a set * ('a * 'a)set set) => 'a program"
|
5608
|
32 |
"mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
|
5596
|
33 |
|
|
34 |
Init :: "'a program => 'a set"
|
5620
|
35 |
"Init F == fst (Rep_Program F)"
|
5596
|
36 |
|
5584
|
37 |
Acts :: "'a program => ('a * 'a)set set"
|
5620
|
38 |
"Acts F == snd (Rep_Program F)"
|
5253
|
39 |
|
|
40 |
|
|
41 |
consts reachable :: "'a program => 'a set"
|
|
42 |
|
5620
|
43 |
inductive "reachable F"
|
5253
|
44 |
intrs
|
5620
|
45 |
Init "s: Init F ==> s : reachable F"
|
5253
|
46 |
|
5620
|
47 |
Acts "[| act: Acts F; s : reachable F; (s,s'): act |]
|
|
48 |
==> s' : reachable F"
|
5253
|
49 |
|
4776
|
50 |
end
|