Structure transferTheory

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

HOL 4, Kananaskis-13