17291

1 
(* $Id$ *)


2 

2570

3 
(* Specification of the following loop back device


4 


5 

17291

6 
g

2570

7 



8 
  


9 
x     y

17291

10 
>  >

2570

11 
 z  f  z 


12 
 >  


13 
     


14 
    


15 
   


16 
 < 

17291

17 
 

2570

18 



19 


20 


21 
First step: Notation in Agent Network Description Language (ANDL)


22 



23 


24 
agent f

17291

25 
input channel i1:'b i2: ('b,'c) tc


26 
output channel o1:'c o2: ('b,'c) tc

2570

27 
is

17291

28 
Rf(i1,i2,o1,o2) (left open in the example)

2570

29 
end f


30 


31 
agent g

17291

32 
input channel x:'b


33 
output channel y:'c

2570

34 
is network

17291

35 
<y,z> = f$<x,z>

2570

36 
end network


37 
end g


38 


39 


40 
Remark: the type of the feedback depends at most on the types of the input and


41 
output of g. (No type miracles inside g)


42 


43 
Second step: Translation of ANDL specification to HOLCF Specification


44 



45 


46 
Specification of agent f ist translated to predicate is_f


47 

17291

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


49 
'c stream * ('b,'c) tc stream) => bool

2570

50 

17291

51 
is_f f = !i1 i2 o1 o2.


52 
f$<i1,i2> = <o1,o2> > Rf(i1,i2,o1,o2)

2570

53 


54 
Specification of agent g is translated to predicate is_g which uses


55 
predicate is_net_g


56 


57 
is_net_g :: ('b stream * ('b,'c) tc stream > 'c stream * ('b,'c) tc stream) =>

17291

58 
'b stream => 'c stream => bool

2570

59 

17291

60 
is_net_g f x y =


61 
? z. <y,z> = f$<x,z> &


62 
!oy hz. <oy,hz> = f$<x,hz> > z << hz

2570

63 


64 


65 
is_g :: ('b stream > 'c stream) => bool


66 

10835

67 
is_g g = ? f. is_f f & (!x y. g$x = y > is_net_g f x y

17291

68 

2570

69 
Third step: (show conservativity)


70 



71 


72 
Suppose we have a model for the theory TH1 which contains the axiom


73 

17291

74 
? f. is_f f

2570

75 


76 
In this case there is also a model for the theory TH2 that enriches TH1 by


77 
axiom


78 

17291

79 
? g. is_g g

2570

80 


81 
The result is proved by showing that there is a definitional extension


82 
that extends TH1 by a definition of g.


83 


84 


85 
We define:


86 

17291

87 
def_g g =


88 
(? f. is_f f &


89 
g = (LAM x. cfst$(f$<x,fix$(LAM k.csnd$(f$<x,k>))>)) )


90 

2570

91 
Now we prove:


92 

17291

93 
(? f. is_f f ) > (? g. is_g g)

2570

94 


95 
using the theorems


96 

17291

97 
loopback_eq) def_g = is_g (real work)

2570

98 

17291

99 
L1) (? f. is_f f ) > (? g. def_g g) (trivial)

2570

100 


101 
*)


102 

17291

103 
theory Focus_ex


104 
imports Stream


105 
begin

2570

106 

17291

107 
typedecl ('a, 'b) tc


108 
arities tc:: (pcpo, pcpo) pcpo

2570

109 


110 
consts


111 


112 
is_f ::


113 
"('b stream * ('b,'c) tc stream > 'c stream * ('b,'c) tc stream) => bool"


114 
is_net_g :: "('b stream *('b,'c) tc stream > 'c stream * ('b,'c) tc stream) =>

17291

115 
'b stream => 'c stream => bool"

2570

116 
is_g :: "('b stream > 'c stream) => bool"


117 
def_g :: "('b stream > 'c stream) => bool"

17291

118 
Rf ::

2570

119 
"('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"


120 


121 
defs


122 

17291

123 
is_f: "is_f f == (!i1 i2 o1 o2.


124 
f$<i1,i2> = <o1,o2> > Rf(i1,i2,o1,o2))"

2570

125 

17291

126 
is_net_g: "is_net_g f x y == (? z.


127 
<y,z> = f$<x,z> &


128 
(!oy hz. <oy,hz> = f$<x,hz> > z << hz))"

2570

129 

17291

130 
is_g: "is_g g == (? f.


131 
is_f f &


132 
(!x y. g$x = y > is_net_g f x y))"

2570

133 


134 

17291

135 
def_g: "def_g g == (? f.


136 
is_f f &


137 
g = (LAM x. cfst$(f$<x,fix$(LAM k. csnd$(f$<x,k>))>)))"


138 

19742

139 


