author | huffman |
Sun, 21 Feb 2010 08:59:39 -0800 | |
changeset 35286 | 0e5fe22fa321 |
parent 35215 | a03462cbf86f |
child 35289 | 08e11c587c3d |
permissions | -rw-r--r-- |
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 |
|
22808 | 11 |
domain 'a seq = nil | cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65) |
3071 | 12 |
|
35286 | 13 |
(* |
17233 | 14 |
sfilter :: "('a -> tr) -> 'a seq -> 'a seq" |
3071 | 15 |
smap :: "('a -> 'b) -> 'a seq -> 'b seq" |
16 |
sforall :: "('a -> tr) => 'a seq => bool" |
|
17 |
sforall2 :: "('a -> tr) -> 'a seq -> tr" |
|
18 |
slast :: "'a seq -> 'a" |
|
19 |
sconc :: "'a seq -> 'a seq -> 'a seq" |
|
35286 | 20 |
sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq" |
21 |
stakewhile :: "('a -> tr) -> 'a seq -> 'a seq" |
|
22 |
szip :: "'a seq -> 'b seq -> ('a*'b) seq" |
|
3071 | 23 |
sflat :: "('a seq) seq -> 'a seq" |
24 |
||
25 |
sfinite :: "'a seq set" |
|
35286 | 26 |
Partial :: "'a seq => bool" |
27 |
Infinite :: "'a seq => bool" |
|
3071 | 28 |
|
29 |
nproj :: "nat => 'a seq => 'a" |
|
4282 | 30 |
sproj :: "nat => 'a seq => 'a seq" |
35286 | 31 |
*) |
3071 | 32 |
|
23778 | 33 |
inductive |
34 |
Finite :: "'a seq => bool" |
|
35 |
where |
|
36 |
sfinite_0: "Finite nil" |
|
37 |
| sfinite_n: "[| Finite tr; a~=UU |] ==> Finite (a##tr)" |
|
3071 | 38 |
|
35286 | 39 |
declare Finite.intros [simp] |
3071 | 40 |
|
35286 | 41 |
definition |
42 |
Partial :: "'a seq => bool" |
|
43 |
where |
|
3071 | 44 |
"Partial x == (seq_finite x) & ~(Finite x)" |
45 |
||
35286 | 46 |
definition |
47 |
Infinite :: "'a seq => bool" |
|
48 |
where |
|
3071 | 49 |
"Infinite x == ~(seq_finite x)" |
50 |
||
51 |
||
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
52 |
subsection {* recursive equations of operators *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
53 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
54 |
subsubsection {* smap *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
55 |
|
35286 | 56 |
fixrec |
57 |
smap :: "('a -> 'b) -> 'a seq -> 'b seq" |
|
58 |
where |
|
59 |
smap_nil: "smap$f$nil=nil" |
|
60 |
| 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
|
61 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
62 |
lemma smap_UU [simp]: "smap$f$UU=UU" |
35286 | 63 |
by fixrec_simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
64 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
65 |
subsubsection {* sfilter *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
66 |
|
35286 | 67 |
fixrec |
68 |
sfilter :: "('a -> tr) -> 'a seq -> 'a seq" |
|
69 |
where |
|
70 |
sfilter_nil: "sfilter$P$nil=nil" |
|
71 |
| sfilter_cons: |
|
72 |
"x~=UU ==> sfilter$P$(x##xs)= |
|
73 |
(If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)" |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
74 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
75 |
lemma sfilter_UU [simp]: "sfilter$P$UU=UU" |
35286 | 76 |
by fixrec_simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
77 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
78 |
subsubsection {* sforall2 *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
79 |
|
35286 | 80 |
fixrec |
81 |
sforall2 :: "('a -> tr) -> 'a seq -> tr" |
|
82 |
where |
|
83 |
sforall2_nil: "sforall2$P$nil=TT" |
|
84 |
| sforall2_cons: |
|
85 |
"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
|
86 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
87 |
lemma sforall2_UU [simp]: "sforall2$P$UU=UU" |
35286 | 88 |
by fixrec_simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
89 |
|
35286 | 90 |
definition |
91 |
sforall_def: "sforall P t == (sforall2$P$t ~=FF)" |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
92 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
93 |
subsubsection {* stakewhile *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
94 |
|
35286 | 95 |
fixrec |
96 |
stakewhile :: "('a -> tr) -> 'a seq -> 'a seq" |
|
97 |
where |
|
98 |
stakewhile_nil: "stakewhile$P$nil=nil" |
|
99 |
| stakewhile_cons: |
|
100 |
"x~=UU ==> stakewhile$P$(x##xs) = |
|
101 |
(If P$x then x##(stakewhile$P$xs) else nil fi)" |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
102 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
103 |
lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU" |
35286 | 104 |
by fixrec_simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
105 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
106 |
subsubsection {* sdropwhile *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
107 |
|
35286 | 108 |
fixrec |
109 |
sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq" |
|
110 |
where |
|
111 |
sdropwhile_nil: "sdropwhile$P$nil=nil" |
|
112 |
| sdropwhile_cons: |
|
113 |
"x~=UU ==> sdropwhile$P$(x##xs) = |
|
114 |
(If P$x then sdropwhile$P$xs else x##xs fi)" |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
115 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
116 |
lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU" |
35286 | 117 |
by fixrec_simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
118 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
119 |
subsubsection {* slast *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
120 |
|
35286 | 121 |
fixrec |
122 |
slast :: "'a seq -> 'a" |
|
123 |
where |
|
124 |
slast_nil: "slast$nil=UU" |
|
125 |
| slast_cons: |
|
126 |
"x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)" |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
127 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
128 |
lemma slast_UU [simp]: "slast$UU=UU" |
35286 | 129 |
by fixrec_simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
130 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
131 |
subsubsection {* sconc *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
132 |
|
35286 | 133 |
fixrec |
134 |
sconc :: "'a seq -> 'a seq -> 'a seq" |
|
135 |
where |
|
136 |
sconc_nil: "sconc$nil$y = y" |
|
137 |
| sconc_cons': |
|
138 |
"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
|
139 |
|
35286 | 140 |
abbreviation |
141 |
sconc_syn :: "'a seq => 'a seq => 'a seq" (infixr "@@" 65) where |
|
142 |
"xs @@ ys == sconc $ xs $ ys" |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
143 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
144 |
lemma sconc_UU [simp]: "UU @@ y=UU" |
35286 | 145 |
by fixrec_simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
146 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
147 |
lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)" |
35286 | 148 |
apply (cases "x=UU") |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
149 |
apply simp_all |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
150 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
151 |
|
35286 | 152 |
declare sconc_cons' [simp del] |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
153 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
154 |
subsubsection {* sflat *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
155 |
|
35286 | 156 |
fixrec |
157 |
sflat :: "('a seq) seq -> 'a seq" |
|
158 |
where |
|
159 |
sflat_nil: "sflat$nil=nil" |
|
160 |
| 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
|
161 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
162 |
lemma sflat_UU [simp]: "sflat$UU=UU" |
35286 | 163 |
by fixrec_simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
164 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
165 |
lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)" |
35286 | 166 |
by (cases "x=UU", simp_all) |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
167 |
|
35286 | 168 |
declare sflat_cons' [simp del] |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
169 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
170 |
subsubsection {* szip *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
171 |
|
35286 | 172 |
fixrec |
173 |
szip :: "'a seq -> 'b seq -> ('a*'b) seq" |
|
174 |
where |
|
175 |
szip_nil: "szip$nil$y=nil" |
|
176 |
| szip_cons_nil: "x~=UU ==> szip$(x##xs)$nil=UU" |
|
177 |
| szip_cons: |
|
178 |
"[| 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
|
179 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
180 |
lemma szip_UU1 [simp]: "szip$UU$y=UU" |
35286 | 181 |
by fixrec_simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
182 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
183 |
lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU" |
35286 | 184 |
by (cases x, simp_all, fixrec_simp) |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
185 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
186 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
187 |
subsection "scons, nil" |
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 |
lemma scons_inject_eq: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
190 |
"[|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
|
191 |
by simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
192 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
193 |
lemma nil_less_is_nil: "nil<<x ==> nil=x" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
194 |
apply (rule_tac x="x" in seq.casedist) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
195 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
196 |
apply simp |
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 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
199 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
200 |
subsection "sfilter, sforall, sconc" |
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 |
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
|
203 |
= (if b then tr1 @@ tr else tr2 @@ tr)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
204 |
by simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
205 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
206 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
207 |
lemma sfiltersconc: "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
208 |
apply (rule_tac x="x" in seq.ind) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
209 |
(* adm *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
210 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
211 |
(* base cases *) |
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 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
214 |
(* main case *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
215 |
apply (rule_tac p="P$a" in trE) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
216 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
217 |
apply simp |
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 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
220 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
221 |
lemma sforallPstakewhileP: "sforall P (stakewhile$P$x)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
222 |
apply (simp add: sforall_def) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
223 |
apply (rule_tac x="x" in seq.ind) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
224 |
(* adm *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
225 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
226 |
(* base cases *) |
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 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
229 |
(* main case *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
230 |
apply (rule_tac p="P$a" in trE) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
231 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
232 |
apply simp |
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 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
235 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
236 |
lemma forallPsfilterP: "sforall P (sfilter$P$x)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
237 |
apply (simp add: sforall_def) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
238 |
apply (rule_tac x="x" in seq.ind) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
239 |
(* adm *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
240 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
241 |
(* base cases *) |
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 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
244 |
(* main case *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
245 |
apply (rule_tac p="P$a" in trE) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
246 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
247 |
apply simp |
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 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
250 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
251 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
252 |
subsection "Finite" |
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 |
(* ---------------------------------------------------- *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
255 |
(* Proofs of rewrite rules for Finite: *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
256 |
(* 1. Finite(nil), (by definition) *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
257 |
(* 2. ~Finite(UU), *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
258 |
(* 3. a~=UU==> Finite(a##x)=Finite(x) *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
259 |
(* ---------------------------------------------------- *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
260 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
261 |
lemma Finite_UU_a: "Finite x --> x~=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
262 |
apply (rule impI) |
23778 | 263 |
apply (erule Finite.induct) |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
264 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
265 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
266 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
267 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
268 |
lemma Finite_UU [simp]: "~(Finite UU)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
269 |
apply (cut_tac x="UU" in Finite_UU_a) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
270 |
apply fast |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
271 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
272 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
273 |
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
|
274 |
apply (intro strip) |
23778 | 275 |
apply (erule Finite.cases) |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
276 |
apply fastsimp |
35215
a03462cbf86f
get rid of warnings about duplicate simp rules in all HOLCF theories
huffman
parents:
35174
diff
changeset
|
277 |
apply simp |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
278 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
279 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
280 |
lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
281 |
apply (rule iffI) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
282 |
apply (erule (1) Finite_cons_a [rule_format]) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
283 |
apply fast |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
284 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
285 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
286 |
|
25803 | 287 |
lemma Finite_upward: "\<lbrakk>Finite x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> Finite y" |
288 |
apply (induct arbitrary: y set: Finite) |
|
289 |
apply (rule_tac x=y in seq.casedist, simp, simp, simp) |
|
290 |
apply (rule_tac x=y in seq.casedist, simp, simp) |
|
35215
a03462cbf86f
get rid of warnings about duplicate simp rules in all HOLCF theories
huffman
parents:
35174
diff
changeset
|
291 |
apply simp |
25803 | 292 |
done |
293 |
||
294 |
lemma adm_Finite [simp]: "adm Finite" |
|
295 |
by (rule adm_upward, rule Finite_upward) |
|
296 |
||
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
297 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
298 |
subsection "induction" |
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 |
|
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 |
(* Extensions to Induction Theorems *) |
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 |
|
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 |
lemma seq_finite_ind_lemma: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
307 |
assumes "(!!n. P(seq_take n$s))" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
308 |
shows "seq_finite(s) -->P(s)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
309 |
apply (unfold seq.finite_def) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
310 |
apply (intro strip) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
311 |
apply (erule exE) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
312 |
apply (erule subst) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
313 |
apply (rule prems) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
314 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
315 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
316 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
317 |
lemma seq_finite_ind: "!!P.[|P(UU);P(nil); |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
318 |
!! x s1.[|x~=UU;P(s1)|] ==> P(x##s1) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
319 |
|] ==> seq_finite(s) --> P(s)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
320 |
apply (rule seq_finite_ind_lemma) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
321 |
apply (erule seq.finite_ind) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
322 |
apply assumption |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
323 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
324 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
325 |
|
3071 | 326 |
end |