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