src/HOL/NumberTheory/Chinese.thy
changeset 11868 56db9f3a6b3e
parent 11701 3d51fbf81c17
child 13187 e5434b822a96
     1.1 --- a/src/HOL/NumberTheory/Chinese.thy	Mon Oct 22 11:01:30 2001 +0200
     1.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Mon Oct 22 11:54:22 2001 +0200
     1.3 @@ -45,11 +45,11 @@
     1.4  defs
     1.5    m_cond_def:
     1.6      "m_cond n mf ==
     1.7 -      (\<forall>i. i \<le> n --> Numeral0 < mf i) \<and>
     1.8 -      (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = Numeral1)"
     1.9 +      (\<forall>i. i \<le> n --> 0 < mf i) \<and>
    1.10 +      (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1)"
    1.11  
    1.12    km_cond_def:
    1.13 -    "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = Numeral1"
    1.14 +    "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1"
    1.15  
    1.16    lincong_sol_def:
    1.17      "lincong_sol n kf bf mf x == \<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i)"
    1.18 @@ -63,8 +63,8 @@
    1.19    xilin_sol_def:
    1.20      "xilin_sol i n kf bf mf ==
    1.21        if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
    1.22 -        (SOME x. Numeral0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
    1.23 -      else Numeral0"
    1.24 +        (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
    1.25 +      else 0"
    1.26  
    1.27    x_sol_def:
    1.28      "x_sol n kf bf mf == funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
    1.29 @@ -72,15 +72,15 @@
    1.30  
    1.31  text {* \medskip @{term funprod} and @{term funsum} *}
    1.32  
    1.33 -lemma funprod_pos: "(\<forall>i. i \<le> n --> Numeral0 < mf i) ==> Numeral0 < funprod mf 0 n"
    1.34 +lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
    1.35    apply (induct n)
    1.36     apply auto
    1.37    apply (simp add: int_0_less_mult_iff)
    1.38    done
    1.39  
    1.40  lemma funprod_zgcd [rule_format (no_asm)]:
    1.41 -  "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i, mf m) = Numeral1) -->
    1.42 -    zgcd (funprod mf k l, mf m) = Numeral1"
    1.43 +  "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i, mf m) = 1) -->
    1.44 +    zgcd (funprod mf k l, mf m) = 1"
    1.45    apply (induct l)
    1.46     apply simp_all
    1.47    apply (rule impI)+
    1.48 @@ -110,14 +110,14 @@
    1.49    done
    1.50  
    1.51  lemma funsum_zero [rule_format (no_asm)]:
    1.52 -    "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = Numeral0) --> (funsum f k l) = Numeral0"
    1.53 +    "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = 0) --> (funsum f k l) = 0"
    1.54    apply (induct l)
    1.55     apply auto
    1.56    done
    1.57  
    1.58  lemma funsum_oneelem [rule_format (no_asm)]:
    1.59    "k \<le> j --> j \<le> k + l -->
    1.60 -    (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j --> f i = Numeral0) -->
    1.61 +    (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j --> f i = 0) -->
    1.62      funsum f k l = f j"
    1.63    apply (induct l)
    1.64     prefer 2
    1.65 @@ -127,9 +127,9 @@
    1.66     apply (subgoal_tac "k = j")
    1.67      apply (simp_all (no_asm_simp))
    1.68    apply (case_tac "Suc (k + n) = j")
    1.69 -   apply (subgoal_tac "funsum f k n = Numeral0")
    1.70 +   apply (subgoal_tac "funsum f k n = 0")
    1.71      apply (rule_tac [2] funsum_zero)
    1.72 -    apply (subgoal_tac [3] "f (Suc (k + n)) = Numeral0")
    1.73 +    apply (subgoal_tac [3] "f (Suc (k + n)) = 0")
    1.74       apply (subgoal_tac [3] "j \<le> k + n")
    1.75        prefer 4
    1.76        apply arith
    1.77 @@ -175,7 +175,7 @@
    1.78  
    1.79  lemma unique_xi_sol:
    1.80    "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
    1.81 -    ==> \<exists>!x. Numeral0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
    1.82 +    ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
    1.83    apply (rule zcong_lineq_unique)
    1.84     apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *})
    1.85      apply (unfold m_cond_def km_cond_def mhf_def)
    1.86 @@ -227,7 +227,7 @@
    1.87  
    1.88  lemma chinese_remainder:
    1.89    "0 < n ==> m_cond n mf ==> km_cond n kf mf
    1.90 -    ==> \<exists>!x. Numeral0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x"
    1.91 +    ==> \<exists>!x. 0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x"
    1.92    apply safe
    1.93     apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq)
    1.94         apply (rule_tac [6] zcong_funprod)
    1.95 @@ -242,7 +242,7 @@
    1.96          apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *})
    1.97          apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
    1.98          apply (subgoal_tac [7]
    1.99 -          "Numeral0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
   1.100 +          "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
   1.101            \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
   1.102           prefer 7
   1.103           apply (simp add: zmult_ac)