author | haftmann |
Sun, 09 Nov 2014 10:03:17 +0100 | |
changeset 58953 | 2e19b392d9e3 |
parent 55932 | 68c5104d2204 |
child 60868 | dd18c33c001e |
permissions | -rw-r--r-- |
23664 | 1 |
theory ComputeNumeral |
29804
e15b74577368
Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents:
29668
diff
changeset
|
2 |
imports ComputeHOL ComputeFloat |
23664 | 3 |
begin |
4 |
||
5 |
(* equality for bit strings *) |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
6 |
lemmas biteq = eq_num_simps |
23664 | 7 |
|
8 |
(* x < y for bit strings *) |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
9 |
lemmas bitless = less_num_simps |
23664 | 10 |
|
11 |
(* x \<le> y for bit strings *) |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
12 |
lemmas bitle = le_num_simps |
23664 | 13 |
|
14 |
(* addition for bit strings *) |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
15 |
lemmas bitadd = add_num_simps |
23664 | 16 |
|
17 |
(* multiplication for bit strings *) |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
18 |
lemmas bitmul = mult_num_simps |
23664 | 19 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
20 |
lemmas bitarith = arith_simps |
23664 | 21 |
|
22 |
(* Normalization of nat literals *) |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
23 |
lemmas natnorm = one_eq_Numeral1_nat |
23664 | 24 |
|
25 |
fun natfac :: "nat \<Rightarrow> nat" |
|
38273 | 26 |
where "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))" |
23664 | 27 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
28 |
lemmas compute_natarith = |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
29 |
arith_simps rel_simps |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
30 |
diff_nat_numeral nat_numeral nat_0 nat_neg_numeral |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
31 |
numeral_1_eq_1 [symmetric] |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
32 |
numeral_1_eq_Suc_0 [symmetric] |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
33 |
Suc_numeral natfac.simps |
23664 | 34 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
35 |
lemmas number_norm = numeral_1_eq_1[symmetric] |
23664 | 36 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
37 |
lemmas compute_numberarith = |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
38 |
arith_simps rel_simps number_norm |
23664 | 39 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
40 |
lemmas compute_num_conversions = |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
41 |
real_of_nat_numeral real_of_nat_zero |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
42 |
nat_numeral nat_0 nat_neg_numeral |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
43 |
real_numeral real_of_int_zero |
23664 | 44 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
45 |
lemmas zpowerarith = zpower_numeral_even zpower_numeral_odd zpower_Pls int_pow_1 |
23664 | 46 |
|
47 |
(* div, mod *) |
|
48 |
||
49 |
lemma adjust: "adjust b (q, r) = (if 0 \<le> r - b then (2 * q + 1, r - b) else (2 * q, r))" |
|
50 |
by (auto simp only: adjust_def) |
|
51 |
||
33343 | 52 |
lemma divmod: "divmod_int a b = (if 0\<le>a then |
23664 | 53 |
if 0\<le>b then posDivAlg a b |
54 |
else if a=0 then (0, 0) |
|
46560
8e252a608765
remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)
huffman
parents:
38273
diff
changeset
|
55 |
else apsnd uminus (negDivAlg (-a) (-b)) |
23664 | 56 |
else |
57 |
if 0<b then negDivAlg a b |
|
46560
8e252a608765
remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)
huffman
parents:
38273
diff
changeset
|
58 |
else apsnd uminus (posDivAlg (-a) (-b)))" |
33343 | 59 |
by (auto simp only: divmod_int_def) |
23664 | 60 |
|
55932 | 61 |
lemmas compute_div_mod = div_int_def mod_int_def divmod adjust apsnd_def map_prod_def posDivAlg.simps negDivAlg.simps |
23664 | 62 |
|
63 |
||
64 |
||
65 |
(* collecting all the theorems *) |
|
66 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
67 |
lemma even_0_int: "even (0::int) = True" |
23664 | 68 |
by simp |
69 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
70 |
lemma even_One_int: "even (numeral Num.One :: int) = False" |
23664 | 71 |
by simp |
72 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
73 |
lemma even_Bit0_int: "even (numeral (Num.Bit0 x) :: int) = True" |
58953 | 74 |
by (simp only: even_numeral) |
23664 | 75 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
76 |
lemma even_Bit1_int: "even (numeral (Num.Bit1 x) :: int) = False" |
58953 | 77 |
by (simp only: odd_numeral) |
23664 | 78 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset
|
79 |
lemmas compute_even = even_0_int even_One_int even_Bit0_int even_Bit1_int |
23664 | 80 |
|
81 |
lemmas compute_numeral = compute_if compute_let compute_pair compute_bool |
|
82 |
compute_natarith compute_numberarith max_def min_def compute_num_conversions zpowerarith compute_div_mod compute_even |
|
83 |
||
84 |
end |