summaryrefslogtreecommitdiff
path: root/backends/IsabelleHOL
diff options
context:
space:
mode:
authorstuebinm2024-07-04 16:23:25 +0200
committerstuebinm2024-07-04 16:23:25 +0200
commitbd4c7558b96b0616023b4e4600a73a82ab2a9a3d (patch)
tree956ad76887defd48b0c22e71719c335c388bcbb7 /backends/IsabelleHOL
parent59214186b817329342d9d72e23adf12f7a3b1348 (diff)
isabelle: more correct u32 typeisabelle
(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)
Diffstat (limited to '')
-rw-r--r--backends/IsabelleHOL/Primitives.thy14
1 files 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) \<le> 4294967295}"
+ morphisms Rep_u32 Abs_u32
+proof
+ show "0 \<in> {n. (n :: nat) \<le> 4294967295}" by simp
+qed
+
+definition u32_lt :: "u32 \<Rightarrow> u32 \<Rightarrow> bool" where
+ "u32_lt a b \<equiv> Rep_u32 a < Rep_u32 b"
+
-datatype u32 = u32 nat
datatype 'a result = Ok 'a | Err
-fun u32_lt :: "u32 \<Rightarrow> u32 \<Rightarrow> bool" where
- "u32_lt (u32 a) (u32 b) = (a < b)"
definition bind :: "'a result \<Rightarrow> ('a \<Rightarrow> 'b result) \<Rightarrow> 'b result" where
"bind m f \<equiv> (case m of Err \<Rightarrow> Err | Ok a \<Rightarrow> 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