theory Universe imports Main begin (* SIMPLE ORDERED UNIVERSES *) class universe = fixes lt :: "'a \ 'a \ bool" and ge :: "'a \ 'a \ bool" assumes lt_asym [simp]: "lt a b \ \ lt b a" and ge_eq_lt [simp]: "ge a b = (\ lt a b)" (* EXAMPLE INSTANCE *) instantiation nat :: universe begin definition lt_nat where "lt_nat \ (op < :: nat \ nat \ bool)" definition ge_nat where "ge_nat \ (op \ :: nat \ nat \ bool)" instance apply intro_classes apply (unfold lt_nat_def ge_nat_def) apply simp by (metis le_antisym less_or_eq_imp_le nat_le_linear nat_less_le) end end