src/HOL/HOLCF/ex/Focus_ex.thy
author wenzelm
Wed, 29 Dec 2010 17:34:41 +0100
changeset 41413 64cd30d6b0b8
parent 40774 0437dbc127b3
child 51717 9e7d1c139569
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     1
(* Specification of the following loop back device
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     2
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     3
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
     4
          g
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     5
           --------------------
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     6
          |      -------       |
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     7
       x  |     |       |      |  y
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
     8
    ------|---->|       |------| ----->
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     9
          |  z  |   f   | z    |
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    10
          |  -->|       |---   |
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    11
          | |   |       |   |  |
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
          |  <--------------   |
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    15
          |                    |
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    16
           --------------------
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    17
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    18
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    19
First step: Notation in Agent Network Description Language (ANDL)
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    20
-----------------------------------------------------------------
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    21
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    22
agent f
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    23
        input  channel i1:'b i2: ('b,'c) tc
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    24
        output channel o1:'c o2: ('b,'c) tc
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    25
is
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    26
        Rf(i1,i2,o1,o2)  (left open in the example)
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    27
end f
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    28
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    29
agent g
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    30
        input  channel x:'b
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    31
        output channel y:'c
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    32
is network
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
    33
        (y,z) = f$(x,z)
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    34
end network
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    35
end g
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    36
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    37
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    38
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
    39
        output of g. (No type miracles inside g)
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    40
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    41
Second step: Translation of ANDL specification to HOLCF Specification
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    42
---------------------------------------------------------------------
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    43
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    44
Specification of agent f ist translated to predicate is_f
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    45
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    46
is_f :: ('b stream * ('b,'c) tc stream ->
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    47
                'c stream * ('b,'c) tc stream) => bool
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    48
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    49
is_f f  = !i1 i2 o1 o2.
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
    50
        f$(i1,i2) = (o1,o2) --> Rf(i1,i2,o1,o2)
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    51
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    52
Specification of agent g is translated to predicate is_g which uses
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    53
predicate is_net_g
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    54
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    55
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
    56
            'b stream => 'c stream => bool
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    57
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    58
is_net_g f x y =
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
    59
        ? z. (y,z) = f$(x,z) &
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
    60
        !oy hz. (oy,hz) = f$(x,hz) --> z << hz
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    61
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    62
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    63
is_g :: ('b stream -> 'c stream) => bool
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    64
10835
nipkow
parents: 3842
diff changeset
    65
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
    66
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    67
Third step: (show conservativity)
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    68
-----------
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    69
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    70
Suppose we have a model for the theory TH1 which contains the axiom
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    71
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    72
        ? f. is_f f
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    73
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    74
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
    75
axiom
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    76
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    77
        ? g. is_g g
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    78
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    79
The result is proved by showing that there is a definitional extension
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    80
that extends TH1 by a definition of g.
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    81
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    82
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    83
We define:
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    84
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    85
def_g g  =
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    86
         (? f. is_f f  &
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
    87
              g = (LAM x. fst (f$(x,fix$(LAM k. snd (f$(x,k)))))) )
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    88
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    89
Now we prove:
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    90
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    91
        (? f. is_f f ) --> (? g. is_g g)
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    92
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    93
using the theorems
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    94
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    95
loopback_eq)    def_g = is_g                    (real work)
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    96
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    97
L1)             (? f. is_f f ) --> (? g. def_g g)  (trivial)
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    98
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    99
*)
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   100
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   101
theory Focus_ex
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 40774
diff changeset
   102
imports "~~/src/HOL/HOLCF/Library/Stream"
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   103
begin
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   104
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   105
typedecl ('a, 'b) tc
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   106
arities tc:: (pcpo, pcpo) pcpo
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   107
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 21404
diff changeset
   108
axiomatization
19763
wenzelm
parents: 19742
diff changeset
   109
  Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   110
19763
wenzelm
parents: 19742
diff changeset
   111
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
   112
  is_f :: "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool" where
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   113
  "is_f f = (!i1 i2 o1 o2. f$(i1,i2) = (o1,o2) --> Rf(i1,i2,o1,o2))"
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   114
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
   115
definition
19763
wenzelm
parents: 19742
diff changeset
   116
  is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
   117
    'b stream => 'c stream => bool" where
19763
wenzelm
parents: 19742
diff changeset
   118
  "is_net_g f x y == (? z.
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   119
                        (y,z) = f$(x,z) &
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   120
                        (!oy hz. (oy,hz) = f$(x,hz) --> z << hz))"
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   121
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
   122
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
   123
  is_g :: "('b stream -> 'c stream) => bool" where
19763
wenzelm
parents: 19742
diff changeset
   124
  "is_g g  == (? f. is_f f  & (!x y. g$x = y --> is_net_g f x y))"
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   125
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
   126
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
   127
  def_g :: "('b stream -> 'c stream) => bool" where
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   128
  "def_g g == (? f. is_f f  & g = (LAM x. fst (f$(x,fix$(LAM  k. snd (f$(x,k)))))))"
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
   129
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   130
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   131
(* first some logical trading *)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   132
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   133
lemma lemma1:
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   134
"is_g(g) =
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   135
  (? f. is_f(f) &  (!x.(? z. (g$x,z) = f$(x,z) &
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   136
                   (! w y. (y,w) = f$(x,w)  --> z << w))))"
