author  huffman 
Sat, 27 Nov 2010 16:08:10 0800  
changeset 40774  0437dbc127b3 
parent 40329  src/HOLCF/IOA/meta_theory/Seq.thy@73f2b99b549d 
child 40945  b8703f63bfb2 
permissions  rwrr 
3071  1 
(* Title: HOLCF/IOA/meta_theory/Seq.thy 
12218  2 
Author: Olaf Müller 
17233  3 
*) 
3071  4 

17233  5 
header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *} 
3071  6 

17233  7 
theory Seq 
8 
imports HOLCF 

9 
begin 

3071  10 

40329
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40322
diff
changeset

11 
default_sort pcpo 
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40322
diff
changeset

12 

73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40322
diff
changeset

13 
domain (unsafe) 'a seq = nil ("nil")  cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65) 
3071  14 

35286  15 
(* 
17233  16 
sfilter :: "('a > tr) > 'a seq > 'a seq" 
3071  17 
smap :: "('a > 'b) > 'a seq > 'b seq" 
18 
sforall :: "('a > tr) => 'a seq => bool" 

19 
sforall2 :: "('a > tr) > 'a seq > tr" 

20 
slast :: "'a seq > 'a" 

21 
sconc :: "'a seq > 'a seq > 'a seq" 

35286  22 
sdropwhile :: "('a > tr) > 'a seq > 'a seq" 
23 
stakewhile :: "('a > tr) > 'a seq > 'a seq" 

24 
szip :: "'a seq > 'b seq > ('a*'b) seq" 

3071  25 
sflat :: "('a seq) seq > 'a seq" 
26 

27 
sfinite :: "'a seq set" 

35286  28 
Partial :: "'a seq => bool" 
29 
Infinite :: "'a seq => bool" 

3071  30 

31 
nproj :: "nat => 'a seq => 'a" 

4282  32 
sproj :: "nat => 'a seq => 'a seq" 
35286  33 
*) 
3071  34 

23778  35 
inductive 
36 
Finite :: "'a seq => bool" 

37 
where 

38 
sfinite_0: "Finite nil" 

39 
 sfinite_n: "[ Finite tr; a~=UU ] ==> Finite (a##tr)" 

3071  40 

35286  41 
declare Finite.intros [simp] 
3071  42 

35286  43 
definition 
44 
Partial :: "'a seq => bool" 

45 
where 

3071  46 
"Partial x == (seq_finite x) & ~(Finite x)" 
47 

35286  48 
definition 
49 
Infinite :: "'a seq => bool" 

50 
where 

3071  51 
"Infinite x == ~(seq_finite x)" 
52 

53 

19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

54 
subsection {* recursive equations of operators *} 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

55 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

56 
subsubsection {* smap *} 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

57 

35286  58 
fixrec 
59 
smap :: "('a > 'b) > 'a seq > 'b seq" 

60 
where 

61 
smap_nil: "smap$f$nil=nil" 

62 
 smap_cons: "[x~=UU] ==> smap$f$(x##xs)= (f$x)##smap$f$xs" 

19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

63 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

64 
lemma smap_UU [simp]: "smap$f$UU=UU" 
35286  65 
by fixrec_simp 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

66 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

67 
subsubsection {* sfilter *} 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

68 

35286  69 
fixrec 
70 
sfilter :: "('a > tr) > 'a seq > 'a seq" 

71 
where 

72 
sfilter_nil: "sfilter$P$nil=nil" 

73 
 sfilter_cons: 

74 
"x~=UU ==> sfilter$P$(x##xs)= 

40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
35924
diff
changeset

