src/HOLCF/FOCUS/Fstreams.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 21210 c17fd2df4e9e
child 24107 fecafd71e758
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
oheimb@15188
     1
(*  Title: 	HOLCF/FOCUS/Fstreams.thy
oheimb@15188
     2
    ID:         $Id$
oheimb@15188
     3
    Author: 	Borislav Gajanovic
oheimb@15188
     4
oheimb@15188
     5
FOCUS flat streams (with lifted elements)
oheimb@15188
     6
###TODO: integrate this with Fstream.*
oheimb@15188
     7
*)
oheimb@15188
     8
haftmann@16417
     9
theory Fstreams imports Stream begin
oheimb@15188
    10
oheimb@15188
    11
defaultsort type
oheimb@15188
    12
oheimb@15188
    13
types 'a fstream = "('a lift) stream"
oheimb@15188
    14
wenzelm@19763
    15
definition
wenzelm@21404
    16
  fsingleton    :: "'a => 'a fstream"  ("<_>" [1000] 999) where
wenzelm@19763
    17
  fsingleton_def2: "fsingleton = (%a. Def a && UU)"
wenzelm@19763
    18
wenzelm@21404
    19
definition
wenzelm@21404
    20
  fsfilter      :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where
wenzelm@19763
    21
  "fsfilter A = sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))"
wenzelm@19763
    22
wenzelm@21404
    23
definition
wenzelm@21404
    24
  fsmap		:: "('a => 'b) => 'a fstream -> 'b fstream" where
wenzelm@19763
    25
  "fsmap f = smap$(flift2 f)"
oheimb@15188
    26
wenzelm@21404
    27
definition
wenzelm@21404
    28
  jth           :: "nat => 'a fstream => 'a" where
wenzelm@19763
    29
  "jth = (%n s. if Fin n < #s then THE a. i_th n s = Def a else arbitrary)"
oheimb@15188
    30
wenzelm@21404
    31
definition
wenzelm@21404
    32
  first         :: "'a fstream => 'a" where
wenzelm@19763
    33
  "first = (%s. jth 0 s)"
wenzelm@19763
    34
wenzelm@21404
    35
definition
wenzelm@21404
    36
  last          :: "'a fstream => 'a" where
wenzelm@19763
    37
  "last = (%s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else arbitrary)
wenzelm@19763
    38
              | Infty => arbitrary)"
oheimb@15188
    39
oheimb@15188
    40
wenzelm@19763
    41
abbreviation
wenzelm@21404
    42
  emptystream :: "'a fstream"  ("<>") where
wenzelm@19763
    43
  "<> == \<bottom>"
wenzelm@21404
    44
wenzelm@21404
    45
abbreviation
wenzelm@21404
    46
  fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"	("(_'(C')_)" [64,63] 63) where
wenzelm@19763
    47
  "A(C)s == fsfilter A\<cdot>s"
oheimb@15188
    48
wenzelm@21210
    49
notation (xsymbols)
wenzelm@19763
    50
  fsfilter'  ("(_\<copyright>_)" [64,63] 63)
oheimb@15188
    51
oheimb@15188
    52
oheimb@15188
    53
lemma ft_fsingleton[simp]: "ft$(<a>) = Def a"
oheimb@15188
    54
by (simp add: fsingleton_def2)
oheimb@15188
    55
oheimb@15188
    56
lemma slen_fsingleton[simp]: "#(<a>) = Fin 1"
oheimb@15188
    57
by (simp add: fsingleton_def2 inat_defs)
oheimb@15188
    58
oheimb@15188
    59
lemma slen_fstreams[simp]: "#(<a> ooo s) = iSuc (#s)"
oheimb@15188
    60
by (simp add: fsingleton_def2)
oheimb@15188
    61
oheimb@15188
    62
lemma slen_fstreams2[simp]: "#(s ooo <a>) = iSuc (#s)"
oheimb@15188
    63
apply (case_tac "#s", auto)
oheimb@15188
    64
apply (insert slen_sconc [of _ s "Suc 0" "<a>"], auto)
oheimb@15188
    65
by (simp add: sconc_def)
oheimb@15188
    66
oheimb@15188
    67
