author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45049  13efaee97111 
child 58880  0baae4311a9f 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/FOCUS/Fstream.thy 
17293  2 
Author: David von Oheimb, TU Muenchen 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

3 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30807
diff
changeset

4 
FOCUS streams (with lifted elements). 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30807
diff
changeset

5 

69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30807
diff
changeset

6 
TODO: integrate Fstreams.thy 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

7 
*) 
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

8 

17293  9 
header {* FOCUS flat streams *} 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

10 

17293  11 
theory Fstream 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41027
diff
changeset

12 
imports "~~/src/HOL/HOLCF/Library/Stream" 
17293  13 
begin 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

14 

36452  15 
default_sort type 
17293  16 

41476  17 
type_synonym 'a fstream = "'a lift stream" 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

18 

19763  19 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

20 
fscons :: "'a \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where 
19763  21 
"fscons a = (\<Lambda> s. Def a && s)" 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
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 
fsfilter :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where 
19763  25 
"fsfilter A = (sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A)))" 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

26 

19763  27 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

28 
emptystream :: "'a fstream" ("<>") where 
19763  29 
"<> == \<bottom>" 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

30 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

31 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

32 
fscons' :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_~>_)" [66,65] 65) where 
19763  33 
"a~>s == fscons a\<cdot>s" 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

34 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

35 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

36 
fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63) where 
19763  37 
"A(C)s == fsfilter A\<cdot>s" 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

38 

21210  39 
notation (xsymbols) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

40 
fscons' ("(_\<leadsto>_)" [66,65] 65) and 
19763  41 
fsfilter' ("(_\<copyright>_)" [64,63] 63) 
11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

42 

4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

43 

19759  44 
lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d" 
40087  45 
by simp 
19759  46 

47 

48 
section "fscons" 

49 

50 
lemma fscons_def2: "a~>s = Def a && s" 

51 
apply (unfold fscons_def) 

52 
apply (simp) 

53 
done 

54 

55 
lemma fstream_exhaust: "x = UU  (? a y. x = a~> y)" 

56 
apply (simp add: fscons_def2) 

35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35532
diff
changeset

57 
apply (cut_tac stream.nchotomy) 
19759  58 
apply (fast dest: not_Undef_is_Def [THEN iffD1]) 
59 
done 

60 

61 
lemma fstream_cases: "[ x = UU ==> P; !!a y. x = a~> y ==> P ] ==> P" 

62 
apply (cut_tac fstream_exhaust) 

63 
apply (erule disjE) 

64 
apply fast 

65 
apply fast 

66 
done 

27148  67 

19759  68 
lemma fstream_exhaust_eq: "(x ~= UU) = (? a y. x = a~> y)" 
69 
apply (simp add: fscons_def2 stream_exhaust_eq) 

70 
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) 

71 
done 

72 

73 

74 
lemma fscons_not_empty [simp]: "a~> s ~= <>" 

75 
by (simp add: fscons_def2) 

76 

77 

78 
lemma fscons_inject [simp]: "(a~> s = b~> t) = (a = b & s = t)" 

79 
by (simp add: fscons_def2) 

80 

81 
lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt & s << tt" 

35532
60647586b173
adapt to changed variable name in casedist theorem
huffman
parents:
35215
diff
changeset

82 
apply (cases t) 
19759  83 
apply (cut_tac fscons_not_empty) 
45049  84 
apply (fast dest: bottomI) 
19759  85 
apply (simp add: fscons_def2) 
86 
done 

87 

88 
lemma fstream_prefix' [simp]: 

89 
"x << a~> z = (x = <>  (? y. x = a~> y & y << z))" 

45049  90 
apply (simp add: fscons_def2 lift.distinct(2) [THEN stream_prefix']) 
19759  91 
apply (safe) 
92 
apply (erule_tac [!] contrapos_np) 

93 
prefer 2 apply (fast elim: DefE) 

40009  94 
apply (rule lift.exhaust) 
19759  95 
apply (erule (1) notE) 
96 
apply (safe) 

40431  97 
apply (drule Def_below_Def [THEN iffD1]) 
19759  98 
apply fast 
99 
done 

100 

101 
(*  *) 

102 

103 
section "ft & rt" 

104 

105 
lemmas ft_empty = stream.sel_rews (1) 

106 
lemma ft_fscons [simp]: "ft\<cdot>(m~> s) = Def m" 

107 
by (simp add: fscons_def) 

108 

109 
lemmas rt_empty = stream.sel_rews (2) 

110 
lemma rt_fscons [simp]: "rt\<cdot>(m~> s) = s" 

111 
by (simp add: fscons_def) 

112 

113 
lemma ft_eq [simp]: "(ft\<cdot>s = Def a) = (? t. s = a~> t)" 

114 
apply (unfold fscons_def) 

115 
apply (simp) 

116 
apply (safe) 

117 
apply (erule subst) 

118 
apply (rule exI) 

119 
apply (rule surjectiv_scons [symmetric]) 

120 
apply (simp) 

121 
done 

122 

123 
lemma surjective_fscons_lemma: "(d\<leadsto>y = x) = (ft\<cdot>x = Def d & rt\<cdot>x = y)" 

124 
by auto 

125 

126 
lemma surjective_fscons: "ft\<cdot>x = Def d \<Longrightarrow> d\<leadsto>rt\<cdot>x = x" 

127 
by (simp add: surjective_fscons_lemma) 

128 

129 

130 
(*  *) 

131 

132 
section "take" 

133 

134 
lemma fstream_take_Suc [simp]: 

135 
"stream_take (Suc n)\<cdot>(a~> s) = a~> stream_take n\<cdot>s" 

136 
by (simp add: fscons_def) 

137 

138 

139 
(*  *) 

140 

141 
section "slen" 

142 

44019
ee784502aed5
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents:
43924
diff
changeset

143 
lemma slen_fscons: "#(m~> s) = eSuc (#s)" 
19759  144 
by (simp add: fscons_def) 
145 

146 
lemma slen_fscons_eq: 

43924  147 
"(enat (Suc n) < #x) = (? a y. x = a~> y & enat n < #y)" 
19759  148 
apply (simp add: fscons_def2 slen_scons_eq) 
149 
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) 

150 
done 

151 

152 
lemma slen_fscons_eq_rev: 

43924  153 
"(#x < enat (Suc (Suc n))) = (!a y. x ~= a~> y  #y < enat (Suc n))" 
19759  154 
apply (simp add: fscons_def2 slen_scons_eq_rev) 
42793  155 
apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *}) 
156 
apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *}) 

