Definizione delle costanti sovraccariche in Isabelle

Question

Come si può definire una funzione in Isabelle che ha una definizione diversa a seconda del tipo di argomento o del tipo di contesto in cui viene utilizzata?

Ad esempio, potrei voler definire una funzione is_default con tipo 'a ⇒ bool, dove ogni diverso tipo 'a ha un "valore predefinito" potenzialmente diverso. (Sto assumendo anche, a titolo di argomentazione, che concetti esistenti come zero non sono adatti.)

Answer 1

Questo tipo di sovraccarico si adatta perfettamente alle classi di tipi. In primo luogo si definisce una classe tipo per la funzione desiderata is_default:

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

Poi si introducono le istanze arbitrari. Ad esempio, per booleani

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

ed elenca

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

Answer 2

Isabelle supporta definizioni sovraccariche definendo un nome costante e quindi fornendo in seguito la costante con nuove definizioni per tipi diversi. Questo può essere fatto con il comando consts per definire il nome della costante, e quindi il comando defs (overloaded) per fornire una definizione parziale.

Ad esempio:

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)" 

Quanto sopra funzionare anche senza il parametro (overloaded), ma causerà Isabelle ad emettere un avviso.

Al comando defs viene anche assegnato un nome, che è il nome del teorema generato da Isabelle che contiene la definizione. Questo nome può quindi essere utilizzato in prove successive:

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

Ulteriori informazioni sono disponibili nella sezione "Costanti e definizioni" nel Isablle/Isar reference manual. Inoltre, vi è un documento "Conservative Overloading in Higher-Order Logic" di Obua che discute alcuni dettagli di implementazione e trucchi per avere una tale struttura senza sacrificare la solidità.