equal
deleted
inserted
replaced
965 by (simp add: star_numeral_def) |
965 by (simp add: star_numeral_def) |
966 |
966 |
967 lemma star_of_numeral [simp]: "star_of (numeral k) = numeral k" |
967 lemma star_of_numeral [simp]: "star_of (numeral k) = numeral k" |
968 by transfer (rule refl) |
968 by transfer (rule refl) |
969 |
969 |
970 lemma star_neg_numeral_def [transfer_unfold]: |
|
971 "- numeral k = star_of (- numeral k)" |
|
972 by (simp only: star_of_minus star_of_numeral) |
|
973 |
|
974 lemma Standard_neg_numeral [simp]: "- numeral k \<in> Standard" |
|
975 using star_neg_numeral_def [of k] by simp |
|
976 |
|
977 lemma star_of_neg_numeral [simp]: "star_of (- numeral k) = - numeral k" |
|
978 by transfer (rule refl) |
|
979 |
|
980 lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)" |
970 lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)" |
981 by (induct n, simp_all) |
971 by (induct n, simp_all) |
982 |
972 |
983 lemmas star_of_compare_numeral [simp] = |
973 lemmas star_of_compare_numeral [simp] = |
984 star_of_less [of "numeral k", simplified star_of_numeral] |
974 star_of_less [of "numeral k", simplified star_of_numeral] |