ternaryComparisonsScript.sml

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