我想证明，在列表的元素传递关系相当于上列出了传递关系（在某些条件下）。
这是第一个引理：
lemma list_all2_rtrancl1:
"(list_all2 P)⇧*⇧* xs ys ⟹
list_all2 P⇧*⇧* xs ys"
apply (induct rule: rtranclp_induct)
apply (simp add: list.rel_refl)
by (smt list_all2_trans rtranclp.rtrancl_into_rtrancl)
这里是一个对称的引理：
lemma list_all2_rtrancl2:
"(⋀x. P x x) ⟹
list_all2 P⇧*⇧* xs ys ⟹
(list_all2 P)⇧*⇧* xs ys"
apply (erule list_all2_induct)
apply simp
我猜的关系应该是反思。 但是，也许我应该用另一种假设。 引理可以证明如果假定P是传递的，但是P是不可传递的。 我卡住了。 你可以建议选择什么样的假设，以及如何证明这个引理？
看来，鸡蛋里挑骨头给我的最后引理的特殊情况下，错误的反例（ xs = [0]和ys = [2]
lemma list_all2_rtrancl2_example:
"list_all2 (λx y. x = y ∨ Suc x = y)⇧*⇧* xs ys ⟹
(list_all2 (λx y. x = y ∨ Suc x = y))⇧*⇧* xs ys"
nitpick
我可以证明引理适用于这个例子：
lemma list_all2_rtrancl2_example_0_2:
"list_all2 (λx y. x = y ∨ Suc x = y)⇧*⇧* [0] [2] ⟹
(list_all2 (λx y. x = y ∨ Suc x = y))⇧*⇧* [0] [2]"
apply (rule_tac ?b="[1]" in converse_rtranclp_into_rtranclp; simp)
apply (rule_tac ?b="[2]" in converse_rtranclp_into_rtranclp; simp)
done
这可能是使用可行listrel代替list_all2 。 实际上，如以下所示，它们是等效的（参见set_listrel_eq_list_all2 ）。 不过，也有大约标准库的几个定理listrel没有它们的等价物的list_all2 。
theory so_htlatrfetl_2
imports Complex_Main
begin
lemma set_listrel_eq_list_all2:
"listrel {(x, y). r x y} = {(xs, ys). list_all2 r xs ys}"
using list_all2_conv_all_nth listrel_iff_nth by fastforce
lemma listrel_tclosure_1: "(listrel r)⇧* ⊆ listrel (r⇧*)"
by (simp add: listrel_rtrancl_eq_rtrancl_listrel1
listrel_subset_rtrancl_listrel1 rtrancl_subset_rtrancl)
lemma listrel_tclosure_2: "refl r ⟹ listrel (r⇧*) ⊆ (listrel r)⇧*"
by (simp add: listrel1_subset_listrel listrel_rtrancl_eq_rtrancl_listrel1
rtrancl_mono)
context includes lifting_syntax
begin
lemma listrel_list_all2_transfer [transfer_rule]:
"((=) ===> (=) ===> (=) ===> (=))
(λr xs ys. (xs, ys) ∈ listrel {(x, y). r x y}) list_all2"
unfolding rel_fun_def using set_listrel_eq_list_all2 listrel_iff_nth by blast
end
lemma list_all2_rtrancl_1:
"(list_all2 r)⇧*⇧* xs ys ⟹ list_all2 r⇧*⇧* xs ys"
proof(transfer)
fix r :: "'a ⇒ 'a ⇒ bool"
fix xs :: "'a list"
fix ys:: "'a list"
assume "(λxs ys. (xs, ys) ∈ listrel {(x, y). r x y})⇧*⇧* xs ys"
then have "(xs, ys) ∈ (listrel {(x, y). r x y})⇧*"
unfolding rtranclp_def rtrancl_def by auto
then have "(xs, ys) ∈ listrel ({(x, y). r x y}⇧*)"
using listrel_tclosure_1 by auto
then show "(xs, ys) ∈ listrel {(x, y). r⇧*⇧* x y}"
unfolding rtranclp_def rtrancl_def by auto
qed
lemma list_all2_rtrancl_2:
"reflp r ⟹ list_all2 r⇧*⇧* xs ys ⟹ (list_all2 r)⇧*⇧* xs ys"
proof(transfer)
fix r :: "'a ⇒ 'a ⇒ bool"
fix xs :: "'a list"
fix ys :: "'a list"
assume as_reflp: "reflp r"
assume p_in_lr: "(xs, ys) ∈ listrel {(x, y). r⇧*⇧* x y}"
from as_reflp have refl: "refl {(x, y). r x y}"
using reflp_refl_eq by fastforce
from p_in_lr have "(xs, ys) ∈ listrel ({(x, y). r x y}⇧*)"
unfolding rtranclp_def rtrancl_def by auto
with refl have "(xs, ys) ∈ (listrel {(x, y). r x y})⇧*"
using listrel_tclosure_2 by auto
then show "(λxs ys. (xs, ys) ∈ listrel {(x, y). r x y})⇧*⇧* xs ys"
unfolding rtranclp_def rtrancl_def by auto
qed
end
对于直接证明list_all2还提供（传统）：
-
list_all2_induct被施加到名单; 基本情况是微不足道的。 从那里，它仍然表明(LP)* x#xs y#ys如果(L (P*)) xs ys ， (LP)* xs ys和P* xy 。 - 我们的想法是，它是有可能找到
zs （如xs ），使得(LP) xs zs和(LP)+ zs ys 。 - 然后，考虑到
P* xy和P xx基于所述传递属性，通过感应P* ， (LP) x#xs y#zs 。 因此，同样， (LP)* x#xs y#zs 。 - 此外，假定
(LP)+ zs ys和P yy ，通过感应， (LP)+ y#zs y#ys 。 因此，同样， (LP)* y#zs y#ys 。 - 从图3和4的结论
(LP)* x#xs y#ys 。
theory so_htlatrfetl
imports Complex_Main
begin
lemma list_all2_rtrancl2:
assumes as_r: "(⋀x. P x x)"
shows "(list_all2 P⇧*⇧*) xs ys ⟹ (list_all2 P)⇧*⇧* xs ys"
proof(induction rule: list_all2_induct)
case Nil then show ?case by simp
next
case (Cons x xs y ys) show ?case
proof -
from as_r have lp_xs_xs: "list_all2 P xs xs" by (rule list_all2_refl)
from Cons.hyps(1) have x_xs_y_zs: "(list_all2 P)⇧*⇧* (x#xs) (y#xs)"
proof(induction rule: rtranclp_induct)
case base then show ?case by simp
next
case (step y z) then show ?case
proof -
have rt_step_2: "(list_all2 P)⇧*⇧* (y#xs) (z#xs)"
by (rule r_into_rtranclp, rule list_all2_Cons[THEN iffD2])
(simp add: step.hyps(2) lp_xs_xs)
from step.IH rt_step_2 show ?thesis by (rule rtranclp_trans)
qed
qed
from Cons.IH have "(list_all2 P)⇧*⇧* (y#xs) (y#ys)"
proof(induction rule: rtranclp_induct)
case base then show ?case by simp
next
case (step ya za) show ?case
proof -
have rt_step_2: "(list_all2 P)⇧*⇧* (y#ya) (y#za)"
by (rule r_into_rtranclp, rule list_all2_Cons[THEN iffD2])
(simp add: step.hyps(2) as_r)
from step.IH rt_step_2 show ?thesis by (rule rtranclp_trans)
qed
qed
with x_xs_y_zs show ?thesis by simp
qed
qed
end
作为一个方面说明，在我看来（我知道很少挑剔），鸡蛋里挑骨头不应该没有任何警告无效提供的反。 我认为，通常情况下，当nitpick “嫌疑人”是一个反例可能是无效的它通知的例子是“潜在的虚假”的用户。 这可能是有用的，如果这个问题没有得到其他地方的记录提交错误报告。
