equal
deleted
inserted
replaced
2016 |
2016 |
2017 lemma uint_mod: "uint ((x :: 'a :: len word) mod y) = uint x mod uint y" |
2017 lemma uint_mod: "uint ((x :: 'a :: len word) mod y) = uint x mod uint y" |
2018 unfolding uint_nat by (simp add : unat_mod zmod_int) |
2018 unfolding uint_nat by (simp add : unat_mod zmod_int) |
2019 |
2019 |
2020 |
2020 |
2021 subsection {* Definition of @[text unat_arith} tactic *} |
2021 subsection {* Definition of @{text unat_arith} tactic *} |
2022 |
2022 |
2023 lemma unat_split: |
2023 lemma unat_split: |
2024 fixes x::"'a::len word" |
2024 fixes x::"'a::len word" |
2025 shows "P (unat x) = |
2025 shows "P (unat x) = |
2026 (ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)" |
2026 (ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)" |