如何证明一个关系具有泛函属性？

Question

这是一个简单的归纳关系：

datatype t1 = A t1 t1 | B
datatype t2 = C t2 t2 | D

inductive P :: "t1 ⇒ t2 ⇒ bool" where
  "P x1 y1 ⟹ P x2 y2 ⟹ P (A x1 x2) (C y1 y2)" |
  "P B D"

lemma P_fun:
  "P x y ⟹ P x z ⟹ y = z"
  apply (erule P.cases)

你能建议如何证明对于相同的第一个参数它总是给出相同的第二个参数吗？

Answer 1

我会在第一个前提 P x y 上进行归纳，然后对每个归纳案例在第二个前提 P x z 上进行案例分析。当然，归纳还需要对第二个前提的z进行归纳，总共得到如下证明：

lemma P_fun:
  "P x y ⟹ P x z ⟹ y = z"
proof (induct x y arbitrary: z rule: P.induct)
  case (1 x1 y1 x2 y2)
  from `P (A x1 x2) z` obtain z1 z2 
    where "z = C z1 z2" "P x1 z1" "P x2 z2" by (cases, auto)
  with 1 show ?case by auto
next
  case 2
  then show ?case by (cases, auto)
qed

如何证明一个关系具有泛函属性？

How to prove that a relation has functional property?

theorem-proving

isabelle