Theory "lifting"

Parents transfer

Signature

Constant	Type
Qt	:(α -> α -> bool) -> (α -> β) -> (β -> α) -> (α -> β -> bool) -> bool
map_fun	:(α -> γ) -> (δ -> β) -> (γ -> δ) -> α -> β

Definitions

Qt_def

⊢ ∀R Abs Rep Tf.
    Qt R Abs Rep Tf ⇔
    (R = Tfᵀ ∘ᵣ Tf) ∧ (∀a b. Tf a b ⇒ (Abs a = b)) ∧ ∀a. Tf (Rep a) a

map_fun_def

⊢ ∀f g h. (f ---> g) h = g ∘ h ∘ f

Theorems

HK_thm2

⊢ Qt R Abs Rep Tf ∧ (f = Abs t) ∧ R t t ⇒ Tf t f

Qt_EQ

⊢ Qt R Abs Rep Tf ⇒ (Tf |==> Tf |==> $<=>) R $=

Qt_alt

⊢ Qt R Abs Rep Tf ⇔
  (∀a. Abs (Rep a) = a) ∧ (∀a. R (Rep a) (Rep a)) ∧
  (∀c1 c2. R c1 c2 ⇔ R c1 c1 ∧ R c2 c2 ∧ (Abs c1 = Abs c2)) ∧
  (Tf = (λc a. R c c ∧ (Abs c = a)))

Qt_alt_def2

⊢ Qt R Abs Rep Tf ⇔
  (∀c a. Tf c a ⇒ (Abs c = a)) ∧ (∀a. Tf (Rep a) a) ∧
  ∀c1 c2. R c1 c2 ⇔ Tf c1 (Abs c2) ∧ Tf c2 (Abs c1)

Qt_right_unique

⊢ Qt R Abs Rep Tf ⇒ right_unique Tf

Qt_surj

⊢ Qt R Abs Rep Tf ⇒ surj Tf

R_repabs

⊢ Qt R Abs Rep Tf ⇒ ∀x. R x x ⇒ R (Rep (Abs x)) x

funQ

⊢ Qt D AbsD RepD TfD ∧ Qt R AbsR RepR TfR ⇒
  Qt (D |==> R) (RepD ---> AbsR) (AbsD ---> RepR) (TfD |==> TfR)

idQ

⊢ Qt $= I I $=

listQ

⊢ Qt R Abs Rep Tf ⇒ Qt (LIST_REL R) (MAP Abs) (MAP Rep) (LIST_REL Tf)

map_fun_I

⊢ (f ---> I = flip $o f) ∧ (I ---> g = $o g)

map_fun_id

⊢ I ---> I = I

map_fun_o

⊢ f1 ∘ f2 ---> g1 ∘ g2 = (f2 ---> g1) ∘ (f1 ---> g2)

map_fun_thm

⊢ (f ---> g) h x = g (h (f x))

pairQ

⊢ Qt R1 Abs1 Rep1 Tf1 ∧ Qt R2 Abs2 Rep2 Tf2 ⇒
  Qt (R1 ### R2) (Abs1 ## Abs2) (Rep1 ## Rep2) (Tf1 ### Tf2)

setQ

⊢ Qt R Abs Rep Tf ⇒
  Qt (R |==> $<=>) (PREIMAGE Rep) (PREIMAGE Abs) (Tf |==> $<=>)