1 (* Title: HOLCF/IOA/meta_theory/Simulations.thy |
|
2 Author: Olaf Müller |
|
3 *) |
|
4 |
|
5 header {* Simulations in HOLCF/IOA *} |
|
6 |
|
7 theory Simulations |
|
8 imports RefCorrectness |
|
9 begin |
|
10 |
|
11 default_sort type |
|
12 |
|
13 definition |
|
14 is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
|
15 "is_simulation R C A = |
|
16 ((!s:starts_of C. R``{s} Int starts_of A ~= {}) & |
|
17 (!s s' t a. reachable C s & |
|
18 s -a--C-> t & |
|
19 (s,s') : R |
|
20 --> (? t' ex. (t,t'):R & move A ex s' a t')))" |
|
21 |
|
22 definition |
|
23 is_backward_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
|
24 "is_backward_simulation R C A = |
|
25 ((!s:starts_of C. R``{s} <= starts_of A) & |
|
26 (!s t t' a. reachable C s & |
|
27 s -a--C-> t & |
|
28 (t,t') : R |
|
29 --> (? ex s'. (s,s'):R & move A ex s' a t')))" |
|
30 |
|
31 definition |
|
32 is_forw_back_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
|
33 "is_forw_back_simulation R C A = |
|
34 ((!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) & |
|
35 (!s S' t a. reachable C s & |
|
36 s -a--C-> t & |
|
37 (s,S') : R |
|
38 --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t'))))" |
|
39 |
|
40 definition |
|
41 is_back_forw_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
|
42 "is_back_forw_simulation R C A = |
|
43 ((!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) & |
|
44 (!s t T' a. reachable C s & |
|
45 s -a--C-> t & |
|
46 (t,T') : R |
|
47 --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t'))))" |
|
48 |
|
49 definition |
|
50 is_history_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
|
51 "is_history_relation R C A = (is_simulation R C A & |
|
52 is_ref_map (%x.(@y. (x,y):(R^-1))) A C)" |
|
53 |
|
54 definition |
|
55 is_prophecy_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
|
56 "is_prophecy_relation R C A = (is_backward_simulation R C A & |
|
57 is_ref_map (%x.(@y. (x,y):(R^-1))) A C)" |
|
58 |
|
59 |
|
60 lemma set_non_empty: "(A~={}) = (? x. x:A)" |
|
61 apply auto |
|
62 done |
|
63 |
|
64 lemma Int_non_empty: "(A Int B ~= {}) = (? x. x: A & x:B)" |
|
65 apply (simp add: set_non_empty) |
|
66 done |
|
67 |
|
68 |
|
69 lemma Sim_start_convert: |
|
70 "(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)" |
|
71 apply (unfold Image_def) |
|
72 apply (simp add: Int_non_empty) |
|
73 done |
|
74 |
|
75 declare Sim_start_convert [simp] |
|
76 |
|
77 |
|
78 lemma ref_map_is_simulation: |
|
79 "!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A" |
|
80 |
|
81 apply (unfold is_ref_map_def is_simulation_def) |
|
82 apply simp |
|
83 done |
|
84 |
|
85 end |
|