(* Specification of the following loop back device
g
--------------------
| ------- |
x | | | | y
------|---->| |------| ----->
| z | f | z |
| -->| |--- |
| | | | | |
| | ------- | |
| | | |
| <-------------- |
| |
--------------------
First step: Notation in Agent Network Description Language (ANDL)
-----------------------------------------------------------------
agent f
input channel i1:'b i2: ('b,'c) tc
output channel o1:'c o2: ('b,'c) tc
is
Rf(i1,i2,o1,o2) (left open in the example)
end f
agent g
input channel x:'b
output channel y:'c
is network
(y,z) = f$(x,z)
end network
end g
Remark: the type of the feedback depends at most on the types of the input and
output of g. (No type miracles inside g)
Second step: Translation of ANDL specification to HOLCF Specification
---------------------------------------------------------------------
Specification of agent f ist translated to predicate is_f
is_f :: ('b stream * ('b,'c) tc stream ->
'c stream * ('b,'c) tc stream) => bool
is_f f = !i1 i2 o1 o2.
f$(i1,i2) = (o1,o2) --> Rf(i1,i2,o1,o2)
Specification of agent g is translated to predicate is_g which uses
predicate is_net_g
is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
'b stream => 'c stream => bool
is_net_g f x y =
? z. (y,z) = f$(x,z) &
!oy hz. (oy,hz) = f$(x,hz) --> z << hz
is_g :: ('b stream -> 'c stream) => bool
is_g g = ? f. is_f f & (!x y. g$x = y --> is_net_g f x y
Third step: (show conservativity)
-----------
Suppose we have a model for the theory TH1 which contains the axiom
? f. is_f f
In this case there is also a model for the theory TH2 that enriches TH1 by
axiom
? g. is_g g
The result is proved by showing that there is a definitional extension
that extends TH1 by a definition of g.
We define:
def_g g =
(? f. is_f f &
g = (LAM x. fst (f$(x,fix$(LAM k. snd (f$(x,k)))))) )
Now we prove:
(? f. is_f f ) --> (? g. is_g g)
using the theorems
loopback_eq) def_g = is_g (real work)
L1) (? f. is_f f ) --> (? g. def_g g) (trivial)
*)
theory Focus_ex
imports "HOLCF-Library.Stream"
begin
typedecl ('a, 'b) tc
axiomatization where tc_arity: "OFCLASS(('a::pcpo, 'b::pcpo) tc, pcop_class)"
instance tc :: (pcpo, pcpo) pcpo by (rule tc_arity)
axiomatization
Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) \ bool"
definition
is_f :: "('b stream * ('b,'c) tc stream \ 'c stream * ('b,'c) tc stream) \ bool" where
"is_f f \ (\i1 i2 o1 o2. f\(i1, i2) = (o1, o2) \ Rf (i1, i2, o1, o2))"
definition
is_net_g :: "('b stream * ('b,'c) tc stream \ 'c stream * ('b,'c) tc stream) \
'b stream \ 'c stream \ bool" where
"is_net_g f x y \ (\z.
(y, z) = f\<cdot>(x,z) \<and>
(\<forall>oy hz. (oy, hz) = f\<cdot>(x, hz) \<longrightarrow> z << hz))"
definition
is_g :: "('b stream \ 'c stream) \ bool" where
"is_g g \ (\f. is_f f \ (\x y. g\x = y \ is_net_g f x y))"
definition
def_g :: "('b stream \ 'c stream) => bool" where
"def_g g \ (\f. is_f f \ g = (LAM x. fst (f\(x, fix\(LAM k. snd (f\(x, k)))))))"
(* first some logical trading *)
lemma lemma1:
"is_g g \
(\<exists>f. is_f(f) \<and> (\<forall>x.(\<exists>z. (g\<cdot>x,z) = f\<cdot>(x,z) \<and> (\<forall>w y. (y, w) = f\<cdot>(x, w) \<longrightarrow> z << w))))"
apply (simp add: is_g_def is_net_g_def)
apply fast
done
lemma lemma2:
"(\f. is_f f \ (\x. (\z. (g\x, z) = f\(x, z) \ (\w y. (y, w) = f\(x,w) \ z << w)))) \
(\<exists>f. is_f f \<and> (\<forall>x. \<exists>z.
g\<cdot>x = fst (f\<cdot>(x, z)) \<and>
z = snd (f\<cdot>(x, z)) \<and>
(\<forall>w y. (y, w) = f\<cdot>(x, w) \<longrightarrow> z << w)))"
apply (rule iffI)
apply (erule exE)
apply (rule_tac x = "f" in exI)
apply (erule conjE)+
apply (erule conjI)
apply (intro strip)
apply (erule allE)
apply (erule exE)
apply (rule_tac x = "z" in exI)
apply (erule conjE)+
apply (rule conjI)
apply (rule_tac [2] conjI)
prefer 3 apply (assumption)
apply (drule sym)
apply (simp)
apply (drule sym)
apply (simp)
apply (erule exE)
apply (rule_tac x = "f" in exI)
apply (erule conjE)+
apply (erule conjI)
apply (intro strip)
apply (erule allE)
apply (erule exE)
apply (rule_tac x = "z" in exI)
apply (erule conjE)+
apply (rule conjI)
prefer 2 apply (assumption)
apply (rule prod_eqI)
apply simp
apply simp
done
lemma lemma3: "def_g g \ is_g g"
apply (tactic \<open>simp_tac (put_simpset HOL_ss \<^context>
addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1\<close>)
apply (rule impI)
apply (erule exE)
apply (rule_tac x = "f" in exI)
apply (erule conjE)+
apply (erule conjI)
apply (intro strip)
apply (rule_tac x = "fix\(LAM k. snd (f\(x, k)))" in exI)
apply (rule conjI)
apply (simp)
apply (rule prod_eqI, simp, simp)
apply (rule trans)
apply (rule fix_eq)
apply (simp (no_asm))
apply (intro strip)
apply (rule fix_least)
apply (simp (no_asm))
apply (erule exE)
apply (drule sym)
back
apply simp
done
lemma lemma4: "is_g g \ def_g g"
apply (tactic \<open>simp_tac (put_simpset HOL_ss \<^context>
delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1\<close>)
apply (rule impI)
apply (erule exE)
apply (rule_tac x = "f" in exI)
apply (erule conjE)+
apply (erule conjI)
apply (rule cfun_eqI)
apply (erule_tac x = "x" in allE)
apply (erule exE)
apply (erule conjE)+
apply (subgoal_tac "fix\(LAM k. snd (f\(x, k))) = z")
apply simp
apply (subgoal_tac "\w y. f\(x, w) = (y, w) \ z << w")
apply (rule fix_eqI)
apply simp
apply (subgoal_tac "f\(x, za) = (fst (f\(x, za)), za)")
apply fast
apply (rule prod_eqI, simp, simp)
apply (intro strip)
apply (erule allE)+
apply (erule mp)
apply (erule sym)
done
(* now we assemble the result *)
lemma loopback_eq: "def_g = is_g"
apply (rule ext)
apply (rule iffI)
apply (erule lemma3 [THEN mp])
apply (erule lemma4 [THEN mp])
done
lemma L2:
"(\f. is_f (f::'b stream * ('b,'c) tc stream \ 'c stream * ('b,'c) tc stream)) \
(\<exists>g. def_g (g::'b stream \<rightarrow> 'c stream))"
apply (simp add: def_g_def)
done
theorem conservative_loopback:
"(\f. is_f (f::'b stream * ('b,'c) tc stream \ 'c stream * ('b,'c) tc stream)) \
(\<exists>g. is_g (g::'b stream \<rightarrow> 'c stream))"
apply (rule loopback_eq [THEN subst])
apply (rule L2)
done
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
