author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 12218 | 6597093b77e7 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
4559 | 1 |
(* Title: HOLCF/IOA/meta_theory/Abstraction.thy |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
4559 | 5 |
|
12218 | 6 |
Abstraction Theory -- tailored for I/O automata. |
4559 | 7 |
*) |
8 |
||
9 |
||
4816 | 10 |
Abstraction = LiveIOA + |
4559 | 11 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12218
diff
changeset
|
12 |
default type |
4559 | 13 |
|
14 |
||
15 |
consts |
|
16 |
||
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
17 |
cex_abs ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
18 |
cex_absSeq ::"('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq" |
4559 | 19 |
|
20 |
is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" |
|
21 |
||
22 |
weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" |
|
23 |
temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" |
|
24 |
temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" |
|
25 |
||
26 |
state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" |
|
27 |
state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" |
|
28 |
||
29 |
is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" |
|
30 |
||
31 |
||
32 |
defs |
|
33 |
||
34 |
is_abstraction_def |
|
35 |
"is_abstraction f C A == |
|
36 |
(!s:starts_of(C). f(s):starts_of(A)) & |
|
37 |
(!s t a. reachable C s & s -a--C-> t |
|
38 |
--> (f s) -a--A-> (f t))" |
|
39 |
||
40 |
is_live_abstraction_def |
|
41 |
"is_live_abstraction h CL AM == |
|
42 |
is_abstraction h (fst CL) (fst AM) & |
|
43 |
temp_weakening (snd AM) (snd CL) h" |
|
44 |
||
45 |
cex_abs_def |
|
10835 | 46 |
"cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))" |
4559 | 47 |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
48 |
(* equals cex_abs on Sequneces -- after ex2seq application -- *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
49 |
cex_absSeq_def |
10835 | 50 |
"cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s" |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
51 |
|
4559 | 52 |
weakeningIOA_def |
53 |
"weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A" |
|
54 |
||
55 |
temp_weakening_def |
|
56 |
"temp_weakening Q P h == temp_strengthening (.~ Q) (.~ P) h" |
|
57 |
||
58 |
temp_strengthening_def |
|
59 |
"temp_strengthening Q P h == ! ex. (cex_abs h ex |== Q) --> (ex |== P)" |
|
60 |
||
61 |
state_weakening_def |
|
62 |
"state_weakening Q P h == state_strengthening (.~Q) (.~P) h" |
|
63 |
||
64 |
state_strengthening_def |
|
65 |
"state_strengthening Q P h == ! s t a. Q (h(s),a,h(t)) --> P (s,a,t)" |
|
66 |
||
67 |
rules |
|
68 |
||
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
69 |
(* thm about ex2seq which is not provable by induction as ex2seq is not continous *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
70 |
ex2seq_abs_cex |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
71 |
"ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)" |
4559 | 72 |
|
5976 | 73 |
(* analog to the proved thm strength_Box - proof skipped as trivial *) |
4559 | 74 |
weak_Box |
75 |
"temp_weakening P Q h |
|
76 |
==> temp_weakening ([] P) ([] Q) h" |
|
77 |
||
5976 | 78 |
(* analog to the proved thm strength_Next - proof skipped as trivial *) |
4559 | 79 |
weak_Next |
80 |
"temp_weakening P Q h |
|
81 |
==> temp_weakening (Next P) (Next Q) h" |
|
82 |
||
83 |
end |