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
    1.98           apply (simp add: ac_simps)
    1.99          apply (unfold xilin_sol_def)
   1.100 -        apply (tactic {* asm_simp_tac @{context} 6 *})
   1.101 +        apply (tactic \<open>asm_simp_tac @{context} 6\<close>)
   1.102          apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
   1.103          apply (rule_tac [6] unique_xi_sol)
   1.104             apply (rule_tac [3] funprod_zdvd)