diff options
| author | stuebinm | 2024-07-04 16:23:25 +0200 |
|---|---|---|
| committer | stuebinm | 2024-07-04 16:23:25 +0200 |
| commit | bd4c7558b96b0616023b4e4600a73a82ab2a9a3d (patch) | |
| tree | 956ad76887defd48b0c22e71719c335c388bcbb7 | |
| parent | 59214186b817329342d9d72e23adf12f7a3b1348 (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)
| -rw-r--r-- | backends/IsabelleHOL/Primitives.thy | 14 |
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 |