--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/Attic/Lsp.thy Sun Feb 05 21:00:12 2012 +0000
@@ -0,0 +1,323 @@
+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