1 (* Title : EvenOdd.thy |
1 (* Title : EvenOdd.thy |
|
2 ID: $Id$ |
2 Author : Jacques D. Fleuriot |
3 Author : Jacques D. Fleuriot |
3 Copyright : 1999 University of Edinburgh |
4 Copyright : 1999 University of Edinburgh |
4 Description : Even and odd numbers defined |
|
5 *) |
5 *) |
6 |
6 |
7 header{*Compatibility file from Parity*} |
7 header{*Even and Odd Numbers: Compatibility file for Parity*} |
8 |
8 |
9 theory EvenOdd = NthRoot: |
9 theory EvenOdd = NthRoot: |
10 |
10 |
11 subsection{*General Lemmas About Division*} |
11 subsection{*General Lemmas About Division*} |
12 |
12 |
13 lemma div_add_self_two_is_m: "(m + m) div 2 = (m::nat)" |
13 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" |
|
14 apply (induct_tac "m") |
|
15 apply (simp_all add: mod_Suc) |
|
16 done |
|
17 |
|
18 declare Suc_times_mod_eq [of "number_of w", standard, simp] |
|
19 |
|
20 lemma [simp]: "n div k \<le> (Suc n) div k" |
|
21 by (simp add: div_le_mono) |
|
22 |
|
23 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2" |
14 by arith |
24 by arith |
15 declare div_add_self_two_is_m [simp] |
|
16 |
25 |
17 lemma div_mult_self_Suc_Suc: "Suc(Suc(m*2)) div 2 = Suc m" |
26 lemma div_2_gt_zero [simp]: "(1::nat) < n ==> 0 < n div 2" |
18 by arith |
27 by arith |
19 declare div_mult_self_Suc_Suc [simp] |
|
20 |
28 |
21 lemma div_mult_self_Suc_Suc2: "Suc(Suc(2*m)) div 2 = Suc m" |
29 lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)" |
22 by arith |
30 by (simp add: mult_ac add_ac) |
23 declare div_mult_self_Suc_Suc2 [simp] |
|
24 |
31 |
25 lemma div_add_self_Suc_Suc: "Suc(Suc(m + m)) div 2 = Suc m" |
32 lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n" |
26 by arith |
|
27 declare div_add_self_Suc_Suc [simp] |
|
28 |
|
29 lemma mod_two_Suc_2m: "Suc (2 * m) mod 2 = 1" |
|
30 apply (induct_tac "m") |
|
31 apply (auto simp add: mod_Suc) |
|
32 done |
|
33 declare mod_two_Suc_2m [simp] |
|
34 |
|
35 lemma Suc_n_le_Suc_Suc_n_div_2: "Suc n div 2 \<le> Suc (Suc n) div 2" |
|
36 by arith |
|
37 declare Suc_n_le_Suc_Suc_n_div_2 [simp] |
|
38 |
|
39 lemma Suc_n_div_2_gt_zero: "(0::nat) < n ==> 0 < (n + 1) div 2" |
|
40 by arith |
|
41 declare Suc_n_div_2_gt_zero [simp] |
|
42 |
|
43 lemma le_Suc_n_div_2: "n div 2 \<le> (Suc n) div 2" |
|
44 by arith |
|
45 declare le_Suc_n_div_2 [simp] |
|
46 |
|
47 lemma div_2_gt_zero: "(1::nat) < n ==> 0 < n div 2" |
|
48 by arith |
|
49 declare div_2_gt_zero [simp] |
|
50 |
|
51 lemma mod_mult_self3: "(k*n + m) mod n = m mod (n::nat)" |
|
52 by (simp add: mult_ac add_ac) |
|
53 declare mod_mult_self3 [simp] |
|
54 |
|
55 lemma mod_mult_self4: "Suc (k*n + m) mod n = Suc m mod n" |
|
56 proof - |
33 proof - |
57 have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp |
34 have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp |
58 also have "... = Suc m mod n" by (rule mod_mult_self3) |
35 also have "... = Suc m mod n" by (rule mod_mult_self3) |
59 finally show ?thesis . |
36 finally show ?thesis . |
60 qed |
37 qed |
61 declare mod_mult_self4 [simp] |
|
62 |
|
63 lemma nat_mod_idem [simp]: "m mod n mod n = (m mod n :: nat)" |
|
64 by (case_tac "n=0", auto) |
|
65 |
38 |
66 lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n" |
39 lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n" |
67 apply (subst mod_Suc [of m]) |
40 apply (subst mod_Suc [of m]) |
68 apply (subst mod_Suc [of "m mod n"], simp) |
41 apply (subst mod_Suc [of "m mod n"], simp) |
69 done |
42 done |
70 |
43 |
71 lemma lemma_4n_add_2_div_2_eq: "((4 * n) + 2) div 2 = (2::nat) * n + 1" |
|
72 by arith |
|
73 declare lemma_4n_add_2_div_2_eq [simp] |
|
74 |
|
75 lemma lemma_Suc_Suc_4n_div_2_eq: "(Suc(Suc(4 * n))) div 2 = (2::nat) * n + 1" |
|
76 by arith |
|
77 declare lemma_Suc_Suc_4n_div_2_eq [simp] |
|
78 |
|
79 lemma lemma_Suc_Suc_4n_div_2_eq2: "(Suc(Suc(n * 4))) div 2 = (2::nat) * n + 1" |
|
80 by arith |
|
81 declare lemma_Suc_Suc_4n_div_2_eq2 [simp] |
|
82 |
|
83 |
44 |
84 subsection{*More Even/Odd Results*} |
45 subsection{*More Even/Odd Results*} |
85 |
46 |
86 lemma even_mult_two_ex: "even(n) = (EX m::nat. n = 2*m)" |
47 lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)" |
87 by (simp add: even_nat_equiv_def2 numeral_2_eq_2) |
48 by (simp add: even_nat_equiv_def2 numeral_2_eq_2) |
88 |
49 |
89 lemma odd_Suc_mult_two_ex: "odd(n) = (EX m. n = Suc (2*m))" |
50 lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))" |
90 by (simp add: odd_nat_equiv_def2 numeral_2_eq_2) |
51 by (simp add: odd_nat_equiv_def2 numeral_2_eq_2) |
91 |
52 |
92 lemma even_add: "even(m + n::nat) = (even m = even n)" |
53 lemma even_add [simp]: "even(m + n::nat) = (even m = even n)" |
93 by auto |
54 by auto |
94 declare even_add [iff] |
|
95 |
55 |
96 lemma odd_add: "odd(m + n::nat) = (odd m ~= odd n)" |
56 lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)" |
97 by auto |
57 by auto |
98 declare odd_add [iff] |
|
99 |
58 |
100 lemma lemma_even_div2: "even (n::nat) ==> (n + 1) div 2 = n div 2" |
59 lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" |
101 apply (simp add: numeral_2_eq_2) |
60 apply (simp add: numeral_2_eq_2) |
102 apply (subst div_Suc) |
61 apply (subst div_Suc) |
103 apply (simp add: even_nat_mod_two_eq_zero) |
62 apply (simp add: even_nat_mod_two_eq_zero) |
104 done |
63 done |
105 declare lemma_even_div2 [simp] |
|
106 |
64 |
107 lemma lemma_not_even_div2: "~even n ==> (n + 1) div 2 = Suc (n div 2)" |
65 lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)" |
108 apply (simp add: numeral_2_eq_2) |
66 apply (simp add: numeral_2_eq_2) |
109 apply (subst div_Suc) |
67 apply (subst div_Suc) |
110 apply (simp add: odd_nat_mod_two_eq_one) |
68 apply (simp add: odd_nat_mod_two_eq_one) |
111 done |
69 done |
112 declare lemma_not_even_div2 [simp] |
|
113 |
70 |
114 lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))" |
71 lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))" |
115 by (case_tac "n", auto) |
72 by (case_tac "n", auto) |
116 |
73 |
117 lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" |
74 lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" |
118 apply (induct n, simp) |
75 apply (induct n, simp) |
119 apply (subst mod_Suc, simp) |
76 apply (subst mod_Suc, simp) |
120 done |
77 done |
121 |
|
122 declare neg_one_odd_power [simp] |
|
123 declare neg_one_even_power [simp] |
|
124 |
78 |
125 lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)" |
79 lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)" |
126 apply (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst]) |
80 apply (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst]) |
127 apply (simp add: even_num_iff) |
81 apply (simp add: even_num_iff) |
128 done |
82 done |
130 lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)" |
84 lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)" |
131 by (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst], simp) |
85 by (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst], simp) |
132 |
86 |
133 ML |
87 ML |
134 {* |
88 {* |
135 val even_Suc = thm"Parity.even_nat_suc"; |
89 val even_nat_Suc = thm"Parity.even_nat_Suc"; |
136 |
90 |
137 val even_mult_two_ex = thm "even_mult_two_ex"; |
91 val even_mult_two_ex = thm "even_mult_two_ex"; |
138 val odd_Suc_mult_two_ex = thm "odd_Suc_mult_two_ex"; |
92 val odd_Suc_mult_two_ex = thm "odd_Suc_mult_two_ex"; |
139 val div_add_self_two_is_m = thm "div_add_self_two_is_m"; |
|
140 val div_mult_self_Suc_Suc = thm "div_mult_self_Suc_Suc"; |
|
141 val div_mult_self_Suc_Suc2 = thm "div_mult_self_Suc_Suc2"; |
|
142 val div_add_self_Suc_Suc = thm "div_add_self_Suc_Suc"; |
|
143 val even_add = thm "even_add"; |
93 val even_add = thm "even_add"; |
144 val odd_add = thm "odd_add"; |
94 val odd_add = thm "odd_add"; |
145 val mod_two_Suc_2m = thm "mod_two_Suc_2m"; |
|
146 val Suc_n_le_Suc_Suc_n_div_2 = thm "Suc_n_le_Suc_Suc_n_div_2"; |
|
147 val Suc_n_div_2_gt_zero = thm "Suc_n_div_2_gt_zero"; |
95 val Suc_n_div_2_gt_zero = thm "Suc_n_div_2_gt_zero"; |
148 val le_Suc_n_div_2 = thm "le_Suc_n_div_2"; |
|
149 val div_2_gt_zero = thm "div_2_gt_zero"; |
96 val div_2_gt_zero = thm "div_2_gt_zero"; |
150 val lemma_even_div2 = thm "lemma_even_div2"; |
|
151 val lemma_not_even_div2 = thm "lemma_not_even_div2"; |
|
152 val even_num_iff = thm "even_num_iff"; |
97 val even_num_iff = thm "even_num_iff"; |
153 val mod_mult_self3 = thm "mod_mult_self3"; |
98 val nat_mod_div_trivial = thm "nat_mod_div_trivial"; |
154 val mod_mult_self4 = thm "mod_mult_self4"; |
99 val nat_mod_mod_trivial = thm "nat_mod_mod_trivial"; |
155 val nat_mod_idem = thm "nat_mod_idem"; |
|
156 val mod_Suc_eq_Suc_mod = thm "mod_Suc_eq_Suc_mod"; |
100 val mod_Suc_eq_Suc_mod = thm "mod_Suc_eq_Suc_mod"; |
157 val even_even_mod_4_iff = thm "even_even_mod_4_iff"; |
101 val even_even_mod_4_iff = thm "even_even_mod_4_iff"; |
158 val lemma_4n_add_2_div_2_eq = thm "lemma_4n_add_2_div_2_eq"; |
|
159 val lemma_Suc_Suc_4n_div_2_eq = thm "lemma_Suc_Suc_4n_div_2_eq"; |
|
160 val lemma_Suc_Suc_4n_div_2_eq2 = thm "lemma_Suc_Suc_4n_div_2_eq2"; |
|
161 val lemma_odd_mod_4_div_2 = thm "lemma_odd_mod_4_div_2"; |
102 val lemma_odd_mod_4_div_2 = thm "lemma_odd_mod_4_div_2"; |
162 val lemma_even_mod_4_div_2 = thm "lemma_even_mod_4_div_2"; |
103 val lemma_even_mod_4_div_2 = thm "lemma_even_mod_4_div_2"; |
163 *} |
104 *} |
164 |
105 |
165 end |
106 end |