equal
deleted
inserted
replaced
8 theory Num_Lemmas imports Parity begin |
8 theory Num_Lemmas imports Parity begin |
9 |
9 |
10 lemma contentsI: "y = {x} ==> contents y = x" |
10 lemma contentsI: "y = {x} ==> contents y = x" |
11 unfolding contents_def by auto |
11 unfolding contents_def by auto |
12 |
12 |
13 lemma prod_case_split: "prod_case = split" |
|
14 by (rule ext)+ auto |
|
15 |
|
16 lemmas split_split = prod.split [unfolded prod_case_split] |
|
17 lemmas split_split_asm = prod.split_asm [unfolded prod_case_split] |
|
18 lemmas "split.splits" = split_split split_split_asm |
13 lemmas "split.splits" = split_split split_split_asm |
19 |
14 |
20 lemmas funpow_0 = funpow.simps(1) |
15 lemmas funpow_0 = funpow.simps(1) |
21 lemmas funpow_Suc = funpow.simps(2) |
16 lemmas funpow_Suc = funpow.simps(2) |
22 |
17 |
29 lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by auto |
24 lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by auto |
30 |
25 |
31 constdefs |
26 constdefs |
32 mod_alt :: "'a => 'a => 'a :: Divides.div" |
27 mod_alt :: "'a => 'a => 'a :: Divides.div" |
33 "mod_alt n m == n mod m" |
28 "mod_alt n m == n mod m" |
34 |
|
35 declare iszero_0 [iff] |
|
36 |
29 |
37 lemmas xtr1 = xtrans(1) |
30 lemmas xtr1 = xtrans(1) |
38 lemmas xtr2 = xtrans(2) |
31 lemmas xtr2 = xtrans(2) |
39 lemmas xtr3 = xtrans(3) |
32 lemmas xtr3 = xtrans(3) |
40 lemmas xtr4 = xtrans(4) |
33 lemmas xtr4 = xtrans(4) |
68 "0 < (number_of w :: nat) ==> |
61 "0 < (number_of w :: nat) ==> |
69 number_of w - (1 :: nat) = number_of (Numeral.pred w)" |
62 number_of w - (1 :: nat) = number_of (Numeral.pred w)" |
70 apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def) |
63 apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def) |
71 apply (simp add: number_of_eq nat_diff_distrib [symmetric]) |
64 apply (simp add: number_of_eq nat_diff_distrib [symmetric]) |
72 done |
65 done |
73 |
|
74 lemma of_int_power: |
|
75 "of_int (a ^ n) = (of_int a ^ n :: 'a :: {recpower, comm_ring_1})" |
|
76 by (induct n) (auto simp add: power_Suc) |
|
77 |
66 |
78 lemma zless2: "0 < (2 :: int)" |
67 lemma zless2: "0 < (2 :: int)" |
79 by auto |
68 by auto |
80 |
69 |
81 lemmas zless2p [simp] = zless2 [THEN zero_less_power] |
70 lemmas zless2p [simp] = zless2 [THEN zero_less_power] |