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