107 where |
107 where |
108 "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))" |
108 "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))" |
109 |
109 |
110 lemmas compute_natarith = bitarith natnorm natsuc natadd natsub natmul nateq natless natle natfac.simps |
110 lemmas compute_natarith = bitarith natnorm natsuc natadd natsub natmul nateq natless natle natfac.simps |
111 |
111 |
112 lemma number_eq: "(((number_of x)::'a::{number_ring, ordered_idom}) = (number_of y)) = (x = y)" |
112 lemma number_eq: "(((number_of x)::'a::{number_ring, linordered_idom}) = (number_of y)) = (x = y)" |
113 unfolding number_of_eq |
113 unfolding number_of_eq |
114 apply simp |
114 apply simp |
115 done |
115 done |
116 |
116 |
117 lemma number_le: "(((number_of x)::'a::{number_ring, ordered_idom}) \<le> (number_of y)) = (x \<le> y)" |
117 lemma number_le: "(((number_of x)::'a::{number_ring, linordered_idom}) \<le> (number_of y)) = (x \<le> y)" |
118 unfolding number_of_eq |
118 unfolding number_of_eq |
119 apply simp |
119 apply simp |
120 done |
120 done |
121 |
121 |
122 lemma number_less: "(((number_of x)::'a::{number_ring, ordered_idom}) < (number_of y)) = (x < y)" |
122 lemma number_less: "(((number_of x)::'a::{number_ring, linordered_idom}) < (number_of y)) = (x < y)" |
123 unfolding number_of_eq |
123 unfolding number_of_eq |
124 apply simp |
124 apply simp |
125 done |
125 done |
126 |
126 |
127 lemma number_diff: "((number_of x)::'a::{number_ring, ordered_idom}) - number_of y = number_of (x + (- y))" |
127 lemma number_diff: "((number_of x)::'a::{number_ring, linordered_idom}) - number_of y = number_of (x + (- y))" |
128 apply (subst diff_number_of_eq) |
128 apply (subst diff_number_of_eq) |
129 apply simp |
129 apply simp |
130 done |
130 done |
131 |
131 |
132 lemmas number_norm = number_of_Pls[symmetric] numeral_1_eq_1[symmetric] |
132 lemmas number_norm = number_of_Pls[symmetric] numeral_1_eq_1[symmetric] |