Индуктивный предикат, перечисляющий элементы множества

Question

Можно ли заставить работать следующий пример?

inductive elems where
  "x |∈| xs ⟹
   elems xs x"

code_pred [show_modes] elems .

values "{x. elems {|1::nat,2,3|} x}"

Answer 1

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

lemma fmember_code_predI [code_pred_intro]:
  "x |∈| xs" if "Predicate_Compile.contains (fset xs) x"
  using that by(simp add: Predicate_Compile.contains_def fmember.rep_eq)

code_pred fmember
  by(simp add: Predicate_Compile.contains_def fmember.rep_eq)

Вот почему это работает: константа Predicate_Compile.contains реализует перечисление для обычных наборов, и компилятор предикатов знает об этом. Лемма с атрибутом code_pred_intro говорит компилятору предиката обрабатывать членство на fset, как если бы оно было определено как индуктивный предикат с оператором леммы в качестве правила введения. В самой команде code_pred вам необходимо доказать соответствующее правило исключения. Этих двух правил (правила введения и исключения) достаточно для того, чтобы компилятор предикатов выполнил анализ мод, скомпилировал уравнения и подтвердил их правильность.

Вам даже не нужно определять свой собственный предикат elems. Членство на fset работает напрямую:

values "{x. x |∈| {|1::nat,2,3|}}"