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 equalityp_def : thm
    val left_unique_def : thm
    val right_unique_def : thm
    val surj_def : thm
    val total_def : thm
  
  (*  Theorems  *)
    val ALL_IFF : thm
    val ALL_surj_RDOM : thm
    val ALL_surj_iff_imp : thm
    val ALL_surj_imp_imp : thm
    val ALL_total_RRANGE : thm
    val ALL_total_cimp_cimp : thm
    val ALL_total_iff_cimp : thm
    val COMMA_CORRECT : thm
    val EQ_bi_unique : thm
    val EXISTS_IFF_RDOM : thm
    val EXISTS_IFF_RRANGE : thm
    val EXISTS_bitotal : thm
    val EXISTS_surj_cimp_cimp : thm
    val EXISTS_surj_iff_cimp : thm
    val EXISTS_total_iff_imp : thm
    val EXISTS_total_imp_imp : thm
    val FST_CORRECT : thm
    val FUN_REL_COMB : thm
    val FUN_REL_EQ2 : thm
    val FUN_REL_IFF_IMP : thm
    val LIST_REL_right_unique : thm
    val LIST_REL_surj : thm
    val LIST_REL_total : thm
    val PAIRU_COMMA : thm
    val PAIRU_def : thm
    val PAIRU_ind : thm
    val RDOM_EQ : thm
    val RRANGE_EQ : thm
    val SND_CORRECT : thm
    val UPAIR_COMMA : thm
    val UPAIR_def : thm
    val UPAIR_ind : thm
    val UREL_EQ : thm
    val bi_unique_EQ : thm
    val bi_unique_implied : thm
    val bitotal_EQ : thm
    val bitotal_implied : thm
    val cimp_disj : thm
    val cimp_imp : thm
    val eq_equalityp : thm
    val eq_imp : thm
    val equalityp_FUN_REL : thm
    val equalityp_LIST_REL : thm
    val equalityp_PAIR_REL : thm
    val equalityp_applied : thm
    val imp_conj : thm
    val imp_disj : thm
    val left_unique_EQ : thm
    val right_unique_EQ : thm
    val surj_EQ : thm
    val surj_sets : thm
    val total_EQ : thm
    val total_total_sets : 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
   
   [equalityp_def]  Definition
      
      ⊢ ∀A. equalityp A ⇔ A = $=
   
   [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
   
   [ALL_IFF]  Theorem
      
      ⊢ bitotal AB ⇒ ((AB |==> $<=>) |==> $<=>) $! $!
   
   [ALL_surj_RDOM]  Theorem
      
      ⊢ surj AB ⇒ ((AB |==> $<=>) |==> $<=>) (RES_FORALL (RDOM AB)) $!
   
   [ALL_surj_iff_imp]  Theorem
      
      ⊢ surj AB ⇒ ((AB |==> $<=>) |==> $==>) $! $!
   
   [ALL_surj_imp_imp]  Theorem
      
      ⊢ surj AB ⇒ ((AB |==> $==>) |==> $==>) $! $!
   
   [ALL_total_RRANGE]  Theorem
      
      ⊢ total AB ⇒ ((AB |==> $<=>) |==> $<=>) $! (RES_FORALL (RRANGE AB))
   
   [ALL_total_cimp_cimp]  Theorem
      
      ⊢ total AB ⇒ ((AB |==> flip $==>) |==> flip $==>) $! $!
   
   [ALL_total_iff_cimp]  Theorem
      
      ⊢ total AB ⇒ ((AB |==> $<=>) |==> flip $==>) $! $!
   
   [COMMA_CORRECT]  Theorem
      
      ⊢ (AB |==> CD |==> AB ### CD) $, $,
   
   [EQ_bi_unique]  Theorem
      
      ⊢ bi_unique AB ⇒ (AB |==> AB |==> $<=>) $= $=
   
   [EXISTS_IFF_RDOM]  Theorem
      
      ⊢ surj AB ⇒ ((AB |==> $<=>) |==> $<=>) (RES_EXISTS (RDOM AB)) $?
   
   [EXISTS_IFF_RRANGE]  Theorem
      
      ⊢ total AB ⇒ ((AB |==> $<=>) |==> $<=>) $? (RES_EXISTS (RRANGE AB))
   
   [EXISTS_bitotal]  Theorem
      
      ⊢ bitotal AB ⇒ ((AB |==> $<=>) |==> $<=>) $? $?
   
   [EXISTS_surj_cimp_cimp]  Theorem
      
      ⊢ surj AB ⇒ ((AB |==> flip $==>) |==> flip $==>) $? $?
   
   [EXISTS_surj_iff_cimp]  Theorem
      
      ⊢ surj AB ⇒ ((AB |==> $<=>) |==> flip $==>) $? $?
   
   [EXISTS_total_iff_imp]  Theorem
      
      ⊢ total AB ⇒ ((AB |==> $<=>) |==> $==>) $? $?
   
   [EXISTS_total_imp_imp]  Theorem
      
      ⊢ total AB ⇒ ((AB |==> $==>) |==> $==>) $? $?
   
   [FST_CORRECT]  Theorem
      
      ⊢ (AB ### CD |==> AB) FST FST
   
   [FUN_REL_COMB]  Theorem
      
      ⊢ (AB |==> CD) f g ∧ AB a b ⇒ CD (f a) (g b)
   
   [FUN_REL_EQ2]  Theorem
      
      ⊢ $= |==> $= = $=
   
   [FUN_REL_IFF_IMP]  Theorem
      
      ⊢ (AB |==> $<=>) P Q ⇒ (AB |==> $==>) P Q ∧ (AB |==> flip $==>) P Q
   
   [LIST_REL_right_unique]  Theorem
      
      ⊢ right_unique AB ⇒ right_unique (LIST_REL AB)
   
   [LIST_REL_surj]  Theorem
      
      ⊢ surj AB ⇒ surj (LIST_REL AB)
   
   [LIST_REL_total]  Theorem
      
      ⊢ total AB ⇒ total (LIST_REL AB)
   
   [PAIRU_COMMA]  Theorem
      
      ⊢ (AB |==> $= |==> PAIRU AB) $, K
   
   [PAIRU_def]  Theorem
      
      ⊢ PAIRU AB (a,()) b = AB a b
   
   [PAIRU_ind]  Theorem
      
      ⊢ ∀P. (∀AB a b. P AB (a,()) b) ⇒ ∀v v1 v2 v3. P v (v1,v2) v3
   
   [RDOM_EQ]  Theorem
      
      ⊢ RDOM $= = K T
   
   [RRANGE_EQ]  Theorem
      
      ⊢ RRANGE $= = K T
   
   [SND_CORRECT]  Theorem
      
      ⊢ (AB ### CD |==> CD) SND SND
   
   [UPAIR_COMMA]  Theorem
      
      ⊢ ($= |==> AB |==> UPAIR AB) $, (K I)
   
   [UPAIR_def]  Theorem
      
      ⊢ UPAIR AB ((),a) b = AB a b
   
   [UPAIR_ind]  Theorem
      
      ⊢ ∀P. (∀AB a b. P AB ((),a) b) ⇒ ∀v v1 v2 v3. P v (v1,v2) v3
   
   [UREL_EQ]  Theorem
      
      ⊢ () = ()
   
   [bi_unique_EQ]  Theorem
      
      ⊢ bi_unique $=
   
   [bi_unique_implied]  Theorem
      
      ⊢ left_unique r ∧ right_unique r ⇒ bi_unique r
   
   [bitotal_EQ]  Theorem
      
      ⊢ bitotal $=
   
   [bitotal_implied]  Theorem
      
      ⊢ total r ∧ surj r ⇒ bitotal r
   
   [cimp_disj]  Theorem
      
      ⊢ (flip $==> |==> flip $==> |==> flip $==>) $\/ $\/
   
   [cimp_imp]  Theorem
      
      ⊢ ($==> |==> flip $==> |==> flip $==>) $==> $==>
   
   [eq_equalityp]  Theorem
      
      ⊢ equalityp $=
   
   [eq_imp]  Theorem
      
      ⊢ ($<=> |==> $<=> |==> $<=>) $==> $==>
   
   [equalityp_FUN_REL]  Theorem
      
      ⊢ equalityp AB ∧ equalityp CD ⇒ equalityp (AB |==> CD)
   
   [equalityp_LIST_REL]  Theorem
      
      ⊢ equalityp AB ⇒ equalityp (LIST_REL AB)
   
   [equalityp_PAIR_REL]  Theorem
      
      ⊢ equalityp AB ∧ equalityp CD ⇒ equalityp (AB ### CD)
   
   [equalityp_applied]  Theorem
      
      ⊢ equalityp A ⇒ A x x
   
   [imp_conj]  Theorem
      
      ⊢ ($==> |==> $==> |==> $==>) $/\ $/\
   
   [imp_disj]  Theorem
      
      ⊢ ($==> |==> $==> |==> $==>) $\/ $\/
   
   [left_unique_EQ]  Theorem
      
      ⊢ left_unique $=
   
   [right_unique_EQ]  Theorem
      
      ⊢ right_unique $=
   
   [surj_EQ]  Theorem
      
      ⊢ surj $=
   
   [surj_sets]  Theorem
      
      ⊢ surj AB ∧ right_unique AB ⇒ surj (AB |==> $<=>)
   
   [total_EQ]  Theorem
      
      ⊢ total $=
   
   [total_total_sets]  Theorem
      
      ⊢ total AB ∧ left_unique AB ⇒ total (AB |==> $<=>)
   
   
*)
end
Source File	Identifier index	Theory binding index
HOL 4, Kananaskis-14