How to prove that a relation has functional property?

Question

Here is a simple inductive relation:

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)

Could you suggest how to prove that for the same 1st argument it will always give the same 2nd argument?

Answer 1

I would perform induction on the first premise P x y and then do a case-analysis on the second premise P x z for each of the inductive cases. Of course, you need to generalise the z of the second premise in the induction, which in total gives rise to the following proof:

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