src/HOLCF/ex/Focus_ex.thy
author oheimb
Fri Jan 31 16:56:32 1997 +0100 (1997-01-31)
changeset 2570 24d7e8fb8261
child 3842 b55686a7b22c
permissions -rw-r--r--
added Classlib.* and Witness.*,
moved (and updated) Coind.*, Dagstuhl.*, Dlist.*, Dnat.*, Focus_ex.*
and Stream.* from HOLCF/explicit_domains to here
adapted several proofs; now they work again.
Hope that the following strange errors (when committing) do not matter:
rlog error: RCS/Classlib.ML,v: No such file or directory
rlog error: RCS/Classlib.thy,v: No such file or directory
rlog error: RCS/Coind.ML,v: No such file or directory
rlog error: RCS/Coind.thy,v: No such file or directory
rlog error: RCS/Dagstuhl.ML,v: No such file or directory
rlog error: RCS/Dagstuhl.thy,v: No such file or directory
rlog error: RCS/Dlist.ML,v: No such file or directory
rlog error: RCS/Dlist.thy,v: No such file or directory
rlog error: RCS/Dnat.ML,v: No such file or directory
rlog error: RCS/Dnat.thy,v: No such file or directory
rlog error: RCS/Focus_ex.ML,v: No such file or directory
rlog error: RCS/Focus_ex.thy,v: No such file or directory
rlog error: RCS/Stream.ML,v: No such file or directory
rlog error: RCS/Stream.thy,v: No such file or directory
rlog error: RCS/Witness.ML,v: No such file or directory
rlog error: RCS/Witness.thy,v: No such file or directory
oheimb@2570
     1
(* Specification of the following loop back device
oheimb@2570
     2
oheimb@2570
     3
oheimb@2570
     4
          g 
oheimb@2570
     5
           --------------------
oheimb@2570
     6
          |      -------       |
oheimb@2570
     7
       x  |     |       |      |  y
oheimb@2570
     8
    ------|---->|       |------| ----->        
oheimb@2570
     9
          |  z  |   f   | z    |
oheimb@2570
    10
          |  -->|       |---   |
oheimb@2570
    11
          | |   |       |   |  |
oheimb@2570
    12
          | |    -------    |  |
oheimb@2570
    13
          | |               |  |
oheimb@2570
    14
          |  <--------------   |
oheimb@2570
    15
          |                    | 
oheimb@2570
    16
           --------------------
oheimb@2570
    17
oheimb@2570
    18
oheimb@2570
    19
First step: Notation in Agent Network Description Language (ANDL)
oheimb@2570
    20
-----------------------------------------------------------------
oheimb@2570
    21
oheimb@2570
    22
agent f
oheimb@2570
    23
	input  channel i1:'b i2: ('b,'c) tc
oheimb@2570
    24
	output channel o1:'c o2: ('b,'c) tc
oheimb@2570
    25
is
oheimb@2570
    26
	Rf(i1,i2,o1,o2)  (left open in the example)
oheimb@2570
    27
end f
oheimb@2570
    28
oheimb@2570
    29
agent g
oheimb@2570
    30
	input  channel x:'b 
oheimb@2570
    31
	output channel y:'c 
oheimb@2570
    32
is network
oheimb@2570
    33
	<y,z> = f`<x,z>
oheimb@2570
    34
end network
oheimb@2570
    35
end g
oheimb@2570
    36
oheimb@2570
    37
oheimb@2570
    38
Remark: the type of the feedback depends at most on the types of the input and
oheimb@2570
    39
        output of g. (No type miracles inside g)
oheimb@2570
    40
oheimb@2570
    41
Second step: Translation of ANDL specification to HOLCF Specification
oheimb@2570
    42
---------------------------------------------------------------------
oheimb@2570
    43
oheimb@2570
    44
Specification of agent f ist translated to predicate is_f
oheimb@2570
    45
oheimb@2570
    46
is_f :: ('b stream * ('b,'c) tc stream -> 
oheimb@2570
    47
		'c stream * ('b,'c) tc stream) => bool
oheimb@2570
    48
oheimb@2570
    49
is_f f  = !i1 i2 o1 o2. 
oheimb@2570
    50
	f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
oheimb@2570
    51
oheimb@2570
    52
Specification of agent g is translated to predicate is_g which uses
oheimb@2570
    53
predicate is_net_g
oheimb@2570
    54
oheimb@2570
    55
is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
oheimb@2570
    56
	    'b stream => 'c stream => bool
oheimb@2570
    57
oheimb@2570
    58
is_net_g f x y = 
oheimb@2570
    59
	? z. <y,z> = f`<x,z> & 
oheimb@2570
    60
	!oy hz. <oy,hz> = f`<x,hz> --> z << hz 
oheimb@2570
    61
oheimb@2570
    62
oheimb@2570
    63
is_g :: ('b stream -> 'c stream) => bool
oheimb@2570
    64
oheimb@2570
    65
is_g g  = ? f. is_f f  & (!x y. g`x = y --> is_net_g f x y
oheimb@2570
    66
	  
oheimb@2570
    67
Third step: (show conservativity)
oheimb@2570
    68
-----------
oheimb@2570
    69
oheimb@2570
    70
Suppose we have a model for the theory TH1 which contains the axiom
oheimb@2570
    71
oheimb@2570
    72
	? f. is_f f 
oheimb@2570
    73
oheimb@2570
    74
In this case there is also a model for the theory TH2 that enriches TH1 by
oheimb@2570
    75
axiom
oheimb@2570
    76
oheimb@2570
    77
	? g. is_g g 
oheimb@2570
    78
oheimb@2570
    79
The result is proved by showing that there is a definitional extension
oheimb@2570
    80
that extends TH1 by a definition of g.
oheimb@2570
    81
oheimb@2570
    82
oheimb@2570
    83
We define:
oheimb@2570
    84
oheimb@2570
    85
def_g g  = 
oheimb@2570
    86
         (? f. is_f f  & 
oheimb@2570
    87
	      g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)) )
