Search code examples
isabelle

Is it a good idea to extend standard types and operations?

I need to defined an extended bool type (ebool = bool ∪ {⊥}) and a set of operations for the type (conjunction, etc.).

Here is the theory:

theory EboolTest
  imports Main "~~/src/HOL/Library/Adhoc_Overloading"
begin

notation
  bot ("⊥")

declare [[coercion_enabled]]

typedef ebool = "UNIV :: bool option set" ..

definition ebool :: "bool ⇒ ebool" where
  "ebool b = Abs_ebool (Some b)"

declare [[coercion "ebool :: bool ⇒ ebool"]]

instantiation ebool :: bot
begin
definition "⊥ ≡ Abs_ebool None"
instance ..
end

free_constructors case_ebool for
  ebool
| "⊥ :: ebool"
  apply (metis Rep_ebool_inverse bot_ebool_def ebool_def not_Some_eq)
  apply (smt Abs_ebool_inverse ebool_def iso_tuple_UNIV_I option.inject)
  by (simp add: Abs_ebool_inject bot_ebool_def ebool_def)

lemmas ebool2_cases = ebool.exhaust[case_product ebool.exhaust]
lemmas ebool3_cases = ebool.exhaust[case_product ebool.exhaust ebool.exhaust]

fun ebool_and :: "ebool ⇒ ebool ⇒ ebool" (infixr "∧" 35) where
  "ebool_and a b = ebool (HOL.conj a b)"
| "ebool_and False _ = False"
| "ebool_and _ False = False"
| "ebool_and ⊥ _ = ⊥"
| "ebool_and _ ⊥ = ⊥"

no_notation HOL.conj (infixr "∧" 35)
consts "(∧)" :: "'a ⇒ 'a ⇒ 'a"
adhoc_overloading "(∧)" HOL.conj
adhoc_overloading "(∧)" ebool_and

end

The following works fine:

value "True ∧ (False::ebool)"
value "True ∧ ⊥"

But the following returns ebool, but I expect to see bool:

value "True ∧ False"

It seems my approach is bad. Could you suggest a better approach? Maybe I it's not good to overload standard operations at all?

Solution

  • First of all, I'm a little surprised that this:

    consts "(∧)" :: "'a ⇒ 'a ⇒ 'a"

    works at all. It sounds like a bug, because the (...) notation is reserved for the system. (To be fair, it does print a warning, and unless you know exactly what you're doing, it's unwise to ignore them.)

    But to circle back to your actual problem, I don't think you should use adhoc_overloading to overload syntax that would otherwise be provided by Main.

    There are alternatives. For example, you could use a bold version. This is used in this theory.

    Or you could use another symbol, like &&.

    As an addendum: I believe there might be weird interactions between coercions and adhoc overloading. Both tools are fine by themselves, but watch out if they interact with each other.