Прекращение проверки типов продукции

Question

Следующее определение функции принимается Isabelle, поэтому прекращение проверки доволен этим:

datatype 'a List = N | C 'a "'a List" 

fun dequeue' :: "'a List × 'a List ⇒ ('a option × 'a queue)" where 
    "dequeue' (N, N) = (None, AQueue N N)" 
|"dequeue' (xs, C y ys) = (Some y, AQueue xs ys)" 
|"dequeue' (xs, N) = dequeue' (N, reverse xs)" 

Это, казалось бы, эквивалентное определение, используя пользовательские, но тип изоморфные данных вместо пары , отклоняется:

fun dequeue :: "'a queue ⇒ ('a option × 'a queue)" where 
    "dequeue (AQueue N N) = (None, AQueue N N)" 
|"dequeue (AQueue xs (C y ys)) = (Some y, AQueue xs ys)" 
|"dequeue (AQueue xs N) = dequeue (AQueue N (reverse xs))" 

Почему это? Есть ли какая-то специальная настройка для пар здесь, и если да, могу ли я расширить эту настройку до моего пользовательского типа данных? Должно быть, datatype сделать это автоматически?

Answer 1

Я мог бы ответить на это сам. После того, как копаться в какой-то код, я нашел это в HOL/Fun_Def.thy:

lemma measure_fst[measure_function]: "is_measure f ⟹ is_measure (λp. f (fst p))" 
by (rule is_measure_trivial) 
lemma measure_snd[measure_function]: "is_measure f ⟹ is_measure (λp. f (snd p))" 
by (rule is_measure_trivial) 

и в самом деле, дублируя эту установку с помощью

datatype 'a queue = AQueue (young: "'a List") (old: "'a List") 

lemma [measure_function]: "is_measure f ⟹ is_measure (f ∘ young)" .. 

Второе определение функции в коде выше проходит через а.