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