blob: 08288d15ecf55ccf96f7bb8e5bbaf79492a5f2e5 (
plain)
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
|
(*Generated by Lem from sorting.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_boolTheory lem_basic_classesTheory lem_maybeTheory lem_listTheory lem_numTheory sortingTheory permLib;
val _ = numLib.prefer_num();
val _ = new_theory "lem_sorting"
(*open import Bool Basic_classes Maybe List Num*)
(*open import {isabelle} `~~/src/HOL/Library/Permutation`*)
(*open import {coq} `Coq.Lists.List`*)
(*open import {hol} `sortingTheory` `permLib`*)
(*open import {isabelle} `$LIB_DIR/Lem`*)
(* ------------------------- *)
(* permutations *)
(* ------------------------- *)
(*val isPermutation : forall 'a. Eq 'a => list 'a -> list 'a -> bool*)
(*val isPermutationBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*)
val _ = Define `
((PERM_BY:('a -> 'a -> bool) -> 'a list -> 'a list -> bool) eq ([]) l2= (NULL l2))
/\ ((PERM_BY:('a -> 'a -> bool) -> 'a list -> 'a list -> bool) eq (x :: xs) l2= ((
(case list_delete_first (eq x) l2 of
NONE => F
| SOME ys => PERM_BY eq xs ys
)
)))`;
(* ------------------------- *)
(* isSorted *)
(* ------------------------- *)
(* isSortedBy R l
checks, whether the list l is sorted by ordering R.
R should represent an order, i.e. it should be transitive.
Different backends defined "isSorted" slightly differently. However,
the definitions coincide for transitive R. Therefore there is the
following restriction:
WARNING: Use isSorted and isSortedBy only with transitive relations!
*)
(*val isSorted : forall 'a. Ord 'a => list 'a -> bool*)
(*val isSortedBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> bool*)
(* DPM: rejigged the definition with a nested match to get past Coq's termination checker. *)
(*let rec isSortedBy cmp l= match l with
| [] -> true
| x1 :: xs ->
match xs with
| [] -> true
| x2 :: _ -> (cmp x1 x2 && isSortedBy cmp xs)
end
end*)
(* ----------------------- *)
(* insertion sort *)
(* ----------------------- *)
(*val insert : forall 'a. Ord 'a => 'a -> list 'a -> list 'a*)
(*val insertBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> list 'a*)
(*val insertSort: forall 'a. Ord 'a => list 'a -> list 'a*)
(*val insertSortBy: forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a*)
val _ = Define `
((INSERT_SORT_INSERT:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list) cmp e ([])= ([e]))
/\ ((INSERT_SORT_INSERT:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list) cmp e (x :: xs)= (if cmp x e then x :: (INSERT_SORT_INSERT cmp e xs) else (e :: (x :: xs))))`;
val _ = Define `
((INSERT_SORT:('a -> 'a -> bool) -> 'a list -> 'a list) cmp l= (FOLDL (\ l e . INSERT_SORT_INSERT cmp e l) [] l))`;
(* ----------------------- *)
(* general sorting *)
(* ----------------------- *)
(*val sort: forall 'a. Ord 'a => list 'a -> list 'a*)
(*val sortBy: forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a*)
(*val sortByOrd: forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a*)
(*val predicate_of_ord : forall 'a. ('a -> 'a -> ordering) -> 'a -> 'a -> bool*)
val _ = Define `
((predicate_of_ord:('a -> 'a -> ordering) -> 'a -> 'a -> bool) f x y=
((case f x y of
LESS => T
| EQUAL => T
| GREATER => F
)))`;
val _ = export_theory()
|
