1(* non-interactive mode 2*) 3open HolKernel Parse boolLib; 4val _ = new_theory "order"; 5 6(* interactive mode 7val () = loadPath := union ["..", "../finished"] (!loadPath); 8val () = app load 9 ["bossLib", 10 "pred_setTheory", 11 "realLib", 12 "pairTheory", 13 "combinTheory", 14 "res_quanLib", 15 "dividesTheory", 16 "primeTheory", 17 "gcdTheory", 18 "prob_extraTools", 19 "millerTools"]; 20val () = show_assums := true; 21*) 22 23open bossLib listTheory subtypeTools res_quanTools res_quanTheory 24 pred_setTheory extra_pred_setTheory listContext relationTheory 25 ho_proverTools subtypeTheory HurdUseful; 26 27infixr 0 ++ << || THENC ORELSEC ORELSER ##; 28infix 1 >>; 29 30val op!! = op REPEAT; 31val op++ = op THEN; 32val op<< = op THENL; 33val op|| = op ORELSE; 34val op>> = op THEN1; 35 36(* ------------------------------------------------------------------------- *) 37(* Tools. *) 38(* ------------------------------------------------------------------------- *) 39 40val S_TAC = !! (POP_ASSUM MP_TAC) ++ !! RESQ_STRIP_TAC; 41 42val (R_TAC, AR_TAC, R_TAC', AR_TAC') = SIMPLIFY_TACS list_c; 43 44(* ------------------------------------------------------------------------- *) 45(* Definitions. *) 46(* ------------------------------------------------------------------------- *) 47 48val reflexive_def = Define `reflexive f = !x. f x x`; 49 50val antisym_def = Define `antisym f = !x y. f x y /\ f y x ==> (x = y)`; 51 52val total_def = Define `total f = !x y. f x y \/ f y x`; 53 54val preorder_def = Define `preorder f = reflexive f /\ transitive f`; 55 56val partialorder_def = Define `partialorder f = preorder f /\ antisym f`; 57 58val totalorder_def = Define `totalorder f = partialorder f /\ total f`; 59 60val sorted_def = Define 61 `(sorted f [] = T) /\ 62 (sorted f [h] = T) /\ 63 (sorted f (h1 :: h2 :: t) = f h1 h2 /\ sorted f (h2 :: t))`; 64 65val insert_def = Define 66 `(insert f a [] = [a]) /\ 67 (insert f a (h :: t) = if f a h then a :: h :: t else h :: insert f a t)`; 68 69(* ------------------------------------------------------------------------- *) 70(* Theorems. *) 71(* ------------------------------------------------------------------------- *) 72 73val INSERT_SORTED = store_thm 74 ("INSERT_SORTED", 75 ``!f a l. totalorder f ==> (sorted f (insert f a l) = sorted f l)``, 76 S_TAC 77 ++ AR_TAC [totalorder_def, partialorder_def, preorder_def, 78 reflexive_def, transitive_def, total_def] 79 ++ Cases_on `sorted f l` << 80 [R_TAC [] 81 ++ Cases_on `l` >> R_TAC [sorted_def, insert_def] 82 ++ R_TAC [insert_def] 83 ++ POP_ASSUM MP_TAC 84 ++ Q.SPEC_TAC (`h`, `x`) 85 ++ Induct_on `t` 86 >> (S_TAC 87 ++ Cases_on `f a x` 88 ++ AR_TAC [sorted_def, insert_def] 89 ++ ho_PROVE_TAC []) 90 ++ S_TAC 91 ++ Cases_on `f a x` >> AR_TAC [sorted_def] 92 ++ Q.PAT_X_ASSUM `!x. P x ==> Q x` (MP_TAC o Q.SPEC `h`) 93 ++ Q.PAT_X_ASSUM `sorted f (x::h::t)` MP_TAC 94 ++ R_TAC [sorted_def, insert_def] 95 ++ Cases_on `f a h` 96 ++ R_TAC [sorted_def] 97 ++ ho_PROVE_TAC [], 98 R_TAC [] 99 ++ Cases_on `l` >> AR_TAC [sorted_def, insert_def] 100 ++ POP_ASSUM MP_TAC 101 ++ Q.SPEC_TAC (`h`, `x`) 102 ++ Induct_on `t` >> R_TAC [sorted_def] 103 ++ S_TAC 104 ++ Q.PAT_X_ASSUM `!x. P x ==> Q x` (MP_TAC o Q.SPEC `h`) 105 ++ NTAC 2 (POP_ASSUM MP_TAC) 106 ++ R_TAC [sorted_def, insert_def] 107 ++ Cases_on `f a x` 108 ++ Cases_on `f a h` 109 ++ R_TAC [sorted_def] 110 ++ ho_PROVE_TAC []]); 111 112(* non-interactive mode 113*) 114val _ = export_theory (); 115