Sorting-in-HOL4/bottomup_mergesortCorrectnessTheory.sig at main · Linisac/Sorting-in-HOL4 · 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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
signature bottomup_mergesortCorrectnessTheory =
sig
  type thm = Thm.thm

  (*  Definitions  *)
    val BOTTOM_UP_MERGESORT_def : thm

  (*  Theorems  *)
    val BOTTOM_UP_MERGEADJACENT_def : thm
    val BOTTOM_UP_MERGEADJACENT_ind : thm
    val BOTTOM_UP_MERGEALL_MAP_lemma : thm
    val BOTTOM_UP_MERGEALL_def : thm
    val BOTTOM_UP_MERGEALL_ind : thm
    val BOTTOM_UP_MERGEAUXILLARY_def : thm
    val BOTTOM_UP_MERGEAUXILLARY_ind : thm
    val CORRECTNESS_MSET_BOTTOM_UP_MERGESORT_thm : thm
    val CORRECTNESS_SORTED_BOTTOM_UP_MERGESORT_thm : thm
    val MEM_BOTTOM_UP_MERGEAUXILLARY_lemma : thm
    val MSET_BOTTOM_UP_MERGEADJACENT_lemma : thm
    val MSET_BOTTOM_UP_MERGEALL_lemma : thm
    val MSET_BOTTOM_UP_MERGEAUXILLARY_lemma : thm
    val SORTED_BOTTOM_UP_MERGEADJACENT_lemma : thm
    val SORTED_BOTTOM_UP_MERGEAUXILLARY_lemma : thm
(*
   [container] Parent theory of "bottomup_mergesortCorrectness"

   [BOTTOM_UP_MERGESORT_def]  Definition

      ⊢ ∀R xs.
          bottom_up_mergesort R xs =
          bottom_up_mergeall R (MAP (λx. [x]) xs)

   [BOTTOM_UP_MERGEADJACENT_def]  Theorem

      ⊢ (∀R. bottom_up_mergeadjacent R [] = []) ∧
        (∀xs R. bottom_up_mergeadjacent R [xs] = [xs]) ∧
        ∀ys xs lst R.
          bottom_up_mergeadjacent R (xs::ys::lst) =
          bottom_up_mergeauxillary R xs ys::bottom_up_mergeadjacent R lst

   [BOTTOM_UP_MERGEADJACENT_ind]  Theorem

      ⊢ ∀P. (∀R. P R []) ∧ (∀R xs. P R [xs]) ∧
            (∀R xs ys lst. P R lst ⇒ P R (xs::ys::lst)) ⇒
            ∀v v1. P v v1

   [BOTTOM_UP_MERGEALL_MAP_lemma]  Theorem

      ⊢ ∀R xss.
          transitive R ∧ total R ⇒
          (SORTED R (bottom_up_mergeall R xss) ⇔ EVERY (SORTED R) xss)

   [BOTTOM_UP_MERGEALL_def]  Theorem

      ⊢ (∀R. bottom_up_mergeall R [] = []) ∧
        (∀xs R. bottom_up_mergeall R [xs] = xs) ∧
        ∀v7 v6 v2 R.
          bottom_up_mergeall R (v2::v6::v7) =
          bottom_up_mergeall R (bottom_up_mergeadjacent R (v2::v6::v7))

   [BOTTOM_UP_MERGEALL_ind]  Theorem

      ⊢ ∀P. (∀R. P R []) ∧ (∀R xs. P R [xs]) ∧
            (∀R v2 v6 v7.
               P R (bottom_up_mergeadjacent R (v2::v6::v7)) ⇒
               P R (v2::v6::v7)) ⇒
            ∀v v1. P v v1

   [BOTTOM_UP_MERGEAUXILLARY_def]  Theorem

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

   [BOTTOM_UP_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

   [CORRECTNESS_MSET_BOTTOM_UP_MERGESORT_thm]  Theorem

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

   [CORRECTNESS_SORTED_BOTTOM_UP_MERGESORT_thm]  Theorem

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

   [MEM_BOTTOM_UP_MERGEAUXILLARY_lemma]  Theorem

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

   [MSET_BOTTOM_UP_MERGEADJACENT_lemma]  Theorem

      ⊢ ∀R xss.
          LIST_TO_BAG (FLAT (bottom_up_mergeadjacent R xss)) =
          LIST_TO_BAG (FLAT xss)

   [MSET_BOTTOM_UP_MERGEALL_lemma]  Theorem

      ⊢ ∀R xss.
          LIST_TO_BAG (bottom_up_mergeall R xss) = LIST_TO_BAG (FLAT xss)

   [MSET_BOTTOM_UP_MERGEAUXILLARY_lemma]  Theorem

      ⊢ ∀R l1 l2.
          LIST_TO_BAG (bottom_up_mergeauxillary R l1 l2) =
          LIST_TO_BAG l1 ⊎ LIST_TO_BAG l2

   [SORTED_BOTTOM_UP_MERGEADJACENT_lemma]  Theorem

      ⊢ ∀R xss.
          transitive R ∧ total R ⇒
          (EVERY (SORTED R) (bottom_up_mergeadjacent R xss) ⇔
           EVERY (SORTED R) xss)

   [SORTED_BOTTOM_UP_MERGEAUXILLARY_lemma]  Theorem

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


*)
end