author | wenzelm |
Wed, 12 Dec 2001 20:37:31 +0100 | |
changeset 12484 | 7ad150f5fc10 |
parent 12036 | 49f6c49454c2 |
child 13454 | 01e2496dee05 |
permissions | -rw-r--r-- |
9169 | 1 |
(* Title: HOLCF/ex//Stream.ML |
2 |
ID: $Id$ |
|
12036 | 3 |
Author: Franz Regensburger and David von Oheimb, TU Muenchen |
11348 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
2570 | 5 |
|
12036 | 6 |
General Stream domain. |
2570 | 7 |
*) |
8 |
||
4044 | 9 |
fun stream_case_tac s i = res_inst_tac [("x",s)] stream.casedist i |
2570 | 10 |
THEN hyp_subst_tac i THEN hyp_subst_tac (i+1); |
11 |
||
12 |
||
9169 | 13 |
val [stream_con_rew1,stream_con_rew2] = stream.con_rews; |
14 |
||
11348 | 15 |
Addsimps stream.rews; |
16 |
Addsimps[eq_UU_iff RS sym]; |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
17 |
|
2570 | 18 |
(* ----------------------------------------------------------------------- *) |
19 |
(* theorems about scons *) |
|
20 |
(* ----------------------------------------------------------------------- *) |
|
21 |
||
22 |
section "scons"; |
|
23 |
||
11655 | 24 |
Goal "(a && s = UU) = (a = UU)"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
25 |
by Safe_tac; |
10230 | 26 |
by (etac contrapos_pp 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
27 |
by (safe_tac (claset() addSIs stream.con_rews)); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
28 |
qed "scons_eq_UU"; |
2570 | 29 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
30 |
Goal "[| a && x = UU; a ~= UU |] ==> R"; |
12484 | 31 |
by (dtac stream_con_rew2 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
32 |
by (contr_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
33 |
qed "scons_not_empty"; |
2570 | 34 |
|
11655 | 35 |
Goal "(x ~= UU) = (EX a y. a ~= UU & x = a && y)"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
36 |
by (cut_facts_tac [stream.exhaust] 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
37 |
by (best_tac (claset() addDs [stream_con_rew2]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
38 |
qed "stream_exhaust_eq"; |
2570 | 39 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
40 |
Goal |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
41 |
"[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
42 |
by (stream_case_tac "t" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
43 |
by (fast_tac (claset() addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
44 |
by (fast_tac (claset() addDs stream.inverts) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
45 |
qed "stream_prefix"; |
2570 | 46 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
47 |
Goal "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
48 |
by (cut_inst_tac [("x1","x::'a::flat"), ("x","y::'a::flat")] |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
49 |
(ax_flat RS spec RS spec) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
50 |
by (forward_tac stream.inverts 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
51 |
by Safe_tac; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
52 |
by (dtac (hd stream.con_rews RS subst) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
53 |
by (fast_tac (claset() addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
54 |
qed "stream_flat_prefix"; |
2570 | 55 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
56 |
Goal "b ~= UU ==> x << b && z = \ |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
57 |
\ (x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
58 |
by Safe_tac; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
59 |
by (stream_case_tac "x" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
60 |
by (safe_tac (claset() addSDs stream.inverts |
11348 | 61 |
addSIs [monofun_cfun, monofun_cfun_arg])); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
62 |
by (Fast_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
63 |
qed "stream_prefix'"; |
2570 | 64 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
65 |
Goal "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b & s = t)"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
66 |
by (best_tac (claset() addSEs stream.injects) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
67 |
qed "stream_inject_eq"; |
11348 | 68 |
Addsimps [stream_inject_eq]; |
2570 | 69 |
|
70 |
||
71 |
(* ----------------------------------------------------------------------- *) |
|
72 |
(* theorems about stream_when *) |
|
73 |
(* ----------------------------------------------------------------------- *) |
|
74 |
||
75 |
section "stream_when"; |
|
76 |
||
10835 | 77 |
Goal "stream_when$UU$s=UU"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
78 |
by (stream_case_tac "s" 1); |
11348 | 79 |
by (ALLGOALS Asm_simp_tac); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
80 |
qed "stream_when_strictf"; |
2570 | 81 |
|
82 |
||
83 |
(* ----------------------------------------------------------------------- *) |
|
84 |
(* theorems about ft and rt *) |
|
85 |
(* ----------------------------------------------------------------------- *) |
|
86 |
||
87 |
section "ft & rt"; |
|
88 |
||
89 |
(* |
|
10835 | 90 |
Goal "ft$s=UU --> s=UU"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
91 |
by (stream_case_tac "s" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
92 |
by (REPEAT (asm_simp_tac (simpset() addsimps stream.rews) 1)); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
93 |
qed "stream_ft_lemma1"; |
2570 | 94 |
*) |
95 |
||
10835 | 96 |
Goal "s~=UU ==> ft$s~=UU"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
97 |
by (stream_case_tac "s" 1); |
11348 | 98 |
by (Blast_tac 1); |
99 |
by (Asm_simp_tac 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
100 |
qed "ft_defin"; |
2570 | 101 |
|
10835 | 102 |
Goal "rt$s~=UU ==> s~=UU"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
103 |
by Auto_tac; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
104 |
qed "rt_strict_rev"; |
2570 | 105 |
|
10835 | 106 |
Goal "(ft$s)&&(rt$s)=s"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
107 |
by (stream_case_tac "s" 1); |
11348 | 108 |
by (ALLGOALS Asm_simp_tac); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
109 |
qed "surjectiv_scons"; |
2570 | 110 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
111 |
Goal "ALL x s. x << s --> iterate i rt x << iterate i rt s"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
112 |
by (induct_tac "i" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
113 |
by (Simp_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
114 |
by (strip_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
115 |
by (stream_case_tac "x" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
116 |
by (rtac (minimal RS (monofun_iterate2 RS monofunE RS spec RS spec RS mp))1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
117 |
by (dtac stream_prefix 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
118 |
by Safe_tac; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
119 |
by (asm_simp_tac (HOL_ss addsimps iterate_Suc2::stream.rews) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
120 |
qed_spec_mp "monofun_rt_mult"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
121 |
|
2570 | 122 |
|
123 |
||
124 |
(* ----------------------------------------------------------------------- *) |
|
125 |
(* theorems about stream_take *) |
|
126 |
(* ----------------------------------------------------------------------- *) |
|
127 |
||
128 |
section "stream_take"; |
|
129 |
||
10835 | 130 |
Goal "(LUB i. stream_take i$s) = s"; |
131 |
by (subgoal_tac "(LUB i. stream_take i$s) = fix$stream_copy$s" 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
132 |
by (simp_tac (simpset() addsimps [fix_def2, stream.take_def, |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
133 |
contlub_cfun_fun, chain_iterate]) 2); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
134 |
by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
135 |
qed "stream_reach2"; |
2570 | 136 |
|
10835 | 137 |
Goal "chain (%i. stream_take i$s)"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
138 |
by (rtac chainI 1); |
11348 | 139 |
by (subgoal_tac "ALL i s::'a stream. stream_take i$s << stream_take (Suc i)$s" 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
140 |
by (Fast_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
141 |
by (rtac allI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
142 |
by (induct_tac "ia" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
143 |
by (Simp_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
144 |
by (rtac allI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
145 |
by (stream_case_tac "s" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
146 |
by (Simp_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
147 |
by (asm_simp_tac (simpset() addsimps [monofun_cfun_arg]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
148 |
qed "chain_stream_take"; |
2570 | 149 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
150 |
|
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
151 |
Goalw [stream.take_def] |
10835 | 152 |
"stream_take n$x = x ==> stream_take (Suc n)$x = x"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
153 |
by (rtac antisym_less 1); |
10835 | 154 |
by (subgoal_tac "iterate (Suc n) stream_copy UU$x << fix$stream_copy$x" 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
155 |
by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
156 |
by (rtac monofun_cfun_fun 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
157 |
by (stac fix_def2 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
158 |
by (rtac is_ub_thelub 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
159 |
by (rtac chain_iterate 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
160 |
by (etac subst 1 THEN rtac monofun_cfun_fun 1); |
11348 | 161 |
by (rtac (rewrite_rule [chain_def] chain_iterate RS spec) 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
162 |
qed "stream_take_more"; |
2570 | 163 |
|
164 |
(* |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
165 |
Goal |
10835 | 166 |
"ALL s2. stream_take n$s2 = s2 --> stream_take (Suc n)$s2=s2"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
167 |
by (induct_tac "n" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
168 |
by (simp_tac (simpset() addsimps stream_rews) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
169 |
by (strip_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
170 |
by (hyp_subst_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
171 |
by (simp_tac (simpset() addsimps stream_rews) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
172 |
by (rtac allI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
173 |
by (res_inst_tac [("s","s2")] streamE 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
174 |
by (asm_simp_tac (simpset() addsimps stream_rews) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
175 |
by (asm_simp_tac (simpset() addsimps stream_rews) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
176 |
by (strip_tac 1 ); |
10835 | 177 |
by (subgoal_tac "stream_take n1$xs = xs" 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
178 |
by (rtac ((hd stream_inject) RS conjunct2) 2); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
179 |
by (atac 4); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
180 |
by (atac 2); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
181 |
by (atac 2); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
182 |
by (rtac cfun_arg_cong 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
183 |
by (Blast_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
184 |
qed "stream_take_lemma2"; |
2570 | 185 |
*) |
186 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
187 |
Goal |
11348 | 188 |
"ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
189 |
by (induct_tac "n" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
190 |
by (Asm_simp_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
191 |
by (strip_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
192 |
by (res_inst_tac [("P","x && xs=UU")] notE 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
193 |
by (eresolve_tac stream.con_rews 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
194 |
by (etac sym 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
195 |
by (strip_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
196 |
by (rtac stream_take_more 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
197 |
by (res_inst_tac [("a1","x")] ((hd stream.injects) RS conjunct2) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
198 |
by (assume_tac 3); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
199 |
by (etac (hd(tl(tl(stream.take_rews))) RS subst) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
200 |
by (atac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
201 |
qed_spec_mp "stream_take_lemma3"; |
2570 | 202 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
203 |
Goal |
10835 | 204 |
"ALL x xs. stream_take n$xs=xs --> stream_take (Suc n)$(x && xs) = x && xs"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
205 |
by (induct_tac "n" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
206 |
by Auto_tac; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
207 |
qed_spec_mp "stream_take_lemma4"; |
2570 | 208 |
|
209 |
||
210 |
(* ------------------------------------------------------------------------- *) |
|
211 |
(* special induction rules *) |
|
212 |
(* ------------------------------------------------------------------------- *) |
|
213 |
||
214 |
section "induction"; |
|
215 |
||
216 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
217 |
val prems = Goalw [stream.finite_def] |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
218 |
"[| stream_finite x; \ |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
219 |
\ P UU; \ |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
220 |
\ !!a s. [| a ~= UU; P s |] \ |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
221 |
\ ==> P (a && s) |] ==> P x"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
222 |
by (cut_facts_tac prems 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
223 |
by (etac exE 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
224 |
by (etac subst 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
225 |
by (rtac stream.finite_ind 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
226 |
by (atac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
227 |
by (eresolve_tac prems 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
228 |
by (atac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
229 |
qed "stream_finite_ind"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
230 |
|
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
231 |
val major::prems = Goal |
2570 | 232 |
"[| P UU;\ |
233 |
\ !! x . x ~= UU ==> P (x && UU); \ |
|
234 |
\ !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s ) \ |
|
10835 | 235 |
\ |] ==> !s. P (stream_take n$s)"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
236 |
by (res_inst_tac [("n","n")] nat_induct2 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
237 |
by (asm_simp_tac (simpset() addsimps [major]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
238 |
by (rtac allI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
239 |
by (stream_case_tac "s" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
240 |
by (asm_simp_tac (simpset() addsimps [major]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
241 |
by (asm_simp_tac (simpset() addsimps prems) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
242 |
by (rtac allI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
243 |
by (stream_case_tac "s" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
244 |
by (asm_simp_tac (simpset() addsimps [major]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
245 |
by (res_inst_tac [("x","sa")] stream.casedist 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
246 |
by (asm_simp_tac (simpset() addsimps prems) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
247 |
by (asm_simp_tac (simpset() addsimps prems) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
248 |
qed "stream_finite_ind2"; |
2570 | 249 |
|
250 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
251 |
val prems = Goal |
2570 | 252 |
"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); \ |
253 |
\ !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s)\ |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
254 |
\ |] ==> P x"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
255 |
by (rtac (stream.reach RS subst) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
256 |
by (rtac (adm_impl_admw RS wfix_ind) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
257 |
by (rtac adm_subst 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
258 |
by (cont_tacR 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
259 |
by (resolve_tac prems 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
260 |
by (rtac allI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
261 |
by (rtac (rewrite_rule [stream.take_def] stream_finite_ind2 RS spec) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
262 |
by (resolve_tac prems 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
263 |
by (eresolve_tac prems 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
264 |
by (eresolve_tac prems 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
265 |
by (atac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
266 |
by (atac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
267 |
qed "stream_ind2"; |
2570 | 268 |
|
269 |
||
270 |
(* ----------------------------------------------------------------------- *) |
|
271 |
(* simplify use of coinduction *) |
|
272 |
(* ----------------------------------------------------------------------- *) |
|
273 |
||
274 |
section "coinduction"; |
|
275 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
276 |
|
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
277 |
Goalw [stream.bisim_def] |
10835 | 278 |
"!s1 s2. R s1 s2 --> ft$s1 = ft$s2 & R (rt$s1) (rt$s2) ==> stream_bisim R"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
279 |
by (strip_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
280 |
by (etac allE 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
281 |
by (etac allE 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
282 |
by (dtac mp 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
283 |
by (atac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
284 |
by (etac conjE 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
285 |
by (case_tac "x = UU & x' = UU" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
286 |
by (rtac disjI1 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
287 |
by (Blast_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
288 |
by (rtac disjI2 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
289 |
by (rtac disjE 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
290 |
by (etac (de_Morgan_conj RS subst) 1); |
10835 | 291 |
by (res_inst_tac [("x","ft$x")] exI 1); |
292 |
by (res_inst_tac [("x","rt$x")] exI 1); |
|
293 |
by (res_inst_tac [("x","rt$x'")] exI 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
294 |
by (rtac conjI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
295 |
by (etac ft_defin 1); |
11348 | 296 |
by (asm_simp_tac (simpset() addsimps [surjectiv_scons]) 1); |
10835 | 297 |
by (eres_inst_tac [("s","ft$x"),("t","ft$x'")] subst 1); |
11348 | 298 |
by (simp_tac (simpset() addsimps [surjectiv_scons]) 1); |
10835 | 299 |
by (res_inst_tac [("x","ft$x'")] exI 1); |
300 |
by (res_inst_tac [("x","rt$x")] exI 1); |
|
301 |
by (res_inst_tac [("x","rt$x'")] exI 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
302 |
by (rtac conjI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
303 |
by (etac ft_defin 1); |
11348 | 304 |
by (asm_simp_tac (simpset() addsimps [surjectiv_scons]) 1); |
10835 | 305 |
by (res_inst_tac [("s","ft$x"),("t","ft$x'")] ssubst 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
306 |
by (etac sym 1); |
11348 | 307 |
by (simp_tac (simpset() addsimps [surjectiv_scons]) 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
308 |
qed "stream_coind_lemma2"; |
2570 | 309 |
|
310 |
(* ----------------------------------------------------------------------- *) |
|
311 |
(* theorems about stream_finite *) |
|
312 |
(* ----------------------------------------------------------------------- *) |
|
313 |
||
314 |
section "stream_finite"; |
|
315 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
316 |
|
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
317 |
Goalw [stream.finite_def] "stream_finite UU"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
318 |
by (rtac exI 1); |
11348 | 319 |
by (Simp_tac 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
320 |
qed "stream_finite_UU"; |
2570 | 321 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
322 |
Goal "~ stream_finite s ==> s ~= UU"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
323 |
by (blast_tac (claset() addIs [stream_finite_UU]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
324 |
qed "stream_finite_UU_rev"; |
2570 | 325 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
326 |
Goalw [stream.finite_def] "stream_finite xs ==> stream_finite (x && xs)"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
327 |
by (blast_tac (claset() addIs [stream_take_lemma4]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
328 |
qed "stream_finite_lemma1"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
329 |
|
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
330 |
Goalw [stream.finite_def] |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
331 |
"[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
332 |
by (blast_tac (claset() addIs [stream_take_lemma3]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
333 |
qed "stream_finite_lemma2"; |
2570 | 334 |
|
10835 | 335 |
Goal "stream_finite (rt$s) = stream_finite s"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
336 |
by (stream_case_tac "s" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
337 |
by (simp_tac (simpset() addsimps [stream_finite_UU]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
338 |
by (Asm_simp_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
339 |
by (fast_tac (claset() addIs [stream_finite_lemma1] |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
340 |
addDs [stream_finite_lemma2]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
341 |
qed "stream_finite_rt_eq"; |
2570 | 342 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
343 |
Goal "stream_finite s ==> !t. t<<s --> stream_finite t"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
344 |
by (eres_inst_tac [("x","s")] stream_finite_ind 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
345 |
by (strip_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
346 |
by (dtac UU_I 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
347 |
by (asm_simp_tac (simpset() addsimps [stream_finite_UU]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
348 |
by (strip_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
349 |
by (asm_full_simp_tac (simpset() addsimps [stream_prefix']) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
350 |
by (fast_tac (claset() addSIs [stream_finite_UU, stream_finite_lemma1]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
351 |
qed_spec_mp "stream_finite_less"; |
2570 | 352 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
353 |
Goal "adm (%x. ~ stream_finite x)"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
354 |
by (rtac admI2 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
355 |
by (best_tac (claset() addIs [stream_finite_less, is_ub_thelub]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
356 |
qed "adm_not_stream_finite"; |
11348 | 357 |
|
358 |
section "smap"; |
|
359 |
||
360 |
bind_thm ("smap_unfold", fix_prover2 thy smap_def |
|
361 |
"smap = (\\<Lambda>f s. case s of x && l => f\\<cdot>x && smap\\<cdot>f\\<cdot>l)"); |
|
362 |
||
363 |
Goal "smap\\<cdot>f\\<cdot>\\<bottom> = \\<bottom>"; |
|
364 |
by (stac smap_unfold 1); |
|
365 |
by (Simp_tac 1); |
|
366 |
qed "smap_empty"; |
|
367 |
||
368 |
Goal "x~=\\<bottom> ==> smap\\<cdot>f\\<cdot>(x&&xs) = (f\\<cdot>x)&&(smap\\<cdot>f\\<cdot>xs)"; |
|
369 |
by (rtac trans 1); |
|
370 |
by (stac smap_unfold 1); |
|
371 |
by (Asm_simp_tac 1); |
|
372 |
by (rtac refl 1); |
|
373 |
qed "smap_scons"; |
|
374 |
||
375 |
Addsimps [smap_empty, smap_scons]; |
|
376 |
||
377 |
(* ------------------------------------------------------------------------- *) |
|
378 |
||
379 |
section "slen"; |
|
380 |
||
381 |
Goalw [slen_def, stream.finite_def] "#\\<bottom> = 0"; |
|
382 |
by (Simp_tac 1); |
|
383 |
by (stac Least_equality 1); |
|
384 |
by Auto_tac; |
|
11355 | 385 |
by (simp_tac(simpset() addsimps [thm "Fin_0"]) 1); |
11348 | 386 |
qed "slen_empty"; |
387 |
||
388 |
Goalw [slen_def] "x ~= \\<bottom> ==> #(x&&xs) = iSuc (#xs)"; |
|
389 |
by (res_inst_tac [("Q1","stream_finite (x && xs)")] (split_if RS iffD2) 1); |
|
390 |
by Safe_tac; |
|
391 |
by (rtac (split_if RS iffD2) 2); |
|
392 |
by Safe_tac; |
|
393 |
by (fast_tac (claset() addIs [stream_finite_lemma1]) 2); |
|
11355 | 394 |
by (rtac (thm "iSuc_Infty" RS sym) 2); |
11348 | 395 |
by (rtac (split_if RS iffD2) 1); |
396 |
by (Simp_tac 1); |
|
397 |
by Safe_tac; |
|
398 |
by (eatac stream_finite_lemma2 1 2); |
|
399 |
by (rewtac stream.finite_def); |
|
400 |
by (Clarify_tac 1); |
|
401 |
by (eatac Least_Suc2 1 1); |
|
402 |
by (rtac not_sym 1); |
|
403 |
by Auto_tac; |
|
404 |
qed "slen_scons"; |
|
405 |
||
406 |
Addsimps [slen_empty, slen_scons]; |
|
407 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11655
diff
changeset
|
408 |
Goal "(#x < Fin (Suc 0)) = (x = UU)"; |
11348 | 409 |
by (stream_case_tac "x" 1); |
11355 | 410 |
by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps |
411 |
[thm "Fin_0", thm "iSuc_Fin" RS sym, thm "i0_iless_iSuc", thm "iSuc_mono"])); |
|
11348 | 412 |
qed "slen_less_1_eq"; |
413 |
||
414 |
Goal "(#x = 0) = (x = \\<bottom>)"; |
|
415 |
by Auto_tac; |
|
416 |
by (stream_case_tac "x" 1); |
|
417 |
by (rotate_tac ~1 2); |
|
418 |
by Auto_tac; |
|
419 |
qed "slen_empty_eq"; |
|
420 |
||
11655 | 421 |
Goal "(Fin (Suc n) < #x) = (? a y. x = a && y & a ~= \\<bottom> & Fin n < #y)"; |
11348 | 422 |
by (stream_case_tac "x" 1); |
11355 | 423 |
by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps |
424 |
[thm "iSuc_Fin" RS sym, thm "iSuc_mono"])); |
|
11348 | 425 |
by (dtac sym 1); |
426 |
by (rotate_tac 2 2); |
|
427 |
by Auto_tac; |
|
428 |
qed "slen_scons_eq"; |
|
429 |
||
430 |
||
431 |
Goal "#x = iSuc n --> (? a y. x = a&&y & a ~= \\<bottom> & #y = n)"; |
|
432 |
by (stream_case_tac "x" 1); |
|
433 |
by Auto_tac; |
|
434 |
qed_spec_mp "slen_iSuc"; |
|
435 |
||
436 |
||
437 |
Goal |
|
11655 | 438 |
"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \\<bottom> | #y < Fin (Suc n))"; |
11355 | 439 |
by (stac (thm "iSuc_Fin" RS sym) 1); |
440 |
by (stac (thm "iSuc_Fin" RS sym) 1); |
|
11348 | 441 |
by (safe_tac HOL_cs); |
442 |
by (rotate_tac ~1 1); |
|
11355 | 443 |
by (asm_full_simp_tac (HOL_ss addsimps [slen_scons, thm "iSuc_mono"]) 1); |
11348 | 444 |
by (Asm_full_simp_tac 1); |
445 |
by (stream_case_tac "x" 1); |
|
11355 | 446 |
by ( simp_tac (HOL_ss addsimps [slen_empty, thm "i0_iless_iSuc"]) 1); |
447 |
by (asm_simp_tac (HOL_ss addsimps [slen_scons, thm "iSuc_mono"]) 1); |
|
11348 | 448 |
by (etac allE 1); |
449 |
by (etac allE 1); |
|
450 |
by (safe_tac HOL_cs); |
|
451 |
by ( contr_tac 2); |
|
452 |
by ( fast_tac HOL_cs 1); |
|
453 |
by (Asm_full_simp_tac 1); |
|
454 |
qed "slen_scons_eq_rev"; |
|
455 |
||
11655 | 456 |
Goal "!x. (Fin n < #x) = (stream_take n\\<cdot>x ~= x)"; |
11348 | 457 |
by (nat_ind_tac "n" 1); |
11355 | 458 |
by (simp_tac(simpset() addsimps [slen_empty_eq, thm "Fin_0"]) 1); |
11348 | 459 |
by (Fast_tac 1); |
460 |
by (rtac allI 1); |
|
461 |
by (asm_simp_tac (simpset() addsimps [slen_scons_eq]) 1); |
|
462 |
by (etac thin_rl 1); |
|
463 |
by (safe_tac HOL_cs); |
|
464 |
by (Asm_full_simp_tac 1); |
|
465 |
by (stream_case_tac "x" 1); |
|
466 |
by (rotate_tac ~1 2); |
|
467 |
by Auto_tac; |
|
468 |
qed_spec_mp "slen_take_eq"; |
|
469 |
||
11655 | 470 |
Goalw [thm "ile_def"] "(#x <= Fin n) = (stream_take n\\<cdot>x = x)"; |
11348 | 471 |
by (simp_tac (simpset() addsimps [slen_take_eq]) 1); |
472 |
qed "slen_take_eq_rev"; |
|
473 |
||
474 |
Goal "#x = Fin n ==> stream_take n\\<cdot>x = x"; |
|
475 |
by (asm_simp_tac (simpset() addsimps [slen_take_eq_rev RS sym]) 1); |
|
476 |
qed "slen_take_lemma1"; |
|
477 |
||
478 |
Goal "!x. ~stream_finite x --> #(stream_take i\\<cdot>x) = Fin i"; |
|
479 |
by (nat_ind_tac "i" 1); |
|
11355 | 480 |
by (simp_tac(simpset() addsimps [thm "Fin_0"]) 1); |
11348 | 481 |
by (rtac allI 1); |
482 |
by (stream_case_tac "x" 1); |
|
11355 | 483 |
by (auto_tac (claset()addSIs [stream_finite_lemma1], simpset() delsimps [thm "iSuc_Fin"] addsimps [thm "iSuc_Fin" RS sym])); |
11348 | 484 |
by (force_tac (claset(), simpset() addsimps [stream.finite_def]) 1); |
485 |
qed_spec_mp "slen_take_lemma2"; |
|
486 |
||
487 |
Goal "stream_finite x = (#x ~= Infty)"; |
|
488 |
by (rtac iffI 1); |
|
489 |
by (etac stream_finite_ind 1); |
|
490 |
by (Simp_tac 1); |
|
491 |
by (etac (slen_scons RS ssubst) 1); |
|
11355 | 492 |
by (stac (thm "iSuc_Infty" RS sym) 1); |
11348 | 493 |
by (etac contrapos_nn 1); |
11355 | 494 |
by (etac (thm "iSuc_inject" RS iffD1) 1); |
11348 | 495 |
by (case_tac "#x" 1); |
496 |
by (auto_tac (claset()addSDs [slen_take_lemma1], |
|
497 |
simpset() addsimps [stream.finite_def])); |
|
498 |
qed "slen_infinite"; |
|
499 |
||
500 |
Goal "s << t ==> #s <= #t"; |
|
501 |
by (case_tac "stream_finite t" 1); |
|
502 |
by (EVERY'[dtac (slen_infinite RS subst), dtac notnotD] 2); |
|
503 |
by (Asm_simp_tac 2); |
|
504 |
by (etac rev_mp 1); |
|
505 |
by (res_inst_tac [("x","s")] allE 1); |
|
506 |
by (atac 2); |
|
507 |
by (etac (stream_finite_ind) 1); |
|
508 |
by (Simp_tac 1); |
|
509 |
by (rtac allI 1); |
|
510 |
by (stream_case_tac "x" 1); |
|
11355 | 511 |
by (asm_simp_tac (HOL_ss addsimps [slen_empty, thm "i0_lb"]) 1); |
11348 | 512 |
by (asm_simp_tac (HOL_ss addsimps [slen_scons]) 1); |
11355 | 513 |
by (fast_tac(claset() addSIs [thm "iSuc_ile_mono" RS iffD2] addSDs stream.inverts) 1); |
11348 | 514 |
qed "slen_mono"; |
515 |
||
516 |
Goal "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> \ |
|
517 |
\ stream_take n\\<cdot>x = stream_take n\\<cdot>y"; |
|
518 |
by (nat_ind_tac "n" 1); |
|
519 |
by ( simp_tac(simpset() addsimps [slen_empty_eq]) 1); |
|
520 |
by (strip_tac 1); |
|
521 |
by (stream_case_tac "x" 1); |
|
522 |
by (asm_full_simp_tac (HOL_ss addsimps [slen_empty, |
|
11355 | 523 |
thm "iSuc_Fin" RS sym, thm "not_iSuc_ilei0"]) 1); |
11348 | 524 |
by (fatac stream_prefix 1 1); |
525 |
by (safe_tac (claset() addSDs [stream_flat_prefix])); |
|
526 |
by (Simp_tac 1); |
|
527 |
by (rtac cfun_arg_cong 1); |
|
528 |
by (rotate_tac 3 1); |
|
11355 | 529 |
by (asm_full_simp_tac (simpset() delsimps [thm "iSuc_Fin"] addsimps |
530 |
[thm "iSuc_Fin" RS sym, thm "iSuc_ile_mono"]) 1); |
|
11348 | 531 |
qed_spec_mp "slen_take_lemma3"; |
532 |
||
533 |
Goal "stream_finite t ==> \ |
|
534 |
\!s. #(s::'a::flat stream) = #t & s << t --> s = t"; |
|
535 |
by (etac stream_finite_ind 1); |
|
536 |
by (fast_tac (claset() addDs [eq_UU_iff RS iffD2]) 1); |
|
12484 | 537 |
by Safe_tac; |
11348 | 538 |
by (stream_case_tac "sa" 1); |
539 |
by (dtac sym 1); |
|
540 |
by (Asm_full_simp_tac 1); |
|
541 |
by (safe_tac (claset() addSDs [stream_flat_prefix])); |
|
542 |
by (rtac cfun_arg_cong 1); |
|
543 |
by (etac allE 1); |
|
544 |
by (etac mp 1); |
|
545 |
by (Asm_full_simp_tac 1); |
|
546 |
qed "slen_strict_mono_lemma"; |
|
547 |
||
548 |
Goal "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"; |
|
11355 | 549 |
by (rtac (thm "ilessI1") 1); |
11348 | 550 |
by (etac slen_mono 1); |
551 |
by (dtac slen_strict_mono_lemma 1); |
|
552 |
by (Fast_tac 1); |
|
553 |
qed "slen_strict_mono"; |
|
554 |
||
555 |
Goal "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i rt x)"; |
|
556 |
by (nat_ind_tac "i" 1); |
|
557 |
by (Simp_tac 1); |
|
558 |
by (strip_tac 1); |
|
559 |
by (stream_case_tac "x" 1); |
|
11355 | 560 |
by (asm_full_simp_tac (simpset() delsimps [thm "iSuc_Fin"] |
561 |
addsimps [thm "iSuc_Fin" RS sym]) 1); |
|
11348 | 562 |
by (stac iterate_Suc2 1); |
563 |
by (rotate_tac 2 1); |
|
11355 | 564 |
by (asm_full_simp_tac (simpset() delsimps [thm "iSuc_Fin"] |
565 |
addsimps [thm "iSuc_Fin" RS sym, thm "iSuc_ile_mono"]) 1); |
|
11348 | 566 |
qed_spec_mp "slen_rt_mult"; |
567 |
||
568 |
||
569 |
(* ------------------------------------------------------------------------- *) |
|
570 |
||
571 |
section "sfilter"; |
|
572 |
||
573 |
bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def |
|
574 |
"sfilter = (\\<Lambda>p s. case s of x && xs => \ |
|
575 |
\ If p\\<cdot>x then x && sfilter\\<cdot>p\\<cdot>xs else sfilter\\<cdot>p\\<cdot>xs fi)"); |
|
576 |
||
577 |
Goal "sfilter\\<cdot>\\<bottom> = \\<bottom>"; |
|
578 |
by (rtac ext_cfun 1); |
|
579 |
by (stac sfilter_unfold 1); |
|
580 |
by (stream_case_tac "x" 1); |
|
581 |
by Auto_tac; |
|
582 |
qed "strict_sfilter"; |
|
583 |
||
584 |
Goal "sfilter\\<cdot>f\\<cdot>\\<bottom> = \\<bottom>"; |
|
585 |
by (stac sfilter_unfold 1); |
|
586 |
by (Simp_tac 1); |
|
587 |
qed "sfilter_empty"; |
|
588 |
||
589 |
Goal "x ~= \\<bottom> ==> sfilter\\<cdot>f\\<cdot>(x && xs) = \ |
|
590 |
\ If f\\<cdot>x then x && sfilter\\<cdot>f\\<cdot>xs else sfilter\\<cdot>f\\<cdot>xs fi"; |
|
591 |
by (rtac trans 1); |
|
592 |
by (stac sfilter_unfold 1); |
|
593 |
by (Asm_simp_tac 1); |
|
594 |
by (rtac refl 1); |
|
595 |
qed "sfilter_scons"; |
|
596 |