src/HOLCF/ex/Focus_ex.thy
author huffman
Sat Oct 16 17:09:57 2010 -0700 (2010-10-16)
changeset 40028 9ee4e0ab2964
parent 40002 c5b5f7a3a3b1
permissions -rw-r--r--
remove old uses of 'simp_tac HOLCF_ss'
oheimb@2570
     1
(* Specification of the following loop back device
oheimb@2570
     2
oheimb@2570
     3
wenzelm@17291
     4
          g
oheimb@2570
     5
           --------------------
oheimb@2570
     6
          |      -------       |
oheimb@2570
     7
       x  |     |       |      |  y
wenzelm@17291
     8
    ------|---->|       |------| ----->
oheimb@2570
     9
          |  z  |   f   | z    |
oheimb@2570
    10
          |  -->|       |---   |
oheimb@2570
    11
          | |   |       |   |  |
oheimb@2570
    12
          | |    -------    |  |
oheimb@2570
    13
          | |               |  |
oheimb@2570
    14
          |  <--------------   |
wenzelm@17291
    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
wenzelm@17291
    23
        input  channel i1:'b i2: ('b,'c) tc
wenzelm@17291
    24
        output channel o1:'c o2: ('b,'c) tc
oheimb@2570
    25
is
wenzelm@17291
    26
        Rf(i1,i2,o1,o2)  (left open in the example)
oheimb@2570
    27
end f
oheimb@2570
    28
oheimb@2570
    29
agent g
wenzelm@17291
    30
        input  channel x:'b
wenzelm@17291
    31
        output channel y:'c
oheimb@2570
    32
is network
huffman@35916
    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
wenzelm@17291
    46
is_f :: ('b stream * ('b,'c) tc stream ->
wenzelm@17291
    47
                'c stream * ('b,'c) tc stream) => bool
oheimb@2570
    48
wenzelm@17291
    49
is_f f  = !i1 i2 o1 o2.
huffman@35916
    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) =>
wenzelm@17291
    56
            'b stream => 'c stream => bool
oheimb@2570
    57
wenzelm@17291
    58
is_net_g f x y =
huffman@35916
    59
        ? z. (y,z) = f$(x,z) &
huffman@35916
    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
nipkow@10835
    65
is_g g  = ? f. is_f f  & (!x y. g$x = y --> is_net_g f x y
wenzelm@17291
    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
wenzelm@17291
    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
wenzelm@17291
    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
wenzelm@17291
    85
def_g g  =
wenzelm@17291
    86
         (? f. is_f f  &
huffman@35916
    87
              g = (LAM x. fst (f$(x,fix$(LAM k. snd (f$(x,k)))))) )
wenzelm@17291
    88
oheimb@2570
    89
Now we prove:
oheimb@2570
    90
wenzelm@17291
    91
        (? f. is_f f ) --> (? g. is_g g)
oheimb@2570
    92
oheimb@2570
    93
using the theorems
oheimb@2570
    94
wenzelm@17291
    95
loopback_eq)    def_g = is_g                    (real work)
oheimb@2570
    96
wenzelm@17291
    97
L1)             (? f. is_f f ) --> (? g. def_g g)  (trivial)
oheimb@2570
    98
oheimb@2570
    99
*)
oheimb@2570
   100
wenzelm@17291
   101
theory Focus_ex
wenzelm@17291
   102
imports Stream
wenzelm@17291
   103
begin
oheimb@2570
   104
wenzelm@17291
   105
typedecl ('a, 'b) tc
wenzelm@17291
   106
arities tc:: (pcpo, pcpo) pcpo
oheimb@2570
   107
wenzelm@25135
   108
axiomatization
wenzelm@19763
   109
  Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
oheimb@2570
   110
wenzelm@19763
   111
definition
wenzelm@21404
   112
  is_f :: "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool" where
huffman@35916
   113
  "is_f f = (!i1 i2 o1 o2. f$(i1,i2) = (o1,o2) --> Rf(i1,i2,o1,o2))"
oheimb@2570
   114
wenzelm@21404
   115
definition
wenzelm@19763
   116
  is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
wenzelm@21404
   117
    'b stream => 'c stream => bool" where
