author | wenzelm |
Thu, 26 Apr 2007 14:24:08 +0200 | |
changeset 22808 | a7daa74e2980 |
parent 19804 | d0318ae1141c |
child 23778 | 18f426a137a9 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/Seq.thy |
3275 | 2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
17233 | 4 |
*) |
3071 | 5 |
|
17233 | 6 |
header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *} |
3071 | 7 |
|
17233 | 8 |
theory Seq |
9 |
imports HOLCF |
|
10 |
begin |
|
3071 | 11 |
|
22808 | 12 |
domain 'a seq = nil | cons (HD :: 'a) (lazy TL :: "'a seq") (infixr "##" 65) |
3071 | 13 |
|
17233 | 14 |
consts |
15 |
sfilter :: "('a -> tr) -> 'a seq -> 'a seq" |
|
3071 | 16 |
smap :: "('a -> 'b) -> 'a seq -> 'b seq" |
17 |
sforall :: "('a -> tr) => 'a seq => bool" |
|
18 |
sforall2 :: "('a -> tr) -> 'a seq -> tr" |
|
19 |
slast :: "'a seq -> 'a" |
|
20 |
sconc :: "'a seq -> 'a seq -> 'a seq" |
|
17233 | 21 |
sdropwhile ::"('a -> tr) -> 'a seq -> 'a seq" |
22 |
stakewhile ::"('a -> tr) -> 'a seq -> 'a seq" |
|
23 |
szip ::"'a seq -> 'b seq -> ('a*'b) seq" |
|
3071 | 24 |
sflat :: "('a seq) seq -> 'a seq" |
25 |
||
26 |
sfinite :: "'a seq set" |
|
27 |
Partial ::"'a seq => bool" |
|
28 |
Infinite ::"'a seq => bool" |
|
29 |
||
30 |
nproj :: "nat => 'a seq => 'a" |
|
4282 | 31 |
sproj :: "nat => 'a seq => 'a seq" |
3071 | 32 |
|
22808 | 33 |
abbreviation |
34 |
sconc_syn :: "'a seq => 'a seq => 'a seq" (infixr "@@" 65) where |
|
35 |
"xs @@ ys == sconc $ xs $ ys" |
|
3071 | 36 |
|
22808 | 37 |
abbreviation |
38 |
Finite :: "'a seq => bool" where |
|
39 |
"Finite x == x:sfinite" |
|
3071 | 40 |
|
17233 | 41 |
defs |
3071 | 42 |
|
43 |
(* f not possible at lhs, as "pattern matching" only for % x arguments, |
|
44 |
f cannot be written at rhs in front, as fix_eq3 does not apply later *) |
|
17233 | 45 |
smap_def: |
46 |
"smap == (fix$(LAM h f tr. case tr of |
|
3071 | 47 |
nil => nil |
10835 | 48 |
| x##xs => f$x ## h$f$xs))" |
3071 | 49 |
|
17233 | 50 |
sfilter_def: |
51 |
"sfilter == (fix$(LAM h P t. case t of |
|
52 |
nil => nil |
|
53 |
| x##xs => If P$x |
|
10835 | 54 |
then x##(h$P$xs) |
55 |
else h$P$xs |
|
17233 | 56 |
fi))" |
57 |
sforall_def: |
|
58 |
"sforall P t == (sforall2$P$t ~=FF)" |
|
3071 | 59 |
|
60 |
||
17233 | 61 |
sforall2_def: |
62 |
"sforall2 == (fix$(LAM h P t. case t of |
|
63 |
nil => TT |
|
64 |
| x##xs => P$x andalso h$P$xs))" |
|
65 |
||
66 |
sconc_def: |
|
67 |
"sconc == (fix$(LAM h t1 t2. case t1 of |
|
3071 | 68 |
nil => t2 |
10835 | 69 |
| x##xs => x##(h$xs$t2)))" |
3071 | 70 |
|
17233 | 71 |
slast_def: |
72 |
"slast == (fix$(LAM h t. case t of |
|
73 |
nil => UU |
|
74 |
| x##xs => (If is_nil$xs |
|
3071 | 75 |
then x |
10835 | 76 |
else h$xs fi)))" |
3071 | 77 |
|
17233 | 78 |
stakewhile_def: |
79 |
"stakewhile == (fix$(LAM h P t. case t of |
|
80 |
nil => nil |
|
81 |
| x##xs => If P$x |
|
10835 | 82 |
then x##(h$P$xs) |
3071 | 83 |
else nil |
17233 | 84 |
fi))" |
85 |
sdropwhile_def: |
|
86 |
"sdropwhile == (fix$(LAM h P t. case t of |
|
87 |
nil => nil |
|
88 |
| x##xs => If P$x |
|
10835 | 89 |
then h$P$xs |
3071 | 90 |
else t |
17233 | 91 |
fi))" |
92 |
sflat_def: |
|
93 |
"sflat == (fix$(LAM h t. case t of |
|
94 |
nil => nil |
|
95 |
| x##xs => x @@ (h$xs)))" |
|
3071 | 96 |
|
17233 | 97 |
szip_def: |
98 |
"szip == (fix$(LAM h t1 t2. case t1 of |
|
3071 | 99 |
nil => nil |
17233 | 100 |
| x##xs => (case t2 of |
101 |
nil => UU |
|
10835 | 102 |
| y##ys => <x,y>##(h$xs$ys))))" |
3071 | 103 |
|
17233 | 104 |
Partial_def: |
3071 | 105 |
"Partial x == (seq_finite x) & ~(Finite x)" |
106 |
||
17233 | 107 |
Infinite_def: |
3071 | 108 |
"Infinite x == ~(seq_finite x)" |
109 |
||
110 |
||
17233 | 111 |
inductive "sfinite" |
112 |
intros |
|
113 |
sfinite_0: "nil:sfinite" |
|
114 |
sfinite_n: "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite" |
|
3071 | 115 |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
116 |
declare sfinite.intros [simp] |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
117 |
declare seq.rews [simp] |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
118 |
|
19804 | 119 |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
120 |
subsection {* recursive equations of operators *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
121 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
122 |
subsubsection {* smap *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
123 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
124 |
lemma smap_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
125 |
"smap = (LAM f tr. case tr of nil => nil | x##xs => f$x ## smap$f$xs)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
126 |
by (subst fix_eq2 [OF smap_def], simp) |
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 smap_nil [simp]: "smap$f$nil=nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
129 |
by (subst smap_unfold, simp) |
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 |
lemma smap_UU [simp]: "smap$f$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
132 |
by (subst smap_unfold, simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
133 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
134 |
lemma smap_cons [simp]: "[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
135 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
136 |
apply (subst smap_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
137 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
138 |
apply (rule refl) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
139 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
140 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
141 |
subsubsection {* sfilter *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
142 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
143 |
lemma sfilter_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
144 |
"sfilter = (LAM P tr. case tr of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
145 |
nil => nil |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
146 |
| x##xs => If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
147 |
by (subst fix_eq2 [OF sfilter_def], simp) |
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 sfilter_nil [simp]: "sfilter$P$nil=nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
150 |
by (subst sfilter_unfold, simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
151 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
152 |
lemma sfilter_UU [simp]: "sfilter$P$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
153 |
by (subst sfilter_unfold, simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
154 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
155 |
lemma sfilter_cons [simp]: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
156 |
"x~=UU ==> sfilter$P$(x##xs)= |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
157 |
(If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
158 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
159 |
apply (subst sfilter_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
160 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
161 |
apply (rule refl) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
162 |
done |
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 |
subsubsection {* sforall2 *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
165 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
166 |
lemma sforall2_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
167 |
"sforall2 = (LAM P tr. case tr of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
168 |
nil => TT |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
169 |
| x##xs => (P$x andalso sforall2$P$xs))" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
170 |
by (subst fix_eq2 [OF sforall2_def], simp) |
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 |
lemma sforall2_nil [simp]: "sforall2$P$nil=TT" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
173 |
by (subst sforall2_unfold, simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
174 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
175 |
lemma sforall2_UU [simp]: "sforall2$P$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
176 |
by (subst sforall2_unfold, simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
177 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
178 |
lemma sforall2_cons [simp]: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
179 |
"x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
180 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
181 |
apply (subst sforall2_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
182 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
183 |
apply (rule refl) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
184 |
done |
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 |
subsubsection {* stakewhile *} |
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 stakewhile_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
190 |
"stakewhile = (LAM P tr. case tr of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
191 |
nil => nil |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
192 |
| x##xs => (If P$x then x##(stakewhile$P$xs) else nil fi))" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
193 |
by (subst fix_eq2 [OF stakewhile_def], simp) |
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 stakewhile_nil [simp]: "stakewhile$P$nil=nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
196 |
apply (subst stakewhile_unfold) |
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 |
lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
201 |
apply (subst stakewhile_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
202 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
203 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
204 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
205 |
lemma stakewhile_cons [simp]: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
206 |
"x~=UU ==> stakewhile$P$(x##xs) = |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
207 |
(If P$x then x##(stakewhile$P$xs) else nil fi)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
208 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
209 |
apply (subst stakewhile_unfold) |
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 |
apply (rule refl) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
212 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
213 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
214 |
subsubsection {* sdropwhile *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
215 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
216 |
lemma sdropwhile_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
217 |
"sdropwhile = (LAM P tr. case tr of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
218 |
nil => nil |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
219 |
| x##xs => (If P$x then sdropwhile$P$xs else tr fi))" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
220 |
by (subst fix_eq2 [OF sdropwhile_def], simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
221 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
222 |
lemma sdropwhile_nil [simp]: "sdropwhile$P$nil=nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
223 |
apply (subst sdropwhile_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
224 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
225 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
226 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
227 |
lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
228 |
apply (subst sdropwhile_unfold) |
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 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
231 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
232 |
lemma sdropwhile_cons [simp]: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
233 |
"x~=UU ==> sdropwhile$P$(x##xs) = |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
234 |
(If P$x then sdropwhile$P$xs else x##xs fi)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
235 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
236 |
apply (subst sdropwhile_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
237 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
238 |
apply (rule refl) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
239 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
240 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
241 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
242 |
subsubsection {* slast *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
243 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
244 |
lemma slast_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
245 |
"slast = (LAM tr. case tr of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
246 |
nil => UU |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
247 |
| x##xs => (If is_nil$xs then x else slast$xs fi))" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
248 |
by (subst fix_eq2 [OF slast_def], simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
249 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
250 |
lemma slast_nil [simp]: "slast$nil=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
251 |
apply (subst slast_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
252 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
253 |
done |
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 |
lemma slast_UU [simp]: "slast$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
256 |
apply (subst slast_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
257 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
258 |
done |
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 |
lemma slast_cons [simp]: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
261 |
"x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
262 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
263 |
apply (subst slast_unfold) |
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 (rule refl) |
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 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
269 |
subsubsection {* sconc *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
270 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
271 |
lemma sconc_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
272 |
"sconc = (LAM t1 t2. case t1 of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
273 |
nil => t2 |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
274 |
| x##xs => x ## (xs @@ t2))" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
275 |
by (subst fix_eq2 [OF sconc_def], simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
276 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
277 |
lemma sconc_nil [simp]: "nil @@ y = y" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
278 |
apply (subst sconc_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
279 |
apply simp |
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 sconc_UU [simp]: "UU @@ y=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
283 |
apply (subst sconc_unfold) |
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 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
287 |
lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
288 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
289 |
apply (subst sconc_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
290 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
291 |
apply (case_tac "x=UU") |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
292 |
apply simp_all |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
293 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
294 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
295 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
296 |
subsubsection {* sflat *} |
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 |
lemma sflat_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
299 |
"sflat = (LAM tr. case tr of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
300 |
nil => nil |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
301 |
| x##xs => x @@ sflat$xs)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
302 |
by (subst fix_eq2 [OF sflat_def], simp) |
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 |
lemma sflat_nil [simp]: "sflat$nil=nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
305 |
apply (subst sflat_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
306 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
307 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
308 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
309 |
lemma sflat_UU [simp]: "sflat$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
310 |
apply (subst sflat_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
311 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
312 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
313 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
314 |
lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
315 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
316 |
apply (subst sflat_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
317 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
318 |
apply (case_tac "x=UU") |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
319 |
apply simp_all |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
320 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
321 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
322 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
323 |
subsubsection {* szip *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
324 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
325 |
lemma szip_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
326 |
"szip = (LAM t1 t2. case t1 of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
327 |
nil => nil |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
328 |
| x##xs => (case t2 of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
329 |
nil => UU |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
330 |
| y##ys => <x,y>##(szip$xs$ys)))" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
331 |
by (subst fix_eq2 [OF szip_def], simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
332 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
333 |
lemma szip_nil [simp]: "szip$nil$y=nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
334 |
apply (subst szip_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
335 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
336 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
337 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
338 |
lemma szip_UU1 [simp]: "szip$UU$y=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
339 |
apply (subst szip_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
340 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
341 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
342 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
343 |
lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
344 |
apply (subst szip_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
345 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
346 |
apply (rule_tac x="x" in seq.casedist) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
347 |
apply simp_all |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
348 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
349 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
350 |
lemma szip_cons_nil [simp]: "x~=UU ==> szip$(x##xs)$nil=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
351 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
352 |
apply (subst szip_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
353 |
apply simp_all |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
354 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
355 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
356 |
lemma szip_cons [simp]: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
357 |
"[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
358 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
359 |
apply (subst szip_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
360 |
apply simp_all |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
361 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
362 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
363 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
364 |
subsection "scons, nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
365 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
366 |
lemma scons_inject_eq: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
367 |
"[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
368 |
by (simp add: seq.injects) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
369 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
370 |
lemma nil_less_is_nil: "nil<<x ==> nil=x" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
371 |
apply (rule_tac x="x" in seq.casedist) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
372 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
373 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
374 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
375 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
376 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
377 |
subsection "sfilter, sforall, sconc" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
378 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
379 |
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
|
380 |
= (if b then tr1 @@ tr else tr2 @@ tr)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
381 |
by simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
382 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
383 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
384 |
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
|
385 |
apply (rule_tac x="x" in seq.ind) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
386 |
(* adm *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
387 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
388 |
(* base cases *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
389 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
390 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
391 |
(* main case *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
392 |
apply (rule_tac p="P$a" in trE) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
393 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
394 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
395 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
396 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
397 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
398 |
lemma sforallPstakewhileP: "sforall P (stakewhile$P$x)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
399 |
apply (simp add: sforall_def) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
400 |
apply (rule_tac x="x" in seq.ind) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
401 |
(* adm *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
402 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
403 |
(* base cases *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
404 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
405 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
406 |
(* main case *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
407 |
apply (rule_tac p="P$a" in trE) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
408 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
409 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
410 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
411 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
412 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
413 |
lemma forallPsfilterP: "sforall P (sfilter$P$x)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
414 |
apply (simp add: sforall_def) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
415 |
apply (rule_tac x="x" in seq.ind) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
416 |
(* adm *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
417 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
418 |
(* base cases *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
419 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
420 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
421 |
(* main case *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
422 |
apply (rule_tac p="P$a" in trE) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
423 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
424 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
425 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
426 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
427 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
428 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
429 |
subsection "Finite" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
430 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
431 |
(* ---------------------------------------------------- *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
432 |
(* Proofs of rewrite rules for Finite: *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
433 |
(* 1. Finite(nil), (by definition) *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
434 |
(* 2. ~Finite(UU), *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
435 |
(* 3. a~=UU==> Finite(a##x)=Finite(x) *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
436 |
(* ---------------------------------------------------- *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
437 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
438 |
lemma Finite_UU_a: "Finite x --> x~=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
439 |
apply (rule impI) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
440 |
apply (erule sfinite.induct) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
441 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
442 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
443 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
444 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
445 |
lemma Finite_UU [simp]: "~(Finite UU)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
446 |
apply (cut_tac x="UU" in Finite_UU_a) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
447 |
apply fast |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
448 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
449 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
450 |
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
|
451 |
apply (intro strip) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
452 |
apply (erule sfinite.elims) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
453 |
apply fastsimp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
454 |
apply (simp add: seq.injects) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
455 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
456 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
457 |
lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
458 |
apply (rule iffI) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
459 |
apply (erule (1) Finite_cons_a [rule_format]) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
460 |
apply fast |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
461 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
462 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
463 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
464 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
465 |
subsection "induction" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
466 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
467 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
468 |
(*-------------------------------- *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
469 |
(* Extensions to Induction Theorems *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
470 |
(*-------------------------------- *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
471 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
472 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
473 |
lemma seq_finite_ind_lemma: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
474 |
assumes "(!!n. P(seq_take n$s))" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
475 |
shows "seq_finite(s) -->P(s)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
476 |
apply (unfold seq.finite_def) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
477 |
apply (intro strip) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
478 |
apply (erule exE) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
479 |
apply (erule subst) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
480 |
apply (rule prems) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
481 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
482 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
483 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
484 |
lemma seq_finite_ind: "!!P.[|P(UU);P(nil); |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
485 |
!! x s1.[|x~=UU;P(s1)|] ==> P(x##s1) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
486 |
|] ==> seq_finite(s) --> P(s)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
487 |
apply (rule seq_finite_ind_lemma) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
488 |
apply (erule seq.finite_ind) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
489 |
apply assumption |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
490 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
491 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
492 |
|
3071 | 493 |
end |