author | paulson |
Wed, 10 Dec 2003 15:59:34 +0100 | |
changeset 14288 | d149e3cbdb39 |
parent 14273 | e33ffff0123c |
child 14353 | 79f9fbef9106 |
permissions | -rw-r--r-- |
7032 | 1 |
(* Title: HOL/NatBin.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
12838 | 5 |
*) |
7032 | 6 |
|
12838 | 7 |
header {* Binary arithmetic for the natural numbers *} |
7032 | 8 |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
9 |
theory NatBin = IntPower: |
7032 | 10 |
|
12838 | 11 |
text {* |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
12 |
Arithmetic for naturals is reduced to that for the non-negative integers. |
12838 | 13 |
*} |
14 |
||
15 |
instance nat :: number .. |
|
16 |
||
17 |
defs (overloaded) |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
18 |
nat_number_of_def: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
19 |
"(number_of::bin => nat) v == nat ((number_of :: bin => int) v)" |
12838 | 20 |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
21 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
22 |
(** nat (coercion from int to nat) **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
23 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
24 |
declare nat_0 [simp] nat_1 [simp] |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
25 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
26 |
lemma nat_number_of [simp]: "nat (number_of w) = number_of w" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
27 |
by (simp add: nat_number_of_def) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
28 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
29 |
lemma numeral_0_eq_0: "Numeral0 = (0::nat)" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
30 |
by (simp add: nat_number_of_def) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
31 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
32 |
lemma numeral_1_eq_1: "Numeral1 = (1::nat)" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
33 |
by (simp add: nat_1 nat_number_of_def) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
34 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
35 |
lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
36 |
by (simp add: numeral_1_eq_1) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
37 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
38 |
lemma numeral_2_eq_2: "2 = Suc (Suc 0)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
39 |
apply (unfold nat_number_of_def) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
40 |
apply (rule nat_2) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
41 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
42 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
43 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
44 |
text{*Distributive laws for type @{text nat}. The others are in theory |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
45 |
@{text IntArith}, but these require div and mod to be defined for type |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
46 |
"int". They also need some of the lemmas proved above.*} |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
47 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
48 |
lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
49 |
apply (case_tac "0 <= z'") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
50 |
apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
51 |
apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
52 |
apply (auto elim!: nonneg_eq_int) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
53 |
apply (rename_tac m m') |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
54 |
apply (subgoal_tac "0 <= int m div int m'") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
55 |
prefer 2 apply (simp add: numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
56 |
apply (rule inj_int [THEN injD], simp) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
57 |
apply (rule_tac r = "int (m mod m') " in quorem_div) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
58 |
prefer 2 apply force |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
59 |
apply (simp add: nat_less_iff [symmetric] quorem_def numeral_0_eq_0 zadd_int |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
60 |
zmult_int) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
61 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
62 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
63 |
(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
64 |
lemma nat_mod_distrib: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
65 |
"[| (0::int) <= z; 0 <= z' |] ==> nat (z mod z') = nat z mod nat z'" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
66 |
apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
67 |
apply (auto elim!: nonneg_eq_int) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
68 |
apply (rename_tac m m') |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
69 |
apply (subgoal_tac "0 <= int m mod int m'") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
70 |
prefer 2 apply (simp add: nat_less_iff numeral_0_eq_0 pos_mod_sign) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
71 |
apply (rule inj_int [THEN injD], simp) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
72 |
apply (rule_tac q = "int (m div m') " in quorem_mod) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
73 |
prefer 2 apply force |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
74 |
apply (simp add: nat_less_iff [symmetric] quorem_def numeral_0_eq_0 zadd_int zmult_int) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
75 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
76 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
77 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
78 |
(** int (coercion from nat to int) **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
79 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
80 |
(*"neg" is used in rewrite rules for binary comparisons*) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
81 |
lemma int_nat_number_of: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
82 |
"int (number_of v :: nat) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
83 |
(if neg (number_of v) then 0 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
84 |
else (number_of v :: int))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
85 |
by (simp del: nat_number_of |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
86 |
add: neg_nat nat_number_of_def not_neg_nat add_assoc) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
87 |
declare int_nat_number_of [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
88 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
89 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
90 |
(** Successor **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
91 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
92 |
lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
93 |
apply (rule sym) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
94 |
apply (simp add: nat_eq_iff int_Suc) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
95 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
96 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
97 |
lemma Suc_nat_number_of_add: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
98 |
"Suc (number_of v + n) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
99 |
(if neg (number_of v) then 1+n else number_of (bin_succ v) + n)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
100 |
by (simp del: nat_number_of |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
101 |
add: nat_number_of_def neg_nat |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
102 |
Suc_nat_eq_nat_zadd1 number_of_succ) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
103 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
104 |
lemma Suc_nat_number_of: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
105 |
"Suc (number_of v) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
106 |
(if neg (number_of v) then 1 else number_of (bin_succ v))" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
107 |
apply (cut_tac n = 0 in Suc_nat_number_of_add) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
108 |
apply (simp cong del: if_weak_cong) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
109 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
110 |
declare Suc_nat_number_of [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
111 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
112 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
113 |
(** Addition **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
114 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
115 |
(*"neg" is used in rewrite rules for binary comparisons*) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
116 |
lemma add_nat_number_of: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
117 |
"(number_of v :: nat) + number_of v' = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
118 |
(if neg (number_of v) then number_of v' |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
119 |
else if neg (number_of v') then number_of v |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
120 |
else number_of (bin_add v v'))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
121 |
by (force dest!: neg_nat |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
122 |
simp del: nat_number_of |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
123 |
simp add: nat_number_of_def nat_add_distrib [symmetric]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
124 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
125 |
declare add_nat_number_of [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
126 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
127 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
128 |
(** Subtraction **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
129 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
130 |
lemma diff_nat_eq_if: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
131 |
"nat z - nat z' = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
132 |
(if neg z' then nat z |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
133 |
else let d = z-z' in |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
134 |
if neg d then 0 else nat d)" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
135 |
apply (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
136 |
apply (simp add: diff_is_0_eq nat_le_eq_zle) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
137 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
138 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
139 |
lemma diff_nat_number_of: |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
140 |
"(number_of v :: nat) - number_of v' = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
141 |
(if neg (number_of v') then number_of v |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
142 |
else let d = number_of (bin_add v (bin_minus v')) in |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
143 |
if neg d then 0 else nat d)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
144 |
by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
145 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
146 |
declare diff_nat_number_of [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
147 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
148 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
149 |
(** Multiplication **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
150 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
151 |
lemma mult_nat_number_of: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
152 |
"(number_of v :: nat) * number_of v' = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
153 |
(if neg (number_of v) then 0 else number_of (bin_mult v v'))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
154 |
by (force dest!: neg_nat |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
155 |
simp del: nat_number_of |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
156 |
simp add: nat_number_of_def nat_mult_distrib [symmetric]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
157 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
158 |
declare mult_nat_number_of [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
159 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
160 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
161 |
(** Quotient **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
162 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
163 |
lemma div_nat_number_of: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
164 |
"(number_of v :: nat) div number_of v' = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
165 |
(if neg (number_of v) then 0 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
166 |
else nat (number_of v div number_of v'))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
167 |
by (force dest!: neg_nat |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
168 |
simp del: nat_number_of |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
169 |
simp add: nat_number_of_def nat_div_distrib [symmetric]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
170 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
171 |
declare div_nat_number_of [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
172 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
173 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
174 |
(** Remainder **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
175 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
176 |
lemma mod_nat_number_of: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
177 |
"(number_of v :: nat) mod number_of v' = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
178 |
(if neg (number_of v) then 0 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
179 |
else if neg (number_of v') then number_of v |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
180 |
else nat (number_of v mod number_of v'))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
181 |
by (force dest!: neg_nat |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
182 |
simp del: nat_number_of |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
183 |
simp add: nat_number_of_def nat_mod_distrib [symmetric]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
184 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
185 |
declare mod_nat_number_of [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
186 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
187 |
ML |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
188 |
{* |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
189 |
val nat_number_of_def = thm"nat_number_of_def"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
190 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
191 |
val nat_number_of = thm"nat_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
192 |
val numeral_0_eq_0 = thm"numeral_0_eq_0"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
193 |
val numeral_1_eq_1 = thm"numeral_1_eq_1"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
194 |
val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
195 |
val numeral_2_eq_2 = thm"numeral_2_eq_2"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
196 |
val nat_div_distrib = thm"nat_div_distrib"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
197 |
val nat_mod_distrib = thm"nat_mod_distrib"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
198 |
val int_nat_number_of = thm"int_nat_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
199 |
val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
200 |
val Suc_nat_number_of_add = thm"Suc_nat_number_of_add"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
201 |
val Suc_nat_number_of = thm"Suc_nat_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
202 |
val add_nat_number_of = thm"add_nat_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
203 |
val diff_nat_eq_if = thm"diff_nat_eq_if"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
204 |
val diff_nat_number_of = thm"diff_nat_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
205 |
val mult_nat_number_of = thm"mult_nat_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
206 |
val div_nat_number_of = thm"div_nat_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
207 |
val mod_nat_number_of = thm"mod_nat_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
208 |
*} |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
209 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
210 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
211 |
ML |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
212 |
{* |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
213 |
structure NatAbstractNumeralsData = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
214 |
struct |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
215 |
val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
216 |
val is_numeral = Bin_Simprocs.is_numeral |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
217 |
val numeral_0_eq_0 = numeral_0_eq_0 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
218 |
val numeral_1_eq_1 = numeral_1_eq_Suc_0 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
219 |
val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
220 |
fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps)) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
221 |
val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
222 |
end; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
223 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
224 |
structure NatAbstractNumerals = AbstractNumeralsFun (NatAbstractNumeralsData); |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
225 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
226 |
val nat_eval_numerals = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
227 |
map Bin_Simprocs.prep_simproc |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
228 |
[("nat_div_eval_numerals", ["(Suc 0) div m"], NatAbstractNumerals.proc div_nat_number_of), |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
229 |
("nat_mod_eval_numerals", ["(Suc 0) mod m"], NatAbstractNumerals.proc mod_nat_number_of)]; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
230 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
231 |
Addsimprocs nat_eval_numerals; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
232 |
*} |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
233 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
234 |
(*** Comparisons ***) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
235 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
236 |
(** Equals (=) **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
237 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
238 |
lemma eq_nat_nat_iff: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
239 |
"[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
240 |
by (auto elim!: nonneg_eq_int) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
241 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
242 |
(*"neg" is used in rewrite rules for binary comparisons*) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
243 |
lemma eq_nat_number_of: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
244 |
"((number_of v :: nat) = number_of v') = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
245 |
(if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
246 |
else if neg (number_of v') then iszero (number_of v) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
247 |
else iszero (number_of (bin_add v (bin_minus v'))))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
248 |
apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
249 |
eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
250 |
split add: split_if cong add: imp_cong) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
251 |
apply (simp only: nat_eq_iff nat_eq_iff2) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
252 |
apply (simp add: not_neg_eq_ge_0 [symmetric]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
253 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
254 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
255 |
declare eq_nat_number_of [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
256 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
257 |
(** Less-than (<) **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
258 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
259 |
(*"neg" is used in rewrite rules for binary comparisons*) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
260 |
lemma less_nat_number_of: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
261 |
"((number_of v :: nat) < number_of v') = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
262 |
(if neg (number_of v) then neg (number_of (bin_minus v')) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
263 |
else neg (number_of (bin_add v (bin_minus v'))))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
264 |
apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
265 |
nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
266 |
cong add: imp_cong, simp) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
267 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
268 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
269 |
declare less_nat_number_of [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
270 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
271 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
272 |
(** Less-than-or-equals (<=) **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
273 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
274 |
lemma le_nat_number_of_eq_not_less: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
275 |
"(number_of x <= (number_of y::nat)) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
276 |
(~ number_of y < (number_of x::nat))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
277 |
apply (rule linorder_not_less [symmetric]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
278 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
279 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
280 |
declare le_nat_number_of_eq_not_less [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
281 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
282 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
283 |
(*Maps #n to n for n = 0, 1, 2*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
284 |
lemmas numerals = numeral_0_eq_0 numeral_1_eq_1 numeral_2_eq_2 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
285 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
286 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
287 |
(** Nat **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
288 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
289 |
lemma Suc_pred': "0 < n ==> n = Suc(n - 1)" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
290 |
by (simp add: numerals) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
291 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
292 |
(*Expresses a natural number constant as the Suc of another one. |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
293 |
NOT suitable for rewriting because n recurs in the condition.*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
294 |
lemmas expand_Suc = Suc_pred' [of "number_of v", standard] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
295 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
296 |
(** Arith **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
297 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
298 |
lemma Suc_eq_add_numeral_1: "Suc n = n + 1" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
299 |
by (simp add: numerals) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
300 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
301 |
(* These two can be useful when m = number_of... *) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
302 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
303 |
lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
304 |
apply (case_tac "m") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
305 |
apply (simp_all add: numerals) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
306 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
307 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
308 |
lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
309 |
apply (case_tac "m") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
310 |
apply (simp_all add: numerals) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
311 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
312 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
313 |
lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
314 |
apply (case_tac "m") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
315 |
apply (simp_all add: numerals) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
316 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
317 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
318 |
lemma diff_less': "[| 0<n; 0<m |] ==> m - n < (m::nat)" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
319 |
by (simp add: diff_less numerals) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
320 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
321 |
declare diff_less' [of "number_of v", standard, simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
322 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
323 |
(** Power **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
324 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
325 |
lemma power_two: "(p::nat) ^ 2 = p*p" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
326 |
by (simp add: numerals) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
327 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
328 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
329 |
(*** Comparisons involving (0::nat) ***) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
330 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
331 |
lemma eq_number_of_0: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
332 |
"(number_of v = (0::nat)) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
333 |
(if neg (number_of v) then True else iszero (number_of v))" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
334 |
apply (simp add: numeral_0_eq_0 [symmetric] iszero_0) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
335 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
336 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
337 |
lemma eq_0_number_of: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
338 |
"((0::nat) = number_of v) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
339 |
(if neg (number_of v) then True else iszero (number_of v))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
340 |
apply (rule trans [OF eq_sym_conv eq_number_of_0]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
341 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
342 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
343 |
lemma less_0_number_of: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
344 |
"((0::nat) < number_of v) = neg (number_of (bin_minus v))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
345 |
by (simp add: numeral_0_eq_0 [symmetric]) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
346 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
347 |
(*Simplification already handles n<0, n<=0 and 0<=n.*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
348 |
declare eq_number_of_0 [simp] eq_0_number_of [simp] less_0_number_of [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
349 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
350 |
lemma neg_imp_number_of_eq_0: "neg (number_of v) ==> number_of v = (0::nat)" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
351 |
by (simp add: numeral_0_eq_0 [symmetric] iszero_0) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
352 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
353 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
354 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
355 |
(*** Comparisons involving Suc ***) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
356 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
357 |
lemma eq_number_of_Suc [simp]: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
358 |
"(number_of v = Suc n) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
359 |
(let pv = number_of (bin_pred v) in |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
360 |
if neg pv then False else nat pv = n)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
361 |
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
362 |
number_of_pred nat_number_of_def |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
363 |
split add: split_if) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
364 |
apply (rule_tac x = "number_of v" in spec) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
365 |
apply (auto simp add: nat_eq_iff) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
366 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
367 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
368 |
lemma Suc_eq_number_of [simp]: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
369 |
"(Suc n = number_of v) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
370 |
(let pv = number_of (bin_pred v) in |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
371 |
if neg pv then False else nat pv = n)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
372 |
apply (rule trans [OF eq_sym_conv eq_number_of_Suc]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
373 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
374 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
375 |
lemma less_number_of_Suc [simp]: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
376 |
"(number_of v < Suc n) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
377 |
(let pv = number_of (bin_pred v) in |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
378 |
if neg pv then True else nat pv < n)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
379 |
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
380 |
number_of_pred nat_number_of_def |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
381 |
split add: split_if) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
382 |
apply (rule_tac x = "number_of v" in spec) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
383 |
apply (auto simp add: nat_less_iff) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
384 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
385 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
386 |
lemma less_Suc_number_of [simp]: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
387 |
"(Suc n < number_of v) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
388 |
(let pv = number_of (bin_pred v) in |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
389 |
if neg pv then False else n < nat pv)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
390 |
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
391 |
number_of_pred nat_number_of_def |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
392 |
split add: split_if) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
393 |
apply (rule_tac x = "number_of v" in spec) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
394 |
apply (auto simp add: zless_nat_eq_int_zless) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
395 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
396 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
397 |
lemma le_number_of_Suc [simp]: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
398 |
"(number_of v <= Suc n) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
399 |
(let pv = number_of (bin_pred v) in |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
400 |
if neg pv then True else nat pv <= n)" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
401 |
apply (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric]) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
402 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
403 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
404 |
lemma le_Suc_number_of [simp]: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
405 |
"(Suc n <= number_of v) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
406 |
(let pv = number_of (bin_pred v) in |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
407 |
if neg pv then False else n <= nat pv)" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
408 |
apply (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric]) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
409 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
410 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
411 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
412 |
(* Push int(.) inwards: *) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
413 |
declare zadd_int [symmetric, simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
414 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
415 |
lemma lemma1: "(m+m = n+n) = (m = (n::int))" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
416 |
by auto |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
417 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
418 |
lemma lemma2: "m+m ~= (1::int) + (n + n)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
419 |
apply auto |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
420 |
apply (drule_tac f = "%x. x mod 2" in arg_cong) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
421 |
apply (simp add: zmod_zadd1_eq) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
422 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
423 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
424 |
lemma eq_number_of_BIT_BIT: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
425 |
"((number_of (v BIT x) ::int) = number_of (w BIT y)) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
426 |
(x=y & (((number_of v) ::int) = number_of w))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
427 |
by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute |
14288 | 428 |
Ring_and_Field.add_left_cancel add_assoc Ring_and_Field.add_0 |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
429 |
split add: split_if cong: imp_cong) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
430 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
431 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
432 |
lemma eq_number_of_BIT_Pls: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
433 |
"((number_of (v BIT x) ::int) = number_of bin.Pls) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
434 |
(x=False & (((number_of v) ::int) = number_of bin.Pls))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
435 |
apply (simp only: simp_thms add: number_of_BIT number_of_Pls eq_commute |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
436 |
split add: split_if cong: imp_cong) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
437 |
apply (rule_tac x = "number_of v" in spec, safe) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
438 |
apply (simp_all (no_asm_use)) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
439 |
apply (drule_tac f = "%x. x mod 2" in arg_cong) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
440 |
apply (simp add: zmod_zadd1_eq) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
441 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
442 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
443 |
lemma eq_number_of_BIT_Min: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
444 |
"((number_of (v BIT x) ::int) = number_of bin.Min) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
445 |
(x=True & (((number_of v) ::int) = number_of bin.Min))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
446 |
apply (simp only: simp_thms add: number_of_BIT number_of_Min eq_commute |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
447 |
split add: split_if cong: imp_cong) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
448 |
apply (rule_tac x = "number_of v" in spec, auto) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
449 |
apply (drule_tac f = "%x. x mod 2" in arg_cong, auto) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
450 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
451 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
452 |
lemma eq_number_of_Pls_Min: "(number_of bin.Pls ::int) ~= number_of bin.Min" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
453 |
by auto |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
454 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
455 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
456 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
457 |
(*** Literal arithmetic involving powers, type nat ***) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
458 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
459 |
lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
460 |
apply (induct_tac "n") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
461 |
apply (simp_all (no_asm_simp) add: nat_mult_distrib) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
462 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
463 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
464 |
lemma power_nat_number_of: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
465 |
"(number_of v :: nat) ^ n = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
466 |
(if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
467 |
by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
468 |
split add: split_if cong: imp_cong) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
469 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
470 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
471 |
declare power_nat_number_of [of _ "number_of w", standard, simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
472 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
473 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
474 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
475 |
(*** Literal arithmetic involving powers, type int ***) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
476 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
477 |
lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
478 |
by (simp add: zpower_zpower mult_commute) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
479 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
480 |
lemma zpower_two: "(p::int) ^ 2 = p*p" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
481 |
by (simp add: numerals) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
482 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
483 |
lemma zpower_odd: "(z::int) ^ (2*a + 1) = z * (z^a)^2" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
484 |
by (simp add: zpower_even zpower_zadd_distrib) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
485 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
486 |
lemma zpower_number_of_even: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
487 |
"(z::int) ^ number_of (w BIT False) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
488 |
(let w = z ^ (number_of w) in w*w)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
489 |
apply (simp del: nat_number_of add: nat_number_of_def number_of_BIT Let_def) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
490 |
apply (simp only: number_of_add) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
491 |
apply (rule_tac x = "number_of w" in spec, clarify) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
492 |
apply (case_tac " (0::int) <= x") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
493 |
apply (auto simp add: nat_mult_distrib zpower_even zpower_two) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
494 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
495 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
496 |
lemma zpower_number_of_odd: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
497 |
"(z::int) ^ number_of (w BIT True) = |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
498 |
(if (0::int) <= number_of w |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
499 |
then (let w = z ^ (number_of w) in z*w*w) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
500 |
else 1)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
501 |
apply (simp del: nat_number_of add: nat_number_of_def number_of_BIT Let_def) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
502 |
apply (simp only: number_of_add int_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0) |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
503 |
apply (rule_tac x = "number_of w" in spec, clarify) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
504 |
apply (auto simp add: nat_add_distrib nat_mult_distrib zpower_even zpower_two neg_nat) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
505 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
506 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
507 |
declare zpower_number_of_even [of "number_of v", standard, simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
508 |
declare zpower_number_of_odd [of "number_of v", standard, simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
509 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
510 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
511 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
512 |
ML |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
513 |
{* |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
514 |
val numerals = thms"numerals"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
515 |
val numeral_ss = simpset() addsimps numerals; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
516 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
517 |
val nat_bin_arith_setup = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
518 |
[Fast_Arith.map_data |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
519 |
(fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
520 |
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
521 |
inj_thms = inj_thms, |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
522 |
lessD = lessD, |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
523 |
simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of, |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
524 |
not_neg_number_of_Pls, |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
525 |
neg_number_of_Min,neg_number_of_BIT]})] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
526 |
*} |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
527 |
|
12838 | 528 |
setup nat_bin_arith_setup |
529 |
||
13189
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13154
diff
changeset
|
530 |
(* Enable arith to deal with div/mod k where k is a numeral: *) |
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13154
diff
changeset
|
531 |
declare split_div[of _ _ "number_of k", standard, arith_split] |
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13154
diff
changeset
|
532 |
declare split_mod[of _ _ "number_of k", standard, arith_split] |
13154 | 533 |
|
13491 | 534 |
lemma nat_number_of_Pls: "number_of bin.Pls = (0::nat)" |
12838 | 535 |
by (simp add: number_of_Pls nat_number_of_def) |
536 |
||
13491 | 537 |
lemma nat_number_of_Min: "number_of bin.Min = (0::nat)" |
12838 | 538 |
apply (simp only: number_of_Min nat_number_of_def nat_zminus_int) |
539 |
apply (simp add: neg_nat) |
|
540 |
done |
|
7032 | 541 |
|
12838 | 542 |
lemma nat_number_of_BIT_True: |
543 |
"number_of (w BIT True) = |
|
544 |
(if neg (number_of w) then 0 |
|
545 |
else let n = number_of w in Suc (n + n))" |
|
546 |
apply (simp only: nat_number_of_def Let_def split: split_if) |
|
547 |
apply (intro conjI impI) |
|
548 |
apply (simp add: neg_nat neg_number_of_BIT) |
|
549 |
apply (rule int_int_eq [THEN iffD1]) |
|
550 |
apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms) |
|
551 |
apply (simp only: number_of_BIT if_True zadd_assoc) |
|
552 |
done |
|
7032 | 553 |
|
12838 | 554 |
lemma nat_number_of_BIT_False: |
555 |
"number_of (w BIT False) = (let n::nat = number_of w in n + n)" |
|
556 |
apply (simp only: nat_number_of_def Let_def) |
|
557 |
apply (cases "neg (number_of w)") |
|
558 |
apply (simp add: neg_nat neg_number_of_BIT) |
|
559 |
apply (rule int_int_eq [THEN iffD1]) |
|
560 |
apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms) |
|
561 |
apply (simp only: number_of_BIT if_False zadd_0 zadd_assoc) |
|
562 |
done |
|
563 |
||
13043
ad1828b479b7
renamed nat_number_of to nat_number (avoid clash with separate theorem);
wenzelm
parents:
12933
diff
changeset
|
564 |
lemmas nat_number = |
12838 | 565 |
nat_number_of_Pls nat_number_of_Min |
566 |
nat_number_of_BIT_True nat_number_of_BIT_False |
|
567 |
||
568 |
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" |
|
569 |
by (simp add: Let_def) |
|
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
9509
diff
changeset
|
570 |
|
12440 | 571 |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
572 |
subsection {*More ML Bindings*} |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
573 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
574 |
ML |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
575 |
{* |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
576 |
val eq_nat_nat_iff = thm"eq_nat_nat_iff"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
577 |
val eq_nat_number_of = thm"eq_nat_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
578 |
val less_nat_number_of = thm"less_nat_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
579 |
val le_nat_number_of_eq_not_less = thm"le_nat_number_of_eq_not_less"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
580 |
val Suc_pred' = thm"Suc_pred'"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
581 |
val expand_Suc = thm"expand_Suc"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
582 |
val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
583 |
val add_eq_if = thm"add_eq_if"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
584 |
val mult_eq_if = thm"mult_eq_if"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
585 |
val power_eq_if = thm"power_eq_if"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
586 |
val diff_less' = thm"diff_less'"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
587 |
val power_two = thm"power_two"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
588 |
val eq_number_of_0 = thm"eq_number_of_0"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
589 |
val eq_0_number_of = thm"eq_0_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
590 |
val less_0_number_of = thm"less_0_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
591 |
val neg_imp_number_of_eq_0 = thm"neg_imp_number_of_eq_0"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
592 |
val eq_number_of_Suc = thm"eq_number_of_Suc"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
593 |
val Suc_eq_number_of = thm"Suc_eq_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
594 |
val less_number_of_Suc = thm"less_number_of_Suc"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
595 |
val less_Suc_number_of = thm"less_Suc_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
596 |
val le_number_of_Suc = thm"le_number_of_Suc"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
597 |
val le_Suc_number_of = thm"le_Suc_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
598 |
val eq_number_of_BIT_BIT = thm"eq_number_of_BIT_BIT"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
599 |
val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
600 |
val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
601 |
val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
602 |
val nat_power_eq = thm"nat_power_eq"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
603 |
val power_nat_number_of = thm"power_nat_number_of"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
604 |
val zpower_even = thm"zpower_even"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
605 |
val zpower_two = thm"zpower_two"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
606 |
val zpower_odd = thm"zpower_odd"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
607 |
val zpower_number_of_even = thm"zpower_number_of_even"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
608 |
val zpower_number_of_odd = thm"zpower_number_of_odd"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
609 |
val nat_number_of_Pls = thm"nat_number_of_Pls"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
610 |
val nat_number_of_Min = thm"nat_number_of_Min"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
611 |
val nat_number_of_BIT_True = thm"nat_number_of_BIT_True"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
612 |
val nat_number_of_BIT_False = thm"nat_number_of_BIT_False"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
613 |
val Let_Suc = thm"Let_Suc"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
614 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
615 |
val nat_number = thms"nat_number"; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
616 |
*} |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset
|
617 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
618 |
subsection {*Lemmas for the Combination and Cancellation Simprocs*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
619 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
620 |
lemma nat_number_of_add_left: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
621 |
"number_of v + (number_of v' + (k::nat)) = |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
622 |
(if neg (number_of v) then number_of v' + k |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
623 |
else if neg (number_of v') then number_of v + k |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
624 |
else number_of (bin_add v v') + k)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
625 |
apply simp |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
626 |
done |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
627 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
628 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
629 |
(** For combine_numerals **) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
630 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
631 |
lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
632 |
by (simp add: add_mult_distrib) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
633 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
634 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
635 |
(** For cancel_numerals **) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
636 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
637 |
lemma nat_diff_add_eq1: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
638 |
"j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
639 |
by (simp split add: nat_diff_split add: add_mult_distrib) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
640 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
641 |
lemma nat_diff_add_eq2: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
642 |
"i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
643 |
by (simp split add: nat_diff_split add: add_mult_distrib) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
644 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
645 |
lemma nat_eq_add_iff1: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
646 |
"j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
647 |
by (auto split add: nat_diff_split simp add: add_mult_distrib) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
648 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
649 |
lemma nat_eq_add_iff2: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
650 |
"i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
651 |
by (auto split add: nat_diff_split simp add: add_mult_distrib) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
652 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
653 |
lemma nat_less_add_iff1: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
654 |
"j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
655 |
by (auto split add: nat_diff_split simp add: add_mult_distrib) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
656 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
657 |
lemma nat_less_add_iff2: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
658 |
"i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
659 |
by (auto split add: nat_diff_split simp add: add_mult_distrib) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
660 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
661 |
lemma nat_le_add_iff1: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
662 |
"j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
663 |
by (auto split add: nat_diff_split simp add: add_mult_distrib) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
664 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
665 |
lemma nat_le_add_iff2: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
666 |
"i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
667 |
by (auto split add: nat_diff_split simp add: add_mult_distrib) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
668 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
669 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
670 |
(** For cancel_numeral_factors **) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
671 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
672 |
lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
673 |
by auto |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
674 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
675 |
lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
676 |
by auto |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
677 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
678 |
lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
679 |
by auto |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
680 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
681 |
lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
682 |
by auto |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
683 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
684 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
685 |
(** For cancel_factor **) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
686 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
687 |
lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k --> m<=n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
688 |
by auto |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
689 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
690 |
lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
691 |
by auto |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
692 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
693 |
lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
694 |
by auto |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
695 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
696 |
lemma nat_mult_div_cancel_disj: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
697 |
"(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
698 |
by (simp add: nat_mult_div_cancel1) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
699 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
700 |
ML |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
701 |
{* |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
702 |
val nat_number_of_add_left = thm"nat_number_of_add_left"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
703 |
val left_add_mult_distrib = thm"left_add_mult_distrib"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
704 |
val nat_diff_add_eq1 = thm"nat_diff_add_eq1"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
705 |
val nat_diff_add_eq2 = thm"nat_diff_add_eq2"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
706 |
val nat_eq_add_iff1 = thm"nat_eq_add_iff1"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
707 |
val nat_eq_add_iff2 = thm"nat_eq_add_iff2"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
708 |
val nat_less_add_iff1 = thm"nat_less_add_iff1"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
709 |
val nat_less_add_iff2 = thm"nat_less_add_iff2"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
710 |
val nat_le_add_iff1 = thm"nat_le_add_iff1"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
711 |
val nat_le_add_iff2 = thm"nat_le_add_iff2"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
712 |
val nat_mult_le_cancel1 = thm"nat_mult_le_cancel1"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
713 |
val nat_mult_less_cancel1 = thm"nat_mult_less_cancel1"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
714 |
val nat_mult_eq_cancel1 = thm"nat_mult_eq_cancel1"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
715 |
val nat_mult_div_cancel1 = thm"nat_mult_div_cancel1"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
716 |
val nat_mult_le_cancel_disj = thm"nat_mult_le_cancel_disj"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
717 |
val nat_mult_less_cancel_disj = thm"nat_mult_less_cancel_disj"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
718 |
val nat_mult_eq_cancel_disj = thm"nat_mult_eq_cancel_disj"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
719 |
val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj"; |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
720 |
*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
721 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
722 |
|
12440 | 723 |
subsection {* Configuration of the code generator *} |
724 |
||
12933
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset
|
725 |
ML {* |
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset
|
726 |
infix 7 `*; |
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset
|
727 |
infix 6 `+; |
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset
|
728 |
|
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset
|
729 |
val op `* = op * : int * int -> int; |
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset
|
730 |
val op `+ = op + : int * int -> int; |
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset
|
731 |
val `~ = ~ : int -> int; |
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset
|
732 |
*} |
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset
|
733 |
|
12440 | 734 |
types_code |
735 |
"int" ("int") |
|
736 |
||
14194
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
737 |
constdefs |
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
738 |
int_aux :: "int \<Rightarrow> nat \<Rightarrow> int" |
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
739 |
"int_aux i n == (i + int n)" |
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
740 |
nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat" |
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
741 |
"nat_aux n i == (n + nat i)" |
12440 | 742 |
|
14194
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
743 |
lemma [code]: |
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
744 |
"int_aux i 0 = i" |
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
745 |
"int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *} |
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
746 |
"int n = int_aux 0 n" |
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
747 |
by (simp add: int_aux_def)+ |
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
748 |
|
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
749 |
lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i - 1))" |
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
750 |
by (simp add: nat_aux_def Suc_nat_eq_nat_zadd1) -- {* tail recursive *} |
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
751 |
lemma [code]: "nat i = nat_aux 0 i" |
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset
|
752 |
by (simp add: nat_aux_def) |
12440 | 753 |
|
754 |
consts_code |
|
755 |
"0" :: "int" ("0") |
|
756 |
"1" :: "int" ("1") |
|
12933
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset
|
757 |
"uminus" :: "int => int" ("`~") |
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset
|
758 |
"op +" :: "int => int => int" ("(_ `+/ _)") |
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset
|
759 |
"op *" :: "int => int => int" ("(_ `*/ _)") |
12440 | 760 |
"neg" ("(_ < 0)") |
761 |
||
7032 | 762 |
end |