lemma j_th_0_fsingleton[simp]:"jth 0 (<a>) = a"
oheimb@15188
    68
apply (simp add: fsingleton_def2 jth_def)
oheimb@15188
    69
by (simp add: i_th_def Fin_0)
oheimb@15188
    70
oheimb@15188
    71
lemma jth_0[simp]: "jth 0 (<a> ooo s) = a"  
oheimb@15188
    72
apply (simp add: fsingleton_def2 jth_def)
oheimb@15188
    73
by (simp add: i_th_def Fin_0)
oheimb@15188
    74
oheimb@15188
    75
lemma first_sconc[simp]: "first (<a> ooo s) = a"
oheimb@15188
    76
by (simp add: first_def)
oheimb@15188
    77
oheimb@15188
    78
lemma first_fsingleton[simp]: "first (<a>) = a"
oheimb@15188
    79
by (simp add: first_def)
oheimb@15188
    80
oheimb@15188
    81
lemma jth_n[simp]: "Fin n = #s ==> jth n (s ooo <a>) = a"
oheimb@15188
    82
apply (simp add: jth_def, auto)
oheimb@15188
    83
apply (simp add: i_th_def rt_sconc1)
oheimb@15188
    84
by (simp add: inat_defs split: inat_splits)
oheimb@15188
    85
oheimb@15188
    86
lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a"
oheimb@15188
    87
apply (simp add: last_def)
oheimb@15188
    88
apply (simp add: inat_defs split:inat_splits)
oheimb@15188
    89
by (drule sym, auto)
oheimb@15188
    90
oheimb@15188
    91
lemma last_fsingleton[simp]: "last (<a>) = a"
oheimb@15188
    92
by (simp add: last_def)
oheimb@15188
    93
oheimb@15188
    94
lemma first_UU[simp]: "first UU = arbitrary"
oheimb@15188
    95
by (simp add: first_def jth_def)
oheimb@15188
    96
oheimb@15188
    97
lemma last_UU[simp]:"last UU = arbitrary"
oheimb@15188
    98
by (simp add: last_def jth_def inat_defs)
oheimb@15188
    99
oheimb@15188
   100
lemma last_infinite[simp]:"#s = Infty ==> last s = arbitrary"
oheimb@15188
   101
by (simp add: last_def)
oheimb@15188
   102
oheimb@15188
   103
lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = arbitrary"
oheimb@15188
   104
by (simp add: jth_def inat_defs split:inat_splits, auto)
oheimb@15188
   105
oheimb@15188
   106
lemma jth_UU[simp]:"jth n UU = arbitrary" 
oheimb@15188
   107
by (simp add: jth_def)
oheimb@15188
   108
oheimb@15188
   109
lemma ext_last:"[|s ~= UU; Fin (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s" 
oheimb@15188
   110
apply (simp add: last_def)
oheimb@15188
   111
apply (case_tac "#s", auto)
oheimb@15188
   112
apply (simp add: fsingleton_def2)
oheimb@15188
   113
apply (subgoal_tac "Def (jth n s) = i_th n s")
oheimb@15188
   114
apply (auto simp add: i_th_last)
oheimb@15188
   115
apply (drule slen_take_lemma1, auto)
oheimb@15188
   116
apply (simp add: jth_def)
oheimb@15188
   117
apply (case_tac "i_th n s = UU")
oheimb@15188
   118
apply auto
oheimb@15188
   119
apply (simp add: i_th_def)
oheimb@15188
   120
apply (case_tac "i_rt n s = UU", auto)
oheimb@15188
   121
apply (drule i_rt_slen [THEN iffD1])
oheimb@15188
   122
apply (drule slen_take_eq_rev [rule_format, THEN iffD2],auto)
oheimb@15188
   123
by (drule not_Undef_is_Def [THEN iffD1], auto)
oheimb@15188
   124
oheimb@15188
   125
oheimb@15188
   126
lemma fsingleton_lemma1[simp]: "(<a> = <b>) = (a=b)"
oheimb@15188
   127
by (simp add: fsingleton_def2)
oheimb@15188
   128
oheimb@15188
   129
lemma fsingleton_lemma2[simp]: "<a> ~= <>"
oheimb@15188
   130
