|
1 (* Title: HOL/sum |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 For sum.ML. The disjoint sum of two types |
|
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]); |
|
16 val Inl_RepI = result(); |
|
17 |
|
18 goalw Sum.thy [Sum_def] "Inr_Rep(b) : Sum"; |
|
19 by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]); |
|
20 val Inr_RepI = result(); |
|
21 |
|
22 goal Sum.thy "inj_onto(Abs_Sum,Sum)"; |
|
23 by (rtac inj_onto_inverseI 1); |
|
24 by (etac Abs_Sum_inverse 1); |
|
25 val inj_onto_Abs_Sum = result(); |
|
26 |
|
27 (** Distinctness of Inl and Inr **) |
|
28 |
|
29 goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "~ (Inl_Rep(a) = Inr_Rep(b))"; |
|
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]) ]); |
|
34 val Inl_Rep_not_Inr_Rep = result(); |
|
35 |
|
36 goalw Sum.thy [Inl_def,Inr_def] "~ Inl(a)=Inr(b)"; |
|
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); |
|
41 val Inl_not_Inr = result(); |
|
42 |
|
43 val Inl_neq_Inr = standard (Inl_not_Inr RS notE); |
|
44 val Inr_neq_Inl = sym RS Inl_neq_Inr; |
|
45 |
|
46 (** Injectiveness of Inl and Inr **) |
|
47 |
|
48 val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c"; |
|
49 by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1); |
|
50 by (fast_tac HOL_cs 1); |
|
51 val Inl_Rep_inject = result(); |
|
52 |
|
53 val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d"; |
|
54 by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1); |
|
55 by (fast_tac HOL_cs 1); |
|
56 val Inr_Rep_inject = result(); |
|
57 |
|
58 goalw Sum.thy [Inl_def] "inj(Inl)"; |
|
59 by (rtac injI 1); |
|
60 by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inl_Rep_inject) 1); |
|
61 by (rtac Inl_RepI 1); |
|
62 by (rtac Inl_RepI 1); |
|
63 val inj_Inl = result(); |
|
64 val Inl_inject = inj_Inl RS injD; |
|
65 |
|
66 goalw Sum.thy [Inr_def] "inj(Inr)"; |
|
67 by (rtac injI 1); |
|
68 by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inr_Rep_inject) 1); |
|
69 by (rtac Inr_RepI 1); |
|
70 by (rtac Inr_RepI 1); |
|
71 val inj_Inr = result(); |
|
72 val Inr_inject = inj_Inr RS injD; |
|
73 |
|
74 goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)"; |
|
75 br iffI 1; |
|
76 be (rewrite_rule [inj_def] Inl_inject) 1; |
|
77 be ssubst 1; |
|
78 br refl 1; |
|
79 val Inl_inj = result(); |
|
80 |
|
81 goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)"; |
|
82 br iffI 1; |
|
83 be (rewrite_rule [inj_def] Inr_inject) 1; |
|
84 be ssubst 1; |
|
85 br refl 1; |
|
86 val Inr_inj = result(); |
|
87 |
|
88 (** case -- the selection operator for sums **) |
|
89 |
|
90 goalw Sum.thy [case_def] "case(Inl(x), f, g) = f(x)"; |
|
91 by (fast_tac (set_cs addIs [select_equality] |
|
92 addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1); |
|
93 val case_Inl = result(); |
|
94 |
|
95 goalw Sum.thy [case_def] "case(Inr(x), f, g) = g(x)"; |
|
96 by (fast_tac (set_cs addIs [select_equality] |
|
97 addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1); |
|
98 val case_Inr = result(); |
|
99 |
|
100 (** Exhaustion rule for sums -- a degenerate form of induction **) |
|
101 |
|
102 val prems = goalw Sum.thy [Inl_def,Inr_def] |
|
103 "[| !!x::'a. s = Inl(x) ==> P; !!y::'b. s = Inr(y) ==> P \ |
|
104 \ |] ==> P"; |
|
105 by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1); |
|
106 by (REPEAT (eresolve_tac [disjE,exE] 1 |
|
107 ORELSE EVERY1 [resolve_tac prems, |
|
108 etac subst, |
|
109 rtac (Rep_Sum_inverse RS sym)])); |
|
110 val sumE = result(); |
|
111 |
|
112 goal Sum.thy "case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)"; |
|
113 by (EVERY1 [res_inst_tac [("s","s")] sumE, |
|
114 etac ssubst, rtac case_Inl, |
|
115 etac ssubst, rtac case_Inr]); |
|
116 val surjective_sum = result(); |
|
117 |
|
118 goal Sum.thy "R(case(s,f,g)) = \ |
|
119 \ ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))"; |
|
120 by (rtac sumE 1); |
|
121 by (etac ssubst 1); |
|
122 by (stac case_Inl 1); |
|
123 by (fast_tac (set_cs addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1); |
|
124 by (etac ssubst 1); |
|
125 by (stac case_Inr 1); |
|
126 by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1); |
|
127 val expand_case = result(); |
|
128 |
|
129 (*FIXME: case's congruence rule only should simplifies the first argument*) |
|
130 val sum_ss = pair_ss addsimps [case_Inl, case_Inr]; |