src/HOL/Matrix_LP/ComputeNumeral.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 62348 9a5f43dac883
permissions -rw-r--r--
tuned: each session has at most one defining entry;
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
lp15@61609
    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
lp15@61694
    31
  numeral_One [symmetric]
huffman@47108
    32
  numeral_1_eq_Suc_0 [symmetric]
huffman@47108
    33
  Suc_numeral natfac.simps
obua@23664
    34
lp15@61694
    35
lemmas number_norm = numeral_One[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 =
lp15@61609
    41
  of_nat_numeral of_nat_0
huffman@47108
    42
  nat_numeral nat_0 nat_neg_numeral
lp15@61609
    43
  of_int_numeral of_int_neg_numeral of_int_0
obua@23664
    44
haftmann@62348
    45
lemmas zpowerarith = power_numeral_even power_numeral_odd zpower_Pls int_pow_1
obua@23664
    46
obua@23664
    47
(* div, mod *)
obua@23664
    48
haftmann@60868
    49
lemmas compute_div_mod = div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
haftmann@60868
    50
  one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
haftmann@60868
    51
  one_div_minus_numeral one_mod_minus_numeral
haftmann@60868
    52
  numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
haftmann@60868
    53
  numeral_div_minus_numeral numeral_mod_minus_numeral
haftmann@60930
    54
  div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
haftmann@60868
    55
  numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
haftmann@60868
    56
  divmod_steps divmod_cancel divmod_step_eq fst_conv snd_conv numeral_One
haftmann@60930
    57
  case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
haftmann@60868
    58
  minus_minus numeral_times_numeral mult_zero_right mult_1_right
obua@23664
    59
obua@23664
    60
obua@23664
    61
(* collecting all the theorems *)
obua@23664
    62
huffman@47108
    63
lemma even_0_int: "even (0::int) = True"
obua@23664
    64
  by simp
obua@23664
    65
huffman@47108
    66
lemma even_One_int: "even (numeral Num.One :: int) = False"
obua@23664
    67
  by simp
obua@23664
    68
huffman@47108
    69
lemma even_Bit0_int: "even (numeral (Num.Bit0 x) :: int) = True"
haftmann@58953
    70
  by (simp only: even_numeral)
obua@23664
    71
huffman@47108
    72
lemma even_Bit1_int: "even (numeral (Num.Bit1 x) :: int) = False"
haftmann@58953
    73
  by (simp only: odd_numeral)
obua@23664
    74
huffman@47108
    75
lemmas compute_even = even_0_int even_One_int even_Bit0_int even_Bit1_int
obua@23664
    76
lp15@61609
    77
lemmas compute_numeral = compute_if compute_let compute_pair compute_bool
obua@23664
    78
                         compute_natarith compute_numberarith max_def min_def compute_num_conversions zpowerarith compute_div_mod compute_even
obua@23664
    79
obua@23664
    80
end