src/HOL/Matrix_LP/ComputeNumeral.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47108 2a1953f0d20d
child 55932 68c5104d2204
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23664
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     3
begin
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     4
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     7
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
     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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    10
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    13
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    16
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    19
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    20
lemmas bitarith = arith_simps
23664
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    21
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    24
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    25
fun natfac :: "nat \<Rightarrow> nat"
38273
d31a34569542 modernized some specifications;
wenzelm
parents: 35416
diff changeset
    26
  where "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))"
23664
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    46
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    47
(* div, mod *)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    48
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    49
lemma adjust: "adjust b (q, r) = (if 0 \<le> r - b then (2 * q + 1, r - b) else (2 * q, r))"
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    50
  by (auto simp only: adjust_def)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    51
33343
2eb0b672ab40 adjusted to changes in theory Divides
haftmann
parents: 32491
diff changeset
    52
lemma divmod: "divmod_int a b = (if 0\<le>a then
23664
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    53
                  if 0\<le>b then posDivAlg a b
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    56
               else 
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
2eb0b672ab40 adjusted to changes in theory Divides
haftmann
parents: 32491
diff changeset
    59
  by (auto simp only: divmod_int_def)
23664
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    60
46561
092f4eca9848 add missing lemmas to compute_div_mod
huffman
parents: 46560
diff changeset
    61
lemmas compute_div_mod = div_int_def mod_int_def divmod adjust apsnd_def map_pair_def posDivAlg.simps negDivAlg.simps
23664
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    62
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    63
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    64
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    65
(* collecting all the theorems *)
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    68
  by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    71
  by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    74
  by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    77
  by simp
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    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
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    80
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    81
lemmas compute_numeral = compute_if compute_let compute_pair compute_bool 
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    82
                         compute_natarith compute_numberarith max_def min_def compute_num_conversions zpowerarith compute_div_mod compute_even
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    83
9c486517354a added computing oracle support for HOL and numerals
obua
parents:
diff changeset
    84
end