|
1 (* Title: HOL/HOLCF/IOA/RefMappings.thy |
|
2 Author: Olaf Müller |
|
3 *) |
|
4 |
|
5 section \<open>Refinement Mappings in HOLCF/IOA\<close> |
|
6 |
|
7 theory RefMappings |
|
8 imports Traces |
|
9 begin |
|
10 |
|
11 default_sort type |
|
12 |
|
13 definition |
|
14 move :: "[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" where |
|
15 "move ioa ex s a t = |
|
16 (is_exec_frag ioa (s,ex) & Finite ex & |
|
17 laststate (s,ex)=t & |
|
18 mk_trace ioa$ex = (if a:ext(ioa) then a\<leadsto>nil else nil))" |
|
19 |
|
20 definition |
|
21 is_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where |
|
22 "is_ref_map f C A = |
|
23 ((!s:starts_of(C). f(s):starts_of(A)) & |
|
24 (!s t a. reachable C s & |
|
25 s \<midarrow>a\<midarrow>C\<rightarrow> t |
|
26 --> (? ex. move A ex (f s) a (f t))))" |
|
27 |
|
28 definition |
|
29 is_weak_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where |
|
30 "is_weak_ref_map f C A = |
|
31 ((!s:starts_of(C). f(s):starts_of(A)) & |
|
32 (!s t a. reachable C s & |
|
33 s \<midarrow>a\<midarrow>C\<rightarrow> t |
|
34 --> (if a:ext(C) |
|
35 then (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t) |
|
36 else (f s)=(f t))))" |
|
37 |
|
38 |
|
39 subsection "transitions and moves" |
|
40 |
|
41 |
|
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) |
|
44 apply (simp add: move_def) |
|
45 done |
|
46 |
|
47 |
|
48 lemma nothing_is_ex: "(~a:ext A) & s=t ==> ? ex. move A ex s a t" |
|
49 apply (rule_tac x = "nil" in exI) |
|
50 apply (simp add: move_def) |
|
51 done |
|
52 |
|
53 |
|
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''" |
|
56 apply (rule_tac x = " (a,s') \<leadsto> (a',s'') \<leadsto>nil" in exI) |
|
57 apply (simp add: move_def) |
|
58 done |
|
59 |
|
60 |
|
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) ==> |
|
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) |
|
65 apply (simp add: move_def) |
|
66 done |
|
67 |
|
68 |
|
69 subsection "weak_ref_map and ref_map" |
|
70 |
|
71 lemma weak_ref_map2ref_map: |
|
72 "[| ext C = ext A; |
|
73 is_weak_ref_map f C A |] ==> is_ref_map f C A" |
|
74 apply (unfold is_weak_ref_map_def is_ref_map_def) |
|
75 apply auto |
|
76 apply (case_tac "a:ext A") |
|
77 apply (auto intro: transition_is_ex nothing_is_ex) |
|
78 done |
|
79 |
|
80 |
|
81 lemma imp_conj_lemma: "(P ==> Q-->R) ==> P&Q --> R" |
|
82 by blast |
|
83 |
|
84 declare split_if [split del] |
|
85 declare if_weak_cong [cong del] |
|
86 |
|
87 lemma rename_through_pmap: "[| is_weak_ref_map f C A |] |
|
88 ==> (is_weak_ref_map f (rename C g) (rename A g))" |
|
89 apply (simp add: is_weak_ref_map_def) |
|
90 apply (rule conjI) |
|
91 (* 1: start states *) |
|
92 apply (simp add: rename_def rename_set_def starts_of_def) |
|
93 (* 2: reachable transitions *) |
|
94 apply (rule allI)+ |
|
95 apply (rule imp_conj_lemma) |
|
96 apply (simp (no_asm) add: rename_def rename_set_def) |
|
97 apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def) |
|
98 apply safe |
|
99 apply (simplesubst split_if) |
|
100 apply (rule conjI) |
|
101 apply (rule impI) |
|
102 apply (erule disjE) |
|
103 apply (erule exE) |
|
104 apply (erule conjE) |
|
105 (* x is input *) |
|
106 apply (drule sym) |
|
107 apply (drule sym) |
|
108 apply simp |
|
109 apply hypsubst+ |
|
110 apply (frule reachable_rename) |
|
111 apply simp |
|
112 (* x is output *) |
|
113 apply (erule exE) |
|
114 apply (erule conjE) |
|
115 apply (drule sym) |
|
116 apply (drule sym) |
|
117 apply simp |
|
118 apply hypsubst+ |
|
119 apply (frule reachable_rename) |
|
120 apply simp |
|
121 (* x is internal *) |
|
122 apply (frule reachable_rename) |
|
123 apply auto |
|
124 done |
|
125 |
|
126 declare split_if [split] |
|
127 declare if_weak_cong [cong] |
|
128 |
|
129 end |