theory Lsp

imports Main

begin

fun lsp :: "('a \<Rightarrow> ('b::linorder)) \<Rightarrow> 'a list \<Rightarrow> ('a list \<times> 'a list \<times> 'a list)"

where 

   "lsp f [] = ([], [], [])" |

   "lsp f [x] = ([], [x], [])" |

   "lsp f (x#xs) = (case (lsp f xs) of

                     (l, [], r) \<Rightarrow> ([], [x], []) |

                     (l, y#ys, r) \<Rightarrow> if f x \<ge> f y then ([], [x], xs) else (x#l, y#ys, r))"

inductive lsp_p :: "('a \<Rightarrow> ('b::linorder)) \<Rightarrow> 'a list \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"

for f :: "('a \<Rightarrow> ('b::linorder))"

where

  lsp_nil [intro]: "lsp_p f [] ([], [], [])" |

  lsp_single [intro]: "lsp_p f [x] ([], [x], [])" |

  lsp_cons_1 [intro]: "\<lbrakk>xs \<noteq> []; lsp_p f xs (l, [m], r); f x \<ge> f m\<rbrakk> \<Longrightarrow> lsp_p f (x#xs) ([], [x], xs)" |

  lsp_cons_2 [intro]: "\<lbrakk>xs \<noteq> []; lsp_p f xs (l, [m], r); f x < f m\<rbrakk> \<Longrightarrow> lsp_p f (x#xs) (x#l, [m], r)"

lemma lsp_p_lsp_1: "lsp_p f x y \<Longrightarrow> y = lsp f x"

proof (induct rule:lsp_p.induct)

  case (lsp_cons_1 xs  l m r x)

  assume lsp_xs [symmetric]: "(l, [m], r) = lsp f xs"

    and le_mx: "f m \<le> f x"

  show ?case (is "?L = ?R")

  proof(cases xs, simp)

    case (Cons v vs)

    show ?thesis

      apply (simp add:Cons)

      apply (fold Cons)

      by (simp add:lsp_xs le_mx)

  qed

next

  case (lsp_cons_2 xs l m r x)

  assume lsp_xs [symmetric]: "(l, [m], r) = lsp f xs"

    and lt_xm: "f x < f m"

  show ?case (is "?L = ?R")

  proof(cases xs)

    case (Cons v vs)

    show ?thesis

      apply (simp add:Cons)

      apply (fold Cons)

      apply (simp add:lsp_xs)

      by (insert lt_xm, auto)

  next

    case Nil

    from prems show ?thesis by simp

  qed

qed auto

lemma lsp_mid_nil: "lsp f xs = (a, [], c) \<Longrightarrow> xs = []"

  apply (induct xs arbitrary:a c, auto)

  apply (case_tac xs, auto)

  by (case_tac "(lsp f (ab # list))", auto split:if_splits list.splits)

lemma lsp_mid_length: "lsp f x = (u, v, w) \<Longrightarrow> length v \<le> 1"

proof(induct x arbitrary:u v w, simp)

  case (Cons x xs)

  assume ih: "\<And> u v w. lsp f xs = (u, v, w) \<Longrightarrow> length v \<le> 1"

  and h: "lsp f (x # xs) = (u, v, w)"

  show "length v \<le> 1" using h

  proof(cases xs, simp add:h)

    case (Cons z zs)

    assume eq_xs: "xs = z # zs"

    show ?thesis

    proof(cases "lsp f xs")

      fix l m r

      assume eq_lsp: "lsp f xs = (l, m, r)"

      show ?thesis

      proof(cases m)

        case Nil

        from Nil and eq_lsp have "lsp f xs = (l, [], r)" by simp

        from lsp_mid_nil [OF this] have "xs = []" .

        with h show ?thesis by auto

      next

        case (Cons y ys)

        assume eq_m: "m = y # ys"

        from ih [OF eq_lsp] have eq_xs_1: "length m \<le> 1" .

        show ?thesis

        proof(cases "f x \<ge> f y")

          case True

          from eq_xs eq_xs_1 True h eq_lsp show ?thesis 

            by (auto split:list.splits if_splits)

        next

          case False

          from eq_xs eq_xs_1 False h eq_lsp show ?thesis 

             by (auto split:list.splits if_splits)

        qed

      qed

    qed

  next

    assume "[] = u \<and> [x] = v \<and> [] = w"

    hence "v = [x]" by simp

    thus "length v \<le> Suc 0" by simp

  qed

qed

lemma lsp_p_lsp_2: "lsp_p f x (lsp f x)"

proof(induct x, auto)

  case (Cons x xs)

  assume ih: "lsp_p f xs (lsp f xs)"

  show ?case

  proof(cases xs)

    case Nil

    thus ?thesis by auto

  next

    case (Cons v vs)

    show ?thesis

    proof(cases "xs")

      case Nil

      thus ?thesis by auto

    next

      case (Cons v vs)

      assume eq_xs: "xs = v # vs"

      show ?thesis

      proof(cases "lsp f xs")

        fix l m r

        assume eq_lsp_xs: "lsp f xs = (l, m, r)"

        show ?thesis

        proof(cases m)

          case Nil

          from eq_lsp_xs and Nil have "lsp f xs = (l, [], r)" by simp

          from lsp_mid_nil [OF this] have eq_xs: "xs = []" .

          hence "lsp f (x#xs) = ([], [x], [])" by simp

          with eq_xs show ?thesis by auto

        next

          case (Cons y ys)

          assume eq_m: "m = y # ys"

          show ?thesis

          proof(cases "f x \<ge> f y")

            case True

            from eq_xs eq_lsp_xs Cons True

            have eq_lsp: "lsp f (x#xs) = ([], [x], v # vs)" by simp

            show ?thesis

            proof (simp add:eq_lsp)

              show "lsp_p f (x # xs) ([], [x], v # vs)"

              proof(fold eq_xs, rule lsp_cons_1 [OF _])

                from eq_xs show "xs \<noteq> []" by simp

              next

                from lsp_mid_length [OF eq_lsp_xs] and Cons

                have "m = [y]" by simp

                with eq_lsp_xs have "lsp f xs = (l, [y], r)" by simp

                with ih show "lsp_p f xs (l, [y], r)" by simp

              next

                from True show "f y \<le> f x" by simp

              qed

            qed

          next

            case False

            from eq_xs eq_lsp_xs Cons False

            have eq_lsp: "lsp f (x#xs) = (x # l, y # ys, r) " by simp

            show ?thesis

            proof (simp add:eq_lsp)

              from lsp_mid_length [OF eq_lsp_xs] and eq_m

              have "ys = []" by simp

              moreover have "lsp_p f (x # xs) (x # l, [y], r)"

              proof(rule lsp_cons_2)

                from eq_xs show "xs \<noteq> []" by simp

              next

                from lsp_mid_length [OF eq_lsp_xs] and Cons

                have "m = [y]" by simp

                with eq_lsp_xs have "lsp f xs = (l, [y], r)" by simp

                with ih show "lsp_p f xs (l, [y], r)" by simp

              next

                from False show "f x < f y" by simp

              qed

              ultimately show "lsp_p f (x # xs) (x # l, y # ys, r)" by simp

            qed

          qed

        qed

      qed

    qed

  qed

qed

lemma lsp_induct:

  fixes f x1 x2 P

  assumes h: "lsp f x1 = x2"

  and p1: "P [] ([], [], [])"

  and p2: "\<And>x. P [x] ([], [x], [])"

  and p3: "\<And>xs l m r x. \<lbrakk>xs \<noteq> []; lsp f xs = (l, [m], r); P xs (l, [m], r); f m \<le> f x\<rbrakk> \<Longrightarrow> P (x # xs) ([], [x], xs)"

  and p4: "\<And>xs l m r x. \<lbrakk>xs \<noteq> []; lsp f xs = (l, [m], r); P xs (l, [m], r); f x < f m\<rbrakk> \<Longrightarrow> P (x # xs) (x # l, [m], r)"

  shows "P x1 x2"

proof(rule lsp_p.induct)

  from lsp_p_lsp_2 and h

  show "lsp_p f x1 x2" by metis

next

  from p1 show "P [] ([], [], [])" by metis

next

  from p2 show "\<And>x. P [x] ([], [x], [])" by metis

next

  fix xs l m r x 

  assume h1: "xs \<noteq> []" and h2: "lsp_p f xs (l, [m], r)" and h3: "P xs (l, [m], r)" and h4: "f m \<le> f x"

  show "P (x # xs) ([], [x], xs)" 

  proof(rule p3 [OF h1 _ h3 h4])

    from h2 and lsp_p_lsp_1 show "lsp f xs = (l, [m], r)" by metis

  qed

next

  fix xs l m r x 

  assume h1: "xs \<noteq> []" and h2: "lsp_p f xs (l, [m], r)" and h3: "P xs (l, [m], r)" and h4: "f x < f m"

  show "P (x # xs) (x # l, [m], r)"

  proof(rule p4 [OF h1 _ h3 h4])

    from h2 and lsp_p_lsp_1 show "lsp f xs = (l, [m], r)" by metis

  qed

qed

lemma lsp_set_eq: 

  fixes f x u v w

  assumes h: "lsp f x = (u, v, w)"

  shows "x = u@v@w"

proof -

  have "\<And> f x r. lsp f x = r \<Longrightarrow> \<forall> u v w. (r = (u, v, w) \<longrightarrow> x = u@v@w)" 

    by (erule lsp_induct, simp+)

  from this [rule_format, OF h] show ?thesis by simp

qed

lemma lsp_set: 

  assumes h: "(u, v, w) = lsp f x"

  shows "set (u@v@w) = set x"

proof -

  from lsp_set_eq [OF h[symmetric]] 

  show ?thesis by simp

qed

lemma max_insert_gt:

  fixes S fx

  assumes h: "fx < Max S"

  and np: "S \<noteq> {}"

  and fn: "finite S" 

  shows "Max S = Max (insert fx S)"

proof -

  from Max_insert [OF fn np]

  have "Max (insert fx S) = max fx (Max S)" .

  moreover have "\<dots> = Max S"

  proof(cases "fx \<le> Max S")

    case False

    with h

    show ?thesis by (simp add:max_def)

  next

    case True

    thus ?thesis by (simp add:max_def)

  qed

  ultimately show ?thesis by simp

qed

lemma max_insert_le: 

  fixes S fx

  assumes h: "Max S \<le> fx"

  and fn: "finite S"

  shows "fx = Max (insert fx S)"

proof(cases "S = {}")

  case True

  thus ?thesis by simp

next

  case False

  from Max_insert [OF fn False]

  have "Max (insert fx S) = max fx (Max S)" .

  moreover have "\<dots> = fx"

  proof(cases "fx \<le> Max S")

    case False

    thus ?thesis by (simp add:max_def)

  next

    case True

    have hh: "\<And> x y. \<lbrakk> x \<le> (y::('a::linorder)); y \<le> x\<rbrakk> \<Longrightarrow> x = y" by auto

    from hh [OF True h]

    have "fx = Max S" .

    thus ?thesis by simp

  qed

  ultimately show ?thesis by simp

qed

lemma lsp_max: 

  fixes f x u m w

  assumes h: "lsp f x = (u, [m], w)"

  shows "f m = Max (f ` (set x))"

proof -

  { fix y

    have "lsp f x = y \<Longrightarrow> \<forall> u m w. y = (u, [m], w) \<longrightarrow> f m = Max (f ` (set x))"

    proof(erule lsp_induct, simp)

      { fix x u m w

        assume "(([]::'a list), ([x]::'a list), ([]::'a list)) = (u, [m], w)"

        hence "f m = Max (f ` set [x])"  by simp

      } thus "\<And>x. \<forall>u m w. ([], [x], []) = (u, [m], w) \<longrightarrow> f m = Max (f ` set [x])" by simp

    next

      fix xs l m r x

      assume h1: "xs \<noteq> []"

        and h2: " lsp f xs = (l, [m], r)"

        and h3: "\<forall>u ma w. (l, [m], r) = (u, [ma], w) \<longrightarrow> f ma = Max (f ` set xs)"

        and h4: "f m \<le> f x"

      show " \<forall>u m w. ([], [x], xs) = (u, [m], w) \<longrightarrow> f m = Max (f ` set (x # xs))"

      proof -

        have "f x = Max (f ` set (x # xs))"

        proof -

          from h2 h3 have "f m = Max (f ` set xs)" by simp

          with h4 show ?thesis

            apply auto

            by (rule_tac max_insert_le, auto)

        qed

        thus ?thesis by simp

      qed

    next

      fix xs l m r x

      assume h1: "xs \<noteq> []"

        and h2: " lsp f xs = (l, [m], r)"

        and h3: " \<forall>u ma w. (l, [m], r) = (u, [ma], w) \<longrightarrow> f ma = Max (f ` set xs)"

        and h4: "f x < f m"

      show "\<forall>u ma w. (x # l, [m], r) = (u, [ma], w) \<longrightarrow> f ma = Max (f ` set (x # xs))"

      proof -

        from h2 h3 have "f m = Max (f ` set xs)" by simp

        with h4

        have "f m =  Max (f ` set (x # xs))"

          apply auto

          apply (rule_tac max_insert_gt, simp+)

          by (insert h1, simp+)

        thus ?thesis by auto

      qed

    qed

  } with h show ?thesis by metis

qed

end