1 (* Title: HOL/Sum.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 The disjoint sum of two types |
|
7 *) |
|
8 |
|
9 (** Inl_Rep and Inr_Rep: Representations of the constructors **) |
|
10 |
|
11 (*This counts as a non-emptiness result for admitting 'a+'b as a type*) |
|
12 Goalw [Sum_def] "Inl_Rep(a) : Sum"; |
|
13 by (EVERY1 [rtac CollectI, rtac disjI1, rtac exI, rtac refl]); |
|
14 qed "Inl_RepI"; |
|
15 |
|
16 Goalw [Sum_def] "Inr_Rep(b) : Sum"; |
|
17 by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]); |
|
18 qed "Inr_RepI"; |
|
19 |
|
20 Goal "inj_on Abs_Sum Sum"; |
|
21 by (rtac inj_on_inverseI 1); |
|
22 by (etac Abs_Sum_inverse 1); |
|
23 qed "inj_on_Abs_Sum"; |
|
24 |
|
25 (** Distinctness of Inl and Inr **) |
|
26 |
|
27 Goalw [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)"; |
|
28 by (EVERY1 [rtac notI, |
|
29 etac (fun_cong RS fun_cong RS fun_cong RS iffE), |
|
30 rtac (notE RS ccontr), etac (mp RS conjunct2), |
|
31 REPEAT o (ares_tac [refl,conjI]) ]); |
|
32 qed "Inl_Rep_not_Inr_Rep"; |
|
33 |
|
34 Goalw [Inl_def,Inr_def] "Inl(a) ~= Inr(b)"; |
|
35 by (rtac (inj_on_Abs_Sum RS inj_on_contraD) 1); |
|
36 by (rtac Inl_Rep_not_Inr_Rep 1); |
|
37 by (rtac Inl_RepI 1); |
|
38 by (rtac Inr_RepI 1); |
|
39 qed "Inl_not_Inr"; |
|
40 |
|
41 bind_thm ("Inr_not_Inl", Inl_not_Inr RS not_sym); |
|
42 |
|
43 AddIffs [Inl_not_Inr, Inr_not_Inl]; |
|
44 |
|
45 bind_thm ("Inl_neq_Inr", Inl_not_Inr RS notE); |
|
46 bind_thm ("Inr_neq_Inl", sym RS Inl_neq_Inr); |
|
47 |
|
48 |
|
49 (** Injectiveness of Inl and Inr **) |
|
50 |
|
51 Goalw [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c"; |
|
52 by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1); |
|
53 by (Blast_tac 1); |
|
54 qed "Inl_Rep_inject"; |
|
55 |
|
56 Goalw [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d"; |
|
57 by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1); |
|
58 by (Blast_tac 1); |
|
59 qed "Inr_Rep_inject"; |
|
60 |
|
61 Goalw [Inl_def] "inj(Inl)"; |
|
62 by (rtac injI 1); |
|
63 by (etac (inj_on_Abs_Sum RS inj_onD RS Inl_Rep_inject) 1); |
|
64 by (rtac Inl_RepI 1); |
|
65 by (rtac Inl_RepI 1); |
|
66 qed "inj_Inl"; |
|
67 bind_thm ("Inl_inject", inj_Inl RS injD); |
|
68 |
|
69 Goalw [Inr_def] "inj(Inr)"; |
|
70 by (rtac injI 1); |
|
71 by (etac (inj_on_Abs_Sum RS inj_onD RS Inr_Rep_inject) 1); |
|
72 by (rtac Inr_RepI 1); |
|
73 by (rtac Inr_RepI 1); |
|
74 qed "inj_Inr"; |
|
75 bind_thm ("Inr_inject", inj_Inr RS injD); |
|
76 |
|
77 Goal "(Inl(x)=Inl(y)) = (x=y)"; |
|
78 by (blast_tac (claset() addSDs [Inl_inject]) 1); |
|
79 qed "Inl_eq"; |
|
80 |
|
81 Goal "(Inr(x)=Inr(y)) = (x=y)"; |
|
82 by (blast_tac (claset() addSDs [Inr_inject]) 1); |
|
83 qed "Inr_eq"; |
|
84 |
|
85 AddIffs [Inl_eq, Inr_eq]; |
|
86 |
|
87 (*** Rules for the disjoint sum of two SETS ***) |
|
88 |
|
89 (** Introduction rules for the injections **) |
|
90 |
|
91 Goalw [sum_def] "a : A ==> Inl(a) : A <+> B"; |
|
92 by (Blast_tac 1); |
|
93 qed "InlI"; |
|
94 |
|
95 Goalw [sum_def] "b : B ==> Inr(b) : A <+> B"; |
|
96 by (Blast_tac 1); |
|
97 qed "InrI"; |
|
98 |
|
99 (** Elimination rules **) |
|
100 |
|
101 val major::prems = Goalw [sum_def] |
|
102 "[| u: A <+> B; \ |
|
103 \ !!x. [| x:A; u=Inl(x) |] ==> P; \ |
|
104 \ !!y. [| y:B; u=Inr(y) |] ==> P \ |
|
105 \ |] ==> P"; |
|
106 by (rtac (major RS UnE) 1); |
|
107 by (REPEAT (rtac refl 1 |
|
108 ORELSE eresolve_tac (prems@[imageE,ssubst]) 1)); |
|
109 qed "PlusE"; |
|
110 |
|
111 |
|
112 AddSIs [InlI, InrI]; |
|
113 AddSEs [PlusE]; |
|
114 |
|
115 |
|
116 (** Exhaustion rule for sums -- a degenerate form of induction **) |
|
117 |
|
118 val prems = Goalw [Inl_def,Inr_def] |
|
119 "[| !!x::'a. s = Inl(x) ==> P; !!y::'b. s = Inr(y) ==> P \ |
|
120 \ |] ==> P"; |
|
121 by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1); |
|
122 by (REPEAT (eresolve_tac [disjE,exE] 1 |
|
123 ORELSE EVERY1 [resolve_tac prems, |
|
124 etac subst, |
|
125 rtac (Rep_Sum_inverse RS sym)])); |
|
126 qed "sumE"; |
|
127 |
|
128 val prems = Goal "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x"; |
|
129 by (res_inst_tac [("s","x")] sumE 1); |
|
130 by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems))); |
|
131 qed "sum_induct"; |
|
132 |
|
133 |
|
134 (** Rules for the Part primitive **) |
|
135 |
|
136 Goalw [Part_def] "[| a : A; a=h(b) |] ==> a : Part A h"; |
|
137 by (Blast_tac 1); |
|
138 qed "Part_eqI"; |
|
139 |
|
140 bind_thm ("PartI", refl RSN (2,Part_eqI)); |
|
141 |
|
142 val major::prems = Goalw [Part_def] |
|
143 "[| a : Part A h; !!z. [| a : A; a=h(z) |] ==> P \ |
|
144 \ |] ==> P"; |
|
145 by (rtac (major RS IntE) 1); |
|
146 by (etac CollectE 1); |
|
147 by (etac exE 1); |
|
148 by (REPEAT (ares_tac prems 1)); |
|
149 qed "PartE"; |
|
150 |
|
151 AddIs [Part_eqI]; |
|
152 AddSEs [PartE]; |
|
153 |
|
154 Goalw [Part_def] "Part A h <= A"; |
|
155 by (rtac Int_lower1 1); |
|
156 qed "Part_subset"; |
|
157 |
|
158 Goal "A<=B ==> Part A h <= Part B h"; |
|
159 by (Blast_tac 1); |
|
160 qed "Part_mono"; |
|
161 |
|
162 val basic_monos = basic_monos @ [Part_mono]; |
|
163 |
|
164 Goalw [Part_def] "a : Part A h ==> a : A"; |
|
165 by (etac IntD1 1); |
|
166 qed "PartD1"; |
|
167 |
|
168 Goal "Part A (%x. x) = A"; |
|
169 by (Blast_tac 1); |
|
170 qed "Part_id"; |
|
171 |
|
172 Goal "Part (A Int B) h = (Part A h) Int (Part B h)"; |
|
173 by (Blast_tac 1); |
|
174 qed "Part_Int"; |
|
175 |
|
176 Goal "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}"; |
|
177 by (Blast_tac 1); |
|
178 qed "Part_Collect"; |
|