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