src/HOLCF/ex/Focus_ex.thy
author wenzelm
Sun, 28 May 2006 20:53:03 +0200
changeset 19742 86f21beabafc
parent 17291 94f6113fe9ed
child 19763 ec18656a2c10
permissions -rw-r--r--
removed legacy ML scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
     1
(* $Id$ *)
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
     2
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     3
(* Specification of the following loop back device
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     4
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     5
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
     6
          g
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     7
           --------------------
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     8
          |      -------       |
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     9
       x  |     |       |      |  y
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    10
    ------|---->|       |------| ----->
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    11
          |  z  |   f   | z    |
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    12
          |  -->|       |---   |
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    13
          | |   |       |   |  |
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    14
          | |    -------    |  |
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    15
          | |               |  |
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    16
          |  <--------------   |
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    17
          |                    |
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    18
           --------------------
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    19
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    20
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    21
First step: Notation in Agent Network Description Language (ANDL)
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    22
-----------------------------------------------------------------
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    23
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    24
agent f
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    25
        input  channel i1:'b i2: ('b,'c) tc
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    26
        output channel o1:'c o2: ('b,'c) tc
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    27
is
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    28
        Rf(i1,i2,o1,o2)  (left open in the example)
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    29
end f
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    30
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    31
agent g
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    32
        input  channel x:'b
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    33
        output channel y:'c
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    34
is network
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    35
        <y,z> = f$<x,z>
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    36
end network
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    37
end g
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    38
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    39
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    40
Remark: the type of the feedback depends at most on the types of the input and
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    41
        output of g. (No type miracles inside g)
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    42
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    43
Second step: Translation of ANDL specification to HOLCF Specification
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    44
---------------------------------------------------------------------
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    45
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    46
Specification of agent f ist translated to predicate is_f
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    47
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    48
is_f :: ('b stream * ('b,'c) tc stream ->
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    49
                'c stream * ('b,'c) tc stream) => bool
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    50
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    51
is_f f  = !i1 i2 o1 o2.
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    52
        f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    53
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    54
Specification of agent g is translated to predicate is_g which uses
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    55
predicate is_net_g
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    56
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    57
is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    58
            'b stream => 'c stream => bool
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    59
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    60
is_net_g f x y =
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    61
        ? z. <y,z> = f$<x,z> &
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    62
        !oy hz. <oy,hz> = f$<x,hz> --> z << hz
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    63
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    64
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    65
is_g :: ('b stream -> 'c stream) => bool
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    66
10835
nipkow
parents: 3842
diff changeset
    67
is_g g  = ? f. is_f f  & (!x y. g$x = y --> is_net_g f x y
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    68
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    69
Third step: (show conservativity)
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    70
-----------
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    71
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    72
Suppose we have a model for the theory TH1 which contains the axiom
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    73
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    74
        ? f. is_f f
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    75
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    76
In this case there is also a model for the theory TH2 that enriches TH1 by
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    77
axiom
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    78
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    79
        ? g. is_g g
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    80
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    81
The result is proved by showing that there is a definitional extension
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    82
that extends TH1 by a definition of g.
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    83
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    84
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    85
We define:
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    86
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    87
def_g g  =
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    88
         (? f. is_f f  &
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    89
              g = (LAM x. cfst$(f$<x,fix$(LAM k.csnd$(f$<x,k>))>)) )
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    90
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    91
Now we prove:
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    92
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    93
        (? f. is_f f ) --> (? g. is_g g)
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    94
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    95
using the theorems
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    96
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    97
loopback_eq)    def_g = is_g                    (real work)
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    98
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    99
L1)             (? f. is_f f ) --> (? g. def_g g)  (trivial)
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   100
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   101
*)
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   102
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   103
theory Focus_ex
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   104
imports Stream
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   105
begin
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   106
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   107
typedecl ('a, 'b) tc
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   108
arities tc:: (pcpo, pcpo) pcpo
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   109
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   110
consts
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   111
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   112
is_f     ::
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   113
 "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   114
is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   115
            'b stream => 'c stream => bool"
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   116
is_g     :: "('b stream -> 'c stream) => bool"
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   117
def_g    :: "('b stream -> 'c stream) => bool"
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   118
Rf       ::
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   119
"('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   120
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   121
defs
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   122
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   123
is_f:           "is_f f == (!i1 i2 o1 o2.
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   124
                        f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   125
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   126
is_net_g:       "is_net_g f x y == (? z.
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   127
                        <y,z> = f$<x,z> &
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   128
                        (!oy hz. <oy,hz> = f$<x,hz> --> z << hz))"
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   129
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   130
is_g:           "is_g g  == (? f.
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   131
                        is_f f  &
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   132
                        (!x y. g$x = y --> is_net_g f x y))"
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   133
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   134
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   135
def_g:          "def_g g == (? f.
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   136
                        is_f f  &
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   137
                        g = (LAM x. cfst$(f$<x,fix$(LAM  k. csnd$(f$<x,k>))>)))"
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   138
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   139
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   140
(* first some logical trading *)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   141
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   142
lemma lemma1:
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   143
"is_g(g) =
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   144
  (? f. is_f(f) &  (!x.(? z. <g$x,z> = f$<x,z> &
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   145
                   (! w y. <y,w> = f$<x,w>  --> z << w))))"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   146
