src/HOL/Algebra/IntRing.thy
author ballarin
Tue Jul 24 15:29:57 2007 +0200 (2007-07-24)
changeset 23957 54fab60ddc97
parent 22063 717425609192
child 24131 1099f6c73649
permissions -rw-r--r--
Interpretation of rings (as integers) maps defined operations to defined
operations..
     1 (*
     2   Title:     HOL/Algebra/IntRing.thy
     3   Id:        $Id$
     4   Author:    Stephan Hohe, TU Muenchen
     5 *)
     6 
     7 theory IntRing
     8 imports QuotRing IntDef
     9 begin
    10 
    11 
    12 section {* The Ring of Integers *}
    13 
    14 subsection {* Some properties of @{typ int} *}
    15 
    16 lemma dvds_imp_abseq:
    17   "\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> abs l = abs (k::int)"
    18 apply (subst abs_split, rule conjI)
    19  apply (clarsimp, subst abs_split, rule conjI)
    20   apply (clarsimp)
    21   apply (cases "k=0", simp)
    22   apply (cases "l=0", simp)
    23   apply (simp add: zdvd_anti_sym)
    24  apply clarsimp
    25  apply (cases "k=0", simp)
    26  apply (simp add: zdvd_anti_sym)
    27 apply (clarsimp, subst abs_split, rule conjI)
    28  apply (clarsimp)
    29  apply (cases "l=0", simp)
    30  apply (simp add: zdvd_anti_sym)
    31 apply (clarsimp)
    32 apply (subgoal_tac "-l = -k", simp)
    33 apply (intro zdvd_anti_sym, simp+)
    34 done
    35 
    36 lemma abseq_imp_dvd:
    37   assumes a_lk: "abs l = abs (k::int)"
    38   shows "l dvd k"
    39 proof -
    40   from a_lk
    41       have "nat (abs l) = nat (abs k)" by simp
    42   hence "nat (abs l) dvd nat (abs k)" by simp
    43   hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff)
    44   hence "abs l dvd k" by simp
    45   thus "l dvd k" 
    46   apply (unfold dvd_def, cases "l<0")
    47    defer 1 apply clarsimp
    48   proof (clarsimp)
    49     fix k
    50     assume l0: "l < 0"
    51     have "- (l * k) = l * (-k)" by simp
    52     thus "\<exists>ka. - (l * k) = l * ka" by fast
    53   qed
    54 qed
    55 
    56 lemma dvds_eq_abseq:
    57   "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
    58 apply rule
    59  apply (simp add: dvds_imp_abseq)
    60 apply (rule conjI)
    61  apply (simp add: abseq_imp_dvd)+
    62 done
    63 
    64 
    65 
    66 subsection {* The Set of Integers as Algebraic Structure *}
    67 
    68 subsubsection {* Definition of @{text "\<Z>"} *}
    69 
    70 constdefs
    71   int_ring :: "int ring" ("\<Z>")
    72   "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
    73 
    74 lemma int_Zcarr [intro!, simp]:
    75   "k \<in> carrier \<Z>"
    76   by (simp add: int_ring_def)
    77 
    78 lemma int_is_cring:
    79   "cring \<Z>"
    80 unfolding int_ring_def
    81 apply (rule cringI)
    82   apply (rule abelian_groupI, simp_all)
    83   defer 1
    84   apply (rule comm_monoidI, simp_all)
    85  apply (rule zadd_zmult_distrib)
    86 apply (fast intro: zadd_zminus_inverse2)
    87 done
    88 
    89 (*
    90 lemma int_is_domain:
    91   "domain \<Z>"
    92 apply (intro domain.intro domain_axioms.intro)
    93   apply (rule int_is_cring)
    94  apply (unfold int_ring_def, simp+)
    95 done
    96 *)
    97 subsubsection {* Interpretations *}
    98 
    99 text {* Since definitions of derived operations are global, their
   100   interpretation needs to be done as early as possible --- that is,
   101   with as few assumptions as possible. *}
   102 
   103 interpretation int: monoid ["\<Z>"]
   104   where "carrier \<Z> = UNIV"
   105     and "mult \<Z> x y = x * y"
   106     and "one \<Z> = 1"
   107     and "pow \<Z> x n = x^n"
   108 proof -
   109   -- "Specification"
   110   show "monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
   111   then interpret int: monoid ["\<Z>"] .
   112 
   113   -- "Carrier"
   114   show "carrier \<Z> = UNIV" by (simp add: int_ring_def)
   115 
   116   -- "Operations"
   117   { fix x y show "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
   118   note mult = this
   119   show one: "one \<Z> = 1" by (simp add: int_ring_def)
   120   show "pow \<Z> x n = x^n" by (induct n) (simp, simp add: int_ring_def)+
   121 qed
   122 
   123 interpretation int: comm_monoid ["\<Z>"]
   124   where "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
   125 proof -
   126   -- "Specification"
   127   show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
   128   then interpret int: comm_monoid ["\<Z>"] .
   129 
   130   -- "Operations"
   131   { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
   132   note mult = this
   133   have one: "one \<Z> = 1" by (simp add: int_ring_def)
   134   show "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
   135   proof (cases "finite A")
   136     case True then show ?thesis proof induct
   137       case empty show ?case by (simp add: one)
   138     next
   139       case insert then show ?case by (simp add: Pi_def mult)
   140     qed
   141   next
   142     case False then show ?thesis by (simp add: finprod_def)
   143   qed
   144 qed
   145 
   146 interpretation int: abelian_monoid ["\<Z>"]
   147   where "zero \<Z> = 0"
   148     and "add \<Z> x y = x + y"
   149     and "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
   150 proof -
   151   -- "Specification"
   152   show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
   153   then interpret int: abelian_monoid ["\<Z>"] .
   154 
   155   -- "Operations"
   156   { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
   157   note add = this
   158   show zero: "zero \<Z> = 0" by (simp add: int_ring_def)
   159   show "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
   160   proof (cases "finite A")
   161     case True then show ?thesis proof induct
   162       case empty show ?case by (simp add: zero)
   163     next
   164       case insert then show ?case by (simp add: Pi_def add)
   165     qed
   166   next
   167     case False then show ?thesis by (simp add: finsum_def finprod_def)
   168   qed
   169 qed
   170 
   171 interpretation int: abelian_group ["\<Z>"]
   172   where "a_inv \<Z> x = - x"
   173     and "a_minus \<Z> x y = x - y"
   174 proof -
   175   -- "Specification"
   176   show "abelian_group \<Z>"
   177   proof (rule abelian_groupI)
   178     show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
   179       by (simp add: int_ring_def) arith
   180   qed (auto simp: int_ring_def)
   181   then interpret int: abelian_group ["\<Z>"] .
   182 
   183   -- "Operations"
   184   { fix x y have "add \<Z> x y = x + y" by (simp add: int_ring_def) }
   185   note add = this
   186   have zero: "zero \<Z> = 0" by (simp add: int_ring_def)
   187   { fix x
   188     have "add \<Z> (-x) x = zero \<Z>" by (simp add: add zero)
   189     then show "a_inv \<Z> x = - x" by (simp add: int.minus_equality) }
   190   note a_inv = this
   191   show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
   192 qed
   193 
   194 interpretation int: "domain" ["\<Z>"]
   195   by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)
   196 
   197 
   198 interpretation int: partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
   199   where "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
   200 proof -
   201   show "partial_order (| carrier = UNIV::int set, le = op \<le> |)"
   202     by unfold_locales simp_all
   203   show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
   204     by (simp add: lless_def) auto
   205 qed
   206 
   207 interpretation int: lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
   208   where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y"
   209     and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y"
   210 proof -
   211   let ?Z = "(| carrier = UNIV::int set, le = op \<le> |)"
   212   show "lattice ?Z"
   213     apply unfold_locales
   214     apply (simp add: least_def Upper_def)
   215     apply arith
   216     apply (simp add: greatest_def Lower_def)
   217     apply arith
   218     done
   219   then interpret int: lattice ["?Z"] .
   220   show "join ?Z x y = max x y"
   221     apply (rule int.joinI)
   222     apply (simp_all add: least_def Upper_def)
   223     apply arith
   224     done
   225   show "meet ?Z x y = min x y"
   226     apply (rule int.meetI)
   227     apply (simp_all add: greatest_def Lower_def)
   228     apply arith
   229     done
   230 qed
   231 
   232 interpretation int: total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
   233   by unfold_locales clarsimp
   234 
   235 (*
   236 lemma int_le_total_order:
   237   "total_order (| carrier = UNIV::int set, le = op \<le> |)"
   238   apply (rule partial_order.total_orderI)
   239    apply (rule partial_order.intro, simp+)
   240   apply clarsimp
   241   done
   242 
   243 lemma less_int:
   244   "lless (| carrier = UNIV::int set, le = op \<le> |) = (op <)"
   245   by (auto simp add: expand_fun_eq lless_def)
   246 
   247 lemma join_int:
   248   "join (| carrier = UNIV::int set, le = op \<le> |) = max"
   249   apply (simp add: expand_fun_eq max_def)
   250   apply (rule+)
   251   apply (rule lattice.joinI)
   252   apply (simp add: int_le_total_order total_order.axioms)
   253   apply (simp add: least_def Upper_def)
   254   apply arith
   255   apply simp apply simp
   256   apply (rule lattice.joinI)
   257   apply (simp add: int_le_total_order total_order.axioms)
   258   apply (simp add: least_def Upper_def)
   259   apply arith
   260   apply simp apply simp
   261   done
   262 
   263 lemma meet_int:
   264   "meet (| carrier = UNIV::int set, le = op \<le> |) = min"
   265   apply (simp add: expand_fun_eq min_def)
   266   apply (rule+)
   267   apply (rule lattice.meetI)
   268   apply (simp add: int_le_total_order total_order.axioms)
   269   apply (simp add: greatest_def Lower_def)
   270   apply arith
   271   apply simp apply simp
   272   apply (rule lattice.meetI)
   273   apply (simp add: int_le_total_order total_order.axioms)
   274   apply (simp add: greatest_def Lower_def)
   275   apply arith
   276   apply simp apply simp
   277   done
   278 
   279 lemma carrier_int:
   280   "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
   281   apply simp
   282   done
   283 
   284 text {* Interpretation unfolding @{text lless}, @{text join} and @{text
   285   meet} since they have natural representations in @{typ int}. *}
   286 
   287 interpretation 
   288   int [unfolded less_int join_int meet_int carrier_int]:
   289   total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
   290   by (rule int_le_total_order)
   291 *)
   292 
   293 
   294 subsubsection {* Generated Ideals of @{text "\<Z>"} *}
   295 
   296 lemma int_Idl:
   297   "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
   298   apply (subst int.cgenideal_eq_genideal[symmetric]) apply (simp add: int_ring_def)
   299   apply (simp add: cgenideal_def int_ring_def)
   300   done
   301 
   302 lemma multiples_principalideal:
   303   "principalideal {x * a | x. True } \<Z>"
   304 apply (subst int_Idl[symmetric], rule principalidealI)
   305  apply (rule int.genideal_ideal, simp)
   306 apply fast
   307 done
   308 
   309 lemma prime_primeideal:
   310   assumes prime: "prime (nat p)"
   311   shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
   312 apply (rule primeidealI)
   313    apply (rule int.genideal_ideal, simp)
   314   apply (rule int_is_cring)
   315  apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
   316  apply (simp add: int_ring_def)
   317  apply clarsimp defer 1
   318  apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
   319  apply (simp add: int_ring_def)
   320  apply (elim exE)
   321 proof -
   322   fix a b x
   323 
   324   from prime
   325       have ppos: "0 <= p" by (simp add: prime_def)
   326   have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
   327   proof -
   328     fix x
   329     assume "nat p dvd nat (abs x)"
   330     hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
   331     thus "p dvd x" by (simp add: ppos)
   332   qed
   333 
   334 
   335   assume "a * b = x * p"
   336   hence "p dvd a * b" by simp
   337   hence "nat p dvd nat (abs (a * b))"
   338   apply (subst nat_dvd_iff, clarsimp)
   339   apply (rule conjI, clarsimp, simp add: zabs_def)
   340   proof (clarsimp)
   341     assume a: " ~ 0 <= p"
   342     from prime
   343         have "0 < p" by (simp add: prime_def)
   344     from a and this
   345         have "False" by simp
   346     thus "nat (abs (a * b)) = 0" ..
   347   qed
   348   hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
   349   hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
   350   hence "p dvd a | p dvd b" by (fast intro: unnat)
   351   thus "(EX x. a = x * p) | (EX x. b = x * p)"
   352   proof
   353     assume "p dvd a"
   354     hence "EX x. a = p * x" by (simp add: dvd_def)
   355     from this obtain x
   356         where "a = p * x" by fast
   357     hence "a = x * p" by simp
   358     hence "EX x. a = x * p" by simp
   359     thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
   360   next
   361     assume "p dvd b"
   362     hence "EX x. b = p * x" by (simp add: dvd_def)
   363     from this obtain x
   364         where "b = p * x" by fast
   365     hence "b = x * p" by simp
   366     hence "EX x. b = x * p" by simp
   367     thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
   368   qed
   369 next
   370   assume "UNIV = {uu. EX x. uu = x * p}"
   371   from this obtain x 
   372       where "1 = x * p" by fast
   373   from this [symmetric]
   374       have "p * x = 1" by (subst zmult_commute)
   375   hence "\<bar>p * x\<bar> = 1" by simp
   376   hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
   377   from this and prime
   378       show "False" by (simp add: prime_def)
   379 qed
   380 
   381 
   382 subsubsection {* Ideals and Divisibility *}
   383 
   384 lemma int_Idl_subset_ideal:
   385   "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
   386 by (rule int.Idl_subset_ideal', simp+)
   387 
   388 lemma Idl_subset_eq_dvd:
   389   "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)"
   390 apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
   391 apply (rule, clarify)
   392 apply (simp add: dvd_def, clarify)
   393 apply (simp add: int.m_comm)
   394 done
   395 
   396 lemma dvds_eq_Idl:
   397   "(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})"
   398 proof -
   399   have a: "l dvd k = (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric])
   400   have b: "k dvd l = (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric])
   401 
   402   have "(l dvd k \<and> k dvd l) = ((Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) \<and> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k}))"
   403   by (subst a, subst b, simp)
   404   also have "((Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) \<and> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})" by (rule, fast+)
   405   finally
   406     show ?thesis .
   407 qed
   408 
   409 lemma Idl_eq_abs:
   410   "(Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}) = (abs l = abs k)"
   411 apply (subst dvds_eq_abseq[symmetric])
   412 apply (rule dvds_eq_Idl[symmetric])
   413 done
   414 
   415 
   416 subsubsection {* Ideals and the Modulus *}
   417 
   418 constdefs
   419    ZMod :: "int => int => int set"
   420   "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
   421 
   422 lemmas ZMod_defs =
   423   ZMod_def genideal_def
   424 
   425 lemma rcos_zfact:
   426   assumes kIl: "k \<in> ZMod l r"
   427   shows "EX x. k = x * l + r"
   428 proof -
   429   from kIl[unfolded ZMod_def]
   430       have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def)
   431   from this obtain xl
   432       where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
   433       and k: "k = xl + r"
   434       by auto
   435   from xl obtain x
   436       where "xl = x * l"
   437       by (simp add: int_Idl, fast)
   438   from k and this
   439       have "k = x * l + r" by simp
   440   thus "\<exists>x. k = x * l + r" ..
   441 qed
   442 
   443 lemma ZMod_imp_zmod:
   444   assumes zmods: "ZMod m a = ZMod m b"
   445   shows "a mod m = b mod m"
   446 proof -
   447   interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
   448   from zmods
   449       have "b \<in> ZMod m a"
   450       unfolding ZMod_def
   451       by (simp add: a_repr_independenceD)
   452   from this
   453       have "EX x. b = x * m + a" by (rule rcos_zfact)
   454   from this obtain x
   455       where "b = x * m + a"
   456       by fast
   457 
   458   hence "b mod m = (x * m + a) mod m" by simp
   459   also
   460       have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
   461   also
   462       have "\<dots> = a mod m" by simp
   463   finally
   464       have "b mod m = a mod m" .
   465   thus "a mod m = b mod m" ..
   466 qed
   467 
   468 lemma ZMod_mod:
   469   shows "ZMod m a = ZMod m (a mod m)"
   470 proof -
   471   interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule int.genideal_ideal, fast)
   472   show ?thesis
   473       unfolding ZMod_def
   474   apply (rule a_repr_independence'[symmetric])
   475   apply (simp add: int_Idl a_r_coset_defs)
   476   apply (simp add: int_ring_def)
   477   proof -
   478     have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality)
   479     hence "a = (a div m) * m + (a mod m)" by simp
   480     thus "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" by fast
   481   qed simp
   482 qed
   483 
   484 lemma zmod_imp_ZMod:
   485   assumes modeq: "a mod m = b mod m"
   486   shows "ZMod m a = ZMod m b"
   487 proof -
   488   have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod)
   489   also have "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric])
   490   also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric])
   491   finally show ?thesis .
   492 qed
   493 
   494 corollary ZMod_eq_mod:
   495   shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)"
   496 by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)
   497 
   498 
   499 subsubsection {* Factorization *}
   500 
   501 constdefs
   502   ZFact :: "int \<Rightarrow> int set ring"
   503   "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
   504 
   505 lemmas ZFact_defs = ZFact_def FactRing_def
   506 
   507 lemma ZFact_is_cring:
   508   shows "cring (ZFact k)"
   509 apply (unfold ZFact_def)
   510 apply (rule ideal.quotient_is_cring)
   511  apply (intro ring.genideal_ideal)
   512   apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
   513  apply simp
   514 apply (rule int_is_cring)
   515 done
   516 
   517 lemma ZFact_zero:
   518   "carrier (ZFact 0) = (\<Union>a. {{a}})"
   519 apply (insert int.genideal_zero)
   520 apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
   521 done
   522 
   523 lemma ZFact_one:
   524   "carrier (ZFact 1) = {UNIV}"
   525 apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps)
   526 apply (subst int.genideal_one[unfolded int_ring_def, simplified ring_record_simps])
   527 apply (rule, rule, clarsimp)
   528  apply (rule, rule, clarsimp)
   529  apply (rule, clarsimp, arith)
   530 apply (rule, clarsimp)
   531 apply (rule exI[of _ "0"], clarsimp)
   532 done
   533 
   534 lemma ZFact_prime_is_domain:
   535   assumes pprime: "prime (nat p)"
   536   shows "domain (ZFact p)"
   537 apply (unfold ZFact_def)
   538 apply (rule primeideal.quotient_is_domain)
   539 apply (rule prime_primeideal[OF pprime])
   540 done
   541 
   542 end