src/HOLCF/ex/Focus_ex.thy
author wenzelm
Fri Jun 02 19:41:37 2006 +0200 (2006-06-02)
changeset 19763 ec18656a2c10
parent 19742 86f21beabafc
child 21404 eb85850d3eb7
permissions -rw-r--r--
tuned;
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
wenzelm@19763
   111
  Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
oheimb@2570
   112
wenzelm@19763
   113
definition
wenzelm@19763
   114
  is_f :: "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
wenzelm@19763
   115
  "is_f f = (!i1 i2 o1 o2. f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
oheimb@2570
   116
wenzelm@19763
   117
  is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
wenzelm@19763
   118
    'b stream => 'c stream => bool"
wenzelm@19763
   119
  "is_net_g f x y == (? z.
wenzelm@17291
   120
                        <y,z> = f$<x,z> &
wenzelm@17291
   121
                        (!oy hz. <oy,hz> = f$<x,hz> --> z << hz))"
oheimb@2570
   122
wenzelm@19763
   123
  is_g :: "('b stream -> 'c stream) => bool"
wenzelm@19763
   124
  "is_g g  == (? f. is_f f  & (!x y. g$x = y --> is_net_g f x y))"
oheimb@2570
   125
wenzelm@19763
   126
  def_g :: "('b stream -> 'c stream) => bool"
wenzelm@19763
   127
  "def_g g == (? f. is_f f  & g = (LAM x. cfst$(f$<x,fix$(LAM  k. csnd$(f$<x,k>))>)))"
wenzelm@17291
   128
wenzelm@19742
   129
wenzelm@19742
   130
(* first some logical trading *)
wenzelm@19742
   131
wenzelm@19742
   132
lemma lemma1:
wenzelm@19742
   133
"is_g(g) =
wenzelm@19742
   134
  (? f. is_f(f) &  (!x.(? z. <g$x,z> = f$<x,z> &
wenzelm@19742
   135
                   (! w y. <y,w> = f$<x,w>  --> z << w))))"
wenzelm@19763
   136
apply (simp add: is_g_def is_net_g_def)
wenzelm@19742
   137
apply fast
wenzelm@19742
   138
done
wenzelm@19742
   139
wenzelm@19742
   140
lemma lemma2:
wenzelm@19742
   141
"(? f. is_f(f) &  (!x. (? z. <g$x,z> = f$<x,z> &
wenzelm@19742
   142
                  (!w y. <y,w> = f$<x,w>  --> z << w))))
wenzelm@19742
   143
  =
wenzelm@19742
   144
  (? f. is_f(f) &  (!x. ? z.
wenzelm@19742
   145
        g$x = cfst$(f$<x,z>) &
wenzelm@19742
   146
          z = csnd$(f$<x,z>) &
wenzelm@19742
   147
        (! w y.  <y,w> = f$<x,w> --> z << w)))"
wenzelm@19742
   148
apply (rule iffI)
wenzelm@19742
   149
apply (erule exE)
wenzelm@19742
   150
apply (rule_tac x = "f" in exI)
wenzelm@19742
   151
apply (erule conjE)+
wenzelm@19742
   152
apply (erule conjI)
wenzelm@19742
   153
apply (intro strip)
wenzelm@19742
   154
apply (erule allE)
wenzelm@19742
   155
apply (erule exE)
wenzelm@19742
   156
apply (rule_tac x = "z" in exI)
wenzelm@19742
   157
apply (erule conjE)+
wenzelm@19742
   158
apply (rule conjI)
wenzelm@19742
   159
apply (rule_tac [2] conjI)
wenzelm@19742
   160
prefer 3 apply (assumption)
wenzelm@19742
   161
apply (drule sym)
wenzelm@19742
   162
apply (tactic "asm_simp_tac HOLCF_ss 1")
wenzelm@19742
   163
apply (drule sym)
wenzelm@19742
   164
apply (tactic "asm_simp_tac HOLCF_ss 1")
wenzelm@19742
   165
apply (erule exE)
wenzelm@19742
   166
apply (rule_tac x = "f" in exI)
wenzelm@19742
   167
apply (erule conjE)+
wenzelm@19742
   168
apply (erule conjI)
wenzelm@19742
   169
apply (intro strip)
wenzelm@19742
   170
apply (erule allE)
wenzelm@19742
   171
apply (erule exE)
wenzelm@19742
   172
apply (rule_tac x = "z" in exI)
wenzelm@19742
   173
apply (erule conjE)+
wenzelm@19742
   174
apply (rule conjI)
wenzelm@19742
   175
prefer 2 apply (assumption)
wenzelm@19742
   176
apply (rule trans)
wenzelm@19742
   177
apply (rule_tac [2] surjective_pairing_Cprod2)
wenzelm@19742
   178
apply (erule subst)
wenzelm@19742
   179
apply (erule subst)
wenzelm@19742
   180
apply (rule refl)
wenzelm@19742
   181
done
wenzelm@19742
   182
wenzelm@19742
   183
lemma lemma3: "def_g(g) --> is_g(g)"
wenzelm@19763
   184
apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g_def", thm "lemma1", thm "lemma2"]) 1 *})
wenzelm@19742
   185
apply (rule impI)
wenzelm@19742
   186
apply (erule exE)
wenzelm@19742
   187
apply (rule_tac x = "f" in exI)
wenzelm@19742
   188
apply (erule conjE)+
wenzelm@19742
   189
apply (erule conjI)
wenzelm@19742
   190
apply (intro strip)
wenzelm@19742
   191
apply (rule_tac x = "fix$ (LAM k. csnd$ (f$<x,k>))" in exI)
wenzelm@19742
   192
apply (rule conjI)
wenzelm@19742
   193
 apply (tactic "asm_simp_tac HOLCF_ss 1")
wenzelm@19742
   194
 apply (rule trans)
wenzelm@19742
   195
  apply (rule_tac [2] surjective_pairing_Cprod2)
wenzelm@19742
   196
 apply (rule cfun_arg_cong)
wenzelm@19742
   197
 apply (rule trans)
wenzelm@19742
   198
  apply (rule fix_eq)
wenzelm@19742
   199
 apply (simp (no_asm))
wenzelm@19742
   200
apply (intro strip)
wenzelm@19742
   201
apply (rule fix_least)
wenzelm@19742
   202
apply (simp (no_asm))
wenzelm@19742
   203
apply (erule exE)
wenzelm@19742
   204
apply (drule sym)
wenzelm@19742
   205
back
wenzelm@19742
   206
apply simp
wenzelm@19742
   207
done
wenzelm@19742
   208
wenzelm@19742
   209
lemma lemma4: "is_g(g) --> def_g(g)"
wenzelm@19742
   210
apply (tactic {* simp_tac (HOL_ss delsimps (thms "ex_simps" @ thms "all_simps")
wenzelm@19763
   211
  addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *})
wenzelm@19742
   212
apply (rule impI)
wenzelm@19742
   213
apply (erule exE)
wenzelm@19742
   214
apply (rule_tac x = "f" in exI)
wenzelm@19742
   215
apply (erule conjE)+
wenzelm@19742
   216
apply (erule conjI)
wenzelm@19742
   217
apply (rule ext_cfun)
wenzelm@19742
   218
apply (erule_tac x = "x" in allE)
wenzelm@19742
   219
apply (erule exE)
wenzelm@19742
   220
apply (erule conjE)+
wenzelm@19742
   221
apply (subgoal_tac "fix$ (LAM k. csnd$ (f$<x, k>)) = z")
wenzelm@19742
   222
 apply simp
wenzelm@19742
   223
apply (subgoal_tac "! w y. f$<x, w> = <y, w> --> z << w")
wenzelm@19742
   224
apply (rule sym)
wenzelm@19742
   225
apply (rule fix_eqI)
wenzelm@19742
   226
apply simp
wenzelm@19742
   227
apply (rule allI)
wenzelm@19742
   228
apply (tactic "simp_tac HOLCF_ss 1")
wenzelm@19742
   229
apply (intro strip)
wenzelm@19742
   230
apply (subgoal_tac "f$<x, za> = <cfst$ (f$<x,za>) ,za>")
wenzelm@19742
   231
apply fast
wenzelm@19742
   232
apply (rule trans)
wenzelm@19742
   233
apply (rule surjective_pairing_Cprod2 [symmetric])
wenzelm@19742
   234
apply (erule cfun_arg_cong)
wenzelm@19742
   235
apply (intro strip)
wenzelm@19742
   236
apply (erule allE)+
wenzelm@19742
   237
apply (erule mp)
wenzelm@19742
   238
apply (erule sym)
wenzelm@19742
   239
done
wenzelm@19742
   240
wenzelm@19742
   241
(* now we assemble the result *)
wenzelm@19742
   242
wenzelm@19742
   243
lemma loopback_eq: "def_g = is_g"
wenzelm@19742
   244
apply (rule ext)
wenzelm@19742
   245
apply (rule iffI)
wenzelm@19742
   246
apply (erule lemma3 [THEN mp])
wenzelm@19742
   247
apply (erule lemma4 [THEN mp])
wenzelm@19742
   248
done
wenzelm@19742
   249
wenzelm@19742
   250
lemma L2:
wenzelm@19742
   251
"(? f.
wenzelm@19742
   252
  is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
wenzelm@19742
   253
  -->
wenzelm@19742
   254
  (? g. def_g(g::'b stream -> 'c stream ))"
wenzelm@19763
   255
apply (simp add: def_g_def)
wenzelm@19742
   256
done
wenzelm@19742
   257
wenzelm@19742
   258
theorem conservative_loopback:
wenzelm@19742
   259
"(? f.
wenzelm@19742
   260
  is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
wenzelm@19742
   261
  -->
wenzelm@19742
   262
  (? g. is_g(g::'b stream -> 'c stream ))"
wenzelm@19742
   263
apply (rule loopback_eq [THEN subst])
wenzelm@19742
   264
apply (rule L2)
wenzelm@19742
   265
done
oheimb@2570
   266
oheimb@2570
   267
end