# Structure liftingTheory

Source File Identifier index Theory binding index

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

(*  Definitions  *)
val Qt_def : thm
val map_fun_def : thm

(*  Theorems  *)
val HK_thm2 : thm
val Qt_EQ : thm
val Qt_alt : thm
val Qt_alt_def2 : thm
val Qt_right_unique : thm
val Qt_surj : thm
val R_repabs : thm
val funQ : thm
val idQ : thm
val listQ : thm
val map_fun_I : thm
val map_fun_id : thm
val map_fun_o : thm
val map_fun_thm : thm
val pairQ : thm
val setQ : thm

val lifting_grammars : type_grammar.grammar * term_grammar.grammar
(*
[transfer] Parent theory of "lifting"

[Qt_def]  Definition

⊢ ∀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]  Definition

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

[HK_thm2]  Theorem

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

[Qt_EQ]  Theorem

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

[Qt_alt]  Theorem

⊢ 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]  Theorem

⊢ 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]  Theorem

⊢ Qt R Abs Rep Tf ⇒ right_unique Tf

[Qt_surj]  Theorem

⊢ Qt R Abs Rep Tf ⇒ surj Tf

[R_repabs]  Theorem

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

[funQ]  Theorem

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

[idQ]  Theorem

⊢ Qt \$= I I \$=

[listQ]  Theorem

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

[map_fun_I]  Theorem

⊢ f ---> I = flip \$o f ∧ I ---> g = \$o g

[map_fun_id]  Theorem

⊢ I ---> I = I

[map_fun_o]  Theorem

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

[map_fun_thm]  Theorem

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

[pairQ]  Theorem

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

[setQ]  Theorem

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

*)
end

```

Source File Identifier index Theory binding index

HOL 4, Trindemossen-1