author | haftmann |
Tue, 06 Dec 2005 17:26:26 +0100 | |
changeset 18362 | e8b7e0a22727 |
parent 17293 | ecf182ccc3ca |
child 18368 | 2f9b2539c5bb |
permissions | -rw-r--r-- |
17293 | 1 |
(* Title: HOLCF/FOCUS/Fstream.ML |
11355 | 2 |
ID: $Id$ |
17293 | 3 |
Author: David von Oheimb, TU Muenchen |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
4 |
*) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
5 |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
6 |
Addsimps[eq_UU_iff RS sym]; |
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
7 |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
8 |
Goal "a = Def d \\<Longrightarrow> a\\<sqsubseteq>b \\<Longrightarrow> b = Def d"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
9 |
by (rtac (flat_eq RS iffD1 RS sym) 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
10 |
by (rtac Def_not_UU 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
11 |
by (dtac antisym_less_inverse 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
12 |
by (eatac (conjunct2 RS trans_less) 1 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
13 |
qed "Def_maximal"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
14 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
15 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
16 |
section "fscons"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
17 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
18 |
Goalw [fscons_def] "a~>s = Def a && s"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
19 |
by (Simp_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
20 |
qed "fscons_def2"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
21 |
|
17293 | 22 |
qed_goal "fstream_exhaust" (the_context ()) "x = UU | (? a y. x = a~> y)" (fn _ => [ |
23 |
simp_tac (simpset() addsimps [fscons_def2]) 1, |
|
24 |
cut_facts_tac [thm "stream.exhaust"] 1, |
|
25 |
fast_tac (claset() addDs [not_Undef_is_Def RS iffD1]) 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
26 |
|
17293 | 27 |
qed_goal "fstream_cases" (the_context ()) "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P" |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
28 |
(fn prems => [ |
17293 | 29 |
cut_facts_tac [fstream_exhaust] 1, |
30 |
etac disjE 1, |
|
31 |
eresolve_tac prems 1, |
|
32 |
REPEAT(etac exE 1), |
|
33 |
eresolve_tac prems 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
34 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
35 |
fun fstream_case_tac s i = res_inst_tac [("x",s)] fstream_cases i |
17293 | 36 |
THEN hyp_subst_tac i THEN hyp_subst_tac (i+1); |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
37 |
|
17293 | 38 |
qed_goal "fstream_exhaust_eq" (the_context ()) "(x ~= UU) = (? a y. x = a~> y)" (fn _ => [ |
39 |
simp_tac(simpset() addsimps [fscons_def2,thm "stream_exhaust_eq"]) 1, |
|
40 |
fast_tac (claset() addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
41 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
42 |
|
17293 | 43 |
qed_goal "fscons_not_empty" (the_context ()) "a~> s ~= <>" (fn _ => [ |
44 |
stac fscons_def2 1, |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
45 |
Simp_tac 1]); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
46 |
Addsimps[fscons_not_empty]; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
47 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
48 |
|
17293 | 49 |
qed_goal "fscons_inject" (the_context ()) "(a~> s = b~> t) = (a = b & s = t)" (fn _ => [ |
50 |
simp_tac (HOL_ss addsimps [fscons_def2]) 1, |
|
51 |
stac (hd lift.inject RS sym) 1, (*2*back();*) |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
52 |
Simp_tac 1]); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
53 |
Addsimps[fscons_inject]; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
54 |
|
17293 | 55 |
qed_goal "fstream_prefix" (the_context ()) "a~> s << t ==> ? tt. t = a~> tt & s << tt" (fn prems =>[ |
56 |
cut_facts_tac prems 1, |
|
57 |
res_inst_tac [("x","t")] (thm "stream.casedist") 1, |
|
58 |
cut_facts_tac [fscons_not_empty] 1, |
|
59 |
fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2]) 1, |
|
60 |
asm_full_simp_tac (HOL_ss addsimps [fscons_def2]) 1, |
|
61 |
dtac (thm "stream_flat_prefix") 1, |
|
62 |
rtac Def_not_UU 1, |
|
63 |
fast_tac HOL_cs 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
64 |
|
17293 | 65 |
qed_goal "fstream_prefix'" (the_context ()) |
66 |
"x << a~> z = (x = <> | (? y. x = a~> y & y << z))" (fn _ => [ |
|
67 |
simp_tac(HOL_ss addsimps [fscons_def2, Def_not_UU RS thm "stream_prefix'"])1, |
|
68 |
Step_tac 1, |
|
18362
e8b7e0a22727
removed thms 'swap' and 'nth_map' from ML toplevel
haftmann
parents:
17293
diff
changeset
|
69 |
ALLGOALS(etac BasicClassical.swap), |
17293 | 70 |
fast_tac (HOL_cs addIs [refl_less] addEs [DefE]) 2, |
71 |
rtac Lift_cases 1, |
|
72 |
contr_tac 1, |
|
73 |
Step_tac 1, |
|
74 |
dtac (Def_inject_less_eq RS iffD1) 1, |
|
75 |
Fast_tac 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
76 |
Addsimps[fstream_prefix']; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
77 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
78 |
(* ------------------------------------------------------------------------- *) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
79 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
80 |
section "ft & rt"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
81 |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
82 |
bind_thm("ft_empty",hd (thms "stream.sel_rews")); |
17293 | 83 |
qed_goalw "ft_fscons" (the_context ()) [fscons_def] "ft\\<cdot>(m~> s) = Def m" (fn _ => [ |
84 |
(Simp_tac 1)]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
85 |
Addsimps[ft_fscons]; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
86 |
|
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
87 |
bind_thm("rt_empty",hd (tl (thms "stream.sel_rews"))); |
17293 | 88 |
qed_goalw "rt_fscons" (the_context ()) [fscons_def] "rt\\<cdot>(m~> s) = s" (fn _ => [ |
89 |
(Simp_tac 1)]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
90 |
Addsimps[rt_fscons]; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
91 |
|
17293 | 92 |
qed_goalw "ft_eq" (the_context ()) [fscons_def] "(ft\\<cdot>s = Def a) = (? t. s = a~> t)" (K [ |
93 |
Simp_tac 1, |
|
94 |
Safe_tac, |
|
95 |
etac subst 1, |
|
96 |
rtac exI 1, |
|
97 |
rtac (thm "surjectiv_scons" RS sym) 1, |
|
98 |
Simp_tac 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
99 |
Addsimps[ft_eq]; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
100 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
101 |
Goal "(d\\<leadsto>y = x) = (ft\\<cdot>x = Def d & rt\\<cdot>x = y)"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
102 |
by Auto_tac; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
103 |
qed "surjective_fscons_lemma"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
104 |
Goal "ft\\<cdot>x = Def d \\<Longrightarrow> d\\<leadsto>rt\\<cdot>x = x"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
105 |
by (asm_simp_tac (simpset() addsimps [surjective_fscons_lemma]) 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
106 |
qed "surjective_fscons"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
107 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
108 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
109 |
(* ------------------------------------------------------------------------- *) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
110 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
111 |
section "take"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
112 |
|
17293 | 113 |
qed_goalw "fstream_take_Suc" (the_context ()) [fscons_def] |
114 |
"stream_take (Suc n)\\<cdot>(a~> s) = a~> stream_take n\\<cdot>s" (K [ |
|
115 |
Simp_tac 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
116 |
Addsimps[fstream_take_Suc]; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
117 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
118 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
119 |
(* ------------------------------------------------------------------------- *) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
120 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
121 |
section "slen"; |
17293 | 122 |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
123 |
(*bind_thm("slen_empty", slen_empty);*) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
124 |
|
17293 | 125 |
qed_goalw "slen_fscons" (the_context ()) [fscons_def] "#(m~> s) = iSuc (#s)" (fn _ => [ |
126 |
(Simp_tac 1)]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
127 |
|
17293 | 128 |
qed_goal "slen_fscons_eq" (the_context ()) |
129 |
"(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)" (fn _ => [ |
|
130 |
simp_tac (HOL_ss addsimps [fscons_def2, thm "slen_scons_eq"]) 1, |
|
131 |
fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
132 |
|
17293 | 133 |
qed_goal "slen_fscons_eq_rev" (the_context ()) |
134 |
"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))" (K [ |
|
135 |
simp_tac (HOL_ss addsimps [fscons_def2, thm "slen_scons_eq_rev"]) 1, |
|
136 |
step_tac (HOL_cs addSEs [DefE]) 1, |
|
137 |
step_tac (HOL_cs addSEs [DefE]) 1, |
|
138 |
step_tac (HOL_cs addSEs [DefE]) 1, |
|
139 |
step_tac (HOL_cs addSEs [DefE]) 1, |
|
140 |
step_tac (HOL_cs addSEs [DefE]) 1, |
|
141 |
step_tac (HOL_cs addSEs [DefE]) 1, |
|
18362
e8b7e0a22727
removed thms 'swap' and 'nth_map' from ML toplevel
haftmann
parents:
17293
diff
changeset
|
142 |
etac BasicClassical.swap 1, |
17293 | 143 |
fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]); |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
144 |
|
17293 | 145 |
qed_goal "slen_fscons_less_eq" (the_context ()) |
146 |
"(#(a~> y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))" (fn _ => [ |
|
147 |
stac slen_fscons_eq_rev 1, |
|
148 |
fast_tac (HOL_cs addSDs [fscons_inject RS iffD1]) 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
149 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
150 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
151 |
(* ------------------------------------------------------------------------- *) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
152 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
153 |
section "induction"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
154 |
|
17293 | 155 |
qed_goal "fstream_ind" (the_context ()) |
156 |
"[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x" (fn prems => [ |
|
157 |
cut_facts_tac prems 1, |
|
158 |
etac (thm "stream.ind") 1, |
|
159 |
atac 1, |
|
160 |
fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] |
|
161 |
addEs (tl (tl prems) RL [fscons_def2 RS subst])) 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
162 |
|
17293 | 163 |
qed_goal "fstream_ind2" (the_context ()) |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
164 |
"[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x" (fn prems => [ |
17293 | 165 |
cut_facts_tac prems 1, |
166 |
etac (thm "stream_ind2") 1, |
|
167 |
atac 1, |
|
168 |
fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] |
|
169 |
addIs ([hd(tl(tl prems))]RL[fscons_def2 RS subst]))1, |
|
170 |
fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] |
|
171 |
addEs [hd(tl(tl(tl prems))RL[fscons_def2 RS subst] |
|
172 |
RL[fscons_def2 RS subst])])1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
173 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
174 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
175 |
(* ------------------------------------------------------------------------- *) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
176 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
177 |
section "fsfilter"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
178 |
|
17293 | 179 |
qed_goalw "fsfilter_empty" (the_context ()) [fsfilter_def] "A(C)UU = UU" (fn _ => [ |
180 |
rtac (thm "sfilter_empty") 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
181 |
|
17293 | 182 |
qed_goalw "fsfilter_fscons" (the_context ()) [fsfilter_def] |
183 |
"A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)" (fn _ => [ |
|
184 |
simp_tac (simpset() addsimps [fscons_def2,thm "sfilter_scons",If_and_if]) 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
185 |
|
17293 | 186 |
qed_goal "fsfilter_emptys" (the_context ()) "{}(C)x = UU" (fn _ => [ |
187 |
res_inst_tac [("x","x")] fstream_ind 1, |
|
188 |
resolve_tac adm_lemmas 1, |
|
189 |
cont_tacR 1, |
|
190 |
rtac fsfilter_empty 1, |
|
191 |
asm_simp_tac (simpset()addsimps [fsfilter_fscons]) 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
192 |
|
17293 | 193 |
qed_goal "fsfilter_insert" (the_context ()) "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)" (fn _=> [ |
194 |
simp_tac (simpset() addsimps [thm "fsfilter_fscons"]) 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
195 |
|
17293 | 196 |
qed_goal "fsfilter_single_in" (the_context ()) "{a}(C)a~> x = a~> ({a}(C)x)" (fn _=> [ |
197 |
rtac fsfilter_insert 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
198 |
|
17293 | 199 |
qed_goal "fsfilter_single_out" (the_context ()) "b ~= a ==> {a}(C)b~> x = ({a}(C)x)" (fn prems => [ |
200 |
cut_facts_tac prems 1, |
|
201 |
asm_simp_tac (simpset() addsimps[fsfilter_fscons]) 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
202 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
203 |
Goal "\\<lbrakk>chain Y; lub (range Y) = a\\<leadsto>s\\<rbrakk> \\<Longrightarrow> \\<exists>j t. Y j = a\\<leadsto>t"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
204 |
by (case_tac "max_in_chain i Y" 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
205 |
by (datac (lub_finch1 RS thelubI RS sym) 1 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
206 |
by (Force_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
207 |
by (rewtac max_in_chain_def); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
208 |
by Auto_tac; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
209 |
by (fatac chain_mono3 1 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
210 |
by (res_inst_tac [("x","Y j")] fstream_cases 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
211 |
by (Force_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
212 |
by (dres_inst_tac [("x","j")] is_ub_thelub 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
213 |
by (Force_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
214 |
qed "fstream_lub_lemma1"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
215 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
216 |
Goal "\\<lbrakk>chain Y; lub (range Y) = a\\<leadsto>s\\<rbrakk> \\<Longrightarrow> (\\<exists>j t. Y j = a\\<leadsto>t) & (\\<exists>X. chain X & (!i. ? j. Y j = a\\<leadsto>X i) & lub (range X) = s)"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
217 |
by (fatac fstream_lub_lemma1 1 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
218 |
by (Clarsimp_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
219 |
by (res_inst_tac [("x","%i. rt\\<cdot>(Y(i+j))")] exI 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
220 |
by (rtac conjI 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
221 |
by (etac (chain_shift RS chain_monofun) 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
222 |
by Safe_tac; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
223 |
by (dres_inst_tac [("x","j"),("y","i+j")] chain_mono3 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
224 |
by (Simp_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
225 |
by (Asm_full_simp_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
226 |
by (res_inst_tac [("x","i+j")] exI 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
227 |
by (dtac fstream_prefix 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
228 |
by (Clarsimp_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
229 |
by (stac (contlub_cfun RS sym) 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
230 |
by (rtac chainI 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
231 |
by (Fast_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
232 |
by (etac chain_shift 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
233 |
by (stac (lub_const RS thelubI) 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
234 |
by (stac lub_range_shift 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
235 |
by (atac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
236 |
by (Asm_simp_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
237 |
qed "fstream_lub_lemma"; |