author  paulson 
Thu, 12 Sep 1996 10:40:05 +0200  
changeset 1985  84cf16192e03 
parent 1761  29e08d527ba1 
child 2212  bd705e9de196 
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 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

43 
bind_thm ("Inr_not_Inl", Inl_not_Inr RS not_sym); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

44 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

45 
AddIffs [Inl_not_Inr, Inr_not_Inl]; 
923  46 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

47 
bind_thm ("Inl_neq_Inr", Inl_not_Inr RS notE); 
923  48 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

49 
val Inr_neq_Inl = sym RS Inl_neq_Inr; 
923  50 

51 

52 
(** Injectiveness of Inl and Inr **) 

53 

54 
val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c"; 

55 
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

56 
by (Fast_tac 1); 
923  57 
qed "Inl_Rep_inject"; 
58 

59 
val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d"; 

60 
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

61 
by (Fast_tac 1); 
923  62 
qed "Inr_Rep_inject"; 
63 

64 
goalw Sum.thy [Inl_def] "inj(Inl)"; 

65 
by (rtac injI 1); 

66 
by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inl_Rep_inject) 1); 

67 
by (rtac Inl_RepI 1); 

68 
by (rtac Inl_RepI 1); 

69 
qed "inj_Inl"; 

70 
val Inl_inject = inj_Inl RS injD; 

71 

72 
goalw Sum.thy [Inr_def] "inj(Inr)"; 

73 
by (rtac injI 1); 

74 
by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inr_Rep_inject) 1); 

75 
by (rtac Inr_RepI 1); 

76 
by (rtac Inr_RepI 1); 

77 
qed "inj_Inr"; 

78 
val Inr_inject = inj_Inr RS injD; 

79 

80 
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

81 
by (fast_tac (!claset addSEs [Inl_inject]) 1); 
923  82 
qed "Inl_eq"; 
83 

84 
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

85 
by (fast_tac (!claset addSEs [Inr_inject]) 1); 
923  86 
qed "Inr_eq"; 
87 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

88 
AddIffs [Inl_eq, Inr_eq]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

89 

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

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

93 

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

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

95 
by (Fast_tac 1); 
923  96 
qed "InlI"; 
97 

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

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

99 
by (Fast_tac 1); 
923  100 
qed "InrI"; 
101 

102 
(** Elimination rules **) 

103 

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

105 
"[ u: A plus B; \ 

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

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

108 
\ ] ==> P"; 

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

110 
by (REPEAT (rtac refl 1 

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

112 
qed "plusE"; 

113 

114 

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

115 
AddSIs [InlI, InrI]; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

116 
AddSEs [plusE]; 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

117 

923  118 

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

120 

121 
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

122 
by (fast_tac (!claset addIs [select_equality]) 1); 
923  123 
qed "sum_case_Inl"; 
124 

125 
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

126 
by (fast_tac (!claset addIs [select_equality]) 1); 
923  127 
qed "sum_case_Inr"; 
128 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

129 
Addsimps [sum_case_Inl, sum_case_Inr]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

130 

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

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

151 
by (res_inst_tac [("s","s")] sumE 1); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1761
diff
changeset

152 
by (Auto_tac()); 
923  153 
qed "expand_sum_case"; 
154 

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

156 
qed_goal "sum_case_weak_cong" Sum.thy 

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

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

159 

160 

161 

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

163 

164 
goalw Sum.thy [Part_def] 

165 
"!!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

166 
by (Fast_tac 1); 
923  167 
qed "Part_eqI"; 
168 

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

170 

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

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

173 
\ ] ==> P"; 

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

175 
by (etac CollectE 1); 

176 
by (etac exE 1); 

177 
by (REPEAT (ares_tac prems 1)); 

178 
qed "PartE"; 

179 

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

181 
by (rtac Int_lower1 1); 

182 
qed "Part_subset"; 

183 

184 
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

185 
by (fast_tac (!claset addSIs [PartI] addSEs [PartE]) 1); 
923  186 
qed "Part_mono"; 
187 

1515  188 
val basic_monos = basic_monos @ [Part_mono]; 
189 

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

192 
qed "PartD1"; 

193 

194 
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

195 
by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1); 
923  196 
qed "Part_id"; 
197 

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

198 
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

199 
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

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

201 

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

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

203 
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

204 
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

205 
qed "Part_Collect"; 