author | paulson |
Thu, 08 Jul 1999 13:38:41 +0200 | |
changeset 6915 | 4ab8e31a8421 |
parent 6543 | da7b170fc8a7 |
child 7294 | 5a50de9141b5 |
permissions | -rw-r--r-- |
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 |
||
6543 | 9 |
(*compatibility*) |
10 |
val [sum_case_Inl, sum_case_Inr] = sum.cases; |
|
11 |
||
2640 | 12 |
qed_goal "Abs_Up_inverse2" thy "Rep_Up (Abs_Up y) = y" |
13 |
(fn prems => |
|
14 |
[ |
|
4098 | 15 |
(simp_tac (simpset() addsimps [Up_def,Abs_Up_inverse]) 1) |
2640 | 16 |
]); |
17 |
||
18 |
qed_goalw "Exh_Up" thy [Iup_def ] |
|
19 |
"z = Abs_Up(Inl ()) | (? x. z = Iup x)" |
|
2278 | 20 |
(fn prems => |
21 |
[ |
|
22 |
(rtac (Rep_Up_inverse RS subst) 1), |
|
2640 | 23 |
(res_inst_tac [("s","Rep_Up z")] sumE 1), |
2278 | 24 |
(rtac disjI1 1), |
25 |
(res_inst_tac [("f","Abs_Up")] arg_cong 1), |
|
2640 | 26 |
(rtac (unit_eq RS subst) 1), |
2278 | 27 |
(atac 1), |
28 |
(rtac disjI2 1), |
|
29 |
(rtac exI 1), |
|
30 |
(res_inst_tac [("f","Abs_Up")] arg_cong 1), |
|
31 |
(atac 1) |
|
32 |
]); |
|
33 |
||
2640 | 34 |
qed_goal "inj_Abs_Up" thy "inj(Abs_Up)" |
2278 | 35 |
(fn prems => |
36 |
[ |
|
37 |
(rtac inj_inverseI 1), |
|
2640 | 38 |
(rtac Abs_Up_inverse2 1) |
2278 | 39 |
]); |
40 |
||
2640 | 41 |
qed_goal "inj_Rep_Up" thy "inj(Rep_Up)" |
2278 | 42 |
(fn prems => |
43 |
[ |
|
44 |
(rtac inj_inverseI 1), |
|
45 |
(rtac Rep_Up_inverse 1) |
|
46 |
]); |
|
47 |
||
2640 | 48 |
qed_goalw "inject_Iup" thy [Iup_def] "Iup x=Iup y ==> x=y" |
2278 | 49 |
(fn prems => |
50 |
[ |
|
51 |
(cut_facts_tac prems 1), |
|
52 |
(rtac (inj_Inr RS injD) 1), |
|
53 |
(rtac (inj_Abs_Up RS injD) 1), |
|
54 |
(atac 1) |
|
55 |
]); |
|
56 |
||
2640 | 57 |
qed_goalw "defined_Iup" thy [Iup_def] "Iup x~=Abs_Up(Inl ())" |
2278 | 58 |
(fn prems => |
59 |
[ |
|
60 |
(rtac notI 1), |
|
61 |
(rtac notE 1), |
|
62 |
(rtac Inl_not_Inr 1), |
|
63 |
(rtac sym 1), |
|
64 |
(etac (inj_Abs_Up RS injD) 1) |
|
65 |
]); |
|
66 |
||
67 |
||
2640 | 68 |
qed_goal "upE" thy |
69 |
"[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q" |
|
2278 | 70 |
(fn prems => |
71 |
[ |
|
72 |
(rtac (Exh_Up RS disjE) 1), |
|
73 |
(eresolve_tac prems 1), |
|
74 |
(etac exE 1), |
|
75 |
(eresolve_tac prems 1) |
|
76 |
]); |
|
77 |
||
2640 | 78 |
qed_goalw "Ifup1" thy [Ifup_def] |
79 |
"Ifup(f)(Abs_Up(Inl ()))=UU" |
|
2278 | 80 |
(fn prems => |
81 |
[ |
|
2640 | 82 |
(stac Abs_Up_inverse2 1), |
2278 | 83 |
(stac sum_case_Inl 1), |
84 |
(rtac refl 1) |
|
85 |
]); |
|
86 |
||
2640 | 87 |
qed_goalw "Ifup2" thy [Ifup_def,Iup_def] |
2278 | 88 |
"Ifup(f)(Iup(x))=f`x" |
89 |
(fn prems => |
|
90 |
[ |
|
2640 | 91 |
(stac Abs_Up_inverse2 1), |
2278 | 92 |
(stac sum_case_Inr 1), |
93 |
(rtac refl 1) |
|
94 |
]); |
|
95 |
||
4098 | 96 |
val Up0_ss = (simpset_of Cfun3.thy) addsimps [Ifup1,Ifup2]; |
2278 | 97 |
|
2640 | 98 |
qed_goalw "less_up1a" thy [less_up_def] |
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2640
diff
changeset
|
99 |
"Abs_Up(Inl ())<< z" |
2278 | 100 |
(fn prems => |
101 |
[ |
|
2640 | 102 |
(stac Abs_Up_inverse2 1), |
2278 | 103 |
(stac sum_case_Inl 1), |
104 |
(rtac TrueI 1) |
|
105 |
]); |
|
106 |
||
2640 | 107 |
qed_goalw "less_up1b" thy [Iup_def,less_up_def] |
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2640
diff
changeset
|
108 |
"~(Iup x) << (Abs_Up(Inl ()))" |
2278 | 109 |
(fn prems => |
110 |
[ |
|
111 |
(rtac notI 1), |
|
112 |
(rtac iffD1 1), |
|
113 |
(atac 2), |
|
2640 | 114 |
(stac Abs_Up_inverse2 1), |
115 |
(stac Abs_Up_inverse2 1), |
|
2278 | 116 |
(stac sum_case_Inr 1), |
117 |
(stac sum_case_Inl 1), |
|
118 |
(rtac refl 1) |
|
119 |
]); |
|
120 |
||
2640 | 121 |
qed_goalw "less_up1c" thy [Iup_def,less_up_def] |
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2640
diff
changeset
|
122 |
" (Iup x) << (Iup y)=(x<<y)" |
2278 | 123 |
(fn prems => |
124 |
[ |
|
2640 | 125 |
(stac Abs_Up_inverse2 1), |
126 |
(stac Abs_Up_inverse2 1), |
|
2278 | 127 |
(stac sum_case_Inr 1), |
128 |
(stac sum_case_Inr 1), |
|
129 |
(rtac refl 1) |
|
130 |
]); |
|
131 |
||
132 |
||
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2640
diff
changeset
|
133 |
qed_goal "refl_less_up" thy "(p::'a u) << p" |
2278 | 134 |
(fn prems => |
135 |
[ |
|
136 |
(res_inst_tac [("p","p")] upE 1), |
|
137 |
(hyp_subst_tac 1), |
|
138 |
(rtac less_up1a 1), |
|
139 |
(hyp_subst_tac 1), |
|
140 |
(rtac (less_up1c RS iffD2) 1), |
|
141 |
(rtac refl_less 1) |
|
142 |
]); |
|
143 |
||
2640 | 144 |
qed_goal "antisym_less_up" thy |
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2640
diff
changeset
|
145 |
"!!p1.[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2" |
2278 | 146 |
(fn _ => |
147 |
[ |
|
148 |
(res_inst_tac [("p","p1")] upE 1), |
|
149 |
(hyp_subst_tac 1), |
|
150 |
(res_inst_tac [("p","p2")] upE 1), |
|
151 |
(etac sym 1), |
|
152 |
(hyp_subst_tac 1), |
|
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2640
diff
changeset
|
153 |
(res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1), |
2278 | 154 |
(rtac less_up1b 1), |
155 |
(atac 1), |
|
156 |
(hyp_subst_tac 1), |
|
157 |
(res_inst_tac [("p","p2")] upE 1), |
|
158 |
(hyp_subst_tac 1), |
|
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2640
diff
changeset
|
159 |
(res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1), |
2278 | 160 |
(rtac less_up1b 1), |
161 |
(atac 1), |
|
162 |
(hyp_subst_tac 1), |
|
163 |
(rtac arg_cong 1), |
|
164 |
(rtac antisym_less 1), |
|
165 |
(etac (less_up1c RS iffD1) 1), |
|
166 |
(etac (less_up1c RS iffD1) 1) |
|
167 |
]); |
|
168 |
||
2640 | 169 |
qed_goal "trans_less_up" thy |
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2640
diff
changeset
|
170 |
"[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3" |
2278 | 171 |
(fn prems => |
172 |
[ |
|
173 |
(cut_facts_tac prems 1), |
|
174 |
(res_inst_tac [("p","p1")] upE 1), |
|
175 |
(hyp_subst_tac 1), |
|
176 |
(rtac less_up1a 1), |
|
177 |
(hyp_subst_tac 1), |
|
178 |
(res_inst_tac [("p","p2")] upE 1), |
|
179 |
(hyp_subst_tac 1), |
|
180 |
(rtac notE 1), |
|
181 |
(rtac less_up1b 1), |
|
182 |
(atac 1), |
|
183 |
(hyp_subst_tac 1), |
|
184 |
(res_inst_tac [("p","p3")] upE 1), |
|
185 |
(hyp_subst_tac 1), |
|
186 |
(rtac notE 1), |
|
187 |
(rtac less_up1b 1), |
|
188 |
(atac 1), |
|
189 |
(hyp_subst_tac 1), |
|
190 |
(rtac (less_up1c RS iffD2) 1), |
|
191 |
(rtac trans_less 1), |
|
192 |
(etac (less_up1c RS iffD1) 1), |
|
193 |
(etac (less_up1c RS iffD1) 1) |
|
194 |
]); |
|
195 |