75 
(If P$x then x##(sfilter$P$xs) else sfilter$P$xs)" 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

76 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

77 
lemma sfilter_UU [simp]: "sfilter$P$UU=UU" 
35286  78 
by fixrec_simp 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

79 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

80 
subsubsection {* sforall2 *} 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

81 

35286  82 
fixrec 
83 
sforall2 :: "('a > tr) > 'a seq > tr" 

84 
where 

85 
sforall2_nil: "sforall2$P$nil=TT" 

86 
 sforall2_cons: 

87 
"x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)" 

19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

88 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

89 
lemma sforall2_UU [simp]: "sforall2$P$UU=UU" 
35286  90 
by fixrec_simp 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

91 

35286  92 
definition 
93 
sforall_def: "sforall P t == (sforall2$P$t ~=FF)" 

19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

94 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

95 
subsubsection {* stakewhile *} 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

96 

35286  97 
fixrec 
98 
stakewhile :: "('a > tr) > 'a seq > 'a seq" 

99 
where 

100 
stakewhile_nil: "stakewhile$P$nil=nil" 

101 
 stakewhile_cons: 

102 
"x~=UU ==> stakewhile$P$(x##xs) = 

40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
35924
diff
changeset

103 
(If P$x then x##(stakewhile$P$xs) else nil)" 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

104 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

105 
lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU" 
35286  106 
by fixrec_simp 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

107 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

108 
subsubsection {* sdropwhile *} 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

109 

35286  110 
fixrec 
111 
sdropwhile :: "('a > tr) > 'a seq > 'a seq" 

112 
where 

113 
sdropwhile_nil: "sdropwhile$P$nil=nil" 

114 
 sdropwhile_cons: 

115 
"x~=UU ==> sdropwhile$P$(x##xs) = 

40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
35924
diff
changeset

116 
(If P$x then sdropwhile$P$xs else x##xs)" 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

117 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

118 
lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU" 
35286  119 
by fixrec_simp 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

120 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

121 
subsubsection {* slast *} 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

122 

35286  123 
fixrec 
124 
slast :: "'a seq > 'a" 

125 
where 

126 
slast_nil: "slast$nil=UU" 

127 
 slast_cons: 

40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
35924
diff
changeset

128 
"x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs)" 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

129 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

130 
lemma slast_UU [simp]: "slast$UU=UU" 
35286  131 
by fixrec_simp 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

132 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

133 
subsubsection {* sconc *} 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

134 

35286  135 
fixrec 
136 
sconc :: "'a seq > 'a seq > 'a seq" 

137 
where 

138 
sconc_nil: "sconc$nil$y = y" 

139 
 sconc_cons': 

140 
"x~=UU ==> sconc$(x##xs)$y = x##(sconc$xs$y)" 

19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

141 

35286  142 
abbreviation 
143 
sconc_syn :: "'a seq => 'a seq => 'a seq" (infixr "@@" 65) where 

144 
"xs @@ ys == sconc $ xs $ ys" 

19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

145 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

146 
lemma sconc_UU [simp]: "UU @@ y=UU" 
35286  147 
by fixrec_simp 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

148 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

149 
lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)" 
35286  150 
apply (cases "x=UU") 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

151 
apply simp_all 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

152 
done 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

153 

35286  154 
declare sconc_cons' [simp del] 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

155 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

156 
subsubsection {* sflat *} 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

157 

35286  158 
fixrec 
159 
sflat :: "('a seq) seq > 'a seq" 

160 
where 

161 
sflat_nil: "sflat$nil=nil" 

162 
 sflat_cons': "x~=UU ==> sflat$(x##xs)= x@@(sflat$xs)" 

19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

163 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

164 
lemma sflat_UU [simp]: "sflat$UU=UU" 
35286  165 
by fixrec_simp 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

166 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

167 
lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)" 
35286  168 
by (cases "x=UU", simp_all) 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

169 

35286  170 
declare sflat_cons' [simp del] 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

171 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

172 
subsubsection {* szip *} 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

173 

35286  174 
fixrec 
175 
szip :: "'a seq > 'b seq > ('a*'b) seq" 

176 
where 

177 
szip_nil: "szip$nil$y=nil" 

178 
 szip_cons_nil: "x~=UU ==> szip$(x##xs)$nil=UU" 

179 
 szip_cons: 

35924  180 
"[ x~=UU; y~=UU] ==> szip$(x##xs)$(y##ys) = (x,y)##szip$xs$ys" 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

181 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

182 
lemma szip_UU1 [simp]: "szip$UU$y=UU" 
35286  183 
by fixrec_simp 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

184 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

185 
lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU" 
35286  186 
by (cases x, simp_all, fixrec_simp) 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

187 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

188 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

189 
subsection "scons, nil" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

190 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

191 
lemma scons_inject_eq: 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

192 
"[x~=UU;y~=UU]==> (x##xs=y##ys) = (x=y & xs=ys)" 
35215
a03462cbf86f
get rid of warnings about duplicate simp rules in all HOLCF theories
huffman
parents:
35174
diff
changeset

193 
by simp 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

194 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

195 
lemma nil_less_is_nil: "nil<<x ==> nil=x" 
35532
60647586b173
adapt to changed variable name in casedist theorem
huffman
parents:
35289
diff
changeset

196 
apply (cases x) 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

197 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

198 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

199 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

200 
done 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

201 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

202 
subsection "sfilter, sforall, sconc" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

203 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

204 
lemma if_and_sconc [simp]: "(if b then tr1 else tr2) @@ tr 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

205 
= (if b then tr1 @@ tr else tr2 @@ tr)" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

206 
by simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

207 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

208 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

209 
lemma sfiltersconc: "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)" 
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35532
diff
changeset

210 
apply (induct x) 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

211 
(* adm *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

212 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

213 
(* base cases *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

214 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

215 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

216 
(* main case *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

217 
apply (rule_tac p="P$a" in trE) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

218 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

219 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

220 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

221 
done 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

222 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

223 
lemma sforallPstakewhileP: "sforall P (stakewhile$P$x)" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

224 
apply (simp add: sforall_def) 
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35532
diff
changeset

225 
apply (induct x) 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

226 
(* adm *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

227 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

228 
(* base cases *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

229 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

230 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

231 
(* main case *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

232 
apply (rule_tac p="P$a" in trE) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

233 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

234 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

235 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

236 
done 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

237 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

238 
lemma forallPsfilterP: "sforall P (sfilter$P$x)" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

239 
apply (simp add: sforall_def) 
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35532
diff
changeset

240 
apply (induct x) 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

241 
(* adm *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

242 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

243 
(* base cases *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

244 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

245 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

246 
(* main case *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

247 
apply (rule_tac p="P$a" in trE) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

248 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

249 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

250 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

251 
done 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

252 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

253 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

254 
subsection "Finite" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

255 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

256 
(*  *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

257 
(* Proofs of rewrite rules for Finite: *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

258 
(* 1. Finite(nil), (by definition) *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

259 
(* 2. ~Finite(UU), *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

260 
(* 3. a~=UU==> Finite(a##x)=Finite(x) *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

261 
(*  *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

262 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

263 
lemma Finite_UU_a: "Finite x > x~=UU" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

264 
apply (rule impI) 
23778  265 
apply (erule Finite.induct) 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

266 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

267 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

268 
done 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

269 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

270 
lemma Finite_UU [simp]: "~(Finite UU)" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

271 
apply (cut_tac x="UU" in Finite_UU_a) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

272 
apply fast 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

273 
done 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

274 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

275 
lemma Finite_cons_a: "Finite x > a~=UU > x=a##xs > Finite xs" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

276 
apply (intro strip) 
23778  277 
apply (erule Finite.cases) 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

278 
apply fastsimp 
35215
a03462cbf86f
get rid of warnings about duplicate simp rules in all HOLCF theories
huffman
parents:
35174
diff
changeset

279 
apply simp 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

280 
done 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

281 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

282 
lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

283 
apply (rule iffI) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

284 
apply (erule (1) Finite_cons_a [rule_format]) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

285 
apply fast 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

286 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

287 
done 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

288 

25803  289 
lemma Finite_upward: "\<lbrakk>Finite x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> Finite y" 
290 
apply (induct arbitrary: y set: Finite) 

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

291 
apply (case_tac y, simp, simp, simp) 
60647586b173
adapt to changed variable name in casedist theorem
huffman
parents:
35289
diff
changeset

292 
apply (case_tac y, simp, simp) 
35215
a03462cbf86f
get rid of warnings about duplicate simp rules in all HOLCF theories
huffman
parents:
35174
diff
changeset

293 
apply simp 
25803  294 
done 
295 

296 
lemma adm_Finite [simp]: "adm Finite" 

297 
by (rule adm_upward, rule Finite_upward) 

298 

19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

299 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

300 
subsection "induction" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

301 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

302 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

303 
(* *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

304 
(* Extensions to Induction Theorems *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

305 
(* *) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

306 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

307 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

308 
lemma seq_finite_ind_lemma: 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

309 
assumes "(!!n. P(seq_take n$s))" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

310 
shows "seq_finite(s) >P(s)" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

311 
apply (unfold seq.finite_def) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

312 
apply (intro strip) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

313 
apply (erule exE) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

314 
apply (erule subst) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

315 
apply (rule prems) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

316 
done 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

317 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

318 

ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

319 
lemma seq_finite_ind: "!!P.[P(UU);P(nil); 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

320 
!! x s1.[x~=UU;P(s1)] ==> P(x##s1) 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

321 
] ==> seq_finite(s) > P(s)" 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

322 
apply (rule seq_finite_ind_lemma) 
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35532
diff
changeset

323 
apply (erule seq.finite_induct) 
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

324 
apply assumption 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

325 
apply simp 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

326 
done 
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset

327 

3071  328 
end 