author  nipkow 
Thu, 30 May 2002 10:12:52 +0200  
changeset 13187  e5434b822a96 
parent 11868  56db9f3a6b3e 
child 13524  604d0f3622d6 
permissions  rwrr 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

1 
(* Title: HOL/NumberTheory/Chinese.thy 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

2 
ID: $Id$ 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

3 
Author: Thomas M. Rasmussen 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

4 
Copyright 2000 University of Cambridge 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

5 
*) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

6 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

7 
header {* The Chinese Remainder Theorem *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

8 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

9 
theory Chinese = IntPrimes: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

10 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

11 
text {* 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

12 
The Chinese Remainder Theorem for an arbitrary finite number of 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

13 
equations. (The oneequation case is included in theory @{text 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

14 
IntPrimes}. Uses functions for indexing.\footnote{Maybe @{term 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

15 
funprod} and @{term funsum} should be based on general @{term fold} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

16 
on indices?} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

17 
*} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

18 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

19 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

20 
subsection {* Definitions *} 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

21 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

22 
consts 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

23 
funprod :: "(nat => int) => nat => nat => int" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

24 
funsum :: "(nat => int) => nat => nat => int" 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

25 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

26 
primrec 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

27 
"funprod f i 0 = f i" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

28 
"funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n" 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

29 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

30 
primrec 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

31 
"funsum f i 0 = f i" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

32 
"funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n" 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

33 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

34 
consts 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

35 
m_cond :: "nat => (nat => int) => bool" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

36 
km_cond :: "nat => (nat => int) => (nat => int) => bool" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

37 
lincong_sol :: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

38 
"nat => (nat => int) => (nat => int) => (nat => int) => int => bool" 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

39 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

40 
mhf :: "(nat => int) => nat => nat => int" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

41 
xilin_sol :: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

42 
"nat => nat => (nat => int) => (nat => int) => (nat => int) => int" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

43 
x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int" 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

44 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

45 
defs 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

46 
m_cond_def: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

47 
"m_cond n mf == 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

48 
(\<forall>i. i \<le> n > 0 < mf i) \<and> 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

49 
(\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j > zgcd (mf i, mf j) = 1)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

50 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

51 
km_cond_def: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

52 
"km_cond n kf mf == \<forall>i. i \<le> n > zgcd (kf i, mf i) = 1" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

53 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

54 
lincong_sol_def: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

55 
"lincong_sol n kf bf mf x == \<forall>i. i \<le> n > zcong (kf i * x) (bf i) (mf i)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

56 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

57 
mhf_def: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

58 
"mhf mf n i == 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset

59 
if i = 0 then funprod mf (Suc 0) (n  Suc 0) 
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset

60 
else if i = n then funprod mf 0 (n  Suc 0) 
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset

61 
else funprod mf 0 (i  Suc 0) * funprod mf (Suc i) (n  Suc 0  i)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

62 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

63 
xilin_sol_def: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

64 
"xilin_sol i n kf bf mf == 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

65 
if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

66 
(SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i)) 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

67 
else 0" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

68 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

69 
x_sol_def: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

70 
"x_sol n kf bf mf == funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

71 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

72 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

73 
text {* \medskip @{term funprod} and @{term funsum} *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

74 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

75 
lemma funprod_pos: "(\<forall>i. i \<le> n > 0 < mf i) ==> 0 < funprod mf 0 n" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

76 
apply (induct n) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

77 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

78 
apply (simp add: int_0_less_mult_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

79 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

80 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

81 
lemma funprod_zgcd [rule_format (no_asm)]: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

82 
"(\<forall>i. k \<le> i \<and> i \<le> k + l > zgcd (mf i, mf m) = 1) > 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

83 
zgcd (funprod mf k l, mf m) = 1" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

84 
apply (induct l) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

85 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

86 
apply (rule impI)+ 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

87 
apply (subst zgcd_zmult_cancel) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

88 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

89 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

90 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

91 
lemma funprod_zdvd [rule_format]: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

92 
"k \<le> i > i \<le> k + l > mf i dvd funprod mf k l" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

93 
apply (induct l) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

94 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

95 
apply (rule_tac [2] zdvd_zmult2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

96 
apply (rule_tac [3] zdvd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

97 
apply (subgoal_tac "i = k") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

98 
apply (subgoal_tac [3] "i = Suc (k + n)") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

99 
apply (simp_all (no_asm_simp)) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

100 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

101 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

102 
lemma funsum_mod: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

103 
"funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

104 
apply (induct l) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

105 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

106 
apply (rule trans) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

107 
apply (rule zmod_zadd1_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

108 
apply simp 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

109 
apply (rule zmod_zadd_right_eq [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

110 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

111 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

112 
lemma funsum_zero [rule_format (no_asm)]: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

113 
"(\<forall>i. k \<le> i \<and> i \<le> k + l > f i = 0) > (funsum f k l) = 0" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

114 
apply (induct l) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

115 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

116 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

117 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

118 
lemma funsum_oneelem [rule_format (no_asm)]: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

119 
"k \<le> j > j \<le> k + l > 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

120 
(\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j > f i = 0) > 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

121 
funsum f k l = f j" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

122 
apply (induct l) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

123 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

124 
apply clarify 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

125 
defer 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

126 
apply clarify 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

127 
apply (subgoal_tac "k = j") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

128 
apply (simp_all (no_asm_simp)) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

129 
apply (case_tac "Suc (k + n) = j") 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

130 
apply (subgoal_tac "funsum f k n = 0") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

131 
apply (rule_tac [2] funsum_zero) 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

132 
apply (subgoal_tac [3] "f (Suc (k + n)) = 0") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

133 
apply (subgoal_tac [3] "j \<le> k + n") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

134 
prefer 4 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

135 
apply arith 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

136 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

137 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

138 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

139 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

140 
subsection {* Chinese: uniqueness *} 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

141 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

142 
lemma aux: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

143 
"m_cond n mf ==> km_cond n kf mf 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

144 
==> lincong_sol n kf bf mf x ==> lincong_sol n kf bf mf y 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

145 
==> [x = y] (mod mf n)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

146 
apply (unfold m_cond_def km_cond_def lincong_sol_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

147 
apply (rule iffD1) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

148 
apply (rule_tac k = "kf n" in zcong_cancel2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

149 
apply (rule_tac [3] b = "bf n" in zcong_trans) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

150 
prefer 4 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

151 
apply (subst zcong_sym) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

152 
defer 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

153 
apply (rule order_less_imp_le) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

154 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

155 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

156 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

157 
lemma zcong_funprod [rule_format]: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

158 
"m_cond n mf > km_cond n kf mf > 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

159 
lincong_sol n kf bf mf x > lincong_sol n kf bf mf y > 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

160 
[x = y] (mod funprod mf 0 n)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

161 
apply (induct n) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

162 
apply (simp_all (no_asm)) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

163 
apply (blast intro: aux) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

164 
apply (rule impI)+ 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

165 
apply (rule zcong_zgcd_zmult_zmod) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

166 
apply (blast intro: aux) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

167 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

168 
apply (subst zgcd_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

169 
apply (rule funprod_zgcd) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

170 
apply (auto simp add: m_cond_def km_cond_def lincong_sol_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

171 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

172 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

173 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

174 
subsection {* Chinese: existence *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

175 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

176 
lemma unique_xi_sol: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

177 
"0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

178 
==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

179 
apply (rule zcong_lineq_unique) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

180 
apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *}) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

181 
apply (unfold m_cond_def km_cond_def mhf_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

182 
apply (simp_all (no_asm_simp)) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

183 
apply safe 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

184 
apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *}) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

185 
apply (rule_tac [!] funprod_zgcd) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

186 
apply safe 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

187 
apply simp_all 
13187  188 
apply (subgoal_tac "i<n") 
189 
prefer 2 

190 
apply arith 

191 
apply (case_tac [2] i) 

192 
apply simp_all 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

193 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

194 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

195 
lemma aux: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

196 
"0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

197 
apply (unfold mhf_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

198 
apply (case_tac "i = 0") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

199 
apply (case_tac [2] "i = n") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

200 
apply (simp_all (no_asm_simp)) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

201 
apply (case_tac [3] "j < i") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

202 
apply (rule_tac [3] zdvd_zmult2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

203 
apply (rule_tac [4] zdvd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

204 
apply (rule_tac [!] funprod_zdvd) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

205 
apply arith+ 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

206 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

207 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

208 
lemma x_sol_lin: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

209 
"0 < n ==> i \<le> n 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

210 
==> x_sol n kf bf mf mod mf i = 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

211 
xilin_sol i n kf bf mf * mhf mf n i mod mf i" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

212 
apply (unfold x_sol_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

213 
apply (subst funsum_mod) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

214 
apply (subst funsum_oneelem) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

215 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

216 
apply (subst zdvd_iff_zmod_eq_0 [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

217 
apply (rule zdvd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

218 
apply (rule aux) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

219 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

220 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

221 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

222 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

223 
subsection {* Chinese *} 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

224 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

225 
lemma chinese_remainder: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

226 
"0 < n ==> m_cond n mf ==> km_cond n kf mf 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

227 
==> \<exists>!x. 0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

228 
apply safe 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

229 
apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

230 
apply (rule_tac [6] zcong_funprod) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

231 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

232 
apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

233 
apply (unfold lincong_sol_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

234 
apply safe 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

235 
apply (tactic {* stac (thm "zcong_zmod") 3 *}) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

236 
apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *}) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

237 
apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *}) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

238 
apply (tactic {* stac (thm "x_sol_lin") 5 *}) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

239 
apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *}) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

240 
apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *}) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

241 
apply (subgoal_tac [7] 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

242 
"0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

243 
\<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

244 
prefer 7 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

245 
apply (simp add: zmult_ac) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

246 
apply (unfold xilin_sol_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

247 
apply (tactic {* Asm_simp_tac 7 *}) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

248 
apply (rule_tac [7] ex1_implies_ex [THEN someI_ex]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

249 
apply (rule_tac [7] unique_xi_sol) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

250 
apply (rule_tac [4] funprod_zdvd) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

251 
apply (unfold m_cond_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

252 
apply (rule funprod_pos [THEN pos_mod_sign]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

253 
apply (rule_tac [2] funprod_pos [THEN pos_mod_bound]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

254 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

255 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

256 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

257 
end 