2278
|
1 |
(* Title: HOLCF/Up1.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Franz Regensburger
|
|
4 |
Copyright 1993 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
open Up1;
|
|
8 |
|
|
9 |
qed_goalw "Exh_Up" Up1.thy [UU_up_def,Iup_def ]
|
|
10 |
"z = UU_up | (? x. z = Iup(x))"
|
|
11 |
(fn prems =>
|
|
12 |
[
|
|
13 |
(rtac (Rep_Up_inverse RS subst) 1),
|
|
14 |
(res_inst_tac [("s","Rep_Up(z)")] sumE 1),
|
|
15 |
(rtac disjI1 1),
|
|
16 |
(res_inst_tac [("f","Abs_Up")] arg_cong 1),
|
|
17 |
(rtac (unique_void2 RS subst) 1),
|
|
18 |
(atac 1),
|
|
19 |
(rtac disjI2 1),
|
|
20 |
(rtac exI 1),
|
|
21 |
(res_inst_tac [("f","Abs_Up")] arg_cong 1),
|
|
22 |
(atac 1)
|
|
23 |
]);
|
|
24 |
|
|
25 |
qed_goal "inj_Abs_Up" Up1.thy "inj(Abs_Up)"
|
|
26 |
(fn prems =>
|
|
27 |
[
|
|
28 |
(rtac inj_inverseI 1),
|
|
29 |
(rtac Abs_Up_inverse 1)
|
|
30 |
]);
|
|
31 |
|
|
32 |
qed_goal "inj_Rep_Up" Up1.thy "inj(Rep_Up)"
|
|
33 |
(fn prems =>
|
|
34 |
[
|
|
35 |
(rtac inj_inverseI 1),
|
|
36 |
(rtac Rep_Up_inverse 1)
|
|
37 |
]);
|
|
38 |
|
|
39 |
qed_goalw "inject_Iup" Up1.thy [Iup_def] "Iup(x)=Iup(y) ==> x=y"
|
|
40 |
(fn prems =>
|
|
41 |
[
|
|
42 |
(cut_facts_tac prems 1),
|
|
43 |
(rtac (inj_Inr RS injD) 1),
|
|
44 |
(rtac (inj_Abs_Up RS injD) 1),
|
|
45 |
(atac 1)
|
|
46 |
]);
|
|
47 |
|
|
48 |
qed_goalw "defined_Iup" Up1.thy [Iup_def,UU_up_def] "Iup(x)~=UU_up"
|
|
49 |
(fn prems =>
|
|
50 |
[
|
|
51 |
(rtac notI 1),
|
|
52 |
(rtac notE 1),
|
|
53 |
(rtac Inl_not_Inr 1),
|
|
54 |
(rtac sym 1),
|
|
55 |
(etac (inj_Abs_Up RS injD) 1)
|
|
56 |
]);
|
|
57 |
|
|
58 |
|
|
59 |
qed_goal "upE" Up1.thy
|
|
60 |
"[| p=UU_up ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
|
|
61 |
(fn prems =>
|
|
62 |
[
|
|
63 |
(rtac (Exh_Up RS disjE) 1),
|
|
64 |
(eresolve_tac prems 1),
|
|
65 |
(etac exE 1),
|
|
66 |
(eresolve_tac prems 1)
|
|
67 |
]);
|
|
68 |
|
|
69 |
qed_goalw "Ifup1" Up1.thy [Ifup_def,UU_up_def]
|
|
70 |
"Ifup(f)(UU_up)=UU"
|
|
71 |
(fn prems =>
|
|
72 |
[
|
|
73 |
(stac Abs_Up_inverse 1),
|
|
74 |
(stac sum_case_Inl 1),
|
|
75 |
(rtac refl 1)
|
|
76 |
]);
|
|
77 |
|
|
78 |
qed_goalw "Ifup2" Up1.thy [Ifup_def,Iup_def]
|
|
79 |
"Ifup(f)(Iup(x))=f`x"
|
|
80 |
(fn prems =>
|
|
81 |
[
|
|
82 |
(stac Abs_Up_inverse 1),
|
|
83 |
(stac sum_case_Inr 1),
|
|
84 |
(rtac refl 1)
|
|
85 |
]);
|
|
86 |
|
|
87 |
val Up0_ss = (simpset_of "Cfun3") addsimps [Ifup1,Ifup2];
|
|
88 |
|
|
89 |
qed_goalw "less_up1a" Up1.thy [less_up_def,UU_up_def]
|
|
90 |
"less_up(UU_up)(z)"
|
|
91 |
(fn prems =>
|
|
92 |
[
|
|
93 |
(stac Abs_Up_inverse 1),
|
|
94 |
(stac sum_case_Inl 1),
|
|
95 |
(rtac TrueI 1)
|
|
96 |
]);
|
|
97 |
|
|
98 |
qed_goalw "less_up1b" Up1.thy [Iup_def,less_up_def,UU_up_def]
|
|
99 |
"~less_up (Iup x) UU_up"
|
|
100 |
(fn prems =>
|
|
101 |
[
|
|
102 |
(rtac notI 1),
|
|
103 |
(rtac iffD1 1),
|
|
104 |
(atac 2),
|
|
105 |
(stac Abs_Up_inverse 1),
|
|
106 |
(stac Abs_Up_inverse 1),
|
|
107 |
(stac sum_case_Inr 1),
|
|
108 |
(stac sum_case_Inl 1),
|
|
109 |
(rtac refl 1)
|
|
110 |
]);
|
|
111 |
|
|
112 |
qed_goalw "less_up1c" Up1.thy [Iup_def,less_up_def,UU_up_def]
|
|
113 |
"less_up (Iup x) (Iup y)=(x<<y)"
|
|
114 |
(fn prems =>
|
|
115 |
[
|
|
116 |
(stac Abs_Up_inverse 1),
|
|
117 |
(stac Abs_Up_inverse 1),
|
|
118 |
(stac sum_case_Inr 1),
|
|
119 |
(stac sum_case_Inr 1),
|
|
120 |
(rtac refl 1)
|
|
121 |
]);
|
|
122 |
|
|
123 |
|
|
124 |
qed_goal "refl_less_up" Up1.thy "less_up p p"
|
|
125 |
(fn prems =>
|
|
126 |
[
|
|
127 |
(res_inst_tac [("p","p")] upE 1),
|
|
128 |
(hyp_subst_tac 1),
|
|
129 |
(rtac less_up1a 1),
|
|
130 |
(hyp_subst_tac 1),
|
|
131 |
(rtac (less_up1c RS iffD2) 1),
|
|
132 |
(rtac refl_less 1)
|
|
133 |
]);
|
|
134 |
|
|
135 |
qed_goal "antisym_less_up" Up1.thy
|
|
136 |
"!!p1. [|less_up p1 p2;less_up p2 p1|] ==> p1=p2"
|
|
137 |
(fn _ =>
|
|
138 |
[
|
|
139 |
(res_inst_tac [("p","p1")] upE 1),
|
|
140 |
(hyp_subst_tac 1),
|
|
141 |
(res_inst_tac [("p","p2")] upE 1),
|
|
142 |
(etac sym 1),
|
|
143 |
(hyp_subst_tac 1),
|
|
144 |
(res_inst_tac [("P","less_up (Iup x) UU_up")] notE 1),
|
|
145 |
(rtac less_up1b 1),
|
|
146 |
(atac 1),
|
|
147 |
(hyp_subst_tac 1),
|
|
148 |
(res_inst_tac [("p","p2")] upE 1),
|
|
149 |
(hyp_subst_tac 1),
|
|
150 |
(res_inst_tac [("P","less_up (Iup x) UU_up")] notE 1),
|
|
151 |
(rtac less_up1b 1),
|
|
152 |
(atac 1),
|
|
153 |
(hyp_subst_tac 1),
|
|
154 |
(rtac arg_cong 1),
|
|
155 |
(rtac antisym_less 1),
|
|
156 |
(etac (less_up1c RS iffD1) 1),
|
|
157 |
(etac (less_up1c RS iffD1) 1)
|
|
158 |
]);
|
|
159 |
|
|
160 |
qed_goal "trans_less_up" Up1.thy
|
|
161 |
"[|less_up p1 p2;less_up p2 p3|] ==> less_up p1 p3"
|
|
162 |
(fn prems =>
|
|
163 |
[
|
|
164 |
(cut_facts_tac prems 1),
|
|
165 |
(res_inst_tac [("p","p1")] upE 1),
|
|
166 |
(hyp_subst_tac 1),
|
|
167 |
(rtac less_up1a 1),
|
|
168 |
(hyp_subst_tac 1),
|
|
169 |
(res_inst_tac [("p","p2")] upE 1),
|
|
170 |
(hyp_subst_tac 1),
|
|
171 |
(rtac notE 1),
|
|
172 |
(rtac less_up1b 1),
|
|
173 |
(atac 1),
|
|
174 |
(hyp_subst_tac 1),
|
|
175 |
(res_inst_tac [("p","p3")] upE 1),
|
|
176 |
(hyp_subst_tac 1),
|
|
177 |
(rtac notE 1),
|
|
178 |
(rtac less_up1b 1),
|
|
179 |
(atac 1),
|
|
180 |
(hyp_subst_tac 1),
|
|
181 |
(rtac (less_up1c RS iffD2) 1),
|
|
182 |
(rtac trans_less 1),
|
|
183 |
(etac (less_up1c RS iffD1) 1),
|
|
184 |
(etac (less_up1c RS iffD1) 1)
|
|
185 |
]);
|
|
186 |
|