equal
deleted
inserted
replaced
49 |
49 |
50 setup NumeralSyntax.setup |
50 setup NumeralSyntax.setup |
51 |
51 |
52 abbreviation |
52 abbreviation |
53 "Numeral0 \<equiv> number_of Pls" |
53 "Numeral0 \<equiv> number_of Pls" |
|
54 |
|
55 abbreviation |
54 "Numeral1 \<equiv> number_of (Pls BIT B1)" |
56 "Numeral1 \<equiv> number_of (Pls BIT B1)" |
55 |
57 |
56 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)" |
58 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)" |
57 -- {* Unfold all @{text let}s involving constants *} |
59 -- {* Unfold all @{text let}s involving constants *} |
58 unfolding Let_def .. |
60 unfolding Let_def .. |
62 |
64 |
63 lemma Let_1 [simp]: "Let 1 f = f 1" |
65 lemma Let_1 [simp]: "Let 1 f = f 1" |
64 unfolding Let_def .. |
66 unfolding Let_def .. |
65 |
67 |
66 definition |
68 definition |
67 succ :: "int \<Rightarrow> int" |
69 succ :: "int \<Rightarrow> int" where |
68 "succ k = k + 1" |
70 "succ k = k + 1" |
69 pred :: "int \<Rightarrow> int" |
71 |
|
72 definition |
|
73 pred :: "int \<Rightarrow> int" where |
70 "pred k = k - 1" |
74 "pred k = k - 1" |
71 |
75 |
72 lemmas numeral_simps = |
76 lemmas numeral_simps = |
73 succ_def pred_def Pls_def Min_def Bit_def |
77 succ_def pred_def Pls_def Min_def Bit_def |
74 |
78 |