author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 63549 | b0d31c7def86 |
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 |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63549
diff
changeset
|
10 |
imports "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 |
63549 | 27 |
"fsmap f = smap\<cdot>(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 |
43924 | 31 |
"jth = (%n s. if enat 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 |
43924 | 39 |
"last = (%s. case #s of enat 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 |
61998 | 47 |
fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<copyright>_)" [64,63] 63) where |
48 |
"A\<copyright>s == fsfilter A\<cdot>s" |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
49 |
|
61998 | 50 |
notation (ASCII) |
51 |
fsfilter' ("(_'(C')_)" [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 |
|
63549 | 54 |
lemma ft_fsingleton[simp]: "ft\<cdot>(<a>) = Def a" |
15188
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 |
|
43924 | 57 |
lemma slen_fsingleton[simp]: "#(<a>) = enat 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 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43924
diff
changeset
|
60 |
lemma slen_fstreams[simp]: "#(<a> ooo s) = eSuc (#s)" |
15188
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 |
|
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43924
diff
changeset
|
63 |
lemma slen_fstreams2[simp]: "#(s ooo <a>) = eSuc (#s)" |
27111 | 64 |
apply (cases "#s") |
44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43924
diff
changeset
|
65 |
apply (auto simp add: eSuc_enat) |
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) |
49521 | 67 |
apply (simp add: sconc_def) |
68 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
69 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
70 |
lemma j_th_0_fsingleton[simp]:"jth 0 (<a>) = a" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
71 |
apply (simp add: fsingleton_def2 jth_def) |
49521 | 72 |
apply (simp add: i_th_def enat_0) |
73 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
74 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
75 |
lemma jth_0[simp]: "jth 0 (<a> ooo s) = a" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
76 |
apply (simp add: fsingleton_def2 jth_def) |
49521 | 77 |
apply (simp add: i_th_def enat_0) |
78 |
done |
|
15188
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_sconc[simp]: "first (<a> ooo s) = 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 first_fsingleton[simp]: "first (<a>) = a" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
84 |
by (simp add: first_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
85 |
|
43924 | 86 |
lemma jth_n[simp]: "enat n = #s ==> jth n (s ooo <a>) = a" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
87 |
apply (simp add: jth_def, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
88 |
apply (simp add: i_th_def rt_sconc1) |
49521 | 89 |
apply (simp add: enat_defs split: enat.splits) |
90 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
91 |
|
43924 | 92 |
lemma last_sconc[simp]: "enat n = #s ==> last (s ooo <a>) = a" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
93 |
apply (simp add: last_def) |
43919 | 94 |
apply (simp add: enat_defs split:enat.splits) |
49521 | 95 |
apply (drule sym, auto) |
96 |
done |
|
15188
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_fsingleton[simp]: "last (<a>) = a" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
99 |
by (simp add: last_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
100 |
|
28524 | 101 |
lemma first_UU[simp]: "first UU = undefined" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
102 |
by (simp add: first_def jth_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
103 |
|
28524 | 104 |
lemma last_UU[simp]:"last UU = undefined" |
43919 | 105 |
by (simp add: last_def jth_def enat_defs) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
106 |
|
63549 | 107 |
lemma last_infinite[simp]:"#s = \<infinity> \<Longrightarrow> last s = undefined" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
108 |
by (simp add: last_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
109 |
|
63549 | 110 |
lemma jth_slen_lemma1:"n \<le> k \<and> enat n = #s \<Longrightarrow> jth k s = undefined" |
43919 | 111 |
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
|
112 |
|
28524 | 113 |
lemma jth_UU[simp]:"jth n UU = undefined" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
114 |
by (simp add: jth_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
115 |
|
63549 | 116 |
lemma ext_last:"\<lbrakk>s \<noteq> UU; enat (Suc n) = #s\<rbrakk> \<Longrightarrow> (stream_take n\<cdot>s) ooo <(last s)> = s" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
117 |
apply (simp add: last_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
118 |
apply (case_tac "#s", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
119 |
apply (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
120 |
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
|
121 |
apply (auto simp add: i_th_last) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
122 |
apply (drule slen_take_lemma1, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
123 |
apply (simp add: jth_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
124 |
apply (case_tac "i_th n s = UU") |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
125 |
apply auto |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
126 |
apply (simp add: i_th_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
127 |
apply (case_tac "i_rt n s = UU", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
128 |
apply (drule i_rt_slen [THEN iffD1]) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
129 |
apply (drule slen_take_eq_rev [rule_format, THEN iffD2],auto) |
49521 | 130 |
apply (drule not_Undef_is_Def [THEN iffD1], auto) |
131 |
done |
|
15188
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 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
134 |
lemma fsingleton_lemma1[simp]: "(<a> = <b>) = (a=b)" |
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 fsingleton_lemma2[simp]: "<a> ~= <>" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
138 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
139 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
140 |
lemma fsingleton_sconc:"<a> ooo s = Def a && s" |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
141 |
by (simp add: fsingleton_def2) |
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_ind: |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
144 |
"[| 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
|
145 |
apply (simp add: fsingleton_def2) |
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35572
diff
changeset
|
146 |
apply (rule stream.induct, auto) |
49521 | 147 |
apply (drule not_Undef_is_Def [THEN iffD1], auto) |
148 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
149 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
150 |
lemma fstreams_ind2: |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
151 |
"[| 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
|
152 |
apply (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
153 |
apply (rule stream_ind2, auto) |
49521 | 154 |
apply (drule not_Undef_is_Def [THEN iffD1], auto)+ |
155 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
156 |
|
63549 | 157 |
lemma fstreams_take_Suc[simp]: "stream_take (Suc n)\<cdot>(<a> ooo s) = <a> ooo stream_take n\<cdot>s" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
158 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
159 |
|
63549 | 160 |
lemma fstreams_not_empty[simp]: "<a> ooo s \<noteq> <>" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
161 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
162 |
|
63549 | 163 |
lemma fstreams_not_empty2[simp]: "s ooo <a> \<noteq> <>" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
164 |
by (case_tac "s=UU", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
165 |
|
63549 | 166 |
lemma fstreams_exhaust: "x = UU \<or> (\<exists>a s. x = <a> ooo s)" |
15188
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 (erule contrapos_pp, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
169 |
apply (drule stream_exhaust_eq [THEN iffD1], auto) |
49521 | 170 |
apply (drule not_Undef_is_Def [THEN iffD1], auto) |
171 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
172 |
|
63549 | 173 |
lemma fstreams_cases: "\<lbrakk>x = UU \<Longrightarrow> P; \<And>a y. x = <a> ooo y \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
174 |
by (insert fstreams_exhaust [of x], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
175 |
|
63549 | 176 |
lemma fstreams_exhaust_eq: "x \<noteq> UU \<longleftrightarrow> (\<exists>a y. x = <a> ooo y)" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
177 |
apply (simp add: fsingleton_def2, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
178 |
apply (drule stream_exhaust_eq [THEN iffD1], auto) |
49521 | 179 |
apply (drule not_Undef_is_Def [THEN iffD1], auto) |
180 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
181 |
|
63549 | 182 |
lemma fstreams_inject: "<a> ooo s = <b> ooo t \<longleftrightarrow> a = b \<and> s = t" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
183 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
184 |
|
63549 | 185 |
lemma fstreams_prefix: "<a> ooo s << t \<Longrightarrow> \<exists>tt. t = <a> ooo tt \<and> s << tt" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
186 |
apply (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
187 |
apply (insert stream_prefix [of "Def a" s t], auto) |
30807 | 188 |
done |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
189 |
|
63549 | 190 |
lemma fstreams_prefix': "x << <a> ooo z \<longleftrightarrow> x = <> \<or> (\<exists>y. x = <a> ooo y \<and> y << z)" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
191 |
apply (auto, case_tac "x=UU", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
192 |
apply (drule stream_exhaust_eq [THEN iffD1], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
193 |
apply (simp add: fsingleton_def2, auto) |
25920 | 194 |
apply (drule ax_flat, simp) |
49521 | 195 |
apply (erule sconc_mono) |
196 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
197 |
|
63549 | 198 |
lemma ft_fstreams[simp]: "ft\<cdot>(<a> ooo s) = Def a" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
199 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
200 |
|
63549 | 201 |
lemma rt_fstreams[simp]: "rt\<cdot>(<a> ooo s) = s" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
202 |
by (simp add: fsingleton_def2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
203 |
|
63549 | 204 |
lemma ft_eq[simp]: "ft\<cdot>s = Def a \<longleftrightarrow> (\<exists>t. s = <a> ooo t)" |
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35572
diff
changeset
|
205 |
apply (cases s, auto) |
49521 | 206 |
apply (auto simp add: fsingleton_def2) |
207 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
208 |
|
63549 | 209 |
lemma surjective_fstreams: "<d> ooo y = x \<longleftrightarrow> (ft\<cdot>x = Def d \<and> rt\<cdot>x = y)" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
210 |
by auto |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
211 |
|
63549 | 212 |
lemma fstreams_mono: "<a> ooo b << <a> ooo c \<Longrightarrow> b << c" |
30807 | 213 |
by (simp add: fsingleton_def2) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
214 |
|
63549 | 215 |
lemma fsmap_UU[simp]: "fsmap f\<cdot>UU = UU" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
216 |
by (simp add: fsmap_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
217 |
|
63549 | 218 |
lemma fsmap_fsingleton_sconc: "fsmap f\<cdot>(<x> ooo xs) = <(f x)> ooo (fsmap f\<cdot>xs)" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
219 |
by (simp add: fsmap_def fsingleton_def2 flift2_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
220 |
|
63549 | 221 |
lemma fsmap_fsingleton[simp]: "fsmap f\<cdot>(<x>) = <(f x)>" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
222 |
by (simp add: fsmap_def fsingleton_def2 flift2_def) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
223 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
224 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
225 |
lemma fstreams_chain_lemma[rule_format]: |
63549 | 226 |
"\<forall>s x y. stream_take n\<cdot>(s::'a fstream) << x \<and> x << y \<and> y << s \<and> x \<noteq> y \<longrightarrow> stream_take (Suc n)\<cdot>s << y" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
227 |
apply (induct_tac n, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
228 |
apply (case_tac "s=UU", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
229 |
apply (drule stream_exhaust_eq [THEN iffD1], 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], auto) |
40431 | 232 |
apply (simp add: flat_below_iff) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
233 |
apply (case_tac "s=UU", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
234 |
apply (drule stream_exhaust_eq [THEN iffD1], auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
235 |
apply (erule_tac x="ya" in allE) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
236 |
apply (drule stream_prefix, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
237 |
apply (case_tac "y=UU",auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
238 |
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
|
239 |
apply auto |
40431 | 240 |
apply (simp add: flat_below_iff) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
241 |
apply (erule_tac x="tt" in allE) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
242 |
apply (erule_tac x="yb" in allE, auto) |
40431 | 243 |
apply (simp add: flat_below_iff) |
49521 | 244 |
apply (simp add: flat_below_iff) |
245 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
246 |
|
63549 | 247 |
lemma fstreams_lub_lemma1: "\<lbrakk>chain Y; (LUB i. Y i) = <a> ooo s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = <a> ooo t" |
27413 | 248 |
apply (subgoal_tac "(LUB i. Y i) ~= UU") |
41431
138f414f14cb
remove various lemmas redundant with lub_eq_bottom_iff
huffman
parents:
41413
diff
changeset
|
249 |
apply (frule lub_eq_bottom_iff, auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
250 |
apply (drule_tac x="i" in is_ub_thelub, auto) |
49521 | 251 |
apply (drule fstreams_prefix' [THEN iffD1], auto) |
252 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
253 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
254 |
lemma fstreams_lub1: |
63549 | 255 |
"\<lbrakk>chain Y; (LUB i. Y i) = <a> ooo s\<rbrakk> |
256 |
\<Longrightarrow> (\<exists>j t. Y j = <a> ooo t) \<and> (\<exists>X. chain X \<and> (\<forall>i. \<exists>j. <a> ooo X i << Y j) \<and> (LUB i. X i) = s)" |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
257 |
apply (auto simp add: fstreams_lub_lemma1) |
63549 | 258 |
apply (rule_tac x="\<lambda>n. stream_take n\<cdot>s" in exI, auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
259 |
apply (induct_tac i, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
260 |
apply (drule fstreams_lub_lemma1, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
261 |
apply (rule_tac x="j" in exI, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
262 |
apply (case_tac "max_in_chain j Y") |
40771 | 263 |
apply (frule lub_finch1 [THEN lub_eqI], auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
264 |
apply (rule_tac x="j" in exI) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
265 |
apply (erule subst) back back |
40431 | 266 |
apply (simp add: below_prod_def sconc_mono) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
267 |
apply (simp add: max_in_chain_def, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
268 |
apply (rule_tac x="ja" in exI) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
269 |
apply (subgoal_tac "Y j << Y ja") |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
270 |
apply (drule fstreams_prefix, auto)+ |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
271 |
apply (rule sconc_mono) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
272 |
apply (rule fstreams_chain_lemma, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
273 |
apply (subgoal_tac "Y ja << (LUB i. (Y i))", clarsimp) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
274 |
apply (drule fstreams_mono, simp) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
275 |
apply (rule is_ub_thelub, simp) |
25922
cb04d05e95fb
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents:
25920
diff
changeset
|
276 |
apply (blast intro: chain_mono) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
277 |
by (rule stream_reach2) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
278 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
279 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
280 |
lemma lub_Pair_not_UU_lemma: |
63549 | 281 |
"\<lbrakk>chain Y; (LUB i. Y i) = ((a::'a::flat), b); a \<noteq> UU; b \<noteq> UU\<rbrakk> |
282 |
\<Longrightarrow> \<exists>j c d. Y j = (c, d) \<and> c \<noteq> UU \<and> d \<noteq> UU" |
|
40771 | 283 |
apply (frule lub_prod, clarsimp) |
41431
138f414f14cb
remove various lemmas redundant with lub_eq_bottom_iff
huffman
parents:
41413
diff
changeset
|
284 |
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
|
285 |
apply (case_tac "Y i", clarsimp) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
286 |
apply (case_tac "max_in_chain i Y") |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
287 |
apply (drule maxinch_is_thelub, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
288 |
apply (rule_tac x="i" in exI, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
289 |
apply (simp add: max_in_chain_def, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
290 |
apply (subgoal_tac "Y i << Y j",auto) |
40431 | 291 |
apply (simp add: below_prod_def, clarsimp) |
25920 | 292 |
apply (drule ax_flat, auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
293 |
apply (case_tac "snd (Y j) = UU",auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
294 |
apply (case_tac "Y j", auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
295 |
apply (rule_tac x="j" in exI) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
296 |
apply (case_tac "Y j",auto) |
49521 | 297 |
apply (drule chain_mono, auto) |
298 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
299 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
300 |
lemma fstreams_lub_lemma2: |
63549 | 301 |
"\<lbrakk>chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) \<noteq> UU\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = (a, <m> ooo t)" |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
302 |
apply (frule lub_Pair_not_UU_lemma, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
303 |
apply (drule_tac x="j" in is_ub_thelub, auto) |
25920 | 304 |
apply (drule ax_flat, clarsimp) |
49521 | 305 |
apply (drule fstreams_prefix' [THEN iffD1], auto) |
306 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
307 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
308 |
lemma fstreams_lub2: |
63549 | 309 |
"\<lbrakk>chain Y; (LUB i. Y i) = (a, <m> ooo ms); (a::'a::flat) \<noteq> UU\<rbrakk> |
310 |
\<Longrightarrow> (\<exists>j t. Y j = (a, <m> ooo t)) \<and> (\<exists>X. chain X \<and> (\<forall>i. \<exists>j. (a, <m> ooo X i) << Y j) \<and> (LUB i. X i) = ms)" |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
311 |
apply (auto simp add: fstreams_lub_lemma2) |
63549 | 312 |
apply (rule_tac x="\<lambda>n. stream_take n\<cdot>ms" in exI, auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
313 |
apply (induct_tac i, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
314 |
apply (drule fstreams_lub_lemma2, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
315 |
apply (rule_tac x="j" in exI, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
316 |
apply (case_tac "max_in_chain j Y") |
40771 | 317 |
apply (frule lub_finch1 [THEN lub_eqI], auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
318 |
apply (rule_tac x="j" in exI) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
319 |
apply (erule subst) back back |
26029 | 320 |
apply (simp add: sconc_mono) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
321 |
apply (simp add: max_in_chain_def, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
322 |
apply (rule_tac x="ja" in exI) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
323 |
apply (subgoal_tac "Y j << Y ja") |
40431 | 324 |
apply (simp add: below_prod_def, auto) |
325 |
apply (drule below_trans) |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
326 |
apply (simp add: ax_flat, auto) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
327 |
apply (drule fstreams_prefix, auto)+ |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
328 |
apply (rule sconc_mono) |
63549 | 329 |
apply (subgoal_tac "tt \<noteq> tta" "tta << ms") |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
330 |
apply (blast intro: fstreams_chain_lemma) |
40771 | 331 |
apply (frule lub_prod, auto) |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
332 |
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
|
333 |
apply (drule fstreams_mono, simp) |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
334 |
apply (rule is_ub_thelub chainI) |
40431 | 335 |
apply (simp add: chain_def below_prod_def) |
63549 | 336 |
apply (subgoal_tac "fst (Y j) \<noteq> fst (Y ja) \<or> snd (Y j) \<noteq> snd (Y ja)", simp) |
25920 | 337 |
apply (drule ax_flat, simp)+ |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
338 |
apply (drule prod_eqI, auto) |
25922
cb04d05e95fb
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents:
25920
diff
changeset
|
339 |
apply (simp add: chain_mono) |
49521 | 340 |
apply (rule stream_reach2) |
341 |
done |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
342 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
343 |
|
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
diff
changeset
|
344 |
lemma cpo_cont_lemma: |
63549 | 345 |
"\<lbrakk>monofun (f::'a::cpo \<Rightarrow> 'b::cpo); (\<forall>Y. chain Y \<longrightarrow> f (lub(range Y)) << (LUB i. f (Y i)))\<rbrakk> \<Longrightarrow> cont f" |
49521 | 346 |
apply (erule contI2) |
347 |
apply simp |
|
348 |
done |
|
15188
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 |
end |