1open HolKernel Parse boolLib bossLib;
2
3val _ = new_theory "NDSupport";
4
5val J_def = Define`J = \x (u:one). NONE`;
6val KT_def = Define`KT = \x. T`;
7
8val    fun_map_def = Define`   fun_map = combin$o         `;
9val    sum_map_def = Define`   sum_map =    sum$++        `;
10val   prod_map_def = Define`  prod_map =   pair$##        `;
11val   list_map_def = Define`  list_map =   list$MAP       `;
12val option_map_def = Define`option_map = option$OPTION_MAP`;
13
14val list_retrieve_def = Define`
15   (list_retrieve f [    ]          _ = NONE                    )
16/\ (list_retrieve f (h::_) (    0, c) = f h c                   )
17/\ (list_retrieve f (h::t) (SUC n, c) = list_retrieve f t (n, c))
18`;
19
20val sum_retrieve_def = Define`
21   (sum_retrieve f1 _ (INL a1) (b1, _) = f1 a1 b1)
22/\ (sum_retrieve _ f2 (INR a2) (_, b2) = f2 a2 b2)`;
23
24val prod_retrieve_def = Define`
25   (prod_retrieve f1 _ (a1, _) (INL b1) = f1 a1 b1)
26/\ (prod_retrieve _ f2 (_, a2) (INR b2) = f2 a2 b2)`;
27
28val fun_retrieve_def = Define`
29    fun_retrieve f g (a, b) = f (g a) b`;
30(*  fun_retrieve = $o ($o UNCURRY) $o *)
31
32val option_retrieve_def = Define`
33   (option_retrieve f  NONE    _ = NONE )
34/\ (option_retrieve f (SOME c) p = f c p)
35`;
36
37
38
39val INJ_def = Define`INJ f = !x y. (f x = f y) ==> (x = y)`;
40
41val inj_pair_def = Define`
42    inj_pair f g = !x y. (f x = f y) /\ (!z. g x z = g y z) ==> (x = y)
43`;
44
45val sum_all_def = Define`
46   (sum_all P Q (INL x) = P x)
47/\ (sum_all P Q (INR y) = Q y)`;
48
49val prod_all_def = Define`
50    prod_all P Q (x,y) = P x /\ Q y`;
51
52(* list_all = EVERY *)
53val list_all_def = Define`
54   (list_all P [    ] = T)
55/\ (list_all P (h::t) = P h /\ list_all P t)`;
56
57val option_all_def = Define`
58   (option_all P  NONE    = T  )
59/\ (option_all P (SOME x) = P x)`;
60
61val fun_all_def = Define`
62    fun_all P f = !x. P (f x)
63`;
64
65val _ = export_theory();
66
67