author | huffman |
Sun, 28 Feb 2010 14:55:42 -0800 | |
changeset 35473 | c4d3d65856dd |
parent 35174 | e15040ae75d7 |
child 35916 | d5c5fc1b993b |
permissions | -rw-r--r-- |
2570 | 1 |
(* Specification of the following loop back device |
2 |
||
3 |
||
17291 | 4 |
g |
2570 | 5 |
-------------------- |
6 |
| ------- | |
|
7 |
x | | | | y |
|
17291 | 8 |
------|---->| |------| -----> |
2570 | 9 |
| z | f | z | |
10 |
| -->| |--- | |
|
11 |
| | | | | | |
|
12 |
| | ------- | | |
|
13 |
| | | | |
|
14 |
| <-------------- | |
|
17291 | 15 |
| | |
2570 | 16 |
-------------------- |
17 |
||
18 |
||
19 |
First step: Notation in Agent Network Description Language (ANDL) |
|
20 |
----------------------------------------------------------------- |
|
21 |
||
22 |
agent f |
|
17291 | 23 |
input channel i1:'b i2: ('b,'c) tc |
24 |
output channel o1:'c o2: ('b,'c) tc |
|
2570 | 25 |
is |
17291 | 26 |
Rf(i1,i2,o1,o2) (left open in the example) |
2570 | 27 |
end f |
28 |
||
29 |
agent g |
|
17291 | 30 |
input channel x:'b |
31 |
output channel y:'c |
|
2570 | 32 |
is network |
17291 | 33 |
<y,z> = f$<x,z> |
2570 | 34 |
end network |
35 |
end g |
|
36 |
||
37 |
||
38 |
Remark: the type of the feedback depends at most on the types of the input and |
|
39 |
output of g. (No type miracles inside g) |
|
40 |
||
41 |
Second step: Translation of ANDL specification to HOLCF Specification |
|
42 |
--------------------------------------------------------------------- |
|
43 |
||
44 |
Specification of agent f ist translated to predicate is_f |
|
45 |
||
17291 | 46 |
is_f :: ('b stream * ('b,'c) tc stream -> |
47 |
'c stream * ('b,'c) tc stream) => bool |
|
2570 | 48 |
|
17291 | 49 |
is_f f = !i1 i2 o1 o2. |
50 |
f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2) |
|
2570 | 51 |
|
52 |
Specification of agent g is translated to predicate is_g which uses |
|
53 |
predicate is_net_g |
|
54 |
||
55 |
is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => |
|
17291 | 56 |
'b stream => 'c stream => bool |
2570 | 57 |
|
17291 | 58 |
is_net_g f x y = |
59 |
? z. <y,z> = f$<x,z> & |
|
60 |
!oy hz. <oy,hz> = f$<x,hz> --> z << hz |
|
2570 | 61 |
|
62 |
||
63 |
is_g :: ('b stream -> 'c stream) => bool |
|
64 |
||
10835 | 65 |
is_g g = ? f. is_f f & (!x y. g$x = y --> is_net_g f x y |
17291 | 66 |
|
2570 | 67 |
Third step: (show conservativity) |
68 |
----------- |
|
69 |
||
70 |
Suppose we have a model for the theory TH1 which contains the axiom |
|
71 |
||
17291 | 72 |
? f. is_f f |
2570 | 73 |
|
74 |
In this case there is also a model for the theory TH2 that enriches TH1 by |
|
75 |
axiom |
|
76 |
||
17291 | 77 |
? g. is_g g |
2570 | 78 |
|
79 |
The result is proved by showing that there is a definitional extension |
|
80 |
that extends TH1 by a definition of g. |
|
81 |
||
82 |
||
83 |
We define: |
|
84 |
||
17291 | 85 |
def_g g = |
86 |
(? f. is_f f & |
|
87 |
g = (LAM x. cfst$(f$<x,fix$(LAM k.csnd$(f$<x,k>))>)) ) |
|
88 |
||
2570 | 89 |
Now we prove: |
90 |
||
17291 | 91 |
(? f. is_f f ) --> (? g. is_g g) |
2570 | 92 |
|
93 |
using the theorems |
|
94 |
||
17291 | 95 |
loopback_eq) def_g = is_g (real work) |
2570 | 96 |
|
17291 | 97 |
L1) (? f. is_f f ) --> (? g. def_g g) (trivial) |
2570 | 98 |
|
99 |
*) |
|
100 |
||
17291 | 101 |
theory Focus_ex |
102 |
imports Stream |
|
103 |
begin |
|
2570 | 104 |
|
17291 | 105 |
typedecl ('a, 'b) tc |
106 |
arities tc:: (pcpo, pcpo) pcpo |
|
2570 | 107 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
21404
diff
changeset
|
108 |
axiomatization |
19763 | 109 |
Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool" |
2570 | 110 |
|
19763 | 111 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
112 |
is_f :: "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool" where |
19763 | 113 |
"is_f f = (!i1 i2 o1 o2. f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))" |
2570 | 114 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
115 |
definition |
19763 | 116 |
is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
117 |
'b stream => 'c stream => bool" where |
19763 | 118 |
"is_net_g f x y == (? z. |
17291 | 119 |
<y,z> = f$<x,z> & |
120 |
(!oy hz. <oy,hz> = f$<x,hz> --> z << hz))" |
|
2570 | 121 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
122 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
123 |
is_g :: "('b stream -> 'c stream) => bool" where |
19763 | 124 |
"is_g g == (? f. is_f f & (!x y. g$x = y --> is_net_g f x y))" |
2570 | 125 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
126 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset
|
127 |
def_g :: "('b stream -> 'c stream) => bool" where |
19763 | 128 |
"def_g g == (? f. is_f f & g = (LAM x. cfst$(f$<x,fix$(LAM k. csnd$(f$<x,k>))>)))" |
17291 | 129 |
|
19742 | 130 |
|
131 |
(* first some logical trading *) |
|
132 |
||
133 |
lemma lemma1: |
|
134 |
"is_g(g) = |
|
135 |
(? f. is_f(f) & (!x.(? z. <g$x,z> = f$<x,z> & |
|
136 |
(! w y. <y,w> = f$<x,w> --> z << w))))" |
|
19763 | 137 |
apply (simp add: is_g_def is_net_g_def) |
19742 | 138 |
apply fast |
139 |
done |
|
140 |
||
141 |
lemma lemma2: |
|
142 |
"(? f. is_f(f) & (!x. (? z. <g$x,z> = f$<x,z> & |
|
143 |
(!w y. <y,w> = f$<x,w> --> z << w)))) |
|
144 |
= |
|
145 |
(? f. is_f(f) & (!x. ? z. |
|
146 |
g$x = cfst$(f$<x,z>) & |
|
147 |
z = csnd$(f$<x,z>) & |
|
148 |
(! w y. <y,w> = f$<x,w> --> z << w)))" |
|
149 |
apply (rule iffI) |
|
150 |
apply (erule exE) |
|
151 |
apply (rule_tac x = "f" in exI) |
|
152 |
apply (erule conjE)+ |
|
153 |
apply (erule conjI) |
|
154 |
apply (intro strip) |
|
155 |
apply (erule allE) |
|
156 |
apply (erule exE) |
|
157 |
apply (rule_tac x = "z" in exI) |
|
158 |
apply (erule conjE)+ |
|
159 |
apply (rule conjI) |
|
160 |
apply (rule_tac [2] conjI) |
|
161 |
prefer 3 apply (assumption) |
|
162 |
apply (drule sym) |
|
163 |
apply (tactic "asm_simp_tac HOLCF_ss 1") |
|
164 |
apply (drule sym) |
|
165 |
apply (tactic "asm_simp_tac HOLCF_ss 1") |
|
166 |
apply (erule exE) |
|
167 |
apply (rule_tac x = "f" in exI) |
|
168 |
apply (erule conjE)+ |
|
169 |
apply (erule conjI) |
|
170 |
apply (intro strip) |
|
171 |
apply (erule allE) |
|
172 |
apply (erule exE) |
|
173 |
apply (rule_tac x = "z" in exI) |
|
174 |
apply (erule conjE)+ |
|
175 |
apply (rule conjI) |
|
176 |
prefer 2 apply (assumption) |
|
177 |
apply (rule trans) |
|
178 |
apply (rule_tac [2] surjective_pairing_Cprod2) |
|
179 |
apply (erule subst) |
|
180 |
apply (erule subst) |
|
181 |
apply (rule refl) |
|
182 |
done |
|
183 |
||
184 |
lemma lemma3: "def_g(g) --> is_g(g)" |
|
19763 | 185 |
apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g_def", thm "lemma1", thm "lemma2"]) 1 *}) |
19742 | 186 |
apply (rule impI) |
187 |
apply (erule exE) |
|
188 |
apply (rule_tac x = "f" in exI) |
|
189 |
apply (erule conjE)+ |
|
190 |
apply (erule conjI) |
|
191 |
apply (intro strip) |
|
192 |
apply (rule_tac x = "fix$ (LAM k. csnd$ (f$<x,k>))" in exI) |
|
193 |
apply (rule conjI) |
|
194 |
apply (tactic "asm_simp_tac HOLCF_ss 1") |
|
195 |
apply (rule trans) |
|
196 |
apply (rule_tac [2] surjective_pairing_Cprod2) |
|
197 |
apply (rule cfun_arg_cong) |
|
198 |
apply (rule trans) |
|
199 |
apply (rule fix_eq) |
|
200 |
apply (simp (no_asm)) |
|
201 |
apply (intro strip) |
|
202 |
apply (rule fix_least) |
|
203 |
apply (simp (no_asm)) |
|
204 |
apply (erule exE) |
|
205 |
apply (drule sym) |
|
206 |
back |
|
207 |
apply simp |
|
208 |
done |
|
209 |
||
210 |
lemma lemma4: "is_g(g) --> def_g(g)" |
|
211 |
apply (tactic {* simp_tac (HOL_ss delsimps (thms "ex_simps" @ thms "all_simps") |
|
19763 | 212 |
addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *}) |
19742 | 213 |
apply (rule impI) |
214 |
apply (erule exE) |
|
215 |
apply (rule_tac x = "f" in exI) |
|
216 |
apply (erule conjE)+ |
|
217 |
apply (erule conjI) |
|
218 |
apply (rule ext_cfun) |
|
219 |
apply (erule_tac x = "x" in allE) |
|
220 |
apply (erule exE) |
|
221 |
apply (erule conjE)+ |
|
222 |
apply (subgoal_tac "fix$ (LAM k. csnd$ (f$<x, k>)) = z") |
|
223 |
apply simp |
|
224 |
apply (subgoal_tac "! w y. f$<x, w> = <y, w> --> z << w") |
|
225 |
apply (rule fix_eqI) |
|
226 |
apply simp |
|
27185
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25135
diff
changeset
|
227 |
(*apply (rule allI)*) |
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25135
diff
changeset
|
228 |
(*apply (tactic "simp_tac HOLCF_ss 1")*) |
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25135
diff
changeset
|
229 |
(*apply (intro strip)*) |
19742 | 230 |
apply (subgoal_tac "f$<x, za> = <cfst$ (f$<x,za>) ,za>") |
231 |
apply fast |
|
232 |
apply (rule trans) |
|
233 |
apply (rule surjective_pairing_Cprod2 [symmetric]) |
|
27185
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25135
diff
changeset
|
234 |
apply (rule cfun_arg_cong) |
0407630909ef
change orientation of fix_eqI and convert to rule_format;
huffman
parents:
25135
diff
changeset
|
235 |
apply simp |
19742 | 236 |
apply (intro strip) |
237 |
apply (erule allE)+ |
|
238 |
apply (erule mp) |
|
239 |
apply (erule sym) |
|
240 |
done |
|
241 |
||
242 |
(* now we assemble the result *) |
|
243 |
||
244 |
lemma loopback_eq: "def_g = is_g" |
|
245 |
apply (rule ext) |
|
246 |
apply (rule iffI) |
|
247 |
apply (erule lemma3 [THEN mp]) |
|
248 |
apply (erule lemma4 [THEN mp]) |
|
249 |
done |
|
250 |
||
251 |
lemma L2: |
|
252 |
"(? f. |
|
253 |
is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream)) |
|
254 |
--> |
|
255 |
(? g. def_g(g::'b stream -> 'c stream ))" |
|
19763 | 256 |
apply (simp add: def_g_def) |
19742 | 257 |
done |
258 |
||
259 |
theorem conservative_loopback: |
|
260 |
"(? f. |
|
261 |
is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream)) |
|
262 |
--> |
|
263 |
(? g. is_g(g::'b stream -> 'c stream ))" |
|
264 |
apply (rule loopback_eq [THEN subst]) |
|
265 |
apply (rule L2) |
|
266 |
done |
|
2570 | 267 |
|
268 |
end |