src/HOL/Matrix/ComputeNumeral.thy
 author haftmann Fri Nov 27 08:41:10 2009 +0100 (2009-11-27) changeset 33963 977b94b64905 parent 33343 2eb0b672ab40 child 35028 108662d50512 permissions -rw-r--r--
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
```     1 theory ComputeNumeral
```
```     2 imports ComputeHOL ComputeFloat
```
```     3 begin
```
```     4
```
```     5 (* normalization of bit strings *)
```
```     6 lemmas bitnorm = normalize_bin_simps
```
```     7
```
```     8 (* neg for bit strings *)
```
```     9 lemma neg1: "neg Int.Pls = False" by (simp add: Int.Pls_def)
```
```    10 lemma neg2: "neg Int.Min = True" apply (subst Int.Min_def) by auto
```
```    11 lemma neg3: "neg (Int.Bit0 x) = neg x" apply (simp add: neg_def) apply (subst Bit0_def) by auto
```
```    12 lemma neg4: "neg (Int.Bit1 x) = neg x" apply (simp add: neg_def) apply (subst Bit1_def) by auto
```
```    13 lemmas bitneg = neg1 neg2 neg3 neg4
```
```    14
```
```    15 (* iszero for bit strings *)
```
```    16 lemma iszero1: "iszero Int.Pls = True" by (simp add: Int.Pls_def iszero_def)
```
```    17 lemma iszero2: "iszero Int.Min = False" apply (subst Int.Min_def) apply (subst iszero_def) by simp
```
```    18 lemma iszero3: "iszero (Int.Bit0 x) = iszero x" apply (subst Int.Bit0_def) apply (subst iszero_def)+ by auto
```
```    19 lemma iszero4: "iszero (Int.Bit1 x) = False" apply (subst Int.Bit1_def) apply (subst iszero_def)+  apply simp by arith
```
```    20 lemmas bitiszero = iszero1 iszero2 iszero3 iszero4
```
```    21
```
```    22 (* lezero for bit strings *)
```
```    23 constdefs
```
```    24   "lezero x == (x \<le> 0)"
```
```    25 lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto
```
```    26 lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto
```
```    27 lemma lezero3: "lezero (Int.Bit0 x) = lezero x" unfolding Int.Bit0_def lezero_def by auto
```
```    28 lemma lezero4: "lezero (Int.Bit1 x) = neg x" unfolding Int.Bit1_def lezero_def neg_def by auto
```
```    29 lemmas bitlezero = lezero1 lezero2 lezero3 lezero4
```
```    30
```
```    31 (* equality for bit strings *)
```
```    32 lemmas biteq = eq_bin_simps
```
```    33
```
```    34 (* x < y for bit strings *)
```
```    35 lemmas bitless = less_bin_simps
```
```    36
```
```    37 (* x \<le> y for bit strings *)
```
```    38 lemmas bitle = le_bin_simps
```
```    39
```
```    40 (* succ for bit strings *)
```
```    41 lemmas bitsucc = succ_bin_simps
```
```    42
```
```    43 (* pred for bit strings *)
```
```    44 lemmas bitpred = pred_bin_simps
```
```    45
```
```    46 (* unary minus for bit strings *)
```
```    47 lemmas bituminus = minus_bin_simps
```
```    48
```
```    49 (* addition for bit strings *)
```
```    50 lemmas bitadd = add_bin_simps
```
```    51
```
```    52 (* multiplication for bit strings *)
```
```    53 lemma mult_Pls_right: "x * Int.Pls = Int.Pls" by (simp add: Pls_def)
```
```    54 lemma mult_Min_right: "x * Int.Min = - x" by (subst mult_commute, simp add: mult_Min)
```
```    55 lemma multb0x: "(Int.Bit0 x) * y = Int.Bit0 (x * y)" by (rule mult_Bit0)
```
```    56 lemma multxb0: "x * (Int.Bit0 y) = Int.Bit0 (x * y)" unfolding Bit0_def by simp
```
```    57 lemma multb1: "(Int.Bit1 x) * (Int.Bit1 y) = Int.Bit1 (Int.Bit0 (x * y) + x + y)"
```
```    58   unfolding Bit0_def Bit1_def by (simp add: algebra_simps)
```
```    59 lemmas bitmul = mult_Pls mult_Min mult_Pls_right mult_Min_right multb0x multxb0 multb1
```
```    60
```
```    61 lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul
```
```    62
```
```    63 constdefs
```
```    64   "nat_norm_number_of (x::nat) == x"
```
```    65
```
```    66 lemma nat_norm_number_of: "nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)"
```
```    67   apply (simp add: nat_norm_number_of_def)
```
```    68   unfolding lezero_def iszero_def neg_def
```
```    69   apply (simp add: numeral_simps)
```
```    70   done
```
```    71
```
```    72 (* Normalization of nat literals *)
```
```    73 lemma natnorm0: "(0::nat) = number_of (Int.Pls)" by auto
```
```    74 lemma natnorm1: "(1 :: nat) = number_of (Int.Bit1 Int.Pls)"  by auto
```
```    75 lemmas natnorm = natnorm0 natnorm1 nat_norm_number_of
```
```    76
```
```    77 (* Suc *)
```
```    78 lemma natsuc: "Suc (number_of x) = (if neg x then 1 else number_of (Int.succ x))" by (auto simp add: number_of_is_id)
```
```    79
```
```    80 (* Addition for nat *)
```
```    81 lemma natadd: "number_of x + ((number_of y)::nat) = (if neg x then (number_of y) else (if neg y then number_of x else (number_of (x + y))))"
```
```    82   unfolding nat_number_of_def number_of_is_id neg_def
```
```    83   by auto
```
```    84
```
```    85 (* Subtraction for nat *)
```
```    86 lemma natsub: "(number_of x) - ((number_of y)::nat) =
```
```    87   (if neg x then 0 else (if neg y then number_of x else (nat_norm_number_of (number_of (x + (- y))))))"
```
```    88   unfolding nat_norm_number_of
```
```    89   by (auto simp add: number_of_is_id neg_def lezero_def iszero_def Let_def nat_number_of_def)
```
```    90
```
```    91 (* Multiplication for nat *)
```
```    92 lemma natmul: "(number_of x) * ((number_of y)::nat) =
```
```    93   (if neg x then 0 else (if neg y then 0 else number_of (x * y)))"
```
```    94   unfolding nat_number_of_def number_of_is_id neg_def
```
```    95   by (simp add: nat_mult_distrib)
```
```    96
```
```    97 lemma nateq: "(((number_of x)::nat) = (number_of y)) = ((lezero x \<and> lezero y) \<or> (x = y))"
```
```    98   by (auto simp add: iszero_def lezero_def neg_def number_of_is_id)
```
```    99
```
```   100 lemma natless: "(((number_of x)::nat) < (number_of y)) = ((x < y) \<and> (\<not> (lezero y)))"
```
```   101   by (simp add: lezero_def numeral_simps not_le)
```
```   102
```
```   103 lemma natle: "(((number_of x)::nat) \<le> (number_of y)) = (y < x \<longrightarrow> lezero x)"
```
```   104   by (auto simp add: number_of_is_id lezero_def nat_number_of_def)
```
```   105
```
```   106 fun natfac :: "nat \<Rightarrow> nat"
```
```   107 where
```
```   108    "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))"
```
```   109
```
```   110 lemmas compute_natarith = bitarith natnorm natsuc natadd natsub natmul nateq natless natle natfac.simps
```
```   111
```
```   112 lemma number_eq: "(((number_of x)::'a::{number_ring, ordered_idom}) = (number_of y)) = (x = y)"
```
```   113   unfolding number_of_eq
```
```   114   apply simp
```
```   115   done
```
```   116
```
```   117 lemma number_le: "(((number_of x)::'a::{number_ring, ordered_idom}) \<le>  (number_of y)) = (x \<le> y)"
```
```   118   unfolding number_of_eq
```
```   119   apply simp
```
```   120   done
```
```   121
```
```   122 lemma number_less: "(((number_of x)::'a::{number_ring, ordered_idom}) <  (number_of y)) = (x < y)"
```
```   123   unfolding number_of_eq
```
```   124   apply simp
```
```   125   done
```
```   126
```
```   127 lemma number_diff: "((number_of x)::'a::{number_ring, ordered_idom}) - number_of y = number_of (x + (- y))"
```
```   128   apply (subst diff_number_of_eq)
```
```   129   apply simp
```
```   130   done
```
```   131
```
```   132 lemmas number_norm = number_of_Pls[symmetric] numeral_1_eq_1[symmetric]
```
```   133
```
```   134 lemmas compute_numberarith = number_of_minus[symmetric] number_of_add[symmetric] number_diff number_of_mult[symmetric] number_norm number_eq number_le number_less
```
```   135
```
```   136 lemma compute_real_of_nat_number_of: "real ((number_of v)::nat) = (if neg v then 0 else number_of v)"
```
```   137   by (simp only: real_of_nat_number_of number_of_is_id)
```
```   138
```
```   139 lemma compute_nat_of_int_number_of: "nat ((number_of v)::int) = (number_of v)"
```
```   140   by simp
```
```   141
```
```   142 lemmas compute_num_conversions = compute_real_of_nat_number_of compute_nat_of_int_number_of real_number_of
```
```   143
```
```   144 lemmas zpowerarith = zpower_number_of_even
```
```   145   zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
```
```   146   zpower_Pls zpower_Min
```
```   147
```
```   148 (* div, mod *)
```
```   149
```
```   150 lemma adjust: "adjust b (q, r) = (if 0 \<le> r - b then (2 * q + 1, r - b) else (2 * q, r))"
```
```   151   by (auto simp only: adjust_def)
```
```   152
```
```   153 lemma negateSnd: "negateSnd (q, r) = (q, -r)"
```
```   154   by (simp add: negateSnd_def)
```
```   155
```
```   156 lemma divmod: "divmod_int a b = (if 0\<le>a then
```
```   157                   if 0\<le>b then posDivAlg a b
```
```   158                   else if a=0 then (0, 0)
```
```   159                        else negateSnd (negDivAlg (-a) (-b))
```
```   160                else
```
```   161                   if 0<b then negDivAlg a b
```
```   162                   else negateSnd (posDivAlg (-a) (-b)))"
```
```   163   by (auto simp only: divmod_int_def)
```
```   164
```
```   165 lemmas compute_div_mod = div_int_def mod_int_def divmod adjust negateSnd posDivAlg.simps negDivAlg.simps
```
```   166
```
```   167
```
```   168
```
```   169 (* collecting all the theorems *)
```
```   170
```
```   171 lemma even_Pls: "even (Int.Pls) = True"
```
```   172   apply (unfold Pls_def even_def)
```
```   173   by simp
```
```   174
```
```   175 lemma even_Min: "even (Int.Min) = False"
```
```   176   apply (unfold Min_def even_def)
```
```   177   by simp
```
```   178
```
```   179 lemma even_B0: "even (Int.Bit0 x) = True"
```
```   180   apply (unfold Bit0_def)
```
```   181   by simp
```
```   182
```
```   183 lemma even_B1: "even (Int.Bit1 x) = False"
```
```   184   apply (unfold Bit1_def)
```
```   185   by simp
```
```   186
```
```   187 lemma even_number_of: "even ((number_of w)::int) = even w"
```
```   188   by (simp only: number_of_is_id)
```
```   189
```
```   190 lemmas compute_even = even_Pls even_Min even_B0 even_B1 even_number_of
```
```   191
```
```   192 lemmas compute_numeral = compute_if compute_let compute_pair compute_bool
```
```   193                          compute_natarith compute_numberarith max_def min_def compute_num_conversions zpowerarith compute_div_mod compute_even
```
```   194
```
```   195 end
```