Центр SQL Server 2005 года на неизвестном числе столбцов

Команда code_pred генерирует уравнения для class_roles, по одному для каждого выведенного режима, и values использует их. Теорема class_roles.equation показывает их все. Если вы хотите использовать их для доказательства своей леммы, вы должны сначала преобразовать цель или утверждение леммы так, чтобы появилась одна из сгенерированных констант class_role_.... Делать это вручную довольно громоздко.

Вы получите гораздо лучшую автоматизацию, если позволите компилятору предикатов выполнить это преобразование за вас. Поскольку лемма содержит универсально квантифицированные переменные (assoc1, assoc2, from и role), я рекомендую определить отрицание леммы как индуктивный предикат, так как отрицание превращает универсальный квантор в экзистенциальный, который моделируется свободной переменной в предположениях. Затем вы можете использовать метод доказательства eval для выполнения тяжелой работы:

inductive foo where
  "foo" if 
  "class_roles associations Employee assoc1 from role"
  "class_roles associations Employee assoc2 from role"
  "assoc1 ≠ assoc2"

code_pred foo .

lemma class_roles_unique:
  assumes "class_roles associations Employee assoc1 from role"
    and "class_roles associations Employee assoc2 from role"
  shows "assoc1 = assoc2"
proof -
  have "¬ foo" by eval
  with assms show ?thesis by(simp add: foo.simps)
qed

Обратите внимание, что eval использует генерацию и оценку кода в PolyML, поэтому он вычисляет результат, а не доказывает его. То есть оценка не проверяется ядром Изабель. Связанный метод доказательства code_simp проходит через ядро, но он не работает "из коробки" в этом примере, потому что настройка кода для String.asciis_of_literals отсутствует в Isabelle2018.

Следующие леммы обеспечивают отсутствующие уравнения кода для литеральных строк, но code_simp очень медленны с литеральными строками (normalization немного быстрее, но также не проверяется ядром Изабель).

definition dup_bit :: "bool ⇒ integer ⇒ integer" where
 "dup_bit b i = i + i + (if b then 1 else 0)"

lemma dup_bit_code [code]:
  "dup_bit True 0 = 1"
  "dup_bit False 0 = 0"
  "dup_bit True (Code_Numeral.Pos n) = Code_Numeral.Pos (num.Bit1 n)"
  "dup_bit False (Code_Numeral.Pos n) = Code_Numeral.Pos (num.Bit0 n)"
  "dup_bit True (Code_Numeral.Neg n) = - Code_Numeral.sub (num.Bit0 n) Num.One"
  "dup_bit False (Code_Numeral.Neg n) = Code_Numeral.Neg (num.Bit0 n)"
  by(simp_all add: dup_bit_def Code_Numeral.sub_def nat_of_num_add num_eq_iff)
    (metis diff_numeral_special(1) numeral_Bit0 numeral_plus_numeral sub_num_simps(2))

fun integer_of_bits :: "bool list ⇒ integer" where
  "integer_of_bits [] = 0"
| "integer_of_bits (b # bs) = dup_bit b (integer_of_bits bs)"

lemma asciis_of_literal_code [code]: 
  "String.asciis_of_literal (STR '''') = []"
  "String.asciis_of_literal (String.Literal b0 b1 b2 b3 b4 b5 b6 s) =
     integer_of_bits [b0, b1, b2, b3, b4, b5, b6] # String.asciis_of_literal s"
  including literal.lifting by(transfer; simp add: dup_bit_def; fail)+