индуктивные предикаты для фиксированного параметра кортежа

Question

давайте предположим, что мы имеем некоторый предикат

definition someP :: "('a × 'a) ⇒ 'a ⇒ 'a ⇒ bool" 

и inductive над его

inductive my_inductive :: "('a × 'a) ⇒ 'a ⇒ bool" 
for "a_b" where 
basecase: "fst a_b = a ⟹ my_inductive a_b a" | 
stepcase: "someP a_b x y ⟹ my_inductive a_b x ⟹ my_inductive a_b y" 

Индуктивный фиксируется для первого параметра «a_b». «a_b» - это кортеж, который приводит к несколько уродливому синтаксису. К сожалению, isabelle не позволяет мне писать что-то вроде for "(a,b)".

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

Answer 1

Мы можем определить новый набор правил введения my_inductive_intros с более красивой basecase и по умолчанию stepcase

lemma my_inductive_intro_1: "my_inductive (a, b) a" 
    by (simp add: my_inductive.basecase) 
lemmas my_inductive_intros = my_inductive_intro_1 my_inductive.stepcase 

Мы можем написать наши собственные красивые индукции правило

lemma my_inductive_tuple_induct[consumes 1, case_names "basecase" "stepcase", induct pred: my_inductive]: 
"my_inductive (a, b) x ⟹ 
(P a) ⟹ (⋀x y. someP (a, b) x y ⟹ my_inductive (a, b) x ⟹ P x ⟹ P y) ⟹ P x" 
apply(rule my_inductive.induct[of "(a,b)"]) 
apply(simp_all) 
done 

consumes 1 говорит Изабелль потреблять первый параметр. Проиллюстрируем это на примере:

lemma "my_inductive (a,b) c ⟹ P a b c" 
    proof(induction rule: my_inductive_tuple_induct) 

Без [consumes 1] это доказательство состояние:

1. my_inductive (my_inductive (а, б) в ⟶ P ABC)
(а, б?)
2. ? A
3. ⋀x y. someP ху ⟹ my_inductive (а, Ь?) х ⟹ х ⟹ у

С [consumes 1], получаем требуемое доказательство состояния (а, б?):

1. P аба
2. ⋀x y. someP (а, б) х у ⟹ my_inductive (а, б) х ⟹ Р а б х ⟹ Р а б у

case_names устанавливает имена случая для доказательства Изар. Таким образом, приведенное выше доказательство может начинаться с case basecase.

induct pred сообщает, что мы объявляем правило индукции. В некоторых случаях просто написать proof(induction) может быть достаточно, чтобы изабелла сама определяла использование нашего нового правила индукционной индукции.

Следующий пример демонстрирует РЕЖИМА УСТАНОВОК

lemma 
    assumes "my_inductive (a,b) c" shows "P a b c" 
    using assms 
proof (induction) 
case basecase thus ?case using my_inductive_intros sorry 
case (stepcase x y) thus ?case using my_inductive_intros sorry 
qed