src/HOL/HOLCF/ex/Focus_ex.thy
 author wenzelm Mon, 10 Feb 2014 17:23:13 +0100 changeset 55381 ca31f042414f parent 51717 9e7d1c139569 child 62175 8ffc4d0e652d permissions -rw-r--r--
more explicit axiomatization;
```
(* 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 "~~/src/HOL/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\$(x,z) &
(!oy hz. (oy,hz) = f\$(x,hz) --> 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) =
(? f. is_f(f) &  (!x.(? z. (g\$x,z) = f\$(x,z) &
(! w y. (y,w) = f\$(x,w)  --> z << w))))"
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))))
=
(? f. is_f(f) &  (!x. ? z.
g\$x = fst (f\$(x,z)) &
z = snd (f\$(x,z)) &
(! w y.  (y,w) = f\$(x,w) --> 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 {* simp_tac (put_simpset HOL_ss @{context}
addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1 *})
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 {* 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 *})
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))
-->
(? g. def_g(g::'b stream -> 'c stream ))"