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