author | wenzelm |
Thu, 22 Nov 2007 14:51:34 +0100 | |
changeset 25456 | 6f79698f294d |
parent 23778 | 18f426a137a9 |
child 25803 | 230c9c87d739 |
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 |
|
23778 | 37 |
inductive |
38 |
Finite :: "'a seq => bool" |
|
39 |
where |
|
40 |
sfinite_0: "Finite nil" |
|
41 |
| sfinite_n: "[| Finite tr; a~=UU |] ==> Finite (a##tr)" |
|
3071 | 42 |
|
17233 | 43 |
defs |
3071 | 44 |
|
45 |
(* f not possible at lhs, as "pattern matching" only for % x arguments, |
|
46 |
f cannot be written at rhs in front, as fix_eq3 does not apply later *) |
|
17233 | 47 |
smap_def: |
48 |
"smap == (fix$(LAM h f tr. case tr of |
|
3071 | 49 |
nil => nil |
10835 | 50 |
| x##xs => f$x ## h$f$xs))" |
3071 | 51 |
|
17233 | 52 |
sfilter_def: |
53 |
"sfilter == (fix$(LAM h P t. case t of |
|
54 |
nil => nil |
|
55 |
| x##xs => If P$x |
|
10835 | 56 |
then x##(h$P$xs) |
57 |
else h$P$xs |
|
17233 | 58 |
fi))" |
59 |
sforall_def: |
|
60 |
"sforall P t == (sforall2$P$t ~=FF)" |
|
3071 | 61 |
|
62 |
||
17233 | 63 |
sforall2_def: |
64 |
"sforall2 == (fix$(LAM h P t. case t of |
|
65 |
nil => TT |
|
66 |
| x##xs => P$x andalso h$P$xs))" |
|
67 |
||
68 |
sconc_def: |
|
69 |
"sconc == (fix$(LAM h t1 t2. case t1 of |
|
3071 | 70 |
nil => t2 |
10835 | 71 |
| x##xs => x##(h$xs$t2)))" |
3071 | 72 |
|
17233 | 73 |
slast_def: |
74 |
"slast == (fix$(LAM h t. case t of |
|
75 |
nil => UU |
|
76 |
| x##xs => (If is_nil$xs |
|
3071 | 77 |
then x |
10835 | 78 |
else h$xs fi)))" |
3071 | 79 |
|
17233 | 80 |
stakewhile_def: |
81 |
"stakewhile == (fix$(LAM h P t. case t of |
|
82 |
nil => nil |
|
83 |
| x##xs => If P$x |
|
10835 | 84 |
then x##(h$P$xs) |
3071 | 85 |
else nil |
17233 | 86 |
fi))" |
87 |
sdropwhile_def: |
|
88 |
"sdropwhile == (fix$(LAM h P t. case t of |
|
89 |
nil => nil |
|
90 |
| x##xs => If P$x |
|
10835 | 91 |
then h$P$xs |
3071 | 92 |
else t |
17233 | 93 |
fi))" |
94 |
sflat_def: |
|
95 |
"sflat == (fix$(LAM h t. case t of |
|
96 |
nil => nil |
|
97 |
| x##xs => x @@ (h$xs)))" |
|
3071 | 98 |
|
17233 | 99 |
szip_def: |
100 |
"szip == (fix$(LAM h t1 t2. case t1 of |
|
3071 | 101 |
nil => nil |
17233 | 102 |
| x##xs => (case t2 of |
103 |
nil => UU |
|
10835 | 104 |
| y##ys => <x,y>##(h$xs$ys))))" |
3071 | 105 |
|
17233 | 106 |
Partial_def: |
3071 | 107 |
"Partial x == (seq_finite x) & ~(Finite x)" |
108 |
||
17233 | 109 |
Infinite_def: |
3071 | 110 |
"Infinite x == ~(seq_finite x)" |
111 |
||
112 |
||
23778 | 113 |
declare Finite.intros [simp] |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
114 |
declare seq.rews [simp] |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
115 |
|
19804 | 116 |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
117 |
subsection {* recursive equations of operators *} |
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 {* smap *} |
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 |
lemma smap_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
122 |
"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
|
123 |
by (subst fix_eq2 [OF smap_def], simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
124 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
125 |
lemma smap_nil [simp]: "smap$f$nil=nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
126 |
by (subst smap_unfold, 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_UU [simp]: "smap$f$UU=UU" |
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_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
|
132 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
133 |
apply (subst smap_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
134 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
135 |
apply (rule refl) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
136 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
137 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
138 |
subsubsection {* sfilter *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
139 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
140 |
lemma sfilter_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
141 |
"sfilter = (LAM P tr. case tr of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
142 |
nil => nil |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
143 |
| 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
|
144 |
by (subst fix_eq2 [OF sfilter_def], simp) |
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 sfilter_nil [simp]: "sfilter$P$nil=nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
147 |
by (subst sfilter_unfold, 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_UU [simp]: "sfilter$P$UU=UU" |
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_cons [simp]: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
153 |
"x~=UU ==> sfilter$P$(x##xs)= |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
154 |
(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
|
155 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
156 |
apply (subst sfilter_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
157 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
158 |
apply (rule refl) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
159 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
160 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
161 |
subsubsection {* sforall2 *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
162 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
163 |
lemma sforall2_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
164 |
"sforall2 = (LAM P tr. case tr of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
165 |
nil => TT |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
166 |
| x##xs => (P$x andalso sforall2$P$xs))" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
167 |
by (subst fix_eq2 [OF sforall2_def], simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
168 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
169 |
lemma sforall2_nil [simp]: "sforall2$P$nil=TT" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
170 |
by (subst sforall2_unfold, 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_UU [simp]: "sforall2$P$UU=UU" |
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_cons [simp]: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
176 |
"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
|
177 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
178 |
apply (subst sforall2_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
179 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
180 |
apply (rule refl) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
181 |
done |
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 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
184 |
subsubsection {* stakewhile *} |
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 |
lemma stakewhile_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
187 |
"stakewhile = (LAM P tr. case tr of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
188 |
nil => nil |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
189 |
| 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
|
190 |
by (subst fix_eq2 [OF stakewhile_def], simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
191 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
192 |
lemma stakewhile_nil [simp]: "stakewhile$P$nil=nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
193 |
apply (subst stakewhile_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
194 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
195 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
196 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
197 |
lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
198 |
apply (subst stakewhile_unfold) |
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 |
lemma stakewhile_cons [simp]: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
203 |
"x~=UU ==> stakewhile$P$(x##xs) = |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
204 |
(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
|
205 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
206 |
apply (subst stakewhile_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
207 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
208 |
apply (rule refl) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
209 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
210 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
211 |
subsubsection {* sdropwhile *} |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
212 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
213 |
lemma sdropwhile_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
214 |
"sdropwhile = (LAM P tr. case tr of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
215 |
nil => nil |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
216 |
| 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
|
217 |
by (subst fix_eq2 [OF sdropwhile_def], simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
218 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
219 |
lemma sdropwhile_nil [simp]: "sdropwhile$P$nil=nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
220 |
apply (subst sdropwhile_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
221 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
222 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
223 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
224 |
lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
225 |
apply (subst sdropwhile_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
226 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
227 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
228 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
229 |
lemma sdropwhile_cons [simp]: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
230 |
"x~=UU ==> sdropwhile$P$(x##xs) = |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
231 |
(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
|
232 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
233 |
apply (subst sdropwhile_unfold) |
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 (rule refl) |
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 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
239 |
subsubsection {* slast *} |
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 |
lemma slast_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
242 |
"slast = (LAM tr. case tr of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
243 |
nil => UU |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
244 |
| 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
|
245 |
by (subst fix_eq2 [OF slast_def], simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
246 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
247 |
lemma slast_nil [simp]: "slast$nil=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
248 |
apply (subst slast_unfold) |
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 |
done |
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 |
lemma slast_UU [simp]: "slast$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
253 |
apply (subst slast_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
254 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
255 |
done |
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 |
lemma slast_cons [simp]: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
258 |
"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
|
259 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
260 |
apply (subst slast_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
261 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
262 |
apply (rule refl) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
263 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
264 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
265 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
266 |
subsubsection {* sconc *} |
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 sconc_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
269 |
"sconc = (LAM t1 t2. case t1 of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
270 |
nil => t2 |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
271 |
| x##xs => x ## (xs @@ t2))" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
272 |
by (subst fix_eq2 [OF sconc_def], simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
273 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
274 |
lemma sconc_nil [simp]: "nil @@ y = y" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
275 |
apply (subst sconc_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
276 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
277 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
278 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
279 |
lemma sconc_UU [simp]: "UU @@ y=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
280 |
apply (subst sconc_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
281 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
282 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
283 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
284 |
lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
285 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
286 |
apply (subst sconc_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
287 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
288 |
apply (case_tac "x=UU") |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
289 |
apply simp_all |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
290 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
291 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
292 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
293 |
subsubsection {* sflat *} |
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 |
lemma sflat_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
296 |
"sflat = (LAM tr. case tr of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
297 |
nil => nil |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
298 |
| x##xs => x @@ sflat$xs)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
299 |
by (subst fix_eq2 [OF sflat_def], simp) |
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 |
lemma sflat_nil [simp]: "sflat$nil=nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
302 |
apply (subst sflat_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
303 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
304 |
done |
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 sflat_UU [simp]: "sflat$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
307 |
apply (subst sflat_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
308 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
309 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
310 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
311 |
lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
312 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
313 |
apply (subst sflat_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
314 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
315 |
apply (case_tac "x=UU") |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
316 |
apply simp_all |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
317 |
done |
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 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
320 |
subsubsection {* szip *} |
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 |
lemma szip_unfold: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
323 |
"szip = (LAM t1 t2. case t1 of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
324 |
nil => nil |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
325 |
| x##xs => (case t2 of |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
326 |
nil => UU |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
327 |
| y##ys => <x,y>##(szip$xs$ys)))" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
328 |
by (subst fix_eq2 [OF szip_def], simp) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
329 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
330 |
lemma szip_nil [simp]: "szip$nil$y=nil" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
331 |
apply (subst szip_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
332 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
333 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
334 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
335 |
lemma szip_UU1 [simp]: "szip$UU$y=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
336 |
apply (subst szip_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
337 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
338 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
339 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
340 |
lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
341 |
apply (subst szip_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
342 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
343 |
apply (rule_tac x="x" in seq.casedist) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
344 |
apply simp_all |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
345 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
346 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
347 |
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
|
348 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
349 |
apply (subst szip_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
350 |
apply simp_all |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
351 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
352 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
353 |
lemma szip_cons [simp]: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
354 |
"[| 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
|
355 |
apply (rule trans) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
356 |
apply (subst szip_unfold) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
357 |
apply simp_all |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
358 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
359 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
360 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
361 |
subsection "scons, nil" |
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 |
lemma scons_inject_eq: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
364 |
"[|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
|
365 |
by (simp add: seq.injects) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
366 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
367 |
lemma nil_less_is_nil: "nil<<x ==> nil=x" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
368 |
apply (rule_tac x="x" in seq.casedist) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
369 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
370 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
371 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
372 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
373 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
374 |
subsection "sfilter, sforall, sconc" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
375 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
376 |
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
|
377 |
= (if b then tr1 @@ tr else tr2 @@ tr)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
378 |
by simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
379 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
380 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
381 |
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
|
382 |
apply (rule_tac x="x" in seq.ind) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
383 |
(* adm *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
384 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
385 |
(* base cases *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
386 |
apply simp |
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 |
(* main case *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
389 |
apply (rule_tac p="P$a" in trE) |
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 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
392 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
393 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
394 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
395 |
lemma sforallPstakewhileP: "sforall P (stakewhile$P$x)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
396 |
apply (simp add: sforall_def) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
397 |
apply (rule_tac x="x" in seq.ind) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
398 |
(* adm *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
399 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
400 |
(* base cases *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
401 |
apply simp |
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 |
(* main case *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
404 |
apply (rule_tac p="P$a" in trE) |
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 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
407 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
408 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
409 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
410 |
lemma forallPsfilterP: "sforall P (sfilter$P$x)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
411 |
apply (simp add: sforall_def) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
412 |
apply (rule_tac x="x" in seq.ind) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
413 |
(* adm *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
414 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
415 |
(* base cases *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
416 |
apply simp |
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 |
(* main case *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
419 |
apply (rule_tac p="P$a" in trE) |
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 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
422 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
423 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
424 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
425 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
426 |
subsection "Finite" |
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 |
(* Proofs of rewrite rules for Finite: *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
430 |
(* 1. Finite(nil), (by definition) *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
431 |
(* 2. ~Finite(UU), *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
432 |
(* 3. a~=UU==> Finite(a##x)=Finite(x) *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
433 |
(* ---------------------------------------------------- *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
434 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
435 |
lemma Finite_UU_a: "Finite x --> x~=UU" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
436 |
apply (rule impI) |
23778 | 437 |
apply (erule Finite.induct) |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
438 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
439 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
440 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
441 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
442 |
lemma Finite_UU [simp]: "~(Finite UU)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
443 |
apply (cut_tac x="UU" in Finite_UU_a) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
444 |
apply fast |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
445 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
446 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
447 |
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
|
448 |
apply (intro strip) |
23778 | 449 |
apply (erule Finite.cases) |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
450 |
apply fastsimp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
451 |
apply (simp add: seq.injects) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
452 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
453 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
454 |
lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
455 |
apply (rule iffI) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
456 |
apply (erule (1) Finite_cons_a [rule_format]) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
457 |
apply fast |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
458 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
459 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
460 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
461 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
462 |
subsection "induction" |
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 |
(*-------------------------------- *) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
466 |
(* Extensions to Induction Theorems *) |
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 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
470 |
lemma seq_finite_ind_lemma: |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
471 |
assumes "(!!n. P(seq_take n$s))" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
472 |
shows "seq_finite(s) -->P(s)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
473 |
apply (unfold seq.finite_def) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
474 |
apply (intro strip) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
475 |
apply (erule exE) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
476 |
apply (erule subst) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
477 |
apply (rule prems) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
478 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
479 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
480 |
|
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
481 |
lemma seq_finite_ind: "!!P.[|P(UU);P(nil); |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
482 |
!! x s1.[|x~=UU;P(s1)|] ==> P(x##s1) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
483 |
|] ==> seq_finite(s) --> P(s)" |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
484 |
apply (rule seq_finite_ind_lemma) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
485 |
apply (erule seq.finite_ind) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
486 |
apply assumption |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
487 |
apply simp |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
488 |
done |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
17233
diff
changeset
|
489 |
|
3071 | 490 |
end |