src/HOL/Number_Theory/MiscAlgebra.thy
 author hoelzl Tue Jan 18 21:37:23 2011 +0100 (2011-01-18) changeset 41654 32fe42892983 parent 41541 1fa4725c4656 child 41959 b460124855b8 permissions -rw-r--r--
Gauge measure removed
 nipkow@31719 ` 1` ```(* Title: MiscAlgebra.thy ``` nipkow@31719 ` 2` ``` Author: Jeremy Avigad ``` nipkow@31719 ` 3` haftmann@31772 ` 4` ```These are things that can be added to the Algebra library. ``` nipkow@31719 ` 5` ```*) ``` nipkow@31719 ` 6` nipkow@31719 ` 7` ```theory MiscAlgebra ``` haftmann@31772 ` 8` ```imports ``` nipkow@31719 ` 9` ``` "~~/src/HOL/Algebra/Ring" ``` nipkow@31719 ` 10` ``` "~~/src/HOL/Algebra/FiniteProduct" ``` nipkow@31719 ` 11` ```begin; ``` nipkow@31719 ` 12` nipkow@31719 ` 13` ```(* finiteness stuff *) ``` nipkow@31719 ` 14` nipkow@31952 ` 15` ```lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}" ``` nipkow@31719 ` 16` ``` apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<.. 'a monoid" where ``` nipkow@31719 ` 35` ``` "units_of G == (| carrier = Units G, ``` nipkow@31719 ` 36` ``` Group.monoid.mult = Group.monoid.mult G, ``` nipkow@31719 ` 37` ``` one = one G |)"; ``` nipkow@31719 ` 38` nipkow@31719 ` 39` ```(* ``` nipkow@31719 ` 40` nipkow@31719 ` 41` ```lemma (in monoid) Units_mult_closed [intro]: ``` nipkow@31719 ` 42` ``` "x : Units G ==> y : Units G ==> x \ y : Units G" ``` nipkow@31719 ` 43` ``` apply (unfold Units_def) ``` nipkow@31719 ` 44` ``` apply (clarsimp) ``` nipkow@31719 ` 45` ``` apply (rule_tac x = "xaa \ xa" in bexI) ``` nipkow@31719 ` 46` ``` apply auto ``` nipkow@31719 ` 47` ``` apply (subst m_assoc) ``` nipkow@31719 ` 48` ``` apply auto ``` nipkow@31719 ` 49` ``` apply (subst (2) m_assoc [symmetric]) ``` nipkow@31719 ` 50` ``` apply auto ``` nipkow@31719 ` 51` ``` apply (subst m_assoc) ``` nipkow@31719 ` 52` ``` apply auto ``` nipkow@31719 ` 53` ``` apply (subst (2) m_assoc [symmetric]) ``` nipkow@31719 ` 54` ``` apply auto ``` nipkow@31719 ` 55` ```done ``` nipkow@31719 ` 56` nipkow@31719 ` 57` ```*) ``` nipkow@31719 ` 58` nipkow@31719 ` 59` ```lemma (in monoid) units_group: "group(units_of G)" ``` nipkow@31719 ` 60` ``` apply (unfold units_of_def) ``` nipkow@31719 ` 61` ``` apply (rule groupI) ``` nipkow@31719 ` 62` ``` apply auto ``` nipkow@31719 ` 63` ``` apply (subst m_assoc) ``` nipkow@31719 ` 64` ``` apply auto ``` nipkow@31719 ` 65` ``` apply (rule_tac x = "inv x" in bexI) ``` nipkow@31719 ` 66` ``` apply auto ``` nipkow@31719 ` 67` ```done ``` nipkow@31719 ` 68` nipkow@31719 ` 69` ```lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)" ``` nipkow@31719 ` 70` ``` apply (rule group.group_comm_groupI) ``` nipkow@31719 ` 71` ``` apply (rule units_group) ``` wenzelm@41541 ` 72` ``` apply (insert comm_monoid_axioms) ``` nipkow@31719 ` 73` ``` apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def) ``` wenzelm@41541 ` 74` ``` apply auto ``` wenzelm@41541 ` 75` ``` done ``` nipkow@31719 ` 76` nipkow@31719 ` 77` ```lemma units_of_carrier: "carrier (units_of G) = Units G" ``` nipkow@31719 ` 78` ``` by (unfold units_of_def, auto) ``` nipkow@31719 ` 79` nipkow@31719 ` 80` ```lemma units_of_mult: "mult(units_of G) = mult G" ``` nipkow@31719 ` 81` ``` by (unfold units_of_def, auto) ``` nipkow@31719 ` 82` nipkow@31719 ` 83` ```lemma units_of_one: "one(units_of G) = one G" ``` nipkow@31719 ` 84` ``` by (unfold units_of_def, auto) ``` nipkow@31719 ` 85` nipkow@31719 ` 86` ```lemma (in monoid) units_of_inv: "x : Units G ==> ``` nipkow@31719 ` 87` ``` m_inv (units_of G) x = m_inv G x" ``` nipkow@31719 ` 88` ``` apply (rule sym) ``` nipkow@31719 ` 89` ``` apply (subst m_inv_def) ``` nipkow@31719 ` 90` ``` apply (rule the1_equality) ``` nipkow@31719 ` 91` ``` apply (rule ex_ex1I) ``` nipkow@31719 ` 92` ``` apply (subst (asm) Units_def) ``` nipkow@31719 ` 93` ``` apply auto ``` nipkow@31719 ` 94` ``` apply (erule inv_unique) ``` nipkow@31719 ` 95` ``` apply auto ``` nipkow@31719 ` 96` ``` apply (rule Units_closed) ``` nipkow@31719 ` 97` ``` apply (simp_all only: units_of_carrier [symmetric]) ``` nipkow@31719 ` 98` ``` apply (insert units_group) ``` nipkow@31719 ` 99` ``` apply auto ``` nipkow@31719 ` 100` ``` apply (subst units_of_mult [symmetric]) ``` nipkow@31719 ` 101` ``` apply (subst units_of_one [symmetric]) ``` nipkow@31719 ` 102` ``` apply (erule group.r_inv, assumption) ``` nipkow@31719 ` 103` ``` apply (subst units_of_mult [symmetric]) ``` nipkow@31719 ` 104` ``` apply (subst units_of_one [symmetric]) ``` nipkow@31719 ` 105` ``` apply (erule group.l_inv, assumption) ``` nipkow@31719 ` 106` ```done ``` nipkow@31719 ` 107` nipkow@31719 ` 108` ```lemma (in group) inj_on_const_mult: "a: (carrier G) ==> ``` nipkow@31719 ` 109` ``` inj_on (%x. a \ x) (carrier G)" ``` nipkow@31719 ` 110` ``` by (unfold inj_on_def, auto) ``` nipkow@31719 ` 111` nipkow@31719 ` 112` ```lemma (in group) surj_const_mult: "a : (carrier G) ==> ``` nipkow@31719 ` 113` ``` (%x. a \ x) ` (carrier G) = (carrier G)" ``` nipkow@31719 ` 114` ``` apply (auto simp add: image_def) ``` nipkow@31719 ` 115` ``` apply (rule_tac x = "(m_inv G a) \ x" in bexI) ``` nipkow@31719 ` 116` ``` apply auto ``` nipkow@31719 ` 117` ```(* auto should get this. I suppose we need "comm_monoid_simprules" ``` nipkow@31719 ` 118` ``` for mult_ac rewriting. *) ``` nipkow@31719 ` 119` ``` apply (subst m_assoc [symmetric]) ``` nipkow@31719 ` 120` ``` apply auto ``` nipkow@31719 ` 121` ```done ``` nipkow@31719 ` 122` nipkow@31719 ` 123` ```lemma (in group) l_cancel_one [simp]: "x : carrier G \ a : carrier G \ ``` nipkow@31719 ` 124` ``` (x \ a = x) = (a = one G)" ``` nipkow@31719 ` 125` ``` apply auto ``` nipkow@31719 ` 126` ``` apply (subst l_cancel [symmetric]) ``` nipkow@31719 ` 127` ``` prefer 4 ``` nipkow@31719 ` 128` ``` apply (erule ssubst) ``` nipkow@31719 ` 129` ``` apply auto ``` nipkow@31719 ` 130` ```done ``` nipkow@31719 ` 131` nipkow@31719 ` 132` ```lemma (in group) r_cancel_one [simp]: "x : carrier G \ a : carrier G \ ``` nipkow@31719 ` 133` ``` (a \ x = x) = (a = one G)" ``` nipkow@31719 ` 134` ``` apply auto ``` nipkow@31719 ` 135` ``` apply (subst r_cancel [symmetric]) ``` nipkow@31719 ` 136` ``` prefer 4 ``` nipkow@31719 ` 137` ``` apply (erule ssubst) ``` nipkow@31719 ` 138` ``` apply auto ``` nipkow@31719 ` 139` ```done ``` nipkow@31719 ` 140` nipkow@31719 ` 141` ```(* Is there a better way to do this? *) ``` nipkow@31719 ` 142` nipkow@31719 ` 143` ```lemma (in group) l_cancel_one' [simp]: "x : carrier G \ a : carrier G \ ``` nipkow@31719 ` 144` ``` (x = x \ a) = (a = one G)" ``` nipkow@31719 ` 145` ``` by (subst eq_commute, simp) ``` nipkow@31719 ` 146` nipkow@31719 ` 147` ```lemma (in group) r_cancel_one' [simp]: "x : carrier G \ a : carrier G \ ``` nipkow@31719 ` 148` ``` (x = a \ x) = (a = one G)" ``` nipkow@31719 ` 149` ``` by (subst eq_commute, simp) ``` nipkow@31719 ` 150` nipkow@31719 ` 151` ```(* This should be generalized to arbitrary groups, not just commutative ``` nipkow@31719 ` 152` ``` ones, using Lagrange's theorem. *) ``` nipkow@31719 ` 153` nipkow@31719 ` 154` ```lemma (in comm_group) power_order_eq_one: ``` nipkow@31719 ` 155` ``` assumes fin [simp]: "finite (carrier G)" ``` nipkow@31719 ` 156` ``` and a [simp]: "a : carrier G" ``` nipkow@31719 ` 157` ``` shows "a (^) card(carrier G) = one G" ``` nipkow@31719 ` 158` ```proof - ``` nipkow@31719 ` 159` ``` have "(\x:carrier G. x) = (\x:carrier G. a \ x)" ``` nipkow@31719 ` 160` ``` by (subst (2) finprod_reindex [symmetric], ``` nipkow@31719 ` 161` ``` auto simp add: Pi_def inj_on_const_mult surj_const_mult) ``` nipkow@31719 ` 162` ``` also have "\ = (\x:carrier G. a) \ (\x:carrier G. x)" ``` nipkow@31719 ` 163` ``` by (auto simp add: finprod_multf Pi_def) ``` nipkow@31719 ` 164` ``` also have "(\x:carrier G. a) = a (^) card(carrier G)" ``` nipkow@31719 ` 165` ``` by (auto simp add: finprod_const) ``` nipkow@31719 ` 166` ``` finally show ?thesis ``` nipkow@31719 ` 167` ```(* uses the preceeding lemma *) ``` nipkow@31719 ` 168` ``` by auto ``` nipkow@31719 ` 169` ```qed ``` nipkow@31719 ` 170` nipkow@31719 ` 171` nipkow@31719 ` 172` ```(* Miscellaneous *) ``` nipkow@31719 ` 173` nipkow@31719 ` 174` ```lemma (in cring) field_intro2: "\\<^bsub>R\<^esub> ~= \\<^bsub>R\<^esub> \ ALL x : carrier R - {\\<^bsub>R\<^esub>}. ``` nipkow@31719 ` 175` ``` x : Units R \ field R" ``` nipkow@31719 ` 176` ``` apply (unfold_locales) ``` wenzelm@41541 ` 177` ``` apply (insert cring_axioms, auto) ``` nipkow@31719 ` 178` ``` apply (rule trans) ``` nipkow@31719 ` 179` ``` apply (subgoal_tac "a = (a \ b) \ inv b") ``` nipkow@31719 ` 180` ``` apply assumption ``` nipkow@31719 ` 181` ``` apply (subst m_assoc) ``` wenzelm@41541 ` 182` ``` apply auto ``` nipkow@31719 ` 183` ``` apply (unfold Units_def) ``` nipkow@31719 ` 184` ``` apply auto ``` wenzelm@41541 ` 185` ``` done ``` nipkow@31719 ` 186` nipkow@31719 ` 187` ```lemma (in monoid) inv_char: "x : carrier G \ y : carrier G \ ``` wenzelm@41541 ` 188` ``` x \ y = \ \ y \ x = \ \ inv x = y" ``` nipkow@31719 ` 189` ``` apply (subgoal_tac "x : Units G") ``` nipkow@31719 ` 190` ``` apply (subgoal_tac "y = inv x \ \") ``` nipkow@31719 ` 191` ``` apply simp ``` nipkow@31719 ` 192` ``` apply (erule subst) ``` nipkow@31719 ` 193` ``` apply (subst m_assoc [symmetric]) ``` nipkow@31719 ` 194` ``` apply auto ``` nipkow@31719 ` 195` ``` apply (unfold Units_def) ``` nipkow@31719 ` 196` ``` apply auto ``` wenzelm@41541 ` 197` ``` done ``` nipkow@31719 ` 198` nipkow@31719 ` 199` ```lemma (in comm_monoid) comm_inv_char: "x : carrier G \ y : carrier G \ ``` nipkow@31719 ` 200` ``` x \ y = \ \ inv x = y" ``` nipkow@31719 ` 201` ``` apply (rule inv_char) ``` nipkow@31719 ` 202` ``` apply auto ``` nipkow@31719 ` 203` ``` apply (subst m_comm, auto) ``` wenzelm@41541 ` 204` ``` done ``` nipkow@31719 ` 205` nipkow@31719 ` 206` ```lemma (in ring) inv_neg_one [simp]: "inv (\ \) = \ \" ``` nipkow@31719 ` 207` ``` apply (rule inv_char) ``` nipkow@31719 ` 208` ``` apply (auto simp add: l_minus r_minus) ``` wenzelm@41541 ` 209` ``` done ``` nipkow@31719 ` 210` nipkow@31719 ` 211` ```lemma (in monoid) inv_eq_imp_eq: "x : Units G \ y : Units G \ ``` nipkow@31719 ` 212` ``` inv x = inv y \ x = y" ``` nipkow@31719 ` 213` ``` apply (subgoal_tac "inv(inv x) = inv(inv y)") ``` nipkow@31719 ` 214` ``` apply (subst (asm) Units_inv_inv)+ ``` nipkow@31719 ` 215` ``` apply auto ``` nipkow@31719 ` 216` ```done ``` nipkow@31719 ` 217` nipkow@31719 ` 218` ```lemma (in ring) Units_minus_one_closed [intro]: "\ \ : Units R" ``` nipkow@31719 ` 219` ``` apply (unfold Units_def) ``` nipkow@31719 ` 220` ``` apply auto ``` nipkow@31719 ` 221` ``` apply (rule_tac x = "\ \" in bexI) ``` nipkow@31719 ` 222` ``` apply auto ``` nipkow@31719 ` 223` ``` apply (simp add: l_minus r_minus) ``` nipkow@31719 ` 224` ```done ``` nipkow@31719 ` 225` nipkow@31719 ` 226` ```lemma (in monoid) inv_one [simp]: "inv \ = \" ``` nipkow@31719 ` 227` ``` apply (rule inv_char) ``` nipkow@31719 ` 228` ``` apply auto ``` nipkow@31719 ` 229` ```done ``` nipkow@31719 ` 230` nipkow@31719 ` 231` ```lemma (in ring) inv_eq_neg_one_eq: "x : Units R \ (inv x = \ \) = (x = \ \)" ``` nipkow@31719 ` 232` ``` apply auto ``` nipkow@31719 ` 233` ``` apply (subst Units_inv_inv [symmetric]) ``` nipkow@31719 ` 234` ``` apply auto ``` nipkow@31719 ` 235` ```done ``` nipkow@31719 ` 236` nipkow@31719 ` 237` ```lemma (in monoid) inv_eq_one_eq: "x : Units G \ (inv x = \) = (x = \)" ``` nipkow@31719 ` 238` ``` apply auto ``` nipkow@31719 ` 239` ``` apply (subst Units_inv_inv [symmetric]) ``` nipkow@31719 ` 240` ``` apply auto ``` nipkow@31719 ` 241` ```done ``` nipkow@31719 ` 242` nipkow@31719 ` 243` nipkow@31719 ` 244` ```(* This goes in FiniteProduct *) ``` nipkow@31719 ` 245` nipkow@31719 ` 246` ```lemma (in comm_monoid) finprod_UN_disjoint: ``` nipkow@31719 ` 247` ``` "finite I \ (ALL i:I. finite (A i)) \ (ALL i:I. ALL j:I. i ~= j \ ``` nipkow@31719 ` 248` ``` (A i) Int (A j) = {}) \ ``` nipkow@31719 ` 249` ``` (ALL i:I. ALL x: (A i). g x : carrier G) \ ``` nipkow@31719 ` 250` ``` finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I" ``` nipkow@31719 ` 251` ``` apply (induct set: finite) ``` nipkow@31719 ` 252` ``` apply force ``` nipkow@31719 ` 253` ``` apply clarsimp ``` nipkow@31719 ` 254` ``` apply (subst finprod_Un_disjoint) ``` nipkow@31719 ` 255` ``` apply blast ``` nipkow@31719 ` 256` ``` apply (erule finite_UN_I) ``` nipkow@31719 ` 257` ``` apply blast ``` nipkow@31721 ` 258` ``` apply (fastsimp) ``` nipkow@31719 ` 259` ``` apply (auto intro!: funcsetI finprod_closed) ``` nipkow@31719 ` 260` ```done ``` nipkow@31719 ` 261` nipkow@31719 ` 262` ```lemma (in comm_monoid) finprod_Union_disjoint: ``` nipkow@31719 ` 263` ``` "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G)); ``` nipkow@31719 ` 264` ``` (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |] ``` nipkow@31719 ` 265` ``` ==> finprod G f (Union C) = finprod G (finprod G f) C" ``` nipkow@31719 ` 266` ``` apply (frule finprod_UN_disjoint [of C id f]) ``` nipkow@31719 ` 267` ``` apply (unfold Union_def id_def, auto) ``` nipkow@31719 ` 268` ```done ``` nipkow@31719 ` 269` nipkow@31719 ` 270` ```lemma (in comm_monoid) finprod_one [rule_format]: ``` nipkow@31719 ` 271` ``` "finite A \ (ALL x:A. f x = \) \ ``` nipkow@31719 ` 272` ``` finprod G f A = \" ``` nipkow@31727 ` 273` ```by (induct set: finite) auto ``` nipkow@31719 ` 274` nipkow@31719 ` 275` nipkow@31719 ` 276` ```(* need better simplification rules for rings *) ``` nipkow@31719 ` 277` ```(* the next one holds more generally for abelian groups *) ``` nipkow@31719 ` 278` nipkow@31719 ` 279` ```lemma (in cring) sum_zero_eq_neg: ``` nipkow@31719 ` 280` ``` "x : carrier R \ y : carrier R \ x \ y = \ \ x = \ y" ``` nipkow@31719 ` 281` ``` apply (subgoal_tac "\ y = \ \ \ y") ``` nipkow@31719 ` 282` ``` apply (erule ssubst)back ``` nipkow@31719 ` 283` ``` apply (erule subst) ``` wenzelm@41541 ` 284` ``` apply (simp_all add: ring_simprules) ``` wenzelm@41541 ` 285` ``` done ``` nipkow@31719 ` 286` nipkow@31719 ` 287` ```(* there's a name conflict -- maybe "domain" should be ``` nipkow@31719 ` 288` ``` "integral_domain" *) ``` nipkow@31719 ` 289` nipkow@31719 ` 290` ```lemma (in Ring.domain) square_eq_one: ``` nipkow@31719 ` 291` ``` fixes x ``` nipkow@31719 ` 292` ``` assumes [simp]: "x : carrier R" and ``` nipkow@31719 ` 293` ``` "x \ x = \" ``` nipkow@31719 ` 294` ``` shows "x = \ | x = \\" ``` nipkow@31719 ` 295` ```proof - ``` nipkow@31719 ` 296` ``` have "(x \ \) \ (x \ \ \) = x \ x \ \ \" ``` nipkow@31719 ` 297` ``` by (simp add: ring_simprules) ``` nipkow@31719 ` 298` ``` also with `x \ x = \` have "\ = \" ``` nipkow@31719 ` 299` ``` by (simp add: ring_simprules) ``` nipkow@31719 ` 300` ``` finally have "(x \ \) \ (x \ \ \) = \" . ``` nipkow@31719 ` 301` ``` hence "(x \ \) = \ | (x \ \ \) = \" ``` nipkow@31719 ` 302` ``` by (intro integral, auto) ``` nipkow@31719 ` 303` ``` thus ?thesis ``` nipkow@31719 ` 304` ``` apply auto ``` nipkow@31719 ` 305` ``` apply (erule notE) ``` nipkow@31719 ` 306` ``` apply (rule sum_zero_eq_neg) ``` nipkow@31719 ` 307` ``` apply auto ``` nipkow@31719 ` 308` ``` apply (subgoal_tac "x = \ (\ \)") ``` nipkow@31719 ` 309` ``` apply (simp add: ring_simprules) ``` nipkow@31719 ` 310` ``` apply (rule sum_zero_eq_neg) ``` nipkow@31719 ` 311` ``` apply auto ``` nipkow@31719 ` 312` ``` done ``` nipkow@31719 ` 313` ```qed ``` nipkow@31719 ` 314` nipkow@31719 ` 315` ```lemma (in Ring.domain) inv_eq_self: "x : Units R \ ``` nipkow@31719 ` 316` ``` x = inv x \ x = \ | x = \ \" ``` nipkow@31719 ` 317` ``` apply (rule square_eq_one) ``` nipkow@31719 ` 318` ``` apply auto ``` nipkow@31719 ` 319` ``` apply (erule ssubst)back ``` nipkow@31719 ` 320` ``` apply (erule Units_r_inv) ``` nipkow@31719 ` 321` ```done ``` nipkow@31719 ` 322` nipkow@31719 ` 323` nipkow@31719 ` 324` ```(* ``` nipkow@31719 ` 325` ``` The following translates theorems about groups to the facts about ``` nipkow@31719 ` 326` ``` the units of a ring. (The list should be expanded as more things are ``` nipkow@31719 ` 327` ``` needed.) ``` nipkow@31719 ` 328` ```*) ``` nipkow@31719 ` 329` nipkow@31719 ` 330` ```lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \ ``` nipkow@31719 ` 331` ``` finite (Units R)" ``` nipkow@31719 ` 332` ``` by (rule finite_subset, auto) ``` nipkow@31719 ` 333` nipkow@31719 ` 334` ```(* this belongs with MiscAlgebra.thy *) ``` nipkow@31719 ` 335` ```lemma (in monoid) units_of_pow: ``` nipkow@31719 ` 336` ``` "x : Units G \ x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n" ``` nipkow@31719 ` 337` ``` apply (induct n) ``` nipkow@31719 ` 338` ``` apply (auto simp add: units_group group.is_monoid ``` wenzelm@41541 ` 339` ``` monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult) ``` wenzelm@41541 ` 340` ``` done ``` nipkow@31719 ` 341` nipkow@31719 ` 342` ```lemma (in cring) units_power_order_eq_one: "finite (Units R) \ a : Units R ``` nipkow@31719 ` 343` ``` \ a (^) card(Units R) = \" ``` nipkow@31719 ` 344` ``` apply (subst units_of_carrier [symmetric]) ``` nipkow@31719 ` 345` ``` apply (subst units_of_one [symmetric]) ``` nipkow@31719 ` 346` ``` apply (subst units_of_pow [symmetric]) ``` nipkow@31719 ` 347` ``` apply assumption ``` nipkow@31719 ` 348` ``` apply (rule comm_group.power_order_eq_one) ``` nipkow@31719 ` 349` ``` apply (rule units_comm_group) ``` nipkow@31719 ` 350` ``` apply (unfold units_of_def, auto) ``` wenzelm@41541 ` 351` ``` done ``` nipkow@31719 ` 352` nipkow@31719 ` 353` ```end ```