1 (* Title: HOLCF/cprod2.ML |
1 (* Title: HOLCF/Cprod2 |
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 cprod2.thy |
6 Class Instance *::(pcpo,pcpo)po |
7 *) |
7 *) |
8 |
8 |
9 open Cprod2; |
9 (* for compatibility with old HOLCF-Version *) |
|
10 val prems = goal thy "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)"; |
|
11 by (fold_goals_tac [less_cprod_def]); |
|
12 by (rtac refl 1); |
|
13 qed "inst_cprod_po"; |
10 |
14 |
11 (* for compatibility with old HOLCF-Version *) |
15 val prems = goalw thy [inst_cprod_po RS eq_reflection] |
12 qed_goal "inst_cprod_po" thy "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)" |
16 "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2"; |
13 (fn prems => |
17 by (cut_facts_tac prems 1); |
14 [ |
18 by (etac conjE 1); |
15 (fold_goals_tac [less_cprod_def]), |
19 by (dtac (fst_conv RS subst) 1); |
16 (rtac refl 1) |
20 by (dtac (fst_conv RS subst) 1); |
17 ]); |
21 by (dtac (fst_conv RS subst) 1); |
18 |
22 by (dtac (snd_conv RS subst) 1); |
19 qed_goalw "less_cprod4c" thy [inst_cprod_po RS eq_reflection] |
23 by (dtac (snd_conv RS subst) 1); |
20 "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2" |
24 by (dtac (snd_conv RS subst) 1); |
21 (fn prems => |
25 by (rtac conjI 1); |
22 [ |
26 by (atac 1); |
23 (cut_facts_tac prems 1), |
27 by (atac 1); |
24 (etac conjE 1), |
28 qed "less_cprod4c"; |
25 (dtac (fst_conv RS subst) 1), |
|
26 (dtac (fst_conv RS subst) 1), |
|
27 (dtac (fst_conv RS subst) 1), |
|
28 (dtac (snd_conv RS subst) 1), |
|
29 (dtac (snd_conv RS subst) 1), |
|
30 (dtac (snd_conv RS subst) 1), |
|
31 (rtac conjI 1), |
|
32 (atac 1), |
|
33 (atac 1) |
|
34 ]); |
|
35 |
29 |
36 (* ------------------------------------------------------------------------ *) |
30 (* ------------------------------------------------------------------------ *) |
37 (* type cprod is pointed *) |
31 (* type cprod is pointed *) |
38 (* ------------------------------------------------------------------------ *) |
32 (* ------------------------------------------------------------------------ *) |
39 |
33 |
40 qed_goal "minimal_cprod" thy "(UU,UU)<<p" |
34 val prems = goal thy "(UU,UU)<<p"; |
41 (fn prems => |
35 by (simp_tac(simpset() addsimps[inst_cprod_po])1); |
42 [ |
36 qed "minimal_cprod"; |
43 (simp_tac(simpset() addsimps[inst_cprod_po])1) |
|
44 ]); |
|
45 |
37 |
46 bind_thm ("UU_cprod_def",minimal_cprod RS minimal2UU RS sym); |
38 bind_thm ("UU_cprod_def",minimal_cprod RS minimal2UU RS sym); |
47 |
39 |
48 qed_goal "least_cprod" thy "? x::'a*'b.!y. x<<y" |
40 val prems = goal thy "? x::'a*'b.!y. x<<y"; |
49 (fn prems => |
41 by (res_inst_tac [("x","(UU,UU)")] exI 1); |
50 [ |
42 by (rtac (minimal_cprod RS allI) 1); |
51 (res_inst_tac [("x","(UU,UU)")] exI 1), |
43 qed "least_cprod"; |
52 (rtac (minimal_cprod RS allI) 1) |
|
53 ]); |
|
54 |
44 |
55 (* ------------------------------------------------------------------------ *) |
45 (* ------------------------------------------------------------------------ *) |
56 (* Pair <_,_> is monotone in both arguments *) |
46 (* Pair <_,_> is monotone in both arguments *) |
57 (* ------------------------------------------------------------------------ *) |
47 (* ------------------------------------------------------------------------ *) |
58 |
48 |
59 qed_goalw "monofun_pair1" thy [monofun] "monofun Pair" |
49 val prems = goalw thy [monofun] "monofun Pair"; |
60 (fn prems => |
50 by (strip_tac 1); |
61 [ |
51 by (rtac (less_fun RS iffD2) 1); |
62 (strip_tac 1), |
52 by (strip_tac 1); |
63 (rtac (less_fun RS iffD2) 1), |
53 by (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1); |
64 (strip_tac 1), |
54 qed "monofun_pair1"; |
65 (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1) |
|
66 ]); |
|
67 |
55 |
68 qed_goalw "monofun_pair2" thy [monofun] "monofun(Pair x)" |
56 val prems = goalw thy [monofun] "monofun(Pair x)"; |
69 (fn prems => |
57 by (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1); |
70 [ |
58 qed "monofun_pair2"; |
71 (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1) |
|
72 ]); |
|
73 |
59 |
74 qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)" |
60 val prems = goal thy "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"; |
75 (fn prems => |
61 by (cut_facts_tac prems 1); |
76 [ |
62 by (rtac trans_less 1); |
77 (cut_facts_tac prems 1), |
63 by (rtac (monofun_pair1 RS monofunE RS spec RS spec RS mp RS (less_fun RS iffD1 RS spec)) 1); |
78 (rtac trans_less 1), |
64 by (rtac (monofun_pair2 RS monofunE RS spec RS spec RS mp) 2); |
79 (rtac (monofun_pair1 RS monofunE RS spec RS spec RS mp RS |
65 by (atac 1); |
80 (less_fun RS iffD1 RS spec)) 1), |
66 by (atac 1); |
81 (rtac (monofun_pair2 RS monofunE RS spec RS spec RS mp) 2), |
67 qed "monofun_pair"; |
82 (atac 1), |
|
83 (atac 1) |
|
84 ]); |
|
85 |
68 |
86 (* ------------------------------------------------------------------------ *) |
69 (* ------------------------------------------------------------------------ *) |
87 (* fst and snd are monotone *) |
70 (* fst and snd are monotone *) |
88 (* ------------------------------------------------------------------------ *) |
71 (* ------------------------------------------------------------------------ *) |
89 |
72 |
90 qed_goalw "monofun_fst" thy [monofun] "monofun fst" |
73 val prems = goalw thy [monofun] "monofun fst"; |
91 (fn prems => |
74 by (strip_tac 1); |
92 [ |
75 by (res_inst_tac [("p","x")] PairE 1); |
93 (strip_tac 1), |
76 by (hyp_subst_tac 1); |
94 (res_inst_tac [("p","x")] PairE 1), |
77 by (res_inst_tac [("p","y")] PairE 1); |
95 (hyp_subst_tac 1), |
78 by (hyp_subst_tac 1); |
96 (res_inst_tac [("p","y")] PairE 1), |
79 by (Asm_simp_tac 1); |
97 (hyp_subst_tac 1), |
80 by (etac (less_cprod4c RS conjunct1) 1); |
98 (Asm_simp_tac 1), |
81 qed "monofun_fst"; |
99 (etac (less_cprod4c RS conjunct1) 1) |
|
100 ]); |
|
101 |
82 |
102 qed_goalw "monofun_snd" thy [monofun] "monofun snd" |
83 val prems = goalw thy [monofun] "monofun snd"; |
103 (fn prems => |
84 by (strip_tac 1); |
104 [ |
85 by (res_inst_tac [("p","x")] PairE 1); |
105 (strip_tac 1), |
86 by (hyp_subst_tac 1); |
106 (res_inst_tac [("p","x")] PairE 1), |
87 by (res_inst_tac [("p","y")] PairE 1); |
107 (hyp_subst_tac 1), |
88 by (hyp_subst_tac 1); |
108 (res_inst_tac [("p","y")] PairE 1), |
89 by (Asm_simp_tac 1); |
109 (hyp_subst_tac 1), |
90 by (etac (less_cprod4c RS conjunct2) 1); |
110 (Asm_simp_tac 1), |
91 qed "monofun_snd"; |
111 (etac (less_cprod4c RS conjunct2) 1) |
|
112 ]); |
|
113 |
92 |
114 (* ------------------------------------------------------------------------ *) |
93 (* ------------------------------------------------------------------------ *) |
115 (* the type 'a * 'b is a cpo *) |
94 (* the type 'a * 'b is a cpo *) |
116 (* ------------------------------------------------------------------------ *) |
95 (* ------------------------------------------------------------------------ *) |
117 |
96 |
118 qed_goal "lub_cprod" thy |
97 val prems = goal thy |
119 "chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))" |
98 "chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"; |
120 (fn prems => |
99 by (cut_facts_tac prems 1); |
121 [ |
100 by (rtac (conjI RS is_lubI) 1); |
122 (cut_facts_tac prems 1), |
101 by (rtac (allI RS ub_rangeI) 1); |
123 (rtac (conjI RS is_lubI) 1), |
102 by (res_inst_tac [("t","S i")] (surjective_pairing RS ssubst) 1); |
124 (rtac (allI RS ub_rangeI) 1), |
103 by (rtac monofun_pair 1); |
125 (res_inst_tac [("t","S i")] (surjective_pairing RS ssubst) 1), |
104 by (rtac is_ub_thelub 1); |
126 (rtac monofun_pair 1), |
105 by (etac (monofun_fst RS ch2ch_monofun) 1); |
127 (rtac is_ub_thelub 1), |
106 by (rtac is_ub_thelub 1); |
128 (etac (monofun_fst RS ch2ch_monofun) 1), |
107 by (etac (monofun_snd RS ch2ch_monofun) 1); |
129 (rtac is_ub_thelub 1), |
108 by (strip_tac 1); |
130 (etac (monofun_snd RS ch2ch_monofun) 1), |
109 by (res_inst_tac [("t","u")] (surjective_pairing RS ssubst) 1); |
131 (strip_tac 1), |
110 by (rtac monofun_pair 1); |
132 (res_inst_tac [("t","u")] (surjective_pairing RS ssubst) 1), |
111 by (rtac is_lub_thelub 1); |
133 (rtac monofun_pair 1), |
112 by (etac (monofun_fst RS ch2ch_monofun) 1); |
134 (rtac is_lub_thelub 1), |
113 by (etac (monofun_fst RS ub2ub_monofun) 1); |
135 (etac (monofun_fst RS ch2ch_monofun) 1), |
114 by (rtac is_lub_thelub 1); |
136 (etac (monofun_fst RS ub2ub_monofun) 1), |
115 by (etac (monofun_snd RS ch2ch_monofun) 1); |
137 (rtac is_lub_thelub 1), |
116 by (etac (monofun_snd RS ub2ub_monofun) 1); |
138 (etac (monofun_snd RS ch2ch_monofun) 1), |
117 qed "lub_cprod"; |
139 (etac (monofun_snd RS ub2ub_monofun) 1) |
|
140 ]); |
|
141 |
118 |
142 bind_thm ("thelub_cprod", lub_cprod RS thelubI); |
119 bind_thm ("thelub_cprod", lub_cprod RS thelubI); |
143 (* |
120 (* |
144 "chain ?S1 ==> |
121 "chain ?S1 ==> |
145 lub (range ?S1) = |
122 lub (range ?S1) = |
146 (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm |
123 (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm |
147 |
124 |
148 *) |
125 *) |
149 |
126 |
150 qed_goal "cpo_cprod" thy "chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x" |
127 val prems = goal thy "chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x"; |
151 (fn prems => |
128 by (cut_facts_tac prems 1); |
152 [ |
129 by (rtac exI 1); |
153 (cut_facts_tac prems 1), |
130 by (etac lub_cprod 1); |
154 (rtac exI 1), |
131 qed "cpo_cprod"; |
155 (etac lub_cprod 1) |
|
156 ]); |
|
157 |
132 |
158 |
133 |