如何證明一個關係具有功能屬性？

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