wenzelm@19763
   118
  "is_net_g f x y == (? z.
huffman@35916
   119
                        (y,z) = f$(x,z) &
huffman@35916
   120
                        (!oy hz. (oy,hz) = f$(x,hz) --> z << hz))"
oheimb@2570
   121
wenzelm@21404
   122
definition
wenzelm@21404
   123
  is_g :: "('b stream -> 'c stream) => bool" where
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@21404
   126
definition
wenzelm@21404
   127
  def_g :: "('b stream -> 'c stream) => bool" where
huffman@35916
   128
  "def_g g == (? f. is_f f  & g = (LAM x. fst (f$(x,fix$(LAM  k. snd (f$(x,k)))))))"
wenzelm@17291
   129
wenzelm@19742
   130
wenzelm@19742
   131
(* first some logical trading *)
wenzelm@19742
   132
wenzelm@19742
   133
lemma lemma1:
wenzelm@19742
   134
"is_g(g) =
huffman@35916
   135
  (? f. is_f(f) &  (!x.(? z. (g$x,z) = f$(x,z) &
huffman@35916
   136
                   (! w y. (y,w) = f$(x,w)  --> z << w))))"
wenzelm@19763
   137
apply (simp add: is_g_def is_net_g_def)
wenzelm@19742
   138
apply fast
wenzelm@19742
   139
done
wenzelm@19742
   140
wenzelm@19742
   141
lemma lemma2:
huffman@35916
   142
"(? f. is_f(f) &  (!x. (? z. (g$x,z) = f$(x,z) &
huffman@35916
   143
                  (!w y. (y,w) = f$(x,w)  --> z << w))))
wenzelm@19742
   144
  =
wenzelm@19742
   145
  (? f. is_f(f) &  (!x. ? z.
huffman@35916
   146
        g$x = fst (f$(x,z)) &
huffman@35916
   147
          z = snd (f$(x,z)) &
huffman@35916
   148
        (! w y.  (y,w) = f$(x,w) --> z << w)))"
wenzelm@19742
   149
apply (rule iffI)
wenzelm@19742
   150
apply (erule exE)
wenzelm@19742
   151
apply (rule_tac x = "f" in exI)
wenzelm@19742
   152
apply (erule conjE)+
wenzelm@19742
   153
apply (erule conjI)
wenzelm@19742
   154
apply (intro strip)
wenzelm@19742
   155
apply (erule allE)
wenzelm@19742
   156
apply (erule exE)
wenzelm@19742
   157
apply (rule_tac x = "z" in exI)
wenzelm@19742
   158
apply (erule conjE)+
wenzelm@19742
   159
apply (rule conjI)
wenzelm@19742
   160
apply (rule_tac [2] conjI)
wenzelm@19742
   161
prefer 3 apply (assumption)
wenzelm@19742
   162
apply (drule sym)
huffman@40028
   163
apply (simp)
wenzelm@19742
   164
apply (drule sym)
huffman@40028
   165
apply (simp)
wenzelm@19742
   166
apply (erule exE)
wenzelm@19742
   167
apply (rule_tac x = "f" in exI)
wenzelm@19742
   168
apply (erule conjE)+
wenzelm@19742
   169
apply (erule conjI)
wenzelm@19742
   170
apply (intro strip)
wenzelm@19742
   171
apply (erule allE)
wenzelm@19742
   172
apply (erule exE)
wenzelm@19742
   173
apply (rule_tac x = "z" in exI)
wenzelm@19742
   174
apply (erule conjE)+
wenzelm@19742
   175
apply (rule conjI)
wenzelm@19742
   176
prefer 2 apply (assumption)
huffman@35916
   177
apply (rule prod_eqI)
huffman@35916
   178
apply simp
huffman@35916
   179
apply simp
wenzelm@19742
   180
done
wenzelm@19742
   181
wenzelm@19742
   182
lemma lemma3: "def_g(g) --> is_g(g)"
wenzelm@39159
   183