oheimb@2570
    88
	
oheimb@2570
    89
Now we prove:
oheimb@2570
    90
oheimb@2570
    91
	(? f. is_f f ) --> (? g. is_g g) 
oheimb@2570
    92
oheimb@2570
    93
using the theorems
oheimb@2570
    94
oheimb@2570
    95
loopback_eq)	def_g = is_g			(real work) 
oheimb@2570
    96
oheimb@2570
    97
L1)		(? f. is_f f ) --> (? g. def_g g)  (trivial)
oheimb@2570
    98
oheimb@2570
    99
*)
oheimb@2570
   100
oheimb@2570
   101
Focus_ex = Stream +
oheimb@2570
   102
oheimb@2570
   103
types  tc 2
oheimb@2570
   104
oheimb@2570
   105
arities tc:: (pcpo,pcpo)pcpo
oheimb@2570
   106
oheimb@2570
   107
consts
oheimb@2570
   108
oheimb@2570
   109
is_f     ::
oheimb@2570
   110
 "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
oheimb@2570
   111
is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
oheimb@2570
   112
	    'b stream => 'c stream => bool"
oheimb@2570
   113
is_g     :: "('b stream -> 'c stream) => bool"
oheimb@2570
   114
def_g    :: "('b stream -> 'c stream) => bool"
oheimb@2570
   115
Rf	 :: 
oheimb@2570
   116
"('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
oheimb@2570
   117
oheimb@2570
   118
defs
oheimb@2570
   119
oheimb@2570
   120
is_f		"is_f f == (!i1 i2 o1 o2.
oheimb@2570
   121
			f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
oheimb@2570
   122
oheimb@2570
   123
is_net_g	"is_net_g f x y == (? z. 
oheimb@2570
   124
			<y,z> = f`<x,z> &
oheimb@2570
   125
			(!oy hz. <oy,hz> = f`<x,hz> --> z << hz))" 
oheimb@2570
   126
oheimb@2570
   127
is_g		"is_g g  == (? f.
oheimb@2570
   128
			is_f f  & 
oheimb@2570
   129
			(!x y. g`x = y --> is_net_g f x y))"
oheimb@2570
   130
oheimb@2570
   131
oheimb@2570
   132
def_g		"def_g g == (? f.
oheimb@2570
   133
			is_f f  & 
oheimb@2570
   134
	      		g = (LAM x. cfst`(f`<x,fix`(LAM  k.csnd`(f`<x,k>))>)))" 
oheimb@2570
   135
oheimb@2570
   136
end