author | hoelzl |
Tue, 19 Jul 2011 14:35:44 +0200 | |
changeset 43919 | a7e4fb1a0502 |
parent 42151 | 4da4fc77664b |
child 43921 | e8511be08ddd |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/FOCUS/Fstreams.thy |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30807
diff
changeset
|
2 |
Author: Borislav Gajanovic |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
3 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30807
diff
changeset
|
4 |
FOCUS flat streams (with lifted elements). |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30807
diff
changeset
|
5 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30807
diff
changeset
|
6 |
TODO: integrate this with Fstream. |
15188
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 |
|
37110
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
36452
diff
changeset
|
9 |
theory Fstreams |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40774
diff
changeset
|
10 |
imports "~~/src/HOL/HOLCF/Library/Stream" |
37110
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
36452
diff
changeset
|
11 |
begin |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
12 |
|
36452 | 13 |
default_sort type |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
14 |
|
41476 | 15 |
type_synonym 'a fstream = "('a lift) stream" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
16 |
|
19763 | 17 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
18 |
fsingleton :: "'a => 'a fstream" ("<_>" [1000] 999) where |
19763 | 19 |
fsingleton_def2: "fsingleton = (%a. Def a && UU)" |
20 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
21 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
22 |
fsfilter :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where |
19763 | 23 |
"fsfilter A = sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))" |
24 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
25 |
definition |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30807
diff
changeset
|
26 |
fsmap :: "('a => 'b) => 'a fstream -> 'b fstream" where |
19763 | 27 |
"fsmap f = smap$(flift2 f)" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
28 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
29 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
30 |
jth :: "nat => 'a fstream => 'a" where |
28524 | 31 |
"jth = (%n s. if Fin n < #s then THE a. i_th n s = Def a else undefined)" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
32 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
33 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
34 |
first :: "'a fstream => 'a" where |
19763 | 35 |
"first = (%s. jth 0 s)" |
36 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
37 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
38 |
last :: "'a fstream => 'a" where |
28524 | 39 |
"last = (%s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else undefined))" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
40 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
41 |
|
19763 | 42 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
43 |
emptystream :: "'a fstream" ("<>") where |
19763 | 44 |
"<> == \<bottom>" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
45 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
46 |
abbreviation |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30807
diff
changeset
|
47 |
fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63) where |
19763 | 48 |
"A(C)s == fsfilter A\<cdot>s" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
49 |
|
21210 | 50 |
notation (xsymbols) |
19763 | 51 |
fsfilter' ("(_\<copyright>_)" [64,63] 63) |
15188
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 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
54 |
lemma ft_fsingleton[simp]: "ft$(<a>) = Def a" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
55 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
56 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
57 |
lemma slen_fsingleton[simp]: "#(<a>) = Fin 1" |
43919 | 58 |
by (simp add: fsingleton_def2 enat_defs) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
59 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
60 |
lemma slen_fstreams[simp]: "#(<a> ooo s) = iSuc (#s)" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
61 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
62 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
63 |
lemma slen_fstreams2[simp]: "#(s ooo <a>) = iSuc (#s)" |
27111 | 64 |
apply (cases "#s") |
65 |
apply (auto simp add: iSuc_Fin) |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
66 |
apply (insert slen_sconc [of _ s "Suc 0" "<a>"], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
67 |
by (simp add: sconc_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
68 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
69 |
lemma j_th_0_fsingleton[simp]:"jth 0 (<a>) = a" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
70 |
apply (simp add: fsingleton_def2 jth_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
71 |
by (simp add: i_th_def Fin_0) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
72 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
73 |
lemma jth_0[simp]: "jth 0 (<a> ooo s) = a" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
74 |
apply (simp add: fsingleton_def2 jth_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
75 |
by (simp add: i_th_def Fin_0) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
76 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
77 |
lemma first_sconc[simp]: "first (<a> ooo s) = a" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
78 |
by (simp add: first_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
79 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
80 |
lemma first_fsingleton[simp]: "first (<a>) = a" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
81 |
by (simp add: first_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
82 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
83 |
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
|
84 |
apply (simp add: jth_def, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
85 |
apply (simp add: i_th_def rt_sconc1) |
43919 | 86 |
by (simp add: enat_defs split: enat.splits) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
87 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
88 |
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
|
89 |
apply (simp add: last_def) |
43919 | 90 |
apply (simp add: enat_defs split:enat.splits) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
91 |
by (drule sym, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
92 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
93 |
lemma last_fsingleton[simp]: "last (<a>) = a" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
94 |
by (simp add: last_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
95 |
|
28524 | 96 |
lemma first_UU[simp]: "first UU = undefined" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
97 |
by (simp add: first_def jth_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
98 |
|
28524 | 99 |
lemma last_UU[simp]:"last UU = undefined" |
43919 | 100 |
by (simp add: last_def jth_def enat_defs) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
101 |
|
28524 | 102 |
lemma last_infinite[simp]:"#s = Infty ==> last s = undefined" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
103 |
by (simp add: last_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
104 |
|
28524 | 105 |
lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined" |
43919 | 106 |
by (simp add: jth_def enat_defs split:enat.splits, auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
107 |
|
28524 | 108 |
lemma jth_UU[simp]:"jth n UU = undefined" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
109 |
by (simp add: jth_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
110 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
111 |
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
|
112 |
apply (simp add: last_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
113 |
apply (case_tac "#s", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
114 |
apply (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
115 |
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
|
116 |
apply (auto simp add: i_th_last) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
117 |
apply (drule slen_take_lemma1, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
118 |
apply (simp add: jth_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
119 |
apply (case_tac "i_th n s = UU") |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
120 |
apply auto |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
121 |
apply (simp add: i_th_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
122 |
apply (case_tac "i_rt n s = UU", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
123 |
apply (drule i_rt_slen [THEN iffD1]) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
124 |
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
|
125 |
by (drule not_Undef_is_Def [THEN iffD1], auto) |
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 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
128 |
lemma fsingleton_lemma1[simp]: "(<a> = <b>) = (a=b)" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
129 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
130 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
131 |
lemma fsingleton_lemma2[simp]: "<a> ~= <>" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
132 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
133 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
134 |
lemma fsingleton_sconc:"<a> ooo s = Def a && s" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
135 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
136 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
137 |
lemma fstreams_ind: |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
138 |
"[| 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
|
139 |
apply (simp add: fsingleton_def2) |
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35572
diff
changeset
|
140 |
apply (rule stream.induct, auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
141 |
by (drule not_Undef_is_Def [THEN iffD1], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
142 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
143 |
lemma fstreams_ind2: |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
144 |
"[| 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
|
145 |
apply (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
146 |
apply (rule stream_ind2, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
147 |
by (drule not_Undef_is_Def [THEN iffD1], auto)+ |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
148 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
149 |
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
|
150 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
151 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
152 |
lemma fstreams_not_empty[simp]: "<a> ooo s ~= <>" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
153 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
154 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
155 |
lemma fstreams_not_empty2[simp]: "s ooo <a> ~= <>" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
156 |
by (case_tac "s=UU", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
157 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
158 |
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
|
159 |
apply (simp add: fsingleton_def2, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
160 |
apply (erule contrapos_pp, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
161 |
apply (drule stream_exhaust_eq [THEN iffD1], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
162 |
by (drule not_Undef_is_Def [THEN iffD1], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
163 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
164 |
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
|
165 |
by (insert fstreams_exhaust [of x], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
166 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
167 |
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
|
168 |
apply (simp add: fsingleton_def2, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
169 |
apply (drule stream_exhaust_eq [THEN iffD1], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
170 |
by (drule not_Undef_is_Def [THEN iffD1], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
171 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
172 |
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
|
173 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
174 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
175 |
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
|
176 |
apply (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
177 |
apply (insert stream_prefix [of "Def a" s t], auto) |
30807 | 178 |
done |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
179 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
180 |
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
|
181 |
apply (auto, case_tac "x=UU", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
182 |
apply (drule stream_exhaust_eq [THEN iffD1], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
183 |
apply (simp add: fsingleton_def2, auto) |
25920 | 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)" |
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35572
diff
changeset
|
194 |
apply (cases s, auto) |
16746 | 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" |
30807 | 201 |
by (simp add: fsingleton_def2) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
202 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
203 |
lemma fsmap_UU[simp]: "fsmap f$UU = UU" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
204 |
by (simp add: fsmap_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
205 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
206 |
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
|
207 |
by (simp add: fsmap_def fsingleton_def2 flift2_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
208 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
209 |
lemma fsmap_fsingleton[simp]: "fsmap f$(<x>) = <(f x)>" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
210 |
by (simp add: fsmap_def fsingleton_def2 flift2_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
211 |
|
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 |
lemma fstreams_chain_lemma[rule_format]: |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
214 |
"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
|
215 |
apply (induct_tac n, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
216 |
apply (case_tac "s=UU", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
217 |
apply (drule stream_exhaust_eq [THEN iffD1], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
218 |
apply (case_tac "y=UU", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
219 |
apply (drule stream_exhaust_eq [THEN iffD1], auto) |
40431 | 220 |
apply (simp add: flat_below_iff) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
221 |
apply (case_tac "s=UU", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
222 |
apply (drule stream_exhaust_eq [THEN iffD1], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
223 |
apply (erule_tac x="ya" in allE) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
224 |
apply (drule stream_prefix, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
225 |
apply (case_tac "y=UU",auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
226 |
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) |
35215
a03462cbf86f
get rid of warnings about duplicate simp rules in all HOLCF theories
huffman
parents:
32960
diff
changeset
|
227 |
apply auto |
40431 | 228 |
apply (simp add: flat_below_iff) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
229 |
apply (erule_tac x="tt" in allE) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
230 |
apply (erule_tac x="yb" in allE, auto) |
40431 | 231 |
apply (simp add: flat_below_iff) |
232 |
by (simp add: flat_below_iff) |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
233 |
|
27413 | 234 |
lemma fstreams_lub_lemma1: "[| chain Y; (LUB i. Y i) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t" |
235 |
apply (subgoal_tac "(LUB i. Y i) ~= UU") |
|
41431
138f414f14cb
remove various lemmas redundant with lub_eq_bottom_iff
huffman
parents:
41413
diff
changeset
|
236 |
apply (frule lub_eq_bottom_iff, auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
237 |
apply (drule_tac x="i" in is_ub_thelub, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
238 |
by (drule fstreams_prefix' [THEN iffD1], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
239 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
240 |
lemma fstreams_lub1: |
27413 | 241 |
"[| chain Y; (LUB i. Y i) = <a> ooo s |] |
242 |
==> (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
|
243 |
apply (auto simp add: fstreams_lub_lemma1) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
244 |
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
|
245 |
apply (induct_tac i, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
246 |
apply (drule fstreams_lub_lemma1, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
247 |
apply (rule_tac x="j" in exI, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
248 |
apply (case_tac "max_in_chain j Y") |
40771 | 249 |
apply (frule lub_finch1 [THEN lub_eqI], auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
250 |
apply (rule_tac x="j" in exI) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
251 |
apply (erule subst) back back |
40431 | 252 |
apply (simp add: below_prod_def sconc_mono) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
253 |
apply (simp add: max_in_chain_def, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
254 |
apply (rule_tac x="ja" in exI) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
255 |
apply (subgoal_tac "Y j << Y ja") |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
256 |
apply (drule fstreams_prefix, auto)+ |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
257 |
apply (rule sconc_mono) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
258 |
apply (rule fstreams_chain_lemma, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
259 |
apply (subgoal_tac "Y ja << (LUB i. (Y i))", clarsimp) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
260 |
apply (drule fstreams_mono, simp) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
261 |
apply (rule is_ub_thelub, simp) |
25922
cb04d05e95fb
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents:
25920
diff
changeset
|
262 |
apply (blast intro: chain_mono) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
263 |
by (rule stream_reach2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
264 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
265 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
266 |
lemma lub_Pair_not_UU_lemma: |
27413 | 267 |
"[| 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
|
268 |
==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU" |
40771 | 269 |
apply (frule lub_prod, clarsimp) |
41431
138f414f14cb
remove various lemmas redundant with lub_eq_bottom_iff
huffman
parents:
41413
diff
changeset
|
270 |
apply (clarsimp simp add: lub_eq_bottom_iff [where Y="\<lambda>i. fst (Y i)"]) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
271 |
apply (case_tac "Y i", clarsimp) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
272 |
apply (case_tac "max_in_chain i Y") |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
273 |
apply (drule maxinch_is_thelub, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
274 |
apply (rule_tac x="i" in exI, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
275 |
apply (simp add: max_in_chain_def, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
276 |
apply (subgoal_tac "Y i << Y j",auto) |
40431 | 277 |
apply (simp add: below_prod_def, clarsimp) |
25920 | 278 |
apply (drule ax_flat, auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
279 |
apply (case_tac "snd (Y j) = UU",auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
280 |
apply (case_tac "Y j", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
281 |
apply (rule_tac x="j" in exI) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
282 |
apply (case_tac "Y j",auto) |
25922
cb04d05e95fb
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents:
25920
diff
changeset
|
283 |
by (drule chain_mono, auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
284 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
285 |
lemma fstreams_lub_lemma2: |
27413 | 286 |
"[| 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
|
287 |
apply (frule lub_Pair_not_UU_lemma, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
288 |
apply (drule_tac x="j" in is_ub_thelub, auto) |
25920 | 289 |
apply (drule ax_flat, clarsimp) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
290 |
by (drule fstreams_prefix' [THEN iffD1], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
291 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
292 |
lemma fstreams_lub2: |
27413 | 293 |
"[| chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] |
294 |
==> (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
|
295 |
apply (auto simp add: fstreams_lub_lemma2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
296 |
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
|
297 |
apply (induct_tac i, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
298 |
apply (drule fstreams_lub_lemma2, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
299 |
apply (rule_tac x="j" in exI, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
300 |
apply (case_tac "max_in_chain j Y") |
40771 | 301 |
apply (frule lub_finch1 [THEN lub_eqI], auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
302 |
apply (rule_tac x="j" in exI) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
303 |
apply (erule subst) back back |
26029 | 304 |
apply (simp add: sconc_mono) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
305 |
apply (simp add: max_in_chain_def, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
306 |
apply (rule_tac x="ja" in exI) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
307 |
apply (subgoal_tac "Y j << Y ja") |
40431 | 308 |
apply (simp add: below_prod_def, auto) |
309 |
apply (drule below_trans) |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
310 |
apply (simp add: ax_flat, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
311 |
apply (drule fstreams_prefix, auto)+ |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
312 |
apply (rule sconc_mono) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
313 |
apply (subgoal_tac "tt ~= tta" "tta << ms") |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
314 |
apply (blast intro: fstreams_chain_lemma) |
40771 | 315 |
apply (frule lub_prod, auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
316 |
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
|
317 |
apply (drule fstreams_mono, simp) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
318 |
apply (rule is_ub_thelub chainI) |
40431 | 319 |
apply (simp add: chain_def below_prod_def) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
320 |
apply (subgoal_tac "fst (Y j) ~= fst (Y ja) | snd (Y j) ~= snd (Y ja)", simp) |
25920 | 321 |
apply (drule ax_flat, simp)+ |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
322 |
apply (drule prod_eqI, auto) |
25922
cb04d05e95fb
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents:
25920
diff
changeset
|
323 |
apply (simp add: chain_mono) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
324 |
by (rule stream_reach2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
325 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
326 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
327 |
lemma cpo_cont_lemma: |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
328 |
"[| monofun (f::'a::cpo => 'b::cpo); (!Y. chain Y --> f (lub(range Y)) << (LUB i. f (Y i))) |] ==> cont f" |
35914 | 329 |
by (erule contI2, simp) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
330 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
331 |
end |