blob: 223773154d9ab3e04952e3453acaa190181816f2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
theory Primitives imports
Main
"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 'a result = Ok 'a | Err
definition bind :: "'a result ⇒ ('a ⇒ 'b result) ⇒ 'b result" where
"bind m f ≡ (case m of Err ⇒ Err | Ok a ⇒ f a)"
adhoc_overloading Monad_Syntax.bind bind
declare bind_def[simp]
(* TODO: instantiation to make u32 usable with literal numbers etc. *)
end
|
