theory Domain_example
imports Expr
begin
--"When interpreting, we have to instantiate the type for domains. As an example, we take a type containing 'low' and 'high' as domains."
datatype Dom = low | high
instantiation Dom :: order
begin
definition
less_eq_Dom_def: "d1 ≤ d2 = (if d1 = d2 then True
else (if d1 = low then True else False))"
definition
less_Dom_def: "d1 < d2 = (if d1 = d2 then False
else (if d1 = low then True else False))"
instance proof
fix x y z :: Dom
show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
unfolding less_eq_Dom_def less_Dom_def by auto
show "x ≤ x" unfolding less_eq_Dom_def by auto
show "[|x ≤ y; y ≤ z|] ==> x ≤ z"
unfolding less_eq_Dom_def by ((split split_if_asm)+, auto)
show "[|x ≤ y; y ≤ x|] ==> x = y"
unfolding less_eq_Dom_def by ((split split_if_asm)+,
auto, (split split_if_asm)+, auto)
qed
end
end