|
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 |