summaryrefslogtreecommitdiff
path: root/backends/IsabelleHOL
diff options
context:
space:
mode:
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