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