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