1 (* Title: HOLCF/sprod2.ML |
1 (* Title: HOLCF/Sprod2.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 Copyright 1993 Technische Universitaet Muenchen |
4 Copyright 1993 Technische Universitaet Muenchen |
5 |
5 |
6 Lemmas for sprod2.thy |
6 Lemmas for Sprod2.thy |
7 *) |
7 *) |
8 |
|
9 |
8 |
10 open Sprod2; |
9 open Sprod2; |
11 |
10 |
12 (* ------------------------------------------------------------------------ *) |
11 (* for compatibility with old HOLCF-Version *) |
13 (* access to less_sprod in class po *) |
12 qed_goal "inst_sprod_po" thy "(op <<)=(%x y.Isfst x<<Isfst y&Issnd x<<Issnd y)" |
14 (* ------------------------------------------------------------------------ *) |
13 (fn prems => |
15 |
|
16 qed_goal "less_sprod3a" Sprod2.thy |
|
17 "p1=Ispair UU UU ==> p1 << p2" |
|
18 (fn prems => |
|
19 [ |
14 [ |
20 (cut_facts_tac prems 1), |
15 (fold_goals_tac [po_def,less_sprod_def]), |
21 (stac inst_sprod_po 1), |
16 (rtac refl 1) |
22 (etac less_sprod1a 1) |
|
23 ]); |
|
24 |
|
25 |
|
26 qed_goal "less_sprod3b" Sprod2.thy |
|
27 "p1~=Ispair UU UU ==>\ |
|
28 \ (p1<<p2) = (Isfst(p1)<<Isfst(p2) & Issnd(p1)<<Issnd(p2))" |
|
29 (fn prems => |
|
30 [ |
|
31 (cut_facts_tac prems 1), |
|
32 (stac inst_sprod_po 1), |
|
33 (etac less_sprod1b 1) |
|
34 ]); |
|
35 |
|
36 qed_goal "less_sprod4b" Sprod2.thy |
|
37 "p << Ispair UU UU ==> p = Ispair UU UU" |
|
38 (fn prems => |
|
39 [ |
|
40 (cut_facts_tac prems 1), |
|
41 (rtac less_sprod2b 1), |
|
42 (etac (inst_sprod_po RS subst) 1) |
|
43 ]); |
|
44 |
|
45 bind_thm ("less_sprod4a", less_sprod4b RS defined_Ispair_rev); |
|
46 (* Ispair ?a ?b << Ispair UU UU ==> ?a = UU | ?b = UU *) |
|
47 |
|
48 qed_goal "less_sprod4c" Sprod2.thy |
|
49 "[|Ispair xa ya << Ispair x y; xa~=UU; ya~=UU; x~=UU; y~=UU|] ==>\ |
|
50 \ xa<<x & ya << y" |
|
51 (fn prems => |
|
52 [ |
|
53 (cut_facts_tac prems 1), |
|
54 (rtac less_sprod2c 1), |
|
55 (etac (inst_sprod_po RS subst) 1), |
|
56 (REPEAT (atac 1)) |
|
57 ]); |
17 ]); |
58 |
18 |
59 (* ------------------------------------------------------------------------ *) |
19 (* ------------------------------------------------------------------------ *) |
60 (* type sprod is pointed *) |
20 (* type sprod is pointed *) |
61 (* ------------------------------------------------------------------------ *) |
21 (* ------------------------------------------------------------------------ *) |
62 |
22 |
63 qed_goal "minimal_sprod" Sprod2.thy "Ispair UU UU << p" |
23 qed_goal "minimal_sprod" thy "Ispair UU UU << p" |
64 (fn prems => |
24 (fn prems => |
65 [ |
25 [ |
66 (rtac less_sprod3a 1), |
26 (simp_tac(Sprod0_ss addsimps[inst_sprod_po,minimal])1) |
67 (rtac refl 1) |
27 ]); |
|
28 |
|
29 bind_thm ("UU_sprod_def",minimal_sprod RS minimal2UU RS sym); |
|
30 |
|
31 qed_goal "least_sprod" thy "? x::'a**'b.!y.x<<y" |
|
32 (fn prems => |
|
33 [ |
|
34 (res_inst_tac [("x","Ispair UU UU")] exI 1), |
|
35 (rtac (minimal_sprod RS allI) 1) |
68 ]); |
36 ]); |
69 |
37 |
70 (* ------------------------------------------------------------------------ *) |
38 (* ------------------------------------------------------------------------ *) |
71 (* Ispair is monotone in both arguments *) |
39 (* Ispair is monotone in both arguments *) |
72 (* ------------------------------------------------------------------------ *) |
40 (* ------------------------------------------------------------------------ *) |
75 (fn prems => |
43 (fn prems => |
76 [ |
44 [ |
77 (strip_tac 1), |
45 (strip_tac 1), |
78 (rtac (less_fun RS iffD2) 1), |
46 (rtac (less_fun RS iffD2) 1), |
79 (strip_tac 1), |
47 (strip_tac 1), |
80 (res_inst_tac [("Q", |
48 (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1), |
81 " Ispair y xa = Ispair UU UU")] (excluded_middle RS disjE) 1), |
49 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
82 (res_inst_tac [("Q", |
50 (forward_tac [notUU_I] 1), |
83 " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1), |
|
84 (rtac (less_sprod3b RS iffD2) 1), |
|
85 (atac 1), |
51 (atac 1), |
86 (rtac conjI 1), |
52 (REPEAT(asm_simp_tac(Sprod0_ss |
87 (stac Isfst 1), |
53 addsimps[inst_sprod_po,refl_less,minimal]) 1)) |
88 (etac (strict_Ispair_rev RS conjunct1) 1), |
|
89 (etac (strict_Ispair_rev RS conjunct2) 1), |
|
90 (stac Isfst 1), |
|
91 (etac (strict_Ispair_rev RS conjunct1) 1), |
|
92 (etac (strict_Ispair_rev RS conjunct2) 1), |
|
93 (atac 1), |
|
94 (stac Issnd 1), |
|
95 (etac (strict_Ispair_rev RS conjunct1) 1), |
|
96 (etac (strict_Ispair_rev RS conjunct2) 1), |
|
97 (stac Issnd 1), |
|
98 (etac (strict_Ispair_rev RS conjunct1) 1), |
|
99 (etac (strict_Ispair_rev RS conjunct2) 1), |
|
100 (rtac refl_less 1), |
|
101 (etac less_sprod3a 1), |
|
102 (res_inst_tac [("Q", |
|
103 " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1), |
|
104 (etac less_sprod3a 2), |
|
105 (res_inst_tac [("P","Ispair y xa = Ispair UU UU")] notE 1), |
|
106 (atac 2), |
|
107 (rtac defined_Ispair 1), |
|
108 (etac notUU_I 1), |
|
109 (etac (strict_Ispair_rev RS conjunct1) 1), |
|
110 (etac (strict_Ispair_rev RS conjunct2) 1) |
|
111 ]); |
54 ]); |
112 |
|
113 |
55 |
114 qed_goalw "monofun_Ispair2" Sprod2.thy [monofun] "monofun(Ispair(x))" |
56 qed_goalw "monofun_Ispair2" Sprod2.thy [monofun] "monofun(Ispair(x))" |
115 (fn prems => |
57 (fn prems => |
116 [ |
58 [ |
117 (strip_tac 1), |
59 (strip_tac 1), |
118 (res_inst_tac [("Q", |
60 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
119 " Ispair x y = Ispair UU UU")] (excluded_middle RS disjE) 1), |
61 (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1), |
120 (res_inst_tac [("Q", |
62 (forward_tac [notUU_I] 1), |
121 " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1), |
|
122 (rtac (less_sprod3b RS iffD2) 1), |
|
123 (atac 1), |
63 (atac 1), |
124 (rtac conjI 1), |
64 (REPEAT(asm_simp_tac(Sprod0_ss |
125 (stac Isfst 1), |
65 addsimps[inst_sprod_po,refl_less,minimal]) 1)) |
126 (etac (strict_Ispair_rev RS conjunct1) 1), |
|
127 (etac (strict_Ispair_rev RS conjunct2) 1), |
|
128 (stac Isfst 1), |
|
129 (etac (strict_Ispair_rev RS conjunct1) 1), |
|
130 (etac (strict_Ispair_rev RS conjunct2) 1), |
|
131 (rtac refl_less 1), |
|
132 (stac Issnd 1), |
|
133 (etac (strict_Ispair_rev RS conjunct1) 1), |
|
134 (etac (strict_Ispair_rev RS conjunct2) 1), |
|
135 (stac Issnd 1), |
|
136 (etac (strict_Ispair_rev RS conjunct1) 1), |
|
137 (etac (strict_Ispair_rev RS conjunct2) 1), |
|
138 (atac 1), |
|
139 (etac less_sprod3a 1), |
|
140 (res_inst_tac [("Q", |
|
141 " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1), |
|
142 (etac less_sprod3a 2), |
|
143 (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1), |
|
144 (atac 2), |
|
145 (rtac defined_Ispair 1), |
|
146 (etac (strict_Ispair_rev RS conjunct1) 1), |
|
147 (etac notUU_I 1), |
|
148 (etac (strict_Ispair_rev RS conjunct2) 1) |
|
149 ]); |
66 ]); |
|
67 |
150 |
68 |
151 qed_goal " monofun_Ispair" Sprod2.thy |
69 qed_goal " monofun_Ispair" Sprod2.thy |
152 "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2" |
70 "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2" |
153 (fn prems => |
71 (fn prems => |
154 [ |
72 [ |
164 |
82 |
165 (* ------------------------------------------------------------------------ *) |
83 (* ------------------------------------------------------------------------ *) |
166 (* Isfst and Issnd are monotone *) |
84 (* Isfst and Issnd are monotone *) |
167 (* ------------------------------------------------------------------------ *) |
85 (* ------------------------------------------------------------------------ *) |
168 |
86 |
169 qed_goalw " monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)" |
87 qed_goalw "monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)" |
170 (fn prems => |
88 (fn prems => [(simp_tac (HOL_ss addsimps [inst_sprod_po]) 1)]); |
171 [ |
|
172 (strip_tac 1), |
|
173 (res_inst_tac [("p","x")] IsprodE 1), |
|
174 (hyp_subst_tac 1), |
|
175 (rtac trans_less 1), |
|
176 (rtac minimal 2), |
|
177 (stac strict_Isfst1 1), |
|
178 (rtac refl_less 1), |
|
179 (hyp_subst_tac 1), |
|
180 (res_inst_tac [("p","y")] IsprodE 1), |
|
181 (hyp_subst_tac 1), |
|
182 (res_inst_tac [("t","Isfst(Ispair xa ya)")] subst 1), |
|
183 (rtac refl_less 2), |
|
184 (etac (less_sprod4b RS sym RS arg_cong) 1), |
|
185 (hyp_subst_tac 1), |
|
186 (stac Isfst 1), |
|
187 (atac 1), |
|
188 (atac 1), |
|
189 (stac Isfst 1), |
|
190 (atac 1), |
|
191 (atac 1), |
|
192 (etac (less_sprod4c RS conjunct1) 1), |
|
193 (REPEAT (atac 1)) |
|
194 ]); |
|
195 |
89 |
196 qed_goalw "monofun_Issnd" Sprod2.thy [monofun] "monofun(Issnd)" |
90 qed_goalw "monofun_Issnd" Sprod2.thy [monofun] "monofun(Issnd)" |
197 (fn prems => |
91 (fn prems => [(simp_tac (HOL_ss addsimps [inst_sprod_po]) 1)]); |
198 [ |
|
199 (strip_tac 1), |
|
200 (res_inst_tac [("p","x")] IsprodE 1), |
|
201 (hyp_subst_tac 1), |
|
202 (rtac trans_less 1), |
|
203 (rtac minimal 2), |
|
204 (stac strict_Issnd1 1), |
|
205 (rtac refl_less 1), |
|
206 (hyp_subst_tac 1), |
|
207 (res_inst_tac [("p","y")] IsprodE 1), |
|
208 (hyp_subst_tac 1), |
|
209 (res_inst_tac [("t","Issnd(Ispair xa ya)")] subst 1), |
|
210 (rtac refl_less 2), |
|
211 (etac (less_sprod4b RS sym RS arg_cong) 1), |
|
212 (hyp_subst_tac 1), |
|
213 (stac Issnd 1), |
|
214 (atac 1), |
|
215 (atac 1), |
|
216 (stac Issnd 1), |
|
217 (atac 1), |
|
218 (atac 1), |
|
219 (etac (less_sprod4c RS conjunct2) 1), |
|
220 (REPEAT (atac 1)) |
|
221 ]); |
|
222 |
|
223 |
92 |
224 (* ------------------------------------------------------------------------ *) |
93 (* ------------------------------------------------------------------------ *) |
225 (* the type 'a ** 'b is a cpo *) |
94 (* the type 'a ** 'b is a cpo *) |
226 (* ------------------------------------------------------------------------ *) |
95 (* ------------------------------------------------------------------------ *) |
227 |
96 |
229 "[|is_chain(S)|] ==> range(S) <<| \ |
98 "[|is_chain(S)|] ==> range(S) <<| \ |
230 \ Ispair (lub(range(%i.Isfst(S i)))) (lub(range(%i.Issnd(S i))))" |
99 \ Ispair (lub(range(%i.Isfst(S i)))) (lub(range(%i.Issnd(S i))))" |
231 (fn prems => |
100 (fn prems => |
232 [ |
101 [ |
233 (cut_facts_tac prems 1), |
102 (cut_facts_tac prems 1), |
234 (rtac is_lubI 1), |
103 (rtac (conjI RS is_lubI) 1), |
235 (rtac conjI 1), |
104 (rtac (allI RS ub_rangeI) 1), |
236 (rtac ub_rangeI 1), |
|
237 (rtac allI 1), |
|
238 (res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1), |
105 (res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1), |
239 (rtac monofun_Ispair 1), |
106 (rtac monofun_Ispair 1), |
240 (rtac is_ub_thelub 1), |
107 (rtac is_ub_thelub 1), |
241 (etac (monofun_Isfst RS ch2ch_monofun) 1), |
108 (etac (monofun_Isfst RS ch2ch_monofun) 1), |
242 (rtac is_ub_thelub 1), |
109 (rtac is_ub_thelub 1), |