author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9311  ab5b24cbaa16 
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 

5316  6 
The disjoint sum of two types 
923  7 
*) 
8 

9 
(** Inl_Rep and Inr_Rep: Representations of the constructors **) 

10 

11 
(*This counts as a nonemptiness result for admitting 'a+'b as a type*) 

5069  12 
Goalw [Sum_def] "Inl_Rep(a) : Sum"; 
923  13 
by (EVERY1 [rtac CollectI, rtac disjI1, rtac exI, rtac refl]); 
14 
qed "Inl_RepI"; 

15 

5069  16 
Goalw [Sum_def] "Inr_Rep(b) : Sum"; 
923  17 
by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]); 
18 
qed "Inr_RepI"; 

19 

5069  20 
Goal "inj_on Abs_Sum Sum"; 
4830  21 
by (rtac inj_on_inverseI 1); 
923  22 
by (etac Abs_Sum_inverse 1); 
4830  23 
qed "inj_on_Abs_Sum"; 
923  24 

25 
(** Distinctness of Inl and Inr **) 

26 

5069  27 
Goalw [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)"; 
923  28 
by (EVERY1 [rtac notI, 
1465  29 
etac (fun_cong RS fun_cong RS fun_cong RS iffE), 
30 
rtac (notE RS ccontr), etac (mp RS conjunct2), 

31 
REPEAT o (ares_tac [refl,conjI]) ]); 

923  32 
qed "Inl_Rep_not_Inr_Rep"; 
33 

5069  34 
Goalw [Inl_def,Inr_def] "Inl(a) ~= Inr(b)"; 
4830  35 
by (rtac (inj_on_Abs_Sum RS inj_on_contraD) 1); 
923  36 
by (rtac Inl_Rep_not_Inr_Rep 1); 
37 
by (rtac Inl_RepI 1); 

38 
by (rtac Inr_RepI 1); 

39 
qed "Inl_not_Inr"; 

40 

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

41 
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

42 

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

43 
AddIffs [Inl_not_Inr, Inr_not_Inl]; 
923  44 

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

45 
bind_thm ("Inl_neq_Inr", Inl_not_Inr RS notE); 
9108  46 
bind_thm ("Inr_neq_Inl", sym RS Inl_neq_Inr); 
923  47 

48 

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

50 

5316  51 
Goalw [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c"; 
52 
by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1); 

2891  53 
by (Blast_tac 1); 
923  54 
qed "Inl_Rep_inject"; 
55 

5316  56 
Goalw [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d"; 
57 
by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1); 

2891  58 
by (Blast_tac 1); 
923  59 
qed "Inr_Rep_inject"; 
60 

5069  61 
Goalw [Inl_def] "inj(Inl)"; 
923  62 
by (rtac injI 1); 
4830  63 
by (etac (inj_on_Abs_Sum RS inj_onD RS Inl_Rep_inject) 1); 
923  64 
by (rtac Inl_RepI 1); 
65 
by (rtac Inl_RepI 1); 

66 
qed "inj_Inl"; 

9108  67 
bind_thm ("Inl_inject", inj_Inl RS injD); 
923  68 

5069  69 
Goalw [Inr_def] "inj(Inr)"; 
923  70 
by (rtac injI 1); 
4830  71 
by (etac (inj_on_Abs_Sum RS inj_onD RS Inr_Rep_inject) 1); 
923  72 
by (rtac Inr_RepI 1); 
73 
by (rtac Inr_RepI 1); 

74 
qed "inj_Inr"; 

9108  75 
bind_thm ("Inr_inject", inj_Inr RS injD); 
923  76 

5069  77 
Goal "(Inl(x)=Inl(y)) = (x=y)"; 
4089  78 
by (blast_tac (claset() addSDs [Inl_inject]) 1); 
923  79 
qed "Inl_eq"; 
80 

5069  81 
Goal "(Inr(x)=Inr(y)) = (x=y)"; 
4089  82 
by (blast_tac (claset() addSDs [Inr_inject]) 1); 
923  83 
qed "Inr_eq"; 
84 

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

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

