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