author  clasohm 
Tue, 30 Jan 1996 15:24:36 +0100  
changeset 1465  5d7a7e439cec 
parent 1264  3eb91524b938 
child 1515  4ed79ebab64d 
permissions  rwrr 
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 

6 
For Sum.thy. 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 nonemptiness 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 
qed "Inl_RepI"; 

17 

18 
goalw Sum.thy [Sum_def] "Inr_Rep(b) : Sum"; 

19 
by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]); 

20 
qed "Inr_RepI"; 

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 
qed "inj_onto_Abs_Sum"; 

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, 

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 

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 
qed "Inl_not_Inr"; 

42 

43 
bind_thm ("Inl_neq_Inr", (Inl_not_Inr RS notE)); 

44 
val Inr_neq_Inl = sym RS Inl_neq_Inr; 

45 

46 
goal Sum.thy "(Inl(a)=Inr(b)) = False"; 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1188
diff
changeset

47 
by (simp_tac (!simpset addsimps [Inl_not_Inr]) 1); 
923  48 
qed "Inl_Inr_eq"; 
49 

50 
goal Sum.thy "(Inr(b)=Inl(a)) = False"; 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1188
diff
changeset

51 
by (simp_tac (!simpset addsimps [Inl_not_Inr RS not_sym]) 1); 
923  52 
qed "Inr_Inl_eq"; 
53 

54 

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); 

60 
qed "Inl_Rep_inject"; 

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); 

65 
qed "Inr_Rep_inject"; 

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); 

72 
qed "inj_Inl"; 

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); 

80 
qed "inj_Inr"; 

81 
val Inr_inject = inj_Inr RS injD; 

82 

83 
goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)"; 

84 
by (fast_tac (HOL_cs addSEs [Inl_inject]) 1); 

85 
qed "Inl_eq"; 

86 

87 
goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)"; 

88 
by (fast_tac (HOL_cs addSEs [Inr_inject]) 1); 

89 
qed "Inr_eq"; 

90 

91 
(*** Rules for the disjoint sum of two SETS ***) 

92 

93 
(** Introduction rules for the injections **) 

94 

95 
goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A plus B"; 

96 
by (REPEAT (ares_tac [UnI1,imageI] 1)); 

97 
qed "InlI"; 

98 

99 
goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A plus B"; 

100 
by (REPEAT (ares_tac [UnI2,imageI] 1)); 

101 
qed "InrI"; 

102 

103 
(** Elimination rules **) 

104 

105 
val major::prems = goalw Sum.thy [sum_def] 

106 
"[ u: A plus B; \ 

107 
\ !!x. [ x:A; u=Inl(x) ] ==> P; \ 

108 
\ !!y. [ y:B; u=Inr(y) ] ==> P \ 

109 
\ ] ==> P"; 

110 
by (rtac (major RS UnE) 1); 

111 
by (REPEAT (rtac refl 1 

112 
ORELSE eresolve_tac (prems@[imageE,ssubst]) 1)); 

113 
qed "plusE"; 

114 

115 

116 
val sum_cs = set_cs addSIs [InlI, InrI] 

117 
addSEs [plusE, Inl_neq_Inr, Inr_neq_Inl] 

118 
addSDs [Inl_inject, Inr_inject]; 

119 

120 

121 
(** sum_case  the selection operator for sums **) 

122 

123 
goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)"; 

124 
by (fast_tac (sum_cs addIs [select_equality]) 1); 

125 
qed "sum_case_Inl"; 

126 

127 
goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)"; 

128 
by (fast_tac (sum_cs addIs [select_equality]) 1); 

129 
qed "sum_case_Inr"; 

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, 

1465  139 
etac subst, 
140 
rtac (Rep_Sum_inverse RS sym)])); 

923  141 
qed "sumE"; 
142 

143 
goal Sum.thy "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; 

144 
by (EVERY1 [res_inst_tac [("s","s")] sumE, 

1465  145 
etac ssubst, rtac sum_case_Inl, 
146 
etac ssubst, rtac sum_case_Inr]); 

923  147 
qed "surjective_sum"; 
148 

149 
goal Sum.thy "R(sum_case f g s) = \ 

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); 

153 
by (stac sum_case_Inl 1); 

154 
by (fast_tac (set_cs addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1); 

155 
by (etac ssubst 1); 

156 
by (stac sum_case_Inr 1); 

157 
by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1); 

158 
qed "expand_sum_case"; 

159 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1188
diff
changeset

160 
Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq, sum_case_Inl, sum_case_Inr]; 
923  161 

162 
(*Prevents simplification of f and g: much faster*) 

163 
qed_goal "sum_case_weak_cong" Sum.thy 

164 
"s=t ==> sum_case f g s = sum_case f g t" 

165 
(fn [prem] => [rtac (prem RS arg_cong) 1]); 

166 

167 

168 

169 

170 
(** Rules for the Part primitive **) 

171 

172 
goalw Sum.thy [Part_def] 

173 
"!!a b A h. [ a : A; a=h(b) ] ==> a : Part A h"; 

174 
by (fast_tac set_cs 1); 

175 
qed "Part_eqI"; 

176 

177 
val PartI = refl RSN (2,Part_eqI); 

178 

179 
val major::prems = goalw Sum.thy [Part_def] 

180 
"[ a : Part A h; !!z. [ a : A; a=h(z) ] ==> P \ 

181 
\ ] ==> P"; 

182 
by (rtac (major RS IntE) 1); 

183 
by (etac CollectE 1); 

184 
by (etac exE 1); 

185 
by (REPEAT (ares_tac prems 1)); 

186 
qed "PartE"; 

187 

188 
goalw Sum.thy [Part_def] "Part A h <= A"; 

189 
by (rtac Int_lower1 1); 

190 
qed "Part_subset"; 

191 

192 
goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h"; 

193 
by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1); 

194 
qed "Part_mono"; 

195 

196 
goalw Sum.thy [Part_def] "!!a. a : Part A h ==> a : A"; 

197 
by (etac IntD1 1); 

198 
qed "PartD1"; 

199 

200 
goal Sum.thy "Part A (%x.x) = A"; 

201 
by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1); 

202 
qed "Part_id"; 

203 

1188
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset

204 
goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)"; 
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset

205 
by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1); 
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset

206 
qed "Part_Int"; 
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset

207 

0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset

208 
(*For inductive definitions*) 
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset

209 
goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}"; 
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset

210 
by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1); 
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset

211 
qed "Part_Collect"; 