author | wenzelm |
Sun, 30 Jul 2000 13:02:14 +0200 | |
changeset 9473 | 7d13a5ace928 |
parent 9248 | e1dee89de037 |
child 10230 | 5eb935d6cc69 |
permissions | -rw-r--r-- |
9169 | 1 |
(* Title: HOLCF/ex//Stream.ML |
2 |
ID: $Id$ |
|
2570 | 3 |
Author: Franz Regensburger, David von Oheimb |
4 |
Copyright 1993, 1995 Technische Universitaet Muenchen |
|
5 |
||
9169 | 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 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
15 |
Addsimps stream.take_rews; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
16 |
Addsimps stream.when_rews; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
17 |
Addsimps stream.sel_rews; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
18 |
|
2570 | 19 |
(* ----------------------------------------------------------------------- *) |
20 |
(* theorems about scons *) |
|
21 |
(* ----------------------------------------------------------------------- *) |
|
22 |
||
23 |
section "scons"; |
|
24 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
25 |
Goal "a && s = UU = (a = UU)"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
26 |
by Safe_tac; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
27 |
by (etac contrapos2 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
28 |
by (safe_tac (claset() addSIs stream.con_rews)); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
29 |
qed "scons_eq_UU"; |
2570 | 30 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
31 |
Goal "[| a && x = UU; a ~= UU |] ==> R"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
32 |
by (dresolve_tac [stream_con_rew2] 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
33 |
by (contr_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
34 |
qed "scons_not_empty"; |
2570 | 35 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
36 |
Goal "x ~= UU = (EX a y. a ~= UU & x = a && y)"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
37 |
by (cut_facts_tac [stream.exhaust] 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
38 |
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
|
39 |
qed "stream_exhaust_eq"; |
2570 | 40 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
41 |
Goal |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
42 |
"[| 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
|
43 |
by (stream_case_tac "t" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
44 |
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
|
45 |
by (fast_tac (claset() addDs stream.inverts) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
46 |
qed "stream_prefix"; |
2570 | 47 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
48 |
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
|
49 |
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
|
50 |
(ax_flat RS spec RS spec) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
51 |
by (forward_tac stream.inverts 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
52 |
by Safe_tac; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
53 |
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
|
54 |
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
|
55 |
qed "stream_flat_prefix"; |
2570 | 56 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
57 |
Goal "b ~= UU ==> x << b && z = \ |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
58 |
\ (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
|
59 |
by Safe_tac; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
60 |
by (stream_case_tac "x" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
61 |
by (safe_tac (claset() addSDs stream.inverts |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
62 |
addSIs [minimal, monofun_cfun, monofun_cfun_arg])); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
63 |
by (Fast_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
64 |
qed "stream_prefix'"; |
2570 | 65 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
66 |
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
|
67 |
by (best_tac (claset() addSEs stream.injects) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
68 |
qed "stream_inject_eq"; |
2570 | 69 |
|
70 |
||
71 |
(* ----------------------------------------------------------------------- *) |
|
72 |
(* theorems about stream_when *) |
|
73 |
(* ----------------------------------------------------------------------- *) |
|
74 |
||
75 |
section "stream_when"; |
|
76 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
77 |
Goal "stream_when`UU`s=UU"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
78 |
by (stream_case_tac "s" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
79 |
by (ALLGOALS(asm_simp_tac (simpset() addsimps [strict_Rep_CFun1]))); |
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 |
(* |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
90 |
Goal "ft`s=UU --> s=UU"; |
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 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
96 |
Goal "s~=UU ==> ft`s~=UU"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
97 |
by (stream_case_tac "s" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
98 |
by (Blast_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
99 |
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
|
100 |
qed "ft_defin"; |
2570 | 101 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
102 |
Goal "rt`s~=UU ==> s~=UU"; |
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 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
106 |
Goal "(ft`s)&&(rt`s)=s"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
107 |
by (stream_case_tac "s" 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
108 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps stream.rews))); |
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 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
130 |
Goal "(LUB i. stream_take i`s) = s"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
131 |
by (subgoal_tac "(LUB i. stream_take i`s) = fix`stream_copy`s" 1); |
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 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
137 |
Goal "chain (%i. stream_take i`s)"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
138 |
by (rtac chainI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
139 |
by (subgoal_tac "ALL i s. stream_take i`s << stream_take (Suc i)`s" 1); |
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] |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
152 |
"stream_take n`x = x ==> stream_take (Suc n)`x = x"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
153 |
by (rtac antisym_less 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
154 |
by (subgoal_tac "iterate (Suc n) stream_copy UU`x << fix`stream_copy`x" 1); |
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); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
161 |
by (rtac (rewrite_rule [chain] chain_iterate RS spec) 1); |
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 |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
166 |
"ALL s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2"; |
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 ); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
177 |
by (subgoal_tac "stream_take n1`xs = xs" 1); |
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 |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
188 |
"ALL x xs. x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs"; |
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 |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
204 |
"ALL x xs. stream_take n`xs=xs --> stream_take (Suc n)`(x && xs) = x && xs"; |
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 ) \ |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
235 |
\ |] ==> !s. P (stream_take n`s)"; |
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] |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
278 |
"!s1 s2. R s1 s2 --> ft`s1 = ft`s2 & R (rt`s1) (rt`s2) ==> stream_bisim R"; |
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); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
291 |
by (res_inst_tac [("x","ft`x")] exI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
292 |
by (res_inst_tac [("x","rt`x")] exI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
293 |
by (res_inst_tac [("x","rt`x'")] exI 1); |
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); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
296 |
by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
297 |
by (eres_inst_tac [("s","ft`x"),("t","ft`x'")] subst 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
298 |
by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
299 |
by (res_inst_tac [("x","ft`x'")] exI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
300 |
by (res_inst_tac [("x","rt`x")] exI 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
301 |
by (res_inst_tac [("x","rt`x'")] exI 1); |
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); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
304 |
by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
305 |
by (res_inst_tac [("s","ft`x"),("t","ft`x'")] ssubst 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
306 |
by (etac sym 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
307 |
by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1); |
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); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
319 |
by (simp_tac (simpset() addsimps stream.rews) 1); |
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 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset
|
335 |
Goal "stream_finite (rt`s) = stream_finite s"; |
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"; |