19763
wenzelm
parents: 19742
diff changeset
   137
apply (simp add: is_g_def is_net_g_def)
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   138
apply fast
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   139
done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   140
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   141
lemma lemma2:
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   142
"(? f. is_f(f) &  (!x. (? z. (g$x,z) = f$(x,z) &
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   143
                  (!w y. (y,w) = f$(x,w)  --> z << w))))
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   144
  =
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   145
  (? f. is_f(f) &  (!x. ? z.
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   146
        g$x = fst (f$(x,z)) &
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   147
          z = snd (f$(x,z)) &
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   148
        (! w y.  (y,w) = f$(x,w) --> z << w)))"
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   149
apply (rule iffI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   150
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   151
apply (rule_tac x = "f" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   152
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   153
apply (erule conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   154
apply (intro strip)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   155
apply (erule allE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   156
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   157
apply (rule_tac x = "z" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   158
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   159
apply (rule conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   160
apply (rule_tac [2] conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   161
prefer 3 apply (assumption)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   162
apply (drule sym)
40028
9ee4e0ab2964 remove old uses of 'simp_tac HOLCF_ss'
huffman
parents: 40002
diff changeset
   163
apply (simp)
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   164
apply (drule sym)
40028
9ee4e0ab2964 remove old uses of 'simp_tac HOLCF_ss'
huffman
parents: 40002
diff changeset
   165
apply (simp)
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   166
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   167
apply (rule_tac x = "f" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   168
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   169
apply (erule conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   170
apply (intro strip)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   171
apply (erule allE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   172
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   173
apply (rule_tac x = "z" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   174
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   175
apply (rule conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   176
prefer 2 apply (assumption)
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   177
apply (rule prod_eqI)
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   178
apply simp
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   179
apply simp
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   180
done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   181
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   182
lemma lemma3: "def_g(g) --> is_g(g)"
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 37598
diff changeset
   183
apply (tactic {* simp_tac (HOL_ss addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1 *})
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   184
apply (rule impI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   185
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   186
apply (rule_tac x = "f" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   187
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   188
apply (erule conjI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   189
apply (intro strip)
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   190
apply (rule_tac x = "fix$ (LAM k. snd (f$(x,k)))" in exI)
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   191
apply (rule conjI)
40028
9ee4e0ab2964 remove old uses of 'simp_tac HOLCF_ss'
huffman
parents: 40002
diff changeset
   192
 apply (simp)
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   193
 apply (rule prod_eqI, simp, simp)
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   194
 apply (rule trans)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   195
  apply (rule fix_eq)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   196
 apply (simp (no_asm))
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   197
apply (intro strip)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   198
apply (rule fix_least)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   199
apply (simp (no_asm))
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   200
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   201
apply (drule sym)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   202
back
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   203
apply simp
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   204
done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   205
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   206
lemma lemma4: "is_g(g) --> def_g(g)"
37598
893dcabf0c04 explicit is better than implicit
haftmann
parents: 35916
diff changeset
   207
apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 37598
diff changeset
   208
  addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1 *})
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   209
apply (rule impI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   210
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   211
apply (rule_tac x = "f" in exI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   212
apply (erule conjE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   213
apply (erule conjI)
40002
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 39159
diff changeset
   214
apply (rule cfun_eqI)
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   215
apply (erule_tac x = "x" in allE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   216
apply (erule exE)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   217
apply (erule conjE)+
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   218
apply (subgoal_tac "fix$ (LAM k. snd (f$(x, k))) = z")
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   219
 apply simp
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   220
apply (subgoal_tac "! w y. f$(x, w) = (y, w) --> z << w")
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   221
apply (rule fix_eqI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   222
apply simp
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   223
apply (subgoal_tac "f$(x, za) = (fst (f$(x,za)) ,za)")
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   224
apply fast
35916
d5c5fc1b993b use Pair, fst, snd instead of cpair, cfst, csnd
huffman
parents: 35174
diff changeset
   225
apply (rule prod_eqI, simp, simp)
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   226
apply (intro strip)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   227
apply (erule allE)+
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   228
apply (erule mp)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   229
apply (erule sym)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   230
done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   231
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   232
(* now we assemble the result *)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   233
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   234
lemma loopback_eq: "def_g = is_g"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   235
apply (rule ext)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   236
apply (rule iffI)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   237
apply (erule lemma3 [THEN mp])
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   238
apply (erule lemma4 [THEN mp])
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   239
done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   240
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   241
lemma L2:
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   242
"(? f.
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   243
  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
   244
  -->
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   245
  (? g. def_g(g::'b stream -> 'c stream ))"
19763
wenzelm
parents: 19742
diff changeset
   246
apply (simp add: def_g_def)
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   247
done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   248
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   249
theorem conservative_loopback:
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   250
"(? f.
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   251
  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
   252
  -->
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   253
  (? g. is_g(g::'b stream -> 'c stream ))"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   254
apply (rule loopback_eq [THEN subst])
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   255
apply (rule L2)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
   256
done
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   257
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
   258
end