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