author  berghofe 
Thu, 23 May 1996 15:15:20 +0200  
changeset 1761  29e08d527ba1 
parent 1760  6f41a494f3b1 
child 1985  84cf16192e03 
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); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

59 
by (Fast_tac 1); 
923  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); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

64 
by (Fast_tac 1); 
923  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)"; 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

84 
by (fast_tac (!claset addSEs [Inl_inject]) 1); 
923  85 
qed "Inl_eq"; 
86 

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

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

88 
by (fast_tac (!claset addSEs [Inr_inject]) 1); 
923  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 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

120 
AddSIs [InlI, InrI]; 
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

121 
AddSEs [plusE, Inl_neq_Inr, Inr_neq_Inl]; 
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

122 
AddSDs [Inl_inject, Inr_inject]; 
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

123 

923  124 

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

126 

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

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

128 
by (fast_tac (!claset addIs [select_equality]) 1); 
923  129 
qed "sum_case_Inl"; 
130 

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

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

132 
by (fast_tac (!claset addIs [select_equality]) 1); 
923  133 
qed "sum_case_Inr"; 
134 

135 
(** Exhaustion rule for sums  a degenerate form of induction **) 

136 

137 
val prems = goalw Sum.thy [Inl_def,Inr_def] 

138 
"[ !!x::'a. s = Inl(x) ==> P; !!y::'b. s = Inr(y) ==> P \ 

139 
\ ] ==> P"; 

140 
by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1); 

141 
by (REPEAT (eresolve_tac [disjE,exE] 1 

142 
ORELSE EVERY1 [resolve_tac prems, 

1465  143 
etac subst, 
144 
rtac (Rep_Sum_inverse RS sym)])); 

923  145 
qed "sumE"; 
146 

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

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

1465  149 
etac ssubst, rtac sum_case_Inl, 
150 
etac ssubst, rtac sum_case_Inr]); 

923  151 
qed "surjective_sum"; 
152 

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

154 
\ ((! x. s = Inl(x) > R(f(x))) & (! y. s = Inr(y) > R(g(y))))"; 

155 
by (rtac sumE 1); 

156 
by (etac ssubst 1); 

157 
by (stac sum_case_Inl 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

158 
by (fast_tac (!claset addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1); 
923  159 
by (etac ssubst 1); 
160 
by (stac sum_case_Inr 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

161 
by (fast_tac (!claset addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1); 
923  162 
qed "expand_sum_case"; 
163 

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

164 
Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq, sum_case_Inl, sum_case_Inr]; 
923  165 

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

167 
qed_goal "sum_case_weak_cong" Sum.thy 

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

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

170 

171 

172 

173 

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

175 

176 
goalw Sum.thy [Part_def] 

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

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

178 
by (Fast_tac 1); 
923  179 
qed "Part_eqI"; 
180 

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

182 

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

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

185 
\ ] ==> P"; 

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

187 
by (etac CollectE 1); 

188 
by (etac exE 1); 

189 
by (REPEAT (ares_tac prems 1)); 

190 
qed "PartE"; 

191 

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

193 
by (rtac Int_lower1 1); 

194 
qed "Part_subset"; 

195 

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

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

197 
by (fast_tac (!claset addSIs [PartI] addSEs [PartE]) 1); 
923  198 
qed "Part_mono"; 
199 

1515  200 
val basic_monos = basic_monos @ [Part_mono]; 
201 

923  202 
goalw Sum.thy [Part_def] "!!a. a : Part A h ==> a : A"; 
203 
by (etac IntD1 1); 

204 
qed "PartD1"; 

205 

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

1761
29e08d527ba1
Removed equalityI from some proofs (because it is now included
berghofe
parents:
1760
diff
changeset

207 
by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1); 
923  208 
qed "Part_id"; 
209 

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

210 
goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)"; 
1761
29e08d527ba1
Removed equalityI from some proofs (because it is now included
berghofe
parents:
1760
diff
changeset

211 
by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 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*) 
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset

215 
goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}"; 
1761
29e08d527ba1
Removed equalityI from some proofs (because it is now included
berghofe
parents:
1760
diff
changeset

216 
by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1); 
1188
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset

217 
qed "Part_Collect"; 