140 
(* first some logical trading *)


141 


142 
lemma lemma1:


143 
"is_g(g) =


144 
(? f. is_f(f) & (!x.(? z. <g$x,z> = f$<x,z> &


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


146 
apply (simp add: is_g is_net_g)


147 
apply fast


148 
done


149 


150 
lemma lemma2:


151 
"(? f. is_f(f) & (!x. (? z. <g$x,z> = f$<x,z> &


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


153 
=


154 
(? f. is_f(f) & (!x. ? z.


155 
g$x = cfst$(f$<x,z>) &


156 
z = csnd$(f$<x,z>) &


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


158 
apply (rule iffI)


159 
apply (erule exE)


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


161 
apply (erule conjE)+


162 
apply (erule conjI)


163 
apply (intro strip)


164 
apply (erule allE)


165 
apply (erule exE)


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


167 
apply (erule conjE)+


168 
apply (rule conjI)


169 
apply (rule_tac [2] conjI)


170 
prefer 3 apply (assumption)


171 
apply (drule sym)


172 
apply (tactic "asm_simp_tac HOLCF_ss 1")


173 
apply (drule sym)


174 
apply (tactic "asm_simp_tac HOLCF_ss 1")


175 
apply (erule exE)


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


177 
apply (erule conjE)+


178 
apply (erule conjI)


179 
apply (intro strip)


180 
apply (erule allE)


181 
apply (erule exE)


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


183 
apply (erule conjE)+


184 
apply (rule conjI)


185 
prefer 2 apply (assumption)


186 
apply (rule trans)


187 
apply (rule_tac [2] surjective_pairing_Cprod2)


188 
apply (erule subst)


189 
apply (erule subst)


190 
apply (rule refl)


191 
done


192 


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


194 
apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g", thm "lemma1", thm "lemma2"]) 1 *})


195 
apply (rule impI)


196 
apply (erule exE)


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


198 
apply (erule conjE)+


199 
apply (erule conjI)


200 
apply (intro strip)


201 
apply (rule_tac x = "fix$ (LAM k. csnd$ (f$<x,k>))" in exI)


202 
apply (rule conjI)


203 
apply (tactic "asm_simp_tac HOLCF_ss 1")


204 
apply (rule trans)


205 
apply (rule_tac [2] surjective_pairing_Cprod2)


206 
apply (rule cfun_arg_cong)


207 
apply (rule trans)


208 
apply (rule fix_eq)


209 
apply (simp (no_asm))


210 
apply (intro strip)


211 
apply (rule fix_least)


212 
apply (simp (no_asm))


213 
apply (erule exE)


214 
apply (drule sym)


215 
back


216 
apply simp


217 
done


218 


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


220 
apply (tactic {* simp_tac (HOL_ss delsimps (thms "ex_simps" @ thms "all_simps")


221 
addsimps [thm "lemma1", thm "lemma2", thm "def_g"]) 1 *})


222 
apply (rule impI)


223 
apply (erule exE)


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


225 
apply (erule conjE)+


226 
apply (erule conjI)


227 
apply (rule ext_cfun)


228 
apply (erule_tac x = "x" in allE)


229 
apply (erule exE)


230 
apply (erule conjE)+


231 
apply (subgoal_tac "fix$ (LAM k. csnd$ (f$<x, k>)) = z")


232 
apply simp


233 
apply (subgoal_tac "! w y. f$<x, w> = <y, w> > z << w")


234 
apply (rule sym)


235 
apply (rule fix_eqI)


236 
apply simp


237 
apply (rule allI)


238 
apply (tactic "simp_tac HOLCF_ss 1")


239 
apply (intro strip)


240 
apply (subgoal_tac "f$<x, za> = <cfst$ (f$<x,za>) ,za>")


241 
apply fast


242 
apply (rule trans)


243 
apply (rule surjective_pairing_Cprod2 [symmetric])


244 
apply (erule cfun_arg_cong)


245 
apply (intro strip)


246 
apply (erule allE)+


247 
apply (erule mp)


248 
apply (erule sym)


249 
done


250 


251 
(* now we assemble the result *)


252 


253 
lemma loopback_eq: "def_g = is_g"


254 
apply (rule ext)


255 
apply (rule iffI)


256 
apply (erule lemma3 [THEN mp])


257 
apply (erule lemma4 [THEN mp])


258 
done


259 


260 
lemma L2:


261 
"(? f.


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


263 
>


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


265 
apply (simp add: def_g)


266 
done


267 


268 
theorem conservative_loopback:


269 
"(? f.


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


271 
>


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


273 
apply (rule loopback_eq [THEN subst])


274 
apply (rule L2)


275 
done

2570

276 


277 
end
