Structure mergesortTheory


Source File Identifier index Theory binding index

signature mergesortTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val mergesort_def : thm
    val mergesort_tail_def : thm
    val sort2_def : thm
    val sort2_tail_def : thm
    val sort3_def : thm
    val sort3_tail_def : thm
    val stable_def : thm
  
  (*  Theorems  *)
    val filter_merge : thm
    val merge_def : thm
    val merge_empty : thm
    val merge_ind : thm
    val merge_perm : thm
    val merge_sorted : thm
    val merge_stable : thm
    val merge_tail_correct1 : thm
    val merge_tail_correct2 : thm
    val merge_tail_def : thm
    val merge_tail_ind : thm
    val mergesortN_correct : thm
    val mergesortN_def : thm
    val mergesortN_ind : thm
    val mergesortN_perm : thm
    val mergesortN_sorted : thm
    val mergesortN_stable : thm
    val mergesortN_tail_def : thm
    val mergesortN_tail_ind : thm
    val mergesort_STABLE_SORT : thm
    val mergesort_mem : thm
    val mergesort_perm : thm
    val mergesort_sorted : thm
    val mergesort_stable : thm
    val mergesort_tail_correct : thm
    val sort2_perm : thm
    val sort2_sorted : thm
    val sort2_stable : thm
    val sort2_tail_correct : thm
    val sort3_perm : thm
    val sort3_sorted : thm
    val sort3_stable : thm
    val sort3_tail_correct : thm
    val stable_cong : thm
    val stable_trans : thm
  
  val mergesort_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [sorting] Parent theory of "mergesort"
   
   [mergesort_def]  Definition
      
      ⊢ ∀R l. mergesort R l = mergesortN R (LENGTH l) l
   
   [mergesort_tail_def]  Definition
      
      ⊢ ∀R l. mergesort_tail R l = mergesortN_tail F R (LENGTH l) l
   
   [sort2_def]  Definition
      
      ⊢ ∀R x y. sort2 R x y = if R x y then [x; y] else [y; x]
   
   [sort2_tail_def]  Definition
      
      ⊢ ∀neg R x y.
            sort2_tail neg R x y = if R x y ⇎ neg then [x; y] else [y; x]
   
   [sort3_def]  Definition
      
      ⊢ ∀R x y z.
            sort3 R x y z =
            if R x y then
              if R y z then [x; y; z]
              else if R x z then [x; z; y]
              else [z; x; y]
            else if R y z then if R x z then [y; x; z] else [y; z; x]
            else [z; y; x]
   
   [sort3_tail_def]  Definition
      
      ⊢ ∀neg R x y z.
            sort3_tail neg R x y z =
            if R x y ⇎ neg then
              if R y z ⇎ neg then [x; y; z]
              else if R x z ⇎ neg then [x; z; y]
              else [z; x; y]
            else if R y z ⇎ neg then
              if R x z ⇎ neg then [y; x; z] else [y; z; x]
            else [z; y; x]
   
   [stable_def]  Definition
      
      ⊢ ∀R l1 l2.
            stable R l1 l2 ⇔
            ∀p. (∀x y. p x ∧ p y ⇒ R x y) ⇒ FILTER p l1 = FILTER p l2
   
   [filter_merge]  Theorem
      
      ⊢ ∀P R l1 l2.
            transitive R ∧ (∀x y. P x ∧ P y ⇒ R x y) ∧ SORTED R l1 ⇒
            FILTER P (merge R l1 l2) = FILTER P (l1 ⧺ l2)
   
   [merge_def]  Theorem
      
      ⊢ (∀R. merge R [] [] = []) ∧
        (∀v9 v8 R. merge R (v8::v9) [] = v8::v9) ∧
        (∀v5 v4 R. merge R [] (v4::v5) = v4::v5) ∧
        ∀y x l2 l1 R.
            merge R (x::l1) (y::l2) =
            if R x y then x::merge R l1 (y::l2) else y::merge R (x::l1) l2
   
   [merge_empty]  Theorem
      
      ⊢ ∀R l acc. merge R l [] = l ∧ merge R [] l = l
   
   [merge_ind]  Theorem
      
      ⊢ ∀P.
            (∀R. P R [] []) ∧ (∀R v8 v9. P R (v8::v9) []) ∧
            (∀R v4 v5. P R [] (v4::v5)) ∧
            (∀R x l1 y l2.
                 (¬R x y ⇒ P R (x::l1) l2) ∧ (R x y ⇒ P R l1 (y::l2)) ⇒
                 P R (x::l1) (y::l2)) ⇒
            ∀v v1 v2. P v v1 v2
   
   [merge_perm]  Theorem
      
      ⊢ ∀R l1 l2. PERM (l1 ⧺ l2) (merge R l1 l2)
   
   [merge_sorted]  Theorem
      
      ⊢ ∀R l1 l2.
            transitive R ∧ total R ∧ SORTED R l1 ∧ SORTED R l2 ⇒
            SORTED R (merge R l1 l2)
   
   [merge_stable]  Theorem
      
      ⊢ ∀R l1 l2.
            transitive R ∧ SORTED R l1 ⇒ stable R (l1 ⧺ l2) (merge R l1 l2)
   
   [merge_tail_correct1]  Theorem
      
      ⊢ ∀neg R l1 l2 acc.
            (neg ⇔ F) ⇒
            merge_tail neg R l1 l2 acc = REVERSE (merge R l1 l2) ⧺ acc
   
   [merge_tail_correct2]  Theorem
      
      ⊢ ∀neg R l1 l2 acc.
            (neg ⇔ T) ∧ transitive R ∧ SORTED R (REVERSE l1) ∧
            SORTED R (REVERSE l2) ⇒
            merge_tail neg R l1 l2 acc =
            merge R (REVERSE l1) (REVERSE l2) ⧺ acc
   
   [merge_tail_def]  Theorem
      
      ⊢ (∀negate acc R. merge_tail negate R [] [] acc = acc) ∧
        (∀v13 v12 negate acc R.
             merge_tail negate R (v12::v13) [] acc = REV (v12::v13) acc) ∧
        (∀v9 v8 negate acc R.
             merge_tail negate R [] (v8::v9) acc = REV (v8::v9) acc) ∧
        ∀y x negate l2 l1 acc R.
            merge_tail negate R (x::l1) (y::l2) acc =
            if R x y ⇎ negate then merge_tail negate R l1 (y::l2) (x::acc)
            else merge_tail negate R (x::l1) l2 (y::acc)
   
   [merge_tail_ind]  Theorem
      
      ⊢ ∀P.
            (∀negate R acc. P negate R [] [] acc) ∧
            (∀negate R v12 v13 acc. P negate R (v12::v13) [] acc) ∧
            (∀negate R v8 v9 acc. P negate R [] (v8::v9) acc) ∧
            (∀negate R x l1 y l2 acc.
                 (¬(R x y ⇎ negate) ⇒ P negate R (x::l1) l2 (y::acc)) ∧
                 ((R x y ⇎ negate) ⇒ P negate R l1 (y::l2) (x::acc)) ⇒
                 P negate R (x::l1) (y::l2) acc) ⇒
            ∀v v1 v2 v3 v4. P v v1 v2 v3 v4
   
   [mergesortN_correct]  Theorem
      
      ⊢ ∀negate R n l.
            total R ∧ transitive R ⇒
            mergesortN_tail negate R n l =
            if negate then REVERSE (mergesortN R n l) else mergesortN R n l
   
   [mergesortN_def]  Theorem
      
      ⊢ (∀l R. mergesortN R 0 l = []) ∧
        (∀x l R. mergesortN R 1 (x::l) = [x]) ∧
        (∀R. mergesortN R 1 [] = []) ∧
        (∀y x l R. mergesortN R 2 (x::y::l) = sort2 R x y) ∧
        (∀x R. mergesortN R 2 [x] = [x]) ∧ (∀R. mergesortN R 2 [] = []) ∧
        (∀z y x l R. mergesortN R 3 (x::y::z::l) = sort3 R x y z) ∧
        (∀y x R. mergesortN R 3 [x; y] = sort2 R x y) ∧
        (∀x R. mergesortN R 3 [x] = [x]) ∧ (∀R. mergesortN R 3 [] = []) ∧
        ∀v4 l R.
            mergesortN R v4 l =
            if v4 = 0 then []
            else if v4 = 1 then case l of [] => [] | x::l' => [x]
            else if v4 = 2 then
              case l of
                [] => []
              | [x'] => [x']
              | x'::y::l'' => sort2 R x' y
            else if v4 = 3 then
              case l of
                [] => []
              | [x''] => [x'']
              | [x''; y'] => sort2 R x'' y'
              | x''::y'::z::l'³' => sort3 R x'' y' z
            else
              (let
                 len1 = DIV2 v4
               in
                 merge R (mergesortN R (DIV2 v4) l)
                   (mergesortN R (v4 − len1) (DROP len1 l)))
   
   [mergesortN_ind]  Theorem
      
      ⊢ ∀P.
            (∀R l. P R 0 l) ∧ (∀R x l. P R 1 (x::l)) ∧ (∀R. P R 1 []) ∧
            (∀R x y l. P R 2 (x::y::l)) ∧ (∀R x. P R 2 [x]) ∧
            (∀R. P R 2 []) ∧ (∀R x y z l. P R 3 (x::y::z::l)) ∧
            (∀R x y. P R 3 [x; y]) ∧ (∀R x. P R 3 [x]) ∧ (∀R. P R 3 []) ∧
            (∀R v4 l.
                 (∀len1.
                      v4 ≠ 0 ∧ v4 ≠ 1 ∧ v4 ≠ 2 ∧ v4 ≠ 3 ∧ len1 = DIV2 v4 ⇒
                      P R (DIV2 v4) l) ∧
                 (∀len1.
                      v4 ≠ 0 ∧ v4 ≠ 1 ∧ v4 ≠ 2 ∧ v4 ≠ 3 ∧ len1 = DIV2 v4 ⇒
                      P R (v4 − len1) (DROP len1 l)) ⇒
                 P R v4 l) ⇒
            ∀v v1 v2. P v v1 v2
   
   [mergesortN_perm]  Theorem
      
      ⊢ ∀R n l. PERM (TAKE n l) (mergesortN R n l)
   
   [mergesortN_sorted]  Theorem
      
      ⊢ ∀R n l. total R ∧ transitive R ⇒ SORTED R (mergesortN R n l)
   
   [mergesortN_stable]  Theorem
      
      ⊢ ∀R n l.
            total R ∧ transitive R ⇒ stable R (TAKE n l) (mergesortN R n l)
   
   [mergesortN_tail_def]  Theorem
      
      ⊢ (∀negate l R. mergesortN_tail negate R 0 l = []) ∧
        (∀x negate l R. mergesortN_tail negate R 1 (x::l) = [x]) ∧
        (∀negate R. mergesortN_tail negate R 1 [] = []) ∧
        (∀y x negate l R.
             mergesortN_tail negate R 2 (x::y::l) = sort2_tail negate R x y) ∧
        (∀x negate R. mergesortN_tail negate R 2 [x] = [x]) ∧
        (∀negate R. mergesortN_tail negate R 2 [] = []) ∧
        (∀z y x negate l R.
             mergesortN_tail negate R 3 (x::y::z::l) =
             sort3_tail negate R x y z) ∧
        (∀y x negate R.
             mergesortN_tail negate R 3 [x; y] = sort2_tail negate R x y) ∧
        (∀x negate R. mergesortN_tail negate R 3 [x] = [x]) ∧
        (∀negate R. mergesortN_tail negate R 3 [] = []) ∧
        ∀v6 negate l R.
            mergesortN_tail negate R v6 l =
            if v6 = 0 then []
            else if v6 = 1 then case l of [] => [] | x::l' => [x]
            else if v6 = 2 then
              case l of
                [] => []
              | [x'] => [x']
              | x'::y::l'' => sort2_tail negate R x' y
            else if v6 = 3 then
              case l of
                [] => []
              | [x''] => [x'']
              | [x''; y'] => sort2_tail negate R x'' y'
              | x''::y'::z::l'³' => sort3_tail negate R x'' y' z
            else
              (let
                 len1 = DIV2 v6 ;
                 neg = ¬negate
               in
                 merge_tail neg R (mergesortN_tail neg R (DIV2 v6) l)
                   (mergesortN_tail neg R (v6 − len1) (DROP len1 l)) [])
   
   [mergesortN_tail_ind]  Theorem
      
      ⊢ ∀P.
            (∀negate R l. P negate R 0 l) ∧
            (∀negate R x l. P negate R 1 (x::l)) ∧
            (∀negate R. P negate R 1 []) ∧
            (∀negate R x y l. P negate R 2 (x::y::l)) ∧
            (∀negate R x. P negate R 2 [x]) ∧
            (∀negate R. P negate R 2 []) ∧
            (∀negate R x y z l. P negate R 3 (x::y::z::l)) ∧
            (∀negate R x y. P negate R 3 [x; y]) ∧
            (∀negate R x. P negate R 3 [x]) ∧
            (∀negate R. P negate R 3 []) ∧
            (∀negate R v6 l.
                 (∀len1 neg.
                      v6 ≠ 0 ∧ v6 ≠ 1 ∧ v6 ≠ 2 ∧ v6 ≠ 3 ∧ len1 = DIV2 v6 ∧
                      (neg ⇔ ¬negate) ⇒
                      P neg R (DIV2 v6) l) ∧
                 (∀len1 neg.
                      v6 ≠ 0 ∧ v6 ≠ 1 ∧ v6 ≠ 2 ∧ v6 ≠ 3 ∧ len1 = DIV2 v6 ∧
                      (neg ⇔ ¬negate) ⇒
                      P neg R (v6 − len1) (DROP len1 l)) ⇒
                 P negate R v6 l) ⇒
            ∀v v1 v2 v3. P v v1 v2 v3
   
   [mergesort_STABLE_SORT]  Theorem
      
      ⊢ ∀R. transitive R ∧ total R ⇒ STABLE mergesort R
   
   [mergesort_mem]  Theorem
      
      ⊢ ∀R L x. MEM x (mergesort R L) ⇔ MEM x L
   
   [mergesort_perm]  Theorem
      
      ⊢ ∀R l. PERM l (mergesort R l)
   
   [mergesort_sorted]  Theorem
      
      ⊢ ∀R l. transitive R ∧ total R ⇒ SORTED R (mergesort R l)
   
   [mergesort_stable]  Theorem
      
      ⊢ ∀R l. transitive R ∧ total R ⇒ stable R l (mergesort R l)
   
   [mergesort_tail_correct]  Theorem
      
      ⊢ ∀R l. total R ∧ transitive R ⇒ mergesort_tail R l = mergesort R l
   
   [sort2_perm]  Theorem
      
      ⊢ ∀R x y. PERM [x; y] (sort2 R x y)
   
   [sort2_sorted]  Theorem
      
      ⊢ ∀R x y. total R ⇒ SORTED R (sort2 R x y)
   
   [sort2_stable]  Theorem
      
      ⊢ ∀R x y. stable R [x; y] (sort2 R x y)
   
   [sort2_tail_correct]  Theorem
      
      ⊢ ∀neg R x y.
            sort2_tail neg R x y =
            if neg then REVERSE (sort2 R x y) else sort2 R x y
   
   [sort3_perm]  Theorem
      
      ⊢ ∀R x y z. PERM [x; y; z] (sort3 R x y z)
   
   [sort3_sorted]  Theorem
      
      ⊢ ∀R x y z. total R ⇒ SORTED R (sort3 R x y z)
   
   [sort3_stable]  Theorem
      
      ⊢ ∀R x y z.
            total R ∧ transitive R ⇒ stable R [x; y; z] (sort3 R x y z)
   
   [sort3_tail_correct]  Theorem
      
      ⊢ ∀neg R x y z.
            sort3_tail neg R x y z =
            if neg then REVERSE (sort3 R x y z) else sort3 R x y z
   
   [stable_cong]  Theorem
      
      ⊢ ∀R l1 l2 l3 l4.
            stable R l1 l2 ∧ stable R l3 l4 ⇒ stable R (l1 ⧺ l3) (l2 ⧺ l4)
   
   [stable_trans]  Theorem
      
      ⊢ ∀R l1 l2 l3. stable R l1 l2 ∧ stable R l2 l3 ⇒ stable R l1 l3
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-13