Работа с генератором кода Изабеллы: Данные уточнения и более высокого порядка функции

Question

Это является продолжением на Isabelle's Code generation: Abstraction lemmas for containers?:

Я хочу, чтобы сгенерировать код для the_question в следующей теории:

theory Scratch imports Main begin 

typedef small = "{x::nat. x < 10}" morphisms to_nat small 
    by (rule exI[where x = 0], simp) 
code_datatype small 
lemma [code abstype]: "small (to_nat x) = x" by (rule to_nat_inverse) 

definition a_pred :: "small ⇒ bool" 
    where "a_pred = undefined" 

definition "smaller j = [small i . i <- [0 ..< to_nat j]]" 

definition "the_question j = (∀i ∈ set (smaller j). a_pred j)" 

Проблема заключается в том что уравнение для smaller не подходит для генерации кода, поскольку оно упоминает функцию абстракции small.

Теперь в соответствии с ответом Андреаса на мой последний вопрос, и документ по уточнению данных, следующим шагом является введение типа для множества малых чисел и создать определение для smaller в этом типе:

typedef small_list = "{l. ∀x∈ set l. (x::nat) < 10}" by (rule exI[where x = "[]"], auto) 
code_datatype Abs_small_list 
lemma [code abstype]: "Abs_small_list (Rep_small_list x) = x" by (rule Rep_small_list_inverse) 

definition "smaller' j = Abs_small_list [ i . i <- [0 ..< to_nat j]]" 
lemma smaller'_code[code abstract]: "Rep_small_list (smaller' j) = [ i . i <- [0 ..< to_nat j]]" 
    unfolding smaller'_def 
    by (rule Abs_small_list_inverse, cases j, auto elim: less_trans simp add: small_inverse) 

Теперь smaller' является исполняемым. Из того, что я понимаю, что нужно переопределить операции small list как операции на small_list:

definition "small_list_all P l = list_all P (map small (Rep_small_list l))" 

lemma[code]: "the_question j = small_list_all a_pred (smaller' j)" 
    unfolding small_list_all_def the_question_def smaller'_code smaller_def Ball_set by simp 

Я могу определить, хорошо выглядящий уравнение кода для the_question. Но определение small_list_all не подходит для генерации кода, так как в нем упоминается морфизм абстракции small. Как сделать small_list_all исполняемым?

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

Answer 1

Короткий ответ no, it does not work.

Долгий ответ заключается в том, что часто возможны обходные пути. Один из них показан Брайаном в его ответе. Основная идея, кажется,

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

В примере Брайана эта функция predecessor. Или, как еще один простой пример, предположим, что функция,

definition smallPrime :: "nat ⇒ small option" 
    where "smallPrime n = (if n ∈ {2,3,5,7} then Some (small n) else None)" 

Это определение не является допустимым уравнение кода, из-за появления small. Но это происходит один:

definition smallPrimeHelper :: "nat ⇒ small" 
    where "smallPrimeHelper n = (if n ∈ {2,3,5,7} then small n else small 0)" 
lemma [code abstract]: "to_nat (smallPrimeHelper n) = (if n ∈ {2,3,5,7} then n else 0)" 
    by (auto simp add: smallPrimeHelper_def intro: small_inverse) 
lemma [code_unfold]: "smallPrime n = (if n ∈ {2,3,5,7} then Some (smallPrimeHelper n) else None)" 
    unfolding smallPrime_def smallPrimeHelper_def by simp 

Если один хочет, чтобы избежать избыточного вычисления предиката (который может быть более сложным, чем просто ∈ {2,3,5,7}, можно сделать тип возврата помощника умнее, вводя абстрактное представление, т.е. тип, который содержит как результат вычисления, и информация, необходимая для построения абстрактного типа из него:

typedef smallPrime_view = "{(x::nat, b::bool). x < 10 ∧ b = (x ∈ {2,3,5,7})}" 
    by (rule exI[where x = "(2, True)"], auto) 
setup_lifting type_definition_small 
setup_lifting type_definition_smallPrime_view 

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

lift_definition smallPrimeHelper' :: "nat ⇒ smallPrime_view" 
    is "λ n. if n ∈ {2,3,5,7} then (n, True) else (0, False)" by simp 
lift_definition smallPrimeView_pred :: "smallPrime_view ⇒ bool" 
    is "λ spv :: (nat × bool) . snd spv" by auto 
lift_definition smallPrimeView_small :: "smallPrime_view ⇒ small" 
    is "λ spv :: (nat × bool) . fst spv" by auto 
lemma [simp]: "smallPrimeView_pred (smallPrimeHelper' n) ⟷ (n ∈ {2,3,5,7})" 
    by transfer simp 
lemma [simp]: "n ∈ {2,3,5,7} ⟹ to_nat (smallPrimeView_small (smallPrimeHelper' n)) = n" 
    by transfer auto 
lemma [simp]: "n ∈ {2,3,5,7} ⟹ smallPrimeView_small (smallPrimeHelper' n) = small n" 
    by (auto intro: iffD1[OF to_nat_inject] simp add: small_inverse) 

При том, что мы можем получить уравнение кода, который делает проверку только один раз:

lemma [code]: "smallPrime n = 
    (let spv = smallPrimeHelper' n in 
    (if smallPrimeView_pred spv 
    then Some (smallPrimeView_small spv) 
    else None))" 
    by (auto simp add: smallPrime_def Let_def) 

Answer 2

У меня нет хорошего решения общей проблемы, но вот идея, которая позволит вам генерировать код для the_question в этом конкретном случае.

Сначала определите функцию predecessor :: "small ⇒ small с абстрактным кодовым уравнением (возможно, используя lift_definition от λn::nat. n - 1).

Теперь вы можете доказать новое уравнение кода для smaller которого шк использует если-то-иначе, predecessor и нормальный список операций:

lemma smaller_code [code]: 
    "smaller j = (if to_nat j = 0 then [] 
    else let k = predecessor j in smaller k @ [k])" 

(Более эффективные реализации, конечно, возможно, если вы готовы определите вспомогательную функцию.)

Генерация кода должна теперь работать для smaller, так как это уравнение кода не использует функцию small.