1 (* Title: HOLCF/IOA/meta_theory/Abstraction.thy |
1 (* Title: HOLCF/IOA/meta_theory/Abstraction.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Müller |
3 Author: Olaf Müller |
|
4 *) |
4 |
5 |
5 Abstraction Theory -- tailored for I/O automata. |
6 header {* Abstraction Theory -- tailored for I/O automata *} |
6 *) |
|
7 |
7 |
8 |
8 theory Abstraction |
9 Abstraction = LiveIOA + |
9 imports LiveIOA |
|
10 begin |
10 |
11 |
11 default type |
12 defaultsort type |
12 |
|
13 |
13 |
14 consts |
14 consts |
15 |
15 |
16 cex_abs ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" |
16 cex_abs ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" |
17 cex_absSeq ::"('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq" |
17 cex_absSeq ::"('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq" |
18 |
18 |
19 is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" |
19 is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" |
20 |
20 |
21 weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" |
21 weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" |
22 temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" |
22 temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" |
23 temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" |
23 temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" |
24 |
24 |
25 state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" |
25 state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" |
26 state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" |
26 state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" |
27 |
27 |
28 is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" |
28 is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" |
29 |
29 |
30 |
30 |
31 defs |
31 defs |
32 |
32 |
33 is_abstraction_def |
33 is_abstraction_def: |
34 "is_abstraction f C A == |
34 "is_abstraction f C A == |
35 (!s:starts_of(C). f(s):starts_of(A)) & |
35 (!s:starts_of(C). f(s):starts_of(A)) & |
36 (!s t a. reachable C s & s -a--C-> t |
36 (!s t a. reachable C s & s -a--C-> t |
37 --> (f s) -a--A-> (f t))" |
37 --> (f s) -a--A-> (f t))" |
38 |
38 |
39 is_live_abstraction_def |
39 is_live_abstraction_def: |
40 "is_live_abstraction h CL AM == |
40 "is_live_abstraction h CL AM == |
41 is_abstraction h (fst CL) (fst AM) & |
41 is_abstraction h (fst CL) (fst AM) & |
42 temp_weakening (snd AM) (snd CL) h" |
42 temp_weakening (snd AM) (snd CL) h" |
43 |
43 |
44 cex_abs_def |
44 cex_abs_def: |
45 "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))" |
45 "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))" |
46 |
46 |
47 (* equals cex_abs on Sequneces -- after ex2seq application -- *) |
47 (* equals cex_abs on Sequneces -- after ex2seq application -- *) |
48 cex_absSeq_def |
48 cex_absSeq_def: |
49 "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s" |
49 "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s" |
50 |
50 |
51 weakeningIOA_def |
51 weakeningIOA_def: |
52 "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A" |
52 "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A" |
53 |
53 |
54 temp_weakening_def |
54 temp_weakening_def: |
55 "temp_weakening Q P h == temp_strengthening (.~ Q) (.~ P) h" |
55 "temp_weakening Q P h == temp_strengthening (.~ Q) (.~ P) h" |
56 |
56 |
57 temp_strengthening_def |
57 temp_strengthening_def: |
58 "temp_strengthening Q P h == ! ex. (cex_abs h ex |== Q) --> (ex |== P)" |
58 "temp_strengthening Q P h == ! ex. (cex_abs h ex |== Q) --> (ex |== P)" |
59 |
59 |
60 state_weakening_def |
60 state_weakening_def: |
61 "state_weakening Q P h == state_strengthening (.~Q) (.~P) h" |
61 "state_weakening Q P h == state_strengthening (.~Q) (.~P) h" |
62 |
62 |
63 state_strengthening_def |
63 state_strengthening_def: |
64 "state_strengthening Q P h == ! s t a. Q (h(s),a,h(t)) --> P (s,a,t)" |
64 "state_strengthening Q P h == ! s t a. Q (h(s),a,h(t)) --> P (s,a,t)" |
65 |
65 |
66 rules |
66 axioms |
67 |
67 |
68 (* thm about ex2seq which is not provable by induction as ex2seq is not continous *) |
68 (* thm about ex2seq which is not provable by induction as ex2seq is not continous *) |
69 ex2seq_abs_cex |
69 ex2seq_abs_cex: |
70 "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)" |
70 "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)" |
71 |
71 |
72 (* analog to the proved thm strength_Box - proof skipped as trivial *) |
72 (* analog to the proved thm strength_Box - proof skipped as trivial *) |
73 weak_Box |
73 weak_Box: |
74 "temp_weakening P Q h |
74 "temp_weakening P Q h |
75 ==> temp_weakening ([] P) ([] Q) h" |
75 ==> temp_weakening ([] P) ([] Q) h" |
76 |
76 |
77 (* analog to the proved thm strength_Next - proof skipped as trivial *) |
77 (* analog to the proved thm strength_Next - proof skipped as trivial *) |
78 weak_Next |
78 weak_Next: |
79 "temp_weakening P Q h |
79 "temp_weakening P Q h |
80 ==> temp_weakening (Next P) (Next Q) h" |
80 ==> temp_weakening (Next P) (Next Q) h" |
81 |
81 |
|
82 ML {* use_legacy_bindings (the_context ()) *} |
|
83 |
82 end |
84 end |