Theory MaxPrefix

(*  Author:     Tobias Nipkow
    Copyright   1998 TUM

section "Maximal prefix"

theory MaxPrefix
imports "HOL-Library.Sublist"

 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"

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

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]