equal
deleted
inserted
replaced
12 lemmas bitle = le_num_simps |
12 lemmas bitle = le_num_simps |
13 |
13 |
14 (* addition for bit strings *) |
14 (* addition for bit strings *) |
15 lemmas bitadd = add_num_simps |
15 lemmas bitadd = add_num_simps |
16 |
16 |
17 (* multiplication for bit strings *) |
17 (* multiplication for bit strings *) |
18 lemmas bitmul = mult_num_simps |
18 lemmas bitmul = mult_num_simps |
19 |
19 |
20 lemmas bitarith = arith_simps |
20 lemmas bitarith = arith_simps |
21 |
21 |
22 (* Normalization of nat literals *) |
22 (* Normalization of nat literals *) |
36 |
36 |
37 lemmas compute_numberarith = |
37 lemmas compute_numberarith = |
38 arith_simps rel_simps number_norm |
38 arith_simps rel_simps number_norm |
39 |
39 |
40 lemmas compute_num_conversions = |
40 lemmas compute_num_conversions = |
41 real_of_nat_numeral real_of_nat_zero |
41 of_nat_numeral of_nat_0 |
42 nat_numeral nat_0 nat_neg_numeral |
42 nat_numeral nat_0 nat_neg_numeral |
43 real_numeral real_of_int_zero |
43 of_int_numeral of_int_neg_numeral of_int_0 |
44 |
44 |
45 lemmas zpowerarith = zpower_numeral_even zpower_numeral_odd zpower_Pls int_pow_1 |
45 lemmas zpowerarith = zpower_numeral_even zpower_numeral_odd zpower_Pls int_pow_1 |
46 |
46 |
47 (* div, mod *) |
47 (* div, mod *) |
48 |
48 |
72 lemma even_Bit1_int: "even (numeral (Num.Bit1 x) :: int) = False" |
72 lemma even_Bit1_int: "even (numeral (Num.Bit1 x) :: int) = False" |
73 by (simp only: odd_numeral) |
73 by (simp only: odd_numeral) |
74 |
74 |
75 lemmas compute_even = even_0_int even_One_int even_Bit0_int even_Bit1_int |
75 lemmas compute_even = even_0_int even_One_int even_Bit0_int even_Bit1_int |
76 |
76 |
77 lemmas compute_numeral = compute_if compute_let compute_pair compute_bool |
77 lemmas compute_numeral = compute_if compute_let compute_pair compute_bool |
78 compute_natarith compute_numberarith max_def min_def compute_num_conversions zpowerarith compute_div_mod compute_even |
78 compute_natarith compute_numberarith max_def min_def compute_num_conversions zpowerarith compute_div_mod compute_even |
79 |
79 |
80 end |
80 end |