author | clasohm |
Sun, 24 Apr 1994 11:27:38 +0200 | |
changeset 70 | 9459592608e2 |
parent 38 | 7ef6ba42914b |
permissions | -rw-r--r-- |
0 | 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 |
||
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]) ]); |
|
34 |
val Inl_Rep_not_Inr_Rep = result(); |
|
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); |
|
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 |
||
38 | 88 |
(** sum_case -- the selection operator for sums **) |
0 | 89 |
|
38 | 90 |
goalw Sum.thy [sum_case_def] "sum_case(Inl(x), f, g) = f(x)"; |
0 | 91 |
by (fast_tac (set_cs addIs [select_equality] |
92 |
addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1); |
|
38 | 93 |
val sum_case_Inl = result(); |
0 | 94 |
|
38 | 95 |
goalw Sum.thy [sum_case_def] "sum_case(Inr(x), f, g) = g(x)"; |
0 | 96 |
by (fast_tac (set_cs addIs [select_equality] |
97 |
addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1); |
|
38 | 98 |
val sum_case_Inr = result(); |
0 | 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 |
||
38 | 112 |
goal Sum.thy "sum_case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)"; |
0 | 113 |
by (EVERY1 [res_inst_tac [("s","s")] sumE, |
38 | 114 |
etac ssubst, rtac sum_case_Inl, |
115 |
etac ssubst, rtac sum_case_Inr]); |
|
0 | 116 |
val surjective_sum = result(); |
117 |
||
38 | 118 |
goal Sum.thy "R(sum_case(s,f,g)) = \ |
0 | 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); |
|
38 | 122 |
by (stac sum_case_Inl 1); |
0 | 123 |
by (fast_tac (set_cs addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1); |
124 |
by (etac ssubst 1); |
|
38 | 125 |
by (stac sum_case_Inr 1); |
0 | 126 |
by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1); |
38 | 127 |
val expand_sum_case = result(); |
0 | 128 |
|
38 | 129 |
val sum_ss = pair_ss addsimps [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
|
130 |
|
befa4e9f7c90
Added weak congruence rules to HOL: if_weak_cong, case_weak_cong,
lcp
parents:
0
diff
changeset
|
131 |
(*Prevents simplification of f and g: much faster*) |
38 | 132 |
val sum_case_weak_cong = prove_goal Sum.thy |
133 |
"s=t ==> sum_case(s,f,g) = sum_case(t,f,g)" |
|
2
befa4e9f7c90
Added weak congruence rules to HOL: if_weak_cong, case_weak_cong,
lcp
parents:
0
diff
changeset
|
134 |
(fn [prem] => [rtac (prem RS arg_cong) 1]); |