Как упростить индуктивный предикат с помощью оценки?

Question

Я определил очень простую объектно-ориентированную модель.Модель определяет набор классов и набор ассоциаций.

nonterminal fmaplets and fmaplet

syntax
  "_fmaplet"  :: "['a, 'a] ⇒ fmaplet"              ("_ /↦⇩f/ _")
  "_fmaplets" :: "['a, 'a] ⇒ fmaplet"              ("_ /[↦⇩f]/ _")
  ""          :: "fmaplet ⇒ fmaplets"              ("_")
  "_FMaplets" :: "[fmaplet, fmaplets] ⇒ fmaplets"  ("_,/ _")
  "_FMapUpd"  :: "['a ⇀ 'b, fmaplets] ⇒ 'a ⇀ 'b" ("_/'(_')" [900, 0] 900)
  "_FMap"     :: "fmaplets ⇒ 'a ⇀ 'b"             ("(1[_])")

syntax (ASCII)
  "_fmaplet"  :: "['a, 'a] ⇒ fmaplet"              ("_ /|->f/ _")
  "_fmaplets" :: "['a, 'a] ⇒ fmaplet"              ("_ /[|->f]/ _")

translations
  "_FMapUpd m (_FMaplets xy ms)"      ⇌ "_FMapUpd (_FMapUpd m xy) ms"
  "_FMapUpd m (_fmaplet  x y)"        ⇌ "CONST fmupd x y m"
  "_FMap ms"                          ⇌ "_FMapUpd (CONST fmempty) ms"
  "_FMap (_FMaplets ms1 ms2)"         ↽ "_FMapUpd (_FMap ms1) ms2"
  "_FMaplets ms1 (_FMaplets ms2 ms3)" ↽ "_FMaplets (_FMaplets ms1 ms2) ms3"

datatype classes1 =
  Object | Person | Employee | Customer | Project | Task | Sprint

abbreviation "associations ≡ [
  STR ''ProjectManager'' ↦⇩f [
    STR ''projects'' ↦⇩f (Project, 0::nat, 100::nat),
    STR ''manager'' ↦⇩f (Employee, 1, 1)],
  STR ''ProjectMember'' ↦⇩f [
    STR ''member_of'' ↦⇩f (Project, 0, 100),
    STR ''members'' ↦⇩f (Employee, 1, 20)],
  STR ''ManagerEmployee'' ↦⇩f [
    STR ''line_manager'' ↦⇩f (Employee, 0, 1),
    STR ''project_manager'' ↦⇩f (Employee, 0, 100),
    STR ''employees'' ↦⇩f (Employee, 3, 7)],
  STR ''ProjectCustomer'' ↦⇩f [
    STR ''projects'' ↦⇩f (Project, 0, 100),
    STR ''customer'' ↦⇩f (Customer, 1, 1)],
  STR ''ProjectTask'' ↦⇩f [
    STR ''project'' ↦⇩f (Project, 1, 1),
    STR ''tasks'' ↦⇩f (Task, 0, 100)],
  STR ''SprintTaskAssignee'' ↦⇩f [
    STR ''sprint'' ↦⇩f (Sprint, 0, 10),
    STR ''tasks'' ↦⇩f (Task, 0, 5),
    STR ''assignee'' ↦⇩f (Employee, 0, 1)]]"

Я также определил предикат class_roles, который связывает класс с набором ассоциаций и концами, доступными из этого класса:

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)

definition "assoc_end_class ≡ fst"

inductive assoc_refer_class where
  "role |∈| fmdom ends ⟹
   fmlookup ends role = Some end ⟹
   assoc_end_class end = ? ⟹
   assoc_refer_class ends ? role"

code_pred [show_modes] assoc_refer_class .

inductive class_roles where
  "assoc |∈| fmdom assocs ⟹
   fmlookup assocs assoc = Some ends ⟹
   assoc_refer_class ends ? from ⟹
   role |∈| fmdom ends ⟹
   fmlookup ends role = Some end ⟹
   role ≠ from ⟹
   class_roles assocs ? assoc from role"

code_pred [show_modes] class_roles .

values "{(x, y, z, a). class_roles associations x y z a}"

Этот предикат может быть оценен очень быстро (см. Последнюю строку выше).

Мне нужно доказать, что все концы ассоциации уникальны для каждого класса.Для простоты я пытаюсь доказать это для Employee класса:

lemma fmupd_to_rhs:
  "fmupd k x xm = y ⟷ y = fmupd k x xm"
  by auto

lemma class_roles_unique:
  "class_roles associations Employee assoc1 from role ⟹
   class_roles associations Employee assoc2 from role ⟹ assoc1 = assoc2"
  apply (erule class_roles.cases; erule class_roles.cases;
     erule assoc_refer_class.cases; erule assoc_refer_class.cases)
  unfolding fmupd_to_rhs
  apply (simp)
  apply (elim disjE)
  apply auto[1]
  apply auto[1]
  apply auto[1]
  (* And so on... Proving of each case is very slow *)

Проблема в том, что он очень медленный.Можно ли упростить предикат class_roles, используя леммы, сгенерированные code_pred?Или вы могли бы предложить лучший подход, чтобы доказать эту лемму?

Answer 1

Команда 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 проходит через ядро, но в этом примере он не работает "из коробки", поскольку в Isabelle2018 отсутствует настройка кода для String.asciis_of_literals.

Следующие леммы содержат отсутствующий кодуравнения для литеральных строк, но 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)+