author | wenzelm |
Sun, 29 Nov 1998 13:16:47 +0100 | |
changeset 5989 | 9670dae0143d |
parent 5316 | 7a8975451a89 |
child 7014 | 11ee650edcd2 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Sum.ML |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
923 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
5316 | 6 |
The disjoint sum of two types |
923 | 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*) |
|
5069 | 14 |
Goalw [Sum_def] "Inl_Rep(a) : Sum"; |
923 | 15 |
by (EVERY1 [rtac CollectI, rtac disjI1, rtac exI, rtac refl]); |
16 |
qed "Inl_RepI"; |
|
17 |
||
5069 | 18 |
Goalw [Sum_def] "Inr_Rep(b) : Sum"; |
923 | 19 |
by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]); |
20 |
qed "Inr_RepI"; |
|
21 |
||
5069 | 22 |
Goal "inj_on Abs_Sum Sum"; |
4830 | 23 |
by (rtac inj_on_inverseI 1); |
923 | 24 |
by (etac Abs_Sum_inverse 1); |
4830 | 25 |
qed "inj_on_Abs_Sum"; |
923 | 26 |
|
27 |
(** Distinctness of Inl and Inr **) |
|
28 |
||
5069 | 29 |
Goalw [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)"; |
923 | 30 |
by (EVERY1 [rtac notI, |
1465 | 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]) ]); |
|
923 | 34 |
qed "Inl_Rep_not_Inr_Rep"; |
35 |
||
5069 | 36 |
Goalw [Inl_def,Inr_def] "Inl(a) ~= Inr(b)"; |
4830 | 37 |
by (rtac (inj_on_Abs_Sum RS inj_on_contraD) 1); |
923 | 38 |
by (rtac Inl_Rep_not_Inr_Rep 1); |
39 |
by (rtac Inl_RepI 1); |
|
40 |
by (rtac Inr_RepI 1); |
|
41 |
qed "Inl_not_Inr"; |
|
42 |
||
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset
|
43 |
bind_thm ("Inr_not_Inl", Inl_not_Inr RS not_sym); |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset
|
44 |
|
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset
|
45 |
AddIffs [Inl_not_Inr, Inr_not_Inl]; |
923 | 46 |
|
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset
|
47 |
bind_thm ("Inl_neq_Inr", Inl_not_Inr RS notE); |
923 | 48 |
|
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset
|
49 |
val Inr_neq_Inl = sym RS Inl_neq_Inr; |
923 | 50 |
|
51 |
||
52 |
(** Injectiveness of Inl and Inr **) |
|
53 |
||
5316 | 54 |
Goalw [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c"; |
55 |
by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1); |
|
2891 | 56 |
by (Blast_tac 1); |
923 | 57 |
qed "Inl_Rep_inject"; |
58 |
||
5316 | 59 |
Goalw [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d"; |
60 |
by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1); |
|
2891 | 61 |
by (Blast_tac 1); |
923 | 62 |
qed "Inr_Rep_inject"; |
63 |
||
5069 | 64 |
Goalw [Inl_def] "inj(Inl)"; |
923 | 65 |
by (rtac injI 1); |
4830 | 66 |
by (etac (inj_on_Abs_Sum RS inj_onD RS Inl_Rep_inject) 1); |
923 | 67 |
by (rtac Inl_RepI 1); |
68 |
by (rtac Inl_RepI 1); |
|
69 |
qed "inj_Inl"; |
|
70 |
val Inl_inject = inj_Inl RS injD; |
|
71 |
||
5069 | 72 |
Goalw [Inr_def] "inj(Inr)"; |
923 | 73 |
by (rtac injI 1); |
4830 | 74 |
by (etac (inj_on_Abs_Sum RS inj_onD RS Inr_Rep_inject) 1); |
923 | 75 |
by (rtac Inr_RepI 1); |
76 |
by (rtac Inr_RepI 1); |
|
77 |
qed "inj_Inr"; |
|
78 |
val Inr_inject = inj_Inr RS injD; |
|
79 |
||
5069 | 80 |
Goal "(Inl(x)=Inl(y)) = (x=y)"; |
4089 | 81 |
by (blast_tac (claset() addSDs [Inl_inject]) 1); |
923 | 82 |
qed "Inl_eq"; |
83 |
||
5069 | 84 |
Goal "(Inr(x)=Inr(y)) = (x=y)"; |
4089 | 85 |
by (blast_tac (claset() addSDs [Inr_inject]) 1); |
923 | 86 |
qed "Inr_eq"; |
87 |
||
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset
|
88 |
AddIffs [Inl_eq, Inr_eq]; |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset
|
89 |
|
923 | 90 |
(*** Rules for the disjoint sum of two SETS ***) |
91 |
||
92 |
(** Introduction rules for the injections **) |
|
93 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
94 |
Goalw [sum_def] "a : A ==> Inl(a) : A Plus B"; |
2891 | 95 |
by (Blast_tac 1); |
923 | 96 |
qed "InlI"; |
97 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
98 |
Goalw [sum_def] "b : B ==> Inr(b) : A Plus B"; |
2891 | 99 |
by (Blast_tac 1); |
923 | 100 |
qed "InrI"; |
101 |
||
102 |
(** Elimination rules **) |
|
103 |
||
5316 | 104 |
val major::prems = Goalw [sum_def] |
2212 | 105 |
"[| u: A Plus B; \ |
923 | 106 |
\ !!x. [| x:A; u=Inl(x) |] ==> P; \ |
107 |
\ !!y. [| y:B; u=Inr(y) |] ==> P \ |
|
108 |
\ |] ==> P"; |
|
109 |
by (rtac (major RS UnE) 1); |
|
110 |
by (REPEAT (rtac refl 1 |
|
111 |
ORELSE eresolve_tac (prems@[imageE,ssubst]) 1)); |
|
2212 | 112 |
qed "PlusE"; |
923 | 113 |
|
114 |
||
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
115 |
AddSIs [InlI, InrI]; |
2212 | 116 |
AddSEs [PlusE]; |
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset
|
117 |
|
923 | 118 |
|
119 |
(** sum_case -- the selection operator for sums **) |
|
120 |
||
5069 | 121 |
Goalw [sum_case_def] "sum_case f g (Inl x) = f(x)"; |
4535 | 122 |
by (Blast_tac 1); |
923 | 123 |
qed "sum_case_Inl"; |
124 |
||
5069 | 125 |
Goalw [sum_case_def] "sum_case f g (Inr x) = g(x)"; |
4535 | 126 |
by (Blast_tac 1); |
923 | 127 |
qed "sum_case_Inr"; |
128 |
||
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset
|
129 |
Addsimps [sum_case_Inl, sum_case_Inr]; |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset
|
130 |
|
923 | 131 |
(** Exhaustion rule for sums -- a degenerate form of induction **) |
132 |
||
5316 | 133 |
val prems = Goalw [Inl_def,Inr_def] |
923 | 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, |
|
1465 | 139 |
etac subst, |
140 |
rtac (Rep_Sum_inverse RS sym)])); |
|
923 | 141 |
qed "sumE"; |
142 |
||
5316 | 143 |
val prems = Goal "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x"; |
5183 | 144 |
by (res_inst_tac [("s","x")] sumE 1); |
145 |
by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems))); |
|
146 |
qed "sum_induct"; |
|
147 |
||
5069 | 148 |
Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; |
923 | 149 |
by (EVERY1 [res_inst_tac [("s","s")] sumE, |
1465 | 150 |
etac ssubst, rtac sum_case_Inl, |
151 |
etac ssubst, rtac sum_case_Inr]); |
|
923 | 152 |
qed "surjective_sum"; |
153 |
||
5069 | 154 |
Goal "R(sum_case f g s) = \ |
923 | 155 |
\ ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))"; |
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset
|
156 |
by (res_inst_tac [("s","s")] sumE 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4089
diff
changeset
|
157 |
by Auto_tac; |
4830 | 158 |
qed "split_sum_case"; |
923 | 159 |
|
4988 | 160 |
qed_goal "split_sum_case_asm" Sum.thy "P (sum_case f g s) = \ |
161 |
\ (~((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))" |
|
162 |
(K [stac split_sum_case 1, |
|
163 |
Blast_tac 1]); |
|
164 |
||
923 | 165 |
(*Prevents simplification of f and g: much faster*) |
166 |
qed_goal "sum_case_weak_cong" Sum.thy |
|
167 |
"s=t ==> sum_case f g s = sum_case f g t" |
|
168 |
(fn [prem] => [rtac (prem RS arg_cong) 1]); |
|
169 |
||
170 |
||
171 |
||
172 |
(** Rules for the Part primitive **) |
|
173 |
||
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
174 |
Goalw [Part_def] "[| a : A; a=h(b) |] ==> a : Part A h"; |
2891 | 175 |
by (Blast_tac 1); |
923 | 176 |
qed "Part_eqI"; |
177 |
||
178 |
val PartI = refl RSN (2,Part_eqI); |
|
179 |
||
5316 | 180 |
val major::prems = Goalw [Part_def] |
923 | 181 |
"[| a : Part A h; !!z. [| a : A; a=h(z) |] ==> P \ |
182 |
\ |] ==> P"; |
|
183 |
by (rtac (major RS IntE) 1); |
|
184 |
by (etac CollectE 1); |
|
185 |
by (etac exE 1); |
|
186 |
by (REPEAT (ares_tac prems 1)); |
|
187 |
qed "PartE"; |
|
188 |
||
2891 | 189 |
AddIs [Part_eqI]; |
190 |
AddSEs [PartE]; |
|
191 |
||
5069 | 192 |
Goalw [Part_def] "Part A h <= A"; |
923 | 193 |
by (rtac Int_lower1 1); |
194 |
qed "Part_subset"; |
|
195 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
196 |
Goal "A<=B ==> Part A h <= Part B h"; |
2922 | 197 |
by (Blast_tac 1); |
923 | 198 |
qed "Part_mono"; |
199 |
||
1515 | 200 |
val basic_monos = basic_monos @ [Part_mono]; |
201 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
202 |
Goalw [Part_def] "a : Part A h ==> a : A"; |
923 | 203 |
by (etac IntD1 1); |
204 |
qed "PartD1"; |
|
205 |
||
5069 | 206 |
Goal "Part A (%x. x) = A"; |
2891 | 207 |
by (Blast_tac 1); |
923 | 208 |
qed "Part_id"; |
209 |
||
5069 | 210 |
Goal "Part (A Int B) h = (Part A h) Int (Part B h)"; |
2922 | 211 |
by (Blast_tac 1); |
1188
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset
|
212 |
qed "Part_Int"; |
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset
|
213 |
|
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset
|
214 |
(*For inductive definitions*) |
5069 | 215 |
Goal "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}"; |
2922 | 216 |
by (Blast_tac 1); |
1188
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset
|
217 |
qed "Part_Collect"; |