author  wenzelm 
Mon, 10 Feb 2014 17:23:13 +0100  
changeset 55381  ca31f042414f 
parent 51717  9e7d1c139569 
child 62175  8ffc4d0e652d 
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 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
40774
diff
changeset

102 
imports "~~/src/HOL/HOLCF/Library/Stream" 
17291  103 
begin 
2570  104 

17291  105 
typedecl ('a, 'b) tc 
55381  106 
axiomatization where tc_arity: "OFCLASS(('a::pcpo, 'b::pcpo) tc, pcop_class)" 
107 
instance tc :: (pcpo, pcpo) pcpo by (rule tc_arity) 

2570  108 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
21404
diff
changeset

109 
axiomatization 
19763  110 
Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool" 
2570  111 

19763  112 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

113 
is_f :: "('b stream * ('b,'c) tc stream > 'c stream * ('b,'c) tc stream) => bool" where 
35916  114 
"is_f f = (!i1 i2 o1 o2. f$(i1,i2) = (o1,o2) > Rf(i1,i2,o1,o2))" 
2570  115 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

116 
definition 
19763  117 
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

118 
'b stream => 'c stream => bool" where 
19763  119 
"is_net_g f x y == (? z. 
35916  120 
(y,z) = f$(x,z) & 
121 
(!oy hz. (oy,hz) = f$(x,hz) > z << hz))" 

2570  122 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

123 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

124 
is_g :: "('b stream > 'c stream) => bool" where 
19763  125 
"is_g g == (? f. is_f f & (!x y. g$x = y > is_net_g f x y))" 
2570  126 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

127 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

128 
def_g :: "('b stream > 'c stream) => bool" where 
35916  129 
"def_g g == (? f. is_f f & g = (LAM x. fst (f$(x,fix$(LAM k. snd (f$(x,k)))))))" 
17291  130 

19742  131 

132 
(* first some logical trading *) 

133 

134 
lemma lemma1: 

135 
"is_g(g) = 

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

19763  138 
apply (simp add: is_g_def is_net_g_def) 
19742  139 
apply fast 
140 
done 

141 

142 
lemma lemma2: 

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

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

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

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

19742  150 
apply (rule iffI) 
151 
apply (erule exE) 

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

153 
apply (erule conjE)+ 

154 
apply (erule conjI) 

155 
apply (intro strip) 

156 
apply (erule allE) 

157 
apply (erule exE) 

158 
apply (rule_tac x = "z" in exI) 

159 
apply (erule conjE)+ 

160 
apply (rule conjI) 

161 
apply (rule_tac [2] conjI) 

162 
prefer 3 apply (assumption) 

163 
apply (drule sym) 

40028  164 
apply (simp) 
19742  165 
apply (drule sym) 
40028  166 
apply (simp) 
19742  167 
apply (erule exE) 
168 
apply (rule_tac x = "f" in exI) 

169 
apply (erule conjE)+ 

170 
apply (erule conjI) 

171 
apply (intro strip) 

172 
apply (erule allE) 

173 
apply (erule exE) 

174 
apply (rule_tac x = "z" in exI) 

175 
apply (erule conjE)+ 

176 
apply (rule conjI) 

177 
prefer 2 apply (assumption) 

35916  178 
apply (rule prod_eqI) 
179 
apply simp 

180 
apply simp 

19742  181 
done 
182 

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

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
41413
diff
changeset

184 
apply (tactic {* simp_tac (put_simpset HOL_ss @{context} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
41413
diff
changeset

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

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

198 
apply (simp (no_asm)) 

199 
apply (intro strip) 

200 
apply (rule fix_least) 

201 
apply (simp (no_asm)) 

202 
apply (erule exE) 

203 
apply (drule sym) 

204 
back 

205 
apply simp 

206 
done 

207 

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

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
41413
diff
changeset

209 
apply (tactic {* simp_tac (put_simpset HOL_ss @{context} 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
41413
diff
changeset

210 
delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps}) 
39159  211 
addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1 *}) 
19742  212 
apply (rule impI) 
213 
apply (erule exE) 

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

215 
apply (erule conjE)+ 

216 
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

217 
apply (rule cfun_eqI) 
19742  218 
apply (erule_tac x = "x" in allE) 
219 
apply (erule exE) 

220 
apply (erule conjE)+ 

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

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

231 
apply (erule mp) 

232 
apply (erule sym) 

233 
done 

234 

235 
(* now we assemble the result *) 

236 

237 
lemma loopback_eq: "def_g = is_g" 

238 
apply (rule ext) 

239 
apply (rule iffI) 

240 
apply (erule lemma3 [THEN mp]) 

241 
apply (erule lemma4 [THEN mp]) 

242 
done 

243 

244 
lemma L2: 

245 
"(? f. 

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

247 
> 

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

19763  249 
apply (simp add: def_g_def) 
19742  250 
done 
251 

252 
theorem conservative_loopback: 

253 
"(? f. 

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

255 
> 

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

257 
apply (rule loopback_eq [THEN subst]) 

258 
apply (rule L2) 

259 
done 

2570  260 

261 
end 