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