Пожалуйста, найдите потенциально жизнеспособное решение в листинге кода ниже.
Фон
Проблема, с которой вы столкнулись, частично описана в документе «Определение рекурсивных функций в Изабель / HOL», написанном Александром Крауссом (также известенкак "Учебное пособие по определениям функций" в документации Изабель) и более подробно в диссертации доктора философии "Автоматизация рекурсивных определений и доказательств завершения в логике высшего порядка" , также написанной Александром Крауссом.В частности, см. Главу 4 в учебном пособии и раздел 3.3 в дипломной работе.
Размер t
Из вышеупомянутых ссылок возможносделать вывод, что один из способов доказать завершение sup_t - предоставить подходящую функцию измерения.В этом случае очевидно, что функция измерения, связанная с размером типа данных, может быть подходящей для приложения.К сожалению, t является вложенным типом и (в данном конкретном случае) функция по умолчанию size, похоже, не отражает рекурсивную природу типа данных - это не всегда так (см. Раздел 3.3.2 тезиса),
В качестве первого шага я предоставил новую функцию размера для t.Определение основано на общем количестве C s, содержащихся в x::t (определение должно быть легко изменить в соответствии с вашими потребностями для других приложений).
Измерение и завершение
Я обнаружил, что функция измерения (λ(xs, ys). size ys) подходит для доказательства завершения sup_t.Кроме того, эта функция измерения используется в Изабель, чтобы доказать завершение sup_t, если оно объявлено командой fun.Однако в этом случае не было возможности доказать, что аргументы рекурсивных вызовов действительно уменьшаются относительно отношения, которое было установлено мерой автоматически.Тем не менее, было бы достаточно показать, что "size (the (fmlookup x k)) < size (C x)".
К сожалению, функция supc (как указано в вашем вопросе) не является самодостаточной в отношении свойства того, что первый аргумент, передаваемый (λk x. f x (the (fmlookup ys k))), находится в области ys.Следовательно, the (fmlookup ys k) может принимать значение the None.Учитывая, что эта проблема, по-видимому, почти ортогональна основной теме вопроса, я решил не исследовать ее дальше и внес поправку в функцию supc, чтобы гарантировать, что она гарантированно вернет конкретный термин t (Вы можете явно доказать, что функция, указанная ниже, по своему поведению идентична той, которую вы указали в своем вопросе, или, в противном случае, предоставить лучшую альтернативу, которая была бы самоочевидной):
abbreviation
"supc f xs ys ≡
fmmap_keys
(λk x. if (k |∈| fmdom ys) then (f x (the (fmlookup ys k))) else A)
(fmfilter (λk. k |∈| fmdom ys) xs)"
После этой модификации предыдущая цель "size (the (fmlookup x k)) < size (C x)" была изменена на "(k |∈| fmdom ys) ⟹ size (the (fmlookup x k)) < size (C x)", что можно легко доказать (см. Лемму measure_cond).Если эта лемма объявлена как правило введения, то завершение sup_t может быть подтверждено автоматически, если оно объявлено с помощью команды fun.
Замечания
Основная причина, по которой я решил исследовать эту проблему и дать ответ, заключается в том, что я очень мало знал о некоторых основных темах этого вопроса и хотел их изучить.В результате мой ответ может быть неоптимальным из-за отсутствия опыта / знаний в этих областях.Конечно, если у вас также есть сомнения относительно того, является ли предложенное мной решение оптимальным для приложения, возможно, стоит попытаться задать вопрос в списке рассылки.
theory termination_problem
imports
Complex_Main
"HOL-Library.Finite_Map"
begin
datatype (plugins del: "size") t = A | B | C "(nat, t) fmap"
abbreviation "tcf ≡ (λ v::(nat × nat). (λ r::nat. snd v + r))"
interpretation tcf: comp_fun_commute tcf
proof
fix x y
show "tcf y ∘ tcf x = tcf x ∘ tcf y"
proof -
fix z
have "(tcf y ∘ tcf x) z = snd y + snd x + z" by auto
also have "(tcf x ∘ tcf y) z = snd y + snd x + z" by auto
ultimately have "(tcf y ∘ tcf x) z = (tcf x ∘ tcf y) z" by auto
then show "(tcf y ∘ tcf x) = (tcf x ∘ tcf y)" by auto
qed
qed
instantiation t :: size
begin
primrec t_size :: "t ⇒ nat" where
AR: "t_size A = 0" |
BR: "t_size B = 0" |
CR: "t_size (C x) =
(Suc 0) + ffold tcf 0 (fset_of_fmap (fmmap t_size x))"
definition size_t where
size_t_def: "size_t = t_size"
instance ..
end
lemma ffold_rec_exp:
assumes "k |∈| fmdom x"
and "ky = (k, the (fmlookup (fmmap t_size x) k))"
shows "ffold tcf 0 (fset_of_fmap (fmmap t_size x)) =
tcf ky (ffold tcf 0 ((fset_of_fmap (fmmap t_size x)) |-| {|ky|}))"
using assms tcf.ffold_rec by auto
lemma elem_le_ffold:
assumes "k |∈| fmdom x"
shows "t_size (the (fmlookup x k)) <
(Suc 0) + ffold tcf 0 (fset_of_fmap (fmmap t_size x))"
using ffold_rec_exp assms by auto
lemma measure_cond [intro]:
assumes "k |∈| fmdom x"
shows "size (the (fmlookup x k)) < size (C x)"
using assms elem_le_ffold size_t_def by auto
abbreviation
"supc f xs ys ≡
fmmap_keys
(λk x. if (k |∈| fmdom ys) then (f x (the (fmlookup ys k))) else A)
(fmfilter (λk. k |∈| fmdom ys) xs)"
fun sup_t (infixl "⊔" 65) where
"A ⊔ _ = A"
| "B ⊔ x = (if x = B then B else A)"
| "C xs ⊔ x = (case x of C ys ⇒ C (supc sup_t xs ys) | _ ⇒ A)"
(*Examples*)
abbreviation "list_1 ≡ fmap_of_list [(1::nat, B)]"
abbreviation "list_2 ≡ fmap_of_list [(1::nat, A), (2::nat, A)]"
value "(C list_1) ⊔ (C list_2)"
abbreviation "list_3 ≡ fmap_of_list [(1::nat, B), (3::nat, A)]"
abbreviation "list_4 ≡ fmap_of_list [(2::nat, A), (4::nat, B)]"
value "(C list_3) ⊔ (C list_4)"
abbreviation "list_5 ≡ fmap_of_list [(1::nat, B), (2::nat, B)]"
abbreviation "list_6 ≡ fmap_of_list [(2::nat, B), (4::nat, B)]"
value "(C list_5) ⊔ (C list_6)"
abbreviation "list_7 ≡
fmap_of_list [(1::nat, B), (2::nat, C list_5), (3::nat, A)]"
abbreviation "list_8 ≡ fmap_of_list [(2::nat, B), (4::nat, B)]"
value "(C list_7) ⊔ (C list_8)"
abbreviation "list_9 ≡
fmap_of_list [(1::nat, B), (2::nat, C list_5), (3::nat, A)]"
abbreviation "list_10 ≡ fmap_of_list [(2::nat, C list_6), (3::nat, B)]"
value "(C list_9) ⊔ (C list_10)"
end