src/HOL/Old_Number_Theory/Chinese.thy
 changeset 61382 efac889fccbc parent 59498 50b60f501b05 child 63167 0909deb8059b
```     1.1 --- a/src/HOL/Old_Number_Theory/Chinese.thy	Sat Oct 10 16:21:34 2015 +0200
1.2 +++ b/src/HOL/Old_Number_Theory/Chinese.thy	Sat Oct 10 16:26:23 2015 +0200
1.3 @@ -3,22 +3,22 @@
1.4      Copyright   2000  University of Cambridge
1.5  *)
1.6
1.7 -section {* The Chinese Remainder Theorem *}
1.8 +section \<open>The Chinese Remainder Theorem\<close>
1.9
1.10  theory Chinese
1.11  imports IntPrimes
1.12  begin
1.13
1.14 -text {*
1.15 +text \<open>
1.16    The Chinese Remainder Theorem for an arbitrary finite number of
1.17    equations.  (The one-equation case is included in theory @{text
1.18    IntPrimes}.  Uses functions for indexing.\footnote{Maybe @{term
1.19    funprod} and @{term funsum} should be based on general @{term fold}
1.20    on indices?}
1.21 -*}
1.22 +\<close>
1.23
1.24
1.25 -subsection {* Definitions *}
1.26 +subsection \<open>Definitions\<close>
1.27
1.28  primrec funprod :: "(nat => int) => nat => nat => int"
1.29  where
1.30 @@ -65,7 +65,7 @@
1.31    "x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
1.32
1.33
1.34 -text {* \medskip @{term funprod} and @{term funsum} *}
1.35 +text \<open>\medskip @{term funprod} and @{term funsum}\<close>
1.36
1.37  lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
1.38  by (induct n) auto
1.39 @@ -126,7 +126,7 @@
1.40    done
1.41
1.42
1.43 -subsection {* Chinese: uniqueness *}
1.44 +subsection \<open>Chinese: uniqueness\<close>
1.45
1.46  lemma zcong_funprod_aux:
1.47    "m_cond n mf ==> km_cond n kf mf
1.48 @@ -160,17 +160,17 @@
1.49    done
1.50
1.51
1.52 -subsection {* Chinese: existence *}
1.53 +subsection \<open>Chinese: existence\<close>
1.54
1.55  lemma unique_xi_sol:
1.56    "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
1.57      ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
1.58    apply (rule zcong_lineq_unique)
1.59 -   apply (tactic {* stac @{context} @{thm zgcd_zmult_cancel} 2 *})
1.60 +   apply (tactic \<open>stac @{context} @{thm zgcd_zmult_cancel} 2\<close>)
1.61      apply (unfold m_cond_def km_cond_def mhf_def)
1.62      apply (simp_all (no_asm_simp))
1.63    apply safe
1.64 -    apply (tactic {* stac @{context} @{thm zgcd_zmult_cancel} 3 *})
1.65 +    apply (tactic \<open>stac @{context} @{thm zgcd_zmult_cancel} 3\<close>)
1.66       apply (rule_tac [!] funprod_zgcd)
1.67       apply safe
1.68       apply simp_all
1.69 @@ -216,7 +216,7 @@
1.70    done
1.71
1.72
1.73 -subsection {* Chinese *}
1.74 +subsection \<open>Chinese\<close>
1.75
1.76  lemma chinese_remainder:
1.77    "0 < n ==> m_cond n mf ==> km_cond n kf mf
1.78 @@ -228,19 +228,19 @@
1.79    apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
1.80    apply (unfold lincong_sol_def)
1.81    apply safe
1.82 -    apply (tactic {* stac @{context} @{thm zcong_zmod} 3 *})
1.83 -    apply (tactic {* stac @{context} @{thm mod_mult_eq} 3 *})
1.84 -    apply (tactic {* stac @{context} @{thm mod_mod_cancel} 3 *})
1.85 -      apply (tactic {* stac @{context} @{thm x_sol_lin} 4 *})
1.86 -        apply (tactic {* stac @{context} (@{thm mod_mult_eq} RS sym) 6 *})
1.87 -        apply (tactic {* stac @{context} (@{thm zcong_zmod} RS sym) 6 *})
1.88 +    apply (tactic \<open>stac @{context} @{thm zcong_zmod} 3\<close>)
1.89 +    apply (tactic \<open>stac @{context} @{thm mod_mult_eq} 3\<close>)
1.90 +    apply (tactic \<open>stac @{context} @{thm mod_mod_cancel} 3\<close>)
1.91 +      apply (tactic \<open>stac @{context} @{thm x_sol_lin} 4\<close>)
1.92 +        apply (tactic \<open>stac @{context} (@{thm mod_mult_eq} RS sym) 6\<close>)
1.93 +        apply (tactic \<open>stac @{context} (@{thm zcong_zmod} RS sym) 6\<close>)
1.94          apply (subgoal_tac [6]
1.95            "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
1.96            \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
1.97           prefer 6