HOL4-data-structures/topdown_mergesortCorrectnessTheory.sig at main · artisanbk/HOL4-data-structures · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
signature topdown_mergesortCorrectnessTheory =
sig
  type thm = Thm.thm

  (*  Theorems  *)
    val CORRECTNESS_MSET_TOP_DOWN_MERGESORT_thm : thm
    val CORRECTNESS_SORTED_TOP_DOWN_MERGESORT_thm : thm
    val MEM_TOP_DOWN_MERGEAUXILLARY_lemma : thm
    val MSET_MERGEAUXILLARY_lemma : thm
    val SORTED_MERGEAUXILLARY_lemma : thm
    val TOP_DOWN_MERGEAUXILLARY_def : thm
    val TOP_DOWN_MERGEAUXILLARY_ind : thm
    val TOP_DOWN_MERGESORT_def : thm
    val TOP_DOWN_MERGESORT_ind : thm
(*
   [container] Parent theory of "topdown_mergesortCorrectness"

   [CORRECTNESS_MSET_TOP_DOWN_MERGESORT_thm]  Theorem

      ⊢ ∀R xs. LIST_TO_BAG (top_down_mergesort R xs) = LIST_TO_BAG xs

   [CORRECTNESS_SORTED_TOP_DOWN_MERGESORT_thm]  Theorem

      ⊢ ∀R xs. total R ∧ transitive R ⇒ SORTED R (top_down_mergesort R xs)

   [MEM_TOP_DOWN_MERGEAUXILLARY_lemma]  Theorem

      ⊢ ∀R xs ys.
          MEM x (top_down_mergeauxillary R xs ys) ⇔ MEM x xs ∨ MEM x ys

   [MSET_MERGEAUXILLARY_lemma]  Theorem

      ⊢ ∀R xs ys.
          LIST_TO_BAG (top_down_mergeauxillary R xs ys) =
          LIST_TO_BAG xs ⊎ LIST_TO_BAG ys

   [SORTED_MERGEAUXILLARY_lemma]  Theorem

      ⊢ ∀R xs ys.
          transitive R ∧ total R ⇒
          (SORTED R (top_down_mergeauxillary R xs ys) ⇔
           SORTED R xs ∧ SORTED R ys)

   [TOP_DOWN_MERGEAUXILLARY_def]  Theorem

      ⊢ (∀xs R. top_down_mergeauxillary R xs [] = xs) ∧
        (∀v5 v4 R. top_down_mergeauxillary R [] (v4::v5) = v4::v5) ∧
        ∀ys y xs x R.
          top_down_mergeauxillary R (x::xs) (y::ys) =
          if R x y then x::top_down_mergeauxillary R xs (y::ys)
          else y::top_down_mergeauxillary R (x::xs) ys

   [TOP_DOWN_MERGEAUXILLARY_ind]  Theorem

      ⊢ ∀P. (∀R xs. P R xs []) ∧ (∀R v4 v5. P R [] (v4::v5)) ∧
            (∀R x xs y ys.
               (¬R x y ⇒ P R (x::xs) ys) ∧ (R x y ⇒ P R xs (y::ys)) ⇒
               P R (x::xs) (y::ys)) ⇒
            ∀v v1 v2. P v v1 v2

   [TOP_DOWN_MERGESORT_def]  Theorem

      ⊢ (∀R. top_down_mergesort R [] = []) ∧
        (∀x R. top_down_mergesort R [x] = [x]) ∧
        ∀v7 v6 v2 R.
          top_down_mergesort R (v2::v6::v7) =
          top_down_mergeauxillary R
            (top_down_mergesort R
               (TAKE (LENGTH (v2::v6::v7) DIV 2) (v2::v6::v7)))
            (top_down_mergesort R
               (DROP (LENGTH (v2::v6::v7) DIV 2) (v2::v6::v7)))

   [TOP_DOWN_MERGESORT_ind]  Theorem

      ⊢ ∀P. (∀R. P R []) ∧ (∀R x. P R [x]) ∧
            (∀R v2 v6 v7.
               P R (DROP (LENGTH (v2::v6::v7) DIV 2) (v2::v6::v7)) ∧
               P R (TAKE (LENGTH (v2::v6::v7) DIV 2) (v2::v6::v7)) ⇒
               P R (v2::v6::v7)) ⇒
            ∀v v1. P v v1


*)
end