1 theory Lsp

     2 imports Main

     3 begin

     4 

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

     6 where 

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

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

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

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

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

    12 

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

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

    15 where

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

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

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

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

    20 

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

    22 proof (induct rule:lsp_p.induct)

    23   case (lsp_cons_1 xs  l m r x)

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

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

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

    27   proof(cases xs, simp)

    28     case (Cons v vs)

    29     show ?thesis

    30       apply (simp add:Cons)

    31       apply (fold Cons)

    32       by (simp add:lsp_xs le_mx)

    33   qed

    34 next

    35   case (lsp_cons_2 xs l m r x)

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

    37     and lt_xm: "f x < f m"

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

    39   proof(cases xs)

    40     case (Cons v vs)

    41     show ?thesis

    42       apply (simp add:Cons)

    43       apply (fold Cons)

    44       apply (simp add:lsp_xs)

    45       by (insert lt_xm, auto)

    46   next

    47     case Nil

    48     from prems show ?thesis by simp

    49   qed

    50 qed auto

    51 

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

    53   apply (induct xs arbitrary:a c, auto)

    54   apply (case_tac xs, auto)

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

    56 

    57 

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

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

    60   case (Cons x xs)

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

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

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

    64   proof(cases xs, simp add:h)

    65     case (Cons z zs)

    66     assume eq_xs: "xs = z # zs"

    67     show ?thesis

    68     proof(cases "lsp f xs")

    69       fix l m r

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

    71       show ?thesis

    72       proof(cases m)

    73         case Nil

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

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

    76         with h show ?thesis by auto

    77       next

    78         case (Cons y ys)

    79         assume eq_m: "m = y # ys"

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

    81         show ?thesis

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

    83           case True

    84           from eq_xs eq_xs_1 True h eq_lsp show ?thesis 

    85             by (auto split:list.splits if_splits)

    86         next

    87           case False

    88           from eq_xs eq_xs_1 False h eq_lsp show ?thesis 

    89              by (auto split:list.splits if_splits)

    90         qed

    91       qed

    92     qed

    93   next

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

    95     hence "v = [x]" by simp

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

    97   qed

    98 qed

    99 

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

   101 proof(induct x, auto)

   102   case (Cons x xs)

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

   104   show ?case

   105   proof(cases xs)

   106     case Nil

   107     thus ?thesis by auto

   108   next

   109     case (Cons v vs)

   110     show ?thesis

   111     proof(cases "xs")

   112       case Nil

   113       thus ?thesis by auto

   114     next

   115       case (Cons v vs)

   116       assume eq_xs: "xs = v # vs"

   117       show ?thesis

   118       proof(cases "lsp f xs")

   119         fix l m r

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

   121         show ?thesis

   122         proof(cases m)

   123           case Nil

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

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

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

   127           with eq_xs show ?thesis by auto

   128         next

   129           case (Cons y ys)

   130           assume eq_m: "m = y # ys"

   131           show ?thesis

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

   133             case True

   134             from eq_xs eq_lsp_xs Cons True

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

   136             show ?thesis

   137             proof (simp add:eq_lsp)

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

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

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

   141               next

   142                 from lsp_mid_length [OF eq_lsp_xs] and Cons

   143                 have "m = [y]" by simp

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

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

   146               next

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

   148               qed

   149             qed

   150           next

   151             case False

   152             from eq_xs eq_lsp_xs Cons False

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

   154             show ?thesis

   155             proof (simp add:eq_lsp)

   156               from lsp_mid_length [OF eq_lsp_xs] and eq_m

   157               have "ys = []" by simp

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

   159               proof(rule lsp_cons_2)

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

   161               next

   162                 from lsp_mid_length [OF eq_lsp_xs] and Cons

   163                 have "m = [y]" by simp

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

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

   166               next

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

   168               qed

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

   170             qed

   171           qed

   172         qed

   173       qed

   174     qed

   175   qed

   176 qed

   177 

   178 lemma lsp_induct:

   179   fixes f x1 x2 P

   180   assumes h: "lsp f x1 = x2"

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

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

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

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

   185   shows "P x1 x2"

   186 proof(rule lsp_p.induct)

   187   from lsp_p_lsp_2 and h

   188   show "lsp_p f x1 x2" by metis

   189 next

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

   191 next

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

   193 next

   194   fix xs l m r x 

   195   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"

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

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

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

   199   qed

   200 next

   201   fix xs l m r x 

   202   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"

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

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

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

   206   qed

   207 qed

   208 

   209 lemma lsp_set_eq: 

   210   fixes f x u v w

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

   212   shows "x = u@v@w"

   213 proof -

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

   215     by (erule lsp_induct, simp+)

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

   217 qed

   218 

   219 lemma lsp_set: 

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

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

   222 proof -

   223   from lsp_set_eq [OF h[symmetric]] 

   224   show ?thesis by simp

   225 qed

   226 

   227 lemma max_insert_gt:

   228   fixes S fx

   229   assumes h: "fx < Max S"

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

   231   and fn: "finite S" 

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

   233 proof -

   234   from Max_insert [OF fn np]

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

   236   moreover have "\<dots> = Max S"

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

   238     case False

   239     with h

   240     show ?thesis by (simp add:max_def)

   241   next

   242     case True

   243     thus ?thesis by (simp add:max_def)

   244   qed

   245   ultimately show ?thesis by simp

   246 qed

   247 

   248 lemma max_insert_le: 

   249   fixes S fx

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

   251   and fn: "finite S"

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

   253 proof(cases "S = {}")

   254   case True

   255   thus ?thesis by simp

   256 next

   257   case False

   258   from Max_insert [OF fn False]

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

   260   moreover have "\<dots> = fx"

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

   262     case False

   263     thus ?thesis by (simp add:max_def)

   264   next

   265     case True

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

   267     from hh [OF True h]

   268     have "fx = Max S" .

   269     thus ?thesis by simp

   270   qed

   271   ultimately show ?thesis by simp

   272 qed

   273   

   274 lemma lsp_max: 

   275   fixes f x u m w

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

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

   278 proof -

   279   { fix y

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

   281     proof(erule lsp_induct, simp)

   282       { fix x u m w

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

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

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

   286     next

   287       fix xs l m r x

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

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

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

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

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

   293       proof -

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

   295         proof -

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

   297           with h4 show ?thesis

   298             apply auto

   299             by (rule_tac max_insert_le, auto)

   300         qed

   301         thus ?thesis by simp

   302       qed

   303     next

   304       fix xs l m r x

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

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

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

   308         and h4: "f x < f m"

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

   310       proof -

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

   312         with h4

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

   314           apply auto

   315           apply (rule_tac max_insert_gt, simp+)

   316           by (insert h1, simp+)

   317         thus ?thesis by auto

   318       qed

   319     qed

   320   } with h show ?thesis by metis

   321 qed

   322 

   323 end