Structure transferTheory

Source File	Identifier index	Theory binding index
signature transferTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val FUN_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_DISTINCT_rule : thm
    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 COND_rule : thm
    val CONS_rule : 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 FOLDL_rule : thm
    val FOLDR_rule : thm
    val FST_CORRECT : thm
    val FUNPOW_rule : thm
    val FUN_REL_COMB : thm
    val FUN_REL_EQ2 : thm
    val FUN_REL_IFF_IMP : thm
    val LENGTH_rule : thm
    val LET_rule : thm
    val LIST_REL_left_unique : thm
    val LIST_REL_right_unique : thm
    val LIST_REL_surj : thm
    val LIST_REL_total : thm
    val MAP_rule : thm
    val NIL_rule : thm
    val NONE_rule : thm
    val OPTION_BIND_rule : thm
    val OPTREL_MAP : thm
    val OPTREL_left_unique : thm
    val OPTREL_right_unique : thm
    val OPTREL_surj : thm
    val OPTREL_total : thm
    val PAIRU_COMMA : thm
    val PAIRU_def : thm
    val PAIRU_ind : thm
    val PAIR_REL_def : thm
    val RDOM_EQ : thm
    val RRANGE_EQ : thm
    val SND_CORRECT : thm
    val SOME_rule : thm
    val TL_rule : 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 list_CASE_CONG : thm
    val option_CASE_CONG : thm
    val pair_CASE_CONG : 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)
   
   [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_DISTINCT_rule]  Theorem
      
      ⊢ left_unique AB ⇒
        right_unique AB ⇒
        (LIST_REL AB |==> $<=>) ALL_DISTINCT ALL_DISTINCT
   
   [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) $, $,
   
   [COND_rule]  Theorem
      
      ⊢ ($<=> |==> AB |==> AB |==> AB) COND COND
   
   [CONS_rule]  Theorem
      
      ⊢ (AB |==> LIST_REL AB |==> LIST_REL AB) CONS CONS
   
   [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 |==> $==>) |==> $==>) $? $?
   
   [FOLDL_rule]  Theorem
      
      ⊢ ((CD |==> AB |==> CD) |==> CD |==> LIST_REL AB |==> CD) FOLDL FOLDL
   
   [FOLDR_rule]  Theorem
      
      ⊢ ((AB |==> CD |==> CD) |==> CD |==> LIST_REL AB |==> CD) FOLDR FOLDR
   
   [FST_CORRECT]  Theorem
      
      ⊢ ((AB ### CD) |==> AB) FST FST
   
   [FUNPOW_rule]  Theorem
      
      ⊢ ((AB |==> AB) |==> $= |==> AB |==> AB) FUNPOW FUNPOW
   
   [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
   
   [LENGTH_rule]  Theorem
      
      ⊢ (LIST_REL AB |==> $=) LENGTH LENGTH
   
   [LET_rule]  Theorem
      
      ⊢ ((AB |==> CD) |==> AB |==> CD) LET LET
   
   [LIST_REL_left_unique]  Theorem
      
      ⊢ left_unique AB ⇒ left_unique (LIST_REL AB)
   
   [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)
   
   [MAP_rule]  Theorem
      
      ⊢ ((AB |==> CD) |==> LIST_REL AB |==> LIST_REL CD) MAP MAP
   
   [NIL_rule]  Theorem
      
      ⊢ LIST_REL AB [] []
   
   [NONE_rule]  Theorem
      
      ⊢ OPTREL AB NONE NONE
   
   [OPTION_BIND_rule]  Theorem
      
      ⊢ (OPTREL AB |==> (AB |==> OPTREL CD) |==> OPTREL CD) OPTION_BIND
          OPTION_BIND
   
   [OPTREL_MAP]  Theorem
      
      ⊢ ((AB |==> CD) |==> OPTREL AB |==> OPTREL CD) OPTION_MAP OPTION_MAP
   
   [OPTREL_left_unique]  Theorem
      
      ⊢ left_unique AB ⇒ left_unique (OPTREL AB)
   
   [OPTREL_right_unique]  Theorem
      
      ⊢ right_unique AB ⇒ right_unique (OPTREL AB)
   
   [OPTREL_surj]  Theorem
      
      ⊢ surj AB ⇒ surj (OPTREL AB)
   
   [OPTREL_total]  Theorem
      
      ⊢ total AB ⇒ total (OPTREL 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
   
   [PAIR_REL_def]  Theorem
      
      ⊢ ∀R1 R2. R1 ### R2 = (λ(s,t) (u,v). R1 s u ∧ R2 t v)
   
   [RDOM_EQ]  Theorem
      
      ⊢ RDOM $= = K T
   
   [RRANGE_EQ]  Theorem
      
      ⊢ RRANGE $= = K T
   
   [SND_CORRECT]  Theorem
      
      ⊢ ((AB ### CD) |==> CD) SND SND
   
   [SOME_rule]  Theorem
      
      ⊢ (AB |==> OPTREL AB) SOME SOME
   
   [TL_rule]  Theorem
      
      ⊢ (LIST_REL AB |==> LIST_REL AB) TL TL
   
   [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 $=
   
   [list_CASE_CONG]  Theorem
      
      ⊢ (LIST_REL AB |==> CD |==> (AB |==> LIST_REL AB |==> CD) |==> CD)
          list_CASE list_CASE
   
   [option_CASE_CONG]  Theorem
      
      ⊢ (OPTREL AB |==> CD |==> (AB |==> CD) |==> CD) option_CASE
          option_CASE
   
   [pair_CASE_CONG]  Theorem
      
      ⊢ ((AB ### CD) |==> (AB |==> CD |==> EF) |==> EF) pair_CASE pair_CASE
   
   [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, Trindemossen-1