author  huffman 
Sat, 27 Nov 2010 16:08:10 0800  
changeset 40774  0437dbc127b3 
parent 40028  src/HOLCF/ex/Focus_ex.thy@9ee4e0ab2964 
child 41413  64cd30d6b0b8 
permissions  rwrr 
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 
35916  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. 
35916  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 = 
35916  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 & 

35916  87 
g = (LAM x. fst (f$(x,fix$(LAM k. snd (f$(x,k)))))) ) 
17291  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 
35916  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. 
35916  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 
35916  128 
"def_g g == (? f. is_f f & g = (LAM x. fst (f$(x,fix$(LAM k. snd (f$(x,k)))))))" 
17291  129 

19742  130 

131 
(* first some logical trading *) 

132 

133 
lemma lemma1: 

134 
"is_g(g) = 

35916  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: 

35916  142 
"(? f. is_f(f) & (!x. (? z. (g$x,z) = f$(x,z) & 
143 
(!w y. (y,w) = f$(x,w) > z << w)))) 

19742  144 
= 
145 
(? f. is_f(f) & (!x. ? z. 

35916  146 
g$x = fst (f$(x,z)) & 
147 
z = snd (f$(x,z)) & 

148 
(! w y. (y,w) = f$(x,w) > z << w)))" 

19742  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) 

40028  163 
apply (simp) 
19742  164 
apply (drule sym) 
40028  165 
apply (simp) 
19742  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) 

35916  177 
apply (rule prod_eqI) 
178 
apply simp 

179 
apply simp 

19742  180 
done 
181 

182 
lemma lemma3: "def_g(g) > is_g(g)" 

39159  183 
apply (tactic {* simp_tac (HOL_ss addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1 *}) 
19742  184 
apply (rule impI) 
185 
apply (erule exE) 

186 
apply (rule_tac x = "f" in exI) 

187 
apply (erule conjE)+ 

188 
apply (erule conjI) 

189 
apply (intro strip) 

35916  190 
apply (rule_tac x = "fix$ (LAM k. snd (f$(x,k)))" in exI) 
19742  191 
apply (rule conjI) 
40028  192 
apply (simp) 
35916  193 
apply (rule prod_eqI, simp, simp) 
19742  194 
apply (rule trans) 
195 
apply (rule fix_eq) 

196 
apply (simp (no_asm)) 

197 
apply (intro strip) 

198 
apply (rule fix_least) 

199 
apply (simp (no_asm)) 

200 
apply (erule exE) 

201 
apply (drule sym) 

202 
back 

203 
apply simp 

204 
done 

205 

206 
lemma lemma4: "is_g(g) > def_g(g)" 

37598  207 
apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps}) 
39159  208 
addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1 *}) 
19742  209 
apply (rule impI) 
210 
apply (erule exE) 

211 
apply (rule_tac x = "f" in exI) 

212 
apply (erule conjE)+ 

213 
apply (erule conjI) 

40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39159
diff
changeset

214 
apply (rule cfun_eqI) 
19742  215 
apply (erule_tac x = "x" in allE) 
216 
apply (erule exE) 

217 
apply (erule conjE)+ 

35916  218 
apply (subgoal_tac "fix$ (LAM k. snd (f$(x, k))) = z") 
19742  219 
apply simp 
35916  220 
apply (subgoal_tac "! w y. f$(x, w) = (y, w) > z << w") 
19742  221 
apply (rule fix_eqI) 
222 
apply simp 

35916  223 
apply (subgoal_tac "f$(x, za) = (fst (f$(x,za)) ,za)") 
19742  224 
apply fast 
35916  225 
apply (rule prod_eqI, simp, simp) 
19742  226 
apply (intro strip) 
227 
apply (erule allE)+ 

228 
apply (erule mp) 

229 
apply (erule sym) 

230 
done 

231 

232 
(* now we assemble the result *) 

233 

234 
lemma loopback_eq: "def_g = is_g" 

235 
apply (rule ext) 

236 
apply (rule iffI) 

237 
apply (erule lemma3 [THEN mp]) 

238 
apply (erule lemma4 [THEN mp]) 

239 
done 

240 

241 
lemma L2: 

242 
"(? f. 

243 
is_f(f::'b stream * ('b,'c) tc stream > 'c stream * ('b,'c) tc stream)) 

244 
> 

245 
(? g. def_g(g::'b stream > 'c stream ))" 

19763  246 
apply (simp add: def_g_def) 
19742  247 
done 
248 

249 
theorem conservative_loopback: 

250 
"(? f. 

251 
is_f(f::'b stream * ('b,'c) tc stream > 'c stream * ('b,'c) tc stream)) 

252 
> 

253 
(? g. is_g(g::'b stream > 'c stream ))" 

254 
apply (rule loopback_eq [THEN subst]) 

255 
apply (rule L2) 

256 
done 

2570  257 

258 
end 