Theory MaxPrefix

(*  Author:     Tobias Nipkow
    Copyright   1998 TUM
*)

section "Maximal prefix"

theory MaxPrefix
imports "HOL-Library.Sublist"
begin

definition
 is_maxpref :: "('a list ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool" where
"is_maxpref P xs ys =
 (prefix xs ys ∧ (xs=[] ∨ P xs) ∧ (∀zs. prefix zs ys ∧ P zs ⟶ prefix zs xs))"

type_synonym 'a splitter = "'a list ⇒ 'a list * 'a list"

definition
 is_maxsplitter :: "('a list ⇒ bool) ⇒ 'a splitter ⇒ bool" where
"is_maxsplitter P f =
 (∀xs ps qs. f xs = (ps,qs) = (xs=ps@qs ∧ is_maxpref P ps xs))"

fun maxsplit :: "('a list ⇒ bool) ⇒ 'a list * 'a list ⇒ 'a list ⇒ 'a splitter" where
"maxsplit P res ps []     = (if P ps then (ps,[]) else res)" |
"maxsplit P res ps (q#qs) = maxsplit P (if P ps then (ps,q#qs) else res)
                                     (ps@[q]) qs"

declare if_split[split del]

lemma maxsplit_lemma: "(maxsplit P res ps qs = (xs,ys)) =
  (if ∃us. prefix us qs ∧ P(ps@us) then xs@ys=ps@qs ∧ is_maxpref P xs (ps@qs)
   else (xs,ys)=res)"
proof (induction P res ps qs rule: maxsplit.induct)
  case 1
  thus ?case by (auto simp: is_maxpref_def split: if_splits)
next
  case (2 P res ps q qs)
  show ?case
  proof (cases "∃us. prefix us qs ∧ P ((ps @ [q]) @ us)")
    case ex1: True
    then obtain us where "prefix us qs" "P ((ps @ [q]) @ us)" by blast
    hence ex2: "∃us. prefix us (q # qs) ∧ P (ps @ us)"
      by (intro exI[of _ "q#us"]) auto
    with ex1 and 2 show ?thesis by simp
  next
    case ex1: False
    show ?thesis
    proof (cases "∃us. prefix us (q#qs) ∧ P (ps @ us)")
      case False
      from 2 show ?thesis
        by (simp only: ex1 False) (insert ex1 False, auto simp: prefix_Cons)
    next
      case True
      note ex2 = this
      show ?thesis
      proof (cases "P ps")
        case True
        with 2 have "(maxsplit P (ps, q # qs) (ps @ [q]) qs = (xs, ys)) ⟷ (xs = ps ∧ ys = q # qs)"
          by (simp only: ex1 ex2) simp_all
        also have "… ⟷ (xs @ ys = ps @ q # qs ∧ is_maxpref P xs (ps @ q # qs))"
          using ex1 True
          by (auto simp: is_maxpref_def prefix_append prefix_Cons append_eq_append_conv2)
        finally show ?thesis using True by (simp only: ex1 ex2) simp_all
      next
        case False
        with 2 have "(maxsplit P res (ps @ [q]) qs = (xs, ys)) ⟷ ((xs, ys) = res)"
          by (simp only: ex1 ex2) simp
        also have "… ⟷ (xs @ ys = ps @ q # qs ∧ is_maxpref P xs (ps @ q # qs))"
          using ex1 ex2 False
          by (auto simp: append_eq_append_conv2 is_maxpref_def prefix_Cons)
        finally show ?thesis
          using False by (simp only: ex1 ex2) simp
      qed
    qed
  qed
qed

declare if_split[split]

lemma is_maxpref_Nil[simp]:
 "¬(∃us. prefix us xs ∧ P us) ⟹ is_maxpref P ps xs = (ps = [])"
  by (auto simp: is_maxpref_def)

lemma is_maxsplitter_maxsplit:
 "is_maxsplitter P (λxs. maxsplit P ([],xs) [] xs)"
  by (auto simp: maxsplit_lemma is_maxsplitter_def)

lemmas maxsplit_eq = is_maxsplitter_maxsplit[simplified is_maxsplitter_def]

end