Structure liftingTheory

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

HOL 4, Kananaskis-14