86 

923  87 
(*** Rules for the disjoint sum of two SETS ***) 
88 

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

90 

9311  91 
Goalw [sum_def] "a : A ==> Inl(a) : A <+> B"; 
2891  92 
by (Blast_tac 1); 
923  93 
qed "InlI"; 
94 

9311  95 
Goalw [sum_def] "b : B ==> Inr(b) : A <+> B"; 
2891  96 
by (Blast_tac 1); 
923  97 
qed "InrI"; 
98 

99 
(** Elimination rules **) 

100 

5316  101 
val major::prems = Goalw [sum_def] 
9311  102 
"[ u: A <+> B; \ 
923  103 
\ !!x. [ x:A; u=Inl(x) ] ==> P; \ 
104 
\ !!y. [ y:B; u=Inr(y) ] ==> P \ 

105 
\ ] ==> P"; 

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

107 
by (REPEAT (rtac refl 1 

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

2212  109 
qed "PlusE"; 
923  110 

111 

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

112 
AddSIs [InlI, InrI]; 
2212  113 
AddSEs [PlusE]; 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1515
diff
changeset

114 

923  115 

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

117 

5316  118 
val prems = Goalw [Inl_def,Inr_def] 
923  119 
"[ !!x::'a. s = Inl(x) ==> P; !!y::'b. s = Inr(y) ==> P \ 
120 
\ ] ==> P"; 

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

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

123 
ORELSE EVERY1 [resolve_tac prems, 

1465  124 
etac subst, 
125 
rtac (Rep_Sum_inverse RS sym)])); 

923  126 
qed "sumE"; 
127 

5316  128 
val prems = Goal "[ !!x. P (Inl x); !!x. P (Inr x) ] ==> P x"; 
5183  129 
by (res_inst_tac [("s","x")] sumE 1); 
130 
by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems))); 

131 
qed "sum_induct"; 

132 

923  133 

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

135 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

136 
Goalw [Part_def] "[ a : A; a=h(b) ] ==> a : Part A h"; 
2891  137 
by (Blast_tac 1); 
923  138 
qed "Part_eqI"; 
139 

9108  140 
bind_thm ("PartI", refl RSN (2,Part_eqI)); 
923  141 

5316  142 
val major::prems = Goalw [Part_def] 
923  143 
"[ a : Part A h; !!z. [ a : A; a=h(z) ] ==> P \ 
144 
\ ] ==> P"; 

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

146 
by (etac CollectE 1); 

147 
by (etac exE 1); 

148 
by (REPEAT (ares_tac prems 1)); 

149 
qed "PartE"; 

150 

2891  151 
AddIs [Part_eqI]; 
152 
AddSEs [PartE]; 

153 

5069  154 
Goalw [Part_def] "Part A h <= A"; 
923  155 
by (rtac Int_lower1 1); 
156 
qed "Part_subset"; 

157 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

158 
Goal "A<=B ==> Part A h <= Part B h"; 
2922  159 
by (Blast_tac 1); 
923  160 
qed "Part_mono"; 
161 

1515  162 
val basic_monos = basic_monos @ [Part_mono]; 
163 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

164 
Goalw [Part_def] "a : Part A h ==> a : A"; 
923  165 
by (etac IntD1 1); 
166 
qed "PartD1"; 

167 

5069  168 
Goal "Part A (%x. x) = A"; 
2891  169 
by (Blast_tac 1); 
923  170 
qed "Part_id"; 
171 

5069  172 
Goal "Part (A Int B) h = (Part A h) Int (Part B h)"; 
2922  173 
by (Blast_tac 1); 
1188
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset

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

175 

5069  176 
Goal "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}"; 
2922  177 
by (Blast_tac 1); 
1188
0443e4dc8511
Added Part_Int and Part_Collect for inductive definitions
lcp
parents:
923
diff
changeset

178 
qed "Part_Collect"; 