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