type_synonym name = string
datatype variable = varname: Var name

instantiation variable::ord begin
  fun less_eq_variable::"variable ⇒ variable ⇒ bool" where
    "less_eq_variable (variable.Var x) (variable.Var y) = (String.implode x ≤ String.implode y)"

  fun less_variable::"variable ⇒ variable ⇒ bool" where
    "less_variable (variable.Var x) (variable.Var y) = (String.implode x < String.implode y)"
instance proof
qed
end

instantiation variable::proper_interval begin
  fun not_adj::"variable ⇒ variable ⇒ bool" where
    "not_adj (variable.Var x) (variable.Var y) = (y ≠ (x @ [CHR 0x00]))"

  fun proper_interval_variable::"variable proper_interval" where
    "proper_interval_variable None None = True"
  | "proper_interval_variable None (Some (variable.Var x)) = (x ≠ [])"
  | "proper_interval_variable (Some x) None = True"
  | "proper_interval_variable (Some x) (Some y) = (less x y ∧ not_adj x y)"
instance proof
  show "proper_interval None None = True"
qed
end

instantiation variable::proper_interval begin
  fun proper_interval_variable::"variable proper_interval" where
    "proper_interval_variable None None = True"
  | "proper_interval_variable None (Some (variable.Var x)) = (x ≠ [])"
  | "proper_interval_variable (Some x) None = True"
  | "proper_interval_variable (Some (variable.Var x)) (Some (variable.Var y)) =
    (less (variable.Var x) (variable.Var y) ∧ y ≠ (x @ [CHR 0x00]))"
instance proof
  show "proper_interval None None = True"
qed
end

  show "proper_interval (None::variable option) None = True"
    sorry