author | wenzelm |
Tue, 06 Sep 2005 21:51:17 +0200 | |
changeset 17293 | ecf182ccc3ca |
parent 15188 | 9d57263faf9e |
child 17955 | 3b34516662c6 |
permissions | -rw-r--r-- |
17293 | 1 |
(* Title: HOLCF/ex/Stream_adm.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 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
6 |
(* ----------------------------------------------------------------------- *) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
7 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
8 |
val down_cont_def = thm "down_cont_def"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
9 |
val INTER_down_iterate_is_gfp = thm "INTER_down_iterate_is_gfp"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
10 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
11 |
section "admissibility"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
12 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
13 |
Goal "[| chain Y; !i. P (Y i);\ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
14 |
\(!!Y. [| chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|]\ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
15 |
\ ==> P(lub (range Y))) |] ==> P(lub (range Y))"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
16 |
by (cut_facts_tac (premises()) 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
17 |
by (eatac increasing_chain_adm_lemma 1 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
18 |
by (etac thin_rl 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
19 |
by (EVERY'[eresolve_tac (premises()), atac, etac thin_rl] 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
20 |
by (rtac allI 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
21 |
by (case_tac "!j. stream_finite (Y j)" 1); |
11355 | 22 |
by ( rtac (thm "chain_incr") 1); |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
23 |
by ( rtac allI 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
24 |
by ( dtac spec 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
25 |
by ( Safe_tac); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
26 |
by ( rtac exI 1); |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
27 |
by ( rtac (thm "slen_strict_mono") 1); |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
28 |
by ( etac spec 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
29 |
by ( atac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
30 |
by ( atac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
31 |
by (dtac (not_ex RS iffD1) 1); |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
32 |
by (stac (thm "slen_infinite") 1); |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
33 |
by (etac thin_rl 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
34 |
by (dtac spec 1); |
11355 | 35 |
by (fold_goals_tac [thm "ile_def"]); |
36 |
by (etac (thm "ile_iless_trans" RS (thm "Infty_eq" RS iffD1)) 1); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
37 |
by (Simp_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
38 |
qed "flatstream_adm_lemma"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
39 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
40 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
41 |
(* should be without reference to stream length? *) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
42 |
Goalw [adm_def] "[|(!!Y. [| chain Y; !i. P (Y i); \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
43 |
\!k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(lub (range Y)))|]==> adm P"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
44 |
by (strip_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
45 |
by (eatac flatstream_adm_lemma 1 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
46 |
by (EVERY'[eresolve_tac (premises()), atac, atac] 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
47 |
qed "flatstream_admI"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
48 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
49 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
50 |
(* context (theory "Nat_InFinity");*) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
51 |
Goal "Fin (i + j) <= x ==> Fin i <= x"; |
11355 | 52 |
by (rtac (thm "ile_trans") 1); |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
53 |
by (atac 2); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
54 |
by (Simp_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
55 |
qed "ile_lemma"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
56 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
57 |
Goalw [stream_monoP_def] |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
58 |
"!!X. stream_monoP F ==> !i. ? l. !x y. \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
59 |
\ Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
60 |
by (safe_tac HOL_cs); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
61 |
by (res_inst_tac [("x","i*ia")] exI 1); |
13454 | 62 |
by (induct_tac "ia" 1); |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
63 |
by ( Simp_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
64 |
by (Simp_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
65 |
by (strip_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
66 |
by (etac allE 1 THEN etac all_dupE 1 THEN dtac mp 1 THEN etac ile_lemma 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
67 |
by (dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
68 |
by (etac allE 1 THEN dtac mp 1 THEN rtac ile_lemma 1); |
11355 | 69 |
by ( etac (thm "ile_trans") 1); |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
70 |
by ( etac (thm "slen_mono") 1); |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
71 |
by (etac ssubst 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
72 |
by (safe_tac HOL_cs); |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
73 |
by ( eatac (ile_lemma RS thm "slen_take_lemma3" RS subst) 2 1); |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
74 |
by (etac allE 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
75 |
by (etac allE 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
76 |
by (dtac mp 1); |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
77 |
by ( etac (thm "slen_rt_mult") 1); |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
78 |
by (dtac mp 1); |
15188
9d57263faf9e
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents:
14981
diff
changeset
|
79 |
by (etac (thm "monofun_rt_mult") 1); |
17293 | 80 |
by (mp_tac 1); |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
81 |
by (atac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
82 |
qed "stream_monoP2I"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
83 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
84 |
Goal "[| !i. ? l. !x y. \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
85 |
\Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;\ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
86 |
\ down_cont F |] ==> adm (%x. x:gfp F)"; |
17293 | 87 |
byev[ etac (INTER_down_iterate_is_gfp RS ssubst) 1, (* cont *) |
88 |
Simp_tac 1, |
|
89 |
resolve_tac adm_lemmas 1, |
|
90 |
rtac flatstream_admI 1, |
|
91 |
etac allE 1, |
|
92 |
etac exE 1, |
|
93 |
etac allE 1 THEN etac exE 1, |
|
94 |
etac allE 1 THEN etac allE 1 THEN dtac mp 1, (* stream_monoP *) |
|
95 |
dtac (thm "ileI1") 1, |
|
96 |
dtac (thm "ile_trans") 1, |
|
97 |
rtac (thm "ile_iSuc") 1, |
|
98 |
dtac (thm "iSuc_ile_mono" RS iffD1) 1, |
|
99 |
atac 1, |
|
100 |
dtac mp 1, |
|
101 |
etac is_ub_thelub 1, |
|
102 |
Fast_tac 1]; |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
103 |
qed "stream_monoP2_gfp_admI"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
104 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
105 |
bind_thm("fstream_gfp_admI",stream_monoP2I RS stream_monoP2_gfp_admI); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
106 |
|
17293 | 107 |
qed_goalw "stream_antiP2I" (the_context ()) [stream_antiP_def] |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
108 |
"!!X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|]\ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
109 |
\ ==> !i x y. x << y --> y:down_iterate F i --> x:down_iterate F i" (K [ |
17293 | 110 |
rtac allI 1, |
111 |
induct_tac "i" 1, |
|
112 |
Simp_tac 1, |
|
113 |
Simp_tac 1, |
|
114 |
strip_tac 1, |
|
115 |
etac allE 1 THEN etac all_dupE 1 THEN etac exE 1 THEN etac exE 1, |
|
116 |
etac conjE 1, |
|
117 |
case_tac "#x < Fin i" 1, |
|
118 |
fast_tac HOL_cs 1, |
|
119 |
fold_goals_tac [thm "ile_def"], |
|
120 |
mp_tac 1, |
|
121 |
etac all_dupE 1 THEN dtac mp 1 THEN rtac refl_less 1, |
|
122 |
etac ssubst 1, |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
123 |
etac allE 1 THEN mp_tac 1, |
17293 | 124 |
dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1, |
125 |
etac conjE 1 THEN rtac conjI 1, |
|
126 |
etac (thm "slen_take_lemma3" RS ssubst) 1 THEN atac 1, |
|
127 |
atac 1, |
|
128 |
etac allE 1 THEN etac allE 1 THEN dtac mp 1 THEN etac (thm "monofun_rt_mult") 1, |
|
129 |
mp_tac 1, |
|
130 |
atac 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
131 |
|
17293 | 132 |
qed_goalw "stream_antiP2_non_gfp_admI" (the_context ()) [adm_def] |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
133 |
"!!X. [|!i x y. x << y --> y:down_iterate F i --> x:down_iterate F i; down_cont F |] \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
134 |
\ ==> adm (%u. ~ u:gfp F)" (K [ |
17293 | 135 |
asm_simp_tac (simpset() addsimps [INTER_down_iterate_is_gfp]) 1, |
136 |
fast_tac (claset() addSDs [is_ub_thelub]) 1]); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
137 |
|
17293 | 138 |
bind_thm ("fstream_non_gfp_admI", stream_antiP2I RS |
139 |
stream_antiP2_non_gfp_admI); |
|
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
140 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
141 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
142 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
143 |
(**new approach for adm********************************************************) |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
144 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
145 |
section "antitonP"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
146 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
147 |
Goalw [antitonP_def] "[| antitonP P; y:P; x<<y |] ==> x:P"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
148 |
by Auto_tac; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
149 |
qed "antitonPD"; |
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 |
Goalw [antitonP_def]"!x y. y:P --> x<<y --> x:P ==> antitonP P"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
152 |
by (Fast_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
153 |
qed "antitonPI"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
154 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
155 |
Goalw [adm_def] "antitonP P ==> adm (%u. u~:P)"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
156 |
by (auto_tac (claset() addDs [antitonPD] addEs [is_ub_thelub],simpset())); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
157 |
qed "antitonP_adm_non_P"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
158 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
159 |
Goal "P \\<equiv> gfp F \\<Longrightarrow> {y. \\<exists>x::'a::pcpo. y \\<sqsubseteq> x \\<and> x \\<in> P} \\<subseteq> F {y. \\<exists>x. y \\<sqsubseteq> x \\<and> x \\<in> P} \\<Longrightarrow> \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
160 |
\ adm (\\<lambda>u. u\\<notin>P)"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
161 |
by (Asm_full_simp_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
162 |
by (rtac antitonP_adm_non_P 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
163 |
by (rtac antitonPI 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
164 |
by (dtac gfp_upperbound 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
165 |
by (Fast_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
166 |
qed "def_gfp_adm_nonP"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
167 |
|
17293 | 168 |
Goalw [adm_def] |
11350
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
169 |
"{lub (range Y) |Y. chain Y & (\\<forall>i. Y i \\<in> P)} \\<subseteq> P \\<Longrightarrow> adm (\\<lambda>x. x\\<in>P)"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
170 |
by (Fast_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
171 |
qed "adm_set"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
172 |
|
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
173 |
Goal "P \\<equiv> gfp F \\<Longrightarrow> {lub (range Y) |Y. chain Y \\<and> (\\<forall>i. Y i \\<in> P)} \\<subseteq> \ |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
174 |
\ F {lub (range Y) |Y. chain Y \\<and> (\\<forall>i. Y i \\<in> P)} \\<Longrightarrow> adm (\\<lambda>x. x\\<in>P)"; |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
175 |
by (Asm_full_simp_tac 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
176 |
by (rtac adm_set 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
177 |
by (etac gfp_upperbound 1); |
4c55b020d6ee
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff
changeset
|
178 |
qed "def_gfp_admI"; |