apply (tactic {* simp_tac (HOL_ss addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1 *})
wenzelm@19742
   184
apply (rule impI)
wenzelm@19742
   185
apply (erule exE)
wenzelm@19742
   186
apply (rule_tac x = "f" in exI)
wenzelm@19742
   187
apply (erule conjE)+
wenzelm@19742
   188
apply (erule conjI)
wenzelm@19742
   189
apply (intro strip)
huffman@35916
   190
apply (rule_tac x = "fix$ (LAM k. snd (f$(x,k)))" in exI)
wenzelm@19742
   191
apply (rule conjI)
huffman@40028
   192
 apply (simp)
huffman@35916
   193
 apply (rule prod_eqI, simp, simp)
wenzelm@19742
   194
 apply (rule trans)
wenzelm@19742
   195
  apply (rule fix_eq)
wenzelm@19742
   196
 apply (simp (no_asm))
wenzelm@19742
   197
apply (intro strip)
wenzelm@19742
   198
apply (rule fix_least)
wenzelm@19742
   199
apply (simp (no_asm))
wenzelm@19742
   200
apply (erule exE)
wenzelm@19742
   201
apply (drule sym)
wenzelm@19742
   202
back
wenzelm@19742
   203
apply simp
wenzelm@19742
   204
done
wenzelm@19742
   205
wenzelm@19742
   206
lemma lemma4: "is_g(g) --> def_g(g)"
haftmann@37598
   207
apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
wenzelm@39159
   208
  addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1 *})
wenzelm@19742
   209
apply (rule impI)
wenzelm@19742
   210
apply (erule exE)
wenzelm@19742
   211
apply (rule_tac x = "f" in exI)
wenzelm@19742
   212
apply (erule conjE)+
wenzelm@19742
   213
apply (erule conjI)
huffman@40002
   214
apply (rule cfun_eqI)
wenzelm@19742
   215
apply (erule_tac x = "x" in allE)
wenzelm@19742
   216
apply (erule exE)
wenzelm@19742
   217
apply (erule conjE)+
huffman@35916
   218
apply (subgoal_tac "fix$ (LAM k. snd (f$(x, k))) = z")
wenzelm@19742
   219
 apply simp
huffman@35916
   220
apply (subgoal_tac "! w y. f$(x, w) = (y, w) --> z << w")
wenzelm@19742
   221
apply (rule fix_eqI)
wenzelm@19742
   222
apply simp
huffman@35916
   223
apply (subgoal_tac "f$(x, za) = (fst (f$(x,za)) ,za)")
wenzelm@19742
   224
apply fast
huffman@35916
   225
apply (rule prod_eqI, simp, simp)
wenzelm@19742
   226
apply (intro strip)
wenzelm@19742
   227
apply (erule allE)+
wenzelm@19742
   228
apply (erule mp)
wenzelm@19742
   229
apply (erule sym)
wenzelm@19742
   230
done
wenzelm@19742
   231
wenzelm@19742
   232
(* now we assemble the result *)
wenzelm@19742
   233
wenzelm@19742
   234
lemma loopback_eq: "def_g = is_g"
wenzelm@19742
   235
apply (rule ext)
wenzelm@19742
   236
apply (rule iffI)
wenzelm@19742
   237
apply (erule lemma3 [THEN mp])
wenzelm@19742
   238
apply (erule lemma4 [THEN mp])
wenzelm@19742
   239
done
wenzelm@19742
   240
wenzelm@19742
   241
lemma L2:
wenzelm@19742
   242
"(? f.
wenzelm@19742
   243
  is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
wenzelm@19742
   244
  -->
wenzelm@19742
   245
  (? g. def_g(g::'b stream -> 'c stream ))"
wenzelm@19763
   246
apply (simp add: def_g_def)
wenzelm@19742
   247
done
wenzelm@19742
   248
wenzelm@19742
   249
theorem conservative_loopback:
wenzelm@19742
   250
"(? f.
wenzelm@19742
   251
  is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
wenzelm@19742
   252
  -->
wenzelm@19742
   253
  (? g. is_g(g::'b stream -> 'c stream ))"
wenzelm@19742
   254
apply (rule loopback_eq [THEN subst])
wenzelm@19742
   255
apply (rule L2)
wenzelm@19742
   256
done
oheimb@2570
   257
oheimb@2570
   258
end