src/HOL/Matrix_LP/ComputeNumeral.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (21 months ago)
changeset 67022 49309fe530fd
parent 62348 9a5f43dac883
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 theory ComputeNumeral
     2 imports ComputeHOL ComputeFloat
     3 begin
     4 
     5 (* equality for bit strings *)
     6 lemmas biteq = eq_num_simps
     7 
     8 (* x < y for bit strings *)
     9 lemmas bitless = less_num_simps
    10 
    11 (* x \<le> y for bit strings *)
    12 lemmas bitle = le_num_simps
    13 
    14 (* addition for bit strings *)
    15 lemmas bitadd = add_num_simps
    16 
    17 (* multiplication for bit strings *)
    18 lemmas bitmul = mult_num_simps
    19 
    20 lemmas bitarith = arith_simps
    21 
    22 (* Normalization of nat literals *)
    23 lemmas natnorm = one_eq_Numeral1_nat
    24 
    25 fun natfac :: "nat \<Rightarrow> nat"
    26   where "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))"
    27 
    28 lemmas compute_natarith =
    29   arith_simps rel_simps
    30   diff_nat_numeral nat_numeral nat_0 nat_neg_numeral
    31   numeral_One [symmetric]
    32   numeral_1_eq_Suc_0 [symmetric]
    33   Suc_numeral natfac.simps
    34 
    35 lemmas number_norm = numeral_One[symmetric]
    36 
    37 lemmas compute_numberarith =
    38   arith_simps rel_simps number_norm
    39 
    40 lemmas compute_num_conversions =
    41   of_nat_numeral of_nat_0
    42   nat_numeral nat_0 nat_neg_numeral
    43   of_int_numeral of_int_neg_numeral of_int_0
    44 
    45 lemmas zpowerarith = power_numeral_even power_numeral_odd zpower_Pls int_pow_1
    46 
    47 (* div, mod *)
    48 
    49 lemmas compute_div_mod = div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
    50   one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
    51   one_div_minus_numeral one_mod_minus_numeral
    52   numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
    53   numeral_div_minus_numeral numeral_mod_minus_numeral
    54   div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
    55   numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
    56   divmod_steps divmod_cancel divmod_step_eq fst_conv snd_conv numeral_One
    57   case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
    58   minus_minus numeral_times_numeral mult_zero_right mult_1_right
    59 
    60 
    61 (* collecting all the theorems *)
    62 
    63 lemma even_0_int: "even (0::int) = True"
    64   by simp
    65 
    66 lemma even_One_int: "even (numeral Num.One :: int) = False"
    67   by simp
    68 
    69 lemma even_Bit0_int: "even (numeral (Num.Bit0 x) :: int) = True"
    70   by (simp only: even_numeral)
    71 
    72 lemma even_Bit1_int: "even (numeral (Num.Bit1 x) :: int) = False"
    73   by (simp only: odd_numeral)
    74 
    75 lemmas compute_even = even_0_int even_One_int even_Bit0_int even_Bit1_int
    76 
    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
    79 
    80 end