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