src/HOL/Old_Number_Theory/IntPrimes.thy

 (*  Title:      HOL/Old_Number_Theory/IntPrimes.thy
     Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
-section {* Divisibility and prime numbers (on integers) *}
+section \<open>Divisibility and prime numbers (on integers)\<close>
 
 theory IntPrimes
 imports Primes
 begin
 
-text {*
+text \<open>
   The @{text dvd} relation, GCD, Euclid's extended algorithm, primes,
   congruences (all on the Integers).  Comparable to theory @{text
   Primes}, but @{text dvd} is included here as it is not present in
   main HOL.  Also includes extended GCD and congruences not present in
   @{text Primes}.
-*}
-
-
-subsection {* Definitions *}
+\<close>
+
+
+subsection \<open>Definitions\<close>
 
 fun xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
 where
   "xzgcda m n r' r s' s t' t =
         (if r \<le> 0 then (r', s', t')

 
 definition zcong :: "int => int => int => bool"  ("(1[_ = _] '(mod _'))")
   where "[a = b] (mod m) = (m dvd (a - b))"
 
 
-subsection {* Euclid's Algorithm and GCD *}
+subsection \<open>Euclid's Algorithm and GCD\<close>
 
 
 lemma zrelprime_zdvd_zmult_aux:
      "zgcd n k = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
     by (metis abs_of_nonneg dvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs mult_1_right)

   done
 
 lemma zgcd_geq_zero: "0 <= zgcd x y"
   by (auto simp add: zgcd_def)
 
-text{*This is merely a sanity check on zprime, since the previous version
-      denoted the empty set.*}
+text\<open>This is merely a sanity check on zprime, since the previous version
+      denoted the empty set.\<close>
 lemma "zprime 2"
   apply (auto simp add: zprime_def) 
   apply (frule zdvd_imp_le, simp) 
   apply (auto simp add: order_le_less dvd_def) 
   done

 lemma zdvd_iff_zgcd: "0 < m ==> m dvd n \<longleftrightarrow> zgcd n m = m"
   by (metis abs_of_pos dvd_mult_div_cancel zgcd_0 zgcd_commute zgcd_geq_zero zgcd_zdvd2 zgcd_zmult_eq_self)
 
 
 
-subsection {* Congruences *}
+subsection \<open>Congruences\<close>
 
 lemma zcong_1 [simp]: "[a = b] (mod 1)"
   by (unfold zcong_def, auto)
 
 lemma zcong_refl [simp]: "[k = k] (mod m)"

 lemma "[a = b] (mod m) = (a mod m = b mod m)"
   apply (cases "m = 0", simp)
   apply (simp add: linorder_neq_iff)
   apply (erule disjE)  
    prefer 2 apply (simp add: zcong_zmod_eq)
-  txt{*Remainding case: @{term "m<0"}*}
+  txt\<open>Remainding case: @{term "m<0"}\<close>
   apply (rule_tac t = m in minus_minus [THEN subst])
   apply (subst zcong_zminus)
   apply (subst zcong_zmod_eq, arith)
   apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b]) 
   apply (simp add: zmod_zminus2_eq_if del: neg_mod_bound)
   done
 
-subsection {* Modulo *}
+subsection \<open>Modulo\<close>
 
 lemma zmod_zdvd_zmod:
     "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
   by (rule mod_mod_cancel) 
 
 
-subsection {* Extended GCD *}
+subsection \<open>Extended GCD\<close>
 
 declare xzgcda.simps [simp del]
 
 lemma xzgcd_correct_aux1:
   "zgcd r' r = k --> 0 < r -->

    apply (rule_tac [2] xzgcd_correct_aux2 [THEN mp, THEN mp])
     apply (rule xzgcd_correct_aux1 [THEN mp, THEN mp], auto)
   done
 
 
-text {* \medskip @{term xzgcd} linear *}
+text \<open>\medskip @{term xzgcd} linear\<close>
 
 lemma xzgcda_linear_aux1:
   "(a - r * b) * m + (c - r * d) * (n::int) =
    (a * m + c * n) - r * (b * m + d * n)"
   by (simp add: left_diff_distrib distrib_left mult.assoc)

 lemma zcong_lineq_unique:
   "0 < n ==>
     zgcd a n = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
   apply auto
    apply (rule_tac [2] zcong_zless_imp_eq)
-       apply (tactic {* stac @{context} (@{thm zcong_cancel2} RS sym) 6 *})
+       apply (tactic \<open>stac @{context} (@{thm zcong_cancel2} RS sym) 6\<close>)
          apply (rule_tac [8] zcong_trans)
           apply (simp_all (no_asm_simp))
    prefer 2
    apply (simp add: zcong_sym)
   apply (cut_tac a = a and n = n in zcong_lineq_ex, auto)