157 
apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *}) 

158 
apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *}) 

159 
apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *}) 

160 
apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *}) 

19759  161 
apply (erule contrapos_np) 
162 
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) 

163 
done 

164 

165 
lemma slen_fscons_less_eq: 

43924  166 
"(#(a~> y) < enat (Suc (Suc n))) = (#y < enat (Suc n))" 
19759  167 
apply (subst slen_fscons_eq_rev) 
168 
apply (fast dest!: fscons_inject [THEN iffD1]) 

169 
done 

170 

171 

172 
(*  *) 

173 

174 
section "induction" 

175 

176 
lemma fstream_ind: 

177 
"[ adm P; P <>; !!a s. P s ==> P (a~> s) ] ==> P x" 

35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35532
diff
changeset

178 
apply (erule stream.induct) 
19759  179 
apply (assumption) 
180 
apply (unfold fscons_def2) 

181 
apply (fast dest: not_Undef_is_Def [THEN iffD1]) 

182 
done 

183 

184 
lemma fstream_ind2: 

185 
"[ adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) ] ==> P x" 

186 
apply (erule stream_ind2) 

187 
apply (assumption) 

188 
apply (unfold fscons_def2) 

189 
apply (fast dest: not_Undef_is_Def [THEN iffD1]) 

190 
apply (fast dest: not_Undef_is_Def [THEN iffD1]) 

191 
done 

192 

193 

194 
(*  *) 

195 

196 
section "fsfilter" 

197 

198 
lemma fsfilter_empty: "A(C)UU = UU" 

199 
apply (unfold fsfilter_def) 

200 
apply (rule sfilter_empty) 

201 
done 

202 

203 
lemma fsfilter_fscons: 

204 
"A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)" 

205 
apply (unfold fsfilter_def) 

35215
a03462cbf86f
get rid of warnings about duplicate simp rules in all HOLCF theories
huffman
parents:
32960
diff
changeset

206 
apply (simp add: fscons_def2 If_and_if) 
19759  207 
done 
208 

209 
lemma fsfilter_emptys: "{}(C)x = UU" 

210 
apply (rule_tac x="x" in fstream_ind) 

211 
apply (simp) 

212 
apply (rule fsfilter_empty) 

213 
apply (simp add: fsfilter_fscons) 

214 
done 

215 

216 
lemma fsfilter_insert: "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)" 

217 
by (simp add: fsfilter_fscons) 

218 

219 
lemma fsfilter_single_in: "{a}(C)a~> x = a~> ({a}(C)x)" 

220 
by (rule fsfilter_insert) 

221 

222 
lemma fsfilter_single_out: "b ~= a ==> {a}(C)b~> x = ({a}(C)x)" 

223 
by (simp add: fsfilter_fscons) 

224 

225 
lemma fstream_lub_lemma1: 

27413  226 
"\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t" 
19759  227 
apply (case_tac "max_in_chain i Y") 
40771  228 
apply (drule (1) lub_finch1 [THEN lub_eqI, THEN sym]) 
19759  229 
apply (force) 
230 
apply (unfold max_in_chain_def) 

231 
apply auto 

25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
24327
diff
changeset

232 
apply (frule (1) chain_mono) 
19759  233 
apply (rule_tac x="Y j" in fstream_cases) 
234 
apply (force) 

235 
apply (drule_tac x="j" in is_ub_thelub) 

236 
apply (force) 

237 
done 

238 

239 
lemma fstream_lub_lemma: 

27413  240 
"\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> (\<exists>j t. Y j = a\<leadsto>t) & (\<exists>X. chain X & (!i. ? j. Y j = a\<leadsto>X i) & (\<Squnion>i. X i) = s)" 
19759  241 
apply (frule (1) fstream_lub_lemma1) 
242 
apply (clarsimp) 

243 
apply (rule_tac x="%i. rt\<cdot>(Y(i+j))" in exI) 

244 
apply (rule conjI) 

245 
apply (erule chain_shift [THEN chain_monofun]) 

246 
apply safe 

25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
24327
diff
changeset

247 
apply (drule_tac i="j" and j="i+j" in chain_mono) 
19759  248 
apply (simp) 
249 
apply (simp) 

250 
apply (rule_tac x="i+j" in exI) 

251 
apply (drule fstream_prefix) 

252 
apply (clarsimp) 

41027  253 
apply (subst lub_APP) 
19759  254 
apply (rule chainI) 
255 
apply (fast) 

256 
apply (erule chain_shift) 

40771  257 
apply (subst lub_const) 
19759  258 
apply (subst lub_range_shift) 
259 
apply (assumption) 

260 
apply (simp) 

261 
done 

262 

11350
4c55b020d6ee
added FOCUS including the OneElement Buffer by Manfred Broy
oheimb
parents:
diff
changeset

263 
end 