1 (* Title: HOLCF/IOA/TrivEx.thy |
1 (* Title: HOLCF/IOA/TrivEx.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Müller |
3 Author: Olaf Müller |
4 |
|
5 Trivial Abstraction Example. |
|
6 *) |
4 *) |
7 |
5 |
8 TrivEx = Abstraction + |
6 header {* Trivial Abstraction Example *} |
|
7 |
|
8 theory TrivEx |
|
9 imports Abstraction |
|
10 begin |
9 |
11 |
10 datatype action = INC |
12 datatype action = INC |
11 |
13 |
12 consts |
14 consts |
13 |
15 |
14 C_asig :: "action signature" |
16 C_asig :: "action signature" |
15 C_trans :: (action, nat)transition set |
17 C_trans :: "(action, nat)transition set" |
16 C_ioa :: (action, nat)ioa |
18 C_ioa :: "(action, nat)ioa" |
17 |
19 |
18 A_asig :: "action signature" |
20 A_asig :: "action signature" |
19 A_trans :: (action, bool)transition set |
21 A_trans :: "(action, bool)transition set" |
20 A_ioa :: (action, bool)ioa |
22 A_ioa :: "(action, bool)ioa" |
21 |
23 |
22 h_abs :: "nat => bool" |
24 h_abs :: "nat => bool" |
23 |
25 |
24 defs |
26 defs |
25 |
27 |
26 C_asig_def |
28 C_asig_def: |
27 "C_asig == ({},{INC},{})" |
29 "C_asig == ({},{INC},{})" |
28 |
30 |
29 C_trans_def "C_trans == |
31 C_trans_def: "C_trans == |
30 {tr. let s = fst(tr); |
32 {tr. let s = fst(tr); |
31 t = snd(snd(tr)) |
33 t = snd(snd(tr)) |
32 in case fst(snd(tr)) |
34 in case fst(snd(tr)) |
33 of |
35 of |
34 INC => t = Suc(s)}" |
36 INC => t = Suc(s)}" |
35 |
37 |
36 C_ioa_def "C_ioa == |
38 C_ioa_def: "C_ioa == |
37 (C_asig, {0}, C_trans,{},{})" |
39 (C_asig, {0}, C_trans,{},{})" |
38 |
40 |
39 A_asig_def |
41 A_asig_def: |
40 "A_asig == ({},{INC},{})" |
42 "A_asig == ({},{INC},{})" |
41 |
43 |
42 A_trans_def "A_trans == |
44 A_trans_def: "A_trans == |
43 {tr. let s = fst(tr); |
45 {tr. let s = fst(tr); |
44 t = snd(snd(tr)) |
46 t = snd(snd(tr)) |
45 in case fst(snd(tr)) |
47 in case fst(snd(tr)) |
46 of |
48 of |
47 INC => t = True}" |
49 INC => t = True}" |
48 |
50 |
49 A_ioa_def "A_ioa == |
51 A_ioa_def: "A_ioa == |
50 (A_asig, {False}, A_trans,{},{})" |
52 (A_asig, {False}, A_trans,{},{})" |
51 |
53 |
52 h_abs_def |
54 h_abs_def: |
53 "h_abs n == n~=0" |
55 "h_abs n == n~=0" |
54 |
56 |
55 rules |
57 axioms |
56 |
58 |
57 MC_result |
59 MC_result: |
58 "validIOA A_ioa (<>[] <%(b,a,c). b>)" |
60 "validIOA A_ioa (<>[] <%(b,a,c). b>)" |
59 |
61 |
|
62 ML {* use_legacy_bindings (the_context ()) *} |
|
63 |
60 end |
64 end |