Theory Types

subsection ‹Types›
  
theory Types
  imports Syntax
begin
  
text‹We implement typing environments as (total) functions from natural numbers to types,
     following the approach of Stefan Berghofer in his formalisation of the simply typed
     $\lambda$-calculus in the Isabelle/HOL library.
     An empty typing environment may be represented by an arbitrary function of the correct type
     as it will never be queried when a typing judgement is valid. We split typing environments,
     dedicating one environment to $\lambda$-variables and another to $\mu$-variables, and
     use $\Gamma$ and $\Delta$ to range over the former and latter, respectively.›

text‹From src/HOL/Proofs/LambdaType.thy›
  
definition
  shift :: "(nat ⇒ 'a) ⇒ nat ⇒ 'a ⇒ nat ⇒ 'a"  ("_⟨_:_⟩" [90, 0, 0] 91) where
  "e⟨i:a⟩ = (λj. if j < i then e j else if j = i then a else e (j-1))"

lemma shift_eq [simp]: "i = j ⟹ (e⟨i:T⟩) j = T"
  by (simp add: shift_def)

lemma shift_gt [simp]: "j < i ⟹ (e⟨i:T⟩) j = e j"
  by (simp add: shift_def)

lemma shift_lt [simp]: "i < j ⟹ (e⟨i:T⟩) j = e (j - 1)"
  by (simp add: shift_def)

lemma shift_commute [simp]: "e⟨i:U⟩⟨0:T⟩ = e⟨0:T⟩⟨Suc i:U⟩"
  by (rule ext) (simp_all add: shift_def split: nat.split, force)
   
inductive typing_trm :: "(nat ⇒ type) ⇒ (nat ⇒ type) ⇒ trm ⇒ type ⇒ bool"  
     ("_ , _ ⊢⇩T _ : _" [50, 50, 50, 50] 50)
and typing_cmd :: "(nat ⇒ type) ⇒ (nat ⇒ type) ⇒ cmd ⇒ bool"
     ("_ , _ ⊢⇩C _" [50, 50, 50] 50)
where 
  var [intro!]: "⟦ Γ x = T ⟧ ⟹ Γ, Δ ⊢⇩T `x : T" |
  app [intro!]: "⟦ Γ, Δ ⊢⇩T t : (T1→T2); Γ, Δ ⊢⇩T s : T1 ⟧
                    ⟹ Γ, Δ ⊢⇩T (t°s) : T2" |
  lambda [intro!]: "⟦ Γ⟨0:T1⟩, Δ ⊢⇩T t : T2 ⟧
                    ⟹ Γ, Δ ⊢⇩T (λ T1 : t) : (T1→T2)" |
  activate [intro!]: "⟦ Γ, Δ⟨0:T⟩ ⊢⇩C c ⟧ ⟹ Γ, Δ ⊢⇩T (μ T : c) : T" |
  passivate [intro!]: "⟦ Γ, Δ ⊢⇩T t : T; Δ x = T⟧ ⟹ Γ, Δ ⊢⇩C (<x> t)"

inductive_cases typing_elims [elim!]:
  "Γ, Δ ⊢⇩T `x : T"
  "Γ, Δ ⊢⇩T t°s : T"
  "Γ, Δ ⊢⇩T λ T1 : t : T"
  "Γ, Δ ⊢⇩T μ T1 : t : T"
  "Γ, Δ ⊢⇩C <x> t"

inductive_cases type_arrow_elim:
  "Γ , Δ ⊢⇩T t : T1 → T2"

lemma uniqueness:
  "Γ, Δ ⊢⇩T t : T1 ⟹ Γ, Δ ⊢⇩T t : T2 ⟹ T1 = T2"
  "Γ, Δ ⊢⇩C c ⟹ Γ, Δ ⊢⇩C c"
  apply(induct arbitrary: T2 rule: typing_trm_typing_cmd.inducts)
  using typing_cmd.cases apply blast+
done

end