text_formalization/tame/ssreflect/sort-compiled.hl

   1 needs "tame/ssreflect/seq2-compiled.hl";;
   2
   3 (* Module Sort*)
   4 module Sort = struct
   5
   6 open Ssrbool;;
   7 open Ssrnat;;
   8 open Seq;;
   9 open Seq2;;
  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)`;;
  17
  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`
  22 [
  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));
  26 ];;
  27
  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))`
  32 [
  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));
  36 ];;
  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)`;;
  39
  40 (* Section Merge *)
  41 Sections.begin_section "Merge";;
  42
  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)`
  46 [
  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));
  50 ];;
  51
  52 (* Lemma all_merge *)
  53 let all_merge = Sections.section_proof ["R";"s1";"s2";"P"]
  54 `all P (merge R s1 s2) <=> all P s1 /\ all P s2`
  55 [
  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));
  58 ];;
  59
  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";;
  64
  65 (* Section Ordered *)
  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`))));;
  69
  70 (* Lemma ordered1 *)
  71 let ordered1 = Sections.section_proof ["x"]
  72 `ordered R [x]`
  73 [
  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));
  75 ];;
  76
  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`
  81 [
  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));
  84 ];;
  85
  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))`
  89 [
  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));
  98 ];;
  99
 100 (* Lemma ordered_nseq *)
 101 let ordered_nseq = Sections.section_proof ["n";"x"]
 102 `R x x ==> ordered R (nseq n x)`
 103 [
 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));
 108 ];;
 109
 110 (* Lemma ordered_subseq *)
 111 let ordered_subseq = Sections.section_proof ["s1";"s2"]
 112 `subseq s1 s2 /\ ordered R s2 ==> ordered R s1`
 113 [
 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));
 119 ];;
 120
 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)`
 124 [
 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));
 126 ];;
 127
 128 (* Lemma ordered_delete1 *)
 129 let ordered_delete1 = Sections.section_proof ["x";"s"]
 130 `ordered R s ==> ordered R (delete1 x s)`
 131 [
 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));
 133 ];;
 134
 135 (* Lemma ordered_filter *)
 136 let ordered_filter = Sections.section_proof ["a";"s"]
 137 `ordered R s ==> ordered R (filter a s)`
 138 [
 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));
 140 ];;
 141
 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`));;
 147
 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)`
 152 [
 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));
 167 ];;
 168
 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`));;
 173
 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`
 177 [
 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));
 187 ];;
 188
 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`
 193 [
 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));
 213 ];;
 214
 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`
 218 [
 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));
 221 ];;
 222
 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";;
 237
 238 (* Section Sorted *)
 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`))));;
 242
 243 (* Lemma sorted_size *)
 244 let sorted_size = Sections.section_proof ["s1";"s2"]
 245 `sorted R s1 s2 ==> sizel s1 = sizel s2`
 246 [
 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));
 248 ];;
 249
 250 (* Lemma sorted_mem *)
 251 let sorted_mem = Sections.section_proof ["s1";"s2"]
 252 `sorted R s1 s2 ==> (!x. x <- s1 <=> x <- s2)`
 253 [
 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));
 255 ];;
 256
 257 (* Lemma size_merge *)
 258 let size_merge = Sections.section_proof ["s1";"s2"]
 259 `sizel (merge R s1 s2) = sizel s1 + sizel s2`
 260 [
 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));
 262 ];;
 263
 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)`
 268 [
 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));
 270 ];;
 271
 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)`
 276 [
 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));
 279 ];;
 280
 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)`
 284 [
 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));
 286 ];;
 287
 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)`
 291 [
 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));
 294 ];;
 295
 296 (* Lemma perm_eq_merge_sort *)
 297 let perm_eq_merge_sort = Sections.section_proof ["s"]
 298 `perm_eq (merge_sort R s) s`
 299 [
 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));
 306 ];;
 307
 308 (* Lemma size_merge_sort *)
 309 let size_merge_sort = Sections.section_proof ["l"]
 310 `sizel (merge_sort R l) = sizel l`
 311 [
 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));
 313 ];;
 314
 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`));;
 318
 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`
 322 [
 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));
 325 ];;
 326
 327 (* Finalization of the section SortedEq *)
 328 let sorted_eq = Sections.finalize_theorem sorted_eq;;
 329 Sections.end_section "SortedEq";;
 330
 331 (* Section SortedNth0 *)
 332 Sections.begin_section "SortedNth0";;
 333
 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)`
 337 [
 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));
 343 ];;
 344 (Sections.add_section_hyp "R_anti" (`!x y. R x y /\ R y x ==> x = y`));;
 345
 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))`
 350 [
 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));
 358 ];;
 359
 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`));;
 365
 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))`
 371 [
 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));
 407 ];;
 408 (Sections.add_section_hyp "R_total" (`!x y. R x y \/ R y x`));;
 409
 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)`
 413 [
 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));
 415 ];;
 416
 417 (* Lemma ordered_merge_sort *)
 418 let ordered_merge_sort = Sections.section_proof ["s"]
 419 `ordered R (merge_sort R s)`
 420 [
 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));
 425 ];;
 426
 427 (* Lemma sorted_merge_sort *)
 428 let sorted_merge_sort = Sections.section_proof ["s"]
 429 `sorted R (merge_sort R s) s`
 430 [
 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));
 432 ];;
 433
 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";;
 452
 453 (* Section SortedReal *)
 454 Sections.begin_section "SortedReal";;
 455 prioritize_real();;
 456
 457 (* Lemma ordered_real_nseq *)
 458 let ordered_real_nseq = Sections.section_proof ["n";"x"]
 459 `ordered (<=) (nseq n x)`
 460 [
 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));
 462 ];;
 463
 464 (* Lemma ordered_cat_filter *)
 465 let ordered_cat_filter = Sections.section_proof ["s";"v"]
 466 `ordered (<=) s ==>
 467         s = filter (\x. x <= v) s ++ filter (predC (\x. x <= v)) s`
 468 [
 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));
 474 ];;
 475
 476 (* Lemma real_merge_sort *)
 477 let real_merge_sort = Sections.section_proof ["s"]
 478 `sorted (<=) (merge_sort (<=) s) s`
 479 [
 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));
 481 ];;
 482
 483 (* Lemma ants *)
 484 let ants = Sections.section_proof ["P";"Q";"R"]
 485 `P /\ (Q ==> R) ==> ((P ==> Q) ==> R)`
 486 [
 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));
 488 ];;
 489
 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)`
 495 [
 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));
 542 ];;
 543
 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)`
 547 [
 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));
 554 ];;
 555
 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)`
 559 [
 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));
 561 ];;
 562
 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'`
 569 [
 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));
 593 ];;
 594
 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";;
 605
 606 (* Section MinK *)
 607 Sections.begin_section "MinK";;
 608
 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`
 612 [
 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));
 618 ];;
 619
 620 (* Lemma mem_min_k *)
 621 let mem_min_k = Sections.section_proof ["k";"list"]
 622 `k < LENGTH list ==> min_k k list <- list`
 623 [
 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));
 627 ];;
 628
 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`
 632 [
 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));
 637 ];;
 638
 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";;
 644
 645 (* Close the module *)
 646 end;;