1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory ListLibLemmas
8imports List_Lib LemmaBucket
9begin
10
11(* This theory contains various list results that
12are used in proofs related to the abstract cdt_list.*)
13
14(* Sorting a list given a partial ordering, where
15        elements are only necessarily comparable if
16        relation R holds between them. *)
17locale partial_sort =
18  fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
19  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
20
21  assumes all_comp: "\<And>x y. R x y \<Longrightarrow> (less x y \<or> less y x)"
22
23  (*This is only necessary to guarantee the uniqueness of
24    sorted lists. *)
25  assumes antisym: "\<And>x y. R x y \<Longrightarrow> less x y \<and> less y x \<Longrightarrow> x = y"
26
27  assumes trans: "\<And>x y z. less x y \<Longrightarrow>  less y z \<Longrightarrow> less x z"
28
29begin
30
31primrec pinsort :: " 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
32   "pinsort x [] = [x]" |
33   "pinsort x (y#ys) = (if (less x y) then (x#y#ys) else y#(pinsort x ys))"
34
35inductive psorted :: "'a list \<Rightarrow> bool" where
36  Nil [iff]: "psorted []"
37| Cons: "\<forall>y\<in>set xs. less x y \<Longrightarrow> psorted xs \<Longrightarrow> psorted (x # xs)"
38
39definition R_set where
40"R_set S \<equiv> \<forall>x y. x \<in> S \<longrightarrow> y \<in> S \<longrightarrow> R x y"
41
42abbreviation R_list where
43"R_list xs \<equiv> R_set (set xs)"
44
45definition psort :: "'a list \<Rightarrow> 'a list" where
46"psort xs = foldr pinsort xs []"
47
48end
49
50context partial_sort begin
51
52lemma psorted_Cons: "psorted (x#xs) = (psorted xs & (\<forall> y \<in> set xs. less x y))"
53  apply (rule iffI)
54  apply (erule psorted.cases,simp)
55   apply clarsimp
56  apply (rule psorted.Cons,clarsimp+)
57  done
58
59lemma psorted_distinct_set_unique:
60assumes "psorted xs" "distinct xs" "psorted ys" "distinct ys" "set xs = set ys"
61        "R_list xs"
62shows "xs = ys"
63proof -
64  from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
65  from assms show ?thesis
66  proof(induct rule:list_induct2[OF 1])
67    case 1 show ?case by simp
68  next
69    case 2 thus ?case
70    by (simp add: psorted_Cons R_set_def)
71         (metis Diff_insert_absorb antisym insertE insert_iff)
72  qed
73qed
74
75
76lemma pinsort_set: "set (pinsort a xs) = insert a (set xs)"
77  apply (induct xs)
78  apply simp
79  apply simp
80  apply blast
81  done
82
83lemma all_comp': "R x y \<Longrightarrow> \<not>less x y \<Longrightarrow> less y x"
84  apply (cut_tac x=x and y=y in all_comp,simp+)
85  done
86
87lemma pinsort_sorted: "R_set (insert a (set xs)) \<Longrightarrow> psorted xs \<Longrightarrow> psorted (pinsort a xs)"
88  apply (induct xs arbitrary: a)
89  apply (simp add: psorted_Cons)
90  apply (simp add: psorted_Cons)
91  apply clarsimp
92  apply (simp add: pinsort_set)
93  apply (intro impI conjI)
94    apply (intro ballI)
95    apply (drule_tac x=x in bspec)
96     apply simp
97    apply (frule(1) trans)
98    apply simp
99   apply (simp add: R_set_def)
100  apply (rule all_comp')
101   apply (simp add: R_set_def)
102  apply simp
103  done
104
105lemma psort_set: "set (psort xs) = set xs"
106  apply (simp add: psort_def)
107  apply (induct xs)
108   apply simp
109  apply (simp add: pinsort_set)
110  done
111
112lemma psort_psorted: "R_list xs \<Longrightarrow> psorted (psort xs)"
113  apply (simp add: psort_def)
114  apply (induct xs)
115   apply simp
116  apply simp
117  apply (cut_tac xs =xs in psort_set)
118  apply (simp add: psort_def)
119  apply (rule pinsort_sorted)
120   apply simp
121  apply (simp add: R_set_def)
122  done
123
124
125lemma insort_length: "length (pinsort a xs) = Suc (length xs)"
126  apply (induct xs)
127  apply simp
128  apply simp
129  done
130
131lemma psort_length: "length (psort xs) = length xs"
132  apply (simp add: psort_def)
133  apply (induct xs)
134   apply simp
135  apply simp
136  apply (simp add: insort_length)
137  done
138
139lemma pinsort_distinct: "\<lbrakk>a \<notin> set xs; distinct xs\<rbrakk>
140       \<Longrightarrow> distinct (pinsort a xs)"
141  apply (induct xs)
142  apply simp
143  apply (clarsimp simp add: pinsort_set)
144  done
145
146lemma psort_distinct: "distinct xs \<Longrightarrow> distinct (psort xs)"
147  apply (simp add: psort_def)
148  apply (induct xs)
149   apply simp
150  apply simp
151  apply (rule pinsort_distinct)
152   apply (fold psort_def)
153   apply (simp add: psort_set)+
154  done
155
156
157lemma in_can_split: "y \<in> set list \<Longrightarrow> \<exists>ys xs. list = xs @ (y # ys)"
158  apply (induct list)
159   apply simp
160  apply clarsimp
161  apply (elim disjE)
162   apply simp
163   apply force
164  apply simp
165  apply (elim exE)
166  apply simp
167  apply (rule_tac x=ys in exI)
168  apply force
169  done
170
171lemma lsorted_sorted:
172assumes lsorted: "\<And>x y xs ys . list = xs @ (x # y # ys) \<Longrightarrow> less x y"
173shows "psorted list"
174  apply (insert lsorted)
175  apply atomize
176  apply simp
177  apply (induct list)
178   apply simp
179  apply (simp add: psorted_Cons)
180  apply (rule context_conjI)
181   apply (erule meta_mp)
182   apply clarsimp
183   apply (drule_tac x="a#xs" in spec)
184   apply (drule_tac x=x in spec)
185   apply (drule_tac x=y in spec)
186   apply (erule mp)
187   apply force
188  apply (intro ballI)
189  apply clarsimp
190  apply (drule in_can_split)
191  apply (elim exE)
192  apply (drule_tac x="[]" in spec)
193  apply simp
194  apply (case_tac xs)
195   apply simp
196  apply (clarsimp simp add: psorted_Cons)
197  apply (blast intro: trans)
198  done
199
200
201lemma psorted_set: "finite A \<Longrightarrow> R_set A \<Longrightarrow> \<exists>!xs. set xs = A \<and> psorted xs \<and> distinct xs"
202  apply (drule finite_distinct_list)
203  apply clarify
204  apply (rule_tac a="psort xs" in ex1I)
205   apply (auto simp: psorted_distinct_set_unique psort_set psort_psorted psort_distinct)
206done
207
208end
209
210
211text \<open>These list operations roughly correspond to cdt
212        operations.\<close>
213
214lemma after_can_split: "after_in_list list x = Some y \<Longrightarrow> \<exists>ys xs. list = xs @ (x # y # ys)"
215  apply (induct list x rule: after_in_list.induct)
216  apply simp+
217  apply (simp split: if_split_asm)
218   apply force
219  apply (elim exE)
220  apply simp
221  apply (rule_tac x="ys" in exI)
222  apply simp
223  done
224
225lemma distinct_inj_middle: "distinct list \<Longrightarrow> list = (xa @ x # xb) \<Longrightarrow> list = (ya @ x # yb) \<Longrightarrow> xa = ya \<and> xb = yb"
226  apply (induct list arbitrary: xa ya)
227  apply simp
228  apply clarsimp
229  apply (case_tac "xa")
230   apply simp
231   apply (case_tac "ya")
232    apply simp
233   apply clarsimp
234  apply clarsimp
235  apply (case_tac "ya")
236   apply (simp (no_asm_simp))
237   apply simp
238  apply clarsimp
239  done
240
241
242lemma after_can_split_distinct:
243  "distinct list \<Longrightarrow> after_in_list list x = Some y \<Longrightarrow> \<exists>!ys. \<exists>!xs. list = xs @ (x # y # ys)"
244  apply (frule after_can_split)
245  apply (elim exE)
246  apply (rule ex1I)
247   apply (rule ex1I)
248    apply assumption
249   apply simp
250  apply (elim ex1E)
251  apply (thin_tac "\<forall>x. P x" for P)
252  apply (frule_tac yb="y#ysa" in distinct_inj_middle,assumption+)
253  apply simp
254  done
255
256
257lemma after_ignore_head: "x \<notin> set list \<Longrightarrow> after_in_list (list @ list') x = after_in_list list' x"
258  apply (induct list x rule: after_in_list.induct)
259  apply simp
260   apply simp
261   apply (case_tac list',simp+)
262  done
263
264
265lemma after_distinct_one_sibling: "distinct list \<Longrightarrow> list = xs @ x # y # ys \<Longrightarrow> after_in_list list x = Some y"
266  apply (induct xs)
267  apply simp
268  apply simp
269  apply clarsimp
270  apply (subgoal_tac "after_in_list ((a # xs) @ (x # y # ys)) x = after_in_list (x # y # ys) x")
271   apply simp
272  apply (rule after_ignore_head)
273  apply simp
274  done
275
276
277lemma (in partial_sort) after_order_sorted:
278assumes after_order: "\<And>x y. after_in_list list x = Some y \<Longrightarrow> less x y"
279assumes distinct: "distinct list"
280shows "psorted list"
281  apply (rule lsorted_sorted)
282  apply (rule after_order)
283  apply (erule after_distinct_one_sibling[OF distinct])
284  done
285
286lemma hd_not_after_in_list:
287  "\<lbrakk>distinct xs; x \<notin> set xs\<rbrakk> \<Longrightarrow> after_in_list (x # xs) a \<noteq> Some x"
288  apply (induct xs a rule: after_in_list.induct)
289    apply simp+
290  apply fastforce
291  done
292
293lemma after_in_list_inj:
294  "\<lbrakk>distinct list; after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk>
295    \<Longrightarrow> a = b"
296  apply(induct list)
297   apply(simp)
298  apply(simp)
299  apply(case_tac "a=aa")
300   apply(case_tac list, simp)
301   apply(simp add: hd_not_after_in_list split: if_split_asm)
302  apply(case_tac list, simp)
303  apply(simp add: hd_not_after_in_list split: if_split_asm)
304  done
305
306lemma list_replace_ignore:"a \<notin> set list \<Longrightarrow> list_replace list a b = list"
307  apply (simp add: list_replace_def)
308  apply (induct list,clarsimp+)
309  done
310
311lemma list_replace_empty[simp]: "list_replace [] a b = []"
312  by (simp add: list_replace_def)
313
314lemma list_replace_empty2[simp]:
315  "(list_replace list a b = []) = (list = [])"
316  by (simp add: list_replace_def)
317
318lemma after_in_list_list_replace: "\<lbrakk>p \<noteq> dest; p \<noteq> src;
319         after_in_list list p = Some src\<rbrakk>
320        \<Longrightarrow> after_in_list (list_replace list src dest) p = Some dest"
321  apply (simp add: list_replace_def)
322  apply (induct list)
323   apply simp+
324  apply (case_tac list)
325   apply simp+
326  apply (intro conjI impI,simp+)
327  done
328
329lemma replace_list_preserve_after: "dest \<notin> set list \<Longrightarrow> distinct list \<Longrightarrow>  after_in_list (list_replace list src dest) dest = after_in_list list src"
330  apply (simp add: list_replace_def)
331  apply (induct list src rule: after_in_list.induct)
332    apply (simp+)
333  apply fastforce
334  done
335
336lemma replace_list_preserve_after': "\<lbrakk>p \<noteq> dest; p \<noteq> src;
337         after_in_list list p \<noteq> Some src\<rbrakk>
338        \<Longrightarrow> after_in_list (list_replace list src dest) p = after_in_list list p"
339  apply (simp add: list_replace_def)
340  apply (induct list p rule: after_in_list.induct)
341    apply (simp+)
342  apply fastforce
343  done
344
345lemma distinct_after_in_list_not_self:
346  "distinct list \<Longrightarrow> after_in_list list src \<noteq> Some src"
347  apply (induct list,simp+)
348  apply (case_tac list,clarsimp+)
349  done
350
351lemma set_list_insert_after:
352  "set (list_insert_after list a b) = set list \<union> (if a \<in> set list then {b} else {})"
353  apply(induct list)
354   apply(simp)
355  apply(simp)
356  done
357
358lemma distinct_list_insert_after:
359  "\<lbrakk>distinct list; b \<notin> set list \<or> a \<notin> set list\<rbrakk> \<Longrightarrow> distinct (list_insert_after list a b)"
360  apply(induct list)
361   apply(simp)
362  apply(fastforce simp: set_list_insert_after)
363  done
364
365lemma list_insert_after_after:
366  "\<lbrakk>distinct list; b \<notin> set list; a \<in> set list\<rbrakk>
367    \<Longrightarrow> after_in_list (list_insert_after list a b) p
368    = (if p = a then Some b else if p = b then after_in_list list a else after_in_list list p)"
369  apply(induct list p rule: after_in_list.induct)
370    apply (simp split: if_split_asm)+
371  apply fastforce
372  done
373
374lemma list_remove_removed:
375  "set (list_remove list x) = (set list) - {x}"
376  apply (induct list,simp+)
377  apply blast
378  done
379
380
381lemma remove_distinct_helper: "\<lbrakk>distinct (list_remove list x); a \<noteq> x; a \<notin> set list;
382        distinct list\<rbrakk>
383       \<Longrightarrow> a \<notin> set (list_remove list x)"
384  apply (induct list)
385   apply (simp split: if_split_asm)+
386  done
387
388
389lemma list_remove_distinct:
390  "distinct list \<Longrightarrow>  distinct (list_remove list x)"
391  apply (induct list)
392  apply (simp add: remove_distinct_helper split: if_split_asm)+
393  done
394
395lemma list_remove_none: "x \<notin> set list \<Longrightarrow> list_remove list x = list"
396  apply (induct list)
397  apply clarsimp+
398  done
399
400lemma replace_distinct: "x \<notin> set list \<Longrightarrow> distinct list \<Longrightarrow> distinct (list_replace list y x)"
401  apply (induct list)
402  apply (simp add: list_replace_def)+
403  apply blast
404  done
405
406lemma set_list_replace_list:
407  "\<lbrakk>distinct list; slot \<in> set list; slot \<notin> set list'\<rbrakk>
408    \<Longrightarrow> set (list_replace_list list slot list') = set list \<union> set list' - {slot}"
409  apply (induct list)
410  apply auto
411  done
412
413lemma after_in_list_in_list:
414  "after_in_list list a = Some b \<Longrightarrow> b \<in> set list"
415  apply(induct list a arbitrary: b rule: after_in_list.induct)
416  apply (simp split: if_split_asm)+
417  done
418
419lemma list_replace_empty_after_empty:
420  "\<lbrakk>after_in_list list p = Some slot; distinct list\<rbrakk>
421    \<Longrightarrow> after_in_list (list_replace_list list slot []) p = after_in_list list slot"
422  apply(induct list slot rule: after_in_list.induct)
423  apply (simp split: if_split_asm)+
424   apply (case_tac xs,simp+)
425  apply (case_tac xs,simp+)
426  apply (auto dest!: after_in_list_in_list)
427  done
428
429lemma list_replace_after_fst_list:
430  "\<lbrakk>after_in_list list p = Some slot; distinct list\<rbrakk>
431    \<Longrightarrow> after_in_list (list_replace_list list slot (x # xs)) p = Some x"
432  apply(induct list p rule: after_in_list.induct)
433  apply (simp split: if_split_asm)+
434  apply (drule after_in_list_in_list)+
435  apply force
436  done
437
438lemma after_in_list_append_notin_hd:
439  "p \<notin> set list' \<Longrightarrow> after_in_list (list' @ list) p = after_in_list list p"
440  apply(induct list', simp, simp)
441  apply(case_tac list', simp)
442   apply(case_tac list, simp+)
443   done
444
445lemma after_in_list_append_last_hd:
446  "\<lbrakk>p \<in> set list'; after_in_list list' p = None\<rbrakk>
447    \<Longrightarrow> after_in_list (list' @ x # xs) p = Some x"
448  apply(induct list' p rule: after_in_list.induct)
449    apply(simp)
450   apply(simp)
451  apply(simp split: if_split_asm)
452  done
453
454lemma after_in_list_append_in_hd:
455  "after_in_list list p = Some a \<Longrightarrow> after_in_list (list @ list') p = Some a"
456  apply(induct list p rule: after_in_list.induct)
457    apply(simp split: if_split_asm)+
458    done
459
460lemma after_in_list_in_list': "after_in_list list a = Some y \<Longrightarrow> a \<in> set list"
461  apply (induct list a rule: after_in_list.induct)
462  apply simp+
463  apply force
464  done
465
466lemma list_replace_after_None_notin_new:
467  "\<lbrakk>after_in_list list p = None; p \<notin> set list'\<rbrakk>
468    \<Longrightarrow> after_in_list (list_replace_list list slot list') p = None"
469  apply(induct list)
470   apply(simp)
471  apply(simp)
472  apply(intro conjI impI)
473   apply(simp)
474   apply(case_tac list, simp)
475    apply(induct list')
476     apply(simp)
477    apply(simp)
478    apply(case_tac list', simp, simp)
479   apply(simp split: if_split_asm)
480    apply(simp add: after_in_list_append_notin_hd)
481   apply(simp add: after_in_list_append_notin_hd)
482  apply(case_tac "list_replace_list list slot list'")
483   apply(simp)
484  apply(simp)
485  apply(case_tac list, simp, simp split: if_split_asm)
486  done
487
488lemma list_replace_after_notin_new:
489  "\<lbrakk>after_in_list list p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot\<rbrakk>
490    \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a"
491  apply(induct list)
492   apply(simp)
493  apply(simp)
494  apply(intro conjI impI)
495   apply(simp add: after_in_list_append_notin_hd)
496   apply(case_tac list, simp, simp)
497  apply(case_tac list, simp, simp split: if_split_asm)
498  apply(insert after_in_list_append_notin_hd)
499  apply(atomize)
500  apply(erule_tac x=p in allE, erule_tac x="[aa]" in allE, erule_tac x="list' @ lista" in allE)
501  apply(simp)
502  done
503
504lemma list_replace_after_None_notin_old:
505  "\<lbrakk>after_in_list list' p = None; p \<in> set list'; p \<notin> set list\<rbrakk>
506    \<Longrightarrow> after_in_list (list_replace_list list slot list') p = after_in_list list slot"
507  apply(induct list)
508   apply(simp)
509  apply(simp)
510  apply(intro conjI impI)
511   apply(simp)
512   apply(case_tac list)
513    apply(simp)
514   apply(simp add: after_in_list_append_last_hd)
515  apply(case_tac "list_replace_list list slot list'")
516   apply(simp)
517   apply(case_tac list, simp, simp)
518  apply(simp)
519  apply(case_tac list, simp, simp)
520  done
521
522lemma list_replace_after_notin_old:
523  "\<lbrakk>after_in_list list' p = Some a; p \<notin> set list; slot \<in> set list\<rbrakk>
524    \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a"
525  apply(induct list)
526   apply(simp)
527  apply(simp)
528  apply(intro conjI impI)
529   apply(simp add: after_in_list_append_in_hd)
530  apply(simp)
531  apply(case_tac "list_replace_list list slot list'")
532   apply(simp)
533  apply(simp)
534  done
535
536
537lemma list_replace_set: "x \<in> set list \<Longrightarrow> set (list_replace list x y) = insert y (set (list) - {x})"
538  apply (induct list)
539  apply (simp add: list_replace_def)+
540  apply (intro impI conjI)
541  apply blast+
542  done
543
544lemma list_swap_both: "x \<in> set list \<Longrightarrow> y \<in> set list \<Longrightarrow> set (list_swap list x y) = set (list)"
545  apply (induct list)
546  apply (simp add: list_swap_def)+
547  apply (intro impI conjI)
548  apply blast+
549  done
550
551lemma list_swap_self[simp]: "list_swap list x x = list"
552  apply (simp add: list_swap_def)
553  done
554
555lemma map_ignore: "x \<notin> set list \<Longrightarrow> (map (\<lambda>xa. if xa = x then y else xa)
556             list) = list"
557  apply (induct list)
558  apply simp+
559  apply blast
560  done
561
562lemma map_ignore2: "y \<notin> set list \<Longrightarrow> (map (\<lambda>xa. if xa = x then y else if xa = y then x else xa)
563             list) = (map (\<lambda>xa. if xa = x then y else xa) list)"
564  apply (simp add: map_ignore)
565  done
566
567lemma map_ignore2': "y \<notin> set list \<Longrightarrow> (map (\<lambda>xa. if xa = y then x else if xa = x then y else xa)
568             list) = (map (\<lambda>xa. if xa = x then y else xa) list)"
569  apply (simp add: map_ignore)
570  apply force
571  done
572
573lemma swap_distinct_helper: "\<lbrakk>x \<in> set list; y \<noteq> x; y \<notin> set list; distinct list\<rbrakk>
574       \<Longrightarrow> distinct (map (\<lambda>xa. if xa = x then y else xa) list)"
575  apply (induct list)
576  apply (simp add: map_ignore | elim conjE | intro impI conjI | blast)+
577  done
578
579lemma swap_distinct: "x \<in> set list \<Longrightarrow> y \<in> set list \<Longrightarrow> distinct list \<Longrightarrow> distinct (list_swap list x y)"
580  apply (induct list)
581  apply (simp add: list_swap_def)+
582  apply (intro impI conjI,simp_all)
583  apply (simp add: map_ignore2 map_ignore2' swap_distinct_helper | elim conjE | force)+
584  done
585
586
587lemma list_swap_none: "x \<notin> set list \<Longrightarrow> y \<notin> set list \<Longrightarrow> list_swap list x y = list"
588  apply (induct list)
589  apply (simp add: list_swap_def)+
590  apply blast
591  done
592
593lemma list_swap_one: "x \<in> set list \<Longrightarrow> y \<notin> set list \<Longrightarrow> set (list_swap list x y) = insert y (set (list)) - {x}"
594  apply (induct list)
595  apply (simp add: list_swap_def)+
596  apply (intro impI conjI)
597  apply blast+
598  done
599
600lemma list_swap_one': "x \<notin> set list \<Longrightarrow> y \<in> set list \<Longrightarrow> set (list_swap list x y) = insert x (set (list)) - {y}"
601  apply (induct list)
602  apply (simp add: list_swap_def)+
603  apply (intro impI conjI)
604  apply blast+
605  done
606
607
608lemma in_swapped_list: "y \<in> set list \<Longrightarrow> x \<in> set (list_swap list x y)"
609  apply (case_tac "x \<in> set list")
610   apply (simp add: list_swap_both)
611  apply (simp add: list_swap_one')
612  apply (intro notI,simp)
613  done
614
615lemma list_swap_empty : "(list_swap list x y = []) = (list = [])"
616  by(simp add: list_swap_def)
617
618lemma distinct_after_in_list_antisym:
619  "distinct list \<Longrightarrow> after_in_list list a = Some b \<Longrightarrow> after_in_list list b \<noteq> Some a"
620  apply (induct list b arbitrary: a rule: after_in_list.induct)
621    apply simp+
622  apply (case_tac xs)
623   apply (clarsimp split: if_split_asm | intro impI conjI)+
624  done
625
626
627lemma after_in_listD: "after_in_list list x = Some y \<Longrightarrow> \<exists>xs ys. list = xs @ (x # y # ys) \<and> x \<notin> set xs"
628  apply (induct list x arbitrary: a rule: after_in_list.induct)
629    apply (simp split: if_split_asm | elim exE | force)+
630  apply (rule_tac x="x # xsa" in exI)
631  apply simp
632  done
633
634lemma list_swap_symmetric: "list_swap list a b = list_swap list b a"
635  apply (simp add: list_swap_def)
636  done
637
638lemma list_swap_preserve_after:
639  "\<lbrakk>desta \<notin> set list; distinct list\<rbrakk>
640\<Longrightarrow> after_in_list (list_swap list srca desta) desta =
641   after_in_list list srca"
642  apply (induct list desta rule: after_in_list.induct)
643  apply (simp add: list_swap_def)+
644  apply force
645  done
646
647lemma list_swap_preserve_after':
648 "\<lbrakk>p \<noteq> desta; p \<noteq> srca; after_in_list list p = Some srca\<rbrakk>
649\<Longrightarrow> after_in_list (list_swap list srca desta) p = Some desta"
650  apply (induct list p rule: after_in_list.induct)
651  apply (simp add: list_swap_def)+
652  apply force
653  done
654
655lemma list_swap_does_swap:
656       "\<lbrakk>distinct list; after_in_list list desta = Some srca\<rbrakk>
657       \<Longrightarrow> after_in_list (list_swap list srca desta) srca = Some desta"
658  apply (induct list srca rule: after_in_list.induct)
659    apply (simp add: list_swap_def)+
660  apply (elim conjE)
661  apply (intro impI conjI,simp_all)
662   apply (frule after_in_list_in_list,simp)+
663  done
664
665lemma list_swap_does_swap':
666  "distinct list \<Longrightarrow> after_in_list list srca = Some desta \<Longrightarrow>
667                after_in_list (list_swap list srca desta) srca =
668          after_in_list list desta"
669  apply (induct list srca rule: after_in_list.induct)
670    apply (simp add: list_swap_def)+
671  apply (elim conjE)
672  apply (intro impI conjI,simp_all)
673   apply (case_tac xs)
674    apply (clarsimp+)[2]
675  apply (case_tac xs)
676   apply clarsimp+
677done
678
679lemmas list_swap_preserve_after'' = list_swap_preserve_after'[simplified list_swap_symmetric]
680
681lemma list_swap_preserve_Some_other:
682 "\<lbrakk>z \<noteq> desta; z \<noteq> srca; after_in_list list srca = Some z\<rbrakk>
683\<Longrightarrow> after_in_list (list_swap list srca desta) desta = Some z"
684  apply (induct list srca rule: after_in_list.induct)
685  apply (simp add: list_swap_def)+
686  apply force
687  done
688
689
690lemmas list_swap_preserve_Some_other' = list_swap_preserve_Some_other[simplified list_swap_symmetric]
691
692lemma list_swap_preserve_None:
693 "\<lbrakk>after_in_list list srca = None\<rbrakk>
694\<Longrightarrow> after_in_list (list_swap list desta srca) desta = None"
695  apply (induct list srca rule: after_in_list.induct)
696  apply (simp add: list_swap_def)+
697  apply force
698  done
699
700lemma list_swap_preserve_None':
701 "\<lbrakk>after_in_list list srca = None\<rbrakk>
702\<Longrightarrow> after_in_list (list_swap list srca desta) desta = None"
703  apply (subst list_swap_symmetric)
704  apply (erule list_swap_preserve_None)
705  done
706
707lemma list_swap_preserve_after_None:
708 "\<lbrakk>p \<noteq> desta; p \<noteq> srca; after_in_list list p = None\<rbrakk>
709\<Longrightarrow> after_in_list (list_swap list srca desta) p = None"
710  apply (induct list p rule: after_in_list.induct)
711  apply (simp add: list_swap_def)+
712  apply force
713  done
714
715lemma list_swap_preserve_Some_other_distinct:
716 "\<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z\<rbrakk>
717\<Longrightarrow> after_in_list (list_swap list srca desta) desta = Some z"
718  apply (rule list_swap_preserve_Some_other)
719  apply simp+
720   apply (rule notI)
721   apply simp
722   apply (frule distinct_after_in_list_not_self[where src=srca])
723   apply simp+
724  done
725
726lemma list_swap_preserve_separate:
727 "\<lbrakk>p \<noteq> desta; p \<noteq> srca; z \<noteq> desta; z \<noteq> srca; after_in_list list p = Some z\<rbrakk>
728\<Longrightarrow> after_in_list (list_swap list srca desta) p = Some z"
729  apply (induct list p rule: after_in_list.induct)
730  apply (simp add: list_swap_def split: if_split_asm)+
731  apply (intro impI conjI)
732   apply simp+
733  done
734
735fun after_in_list_list where
736  "after_in_list_list [] a = []" |
737  "after_in_list_list (x # xs) a = (if a = x then xs else after_in_list_list xs a)"
738
739lemma after_in_list_list_in_list:
740  notes split_paired_All[simp del] split_paired_Ex[simp del]
741  shows "y \<in> set (after_in_list_list list x) \<Longrightarrow> y \<in> set list"
742  apply(induct list arbitrary:x y)
743  apply(simp)
744  apply(case_tac "x=a", simp+)
745done
746
747lemma range_nat_relation_induct:
748"\<lbrakk> m = Suc (n + k) ; m < cap ; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n );
749   \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k \<rbrakk> \<Longrightarrow>  P n m"
750  apply (clarify)
751  apply (thin_tac "m = t" for t)
752  apply (induct k)
753   apply (drule_tac x = "n" in spec)
754   apply (erule impE, simp, simp)
755  apply (frule_tac x = "Suc (n + k)" in spec)
756  apply (erule impE)
757   apply (simp only: add_Suc_right)
758  apply (rotate_tac 3, frule_tac x = n in spec)
759  apply (rotate_tac -1, drule_tac x = "Suc (n + k)" in spec)
760  apply (rotate_tac -1, drule_tac x = "Suc (n + Suc k) " in spec)
761  apply (erule impE)
762   apply (intro conjI)
763     apply (rule_tac y = "Suc (n + Suc k)" in less_trans)
764      apply (rule less_SucI)
765      apply (simp only: add_Suc_right)+
766done
767
768lemma indexed_trancl_as_set_helper : "\<lbrakk>p < q; q < length list; list ! p = a; list ! q = b;
769        q = Suc (p + k); Suc n < length list\<rbrakk>
770       \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p <length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+"
771  apply (induct k arbitrary: p q a b)
772   apply (rule r_into_trancl,simp, rule_tac x = p in exI, simp)
773  apply (atomize)
774  apply (erule_tac x = p in allE, erule_tac x = "Suc (p + k)" in allE, erule_tac x = "a" in allE, erule_tac x = "list ! Suc (p + k)" in allE)
775  apply (elim impE)
776        apply (simp)+
777  apply (rule_tac b = "list ! Suc (p + k)" in trancl_into_trancl)
778   apply (simp)+
779  apply (rule_tac x = "Suc (p + k)" in exI, simp)
780  done
781
782lemma indexed_trancl_as_set: "distinct list \<Longrightarrow> {(i, j). \<exists> p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j }
783      = {(i, j). \<exists> p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j }\<^sup>+"
784  apply (rule equalityI)
785    apply (rule subsetI)
786    apply (case_tac x, simp)
787    apply (elim exE conjE)
788    apply (frule less_imp_Suc_add)
789    apply (erule exE)
790    apply (rule_tac cap = "length list" and m = q and n = p and k = k in range_nat_relation_induct)
791      apply (simp)
792      apply (simp)
793      apply (rule allI, rule impI)
794      apply (rule_tac p = p and q = q and k = k and n = n in indexed_trancl_as_set_helper)
795        apply (simp)+
796  apply (rule subsetI)
797    apply (case_tac x, simp)
798    apply (erule trancl_induct)
799      apply (simp, elim exE conjE)
800      apply (rule_tac x = p in exI, rule_tac x = "Suc p" in exI, simp)
801      apply (simp)
802      apply (rotate_tac 4, erule exE, rule_tac x = p in exI)
803      apply (erule exE, rule_tac x = "Suc pa" in exI)
804      apply (intro conjI)
805        defer
806        apply (simp)
807        apply (erule exE, simp)
808        apply (simp)
809        apply (erule exE)
810        apply (subgoal_tac "pa = q")
811          apply (simp)
812          apply (frule_tac xs = list and i = pa and j = q in nth_eq_iff_index_eq)
813            apply (simp)+
814done
815
816lemma indexed_trancl_irrefl: "distinct list \<Longrightarrow> (x,x) \<notin> {(i, j). \<exists> p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j }\<^sup>+"
817 apply (frule indexed_trancl_as_set [THEN sym])
818 apply (simp)
819 apply (intro allI impI notI)
820 apply (frule_tac xs = list and i = p and j = q in nth_eq_iff_index_eq)
821 apply (simp+)
822done
823
824lemma after_in_list_trancl_indexed_trancl: "distinct list \<Longrightarrow> {(p, q). after_in_list list p = Some q}\<^sup>+ = {(i, j). \<exists> p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j }\<^sup>+"
825  apply (rule_tac f = "\<lambda> x. x\<^sup>+" in  arg_cong)
826  apply (intro equalityI subsetI)
827
828  apply (case_tac x, simp)
829  apply (induct list)
830   apply (simp)
831   apply (case_tac "a = aa")
832     apply (rule_tac x = 0 in exI, case_tac list, simp, simp)
833     apply (case_tac list, simp, simp)
834     apply (atomize, drule_tac x = x in spec, drule_tac x = aa in spec, drule_tac x = b in spec, simp)
835     apply (erule exE, rule_tac x = "Suc p" in exI, simp)
836
837  apply (case_tac x, simp)
838  apply (induct list)
839    apply (simp)
840    apply (case_tac "a = aa")
841      apply (erule exE)
842      apply (subgoal_tac "p = 0")
843        apply (case_tac list, simp, simp)
844        apply (subgoal_tac "distinct (aa # list)")
845          apply (frule_tac i = 0 and j = p and xs = "aa # list" in nth_eq_iff_index_eq)
846          apply (simp, simp, simp, simp)
847    apply (atomize, drule_tac x = x in spec, drule_tac x = aa in spec, drule_tac x = b in spec, simp)
848    apply (drule mp)
849      apply (erule exE)
850      apply (case_tac p, simp, simp)
851      apply (rule_tac x = nat in exI, simp)
852   apply (case_tac list, simp, simp)
853done
854
855lemma distinct_after_in_list_not_self_trancl:
856  notes split_paired_All[simp del] split_paired_Ex[simp del]
857  shows "distinct list \<Longrightarrow> (x, x) \<notin> {(p, q). after_in_list list p = Some q}\<^sup>+"
858  by (simp add: after_in_list_trancl_indexed_trancl indexed_trancl_irrefl)
859
860lemma distinct_after_in_list_in_list_trancl:
861  notes split_paired_All[simp del] split_paired_Ex[simp del]
862  shows "\<lbrakk>distinct list; (x, y) \<in> {(p, q). after_in_list list q = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> set list"
863  by(erule tranclE2, (drule CollectD, simp, drule after_in_list_in_list, simp)+)
864
865
866lemma after_in_list_trancl_prepend:
867  notes split_paired_All[simp del] split_paired_Ex[simp del]
868  shows "\<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+"
869  apply(induct list arbitrary:x y)
870    apply(simp)
871    apply(case_tac "x=a")
872      apply(rule r_into_trancl)
873      apply(simp)
874      apply(drule set_ConsD)
875      apply(elim disjE)
876        apply(simp)
877        apply(atomize)
878        apply(drule_tac x=x in spec)
879        apply(drule_tac x=y in spec)
880        apply(drule_tac mp)
881          apply(simp)
882        apply(drule_tac mp)
883          apply(simp)
884        apply(erule trancl_induct)
885          apply(drule CollectD, simp)
886          apply(rule_tac b = a in trancl_into_trancl2)
887            apply(simp)
888          apply(rule r_into_trancl)
889          apply(rule_tac a = "(a,ya)" in CollectI)
890          apply(clarsimp)
891          apply(case_tac list)
892            apply(simp)
893            apply(simp)
894          apply(case_tac "ya=a")
895            apply(drule CollectD)
896            apply(simp del:after_in_list.simps)
897            apply(drule after_in_list_in_list')
898            apply(simp)
899            apply(rule_tac b=ya in trancl_into_trancl)
900              apply(simp)
901              apply(drule CollectD)
902              apply(rule CollectI)
903              apply(case_tac "ya=y")
904                apply(frule_tac x=y in distinct_after_in_list_not_self_trancl)
905                apply(simp)
906                apply(case_tac list)
907                  apply(simp)
908                  apply(simp)
909done
910
911lemma after_in_list_append_not_hd:
912  notes split_paired_All[simp del] split_paired_Ex[simp del]
913  shows "a \<noteq> x \<Longrightarrow> after_in_list (a # list) x = after_in_list list x"
914by (case_tac list, simp, simp)
915
916lemma trancl_Collect_rev:
917  "(a, b) \<in> {(x, y). P x y}\<^sup>+ \<Longrightarrow> (b, a) \<in> {(x, y). P y x}\<^sup>+"
918  apply(induct rule: trancl_induct)
919   apply(fastforce intro: trancl_into_trancl2)+
920   done
921
922
923lemma prepend_after_in_list_distinct : "distinct (a # list) \<Longrightarrow> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ =
924       {(next, p). after_in_list (list) p = Some next}\<^sup>+ \<union>
925       set list \<times> {a} "
926  apply (rule equalityI)
927   (* \<subseteq> direction *)
928   apply (rule subsetI, case_tac x)
929   apply (simp)
930   apply (erule trancl_induct)
931     (* base case *)
932    apply (drule CollectD, simp)
933    apply (case_tac list, simp)
934    apply (simp split:if_split_asm)
935    apply (rule r_into_trancl)
936    apply (rule CollectI, simp)
937    (* Inductive case *)
938   apply (drule CollectD, simp)
939   apply (erule disjE)
940    apply (case_tac "a \<noteq> z")
941     apply (rule disjI1)
942     apply (rule_tac b =y in trancl_into_trancl)
943      apply (simp, case_tac list, simp, simp)
944
945    apply (simp)
946    apply (rule disjI2)
947    apply (erule conjE)
948    apply (frule_tac x = aa and y = y in distinct_after_in_list_in_list_trancl)
949     apply (simp)
950    apply (simp)
951   apply (subgoal_tac "after_in_list (a # list) z \<noteq> Some a", simp)
952   apply (rule_tac hd_not_after_in_list, simp, simp)
953(* \<supseteq> direction *)
954  apply (rule subsetI)
955  apply (case_tac x)
956  apply (simp)
957  apply (erule disjE)
958    (* transitive case *)
959   apply (erule tranclE2)
960    apply (drule CollectD, simp)
961    apply (subgoal_tac "b \<noteq> a")
962     apply (rule r_into_trancl)
963     apply (rule CollectI, simp)
964     apply (case_tac list, simp, simp)
965    apply (frule after_in_list_in_list')
966    apply (erule conjE)
967    apply (blast)
968   apply (rule_tac y = c in trancl_trans)
969    apply (subgoal_tac "c \<noteq> a")
970     apply (case_tac list, simp, simp)
971     apply (case_tac "aaa = aa")
972      apply (rule r_into_trancl)
973      apply (rule CollectI, simp)
974
975     apply (rule r_into_trancl)
976     apply (rule CollectI, simp)
977    apply (erule CollectE, simp)
978    apply (frule after_in_list_in_list')
979    apply (erule conjE, blast)
980   apply (erule trancl_induct)
981    apply (simp)
982    apply (rule r_into_trancl, simp)
983    apply (subgoal_tac "y \<noteq> a")
984     apply (case_tac list, simp, simp)
985    apply (rotate_tac 3)
986    apply (frule after_in_list_in_list')
987    apply (erule conjE, blast)
988   apply (rule_tac b = y in trancl_into_trancl, simp)
989   apply (rule CollectI, simp)
990   apply (subgoal_tac "a \<noteq> z")
991    apply (case_tac list, simp, simp)
992   apply (rotate_tac 3)
993   apply (frule after_in_list_in_list')
994   apply (blast)
995(* not so transitive case *)
996  apply (subgoal_tac "distinct (a # list)")
997   apply (frule_tac x = aa in after_in_list_trancl_prepend, simp, simp)
998   apply (rule trancl_Collect_rev, simp)
999  apply (simp)
1000done
1001
1002lemma after_in_list_in_cons:
1003  notes split_paired_All[simp del] split_paired_Ex[simp del]
1004  shows "\<lbrakk>after_in_list (x # xs) y = Some z; distinct (x # xs); y \<in> set xs\<rbrakk> \<Longrightarrow> z \<in> set xs"
1005  apply(case_tac "y=x")
1006  apply(simp)
1007  apply(simp add:after_in_list_append_not_hd after_in_list_in_list)
1008done
1009
1010lemma after_in_list_list_set:
1011  notes split_paired_All[simp del] split_paired_Ex[simp del]
1012  shows "distinct list \<Longrightarrow>
1013         set (after_in_list_list list x)
1014         = {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}"
1015  apply(intro equalityI)
1016  (* \<subseteq> *)
1017   apply(induct list arbitrary:x)
1018    apply(simp)
1019   apply(atomize)
1020   apply(simp)
1021   apply(rule conjI, rule impI, rule subsetI)
1022    apply(rule_tac a = xa in CollectI)
1023    apply(rule trancl_Collect_rev)
1024    apply(rule after_in_list_trancl_prepend)
1025     apply(simp)
1026    apply(simp)
1027   apply(clarify)
1028   apply(drule_tac x=x in spec)
1029   apply(drule_tac B="{a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}" in set_rev_mp)
1030    apply(simp)
1031   apply(drule CollectD)
1032   apply(simp add:prepend_after_in_list_distinct)
1033 (* \<supseteq> *)
1034  apply(clarsimp)
1035  apply(drule trancl_Collect_rev)
1036  apply(erule trancl_induct)
1037    (* base *)
1038   apply(simp)
1039   apply(induct list arbitrary:x)
1040    apply(simp)
1041   apply(case_tac "a=x")
1042    apply(frule_tac src=x in distinct_after_in_list_not_self)
1043    apply(simp)
1044    apply(drule after_in_list_in_list)
1045    apply(simp)+
1046   apply(drule_tac list=list in after_in_list_append_not_hd)
1047   apply(simp)
1048   (* inductive *)
1049  apply(simp)
1050  apply(drule trancl_Collect_rev)
1051  apply(induct list arbitrary: x)
1052   apply(simp)
1053  apply(case_tac "a\<noteq>x")
1054  (* a\<noteq>x *)
1055   apply(atomize, drule_tac x=y in spec, drule_tac x=z in spec, drule_tac x=x in spec)
1056   apply(simp add:prepend_after_in_list_distinct)
1057   apply(case_tac "a=y")
1058    apply(simp add:after_in_list_list_in_list)
1059   apply(simp add:after_in_list_append_not_hd)
1060   (* a=x *)
1061  apply(frule after_in_list_in_cons, simp+)
1062done
1063
1064lemma list_eq_after_in_list':
1065  "\<lbrakk> distinct xs; p = xs ! i; i < length xs \<rbrakk>
1066    \<Longrightarrow> \<exists>list. xs = list @ p # after_in_list_list xs p"
1067   apply (induct xs arbitrary: i)
1068     apply (simp)
1069  apply (atomize)
1070  apply (case_tac i)
1071   apply (simp)
1072  apply (drule_tac x = nat in spec, simp)
1073  apply (erule exE, rule impI, rule_tac x = "a # list" in exI)
1074  apply (simp)
1075done
1076
1077lemma after_in_list_last_None:
1078  "distinct list \<Longrightarrow> after_in_list list (last list) = None"
1079  apply(induct list)
1080   apply(simp)
1081  apply(case_tac list)
1082   apply(simp)
1083  apply(fastforce split: if_split_asm)
1084  done
1085
1086lemma after_in_list_None_last:
1087  "\<lbrakk>after_in_list list x = None; x \<in> set list\<rbrakk> \<Longrightarrow> x = last list"
1088  by (induct list x rule: after_in_list.induct,(simp split: if_split_asm)+)
1089
1090end
1091