author | wenzelm |
Wed, 30 Dec 2015 22:05:00 +0100 | |
changeset 62003 | ba465fcd0267 |
parent 62002 | f1599e98c4d0 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/IOA/meta_theory/Simulations.thy |
40945 | 2 |
Author: Olaf Müller |
4565 | 3 |
*) |
4 |
||
62002 | 5 |
section \<open>Simulations in HOLCF/IOA\<close> |
4565 | 6 |
|
17233 | 7 |
theory Simulations |
8 |
imports RefCorrectness |
|
9 |
begin |
|
10 |
||
36452 | 11 |
default_sort type |
4565 | 12 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
13 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
14 |
is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
15 |
"is_simulation R C A = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
16 |
((!s:starts_of C. R``{s} Int starts_of A ~= {}) & |
17233 | 17 |
(!s s' t a. reachable C s & |
62003 | 18 |
s \<midarrow>a\<midarrow>C\<rightarrow> t & |
17233 | 19 |
(s,s') : R |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
20 |
--> (? t' ex. (t,t'):R & move A ex s' a t')))" |
4565 | 21 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
22 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
23 |
is_backward_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
24 |
"is_backward_simulation R C A = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
25 |
((!s:starts_of C. R``{s} <= starts_of A) & |
17233 | 26 |
(!s t t' a. reachable C s & |
62003 | 27 |
s \<midarrow>a\<midarrow>C\<rightarrow> t & |
17233 | 28 |
(t,t') : R |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
29 |
--> (? ex s'. (s,s'):R & move A ex s' a t')))" |
4565 | 30 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
31 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
32 |
is_forw_back_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
33 |
"is_forw_back_simulation R C A = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
34 |
((!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) & |
17233 | 35 |
(!s S' t a. reachable C s & |
62003 | 36 |
s \<midarrow>a\<midarrow>C\<rightarrow> t & |
17233 | 37 |
(s,S') : R |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
38 |
--> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t'))))" |
4565 | 39 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
40 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
41 |
is_back_forw_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
42 |
"is_back_forw_simulation R C A = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
43 |
((!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) & |
17233 | 44 |
(!s t T' a. reachable C s & |
62003 | 45 |
s \<midarrow>a\<midarrow>C\<rightarrow> t & |
17233 | 46 |
(t,T') : R |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
47 |
--> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t'))))" |
4565 | 48 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
49 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
50 |
is_history_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
51 |
"is_history_relation R C A = (is_simulation R C A & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
52 |
is_ref_map (%x.(@y. (x,y):(R^-1))) A C)" |
4565 | 53 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
54 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
55 |
is_prophecy_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
56 |
"is_prophecy_relation R C A = (is_backward_simulation R C A & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
57 |
is_ref_map (%x.(@y. (x,y):(R^-1))) A C)" |
17233 | 58 |
|
19741 | 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 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
69 |
lemma Sim_start_convert: |
19741 | 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 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
78 |
lemma ref_map_is_simulation: |
19741 | 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 |
|
17233 | 84 |
|
4565 | 85 |
end |