1open HolKernel Parse boolLib bossLib;
2
3open stringTheory
4
5val _ = new_theory "ternaryComparisons";
6
7val _ = Datatype `ordering = LESS | EQUAL | GREATER`;
8
9fun type_rws ty = #rewrs (TypeBase.simpls_of ty)
10
11val thms =
12  LIST_CONJ
13    (INST_TYPE[Type.alpha |-> ``:ordering``] REFL_CLAUSE
14     :: tl (type_rws ``:ordering``));
15
16val ordering_eq_dec = save_thm("ordering_eq_dec",
17  PURE_REWRITE_RULE[GSYM (hd (rev (CONJUNCTS (SPEC_ALL EQ_CLAUSES))))] thms);
18
19val bool_compare_def = Define `
20  (bool_compare T T = EQUAL) /\
21  (bool_compare F F = EQUAL) /\
22  (bool_compare T F = GREATER) /\
23  (bool_compare F T = LESS)
24`;
25val _ = export_rewrites ["bool_compare_def"]
26
27(* Lifting comparison functions through various type operators *)
28val pair_compare_def = Define`
29  pair_compare c1 c2 (a,b) (x,y) =
30     case c1 a x of
31        EQUAL => c2 b y
32      | res => res
33`;
34
35val option_compare_def = Define`
36  (option_compare c NONE NONE = EQUAL) /\
37  (option_compare c NONE (SOME _) = LESS) /\
38  (option_compare c (SOME _) NONE = GREATER) /\
39  (option_compare c (SOME v1) (SOME v2) = c v1 v2)
40`;
41val _ = export_rewrites ["option_compare_def"]
42
43val num_compare_def = Define `
44  num_compare n1 n2 =
45    if n1 = n2 then
46      EQUAL
47    else if n1 < n2 then
48      LESS
49    else
50      GREATER
51`;
52
53val char_compare_def = Define `
54  char_compare c1 c2 = num_compare (ORD c1) (ORD c2)
55`;
56
57
58
59
60(* General results on lists *)
61val list_compare_def = Define `
62   (list_compare cmp [] [] = EQUAL)
63/\ (list_compare cmp [] l2 = LESS)
64/\ (list_compare cmp l1 [] = GREATER)
65/\ (list_compare cmp (x::l1) (y::l2) =
66     case cmp (x:'a) y of
67       LESS => LESS
68     | EQUAL => list_compare cmp l1 l2
69     | GREATER => GREATER) `;
70
71val string_compare_def = Define `
72  string_compare = list_compare char_compare
73`;
74
75val compare_equal = store_thm("compare_equal",
76  ���(!x y. (cmp x y = EQUAL) = (x = y)) ==>
77   !l1 l2. (list_compare cmp l1 l2 = EQUAL) = (l1 = l2)���,
78 DISCH_THEN (ASSUME_TAC o GSYM)
79   THEN NTAC 2 (Induct THENL [ALL_TAC,GEN_TAC])
80   THEN TRY (ASM_REWRITE_TAC[] THEN Cases_on `cmp h h'`)
81   THEN RW_TAC bool_ss [list_compare_def]);
82
83(* looks out of place *)
84val list_merge_def = Define `
85   (list_merge a_lt l1 [] = l1)
86/\ (list_merge a_lt [] l2 = l2)
87/\ (list_merge a_lt (x:'a :: l1) (y::l2) =
88      if a_lt x y
89      then x::list_merge a_lt l1 (y::l2)
90      else y::list_merge a_lt (x::l1) l2) `;
91
92val invert_comparison_def = Define`
93  (invert_comparison GREATER = LESS) /\
94  (invert_comparison LESS = GREATER) /\
95  (invert_comparison EQUAL = EQUAL)`
96val _ = export_rewrites["invert_comparison_def"]
97
98val invert_eq_EQUAL = store_thm("invert_eq_EQUAL[simp]",
99  ``!x. (invert_comparison x = EQUAL) <=> (x = EQUAL)``,
100  Cases >> simp[])
101
102
103
104val _ = export_theory();
105