1 needs "tame/ssreflect/seq2-compiled.hl";;
10 let general_rec_exists_tac g = ((apply_tac o DISCH_ALL o prove_general_recursive_function_exists o snd) g) g;;
11 let ordered = (GEN_ALL o define) `(ordered R [] <=> T) /\
12 (ordered R (h :: t) <=> ordered R t /\ all (R h) t)`;;
13 let sorted = new_definition `sorted R s s0 <=> ordered R s /\ perm_eq s s0`;;
14 let merge = (GEN_ALL o define) `merge R [] s2 = s2 /\ merge R s1 [] = s1 /\
15 merge R (CONS h1 t1) (CONS h2 t2) =
16 if (R h1 h2) then CONS h1 (merge R t1 (CONS h2 t2)) else CONS h2 (merge R (CONS h1 t1) t2)`;;
18 (* Lemma merge_ineqs *)
19 let merge_ineqs = Sections.section_proof ["s"]
20 `~(LENGTH s <= 1) ==> LENGTH (take (LENGTH s DIV 2) s) < LENGTH s /\
21 LENGTH (dropl (LENGTH s DIV 2) s) < LENGTH s`
23 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(2 = 0)`))) (term_tac (have_gen_tac [](move ["n20"])))) ((arith_tac) THEN (done_tac)));
24 ((((use_arg_then2 ("size", [size]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> arg_tac (Arg_term (`sizel s`))) (term_tac (set_tac "n"))));
25 (((((use_arg_then2 ("size_take", [size_take]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_drop", [size_drop]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
28 (* Lemma merge_sort_exists *)
29 let merge_sort_exists = Sections.section_proof []
30 `?f. !R s. f R s = if LENGTH s <= 1 then s else
31 merge R (f R (take (LENGTH s DIV 2) s)) (f R (dropl (LENGTH s DIV 2) s))`
33 (general_rec_exists_tac);
34 ((fun arg_tac -> arg_tac (Arg_term (`MEASURE (LENGTH o SND)`))) (term_tac exists_tac));
35 (((((use_arg_then2 ("WF_MEASURE", [WF_MEASURE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("MEASURE", [MEASURE]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN ((split_tac) THEN (move ["s"]) THEN (move ["ineq"])) THEN (((use_arg_then2 ("merge_ineqs", [merge_ineqs]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
37 let merge_sort = new_specification ["merge_sort"] merge_sort_exists;;
38 let min_k = new_definition `min_k k (l:(real)list) = EL k (merge_sort (<=) l)`;;
41 Sections.begin_section "Merge";;
43 (* Lemma perm_eq_merge *)
44 let perm_eq_merge = Sections.section_proof ["R";"s1";"s2"]
45 `perm_eq (merge R s1 s2) (s1 ++ s2)`
47 (((((use_arg_then2 ("perm_eqP", [perm_eqP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("count_cat", [count_cat]))(thm_tac (new_rewrite [] []))))) THEN (move ["P"]));
48 (((THENL) (((use_arg_then2 ("s2", [])) (disch_tac [])) THEN (clear_assumption "s2") THEN ((use_arg_then2 ("s1", [])) (disch_tac [])) THEN (clear_assumption "s1") THEN elim) [ALL_TAC; ((move ["h1"]) THEN (move ["t1"]) THEN (move ["IH1"]))]) THEN ((THENL) elim [ALL_TAC; ((move ["h2"]) THEN (move ["t2"]) THEN (move ["IH2"]))]) THEN ((((use_arg_then2 ("merge", [merge]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("count", [count]))(thm_tac (new_rewrite [] [])))))) THEN (TRY ((arith_tac))));
49 ((((fun arg_tac -> arg_tac (Arg_term (`R h1 h2`))) (disch_tac [])) THEN case THEN (simp_tac)) THEN ((((use_arg_then2 ("count", [count]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac ->(use_arg_then2 ("IH1", []))(fun tmp_arg1 -> (use_arg_then2 ("IH2", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("count", [count]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
53 let all_merge = Sections.section_proof ["R";"s1";"s2";"P"]
54 `all P (merge R s1 s2) <=> all P s1 /\ all P s2`
56 (((THENL) (((use_arg_then2 ("s2", [])) (disch_tac [])) THEN (clear_assumption "s2") THEN ((use_arg_then2 ("s1", [])) (disch_tac [])) THEN (clear_assumption "s1") THEN elim) [ALL_TAC; ((move ["h1"]) THEN (move ["t1"]) THEN (move ["IH1"]))]) THEN ((THENL) elim [ALL_TAC; ((move ["h2"]) THEN (move ["t2"]) THEN (move ["IH2"]))]) THEN ((((use_arg_then2 ("merge", [merge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
57 ((((fun arg_tac -> arg_tac (Arg_term (`R h1 h2`))) (disch_tac [])) THEN case THEN (simp_tac)) THEN ((((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac ->(use_arg_then2 ("IH1", []))(fun tmp_arg1 -> (use_arg_then2 ("IH2", []))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))))) THEN (REWRITE_TAC[CONJ_ACI]) THEN (done_tac));
60 (* Finalization of the section Merge *)
61 let perm_eq_merge = Sections.finalize_theorem perm_eq_merge;;
62 let all_merge = Sections.finalize_theorem all_merge;;
63 Sections.end_section "Merge";;
66 Sections.begin_section "Ordered";;
67 (Sections.add_section_var (mk_var ("x0", (`:A`))));;
68 (Sections.add_section_var (mk_var ("R", (`:A->A->bool`))));;
71 let ordered1 = Sections.section_proof ["x"]
74 (((repeat_tactic 1 9 (((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
77 (* Lemma ordered_cat *)
78 let ordered_cat = Sections.section_proof ["s1";"s2"]
79 `ordered R (s1 ++ s2) <=>
80 ordered R s1 /\ ordered R s2 /\ all (\x. all (R x) s2) s1`
82 (((THENL) (((use_arg_then2 ("s1", [])) (disch_tac [])) THEN (clear_assumption "s1") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["IH"]))]) THEN ((((use_arg_then2 ("cat", [cat]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then2 ("IH", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("all_cat", [all_cat]))(thm_tac (new_rewrite [] []))))));
83 ((REWRITE_TAC[CONJ_ACI]) THEN (done_tac));
86 (* Lemma ordered_nthP *)
87 let ordered_nthP = Sections.section_proof ["s"]
88 `ordered R s <=> (!i j. i < j /\ j < sizel s ==> R (nth x0 s i) (nth x0 s j))`
90 ((split_tac) THEN ((THENL) (((use_arg_then2 ("s", [])) (disch_tac [])) THEN (clear_assumption "s") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["IH"]))]) THEN ((((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size", [size]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LENGTH", [LENGTH]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ltn0", [ltn0]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size", [size]))(gsym_then (thm_tac (new_rewrite [] [])))))));
91 ((THENL_LAST) ((BETA_TAC THEN (case THEN ((move ["ord"]) THEN (move ["all_t"]))) THEN ((THENL) case [ALL_TAC; (move ["i"])]) THEN ((THENL) case [ALL_TAC; (move ["j"])])) THEN (TRY ((arith_tac))) THEN (((repeat_tactic 1 9 (((use_arg_then2 ("ltSS", [ltSS]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))))) THEN (move ["ineqs"]))) ((((use_arg_then2 ("IH", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
92 ((((use_arg_then2 ("all_t", [])) (disch_tac [])) THEN (clear_assumption "all_t") THEN BETA_TAC) THEN (((fun arg_tac -> (use_arg_then2 ("all_nthP", [all_nthP])) (fun fst_arg -> (use_arg_then2 ("x0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (exact_tac) THEN (done_tac));
93 ((BETA_TAC THEN (move ["cond"])) THEN (split_tac));
94 (((use_arg_then2 ("IH", [])) (disch_tac [])) THEN (clear_assumption "IH") THEN (DISCH_THEN apply_tac) THEN (move ["i"]) THEN (move ["j"]) THEN (move ["ineqs"]));
95 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("cond", [])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SUC i`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SUC j`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("ltSS", [ltSS]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ineqs", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))))) THEN (exact_tac) THEN (done_tac));
96 ((((fun arg_tac -> (use_arg_then2 ("all_nthP", [all_nthP])) (fun fst_arg -> (use_arg_then2 ("x0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (move ["j"]) THEN (move ["j_lt"]));
97 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("cond", [])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`SUC j`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("ltSS", [ltSS]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("gtS0", [gtS0]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("j_lt", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))))) THEN (exact_tac));
100 (* Lemma ordered_nseq *)
101 let ordered_nseq = Sections.section_proof ["n";"x"]
102 `R x x ==> ordered R (nseq n x)`
104 ((BETA_TAC THEN (move ["Rxx"])) THEN (((((use_arg_then2 ("ordered_nthP", [ordered_nthP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size_nseq", [size_nseq]))(thm_tac (new_rewrite [] []))))) THEN (move ["i"]) THEN (move ["j"]) THEN (case THEN (move ["i_lt_j"])) THEN (move ["j_lt"])));
105 ((repeat_tactic 1 9 (((use_arg_then2 ("nth_nseq", [nth_nseq]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("j_lt", []))(thm_tac (new_rewrite [] [])))));
106 ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`i < n:num`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((ALL_TAC) THEN (done_tac)));
107 ((((use_arg_then2 ("i_lt_j", [])) (disch_tac [])) THEN (clear_assumption "i_lt_j") THEN ((use_arg_then2 ("j_lt", [])) (disch_tac [])) THEN (clear_assumption "j_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
110 (* Lemma ordered_subseq *)
111 let ordered_subseq = Sections.section_proof ["s1";"s2"]
112 `subseq s1 s2 /\ ordered R s2 ==> ordered R s1`
114 (((THENL) (((use_arg_then2 ("s2", [])) (disch_tac [])) THEN (clear_assumption "s2") THEN ((use_arg_then2 ("s1", [])) (disch_tac [])) THEN (clear_assumption "s1") THEN elim) [ALL_TAC; ((move ["h1"]) THEN (move ["t1"]) THEN (move ["IH1"]))]) THEN ((THENL) elim [ALL_TAC; ((move ["h2"]) THEN (move ["t2"]) THEN (move ["IH2"]))]) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> arg_tac (Arg_theorem (GEN_ALL subseq)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))));
115 ((THENL_ROT (-1)) ((((fun arg_tac -> arg_tac (Arg_term (`h1 = h2`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (BETA_TAC THEN (case THEN (move ["sub"])) THEN (case THEN ((move ["ord2"]) THEN (move ["all2"]))))));
116 ((((use_arg_then2 ("IH2", [])) (disch_tac [])) THEN (clear_assumption "IH2") THEN BETA_TAC) THEN ((((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("sub", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ord2", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
117 (((((fun arg_tac -> (use_arg_then2 ("IH1", [])) (fun fst_arg -> (use_arg_then2 ("sub", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["x"]) THEN (DISCH_THEN (fun snd_th -> (fun arg_tac -> (use_arg_then2 ("mem_subseq", [mem_subseq])) (fun fst_arg -> (use_arg_then2 ("sub", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (move ["mem_x"]));
118 ((((use_arg_then2 ("all2", [])) (disch_tac [])) THEN (clear_assumption "all2") THEN BETA_TAC) THEN ((((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (exact_tac) THEN (done_tac));
121 (* Lemma ordered_delete_at *)
122 let ordered_delete_at = Sections.section_proof ["i";"s"]
123 `ordered R s ==> ordered R (delete_at i s)`
125 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("ordered_subseq", [ordered_subseq])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (DISCH_THEN apply_tac) THEN (((use_arg_then2 ("subseq_delete_at", [subseq_delete_at])) (disch_tac [])) THEN (clear_assumption "subseq_delete_at") THEN (exact_tac)) THEN (done_tac));
128 (* Lemma ordered_delete1 *)
129 let ordered_delete1 = Sections.section_proof ["x";"s"]
130 `ordered R s ==> ordered R (delete1 x s)`
132 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("ordered_subseq", [ordered_subseq])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (DISCH_THEN apply_tac) THEN (((use_arg_then2 ("subseq_delete1", [subseq_delete1])) (disch_tac [])) THEN (clear_assumption "subseq_delete1") THEN (exact_tac)) THEN (done_tac));
135 (* Lemma ordered_filter *)
136 let ordered_filter = Sections.section_proof ["a";"s"]
137 `ordered R s ==> ordered R (filter a s)`
139 (((DISCH_THEN (fun snd_th -> (use_arg_then2 ("ordered_subseq", [ordered_subseq])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC) THEN (DISCH_THEN apply_tac) THEN (((use_arg_then2 ("filter_subseq", [filter_subseq]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
142 (* Section OrderedMergeGeneral *)
143 Sections.begin_section "OrderedMergeGeneral";;
144 (Sections.add_section_var (mk_var ("S", (`:A -> bool`))));;
145 (Sections.add_section_hyp "R_trans" (`!x y z. x IN S /\ y IN S /\ z IN S ==> R x y /\ R y z ==> R x z`));;
146 (Sections.add_section_hyp "R_total" (`!x y. x IN S /\ y IN S ==> R x y \/ R y x`));;
148 (* Lemma ordered_merge_general *)
149 let ordered_merge_general = Sections.section_proof ["s1";"s2"]
150 `set_of_list s1 SUBSET S /\ set_of_list s2 SUBSET S ==>
151 ordered R s1 /\ ordered R s2 ==> ordered R (merge R s1 s2)`
153 ((repeat_tactic 1 9 (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_SET_OF_LIST", [IN_SET_OF_LIST]))(thm_tac (new_rewrite [] []))))));
154 (((THENL) (((use_arg_then2 ("s2", [])) (disch_tac [])) THEN (clear_assumption "s2") THEN ((use_arg_then2 ("s1", [])) (disch_tac [])) THEN (clear_assumption "s1") THEN elim) [ALL_TAC; ((move ["h1"]) THEN (move ["t1"]) THEN (move ["IH1"]))]) THEN ((THENL) elim [ALL_TAC; ((move ["h2"]) THEN (move ["t2"]) THEN (move ["IH2"]))]) THEN ((((use_arg_then2 ("merge", [merge]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
155 (BETA_TAC THEN (case THEN ((move ["s1S"]) THEN (move ["s2S"]))) THEN (case THEN ((case THEN ((move ["ord1"]) THEN (move ["all1"]))) THEN (case THEN ((move ["ord2"]) THEN (move ["all2"]))))));
156 ((fun arg_tac -> arg_tac (Arg_term (`(!x. x <- t2 ==> x IN S) /\ (!x. x <- t1 ==> x IN S)`))) (term_tac (have_gen_tac [](case THEN ((move ["t2S"]) THEN (move ["t1S"]))))));
157 ((((use_arg_then2 ("s1S", [])) (disch_tac [])) THEN (clear_assumption "s1S") THEN ((use_arg_then2 ("s2S", [])) (disch_tac [])) THEN (clear_assumption "s2S") THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (done_tac));
158 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`h1 IN S /\ h2 IN S`))) (term_tac (have_gen_tac [](move ["hS"])))) ((((fun arg_tac -> (use_arg_then2 ("s2S", [])) (fun fst_arg -> (use_arg_then2 ("h2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((fun arg_tac -> (use_arg_then2 ("s1S", [])) (fun fst_arg -> (use_arg_then2 ("h1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (done_tac)));
159 ((((fun arg_tac -> arg_tac (Arg_term (`R h1 h2`))) (disch_eq_tac "h12" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] [])))));
160 ((((use_arg_then2 ("IH1", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("all_merge", [all_merge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("all1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h12", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))));
161 ((((use_arg_then2 ("all2", [])) (disch_tac [])) THEN (clear_assumption "all2") THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["all2"]) THEN (move ["x"]) THEN (move ["mem_x"])));
162 (((((fun arg_tac -> (use_arg_then2 ("R_trans", [])) (fun fst_arg -> (use_arg_then2 ("h12", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("hS", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("all2", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("t2S", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
163 ((((use_arg_then2 ("IH2", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("all_merge", [all_merge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("all2", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
164 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("R_total", [])) (fun fst_arg -> (use_arg_then2 ("h1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("h2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((repeat_tactic 1 9 (((use_arg_then2 ("hS", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac) THEN (((use_arg_then2 ("h12", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] []))))) THEN (move ["h21"])) THEN ((((use_arg_then2 ("h21", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))));
165 ((((use_arg_then2 ("all1", [])) (disch_tac [])) THEN (clear_assumption "all1") THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["all1"]) THEN (move ["x"]) THEN (move ["mem_x"])));
166 (((((fun arg_tac -> (use_arg_then2 ("R_trans", [])) (fun fst_arg -> (use_arg_then2 ("h21", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("hS", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("all1", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("t1S", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
169 (* Finalization of the section OrderedMergeGeneral *)
170 let ordered_merge_general = Sections.finalize_theorem ordered_merge_general;;
171 Sections.end_section "OrderedMergeGeneral";;
172 (Sections.add_section_hyp "R_asym" (`!x y. R x y /\ R y x ==> x = y`));;
174 (* Lemma ordered_eq *)
175 let ordered_eq = Sections.section_proof ["s1";"s2"]
176 `perm_eq s1 s2 /\ ordered R s1 /\ ordered R s2 ==> s1 = s2`
178 (((THENL) (((use_arg_then2 ("s2", [])) (disch_tac [])) THEN (clear_assumption "s2") THEN ((use_arg_then2 ("s1", [])) (disch_tac [])) THEN (clear_assumption "s1") THEN elim) [ALL_TAC; ((move ["h1"]) THEN (move ["t1"]) THEN (move ["IH1"]))]) THEN ((THENL) elim [ALL_TAC; ((move ["h2"]) THEN (move ["t2"]) THEN (move ["IH2"]))]) THEN ((repeat_tactic 0 10 (((fun arg_tac ->(use_arg_then2 ("perm_eq0l", [perm_eq0l]))(fun tmp_arg1 -> (use_arg_then2 ("perm_eq0r", [perm_eq0r]))(fun tmp_arg2 -> arg_tac (Arg_theorem (CONJ (get_arg_thm tmp_arg1) (get_arg_thm tmp_arg2))))))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("NOT_CONS_NIL", [NOT_CONS_NIL]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
179 ((repeat_tactic 1 9 (((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["p_eq"])) THEN (case THEN (case THEN ((move ["ord1"]) THEN (move ["all1"])))) THEN (case THEN ((move ["ord2"]) THEN (move ["all2"]))));
180 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`h1 = h2`))) (term_tac (have_gen_tac [](move ["eq12"])))));
181 ((in_tac ["p_eq"] true (((use_arg_then2 ("eq12", []))(thm_tac (new_rewrite [] []))))) THEN (congr_tac (`CONS h2 _2`)));
182 ((((use_arg_then2 ("IH1", [])) (disch_tac [])) THEN (clear_assumption "IH1") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("ord1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ord2", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("perm_cons", [perm_cons])) (fun fst_arg -> (use_arg_then2 ("h2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
183 ((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("p_eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["mem_eq"])));
184 ((((fun arg_tac -> (use_arg_then2 ("mem_eq", [])) (fun fst_arg -> (use_arg_then2 ("h2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((fun arg_tac -> (use_arg_then2 ("mem_eq", [])) (fun fst_arg -> (use_arg_then2 ("h1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("MEM", [MEM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
185 ((case THEN (simp_tac) THEN (move ["mem12"])) THEN (case THEN (simp_tac) THEN (move ["mem21"])) THEN (((use_arg_then2 ("R_asym", [])) (disch_tac [])) THEN (clear_assumption "R_asym") THEN (DISCH_THEN apply_tac)));
186 ((((use_arg_then2 ("all2", [])) (disch_tac [])) THEN (clear_assumption "all2") THEN ((use_arg_then2 ("all1", [])) (disch_tac [])) THEN (clear_assumption "all1") THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (use_arg_then2 ("mem21", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)) THEN (move ["R12"]) THEN ((fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (use_arg_then2 ("mem12", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC)) THEN (move ["R21"])) THEN (done_tac));
189 (* Lemma ordered_merge_delete_at_eq *)
190 let ordered_merge_delete_at_eq = Sections.section_proof ["x0";"i";"s"]
191 `i < sizel s /\ ordered R s ==>
192 merge R [nth x0 s i] (delete_at i s) = s`
194 ((BETA_TAC THEN (case THEN ((move ["i_lt"]) THEN (move ["ord"])))) THEN (((use_arg_then2 ("ordered_eq", [ordered_eq])) (disch_tac [])) THEN (clear_assumption "ordered_eq") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("ord", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (split_tac));
195 ((((use_arg_then2 ("perm_eq_trans", [perm_eq_trans])) (disch_tac [])) THEN (clear_assumption "perm_eq_trans") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`nth x0 s i :: delete_at i s`))) (term_tac exists_tac)));
196 (((((use_arg_then2 ("perm_eq_cons_delete_at", [perm_eq_cons_delete_at]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("cat1s", [cat1s])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`nth x0 s i`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`delete_at i s`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_eq_merge", [perm_eq_merge]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
197 (((THENL) (((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN ((use_arg_then2 ("i", [])) (disch_tac [])) THEN (clear_assumption "i") THEN ((use_arg_then2 ("ord", [])) (disch_tac [])) THEN (clear_assumption "ord") THEN ((use_arg_then2 ("s", [])) (disch_tac [])) THEN (clear_assumption "s") THEN elim) [ALL_TAC; ((move ["h"]) THEN (move ["t"]) THEN (move ["IH"]))]) THEN (((((use_arg_then2 ("size", [size]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LENGTH", [LENGTH]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ltn0", [ltn0]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size", [size]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (move ["ord"])) THEN (move ["h_all"])));
198 (((THENL) elim [ALL_TAC; ((move ["i"]) THEN (move ["iIH"]))]) THEN (((((use_arg_then2 ("nth", [nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("delete_at", [delete_at]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("ltSS", [ltSS]))(thm_tac (new_rewrite [] [])))))) THEN (move ["i_lt"])));
199 ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`merge R [h] t = h :: t`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
200 (((THENL) (((use_arg_then2 ("h_all", [])) (disch_tac [])) THEN (clear_assumption "h_all") THEN ((use_arg_then2 ("t", [])) (disch_tac [])) THEN (clear_assumption "t") THEN case) [ALL_TAC; ((move ["h'"]) THEN (move ["t'"]))]) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("merge", [merge]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
201 (repeat_tactic 1 9 (((use_arg_then2 ("merge", [merge]))(thm_tac (new_rewrite [] [])))));
202 ((fun arg_tac -> arg_tac (Arg_term (`nth x0 t i`))) (term_tac (set_tac "x")));
203 ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`R x h`))) (disch_eq_tac "Rxh" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
204 ((((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("IH", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("all_merge", [all_merge]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
205 ((THENL_FIRST) ((((use_arg_then2 ("h_all", [])) (disch_tac [])) THEN (clear_assumption "h_all") THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["h_all"])) THEN (split_tac)) (((((use_arg_then2 ("h_all", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_nth", [mem_nth]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
206 ((BETA_TAC THEN (move ["x'"]) THEN (move ["mem"])) THEN ((((use_arg_then2 ("h_all", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("mem_delete_at", [mem_delete_at])) (fun fst_arg -> (use_arg_then2 ("i", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
207 ((repeat_tactic 1 9 (((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Rxh", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ordered_delete_at", [ordered_delete_at]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))));
208 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`x = h`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))))));
209 ((((use_arg_then2 ("h_all", [])) (disch_tac [])) THEN (clear_assumption "h_all") THEN BETA_TAC) THEN (((((use_arg_then2 ("andbb", [andbb]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (move ["h_all"]) THEN (move ["x'"]) THEN (move ["mem"])) THEN (((use_arg_then2 ("h_all", []))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("mem_delete_at", [mem_delete_at])) (fun fst_arg -> (use_arg_then2 ("i", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac)) THEN (done_tac));
210 ((((use_arg_then2 ("R_asym", [])) (disch_tac [])) THEN (clear_assumption "R_asym") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("Rxh", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))));
211 ((((use_arg_then2 ("h_all", [])) (disch_tac [])) THEN (clear_assumption "h_all") THEN BETA_TAC) THEN ((((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((fun arg_tac -> (conv_thm_tac DISCH_THEN) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac MP_TAC))) THEN (DISCH_THEN apply_tac));
212 (((((use_arg_then2 ("x_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_nth", [mem_nth]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
215 (* Lemma ordered_merge_delete1_eq *)
216 let ordered_merge_delete1_eq = Sections.section_proof ["x";"s"]
217 `x <- s /\ ordered R s ==> merge R [x] (delete1 x s) = s`
219 (BETA_TAC THEN (case THEN ((move ["xs"]) THEN (move ["ord"]))));
220 (((((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`(@)(UNIV)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("delete1_eq_at", [delete1_eq_at]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ordered_merge_delete_at_eq", [ordered_merge_delete_at_eq]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("ord", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
223 (* Finalization of the section Ordered *)
224 let ordered1 = Sections.finalize_theorem ordered1;;
225 let ordered_cat = Sections.finalize_theorem ordered_cat;;
226 let ordered_nthP = Sections.finalize_theorem ordered_nthP;;
227 let ordered_nseq = Sections.finalize_theorem ordered_nseq;;
228 let ordered_subseq = Sections.finalize_theorem ordered_subseq;;
229 let ordered_delete_at = Sections.finalize_theorem ordered_delete_at;;
230 let ordered_delete1 = Sections.finalize_theorem ordered_delete1;;
231 let ordered_filter = Sections.finalize_theorem ordered_filter;;
232 let ordered_merge_general = Sections.finalize_theorem ordered_merge_general;;
233 let ordered_eq = Sections.finalize_theorem ordered_eq;;
234 let ordered_merge_delete_at_eq = Sections.finalize_theorem ordered_merge_delete_at_eq;;
235 let ordered_merge_delete1_eq = Sections.finalize_theorem ordered_merge_delete1_eq;;
236 Sections.end_section "Ordered";;
239 Sections.begin_section "Sorted";;
240 (Sections.add_section_var (mk_var ("R", (`:A->A->bool`))));;
241 (Sections.add_section_var (mk_var ("x0", (`:A`))));;
243 (* Lemma sorted_size *)
244 let sorted_size = Sections.section_proof ["s1";"s2"]
245 `sorted R s1 s2 ==> sizel s1 = sizel s2`
247 (((((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["_"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("perm_eq_size", [perm_eq_size])) (thm_tac (match_mp_then snd_th MP_TAC))))))) THEN (done_tac));
250 (* Lemma sorted_mem *)
251 let sorted_mem = Sections.section_proof ["s1";"s2"]
252 `sorted R s1 s2 ==> (!x. x <- s1 <=> x <- s2)`
254 (((((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["_"]) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (thm_tac (match_mp_then snd_th MP_TAC))))))) THEN (done_tac));
257 (* Lemma size_merge *)
258 let size_merge = Sections.section_proof ["s1";"s2"]
259 `sizel (merge R s1 s2) = sizel s1 + sizel s2`
261 ((((use_arg_then2 ("size_cat", [size_cat]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((use_arg_then2 ("perm_eq_size", [perm_eq_size])) (thm_tac apply_tac)) THEN ((use_arg_then2 ("perm_eq_merge", [perm_eq_merge])) (thm_tac apply_tac)) THEN (done_tac));
264 (* Lemma sorted_delete_at_1 *)
265 let sorted_delete_at_1 = Sections.section_proof ["i";"s1";"s2"]
266 `i < sizel s1 /\ sorted R s1 s2 ==>
267 sorted R (delete_at i s1) (delete1 (nth x0 s1 i) s2)`
269 (((repeat_tactic 1 9 (((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["i_lt"])) THEN (case THEN ((move ["ord"]) THEN (move ["p_eq"])))) THEN ((((use_arg_then2 ("ordered_delete_at", [ordered_delete_at]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("perm_eq_delete_at_1", [perm_eq_delete_at_1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
272 (* Lemma sorted_delete_1_at *)
273 let sorted_delete_1_at = Sections.section_proof ["i";"s1";"s2"]
274 `i < sizel s2 /\ sorted R s1 s2 ==>
275 sorted R (delete1 (nth x0 s2 i) s1) (delete_at i s2)`
277 ((repeat_tactic 1 9 (((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["i_lt"])) THEN (case THEN ((move ["ord"]) THEN (move ["p_eq"]))));
278 (((((use_arg_then2 ("ordered_delete1", [ordered_delete1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_eq_delete_at_1", [perm_eq_delete_at_1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
281 (* Lemma sorted_delete1 *)
282 let sorted_delete1 = Sections.section_proof ["x";"s1";"s2"]
283 `sorted R s1 s2 ==> sorted R (delete1 x s1) (delete1 x s2)`
285 (((repeat_tactic 1 9 (((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["ord"]) THEN (move ["p_eq"])))) THEN ((((use_arg_then2 ("ordered_delete1", [ordered_delete1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("perm_eq_delete1", [perm_eq_delete1]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
288 (* Lemma sorted_filter *)
289 let sorted_filter = Sections.section_proof ["a";"s";"l"]
290 `sorted R s l ==> sorted R (filter a s) (filter a l)`
292 ((repeat_tactic 1 9 (((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["ord_s"]) THEN (move ["perm_s"]))));
293 (((((fun arg_tac -> (use_arg_then2 ("ordered_subseq", [ordered_subseq])) (fun fst_arg -> (use_arg_then2 ("ord_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("filter_subseq", [filter_subseq]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("perm_eq_filter", [perm_eq_filter]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
296 (* Lemma perm_eq_merge_sort *)
297 let perm_eq_merge_sort = Sections.section_proof ["s"]
298 `perm_eq (merge_sort R s) s`
300 (((use_arg_then2 ("s", [])) (disch_tac [])) THEN (clear_assumption "s") THEN ((use_arg_then2 ("seq_wf_ind", [seq_wf_ind])) (thm_tac apply_tac)) THEN (move ["s"]) THEN (move ["IH"]));
301 ((((use_arg_then2 ("merge_sort", [merge_sort]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_term (`LENGTH s <= 1`))) (disch_eq_tac "ineq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) THEN (repeat_tactic 0 10 (((use_arg_then2 ("perm_eq_refl", [perm_eq_refl]))(thm_tac (new_rewrite [] []))))));
302 ((fun arg_tac -> arg_tac (Arg_term (`_ DIV 2`))) (term_tac (set_tac "n")));
303 ((((fun arg_tac -> (use_arg_then2 ("perm_eq_trans", [perm_eq_trans])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`merge_sort R (take n s) ++ merge_sort R (dropl n s)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN (split_tac));
304 ((((use_arg_then2 ("perm_eq_merge", [perm_eq_merge]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
305 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("cat_take_drop", [cat_take_drop])) (fun fst_arg -> (use_arg_then2 ("n", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [3] []))))) THEN ((use_arg_then2 ("perm_eq_cat", [perm_eq_cat])) (thm_tac apply_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("IH", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("n_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("merge_ineqs", [merge_ineqs]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
308 (* Lemma size_merge_sort *)
309 let size_merge_sort = Sections.section_proof ["l"]
310 `sizel (merge_sort R l) = sizel l`
312 (((use_arg_then2 ("perm_eq_size", [perm_eq_size])) (thm_tac apply_tac)) THEN (((use_arg_then2 ("perm_eq_merge_sort", [perm_eq_merge_sort]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
315 (* Section SortedEq *)
316 Sections.begin_section "SortedEq";;
317 (Sections.add_section_hyp "R_asym" (`!x y. R x y /\ R y x ==> x = y`));;
319 (* Lemma sorted_eq *)
320 let sorted_eq = Sections.section_proof ["s1";"s2";"s"]
321 `sorted R s1 s /\ sorted R s2 s ==> s1 = s2`
323 ((repeat_tactic 1 9 (((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((case THEN ((move ["ord1"]) THEN (move ["p1"]))) THEN (case THEN ((move ["ord2"]) THEN (move ["p2"]))))));
324 ((((fun arg_tac -> (use_arg_then2 ("ordered_eq", [ordered_eq])) (fun fst_arg -> (use_arg_then2 ("R_asym", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("ord1", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ord2", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_trans", [perm_eq_trans])) (fun fst_arg -> (use_arg_then2 ("p1", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
327 (* Finalization of the section SortedEq *)
328 let sorted_eq = Sections.finalize_theorem sorted_eq;;
329 Sections.end_section "SortedEq";;
331 (* Section SortedNth0 *)
332 Sections.begin_section "SortedNth0";;
334 (* Lemma nth0_sorted_imp *)
335 let nth0_sorted_imp = Sections.section_proof ["l";"s"]
336 `sorted R s l ==> (!y. y <- l /\ ~(y = nth x0 s 0) ==> R (nth x0 s 0) y)`
338 (((((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("ordered_nthP", [ordered_nthP])) (fun fst_arg -> (use_arg_then2 ("x0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["sort"]) THEN (move ["perm"]))) THEN (move ["y"]));
339 ((((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["ys"]) THEN (move ["y_neq"]))));
340 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (use_arg_then2 ("x0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ys", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("sort", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ys", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))));
341 ((((use_arg_then2 ("y_neq", [])) (disch_tac [])) THEN (clear_assumption "y_neq") THEN ((use_arg_then2 ("contraR", [contraR])) (disch_tac [])) THEN (clear_assumption "contraR") THEN (DISCH_THEN apply_tac)) THEN (((((use_arg_then2 ("lt0n", [lt0n]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))) THEN (move ["eq0"])));
342 (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (use_arg_then2 ("x0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ys", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq0", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
344 (Sections.add_section_hyp "R_anti" (`!x y. R x y /\ R y x ==> x = y`));;
346 (* Lemma nth0_sorted_eq *)
347 let nth0_sorted_eq = Sections.section_proof ["x";"l";"s"]
348 `sorted R s l /\ 0 < sizel l ==>
349 (nth x0 s 0 = x <=> (x <- l /\ !y. y <- l /\ ~(y = x) ==> R x y))`
351 ((BETA_TAC THEN (case THEN ((move ["sort"]) THEN (move ["size_gt0"])))) THEN (((use_arg_then2 ("sort", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN ((move ["ord"]) THEN (move ["perm"])))));
352 ((THENL) (split_tac) [(((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] []))))); (case THEN ((move ["mem_x"]) THEN (move ["r_xy"])))]);
353 ((((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_nth", [mem_nth]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("perm_eq_size", [perm_eq_size])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
354 (((use_arg_then2 ("nth0_sorted_imp", [nth0_sorted_imp])) (disch_tac [])) THEN (clear_assumption "nth0_sorted_imp") THEN (exact_tac));
355 ((((use_arg_then2 ("contraT", [contraT])) (disch_tac [])) THEN (clear_assumption "contraT") THEN (DISCH_THEN apply_tac) THEN (move ["neq"])) THEN (((use_arg_then2 ("neq", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("implybF", [implybF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))));
356 ((((use_arg_then2 ("R_anti", [])) (disch_tac [])) THEN (clear_assumption "R_anti") THEN (DISCH_THEN apply_tac)) THEN ((((use_arg_then2 ("r_xy", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("neq", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("mem_nth", [mem_nth]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((fun arg_tac -> (use_arg_then2 ("perm_eq_size", [perm_eq_size])) (fun fst_arg -> (use_arg_then2 ("perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
357 ((((fun arg_tac -> (use_arg_then2 ("nth0_sorted_imp", [nth0_sorted_imp])) (fun fst_arg -> (use_arg_then2 ("sort", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
360 (* Finalization of the section SortedNth0 *)
361 let nth0_sorted_imp = Sections.finalize_theorem nth0_sorted_imp;;
362 let nth0_sorted_eq = Sections.finalize_theorem nth0_sorted_eq;;
363 Sections.end_section "SortedNth0";;
364 (Sections.add_section_hyp "R_trans" (`!x y z. R x y /\ R y z ==> R x z`));;
366 (* Lemma sorted_le *)
367 let sorted_le = Sections.section_proof ["l";"l'";"s";"s'"]
368 `sorted R s l /\ sorted R s' l' /\ sizel l' = sizel l /\
369 (!i. i < sizel l ==> R (nth x0 l i) (nth x0 l' i)) ==>
370 (!i. i < sizel l ==> R (nth x0 s i) (nth x0 s' i))`
372 ((BETA_TAC THEN (case THEN (move ["sort_s"])) THEN (case THEN (move ["sort_s'"])) THEN (case THEN (move ["l_l'"])) THEN (move ["ineqs"]) THEN (move ["i"]) THEN (move ["i_lt"])) THEN (((use_arg_then2 ("sort_s'", [])) (disch_tac [])) THEN ((use_arg_then2 ("sort_s", [])) (disch_tac [])) THEN BETA_TAC));
373 ((fun arg_tac -> arg_tac (Arg_term (`sizel l`))) (term_tac (set_tac "n")));
374 ((repeat_tactic 1 9 (((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["ord_s"]) THEN (move ["perm_s"]))) THEN (case THEN ((move ["ord_s'"]) THEN (move ["perm_s'"]))));
375 ((fun arg_tac -> arg_tac (Arg_term (`sizel s = n /\ sizel s' = n`))) (term_tac (have_gen_tac [](move ["sizes"]))));
376 (((((fun arg_tac -> (use_arg_then2 ("perm_eq_size", [perm_eq_size])) (fun fst_arg -> (use_arg_then2 ("perm_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_size", [perm_eq_size])) (fun fst_arg -> (use_arg_then2 ("perm_s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
377 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`?t. t HAS_SIZE (n - i) /\ (!k. k IN t ==> k < n /\ R (nth x0 s i) (nth x0 s' k))`))) (term_tac (have_gen_tac []ALL_TAC))));
378 ((((use_arg_then2 ("HAS_SIZE", [HAS_SIZE]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["t"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["fin_t"])) THEN (move ["card_t"]) THEN (move ["R_in_t"]));
379 ((THENL) (((fun arg_tac -> (use_arg_then2 ("EXCLUDED_MIDDLE", [EXCLUDED_MIDDLE])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`?k. k IN t /\ k < i:num`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case) [((case THEN (move ["k"])) THEN (case THEN ((move ["kt"]) THEN (move ["k_lt"])))); ALL_TAC]);
380 ((((use_arg_then2 ("R_trans", [])) (disch_tac [])) THEN (clear_assumption "R_trans") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`nth x0 s' k`))) (term_tac exists_tac)));
381 (((((use_arg_then2 ("R_in_t", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (in_tac ["ord_s'"] false (((fun arg_tac -> (use_arg_then2 ("ordered_nthP", [ordered_nthP])) (fun fst_arg -> (use_arg_then2 ("x0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("ord_s'", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
382 (((((use_arg_then2 ("NOT_EXISTS_THM", [NOT_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"]));
383 ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`t = i..n - 1`))) (term_tac (have_gen_tac [](move ["t_eq"]))))) (((((use_arg_then2 ("R_in_t", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("t_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_NUMSEG", [IN_NUMSEG]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
384 (((use_arg_then2 ("CARD_SUBSET_EQ", [CARD_SUBSET_EQ])) (thm_tac apply_tac)) THEN ((((use_arg_then2 ("CARD_NUMSEG", [CARD_NUMSEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card_t", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FINITE_NUMSEG", [FINITE_NUMSEG]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("SUBSET", [SUBSET]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_NUMSEG", [IN_NUMSEG]))(thm_tac (new_rewrite [] []))))));
385 ((THENL_LAST) (split_tac) ((((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
386 ((BETA_TAC THEN (move ["k"]) THEN (move ["kt"])) THEN (((fun arg_tac -> (use_arg_then2 ("R_in_t", [])) (fun fst_arg -> (use_arg_then2 ("kt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("k", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then2 ("kt", []))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
387 (in_tac ["perm_s"] false (((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] [])))));
388 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("perm_eq_bij", [perm_eq_bij])) (fun fst_arg -> (use_arg_then2 ("perm_s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("perm_eq_bij", [perm_eq_bij])) (fun fst_arg -> (use_arg_then2 ("perm_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("n_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("sizes", []))(thm_tac (new_rewrite [] []))))));
389 (BETA_TAC THEN (case THEN (move ["p"])) THEN (case THEN (move ["p_perm"])) THEN (move ["p_eq"]) THEN (case THEN (move ["q"])) THEN (case THEN (move ["q_perm"])) THEN (move ["q_eq"]));
390 ((fun arg_tac -> arg_tac (Arg_term (`j < n:num ==> p j < n`))) (term_tac (have_gen_tac ["j"](move ["p_lt"]))));
391 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PERMUTES_IN_IMAGE", [PERMUTES_IN_IMAGE])) (fun fst_arg -> (use_arg_then2 ("p_perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("j", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("IN_NUMSEG", [IN_NUMSEG]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq0n", [leq0n]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
392 ((fun arg_tac -> arg_tac (Arg_term (`j < n:num ==> q j < n`))) (term_tac (have_gen_tac ["j"](move ["q_lt"]))));
393 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PERMUTES_IN_IMAGE", [PERMUTES_IN_IMAGE])) (fun fst_arg -> (use_arg_then2 ("q_perm", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("j", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("IN_NUMSEG", [IN_NUMSEG]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("leq0n", [leq0n]))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
394 (((fun arg_tac -> arg_tac (Arg_term (`IMAGE (q o p) (i..n - 1)`))) (term_tac exists_tac)) THEN (split_tac));
395 ((((use_arg_then2 ("HAS_SIZE", [HAS_SIZE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FINITE_IMAGE", [FINITE_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("FINITE_NUMSEG", [FINITE_NUMSEG]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
396 ((THENL_LAST) ((((use_arg_then2 ("CARD_IMAGE_INJ", [CARD_IMAGE_INJ]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("CARD_NUMSEG", [CARD_NUMSEG]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("FINITE_NUMSEG", [FINITE_NUMSEG]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))))) ((((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
397 (BETA_TAC THEN (move ["x"]) THEN (move ["y"]) THEN (case THEN (move ["_"])) THEN (case THEN (move ["_"])));
398 (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("PERMUTES_INJECTIVE", [PERMUTES_INJECTIVE])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`q o p`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`0..n-1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("PERMUTES_COMPOSE", [PERMUTES_COMPOSE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
399 (((((use_arg_then2 ("IN_IMAGE", [IN_IMAGE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("IN_NUMSEG", [IN_NUMSEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("o_THM", [o_THM]))(thm_tac (new_rewrite [] []))))) THEN (move ["k"]) THEN (case THEN (move ["j"])) THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (move ["j_ineqs"]));
400 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`j < n:num`))) (term_tac (have_gen_tac [](move ["j_lt"])))) ((((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN ((use_arg_then2 ("j_ineqs", [])) (disch_tac [])) THEN (clear_assumption "j_ineqs") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
401 ((((use_arg_then2 ("q_lt", []))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("p_lt", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("q_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("p_lt", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))));
402 ((((fun arg_tac -> (use_arg_then2 ("ineqs", [])) (fun fst_arg -> (fun arg_tac -> (use_arg_then2 ("p_lt", [])) (fun fst_arg -> (use_arg_then2 ("j_lt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("p_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["Rj"])));
403 ((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`i = j`))) (disch_eq_tac "eq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)) ((((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
404 ((((use_arg_then2 ("R_trans", [])) (disch_tac [])) THEN (clear_assumption "R_trans") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`nth x0 s j`))) (term_tac exists_tac)) THEN ((((use_arg_then2 ("Rj", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] []))))));
405 (in_tac ["ord_s"] false (((fun arg_tac -> (use_arg_then2 ("ordered_nthP", [ordered_nthP])) (fun fst_arg -> (use_arg_then2 ("x0", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))));
406 (((((use_arg_then2 ("ord_s", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("sizes", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("j_lt", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LT_LE", [LT_LE]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
408 (Sections.add_section_hyp "R_total" (`!x y. R x y \/ R y x`));;
410 (* Lemma ordered_merge *)
411 let ordered_merge = Sections.section_proof ["s1";"s2"]
412 `ordered R s1 /\ ordered R s2 ==> ordered R (merge R s1 s2)`
414 ((BETA_TAC THEN (case THEN ((move ["ord1"]) THEN (move ["ord2"])))) THEN ((((fun arg_tac -> (use_arg_then2 ("ordered_merge_general", [ordered_merge_general])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`UNIV`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_UNIV", [IN_UNIV]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("SUBSET_UNIV", [SUBSET_UNIV]))(thm_tac (new_rewrite [] [])))))) THEN (done_tac));
417 (* Lemma ordered_merge_sort *)
418 let ordered_merge_sort = Sections.section_proof ["s"]
419 `ordered R (merge_sort R s)`
421 ((((use_arg_then2 ("s", [])) (disch_tac [])) THEN (clear_assumption "s") THEN ((use_arg_then2 ("seq_wf_ind", [seq_wf_ind])) (thm_tac apply_tac)) THEN (move ["s"]) THEN (move ["IH"])) THEN (((use_arg_then2 ("merge_sort", [merge_sort]))(thm_tac (new_rewrite [] [])))));
422 (((fun arg_tac -> arg_tac (Arg_term (`LENGTH s <= 1`))) (disch_eq_tac "ineq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
423 ((((fun arg_tac -> (use_arg_then2 ("length_le_1", [length_le_1])) (fun fst_arg -> (use_arg_then2 ("ineq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("ordered", [ordered]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("all", [all]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
424 ((((use_arg_then2 ("ordered_merge", [ordered_merge])) (disch_tac [])) THEN (clear_assumption "ordered_merge") THEN (DISCH_THEN apply_tac)) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("IH", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("merge_ineqs", [merge_ineqs]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
427 (* Lemma sorted_merge_sort *)
428 let sorted_merge_sort = Sections.section_proof ["s"]
429 `sorted R (merge_sort R s) s`
431 (((((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ordered_merge_sort", [ordered_merge_sort]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_eq_merge_sort", [perm_eq_merge_sort]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
434 (* Finalization of the section Sorted *)
435 let sorted_size = Sections.finalize_theorem sorted_size;;
436 let sorted_mem = Sections.finalize_theorem sorted_mem;;
437 let size_merge = Sections.finalize_theorem size_merge;;
438 let sorted_delete_at_1 = Sections.finalize_theorem sorted_delete_at_1;;
439 let sorted_delete_1_at = Sections.finalize_theorem sorted_delete_1_at;;
440 let sorted_delete1 = Sections.finalize_theorem sorted_delete1;;
441 let sorted_filter = Sections.finalize_theorem sorted_filter;;
442 let perm_eq_merge_sort = Sections.finalize_theorem perm_eq_merge_sort;;
443 let size_merge_sort = Sections.finalize_theorem size_merge_sort;;
444 let sorted_eq = Sections.finalize_theorem sorted_eq;;
445 let nth0_sorted_imp = Sections.finalize_theorem nth0_sorted_imp;;
446 let nth0_sorted_eq = Sections.finalize_theorem nth0_sorted_eq;;
447 let sorted_le = Sections.finalize_theorem sorted_le;;
448 let ordered_merge = Sections.finalize_theorem ordered_merge;;
449 let ordered_merge_sort = Sections.finalize_theorem ordered_merge_sort;;
450 let sorted_merge_sort = Sections.finalize_theorem sorted_merge_sort;;
451 Sections.end_section "Sorted";;
453 (* Section SortedReal *)
454 Sections.begin_section "SortedReal";;
457 (* Lemma ordered_real_nseq *)
458 let ordered_real_nseq = Sections.section_proof ["n";"x"]
459 `ordered (<=) (nseq n x)`
461 (((((use_arg_then2 ("ordered_nseq", [ordered_nseq]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_REFL", [REAL_LE_REFL]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
464 (* Lemma ordered_cat_filter *)
465 let ordered_cat_filter = Sections.section_proof ["s";"v"]
467 s = filter (\x. x <= v) s ++ filter (predC (\x. x <= v)) s`
469 ((BETA_TAC THEN (move ["ord_s"])) THEN ((fun arg_tac -> arg_tac (Arg_term (`_1 ++ _2`))) (term_tac (set_tac "s2"))));
470 ((THENL_FIRST) (((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("ordered_eq", [ordered_eq])) (fun fst_arg -> (use_arg_then2 ("ord_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("s2", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (split_tac)) ((BETA_TAC THEN (move ["x"]) THEN (move ["y"])) THEN (((use_arg_then2 ("REAL_LE_ANTISYM", [REAL_LE_ANTISYM]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
471 ((((use_arg_then2 ("s2_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("perm_eq_sym", [perm_eq_sym]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_filterC", [perm_filterC]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("perm_eq_refl", [perm_eq_refl]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ordered_cat", [ordered_cat]))(thm_tac (new_rewrite [] [])))));
472 (((repeat_tactic 1 9 (((use_arg_then2 ("ordered_filter", [ordered_filter]))(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("allP", [allP]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then2 ("mem_filter", [mem_filter]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("predC", [predC]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["x"]) THEN (case THEN ((move ["x_le"]) THEN (move ["mem_x"]))) THEN (move ["y"]) THEN (case THEN ((move ["y_gt"]) THEN (move ["mem_y"]))));
473 ((((use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE])) (disch_tac [])) THEN (clear_assumption "REAL_LT_IMP_LE") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("REAL_LET_TRANS", [REAL_LET_TRANS])) (disch_tac [])) THEN (clear_assumption "REAL_LET_TRANS") THEN (DISCH_THEN apply_tac)) THEN ((use_arg_then2 ("v", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("REAL_NOT_LE", [REAL_NOT_LE]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac));
476 (* Lemma real_merge_sort *)
477 let real_merge_sort = Sections.section_proof ["s"]
478 `sorted (<=) (merge_sort (<=) s) s`
480 (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sorted_merge_sort", [sorted_merge_sort])) (fun fst_arg -> (use_arg_then2 ("REAL_LE_TRANS", [REAL_LE_TRANS])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("REAL_LE_TOTAL", [REAL_LE_TOTAL])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (exact_tac));
484 let ants = Sections.section_proof ["P";"Q";"R"]
485 `P /\ (Q ==> R) ==> ((P ==> Q) ==> R)`
487 ((BETA_TAC THEN (case THEN ((move ["p"]) THEN (move ["qr"]))) THEN (move ["pq"])) THEN ((((use_arg_then2 ("qr", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("pq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
490 (* Lemma sort_continuous *)
491 let sort_continuous = Sections.section_proof ["l";"l'";"s";"s'";"e"]
492 `sorted (<=) s l /\ sorted (<=) s' l' /\ sizel l = sizel l' /\
493 (!i. i < sizel l ==> abs (nth (&0) l i - nth (&0) l' i) < e) ==>
494 (!i. i < sizel l ==> abs (nth (&0) s i - nth (&0) s' i) < e)`
496 (((use_arg_then2 ("l'", [])) (disch_tac [])) THEN (clear_assumption "l'") THEN ((use_arg_then2 ("s'", [])) (disch_tac [])) THEN (clear_assumption "s'") THEN ((use_arg_then2 ("s", [])) (disch_tac [])) THEN (clear_assumption "s") THEN ((use_arg_then2 ("l", [])) (disch_tac [])) THEN (clear_assumption "l") THEN ((use_arg_then2 ("seq_wf_ind", [seq_wf_ind])) (thm_tac apply_tac)) THEN (move ["l"]) THEN (move ["IH"]) THEN (move ["s"]) THEN (move ["s'"]) THEN (move ["l'"]) THEN (case THEN (move ["sort_s"])) THEN (case THEN (move ["sort_s'"])) THEN (case THEN (move ["l_l'"])) THEN (move ["ineqs"]) THEN (move ["i"]) THEN (move ["i_ineq"]));
497 ((fun arg_tac -> arg_tac (Arg_term (`sizel s = sizel l /\ sizel s' = sizel l`))) (term_tac (have_gen_tac [](move ["h_size"]))));
498 (((((fun arg_tac -> (use_arg_then2 ("sorted_size", [sorted_size])) (fun fst_arg -> (use_arg_then2 ("sort_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("sorted_size", [sorted_size])) (fun fst_arg -> (use_arg_then2 ("sort_s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("l_l'", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (done_tac));
499 ((fun arg_tac -> arg_tac (Arg_term (`nth (&0) s i`))) (term_tac (set_tac "x")));
500 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`x <- s`))) (term_tac (have_gen_tac [](move ["xs"])))) (((((use_arg_then2 ("x_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_nth", [mem_nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("h_size", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
501 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`x <- l`))) (term_tac (have_gen_tac [](move ["xl"])))) ((((fun arg_tac -> (use_arg_then2 ("sorted_mem", [sorted_mem])) (fun fst_arg -> (use_arg_then2 ("sort_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)));
502 ((fun arg_tac -> arg_tac (Arg_term (`nth (&0) l' (indexl x l)`))) (term_tac (set_tac "x'")));
503 ((fun arg_tac -> arg_tac (Arg_term (`abs (x - x') < e`))) (term_tac (have_gen_tac [](move ["x_ineq"]))));
504 (((((use_arg_then2 ("x'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("l", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("ineqs", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
505 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`x' <- l'`))) (term_tac (have_gen_tac [](move ["x'_l'"])))) (((((use_arg_then2 ("x'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("mem_nth", [mem_nth]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("l_l'", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)));
506 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`x' <- s'`))) (term_tac (have_gen_tac [](move ["x'_s'"])))) ((((fun arg_tac -> (use_arg_then2 ("sorted_mem", [sorted_mem])) (fun fst_arg -> (use_arg_then2 ("sort_s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
507 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("IH", [])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`delete1 x l`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`delete_at i s`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`delete1 x' s'`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`delete_at (indexl x l) l'`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((use_arg_then2 ("IH", [])) (disch_tac [])) THEN (clear_assumption "IH") THEN BETA_TAC THEN (move ["_"]));
508 ((THENL_FIRST) (((((use_arg_then2 ("size", [size]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_delete1", [size_delete1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("xl", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("COND_CLAUSES", [COND_CLAUSES]))(thm_tac (new_rewrite [] []))))) THEN (ANTS_TAC)) ((((use_arg_then2 ("i_ineq", [])) (disch_tac [])) THEN (clear_assumption "i_ineq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
509 ((((use_arg_then2 ("ants", [ants])) (disch_tac [])) THEN (clear_assumption "ants") THEN (DISCH_THEN apply_tac)) THEN ((THENL) (split_tac) [ALL_TAC; (move ["IH"])]));
510 ((((use_arg_then2 ("x_def", []))(gsym_then (thm_tac (new_rewrite [1] []))))) THEN (((use_arg_then2 ("sorted_delete_at_1", [sorted_delete_at_1]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("h_size", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
511 ((((use_arg_then2 ("x'_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("sorted_delete_1_at", [sorted_delete_1_at]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("l_l'", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
512 (((((use_arg_then2 ("size_delete_at", [size_delete_at]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("l_l'", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("xl", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (move ["k"]) THEN (move ["k_lt"]));
513 (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("size_delete_at", [size_delete_at])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`indexl x l`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("l'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("size_delete1", [size_delete1])) (fun fst_arg -> (use_arg_then2 ("x", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("l", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
514 (((((use_arg_then2 ("l_l'", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("xl", []))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["size1"]) THEN (move ["size2"]));
515 (((((use_arg_then2 ("nth_delete1", [nth_delete1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_delete_at", [nth_delete_at]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ineqs", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("k_lt", [])) (disch_tac [])) THEN (clear_assumption "k_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
516 ((fun arg_tac -> arg_tac (Arg_term (`nth _1 _2 _3`))) (term_tac (set_tac "y")));
517 (((fun arg_tac -> arg_tac (Arg_term (`i <= indexl x' s'`))) (disch_eq_tac "i_le" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac));
518 ((((use_arg_then2 ("i_le", [])) (disch_tac [])) THEN (clear_assumption "i_le") THEN BETA_TAC) THEN (((use_arg_then2 ("leq_eqVlt", [leq_eqVlt]))(thm_tac (new_rewrite [] [])))) THEN ((THENL) case [(move ["eq"]); (move ["i_lt"])]));
519 (((((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_index", [nth_index]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
520 ((fun arg_tac -> arg_tac (Arg_term (`y <= x'`))) (term_tac (have_gen_tac []ALL_TAC)));
521 ((((use_arg_then2 ("sort_s'", [])) (disch_tac [])) THEN (clear_assumption "sort_s'") THEN BETA_TAC) THEN (((((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("ordered_nthP", [ordered_nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
522 ((((use_arg_then2 ("index_mem", [index_mem]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
523 ((fun arg_tac -> arg_tac (Arg_term (`SUC i < sizel l`))) (term_tac (have_gen_tac [](move ["Si"]))));
524 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("iffRL", [iffRL])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("index_mem", [index_mem])) (fun fst_arg -> (use_arg_then2 ("x'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x'_s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (((use_arg_then2 ("h_size", []))(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
525 ((fun arg_tac -> arg_tac (Arg_term (`x <= nth (&0) s (SUC i)`))) (term_tac (have_gen_tac []ALL_TAC)));
526 ((((use_arg_then2 ("sort_s", [])) (disch_tac [])) THEN (clear_assumption "sort_s") THEN BETA_TAC) THEN (((((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("ordered_nthP", [ordered_nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
527 (((((use_arg_then2 ("h_size", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Si", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltnSn", [ltnSn]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
528 ((THENL_FIRST) ((((use_arg_then2 ("x_ineq", [])) (disch_tac [])) THEN (clear_assumption "x_ineq") THEN ((fun arg_tac -> (use_arg_then2 ("IH", [])) (fun fst_arg -> (use_arg_then2 ("i", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then2 ("ants", [ants])) (disch_tac [])) THEN (clear_assumption "ants") THEN (DISCH_THEN apply_tac)) THEN (split_tac)) ((((use_arg_then2 ("Si", [])) (disch_tac [])) THEN (clear_assumption "Si") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
529 (((((use_arg_then2 ("nth_delete_at", [nth_delete_at]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("ltnn", [ltnn]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_delete1", [nth_delete1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("i_lt", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("y_def", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
530 (in_tac ["i_le"] false (((use_arg_then2 ("ltnNge", [ltnNge]))(gsym_then (thm_tac (new_rewrite [] []))))));
531 ((fun arg_tac -> arg_tac (Arg_term (`x' <= y`))) (term_tac (have_gen_tac []ALL_TAC)));
532 ((((use_arg_then2 ("sort_s'", [])) (disch_tac [])) THEN (clear_assumption "sort_s'") THEN BETA_TAC) THEN (((((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("ordered_nthP", [ordered_nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("nth_index", [nth_index])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("x'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("y_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
533 ((((use_arg_then2 ("h_size", []))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
534 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`i - 1 < i`))) (term_tac (have_gen_tac [](move ["Pi"])))) ((((use_arg_then2 ("i_le", [])) (disch_tac [])) THEN (clear_assumption "i_le") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
535 ((fun arg_tac -> arg_tac (Arg_term (`nth (&0) s (i - 1) <= x`))) (term_tac (have_gen_tac []ALL_TAC)));
536 ((((use_arg_then2 ("sort_s", [])) (disch_tac [])) THEN (clear_assumption "sort_s") THEN BETA_TAC) THEN (((((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("ordered_nthP", [ordered_nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("x_def", []))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))));
537 (((((use_arg_then2 ("h_size", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("i_ineq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
538 ((THENL_FIRST) ((((use_arg_then2 ("x_ineq", [])) (disch_tac [])) THEN (clear_assumption "x_ineq") THEN ((fun arg_tac -> (use_arg_then2 ("IH", [])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`i - 1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then2 ("ants", [ants])) (disch_tac [])) THEN (clear_assumption "ants") THEN (DISCH_THEN apply_tac)) THEN (split_tac)) ((((use_arg_then2 ("i_ineq", [])) (disch_tac [])) THEN (clear_assumption "i_ineq") THEN ((use_arg_then2 ("i_le", [])) (disch_tac [])) THEN (clear_assumption "i_le") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
539 ((((use_arg_then2 ("nth_delete_at", [nth_delete_at]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("Pi", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("nth_delete1", [nth_delete1]))(thm_tac (new_rewrite [] [])))));
540 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`~(i - 1 < indexl x' s')`))) (term_tac (have_gen_tac []((((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN (simp_tac))))) ((((use_arg_then2 ("i_le", [])) (disch_tac [])) THEN (clear_assumption "i_le") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
541 (((((fun arg_tac -> (use_arg_then2 ("ltn_predK", [ltn_predK])) (fun fst_arg -> (use_arg_then2 ("Pi", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("y_def", []))(thm_tac (new_rewrite [] []))))) THEN (arith_tac) THEN (done_tac));
544 (* Lemma min_exists *)
545 let min_exists = Sections.section_proof ["P";"n"]
546 `P (n:num) ==> ?m. P m /\ (!i. P i ==> m <= i)`
548 (((use_arg_then2 ("n", [])) (disch_tac [])) THEN (clear_assumption "n") THEN ((use_arg_then2 ("num_WF", [num_WF])) (thm_tac apply_tac)) THEN (move ["n"]) THEN (move ["IH"]) THEN (move ["Pn"]));
549 ((THENL) (((fun arg_tac -> (use_arg_then2 ("EXCLUDED_MIDDLE", [EXCLUDED_MIDDLE])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`!i:num. i < n ==> ~P i`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case) [(move ["h"]); ALL_TAC]);
550 (((use_arg_then2 ("n", [])) (term_tac exists_tac)) THEN (((((use_arg_then2 ("Pn", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN (move ["i"])));
551 ((((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac)) THEN (((use_arg_then2 ("NOT_LE", [NOT_LE]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
552 (((((use_arg_then2 ("NOT_FORALL_THM", [NOT_FORALL_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("NOT_IMP", [NOT_IMP]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN (move ["k"])) THEN (case THEN (move ["k_lt"])) THEN (move ["Pk"]));
553 ((((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("IH", [])) (fun fst_arg -> (use_arg_then2 ("k_lt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("Pk", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (case THEN (move ["m"])) THEN (move ["conds"])) THEN ((use_arg_then2 ("m", [])) (term_tac exists_tac)) THEN (done_tac));
556 (* Lemma min_exists_alt *)
557 let min_exists_alt = Sections.section_proof ["P"]
558 `(?n:num. P n) ==> ?m. P m /\ (!i. P i ==> m <= i)`
560 ((BETA_TAC THEN (case THEN (move ["n"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("min_exists", [min_exists])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (done_tac));
563 (* Lemma real_sorted_lt *)
564 let real_sorted_lt = Sections.section_proof ["l";"l'";"s";"s'"]
565 `sorted (<=) s l /\ sorted (<=) s' l' /\ sizel l' = sizel l /\
566 (!i. i < sizel l ==> EL i l <= EL i l') /\
567 (?i. i < sizel l /\ EL i l < EL i l') ==>
568 ?k. k < sizel l /\ (!i. i < k ==> EL i s = EL i s') /\ EL k s < EL k s'`
570 (BETA_TAC THEN (case THEN (move ["sort_s"])) THEN (case THEN (move ["sort_s'"])) THEN (case THEN (move ["size_eq"])) THEN (case THEN (move ["el_le"])) THEN (case THEN (move ["r"])) THEN (case THEN (move ["r_lt"])) THEN (move ["el_lt"]));
571 ((((use_arg_then2 ("sort_s'", [])) (disch_tac [])) THEN ((use_arg_then2 ("sort_s", [])) (disch_tac [])) THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] []))))) THEN ALL_TAC THEN (case THEN ((move ["ord_s"]) THEN (move ["perm_s"]))) THEN (case THEN ((move ["ord_s'"]) THEN (move ["perm_s'"])))));
572 ((fun arg_tac -> arg_tac (Arg_term (`sizel s = sizel l /\ sizel s' = sizel l`))) (term_tac (have_gen_tac [](move ["sizes"]))));
573 (((((fun arg_tac -> (use_arg_then2 ("perm_eq_size", [perm_eq_size])) (fun fst_arg -> (use_arg_then2 ("perm_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("perm_eq_size", [perm_eq_size])) (fun fst_arg -> (use_arg_then2 ("perm_s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
574 ((fun arg_tac -> arg_tac (Arg_term (`~(l = []) /\ ~(l' = [])`))) (term_tac (have_gen_tac [](move ["not_nil"]))));
575 (((repeat_tactic 1 9 (((use_arg_then2 ("size_eq0", [size_eq0]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then2 ("size_eq", []))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("r_lt", [])) (disch_tac [])) THEN (clear_assumption "r_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
576 ((fun arg_tac -> arg_tac (Arg_term (`list_sum l I < list_sum l' I`))) (term_tac (have_gen_tac [](move ["sum_neq"]))));
577 ((repeat_tactic 1 9 (((use_arg_then2 ("list_sum_EL", [list_sum_EL]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("size_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("SUM_LT", [SUM_LT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("FINITE_NUMSEG", [FINITE_NUMSEG]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("IN_NUMSEG", [IN_NUMSEG]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("leq0n", [leq0n]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac));
578 ((THENL_FIRST) ((THENL) (split_tac) [((move ["i"]) THEN (move ["i_le"])); ALL_TAC]) ((((use_arg_then2 ("el_le", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("r_lt", [])) (disch_tac [])) THEN (clear_assumption "r_lt") THEN ((use_arg_then2 ("i_le", [])) (disch_tac [])) THEN (clear_assumption "i_le") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
579 (((use_arg_then2 ("r", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("el_lt", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("r_lt", [])) (disch_tac [])) THEN (clear_assumption "r_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
580 (((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sorted_le", [sorted_le])) (fun fst_arg -> (use_arg_then2 ("REAL_LE_TRANS", [REAL_LE_TRANS])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("sort_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("sort_s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("size_eq", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)) THEN ((THENL) (ANTS_TAC) [((move ["i"]) THEN (move ["i_lt"])); (move ["s_le"])]));
581 (((repeat_tactic 1 9 (((use_arg_then2 ("EL_nth", [EL_nth]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("el_le", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
582 (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`?m. m < sizel l /\ ~(EL m s = EL m s')`))) (term_tac (have_gen_tac []ALL_TAC))));
583 ((DISCH_THEN (fun snd_th -> (use_arg_then2 ("min_exists_alt", [min_exists_alt])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC THEN (case THEN (move ["m"])) THEN (case THEN ALL_TAC) THEN (case THEN ((move ["m_lt"]) THEN (move ["m_neq"]))) THEN (move ["m_min"]));
584 (((use_arg_then2 ("m", [])) (term_tac exists_tac)) THEN ((((use_arg_then2 ("m_lt", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] []))))) THEN ((THENL) (split_tac) [((move ["i"]) THEN (move ["i_lt"])); ALL_TAC]));
585 ((((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("m_min", [])) (thm_tac (match_mp_then snd_th MP_TAC))))) THEN (((use_arg_then2 ("m_lt", [])) (disch_tac [])) THEN (clear_assumption "m_lt") THEN ((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
586 ((((fun arg_tac -> (use_arg_then2 ("s_le", [])) (fun fst_arg -> (use_arg_then2 ("m_lt", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((repeat_tactic 1 9 (((use_arg_then2 ("EL_nth", [EL_nth]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("sizes", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("REAL_LE_LT", [REAL_LE_LT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("m_neq", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
587 (((use_arg_then2 ("sum_neq", [])) (disch_tac [])) THEN (clear_assumption "sum_neq") THEN ((use_arg_then2 ("contraLR", [contraLR])) (disch_tac [])) THEN (clear_assumption "contraLR") THEN (DISCH_THEN apply_tac));
588 ((((((use_arg_then2 ("NOT_EXISTS_THM", [NOT_EXISTS_THM]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negb_and", [negb_and]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("negbK", [negbK]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_NOT_LT", [REAL_NOT_LT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LE_LT", [REAL_LE_LT]))(thm_tac (new_rewrite [] []))))) THEN (move ["h"])) THEN (DISJ2_TAC));
589 ((((fun arg_tac -> (use_arg_then2 ("list_sum_perm_eq", [list_sum_perm_eq])) (fun fst_arg -> (use_arg_then2 ("perm_s", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("list_sum_perm_eq", [list_sum_perm_eq])) (fun fst_arg -> (use_arg_then2 ("perm_s'", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(gsym_then (thm_tac (new_rewrite [] []))))));
590 (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("list_sum_nth_eq", [list_sum_nth_eq])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (thm_tac apply_tac)) THEN (((repeat_tactic 1 9 (((use_arg_then2 ("sizes", []))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("I_THM", [I_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["i"]) THEN (move ["i_lt"])));
591 ((repeat_tactic 1 9 (((use_arg_then2 ("EL_nth", [EL_nth]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("sizes", []))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
592 ((((fun arg_tac -> (use_arg_then2 ("h", [])) (fun fst_arg -> (use_arg_then2 ("i", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("i_lt", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
595 (* Finalization of the section SortedReal *)
596 let ordered_real_nseq = Sections.finalize_theorem ordered_real_nseq;;
597 let ordered_cat_filter = Sections.finalize_theorem ordered_cat_filter;;
598 let real_merge_sort = Sections.finalize_theorem real_merge_sort;;
599 let ants = Sections.finalize_theorem ants;;
600 let sort_continuous = Sections.finalize_theorem sort_continuous;;
601 let min_exists = Sections.finalize_theorem min_exists;;
602 let min_exists_alt = Sections.finalize_theorem min_exists_alt;;
603 let real_sorted_lt = Sections.finalize_theorem real_sorted_lt;;
604 Sections.end_section "SortedReal";;
607 Sections.begin_section "MinK";;
609 (* Lemma min_k_ordered *)
610 let min_k_ordered = Sections.section_proof ["i";"j";"list"]
611 `j < LENGTH list /\ i <= j ==> min_k i list <= min_k j list`
613 (((((use_arg_then2 ("size", [size]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("min_k", [min_k]))(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (move ["j_lt"])) THEN (move ["i_le_j"]));
614 ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`i < sizel list`))) (term_tac (have_gen_tac [](move ["i_lt"])))) ((((use_arg_then2 ("j_lt", [])) (disch_tac [])) THEN (clear_assumption "j_lt") THEN ((use_arg_then2 ("i_le_j", [])) (disch_tac [])) THEN (clear_assumption "i_le_j") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
615 ((repeat_tactic 1 9 (((fun arg_tac -> (use_arg_then2 ("EL_nth", [EL_nth])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_merge_sort", [size_merge_sort]))(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)));
616 ((THENL_FIRST) ((THENL) (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("iffLR", [iffLR])) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("leq_eqVlt", [leq_eqVlt])) (fun fst_arg -> (use_arg_then2 ("i", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("j", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("i_le_j", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case) [(((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))); (move ["i_lt_j"])]) ((((use_arg_then2 ("REAL_LE_REFL", [REAL_LE_REFL]))(thm_tac (new_rewrite [] [])))) THEN (done_tac)));
617 ((((fun arg_tac -> (use_arg_then2 ("real_merge_sort", [real_merge_sort])) (fun fst_arg -> (use_arg_then2 ("list", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("ordered_nthP", [ordered_nthP])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_merge_sort", [size_merge_sort]))(thm_tac (new_rewrite [] [])))) THEN (done_tac));
620 (* Lemma mem_min_k *)
621 let mem_min_k = Sections.section_proof ["k";"list"]
622 `k < LENGTH list ==> min_k k list <- list`
624 (((((use_arg_then2 ("min_k", [min_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size", [size]))(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (move ["k_lt"]));
625 ((((fun arg_tac -> (use_arg_then2 ("real_merge_sort", [real_merge_sort])) (fun fst_arg -> (use_arg_then2 ("list", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("sorted", [sorted]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["_"])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("perm_eq_mem", [perm_eq_mem])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))));
626 (((((use_arg_then2 ("MEM_EL", [MEM_EL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("size", [size]))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("size_merge_sort", [size_merge_sort]))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
629 (* Lemma min_k0_le_EL *)
630 let min_k0_le_EL = Sections.section_proof ["l"]
631 `!i. i < sizel l ==> min_k 0 l <= EL i l`
633 ((THENL_FIRST) ((BETA_TAC THEN (move ["i"]) THEN (move ["i_lt"])) THEN ((((use_arg_then2 ("min_k", [min_k]))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then2 ("EL_nth", [EL_nth])) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`&0`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size_merge_sort", [size_merge_sort]))(thm_tac (new_rewrite [] []))))))) ((((use_arg_then2 ("i_lt", [])) (disch_tac [])) THEN (clear_assumption "i_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
634 ((((fun arg_tac -> arg_tac (Arg_theorem (REAL_ARITH `!a b. a <= b <=> a <= b \/ a = b`)))(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> arg_tac (Arg_term (`_1 = _2`))) (disch_eq_tac "neq" [])) THEN case THEN (simp_tac) THEN (process_fst_eq_tac)));
635 (((fun arg_tac -> (use_arg_then2 ("real_merge_sort", [real_merge_sort])) (fun fst_arg -> (use_arg_then2 ("l", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("nth0_sorted_imp", [nth0_sorted_imp])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN (DISCH_THEN apply_tac));
636 (((((use_arg_then2 ("MEM_EL", [MEM_EL]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then2 ("size", [size]))(gsym_then (thm_tac (new_rewrite [] []))))))) THEN (done_tac));
639 (* Finalization of the section MinK *)
640 let min_k_ordered = Sections.finalize_theorem min_k_ordered;;
641 let mem_min_k = Sections.finalize_theorem mem_min_k;;
642 let min_k0_le_EL = Sections.finalize_theorem min_k0_le_EL;;
643 Sections.end_section "MinK";;
645 (* Close the module *)