author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47108  2a1953f0d20d 
child 55932  68c5104d2204 
permissions  rwrr 
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 

46561  61 
lemmas compute_div_mod = div_int_def mod_int_def divmod adjust apsnd_def map_pair_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" 
23664  74 
by simp 
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" 
23664  77 
by simp 
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 