apply (simp add: is_g is_net_g)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   147
apply fast
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   148
done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   149
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   150
lemma lemma2:
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   151
"(? f. is_f(f) &  (!x. (? z. <g$x,z> = f$<x,z> &
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   152
                  (!w y. <y,w> = f$<x,w>  --> z << w))))
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   153
  =
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   154
  (? f. is_f(f) &  (!x. ? z.
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   155
        g$x = cfst$(f$<x,z>) &
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   156
          z = csnd$(f$<x,z>) &
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   157
        (! w y.  <y,w> = f$<x,w> --> z << w)))"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   158
apply (rule iffI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   159
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   160
apply (rule_tac x = "f" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   161
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   162
apply (erule conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   163
apply (intro strip)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   164
apply (erule allE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   165
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   166
apply (rule_tac x = "z" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   167
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   168
apply (rule conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   169
apply (rule_tac [2] conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   170
prefer 3 apply (assumption)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   171
apply (drule sym)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   172
apply (tactic "asm_simp_tac HOLCF_ss 1")
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   173
apply (drule sym)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   174
apply (tactic "asm_simp_tac HOLCF_ss 1")
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   175
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   176
apply (rule_tac x = "f" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   177
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   178
apply (erule conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   179
apply (intro strip)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   180
apply (erule allE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   181
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   182
apply (rule_tac x = "z" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   183
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   184
apply (rule conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   185
prefer 2 apply (assumption)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   186
apply (rule trans)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   187
apply (rule_tac [2] surjective_pairing_Cprod2)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   188
apply (erule subst)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   189
apply (erule subst)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   190
apply (rule refl)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   191
done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   192
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   193
lemma lemma3: "def_g(g) --> is_g(g)"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   194
apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g", thm "lemma1", thm "lemma2"]) 1 *})
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   195
apply (rule impI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   196
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   197
apply (rule_tac x = "f" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   198
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   199
apply (erule conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   200
apply (intro strip)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   201
apply (rule_tac x = "fix$ (LAM k. csnd$ (f$<x,k>))" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   202
apply (rule conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   203
 apply (tactic "asm_simp_tac HOLCF_ss 1")
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   204
 apply (rule trans)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   205
  apply (rule_tac [2] surjective_pairing_Cprod2)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   206
 apply (rule cfun_arg_cong)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   207
 apply (rule trans)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   208
  apply (rule fix_eq)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   209
 apply (simp (no_asm))
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   210
apply (intro strip)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   211
apply (rule fix_least)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   212
apply (simp (no_asm))
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   213
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   214
apply (drule sym)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   215
back
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   216
apply simp
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   217
done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   218
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   219
lemma lemma4: "is_g(g) --> def_g(g)"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   220
apply (tactic {* simp_tac (HOL_ss delsimps (thms "ex_simps" @ thms "all_simps")
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   221
  addsimps [thm "lemma1", thm "lemma2", thm "def_g"]) 1 *})
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   222
apply (rule impI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   223
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   224
apply (rule_tac x = "f" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   225
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   226
apply (erule conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   227
apply (rule ext_cfun)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   228
apply (erule_tac x = "x" in allE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   229
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   230
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   231
apply (subgoal_tac "fix$ (LAM k. csnd$ (f$<x, k>)) = z")
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   232
 apply simp
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   233
apply (subgoal_tac "! w y. f$<x, w> = <y, w> --> z << w")
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   234
apply (rule sym)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   235
apply (rule fix_eqI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   236
apply simp
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   237
apply (rule allI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   238
apply (tactic "simp_tac HOLCF_ss 1")
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   239
apply (intro strip)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   240
apply (subgoal_tac "f$<x, za> = <cfst$ (f$<x,za>) ,za>")
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   241
apply fast
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   242
apply (rule trans)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   243
apply (rule surjective_pairing_Cprod2 [symmetric])
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   244
apply (erule cfun_arg_cong)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   245
apply (intro strip)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   246
apply (erule allE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   247
apply (erule mp)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   248
apply (erule sym)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   249
done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   250
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   251
(* now we assemble the result *)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   252
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   253
lemma loopback_eq: "def_g = is_g"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   254
apply (rule ext)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   255
apply (rule iffI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   256
apply (erule lemma3 [THEN mp])
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   257
apply (erule lemma4 [THEN mp])
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   258
done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   259
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   260
lemma L2:
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   261
"(? f.
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   262
  is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   263
  -->
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   264
  (? g. def_g(g::'b stream -> 'c stream ))"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   265
apply (simp add: def_g)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   266
done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   267
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   268
theorem conservative_loopback:
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   269
"(? f.
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   270
  is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   271
  -->
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   272
  (? g. is_g(g::'b stream -> 'c stream ))"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   273
apply (rule loopback_eq [THEN subst])
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   274
apply (rule L2)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   275
done
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   276
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   277
end