# Theory MaxPrefix

```(*  Author:     Tobias Nipkow
*)

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
```