Расторжение доказательство с функциями, используя набор постижений

Question

Рассмотрим следующую глупое определение Isabelle деревьев и поддеревьев:

datatype tree = Leaf int 
       | Node tree tree 

fun children :: "tree ⇒ tree set" where 
"children (Leaf _) = {}" | 
"children (Node a b) = {a, b}" 

lemma children_decreasing_size: 
    assumes "c ∈ children t" 
    shows "size c < size t" 
using assms 
by (induction t, auto) 

function subtrees :: "tree ⇒ tree set" where 
"subtrees t = { s | c s. c ∈ children t ∧ s ∈ subtrees c }" 
by auto 
termination 
apply (relation "measure size", simp) 

Расторжение доказательство subtrees застревает в этой точке, хотя рекурсивные вызовы только когда-либо делали на детей, которые строго ограничены обоснованным отношением size (как показывает тривиальная лемма).

Доказательство состояния выглядит следующим образом:

goal (1 subgoal): 
1. ⋀t x xa xb. (xa, t) ∈ measure size 

Это невозможно доказать, конечно, так как информация, что xa является дочерним t теряется. Я сделал что-то не так? Есть ли что-нибудь, что я могу сделать, чтобы сохранить доказательство? Хочу отметить, что я могу сформулировать такое же определение, используя списки вместо множества:

fun children_list :: "tree ⇒ tree list" where 
"children_list (Leaf _) = []" | 
"children_list (Node a b) = [a, b]" 

function subtrees_list :: "tree ⇒ tree list" where 
"subtrees_list t = concat (map subtrees_list (children_list t))" 
by auto 
termination 
apply (relation "measure size", simp) 

и получить более информативный, доказуемую терминации цель:

goal (1 subgoal): 
1. ⋀t x. 
     x ∈ set (children_list t) ⟹ 
     (x, t) ∈ measure size 

Является ли это некоторые ограничения в Изабелле, что я должен просто работать вокруг, не используя наборы для этого?

Answer 1

Ограничение на c : children t в установленном понимании для subtrees не отображается в обязательстве о прекращении действия, поскольку пакет функций ничего не знает априори около &. Для достижения этой цели можно использовать правила сопоставления. В этом случае вы можете локально объявить conj_cong как [fundef_cong], чтобы по существу имитировать порядок оценки слева направо (хотя в HOL нет такой вещи, как оценка). Например,

context notes conj_cong[fundef_cong] begin 
fun subtrees :: ... 
termination ... 
end 

Контекст блок гарантирует, что декларация conj_cong[fundef_cong] только в силу для этого определения функции.

Версия со списками работает, потому что она использует функцию map, для которой по умолчанию установлено правило сравнения. То же самое должно было работать для множеств, если вы использовали операцию монодального связывания на наборах (а не на основе набора).