|
1 (* Title: HOLCF/cprod2.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for cprod2.thy |
|
7 *) |
|
8 |
|
9 open Cprod2; |
|
10 |
|
11 val less_cprod3a = prove_goal Cprod2.thy |
|
12 "p1=<UU,UU> ==> p1 << p2" |
|
13 (fn prems => |
|
14 [ |
|
15 (cut_facts_tac prems 1), |
|
16 (rtac (inst_cprod_po RS ssubst) 1), |
|
17 (rtac (less_cprod1b RS ssubst) 1), |
|
18 (hyp_subst_tac 1), |
|
19 (asm_simp_tac pair_ss 1), |
|
20 (rtac conjI 1), |
|
21 (rtac minimal 1), |
|
22 (rtac minimal 1) |
|
23 ]); |
|
24 |
|
25 val less_cprod3b = prove_goal Cprod2.thy |
|
26 "(p1 << p2) = (fst(p1)<<fst(p2) & snd(p1)<<snd(p2))" |
|
27 (fn prems => |
|
28 [ |
|
29 (rtac (inst_cprod_po RS ssubst) 1), |
|
30 (rtac less_cprod1b 1) |
|
31 ]); |
|
32 |
|
33 val less_cprod4a = prove_goal Cprod2.thy |
|
34 "<x1,x2> << <UU,UU> ==> x1=UU & x2=UU" |
|
35 (fn prems => |
|
36 [ |
|
37 (cut_facts_tac prems 1), |
|
38 (rtac less_cprod2a 1), |
|
39 (etac (inst_cprod_po RS subst) 1) |
|
40 ]); |
|
41 |
|
42 val less_cprod4b = prove_goal Cprod2.thy |
|
43 "p << <UU,UU> ==> p = <UU,UU>" |
|
44 (fn prems => |
|
45 [ |
|
46 (cut_facts_tac prems 1), |
|
47 (rtac less_cprod2b 1), |
|
48 (etac (inst_cprod_po RS subst) 1) |
|
49 ]); |
|
50 |
|
51 val less_cprod4c = prove_goal Cprod2.thy |
|
52 " <xa,ya> << <x,y> ==> xa<<x & ya << y" |
|
53 (fn prems => |
|
54 [ |
|
55 (cut_facts_tac prems 1), |
|
56 (rtac less_cprod2c 1), |
|
57 (etac (inst_cprod_po RS subst) 1), |
|
58 (REPEAT (atac 1)) |
|
59 ]); |
|
60 |
|
61 (* ------------------------------------------------------------------------ *) |
|
62 (* type cprod is pointed *) |
|
63 (* ------------------------------------------------------------------------ *) |
|
64 |
|
65 val minimal_cprod = prove_goal Cprod2.thy "<UU,UU><<p" |
|
66 (fn prems => |
|
67 [ |
|
68 (rtac less_cprod3a 1), |
|
69 (rtac refl 1) |
|
70 ]); |
|
71 |
|
72 (* ------------------------------------------------------------------------ *) |
|
73 (* Pair <_,_> is monotone in both arguments *) |
|
74 (* ------------------------------------------------------------------------ *) |
|
75 |
|
76 val monofun_pair1 = prove_goalw Cprod2.thy [monofun] "monofun(Pair)" |
|
77 (fn prems => |
|
78 [ |
|
79 (strip_tac 1), |
|
80 (rtac (less_fun RS iffD2) 1), |
|
81 (strip_tac 1), |
|
82 (rtac (less_cprod3b RS iffD2) 1), |
|
83 (simp_tac pair_ss 1), |
|
84 (asm_simp_tac Cfun_ss 1) |
|
85 ]); |
|
86 |
|
87 val monofun_pair2 = prove_goalw Cprod2.thy [monofun] "monofun(Pair(x))" |
|
88 (fn prems => |
|
89 [ |
|
90 (strip_tac 1), |
|
91 (rtac (less_cprod3b RS iffD2) 1), |
|
92 (simp_tac pair_ss 1), |
|
93 (asm_simp_tac Cfun_ss 1) |
|
94 ]); |
|
95 |
|
96 val monofun_pair = prove_goal Cprod2.thy |
|
97 "[|x1<<x2; y1<<y2|] ==> <x1,y1> << <x2,y2>" |
|
98 (fn prems => |
|
99 [ |
|
100 (cut_facts_tac prems 1), |
|
101 (rtac trans_less 1), |
|
102 (rtac (monofun_pair1 RS monofunE RS spec RS spec RS mp RS |
|
103 (less_fun RS iffD1 RS spec)) 1), |
|
104 (rtac (monofun_pair2 RS monofunE RS spec RS spec RS mp) 2), |
|
105 (atac 1), |
|
106 (atac 1) |
|
107 ]); |
|
108 |
|
109 (* ------------------------------------------------------------------------ *) |
|
110 (* fst and snd are monotone *) |
|
111 (* ------------------------------------------------------------------------ *) |
|
112 |
|
113 val monofun_fst = prove_goalw Cprod2.thy [monofun] "monofun(fst)" |
|
114 (fn prems => |
|
115 [ |
|
116 (strip_tac 1), |
|
117 (res_inst_tac [("p","x")] PairE 1), |
|
118 (hyp_subst_tac 1), |
|
119 (res_inst_tac [("p","y")] PairE 1), |
|
120 (hyp_subst_tac 1), |
|
121 (asm_simp_tac pair_ss 1), |
|
122 (etac (less_cprod4c RS conjunct1) 1) |
|
123 ]); |
|
124 |
|
125 val monofun_snd = prove_goalw Cprod2.thy [monofun] "monofun(snd)" |
|
126 (fn prems => |
|
127 [ |
|
128 (strip_tac 1), |
|
129 (res_inst_tac [("p","x")] PairE 1), |
|
130 (hyp_subst_tac 1), |
|
131 (res_inst_tac [("p","y")] PairE 1), |
|
132 (hyp_subst_tac 1), |
|
133 (asm_simp_tac pair_ss 1), |
|
134 (etac (less_cprod4c RS conjunct2) 1) |
|
135 ]); |
|
136 |
|
137 (* ------------------------------------------------------------------------ *) |
|
138 (* the type 'a * 'b is a cpo *) |
|
139 (* ------------------------------------------------------------------------ *) |
|
140 |
|
141 val lub_cprod = prove_goal Cprod2.thy |
|
142 " is_chain(S) ==> range(S) <<| \ |
|
143 \ < lub(range(%i.fst(S(i)))),lub(range(%i.snd(S(i))))> " |
|
144 (fn prems => |
|
145 [ |
|
146 (cut_facts_tac prems 1), |
|
147 (rtac is_lubI 1), |
|
148 (rtac conjI 1), |
|
149 (rtac ub_rangeI 1), |
|
150 (rtac allI 1), |
|
151 (res_inst_tac [("t","S(i)")] (surjective_pairing RS ssubst) 1), |
|
152 (rtac monofun_pair 1), |
|
153 (rtac is_ub_thelub 1), |
|
154 (etac (monofun_fst RS ch2ch_monofun) 1), |
|
155 (rtac is_ub_thelub 1), |
|
156 (etac (monofun_snd RS ch2ch_monofun) 1), |
|
157 (strip_tac 1), |
|
158 (res_inst_tac [("t","u")] (surjective_pairing RS ssubst) 1), |
|
159 (rtac monofun_pair 1), |
|
160 (rtac is_lub_thelub 1), |
|
161 (etac (monofun_fst RS ch2ch_monofun) 1), |
|
162 (etac (monofun_fst RS ub2ub_monofun) 1), |
|
163 (rtac is_lub_thelub 1), |
|
164 (etac (monofun_snd RS ch2ch_monofun) 1), |
|
165 (etac (monofun_snd RS ub2ub_monofun) 1) |
|
166 ]); |
|
167 |
|
168 val thelub_cprod = (lub_cprod RS thelubI); |
|
169 (* "is_chain(?S1) ==> lub(range(?S1)) = *) |
|
170 (* <lub(range(%i. fst(?S1(i)))), lub(range(%i. snd(?S1(i))))>" *) |
|
171 |
|
172 |
|
173 val cpo_cprod = prove_goal Cprod2.thy |
|
174 "is_chain(S::nat=>'a*'b)==>? x.range(S)<<| x" |
|
175 (fn prems => |
|
176 [ |
|
177 (cut_facts_tac prems 1), |
|
178 (rtac exI 1), |
|
179 (etac lub_cprod 1) |
|
180 ]); |
|
181 |