1open HolKernel Parse boolLib bossLib;
2
3val _ = new_theory "transfer";
4
5(* uniqueness, which might also be termed injectivity *)
6val right_unique_def = Define���
7  right_unique (R : 'a -> 'b -> bool) <=>
8    !a b1 b2. R a b1 /\ R a b2 ==> (b1 = b2)���;
9
10val left_unique_def = Define���
11  left_unique (R: 'a -> 'b -> bool) <=>
12    !a1 a2 b. R a1 b /\ R a2 b ==> (a1 = a2)���;
13
14val bi_unique_def = Define���bi_unique R <=> left_unique R /\ right_unique R���;
15
16(* totality or surjectivity *)
17val total_def = Define���total (R : 'a -> 'b -> bool) <=> !x:'a. ?y. R x y���;
18val surj_def = Define���surj (R : 'a -> 'b -> bool) <=> !y:'b. ?x. R x y���;
19val bitotal_def = Define���bitotal (R : 'a -> 'b -> bool) <=> total R /\ surj R���;
20
21val _ =
22    set_mapped_fixity {fixity = Infixr 490, term_name = "FUN_REL", tok = "===>"}
23
24val FUN_REL_def = Define���
25  (AB ===> CD) (f : 'a -> 'c) (g : 'b -> 'd) <=>
26    !a:'a b:'b. AB a b ==> CD (f a) (g b)
27���;
28
29val FUN_REL_COMB = Q.store_thm(
30  "FUN_REL_COMB",
31  ���(AB ===> CD) f g /\ AB a b ==> CD (f a) (g b)���,
32  simp[FUN_REL_def]);
33
34val FUN_REL_ABS = Q.store_thm(
35  "FUN_REL_ABS",
36  ���(!a b. AB a b ==> CD (f a) (g b)) ==>
37   (AB ===> CD) (\a. f a) (\b. g b)���,
38  simp[FUN_REL_def]);
39
40val FUN_REL_EQ2 = Q.store_thm(
41  "FUN_REL_EQ2[simp]",
42  ���((=) ===> (=)) = (=)���,
43  simp[FUN_REL_def, FUN_EQ_THM]);
44
45val PAIR_REL_def = Define���PAIR_REL AB CD (a,c) (b,d) <=> AB a b /\ CD c d���;
46val _ =
47    set_mapped_fixity {fixity = Infixr 601, term_name = "PAIR_REL", tok = "###"}
48
49val _ = export_theory();
50