src/HOLCF/ex/Focus_ex.thy
author wenzelm
Tue Sep 06 19:28:58 2005 +0200 (2005-09-06)
changeset 17291 94f6113fe9ed
parent 10835 f4745d77e620
child 19742 86f21beabafc
permissions -rw-r--r--
converted to Isar theory format;
wenzelm@17291
     1
(* $Id$ *)
wenzelm@17291
     2
oheimb@2570
     3
(* Specification of the following loop back device
oheimb@2570
     4
oheimb@2570
     5
wenzelm@17291
     6
          g
oheimb@2570
     7
           --------------------
oheimb@2570
     8
          |      -------       |
oheimb@2570
     9
       x  |     |       |      |  y
wenzelm@17291
    10
    ------|---->|       |------| ----->
oheimb@2570
    11
          |  z  |   f   | z    |
oheimb@2570
    12
          |  -->|       |---   |
oheimb@2570
    13
          | |   |       |   |  |
oheimb@2570
    14
          | |    -------    |  |
oheimb@2570
    15
          | |               |  |
oheimb@2570
    16
          |  <--------------   |
wenzelm@17291
    17
          |                    |
oheimb@2570
    18
           --------------------
oheimb@2570
    19
oheimb@2570
    20
oheimb@2570
    21
First step: Notation in Agent Network Description Language (ANDL)
oheimb@2570
    22
-----------------------------------------------------------------
oheimb@2570
    23
oheimb@2570
    24
agent f
wenzelm@17291
    25
        input  channel i1:'b i2: ('b,'c) tc
wenzelm@17291
    26
        output channel o1:'c o2: ('b,'c) tc
oheimb@2570
    27
is
wenzelm@17291
    28
        Rf(i1,i2,o1,o2)  (left open in the example)
oheimb@2570
    29
end f
oheimb@2570
    30
oheimb@2570
    31
agent g
wenzelm@17291
    32
        input  channel x:'b
wenzelm@17291
    33
        output channel y:'c
oheimb@2570
    34
is network
wenzelm@17291
    35
        <y,z> = f$<x,z>
oheimb@2570
    36
end network
oheimb@2570
    37
end g
oheimb@2570
    38
oheimb@2570
    39
oheimb@2570
    40
Remark: the type of the feedback depends at most on the types of the input and
oheimb@2570
    41
        output of g. (No type miracles inside g)
oheimb@2570
    42
oheimb@2570
    43
Second step: Translation of ANDL specification to HOLCF Specification
oheimb@2570
    44
---------------------------------------------------------------------
oheimb@2570
    45
oheimb@2570
    46
Specification of agent f ist translated to predicate is_f
oheimb@2570
    47
wenzelm@17291
    48
is_f :: ('b stream * ('b,'c) tc stream ->
wenzelm@17291
    49
                'c stream * ('b,'c) tc stream) => bool
oheimb@2570
    50
wenzelm@17291
    51
is_f f  = !i1 i2 o1 o2.
wenzelm@17291
    52
        f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
oheimb@2570
    53
oheimb@2570
    54
Specification of agent g is translated to predicate is_g which uses
oheimb@2570
    55
predicate is_net_g
oheimb@2570
    56
oheimb@2570
    57
is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
wenzelm@17291
    58
            'b stream => 'c stream => bool
oheimb@2570
    59
wenzelm@17291
    60
is_net_g f x y =
wenzelm@17291
    61
        ? z. <y,z> = f$<x,z> &
wenzelm@17291
    62
        !oy hz. <oy,hz> = f$<x,hz> --> z << hz
oheimb@2570
    63
oheimb@2570
    64
oheimb@2570
    65
is_g :: ('b stream -> 'c stream) => bool
oheimb@2570
    66
nipkow@10835
    67
is_g g  = ? f. is_f f  & (!x y. g$x = y --> is_net_g f x y
wenzelm@17291
    68
oheimb@2570
    69
Third step: (show conservativity)
oheimb@2570
    70
-----------
oheimb@2570
    71
oheimb@2570
    72
Suppose we have a model for the theory TH1 which contains the axiom
oheimb@2570
    73
wenzelm@17291
    74
        ? f. is_f f
oheimb@2570
    75
oheimb@2570
    76
In this case there is also a model for the theory TH2 that enriches TH1 by
oheimb@2570
    77
axiom
oheimb@2570
    78
wenzelm@17291
    79
        ? g. is_g g
oheimb@2570
    80
oheimb@2570
    81
The result is proved by showing that there is a definitional extension
oheimb@2570
    82
that extends TH1 by a definition of g.
oheimb@2570
    83
oheimb@2570
    84
oheimb@2570
    85
We define:
oheimb@2570
    86
wenzelm@17291
    87
def_g g  =
wenzelm@17291
    88
         (? f. is_f f  &
wenzelm@17291
    89
              g = (LAM x. cfst$(f$<x,fix$(LAM k.csnd$(f$<x,k>))>)) )
wenzelm@17291
    90
oheimb@2570
    91
Now we prove:
oheimb@2570
    92
wenzelm@17291
    93
        (? f. is_f f ) --> (? g. is_g g)
oheimb@2570
    94
oheimb@2570
    95
using the theorems
oheimb@2570
    96
wenzelm@17291
    97
loopback_eq)    def_g = is_g                    (real work)
oheimb@2570
    98
wenzelm@17291
    99
L1)             (? f. is_f f ) --> (? g. def_g g)  (trivial)
oheimb@2570
   100
oheimb@2570
   101
*)
oheimb@2570
   102
wenzelm@17291
   103
theory Focus_ex
wenzelm@17291
   104
imports Stream
wenzelm@17291
   105
begin
oheimb@2570
   106
wenzelm@17291
   107
typedecl ('a, 'b) tc
wenzelm@17291
   108
arities tc:: (pcpo, pcpo) pcpo
oheimb@2570
   109
oheimb@2570
   110
consts
oheimb@2570
   111
oheimb@2570
   112
is_f     ::
oheimb@2570
   113
 "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
oheimb@2570
   114
is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
wenzelm@17291
   115
            'b stream => 'c stream => bool"
oheimb@2570
   116
is_g     :: "('b stream -> 'c stream) => bool"
oheimb@2570
   117
def_g    :: "('b stream -> 'c stream) => bool"
wenzelm@17291
   118
Rf       ::
oheimb@2570
   119
"('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
oheimb@2570
   120
oheimb@2570
   121
defs
oheimb@2570
   122
wenzelm@17291
   123
is_f:           "is_f f == (!i1 i2 o1 o2.
wenzelm@17291
   124
                        f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
oheimb@2570
   125
wenzelm@17291
   126
is_net_g:       "is_net_g f x y == (? z.
wenzelm@17291
   127
                        <y,z> = f$<x,z> &
wenzelm@17291
   128
                        (!oy hz. <oy,hz> = f$<x,hz> --> z << hz))"
oheimb@2570
   129
wenzelm@17291
   130
is_g:           "is_g g  == (? f.
wenzelm@17291
   131
                        is_f f  &
wenzelm@17291
   132
                        (!x y. g$x = y --> is_net_g f x y))"
oheimb@2570
   133
oheimb@2570
   134
wenzelm@17291
   135
def_g:          "def_g g == (? f.
wenzelm@17291
   136
                        is_f f  &
wenzelm@17291
   137
                        g = (LAM x. cfst$(f$<x,fix$(LAM  k. csnd$(f$<x,k>))>)))"
wenzelm@17291
   138
wenzelm@17291
   139
ML {* use_legacy_bindings (the_context ()) *}
oheimb@2570
   140
oheimb@2570
   141
end