palindrome_converse

Pal_Converse.thy

lemma nat_inducts_all:
  "⋀P n. P 0 ⟹ (⋀n :: nat. (⋀m :: nat. m ≤ n ⟹ P m) ⟹ P (Suc n)) ⟹ P n"
proof-
  fix P and n :: nat
  assume a: "P 0" "⋀n :: nat. (⋀m :: nat. m ≤ n ⟹ P m) ⟹ P (Suc n)"
  show "P n"
    proof (rule nat_less_induct)
      fix na
      assume a2: "∀m<na. P m"
      show "P na"
        apply (cases na, simp, rule a(1), simp, rule a(2))
        using a2 by simp
    qed
qed

lemma induct_by_length:
  fixes l :: "'a list"
  assumes P_0: "P []"
  and P_step: "⋀l n. length l = Suc n ⟹ (⋀la. length la ≤ n ⟹ P la) ⟹ P l"
  shows "P l"
using nat_inducts_all [of "λk. ∀l. length l = k ⟶ P l"] apply rule
proof (simp, rule P_0, auto)
  fix n and x :: "'a list"
  assume h: "⋀m. m ≤ n ⟹ ∀x. length x = m ⟶ P x" "length x = Suc n"
  hence "⋀la. length la ≤ n ⟹ P la" by simp
  thus "P x" using P_step [OF h(2)] by simp
qed

theorem palindrome_converse: "l = rev l ⟹ l ∈ pal"
using induct_by_length [of "λl. l = rev l ⟶ l ∈ pal"] apply rule
proof (auto, rule)
  fix la :: "'a list" and n
  assume "l = rev l"
  and a: "length la = Suc n" "⋀la :: 'a list. length la ≤ n ⟹ la = rev la ⟶ la ∈ pal" "la = rev la"
  from a(1) obtain x xs where xxs: "la = x # xs" using neq_Nil_conv [of la] by auto
  from a(3) have 1: "last la = x" using xxs by simp

  have 2: "(la = [x]) ∨ (∃ys. la = x # ys @ [x])"
    using xxs 1 by (metis append_Cons append_butlast_last_id butlast.simps(2) list.distinct(1))

  have "la = [x] ⟹ la ∈ pal"
    by (simp, rule)
  moreover have "∃ys. la = x # ys @ [x] ⟹ la ∈ pal"
    proof-
      assume "∃ys. la = x # ys @ [x]"
      then obtain ys where ys: "la = x # ys @ [x]" by auto
      have "rev ys = ys" using a(3) by (simp add: ys)
      have "length ys ≤ n"
        using a(1) by (simp add: ys)
      thus "la ∈ pal"
        using a(2) [OF `length ys ≤ n`]
        by (simp add: `rev ys = ys` ys, rule_tac pal_cons, simp)
    qed
  ultimately
    show "la ∈ pal" by (metis 2)
qed