by (simp add: fsingleton_def2)
oheimb@15188
   131
oheimb@15188
   132
lemma fsingleton_sconc:"<a> ooo s = Def a && s"
oheimb@15188
   133
by (simp add: fsingleton_def2)
oheimb@15188
   134
oheimb@15188
   135
lemma fstreams_ind: 
oheimb@15188
   136
  "[| adm P; P <>; !!a s. P s ==> P (<a> ooo s) |] ==> P x"
oheimb@15188
   137
apply (simp add: fsingleton_def2)
oheimb@15188
   138
apply (rule stream.ind, auto)
oheimb@15188
   139
by (drule not_Undef_is_Def [THEN iffD1], auto)
oheimb@15188
   140
oheimb@15188
   141
lemma fstreams_ind2:
oheimb@15188
   142
  "[| adm P; P <>; !!a. P (<a>); !!a b s. P s ==> P (<a> ooo <b> ooo s) |] ==> P x"
oheimb@15188
   143
apply (simp add: fsingleton_def2)
oheimb@15188
   144
apply (rule stream_ind2, auto)
oheimb@15188
   145
by (drule not_Undef_is_Def [THEN iffD1], auto)+
oheimb@15188
   146
oheimb@15188
   147
lemma fstreams_take_Suc[simp]: "stream_take (Suc n)$(<a> ooo s) = <a> ooo stream_take n$s"
oheimb@15188
   148
by (simp add: fsingleton_def2)
oheimb@15188
   149
oheimb@15188
   150
lemma fstreams_not_empty[simp]: "<a> ooo s ~= <>"
oheimb@15188
   151
by (simp add: fsingleton_def2)
oheimb@15188
   152
oheimb@15188
   153
lemma fstreams_not_empty2[simp]: "s ooo <a> ~= <>"
oheimb@15188
   154
by (case_tac "s=UU", auto)
oheimb@15188
   155
oheimb@15188
   156
lemma fstreams_exhaust: "x = UU | (EX a s. x = <a> ooo s)"
oheimb@15188
   157
apply (simp add: fsingleton_def2, auto)
oheimb@15188
   158
apply (erule contrapos_pp, auto)
oheimb@15188
   159
apply (drule stream_exhaust_eq [THEN iffD1], auto)
oheimb@15188
   160
by (drule not_Undef_is_Def [THEN iffD1], auto)
oheimb@15188
   161
oheimb@15188
   162
lemma fstreams_cases: "[| x = UU ==> P; !!a y. x = <a> ooo y ==> P |] ==> P"
oheimb@15188
   163
by (insert fstreams_exhaust [of x], auto)
oheimb@15188
   164
oheimb@15188
   165
lemma fstreams_exhaust_eq: "(x ~= UU) = (? a y. x = <a> ooo y)"
oheimb@15188
   166
apply (simp add: fsingleton_def2, auto)
oheimb@15188
   167
apply (drule stream_exhaust_eq [THEN iffD1], auto)
oheimb@15188
   168
by (drule not_Undef_is_Def [THEN iffD1], auto)
oheimb@15188
   169
oheimb@15188
   170
lemma fstreams_inject: "(<a> ooo s = <b> ooo t) = (a=b & s=t)"
oheimb@15188
   171
by (simp add: fsingleton_def2)
oheimb@15188
   172
oheimb@15188
   173
lemma fstreams_prefix: "<a> ooo s << t ==> EX tt. t = <a> ooo tt &  s << tt"
oheimb@15188
   174
apply (simp add: fsingleton_def2)
oheimb@15188
   175
apply (insert stream_prefix [of "Def a" s t], auto)
huffman@19550
   176
by (auto simp add: stream.inverts)
oheimb@15188
   177
oheimb@15188
   178
lemma fstreams_prefix': "x << <a> ooo z = (x = <> |  (EX y. x = <a> ooo y &  y << z))"
oheimb@15188
   179
apply (auto, case_tac "x=UU", auto)
oheimb@15188
   180
apply (drule stream_exhaust_eq [THEN iffD1], auto)
oheimb@15188
   181
apply (simp add: fsingleton_def2, auto)
huffman@19550
   182
