Базовый стиль Изабель / Изар (упражнение 4.6)

Я заинтересован в использовании Isabelle / Isar для написания доказательств, которые могут быть прочитаны человеком и проверены машиной, и я хочу улучшить свой стиль и упростить свои доказательства.

prog-proof предлагает следующее упражнение:

Упражнение 4.6. Определите рекурсивную функцию elems :: 'a list ⇒ 'a set и докажите x ∈ elems xs ⟹ ∃ ys zs. xs = ys @ x # zs ∧ x ∉ elems ys.

Имитируя что-то похожее на то, что я бы написал ручкой и бумагой, мое решение:

fun elems :: "'a list ⇒ 'a set" where
"elems [] = {}" |
"elems (x # xs) = {x} ∪ elems xs"

fun takeUntil :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
"takeUntil f [] = []" |
"takeUntil f (x # xs) = (case (f x) of False ⇒ x # takeUntil f xs | True ⇒ [])"

theorem "x ∈ elems xs ⟹ ∃ ys zs. xs = ys @ x # zs ∧ x ∉ elems ys"
proof -
  assume 1: "x ∈ elems xs"
  let ?ys = "takeUntil (λ z. z = x) xs"
  let ?zs = "drop (length ?ys + 1) xs"
  have "xs = ?ys @ x # ?zs ∧ x ∉ elems ?ys"
  proof
    have 2: "x ∉ elems ?ys"
    proof (induction xs)
      case Nil
      thus ?case by simp
    next
      case (Cons a xs)
      thus ?case
      proof -
        {
          assume "a = x"
          hence "takeUntil (λz. z = x) (a # xs) = []" by simp
          hence A: ?thesis by simp
        }
        note eq = this
        {
          assume "a ≠ x"
          hence "takeUntil (λz. z = x) (a # xs) = a # takeUntil (λz. z = x) xs" by simp
          hence ?thesis using Cons.IH by auto
        }
        note noteq = this
        have "a = x ∨ a ≠ x" by simp
        thus ?thesis using eq noteq by blast
      qed
    qed

    from 1 have "xs = ?ys @ x # ?zs"
    proof (induction xs)
      case Nil
      hence False by simp
      thus ?case by simp
    next
      case (Cons a xs)
      {
        assume 1: "a = x"
        hence 2: "takeUntil (λz. z = x) (a # xs) = []" by simp
        hence "length (takeUntil (λz. z = x) (a # xs)) + 1 = 1" by simp
        hence 3: "drop (length (takeUntil (λz. z = x) (a # xs)) + 1) (a # xs) = xs" by simp
        from 1 2 3 have ?case by simp
      }
      note eq = this
      {
        assume 1: "a ≠ x"
        with Cons.prems have "x ∈ elems xs" by simp
        with Cons.IH
         have IH: "xs = takeUntil (λz. z = x) xs @ x # drop (length (takeUntil (λz. z = x) xs) + 1) xs" by simp
        from 1 have 2: "takeUntil (λz. z = x) (a # xs) = a # takeUntil (λz. z = x) (xs)" by simp
        from 1 have "drop (length (takeUntil (λz. z = x) (a # xs)) + 1) (a # xs) = drop (length (takeUntil (λz. z = x) xs) + 1) xs" by simp
        hence ?case using IH 2 by simp
      }
      note noteq = this
      have "a = x ∨ a ≠ x" by simp
      thus ?case using eq noteq by blast
    qed
    with 2 have 3: ?thesis by blast
    thus "xs = takeUntil (λz. z = x) xs @ x # drop (length (takeUntil (λz. z = x) xs) + 1) xs" by simp
    from 3 show "x ∉ elems (takeUntil (λz. z = x) xs)" by simp
  qed
  thus ?thesis by blast
qed

но кажется довольно длинным. В частности, я думаю, что применение закона исключенного среднего здесь громоздко, и я чувствую, что должна быть какая-то удобная схематическая переменная, такая как ?goal, которая может ссылаться на текущую цель или что-то в этом роде.

Как я могу сделать это доказательство короче, не жертвуя ясностью?