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