How to define a semilattice of lists?

I'm trying to define an upper semilattice:

A ≺ B
... ≺ C [B,B,B] ≺ C [B,B] ≺ C [B] ≺ B
C [A] ≺ C [B]
C [A,A] ≺ C [A,B] ≺ C [B,B]
C [A,A] ≺ C [B,A] ≺ C [B,B]
C [A,A,A] ≺ C [A,A,B] ≺ C [A,B,B] ≺ C [B,B,B]
C [A,A,A] ≺ C [A,B,A] ≺ C [A,B,B] ≺ C [B,B,B]
C [A,A,A] ≺ C [A,A,B] ≺ C [B,A,B] ≺ C [B,B,B]
C [A,A,A] ≺ C [B,A,A] ≺ C [B,A,B] ≺ C [B,B,B]
C [A,A,A] ≺ C [A,B,A] ≺ C [B,B,A] ≺ C [B,B,B]
C [A,A,A] ≺ C [B,A,A] ≺ C [B,B,A] ≺ C [B,B,B]
and so on...

I need to prohibit a direct relations of the form:

C [A,A] ≺ C [B,B]
C [A,A,B] ≺ C [B,B,B]
and so on...

Only one element must differ in preceding elements. I will define this indirect relations as a transitive closure.

I tried to define it as follows:

datatype t = A | B | C "t list"

definition "only_one p xs ys ≡
  let xys = zip xs ys in
  length xs = length ys ∧
  list_all (λ(x, y). x = y ∨ p x y) xys ∧
  length xs =
    length (takeWhile (λ(x, y). x = y) xys) +
    length (takeWhile (λ(x, y). x = y) (rev xys)) + 1"

inductive prec_t ("_ ≺ _" [65, 65] 65) where
  "A ≺ B"
| "C [B] ≺ B"
| "C (xs@[B]) ≺ C xs"
| "only_one (λx y. x ≺ y) xs ys ⟹
   C xs ≺ C ys"

But I get the following error:

Proof failed.
 1. ⋀x y xa xb xs ys.
       x (?x47 x y xa xb xs ys) (?x48 x y xa xb xs ys) ⟶
       y (?x47 x y xa xb xs ys) (?x48 x y xa xb xs ys) ⟹
       only_one x xs ys ⟶ only_one y xs ys
The error(s) above occurred for the goal statement⌂:
mono
 (λp x1 x2.
     x1 = A ∧ x2 = B ∨
     x1 = C [B] ∧ x2 = B ∨
     (∃xs. x1 = C (xs @ [B]) ∧ x2 = C xs) ∨ (∃xs ys. x1 = C xs ∧ x2 = C ys ∧ only_one p xs ys))

Could you suggest how to fix it?

UPDATE

I redefined the condition checker as follows. But it doesn't help.

primrec only_one' :: "bool ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool" where
  "only_one' found p xs [] = (case xs of [] ⇒ found | _ ⇒ False)"
| "only_one' found p xs (y # ys) = (case xs of [] ⇒ False | z # zs ⇒
    if z = y then only_one' found p zs ys else
    let found' = p z y in
    if found ∧ found' then False else only_one' found' p zs ys)"

abbreviation "only_one ≡ only_one' False"

UPDATE 2

An inductive definition doesn't help too:

inductive only_one :: "bool ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool" where
  "only_one True p [] []"
| "x = y ⟹
   only_one found p xs ys ⟹
   only_one found p (x#xs) (y#ys)"
| "p x y ⟹
   found = False ⟹
   only_one True p xs ys ⟹
   only_one found p (x#xs) (y#ys)"

Solution

Your inductive definition is not accepted, since Isabelle does not know that only_one is monotone.

Therefore, the following code in front of your inductive definition should solve your problem.

lemma only_one_mono: "(⋀ x y. x ∈ set xs ⟹ y ∈ set ys ⟹ p x y ⟶ q x y) ⟹ 
  only_one p xs ys ⟶ only_one q xs ys" sorry

declare only_one_mono[mono]

Best, René