From bd4c7558b96b0616023b4e4600a73a82ab2a9a3d Mon Sep 17 00:00:00 2001 From: stuebinm Date: Thu, 4 Jul 2024 16:23:25 +0200 Subject: isabelle: more correct u32 type (I'd have to figure out how to do the code equation stuff to make this type actually usable the way nat is, but it should behave correctly in proofs) --- backends/IsabelleHOL/Primitives.thy | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/backends/IsabelleHOL/Primitives.thy b/backends/IsabelleHOL/Primitives.thy index a0cc40bd..22377315 100644 --- a/backends/IsabelleHOL/Primitives.thy +++ b/backends/IsabelleHOL/Primitives.thy @@ -3,11 +3,17 @@ theory Primitives imports "HOL-Library.Monad_Syntax" begin +typedef u32 = "{n. (n :: nat) \ 4294967295}" + morphisms Rep_u32 Abs_u32 +proof + show "0 \ {n. (n :: nat) \ 4294967295}" by simp +qed + +definition u32_lt :: "u32 \ u32 \ bool" where + "u32_lt a b \ Rep_u32 a < Rep_u32 b" + -datatype u32 = u32 nat datatype 'a result = Ok 'a | Err -fun u32_lt :: "u32 \ u32 \ bool" where - "u32_lt (u32 a) (u32 b) = (a < b)" definition bind :: "'a result \ ('a \ 'b result) \ 'b result" where "bind m f \ (case m of Err \ Err | Ok a \ f a)" @@ -16,4 +22,6 @@ adhoc_overloading Monad_Syntax.bind bind declare bind_def[simp] +(* TODO: instantiation to make u32 usable with literal numbers etc. *) + end \ No newline at end of file -- cgit v1.2.3