262
+ − 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