blob: 48032c8ee7e3024ac2b0324a92dbf9e77e5ef1bc (
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
108
109
110
|
chapter \<open>Generated by Lem from \<open>sorting.lem\<close>.\<close>
theory "Lem_sorting"
imports
Main
"Lem_bool"
"Lem_basic_classes"
"Lem_maybe"
"Lem_list"
"Lem_num"
"Lem"
"HOL-Library.Permutation"
begin
(*open import Bool Basic_classes Maybe List Num*)
(*open import {isabelle} `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*)
fun isPermutationBy :: "('a \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool " where
" isPermutationBy eq ([]) l2 = ( (l2 = []))"
|" isPermutationBy eq (x # xs) l2 = ( (
(case delete_first (eq x) l2 of
None => False
| Some ys => isPermutationBy 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*)
(*let rec insertBy cmp e l= match l with
| [] -> [e]
| x :: xs -> if cmp x e then x :: (insertBy cmp e xs) else (e :: x :: xs)
end*)
(*let insertSortBy cmp l= List.foldl (fun l e -> insertBy 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*)
definition predicate_of_ord :: "('a \<Rightarrow> 'a \<Rightarrow> ordering)\<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool " where
" predicate_of_ord f x y = (
(case f x y of
LT => True
| EQ => True
| GT => False
))"
end
|
