Theory HIT_Typing

theory HIT_Typing
  imports HIT_Reduction
begin

section ‹Typing›

text ‹
  A judgment carries an ambient dimension context, a set of dimension
  variables, and an ordinary typing context.  The reserved index ‹0› never
  belongs to an ambient dimension context: it is bound by the path methods of
  an eliminator, and the typing rule for the eliminator is the only place
  where it enters scope.
›

primrec argTy :: "nat ⇒ argspec ⇒ ty" where
  "argTy h (Par h') = Hit h'"
| "argTy h Rec = Hit h"

text ‹
  A method for a constructor consumes the arguments of that constructor, and
  in addition, for every recursive argument, the value of the eliminator on
  it.  This is exactly the list produced by \<^const>‹elimArgs›.
›

primrec methodTy :: "nat ⇒ ty ⇒ argspec list ⇒ ty" where
  "methodTy h C [] = C"
| "methodTy h C (s # ss) =
    (case s of
       Par h' ⇒ Fun (Hit h') (methodTy h C ss)
     | Rec ⇒ Fun (Hit h) (Fun C (methodTy h C ss)))"

inductive wt :: "sigenv ⇒ nat set ⇒ ty list ⇒ tm ⇒ ty ⇒ bool"
  for S :: sigenv
where
  wtVar:
    "i < length G ⟹ wt S D G (Var i) (G ! i)"
| wtLam:
    "wt S D (A # G) t B ⟹ wt S D G (Lam A t) (Fun A B)"
| wtApp:
    "wt S D G t (Fun A B) ⟹ wt S D G u A ⟹ wt S D G (App t u) B"
| wtPCon:
    "k < length (pcons (S h)) ⟹
      length as = length (pcons (S h) ! k) ⟹
      (∀i < length as.
        wt S D G (as ! i) (argTy h (pcons (S h) ! k ! i))) ⟹
      wt S D G (PCon h k as) (Hit h)"
| wtLCon:
    "j ∈ D ⟹ k < length (lcons (S h)) ⟹
      length as = length (lcons (S h) ! k) ⟹
      (∀i < length as.
        wt S D G (as ! i) (argTy h (lcons (S h) ! k ! i))) ⟹
      wt S D G (LCon h k as (DVar j)) (Hit h)"
| wtElim:
    "wt S D G t (Hit h) ⟹
      length pms = length (pcons (S h)) ⟹
      length lms = length (lcons (S h)) ⟹
      (∀k < length pms.
        wt S D G (pms ! k) (methodTy h C (pcons (S h) ! k))) ⟹
      (∀k < length lms.
        wt S (insert 0 D) G (lms ! k)
          (methodTy h C (lcons (S h) ! k))) ⟹
      wt S D G (HElim h C pms lms t) C"

subsection ‹Applying a method to the eliminator arguments›

text ‹
  The computation rules replace an eliminator at a constructor by the
  corresponding method applied to \<^const>‹elimArgs›.  The following lemma is
  the typing analogue: a method of the declared type, applied to arguments
  of the declared kinds, lands in the motive.
›

lemma wt_apps_elimArgs:
  assumes E: "⋀a. wt S D G a (Hit h) ⟹
      wt S D G (HElim h C pms lms a) C"
  shows "⋀as m. length as = length ss ⟹
    (∀i < length ss. wt S D G (as ! i) (argTy h (ss ! i))) ⟹
    wt S D G m (methodTy h C ss) ⟹
    wt S D G (apps m (elimArgs h C pms lms ss as)) C"
proof (induct ss)
  case Nil
  then show ?case by simp
next
  case (Cons s ss)
  from Cons(2) obtain a as' where as: "as = a # as'"
    and len: "length as' = length ss"
    by (cases as) auto
  have a0: "wt S D G a (argTy h s)"
    using Cons(3) as by force
  have rest: "∀i < length ss. wt S D G (as' ! i) (argTy h (ss ! i))"
    using Cons(3) as by fastforce
  show ?case
  proof (cases s)
    case (Par h')
    then have "wt S D G a (Hit h')" using a0 by simp
    moreover from Cons(4) Par
      have "wt S D G m (Fun (Hit h') (methodTy h C ss))" by simp
    ultimately have "wt S D G (App m a) (methodTy h C ss)"
      by (rule wt.wtApp[rotated])
    then have "wt S D G (apps (App m a) (elimArgs h C pms lms ss as')) C"
      by (rule Cons(1)[OF len rest])
    then show ?thesis using as Par by simp
  next
    case Rec
    then have aH: "wt S D G a (Hit h)" using a0 by simp
    from Cons(4) Rec
      have "wt S D G m (Fun (Hit h) (Fun C (methodTy h C ss)))" by simp
    from wt.wtApp[OF this aH]
      have step: "wt S D G (App m a) (Fun C (methodTy h C ss))" .
    have "wt S D G (App (App m a) (HElim h C pms lms a)) (methodTy h C ss)"
      by (rule wt.wtApp[OF step E[OF aH]])
    then have "wt S D G
        (apps (App (App m a) (HElim h C pms lms a))
          (elimArgs h C pms lms ss as')) C"
      by (rule Cons(1)[OF len rest])
    then show ?thesis using as Rec by simp
  qed
qed

end