author | lcp |
Thu, 06 Apr 1995 11:49:42 +0200 | |
changeset 246 | 0f9230a24164 |
parent 202 | c533bc92e882 |
permissions | -rw-r--r-- |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
1 |
(* Title: HOL/Sum.ML |
0 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1991 University of Cambridge |
|
5 |
||
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
6 |
For Sum.thy. The disjoint sum of two types |
0 | 7 |
*) |
8 |
||
9 |
open Sum; |
|
10 |
||
11 |
(** Inl_Rep and Inr_Rep: Representations of the constructors **) |
|
12 |
||
13 |
(*This counts as a non-emptiness result for admitting 'a+'b as a type*) |
|
14 |
goalw Sum.thy [Sum_def] "Inl_Rep(a) : Sum"; |
|
15 |
by (EVERY1 [rtac CollectI, rtac disjI1, rtac exI, rtac refl]); |
|
171 | 16 |
qed "Inl_RepI"; |
0 | 17 |
|
18 |
goalw Sum.thy [Sum_def] "Inr_Rep(b) : Sum"; |
|
19 |
by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]); |
|
171 | 20 |
qed "Inr_RepI"; |
0 | 21 |
|
22 |
goal Sum.thy "inj_onto(Abs_Sum,Sum)"; |
|
23 |
by (rtac inj_onto_inverseI 1); |
|
24 |
by (etac Abs_Sum_inverse 1); |
|
171 | 25 |
qed "inj_onto_Abs_Sum"; |
0 | 26 |
|
27 |
(** Distinctness of Inl and Inr **) |
|
28 |
||
5 | 29 |
goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)"; |
0 | 30 |
by (EVERY1 [rtac notI, |
31 |
etac (fun_cong RS fun_cong RS fun_cong RS iffE), |
|
32 |
rtac (notE RS ccontr), etac (mp RS conjunct2), |
|
33 |
REPEAT o (ares_tac [refl,conjI]) ]); |
|
171 | 34 |
qed "Inl_Rep_not_Inr_Rep"; |
0 | 35 |
|
5 | 36 |
goalw Sum.thy [Inl_def,Inr_def] "Inl(a) ~= Inr(b)"; |
0 | 37 |
by (rtac (inj_onto_Abs_Sum RS inj_onto_contraD) 1); |
38 |
by (rtac Inl_Rep_not_Inr_Rep 1); |
|
39 |
by (rtac Inl_RepI 1); |
|
40 |
by (rtac Inr_RepI 1); |
|
171 | 41 |
qed "Inl_not_Inr"; |
0 | 42 |
|
202 | 43 |
bind_thm ("Inl_neq_Inr", (Inl_not_Inr RS notE)); |
0 | 44 |
val Inr_neq_Inl = sym RS Inl_neq_Inr; |
45 |
||
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
46 |
goal Sum.thy "(Inl(a)=Inr(b)) = False"; |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
47 |
by (simp_tac (HOL_ss addsimps [Inl_not_Inr]) 1); |
171 | 48 |
qed "Inl_Inr_eq"; |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
49 |
|
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
50 |
goal Sum.thy "(Inr(b)=Inl(a)) = False"; |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
51 |
by (simp_tac (HOL_ss addsimps [Inl_not_Inr RS not_sym]) 1); |
171 | 52 |
qed "Inr_Inl_eq"; |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
53 |
|
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
54 |
|
0 | 55 |
(** Injectiveness of Inl and Inr **) |
56 |
||
57 |
val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c"; |
|
58 |
by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1); |
|
59 |
by (fast_tac HOL_cs 1); |
|
171 | 60 |
qed "Inl_Rep_inject"; |
0 | 61 |
|
62 |
val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d"; |
|
63 |
by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1); |
|
64 |
by (fast_tac HOL_cs 1); |
|
171 | 65 |
qed "Inr_Rep_inject"; |
0 | 66 |
|
67 |
goalw Sum.thy [Inl_def] "inj(Inl)"; |
|
68 |
by (rtac injI 1); |
|
69 |
by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inl_Rep_inject) 1); |
|
70 |
by (rtac Inl_RepI 1); |
|
71 |
by (rtac Inl_RepI 1); |
|
171 | 72 |
qed "inj_Inl"; |
0 | 73 |
val Inl_inject = inj_Inl RS injD; |
74 |
||
75 |
goalw Sum.thy [Inr_def] "inj(Inr)"; |
|
76 |
by (rtac injI 1); |
|
77 |
by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inr_Rep_inject) 1); |
|
78 |
by (rtac Inr_RepI 1); |
|
79 |
by (rtac Inr_RepI 1); |
|
171 | 80 |
qed "inj_Inr"; |
0 | 81 |
val Inr_inject = inj_Inr RS injD; |
82 |
||
83 |
goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)"; |
|
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
84 |
by (fast_tac (HOL_cs addSEs [Inl_inject]) 1); |
171 | 85 |
qed "Inl_eq"; |
0 | 86 |
|
87 |
goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)"; |
|
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
88 |
by (fast_tac (HOL_cs addSEs [Inr_inject]) 1); |
171 | 89 |
qed "Inr_eq"; |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
90 |
|
117
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
91 |
(*** Rules for the disjoint sum of two SETS ***) |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
92 |
|
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
93 |
(** Introduction rules for the injections **) |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
94 |
|
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
95 |
goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A plus B"; |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
96 |
by (REPEAT (ares_tac [UnI1,imageI] 1)); |
171 | 97 |
qed "InlI"; |
117
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
98 |
|
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
99 |
goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A plus B"; |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
100 |
by (REPEAT (ares_tac [UnI2,imageI] 1)); |
171 | 101 |
qed "InrI"; |
117
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
102 |
|
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
103 |
(** Elimination rules **) |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
104 |
|
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
105 |
val major::prems = goalw Sum.thy [sum_def] |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
106 |
"[| u: A plus B; \ |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
107 |
\ !!x. [| x:A; u=Inl(x) |] ==> P; \ |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
108 |
\ !!y. [| y:B; u=Inr(y) |] ==> P \ |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
109 |
\ |] ==> P"; |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
110 |
by (rtac (major RS UnE) 1); |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
111 |
by (REPEAT (rtac refl 1 |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
112 |
ORELSE eresolve_tac (prems@[imageE,ssubst]) 1)); |
171 | 113 |
qed "plusE"; |
117
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
114 |
|
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
115 |
|
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
116 |
val sum_cs = set_cs addSIs [InlI, InrI] |
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
117 |
addSEs [plusE, Inl_neq_Inr, Inr_neq_Inl] |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
118 |
addSDs [Inl_inject, Inr_inject]; |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
119 |
|
0 | 120 |
|
38 | 121 |
(** sum_case -- the selection operator for sums **) |
0 | 122 |
|
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
123 |
goalw Sum.thy [sum_case_def] "sum_case(f, g, Inl(x)) = f(x)"; |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
124 |
by (fast_tac (sum_cs addIs [select_equality]) 1); |
171 | 125 |
qed "sum_case_Inl"; |
0 | 126 |
|
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
127 |
goalw Sum.thy [sum_case_def] "sum_case(f, g, Inr(x)) = g(x)"; |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
128 |
by (fast_tac (sum_cs addIs [select_equality]) 1); |
171 | 129 |
qed "sum_case_Inr"; |
0 | 130 |
|
131 |
(** Exhaustion rule for sums -- a degenerate form of induction **) |
|
132 |
||
133 |
val prems = goalw Sum.thy [Inl_def,Inr_def] |
|
134 |
"[| !!x::'a. s = Inl(x) ==> P; !!y::'b. s = Inr(y) ==> P \ |
|
135 |
\ |] ==> P"; |
|
136 |
by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1); |
|
137 |
by (REPEAT (eresolve_tac [disjE,exE] 1 |
|
138 |
ORELSE EVERY1 [resolve_tac prems, |
|
139 |
etac subst, |
|
140 |
rtac (Rep_Sum_inverse RS sym)])); |
|
171 | 141 |
qed "sumE"; |
0 | 142 |
|
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
143 |
goal Sum.thy "sum_case(%x::'a. f(Inl(x)), %y::'b. f(Inr(y)), s) = f(s)"; |
0 | 144 |
by (EVERY1 [res_inst_tac [("s","s")] sumE, |
38 | 145 |
etac ssubst, rtac sum_case_Inl, |
146 |
etac ssubst, rtac sum_case_Inr]); |
|
171 | 147 |
qed "surjective_sum"; |
0 | 148 |
|
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
149 |
goal Sum.thy "R(sum_case(f,g,s)) = \ |
0 | 150 |
\ ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))"; |
151 |
by (rtac sumE 1); |
|
152 |
by (etac ssubst 1); |
|
38 | 153 |
by (stac sum_case_Inl 1); |
0 | 154 |
by (fast_tac (set_cs addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1); |
155 |
by (etac ssubst 1); |
|
38 | 156 |
by (stac sum_case_Inr 1); |
0 | 157 |
by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1); |
171 | 158 |
qed "expand_sum_case"; |
0 | 159 |
|
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
160 |
val sum_ss = prod_ss addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq, |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
161 |
sum_case_Inl, sum_case_Inr]; |
2
befa4e9f7c90
Added weak congruence rules to HOL: if_weak_cong, case_weak_cong,
lcp
parents:
0
diff
changeset
|
162 |
|
befa4e9f7c90
Added weak congruence rules to HOL: if_weak_cong, case_weak_cong,
lcp
parents:
0
diff
changeset
|
163 |
(*Prevents simplification of f and g: much faster*) |
179 | 164 |
qed_goal "sum_case_weak_cong" Sum.thy |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
165 |
"s=t ==> sum_case(f,g,s) = sum_case(f,g,t)" |
2
befa4e9f7c90
Added weak congruence rules to HOL: if_weak_cong, case_weak_cong,
lcp
parents:
0
diff
changeset
|
166 |
(fn [prem] => [rtac (prem RS arg_cong) 1]); |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
167 |
|
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
168 |
|
117
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
169 |
|
3716c99fb6a1
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
lcp
parents:
107
diff
changeset
|
170 |
|
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
171 |
(** Rules for the Part primitive **) |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
172 |
|
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
173 |
goalw Sum.thy [Part_def] |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
174 |
"!!a b A h. [| a : A; a=h(b) |] ==> a : Part(A,h)"; |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
175 |
by (fast_tac set_cs 1); |
171 | 176 |
qed "Part_eqI"; |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
177 |
|
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
178 |
val PartI = refl RSN (2,Part_eqI); |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
179 |
|
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
180 |
val major::prems = goalw Sum.thy [Part_def] |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
181 |
"[| a : Part(A,h); !!z. [| a : A; a=h(z) |] ==> P \ |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
182 |
\ |] ==> P"; |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
183 |
by (rtac (major RS IntE) 1); |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
184 |
by (etac CollectE 1); |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
185 |
by (etac exE 1); |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
186 |
by (REPEAT (ares_tac prems 1)); |
171 | 187 |
qed "PartE"; |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
188 |
|
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
189 |
goalw Sum.thy [Part_def] "Part(A,h) <= A"; |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
190 |
by (rtac Int_lower1 1); |
171 | 191 |
qed "Part_subset"; |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
192 |
|
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
193 |
goal Sum.thy "!!A B. A<=B ==> Part(A,h) <= Part(B,h)"; |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
194 |
by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1); |
171 | 195 |
qed "Part_mono"; |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
196 |
|
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
197 |
goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A"; |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
198 |
by (etac IntD1 1); |
171 | 199 |
qed "PartD1"; |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
200 |
|
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
201 |
goal Sum.thy "Part(A,%x.x) = A"; |
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
202 |
by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1); |
171 | 203 |
qed "Part_id"; |
107
960e332d2e70
HOL/Sum: rotated arguments of sum_case; added translation for case macro
lcp
parents:
38
diff
changeset
|
204 |