20 definition |
20 definition |
21 is_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where |
21 is_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where |
22 "is_ref_map f C A = |
22 "is_ref_map f C A = |
23 ((!s:starts_of(C). f(s):starts_of(A)) & |
23 ((!s:starts_of(C). f(s):starts_of(A)) & |
24 (!s t a. reachable C s & |
24 (!s t a. reachable C s & |
25 s -a--C-> t |
25 s \<midarrow>a\<midarrow>C\<rightarrow> t |
26 --> (? ex. move A ex (f s) a (f t))))" |
26 --> (? ex. move A ex (f s) a (f t))))" |
27 |
27 |
28 definition |
28 definition |
29 is_weak_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where |
29 is_weak_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where |
30 "is_weak_ref_map f C A = |
30 "is_weak_ref_map f C A = |
31 ((!s:starts_of(C). f(s):starts_of(A)) & |
31 ((!s:starts_of(C). f(s):starts_of(A)) & |
32 (!s t a. reachable C s & |
32 (!s t a. reachable C s & |
33 s -a--C-> t |
33 s \<midarrow>a\<midarrow>C\<rightarrow> t |
34 --> (if a:ext(C) |
34 --> (if a:ext(C) |
35 then (f s) -a--A-> (f t) |
35 then (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t) |
36 else (f s)=(f t))))" |
36 else (f s)=(f t))))" |
37 |
37 |
38 |
38 |
39 subsection "transitions and moves" |
39 subsection "transitions and moves" |
40 |
40 |
41 |
41 |
42 lemma transition_is_ex: "s -a--A-> t ==> ? ex. move A ex s a t" |
42 lemma transition_is_ex: "s \<midarrow>a\<midarrow>A\<rightarrow> t ==> ? ex. move A ex s a t" |
43 apply (rule_tac x = " (a,t) \<leadsto>nil" in exI) |
43 apply (rule_tac x = " (a,t) \<leadsto>nil" in exI) |
44 apply (simp add: move_def) |
44 apply (simp add: move_def) |
45 done |
45 done |
46 |
46 |
47 |
47 |
49 apply (rule_tac x = "nil" in exI) |
49 apply (rule_tac x = "nil" in exI) |
50 apply (simp add: move_def) |
50 apply (simp add: move_def) |
51 done |
51 done |
52 |
52 |
53 |
53 |
54 lemma ei_transitions_are_ex: "(s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) |
54 lemma ei_transitions_are_ex: "(s \<midarrow>a\<midarrow>A\<rightarrow> s') & (s' \<midarrow>a'\<midarrow>A\<rightarrow> s'') & (~a':ext A) |
55 ==> ? ex. move A ex s a s''" |
55 ==> ? ex. move A ex s a s''" |
56 apply (rule_tac x = " (a,s') \<leadsto> (a',s'') \<leadsto>nil" in exI) |
56 apply (rule_tac x = " (a,s') \<leadsto> (a',s'') \<leadsto>nil" in exI) |
57 apply (simp add: move_def) |
57 apply (simp add: move_def) |
58 done |
58 done |
59 |
59 |
60 |
60 |
61 lemma eii_transitions_are_ex: "(s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) & |
61 lemma eii_transitions_are_ex: "(s1 \<midarrow>a1\<midarrow>A\<rightarrow> s2) & (s2 \<midarrow>a2\<midarrow>A\<rightarrow> s3) & (s3 \<midarrow>a3\<midarrow>A\<rightarrow> s4) & |
62 (~a2:ext A) & (~a3:ext A) ==> |
62 (~a2:ext A) & (~a3:ext A) ==> |
63 ? ex. move A ex s1 a1 s4" |
63 ? ex. move A ex s1 a1 s4" |
64 apply (rule_tac x = " (a1,s2) \<leadsto> (a2,s3) \<leadsto> (a3,s4) \<leadsto>nil" in exI) |
64 apply (rule_tac x = " (a1,s2) \<leadsto> (a2,s3) \<leadsto> (a3,s4) \<leadsto>nil" in exI) |
65 apply (simp add: move_def) |
65 apply (simp add: move_def) |
66 done |
66 done |