Как мне написать собственное правило индукции для параметризованного индуктивного набора?

Я пытаюсь написать собственное правило индукции для индуктивного набора. К сожалению, когда я пытаюсь применить это с induction rule: my_induct_rule, я получаю лишнее, невозможно доказать. Имею следующее:

inductive iterate :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for f where
  iter_refl [simp]: "iterate f a a"
| iter_step [elim]: "f a b ⟹ iterate f b c ⟹ iterate f a c"

theorem my_iterate_induct: "iterate f x y ⟹ (⋀a. P a a) ⟹ 
    (⋀a b c. f a b ⟹ iterate f b c ⟹ P b c ⟹ P a c) ⟹ P x y"
  by (induction x y rule: iterate.induct) simp_all

lemma iter_step_backwards: "iterate f a b ⟹ f b c ⟹ iterate f a c"
  proof (induction a b rule: my_iterate_induct)
    ...
  qed

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

goal (3 subgoals):
 1. iterate ?f a b
 2. ⋀a. iterate f a a ⟹ f a c ⟹ iterate f a c
 3. ⋀a b ca. ?f a b ⟹ iterate ?f b ca ⟹ 
      (iterate f b ca ⟹ f ca c ⟹ iterate f b c) ⟹ iterate f a ca ⟹ 
        f ca c ⟹ iterate f a c

Цель 1, кажется, возникла из-за некоторой неспособности унифицировать? F с фактическим аргументом f, но если я проигнорирую тот факт, что f фиксирован, и попробую induction f a b rule: my_iterate_induct, я просто получу Failed to apply proof method, как и ожидалось. Как добиться хорошего поведения, которое обеспечивает обычный iterate.induct?


induction isabelle
person Zyzzyva    schedule 24.03.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Вам необходимо объявить свое настраиваемое правило индукции как «потребляющее» одну предпосылку с помощью атрибута consumes (см. Справочное руководство Isabelle / Isar, §6.5.1):

theorem my_iterate_induct [consumes 1]: "iterate f x y ⟹ (⋀a. P a a) ⟹ 
   (⋀a b c. f a b ⟹ iterate f b c ⟹ P b c ⟹ P a c) ⟹ P x y"
  by (induction x y rule: iterate.induct) simp_all
person Manuel Eberl    schedule 24.03.2018
comment
Красивый. Полагаю, из-за этого имена case_names тоже выстроятся в линию? Спасибо! - person Zyzzyva; 24.03.2018
comment
Что вы имеете в виду под «составом»? В общем, я считаю, что вам нужно добавить атрибут case_names в пользовательские правила индукции, если вам нужны необычные имена для ваших дел. - person Manuel Eberl; 24.03.2018
comment
Ну, просто, когда я вставил [case_names: iter_refl iter_step], они не были прикреплены к нужным ящикам из-за лишнего ящика в начале. Добавление [consumes 1, case_names: iter_refl iter_step] действительно работает. - person Zyzzyva; 25.03.2018