Определение перегруженных констант в Isabelle

Question

Как определить функцию в Isabelle, которая имеет другое определение в зависимости от типа аргумента или типа контекста, в котором он используется?

Например, я хотел бы определить функции is_default с типом 'a ⇒ bool, где каждый другой тип 'a имеет потенциально различное «значение по умолчанию». (Я также предполагаю, что для аргументов, что существующие концепции, такие как zero, не подходят.)

Answer 1

Этот вид перегрузки выглядит идеально подходящим для классов типов. Сначала нужно определить класс типа для искомой функции is_default:

class is_default = 
    fixes is_default :: "'a ⇒ bool" 

Затем ввести произвольные экземпляры. Например, для Booleans

instantiation bool :: is_default 
begin 
definition "is_default (b::bool) ⟷ b" 
instance .. 
end 

и списки

instantiation list :: (type) is_default 
begin 
definition "is_default (xs::'a list) ⟷ xs = []" 
instance .. 
end 

Answer 2

Isabelle поддерживает перегруженные определения, определяя константное имя, а затем предоставляя константу новые определения для разных типов. Это можно сделать с помощью команды consts для определения имени константы, а затем команды defs (overloaded) для предоставления частичного определения.

Например:

consts is_default :: "'a ⇒ bool" 

defs (overloaded) is_default_nat: 
    "is_default a ≡ ((a::nat) = 0)" 

defs (overloaded) is_default_option: 
    "is_default a ≡ (a = None)" 

Вышесказанное также будет работать без параметра (overloaded), но заставит Изабеллу выдать предупреждение.

Команда defs также имеет имя, которое является именем теоремы, порожденной Изабеллой, которая содержит определение. Это имя может быть использовано в следующих доказательствах:

lemma "¬ is_default (Some 3)" 
    by (clarsimp simp: is_default_option) 

Более подробная информация доступна в разделе «Константа и определение» в Isablle/Isar reference manual. Кроме того, Obua описывает бумагу "Conservative Overloading in Higher-Order Logic", в которой обсуждаются некоторые детали реализации и gotchas, имеющие такую ​​структуру без ущерба для надежности.