apply (auto simp add: stream.inverts)
oheimb@15188
   183
apply (drule ax_flat [rule_format], simp)
oheimb@15188
   184
by (erule sconc_mono)
oheimb@15188
   185
oheimb@15188
   186
lemma ft_fstreams[simp]: "ft$(<a> ooo s) = Def a"
oheimb@15188
   187
by (simp add: fsingleton_def2)
oheimb@15188
   188
oheimb@15188
   189
lemma rt_fstreams[simp]: "rt$(<a> ooo s) = s"
oheimb@15188
   190
by (simp add: fsingleton_def2)
oheimb@15188
   191
oheimb@15188
   192
lemma ft_eq[simp]: "(ft$s = Def a) = (EX t. s = <a> ooo t)"
oheimb@15188
   193
apply (rule stream.casedist [of s],auto)
huffman@16746
   194
by ((*drule sym,*) auto simp add: fsingleton_def2)
oheimb@15188
   195
oheimb@15188
   196
lemma surjective_fstreams: "(<d> ooo y = x) = (ft$x = Def d & rt$x = y)"
oheimb@15188
   197
by auto
oheimb@15188
   198
oheimb@15188
   199
lemma fstreams_mono: "<a> ooo b << <a> ooo c ==> b << c"
oheimb@15188
   200
apply (simp add: fsingleton_def2)
huffman@19550
   201
by (auto simp add: stream.inverts)
oheimb@15188
   202
oheimb@15188
   203
lemma fsmap_UU[simp]: "fsmap f$UU = UU"
oheimb@15188
   204
by (simp add: fsmap_def)
oheimb@15188
   205
oheimb@15188
   206
lemma fsmap_fsingleton_sconc: "fsmap f$(<x> ooo xs) = <(f x)> ooo (fsmap f$xs)"
oheimb@15188
   207
by (simp add: fsmap_def fsingleton_def2 flift2_def)
oheimb@15188
   208
oheimb@15188
   209
lemma fsmap_fsingleton[simp]: "fsmap f$(<x>) = <(f x)>"
oheimb@15188
   210
by (simp add: fsmap_def fsingleton_def2 flift2_def)
oheimb@15188
   211
oheimb@15188
   212
oheimb@15188
   213
declare range_composition[simp del]
oheimb@15188
   214
oheimb@15188
   215
oheimb@15188
   216
lemma fstreams_chain_lemma[rule_format]:
oheimb@15188
   217
  "ALL s x y. stream_take n$(s::'a fstream) << x & x << y & y << s & x ~= y --> stream_take (Suc n)$s << y"
oheimb@15188
   218
apply (induct_tac n, auto)
oheimb@15188
   219
apply (case_tac "s=UU", auto)
oheimb@15188
   220
apply (drule stream_exhaust_eq [THEN iffD1], auto)
oheimb@15188
   221
apply (case_tac "y=UU", auto)
oheimb@15188
   222
apply (drule stream_exhaust_eq [THEN iffD1], auto)
huffman@19550
   223
apply (auto simp add: stream.inverts)
huffman@19550
   224
apply (simp add: less_lift)
oheimb@15188
   225
apply (case_tac "s=UU", auto)
oheimb@15188
   226
apply (drule stream_exhaust_eq [THEN iffD1], auto)
oheimb@15188
   227
apply (erule_tac x="ya" in allE)
oheimb@15188
   228
apply (drule stream_prefix, auto)
oheimb@15188
   229
apply (case_tac "y=UU",auto)
oheimb@15188
   230
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
huffman@19550
   231
apply (auto simp add: stream.inverts)
huffman@16746
   232
apply (simp add: less_lift)
oheimb@15188
   233
apply (erule_tac x="tt" in allE)
oheimb@15188
   234
apply (erule_tac x="yb" in allE, auto)
huffman@16746
   235
apply (simp add: less_lift)
huffman@19550
   236
by (simp add: less_lift)
oheimb@15188
   237
oheimb@15188
   238
lemma fstreams_lub_lemma1: "[| chain Y; lub (range Y) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
oheimb@15188
   239
apply (subgoal_tac "lub(range Y) ~= UU")
oheimb@15188
   240
apply (drule chain_UU_I_inverse2, auto)
oheimb@15188
   241
