author | paulson |
Mon, 22 Oct 2001 11:54:22 +0200 | |
changeset 11868 | 56db9f3a6b3e |
parent 11704 | 3c50a2cd6f00 |
child 12196 | a3be6b3a9c0b |
permissions | -rw-r--r-- |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
1 |
(* Title: HOL/nat_bin.ML |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
5 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
6 |
Binary arithmetic for the natural numbers |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
7 |
*) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
8 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
9 |
val nat_number_of_def = thm "nat_number_of_def"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
10 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
11 |
(** nat (coercion from int to nat) **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
12 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
13 |
Goal "nat (number_of w) = number_of w"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
14 |
by (simp_tac (simpset() addsimps [nat_number_of_def]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
15 |
qed "nat_number_of"; |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
16 |
Addsimps [nat_number_of, nat_0, nat_1]; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
17 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
18 |
Goal "Numeral0 = (0::nat)"; |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
19 |
by (simp_tac (simpset() addsimps [nat_number_of_def]) 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
20 |
qed "numeral_0_eq_0"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
21 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
22 |
Goal "Numeral1 = (1::nat)"; |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
23 |
by (simp_tac (simpset() addsimps [nat_1, nat_number_of_def]) 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
24 |
qed "numeral_1_eq_1"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
25 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
26 |
Goal "Numeral1 = Suc 0"; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
27 |
by (simp_tac (simpset() addsimps [numeral_1_eq_1]) 1); |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
28 |
qed "numeral_1_eq_Suc_0"; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
29 |
|
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
30 |
Goalw [nat_number_of_def, One_nat_def] "2 = Suc 1"; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
31 |
by (rtac nat_2 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
32 |
qed "numeral_2_eq_2"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
33 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
34 |
(** int (coercion from nat to int) **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
35 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
36 |
(*"neg" is used in rewrite rules for binary comparisons*) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
37 |
Goal "int (number_of v :: nat) = \ |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
38 |
\ (if neg (number_of v) then 0 \ |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
39 |
\ else (number_of v :: int))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
40 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
41 |
(simpset_of Int.thy addsimps [neg_nat, nat_number_of_def, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
42 |
not_neg_nat, int_0]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
43 |
qed "int_nat_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
44 |
Addsimps [int_nat_number_of]; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
45 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
46 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
47 |
val nat_bin_arith_setup = |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
48 |
[Fast_Arith.map_data |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
49 |
(fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
50 |
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
51 |
inj_thms = inj_thms, |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
52 |
lessD = lessD, |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
53 |
simpset = simpset addsimps [int_nat_number_of, not_neg_number_of_Pls, |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
54 |
neg_number_of_Min,neg_number_of_BIT]})]; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
55 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
56 |
(** Successor **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
57 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
58 |
Goal "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
59 |
by (rtac sym 1); |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
60 |
by (asm_simp_tac (simpset() addsimps [nat_eq_iff, int_Suc]) 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
61 |
qed "Suc_nat_eq_nat_zadd1"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
62 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
63 |
Goal "Suc (number_of v + n) = \ |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
64 |
\ (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
65 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
66 |
(simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
67 |
nat_number_of_def, int_Suc, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
68 |
Suc_nat_eq_nat_zadd1, number_of_succ]) 1); |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
69 |
qed "Suc_nat_number_of_add"; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
70 |
|
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
71 |
Goal "Suc (number_of v) = \ |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
72 |
\ (if neg (number_of v) then 1 else number_of (bin_succ v))"; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
73 |
by (cut_inst_tac [("n","0")] Suc_nat_number_of_add 1); |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
74 |
by (asm_full_simp_tac (simpset() delcongs [if_weak_cong]) 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
75 |
qed "Suc_nat_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
76 |
Addsimps [Suc_nat_number_of]; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
77 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
78 |
(** Addition **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
79 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
80 |
Goal "[| (0::int) <= z; 0 <= z' |] ==> nat (z+z') = nat z + nat z'"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
81 |
by (rtac (inj_int RS injD) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
82 |
by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
83 |
qed "nat_add_distrib"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
84 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
85 |
(*"neg" is used in rewrite rules for binary comparisons*) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
86 |
Goal "(number_of v :: nat) + number_of v' = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
87 |
\ (if neg (number_of v) then number_of v' \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
88 |
\ else if neg (number_of v') then number_of v \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
89 |
\ else number_of (bin_add v v'))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
90 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
91 |
(simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
92 |
nat_add_distrib RS sym, number_of_add]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
93 |
qed "add_nat_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
94 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
95 |
Addsimps [add_nat_number_of]; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
96 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
97 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
98 |
(** Subtraction **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
99 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
100 |
Goal "[| (0::int) <= z'; z' <= z |] ==> nat (z-z') = nat z - nat z'"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
101 |
by (rtac (inj_int RS injD) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
102 |
by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
103 |
qed "nat_diff_distrib"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
104 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
105 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
106 |
Goal "nat z - nat z' = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
107 |
\ (if neg z' then nat z \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
108 |
\ else let d = z-z' in \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
109 |
\ if neg d then 0 else nat d)"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
110 |
by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
111 |
neg_eq_less_0, not_neg_eq_ge_0]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
112 |
by (simp_tac (simpset() addsimps [diff_is_0_eq, nat_le_eq_zle]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
113 |
qed "diff_nat_eq_if"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
114 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
115 |
Goalw [nat_number_of_def] |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
116 |
"(number_of v :: nat) - number_of v' = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
117 |
\ (if neg (number_of v') then number_of v \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
118 |
\ else let d = number_of (bin_add v (bin_minus v')) in \ |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
119 |
\ if neg d then 0 else nat d)"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
120 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
121 |
(simpset_of Int.thy delcongs [if_weak_cong] |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
122 |
addsimps [not_neg_eq_ge_0, nat_0, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
123 |
diff_nat_eq_if, diff_number_of_eq]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
124 |
qed "diff_nat_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
125 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
126 |
Addsimps [diff_nat_number_of]; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
127 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
128 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
129 |
(** Multiplication **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
130 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
131 |
Goal "(0::int) <= z ==> nat (z*z') = nat z * nat z'"; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
132 |
by (case_tac "0 <= z'" 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
133 |
by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
134 |
by (rtac (inj_int RS injD) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
135 |
by (asm_simp_tac (simpset() addsimps [zmult_int RS sym, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
136 |
int_0_le_mult_iff]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
137 |
qed "nat_mult_distrib"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
138 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
139 |
Goal "z <= (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
140 |
by (rtac trans 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
141 |
by (rtac nat_mult_distrib 2); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
142 |
by Auto_tac; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
143 |
qed "nat_mult_distrib_neg"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
144 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
145 |
Goal "(number_of v :: nat) * number_of v' = \ |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
146 |
\ (if neg (number_of v) then 0 else number_of (bin_mult v v'))"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
147 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
148 |
(simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
149 |
nat_mult_distrib RS sym, number_of_mult, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
150 |
nat_0]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
151 |
qed "mult_nat_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
152 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
153 |
Addsimps [mult_nat_number_of]; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
154 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
155 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
156 |
(** Quotient **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
157 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
158 |
Goal "(0::int) <= z ==> nat (z div z') = nat z div nat z'"; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
159 |
by (case_tac "0 <= z'" 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
160 |
by (auto_tac (claset(), |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
161 |
simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV])); |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
162 |
by (zdiv_undefined_case_tac "z' = 0" 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
163 |
by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
164 |
by (auto_tac (claset() addSEs [nonneg_eq_int], simpset())); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
165 |
by (rename_tac "m m'" 1); |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
166 |
by (subgoal_tac "0 <= int m div int m'" 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
167 |
by (asm_full_simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
168 |
(simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
169 |
by (rtac (inj_int RS injD) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
170 |
by (Asm_simp_tac 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
171 |
by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
172 |
by (Force_tac 2); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
173 |
by (asm_full_simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
174 |
(simpset() addsimps [nat_less_iff RS sym, quorem_def, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
175 |
numeral_0_eq_0, zadd_int, zmult_int]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
176 |
by (rtac (mod_div_equality RS sym RS trans) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
177 |
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
178 |
qed "nat_div_distrib"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
179 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
180 |
Goal "(number_of v :: nat) div number_of v' = \ |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
181 |
\ (if neg (number_of v) then 0 \ |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
182 |
\ else nat (number_of v div number_of v'))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
183 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
184 |
(simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
185 |
nat_div_distrib RS sym, nat_0]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
186 |
qed "div_nat_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
187 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
188 |
Addsimps [div_nat_number_of]; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
189 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
190 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
191 |
(** Remainder **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
192 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
193 |
(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
194 |
Goal "[| (0::int) <= z; 0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
195 |
by (zdiv_undefined_case_tac "z' = 0" 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
196 |
by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
197 |
by (auto_tac (claset() addSEs [nonneg_eq_int], simpset())); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
198 |
by (rename_tac "m m'" 1); |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
199 |
by (subgoal_tac "0 <= int m mod int m'" 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
200 |
by (asm_full_simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
201 |
(simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
202 |
by (rtac (inj_int RS injD) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
203 |
by (Asm_simp_tac 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
204 |
by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
205 |
by (Force_tac 2); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
206 |
by (asm_full_simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
207 |
(simpset() addsimps [nat_less_iff RS sym, quorem_def, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
208 |
numeral_0_eq_0, zadd_int, zmult_int]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
209 |
by (rtac (mod_div_equality RS sym RS trans) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
210 |
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
211 |
qed "nat_mod_distrib"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
212 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
213 |
Goal "(number_of v :: nat) mod number_of v' = \ |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
214 |
\ (if neg (number_of v) then 0 \ |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
215 |
\ else if neg (number_of v') then number_of v \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
216 |
\ else nat (number_of v mod number_of v'))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
217 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
218 |
(simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
219 |
neg_nat, nat_0, DIVISION_BY_ZERO_MOD, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
220 |
nat_mod_distrib RS sym]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
221 |
qed "mod_nat_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
222 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
223 |
Addsimps [mod_nat_number_of]; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
224 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
225 |
structure NatAbstractNumeralsData = |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
226 |
struct |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
227 |
val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
228 |
val is_numeral = Bin_Simprocs.is_numeral |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
229 |
val numeral_0_eq_0 = numeral_0_eq_0 |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
230 |
val numeral_1_eq_1 = numeral_1_eq_Suc_0 |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
231 |
val prove_conv = Bin_Simprocs.prove_conv_nohyps "nat_abstract_numerals" |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
232 |
fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps)) |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
233 |
val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
234 |
end |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
235 |
|
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
236 |
structure NatAbstractNumerals = AbstractNumeralsFun (NatAbstractNumeralsData) |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
237 |
|
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
238 |
val nat_eval_numerals = |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
239 |
map Bin_Simprocs.prep_simproc |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
240 |
[("nat_div_eval_numerals", |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
241 |
Bin_Simprocs.prep_pats ["(Suc 0) div m"], |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
242 |
NatAbstractNumerals.proc div_nat_number_of), |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
243 |
("nat_mod_eval_numerals", |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
244 |
Bin_Simprocs.prep_pats ["(Suc 0) mod m"], |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
245 |
NatAbstractNumerals.proc mod_nat_number_of)]; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
246 |
|
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
247 |
Addsimprocs nat_eval_numerals; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
248 |
|
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
249 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
250 |
(*** Comparisons ***) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
251 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
252 |
(** Equals (=) **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
253 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
254 |
Goal "[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
255 |
by (auto_tac (claset() addSEs [nonneg_eq_int], simpset())); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
256 |
qed "eq_nat_nat_iff"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
257 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
258 |
(*"neg" is used in rewrite rules for binary comparisons*) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
259 |
Goal "((number_of v :: nat) = number_of v') = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
260 |
\ (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
261 |
\ else if neg (number_of v') then iszero (number_of v) \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
262 |
\ else iszero (number_of (bin_add v (bin_minus v'))))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
263 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
264 |
(simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
265 |
eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
266 |
by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, nat_eq_iff2, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
267 |
iszero_def]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
268 |
by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
269 |
qed "eq_nat_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
270 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
271 |
Addsimps [eq_nat_number_of]; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
272 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
273 |
(** Less-than (<) **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
274 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
275 |
(*"neg" is used in rewrite rules for binary comparisons*) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
276 |
Goal "((number_of v :: nat) < number_of v') = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
277 |
\ (if neg (number_of v) then neg (number_of (bin_minus v')) \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
278 |
\ else neg (number_of (bin_add v (bin_minus v'))))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
279 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
280 |
(simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
281 |
nat_less_eq_zless, less_number_of_eq_neg, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
282 |
nat_0]) 1); |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
283 |
by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_0, zminus_zless, |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
284 |
number_of_minus, zless_nat_eq_int_zless]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
285 |
qed "less_nat_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
286 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
287 |
Addsimps [less_nat_number_of]; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
288 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
289 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
290 |
(** Less-than-or-equals (<=) **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
291 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
292 |
Goal "(number_of x <= (number_of y::nat)) = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
293 |
\ (~ number_of y < (number_of x::nat))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
294 |
by (rtac (linorder_not_less RS sym) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
295 |
qed "le_nat_number_of_eq_not_less"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
296 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
297 |
Addsimps [le_nat_number_of_eq_not_less]; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
298 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
299 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
300 |
(*Maps #n to n for n = 0, 1, 2*) |
11018 | 301 |
bind_thms ("numerals", [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2]); |
302 |
val numeral_ss = simpset() addsimps numerals; |
|
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
303 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
304 |
(** Nat **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
305 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
306 |
Goal "0 < n ==> n = Suc(n - 1)"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
307 |
by (asm_full_simp_tac numeral_ss 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
308 |
qed "Suc_pred'"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
309 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
310 |
(*Expresses a natural number constant as the Suc of another one. |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
311 |
NOT suitable for rewriting because n recurs in the condition.*) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
312 |
bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred'); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
313 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
314 |
(** Arith **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
315 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
316 |
Goal "Suc n = n + 1"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
317 |
by (asm_simp_tac numeral_ss 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
318 |
qed "Suc_eq_add_numeral_1"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
319 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
320 |
(* These two can be useful when m = number_of... *) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
321 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
322 |
Goal "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
323 |
by (case_tac "m" 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
324 |
by (ALLGOALS (asm_simp_tac numeral_ss)); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
325 |
qed "add_eq_if"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
326 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
327 |
Goal "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
328 |
by (case_tac "m" 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
329 |
by (ALLGOALS (asm_simp_tac numeral_ss)); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
330 |
qed "mult_eq_if"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
331 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
332 |
Goal "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
333 |
by (case_tac "m" 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
334 |
by (ALLGOALS (asm_simp_tac numeral_ss)); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
335 |
qed "power_eq_if"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
336 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
337 |
Goal "[| 0<n; 0<m |] ==> m - n < (m::nat)"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
338 |
by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
339 |
qed "diff_less'"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
340 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
341 |
Addsimps [inst "n" "number_of ?v" diff_less']; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
342 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
343 |
(** Power **) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
344 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
345 |
Goal "(p::nat) ^ 2 = p*p"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
346 |
by (simp_tac numeral_ss 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
347 |
qed "power_two"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
348 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
349 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
350 |
(*** Comparisons involving (0::nat) ***) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
351 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
352 |
Goal "(number_of v = (0::nat)) = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
353 |
\ (if neg (number_of v) then True else iszero (number_of v))"; |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
354 |
by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1); |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
355 |
qed "eq_number_of_0"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
356 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
357 |
Goal "((0::nat) = number_of v) = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
358 |
\ (if neg (number_of v) then True else iszero (number_of v))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
359 |
by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
360 |
qed "eq_0_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
361 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
362 |
Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
363 |
by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
364 |
qed "less_0_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
365 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
366 |
(*Simplification already handles n<0, n<=0 and 0<=n.*) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
367 |
Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of]; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
368 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
369 |
Goal "neg (number_of v) ==> number_of v = (0::nat)"; |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
370 |
by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
371 |
qed "neg_imp_number_of_eq_0"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
372 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
373 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
374 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
375 |
(*** Comparisons involving Suc ***) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
376 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
377 |
Goal "(number_of v = Suc n) = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
378 |
\ (let pv = number_of (bin_pred v) in \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
379 |
\ if neg pv then False else nat pv = n)"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
380 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
381 |
(simpset_of Int.thy addsimps |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
382 |
[Let_def, neg_eq_less_0, linorder_not_less, number_of_pred, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
383 |
nat_number_of_def, zadd_0] @ zadd_ac) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
384 |
by (res_inst_tac [("x", "number_of v")] spec 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
385 |
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff])); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
386 |
qed "eq_number_of_Suc"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
387 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
388 |
Goal "(Suc n = number_of v) = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
389 |
\ (let pv = number_of (bin_pred v) in \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
390 |
\ if neg pv then False else nat pv = n)"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
391 |
by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
392 |
qed "Suc_eq_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
393 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
394 |
Goal "(number_of v < Suc n) = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
395 |
\ (let pv = number_of (bin_pred v) in \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
396 |
\ if neg pv then True else nat pv < n)"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
397 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
398 |
(simpset_of Int.thy addsimps |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
399 |
[Let_def, neg_eq_less_0, linorder_not_less, number_of_pred, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
400 |
nat_number_of_def, zadd_0] @ zadd_ac) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
401 |
by (res_inst_tac [("x", "number_of v")] spec 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
402 |
by (auto_tac (claset(), simpset() addsimps [nat_less_iff])); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
403 |
qed "less_number_of_Suc"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
404 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
405 |
Goal "(Suc n < number_of v) = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
406 |
\ (let pv = number_of (bin_pred v) in \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
407 |
\ if neg pv then False else n < nat pv)"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
408 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
409 |
(simpset_of Int.thy addsimps |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
410 |
[Let_def, neg_eq_less_0, linorder_not_less, number_of_pred, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
411 |
nat_number_of_def, zadd_0] @ zadd_ac) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
412 |
by (res_inst_tac [("x", "number_of v")] spec 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
413 |
by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless])); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
414 |
qed "less_Suc_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
415 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
416 |
Goal "(number_of v <= Suc n) = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
417 |
\ (let pv = number_of (bin_pred v) in \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
418 |
\ if neg pv then True else nat pv <= n)"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
419 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
420 |
(simpset () addsimps |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
421 |
[Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
422 |
qed "le_number_of_Suc"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
423 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
424 |
Goal "(Suc n <= number_of v) = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
425 |
\ (let pv = number_of (bin_pred v) in \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
426 |
\ if neg pv then False else n <= nat pv)"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
427 |
by (simp_tac |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
428 |
(simpset () addsimps |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
429 |
[Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
430 |
qed "le_Suc_number_of"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
431 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
432 |
Addsimps [eq_number_of_Suc, Suc_eq_number_of, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
433 |
less_number_of_Suc, less_Suc_number_of, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
434 |
le_number_of_Suc, le_Suc_number_of]; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
435 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
436 |
(* Push int(.) inwards: *) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
437 |
Addsimps [zadd_int RS sym]; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
438 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
439 |
Goal "(m+m = n+n) = (m = (n::int))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
440 |
by Auto_tac; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
441 |
val lemma1 = result(); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
442 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
443 |
Goal "m+m ~= (1::int) + n + n"; |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
444 |
by Auto_tac; |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
445 |
by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
446 |
by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
447 |
val lemma2 = result(); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
448 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
449 |
Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
450 |
\ (x=y & (((number_of v) ::int) = number_of w))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
451 |
by (simp_tac (simpset_of Int.thy addsimps |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
452 |
[number_of_BIT, lemma1, lemma2, eq_commute]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
453 |
qed "eq_number_of_BIT_BIT"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
454 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
455 |
Goal "((number_of (v BIT x) ::int) = number_of Pls) = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
456 |
\ (x=False & (((number_of v) ::int) = number_of Pls))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
457 |
by (simp_tac (simpset_of Int.thy addsimps |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
458 |
[number_of_BIT, number_of_Pls, eq_commute]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
459 |
by (res_inst_tac [("x", "number_of v")] spec 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
460 |
by Safe_tac; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
461 |
by (ALLGOALS Full_simp_tac); |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
462 |
by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
463 |
by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
464 |
qed "eq_number_of_BIT_Pls"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
465 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
466 |
Goal "((number_of (v BIT x) ::int) = number_of Min) = \ |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
467 |
\ (x=True & (((number_of v) ::int) = number_of Min))"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
468 |
by (simp_tac (simpset_of Int.thy addsimps |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
469 |
[number_of_BIT, number_of_Min, eq_commute]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
470 |
by (res_inst_tac [("x", "number_of v")] spec 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
471 |
by Auto_tac; |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
472 |
by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
473 |
by Auto_tac; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
474 |
qed "eq_number_of_BIT_Min"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
475 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
476 |
Goal "(number_of Pls ::int) ~= number_of Min"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
477 |
by Auto_tac; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
478 |
qed "eq_number_of_Pls_Min"; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
479 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
480 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
481 |
(*** Further lemmas about "nat" ***) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
482 |
|
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
483 |
Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)"; |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
484 |
by (case_tac "z=0 | w=0" 1); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
485 |
by Auto_tac; |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
486 |
by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym, |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
487 |
nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
488 |
by (arith_tac 1); |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
diff
changeset
|
489 |
qed "nat_abs_mult_distrib"; |
10754
9bc30e51144c
now #16*(x+y) distributes for nat just as for other numeric types
paulson
parents:
10710
diff
changeset
|
490 |
|
9bc30e51144c
now #16*(x+y) distributes for nat just as for other numeric types
paulson
parents:
10710
diff
changeset
|
491 |
(*Distributive laws for literals*) |
9bc30e51144c
now #16*(x+y) distributes for nat just as for other numeric types
paulson
parents:
10710
diff
changeset
|
492 |
Addsimps (map (inst "k" "number_of ?v") |
9bc30e51144c
now #16*(x+y) distributes for nat just as for other numeric types
paulson
parents:
10710
diff
changeset
|
493 |
[add_mult_distrib, add_mult_distrib2, |
9bc30e51144c
now #16*(x+y) distributes for nat just as for other numeric types
paulson
parents:
10710
diff
changeset
|
494 |
diff_mult_distrib, diff_mult_distrib2]); |
9bc30e51144c
now #16*(x+y) distributes for nat just as for other numeric types
paulson
parents:
10710
diff
changeset
|
495 |