# Structure transferTheory

Source File Identifier index Theory binding index

```signature transferTheory =
sig
type thm = Thm.thm

(*  Definitions  *)
val FUN_REL_def : thm
val PAIR_REL_def : thm
val bi_unique_def : thm
val bitotal_def : thm
val left_unique_def : thm
val right_unique_def : thm
val surj_def : thm
val total_def : thm

(*  Theorems  *)
val FUN_REL_ABS : thm
val FUN_REL_COMB : thm
val FUN_REL_EQ2 : thm

val transfer_grammars : type_grammar.grammar * term_grammar.grammar
(*
[indexedLists] Parent theory of "transfer"

[patternMatches] Parent theory of "transfer"

[FUN_REL_def]  Definition

⊢ ∀AB CD f g. (AB ===> CD) f g ⇔ ∀a b. AB a b ⇒ CD (f a) (g b)

[PAIR_REL_def]  Definition

⊢ ∀AB CD a c b d. (AB ### CD) (a,c) (b,d) ⇔ AB a b ∧ CD c d

[bi_unique_def]  Definition

⊢ ∀R. bi_unique R ⇔ left_unique R ∧ right_unique R

[bitotal_def]  Definition

⊢ ∀R. bitotal R ⇔ total R ∧ surj R

[left_unique_def]  Definition

⊢ ∀R. left_unique R ⇔ ∀a1 a2 b. R a1 b ∧ R a2 b ⇒ (a1 = a2)

[right_unique_def]  Definition

⊢ ∀R. right_unique R ⇔ ∀a b1 b2. R a b1 ∧ R a b2 ⇒ (b1 = b2)

[surj_def]  Definition

⊢ ∀R. surj R ⇔ ∀y. ∃x. R x y

[total_def]  Definition

⊢ ∀R. total R ⇔ ∀x. ∃y. R x y

[FUN_REL_ABS]  Theorem

⊢ (∀a b. AB a b ⇒ CD (f a) (g b)) ⇒ (AB ===> CD) (λa. f a) (λb. g b)

[FUN_REL_COMB]  Theorem

⊢ (AB ===> CD) f g ∧ AB a b ⇒ CD (f a) (g b)

[FUN_REL_EQ2]  Theorem

⊢ \$= ===> \$= = \$=

*)
end

```

Source File Identifier index Theory binding index