apply (drule_tac x="i" in is_ub_thelub, auto)
oheimb@15188
   242
by (drule fstreams_prefix' [THEN iffD1], auto)
oheimb@15188
   243
oheimb@15188
   244
lemma fstreams_lub1: 
oheimb@15188
   245
 "[| chain Y; lub (range Y) = <a> ooo s |]
oheimb@15188
   246
     ==> (EX j t. Y j = <a> ooo t) & (EX X. chain X & (ALL i. EX j. <a> ooo X i << Y j) & lub (range X) = s)"
oheimb@15188
   247
apply (auto simp add: fstreams_lub_lemma1)
oheimb@15188
   248
apply (rule_tac x="%n. stream_take n$s" in exI, auto)
oheimb@15188
   249
apply (simp add: chain_stream_take)
oheimb@15188
   250
apply (induct_tac i, auto)
oheimb@15188
   251
apply (drule fstreams_lub_lemma1, auto)
oheimb@15188
   252
apply (rule_tac x="j" in exI, auto)
oheimb@15188
   253
apply (case_tac "max_in_chain j Y")
oheimb@15188
   254
apply (frule lub_finch1 [THEN thelubI], auto)
oheimb@15188
   255
apply (rule_tac x="j" in exI)
oheimb@15188
   256
apply (erule subst) back back
oheimb@15188
   257
apply (simp add: less_cprod_def sconc_mono)
oheimb@15188
   258
apply (simp add: max_in_chain_def, auto)
oheimb@15188
   259
apply (rule_tac x="ja" in exI)
oheimb@15188
   260
apply (subgoal_tac "Y j << Y ja")
oheimb@15188
   261
apply (drule fstreams_prefix, auto)+
oheimb@15188
   262
apply (rule sconc_mono)
oheimb@15188
   263
apply (rule fstreams_chain_lemma, auto)
oheimb@15188
   264
apply (subgoal_tac "Y ja << (LUB i. (Y i))", clarsimp)
oheimb@15188
   265
apply (drule fstreams_mono, simp)
oheimb@15188
   266
apply (rule is_ub_thelub, simp)
oheimb@15188
   267
apply (blast intro: chain_mono3)
oheimb@15188
   268
by (rule stream_reach2)
oheimb@15188
   269
oheimb@15188
   270
oheimb@15188
   271
lemma lub_Pair_not_UU_lemma: 
oheimb@15188
   272
  "[| chain Y; lub (range Y) = ((a::'a::flat), b); a ~= UU; b ~= UU |] 
oheimb@15188
   273
      ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
oheimb@15188
   274
apply (frule thelub_cprod, clarsimp)
oheimb@15188
   275
apply (drule chain_UU_I_inverse2, clarsimp)
oheimb@15188
   276
apply (case_tac "Y i", clarsimp)
oheimb@15188
   277
apply (case_tac "max_in_chain i Y")
oheimb@15188
   278
apply (drule maxinch_is_thelub, auto)
oheimb@15188
   279
apply (rule_tac x="i" in exI, auto)
oheimb@15188
   280
apply (simp add: max_in_chain_def, auto)
oheimb@15188
   281
apply (subgoal_tac "Y i << Y j",auto)
oheimb@15188
   282
apply (simp add: less_cprod_def, clarsimp)
oheimb@15188
   283
apply (drule ax_flat [rule_format], auto)
oheimb@15188
   284
apply (case_tac "snd (Y j) = UU",auto)
oheimb@15188
   285
apply (case_tac "Y j", auto)
oheimb@15188
   286
apply (rule_tac x="j" in exI)
oheimb@15188
   287
apply (case_tac "Y j",auto)
oheimb@15188
   288
by (drule chain_mono3, auto)
oheimb@15188
   289
oheimb@15188
   290
lemma fstreams_lub_lemma2: 
oheimb@15188
   291
  "[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, <m> ooo t)"
oheimb@15188
   292
apply (frule lub_Pair_not_UU_lemma, auto)
oheimb@15188
   293
apply (drule_tac x="j" in is_ub_thelub, auto)
oheimb@15188
   294
apply (simp add: less_cprod_def, clarsimp)
oheimb@15188
   295
apply (drule ax_flat [rule_format], clarsimp)
oheimb@15188
   296
by (drule fstreams_prefix' [THEN iffD1], auto)
oheimb@15188
   297
oheimb@15188
   298
lemma fstreams_lub2:
oheimb@15188
   299
  "[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] 
oheimb@15188
   300
      ==> (EX j t. Y j = (a, <m> ooo t)) & (EX X. chain X & (ALL i. EX j. (a, <m> ooo X i) << Y j) & lub (range X) = ms)"
oheimb@15188
   301
apply (auto simp add: fstreams_lub_lemma2)
oheimb@15188
   302
apply (rule_tac x="%n. stream_take n$ms" in exI, auto)
oheimb@15188
   303
apply (simp add: chain_stream_take)
oheimb@15188
   304
apply (induct_tac i, auto)
oheimb@15188
   305
apply (drule fstreams_lub_lemma2, auto)
oheimb@15188
   306
apply (rule_tac x="j" in exI, auto)
oheimb@15188
   307
apply (simp add: less_cprod_def)
oheimb@15188
   308
apply (case_tac "max_in_chain j Y")
oheimb@15188
   309
apply (frule lub_finch1 [THEN thelubI], auto)
oheimb@15188
   310
apply (rule_tac x="j" in exI)
oheimb@15188
   311
apply (erule subst) back back
oheimb@15188
   312
apply (simp add: less_cprod_def sconc_mono)
oheimb@15188
   313
apply (simp add: max_in_chain_def, auto)
oheimb@15188
   314
apply (rule_tac x="ja" in exI)
oheimb@15188
   315
apply (subgoal_tac "Y j << Y ja")
oheimb@15188
   316
apply (simp add: less_cprod_def, auto)
oheimb@15188
   317
apply (drule trans_less)
oheimb@15188
   318
apply (simp add: ax_flat, auto)
oheimb@15188
   319
apply (drule fstreams_prefix, auto)+
oheimb@15188
   320
apply (rule sconc_mono)
oheimb@15188
   321
apply (subgoal_tac "tt ~= tta" "tta << ms")
oheimb@15188
   322
apply (blast intro: fstreams_chain_lemma)
oheimb@15188
   323
apply (frule lub_cprod [THEN thelubI], auto)
oheimb@15188
   324
apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp)
oheimb@15188
   325
apply (drule fstreams_mono, simp)
oheimb@15188
   326
apply (rule is_ub_thelub chainI)
oheimb@15188
   327
apply (simp add: chain_def less_cprod_def)
oheimb@15188
   328
apply (subgoal_tac "fst (Y j) ~= fst (Y ja) | snd (Y j) ~= snd (Y ja)", simp)
oheimb@15188
   329
apply (drule ax_flat[rule_format], simp)+
oheimb@15188
   330
apply (drule prod_eqI, auto)
oheimb@15188
   331
apply (simp add: chain_mono3)
oheimb@15188
   332
by (rule stream_reach2)
oheimb@15188
   333
oheimb@15188
   334
oheimb@15188
   335
lemma cpo_cont_lemma:
oheimb@15188
   336
  "[| monofun (f::'a::cpo => 'b::cpo); (!Y. chain Y --> f (lub(range Y)) << (LUB i. f (Y i))) |] ==> cont f"
oheimb@15188
   337
apply (rule monocontlub2cont, auto)
huffman@16219
   338
apply (simp add: contlub_def, auto)
oheimb@15188
   339
apply (erule_tac x="Y" in allE, auto)
oheimb@15188
   340
apply (simp add: po_eq_conv)
oheimb@15188
   341
apply (frule cpo,auto)
oheimb@15188
   342
apply (frule is_lubD1)
oheimb@15188
   343
apply (frule ub2ub_monofun, auto)
oheimb@15188
   344
apply (drule thelubI, auto)
oheimb@15188
   345
apply (rule is_lub_thelub, auto)
oheimb@15188
   346
by (erule ch2ch_monofun, simp)
oheimb@15188
   347
oheimb@15188
   348
end
oheimb@15188
   349
oheimb@15188
   350
oheimb@15188
   351
oheimb@15188
   352