theory Lspimports Mainbeginfun 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) qednext 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 qedqed autolemma 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 qedqedlemma 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 qedqedlemma 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 metisnext from p1 show "P [] ([], [], [])" by metisnext from p2 show "\<And>x. P [x] ([], [x], [])" by metisnext 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 qednext 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 qedqedlemma 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 simpqedlemma 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 simpqedlemma 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 simpqedlemma 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 simpnext 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 simpqedlemma 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 metisqedend