Theory POPLmark

(*  Title:      POPLmark/POPLmark.thy
    Author:     Stefan Berghofer, TU Muenchen, 2005
                Conversion to Isar by LCP, 2025
*)

theory POPLmark
  imports Basis
begin


section ‹Formalization of the basic calculus›

text ‹
\label{sec:basic-calculus}
In this section, we describe the formalization of the basic calculus
without records. As a main result, we prove {\it type safety}, presented
as two separate theorems, namely {\it preservation} and {\it progress}.
›


subsection ‹Types and Terms›

text ‹
The types of System \fsub{} are represented by the following datatype:
›

datatype type =
    TVar nat
  | Top
  | Fun type type    (infixr  200)
  | TyAll type type  ((3∀<:_./ _) [0, 10] 10)

text ‹
The subtyping and typing judgements depend on a {\it context} (or environment) @{term Γ}
containing bindings for term and type variables. A context is a list of bindings,
where the @{term i}th element @{term "Γi"} corresponds to the variable
with index @{term i}.
›

datatype binding = VarB type | TVarB type
type_synonym env = "binding list"

text ‹
In contrast to the usual presentation of type systems often found in textbooks, new
elements are added to the left of a context using the Cons› operator ∷› for lists.
We write @{term is_TVarB} for the predicate that returns @{term True} when applied to
a type variable binding, function @{term type_ofB} extracts the type contained in a binding,
and @{term "mapB f"} applies @{term f} to the type contained in a binding.
›

primrec is_TVarB :: "binding  bool"
where
  "is_TVarB (VarB T) = False"
| "is_TVarB (TVarB T) = True"

primrec type_ofB :: "binding  type"
where
  "type_ofB (VarB T) = T"
| "type_ofB (TVarB T) = T"

primrec mapB :: "(type  type)  binding  binding"
where
  "mapB f (VarB T) = VarB (f T)"
| "mapB f (TVarB T) = TVarB (f T)"

text ‹
The following datatype represents the terms of System \fsub{}:
›

datatype trm =
    Var nat
  | Abs type trm   ((3λ:_./ _) [0, 10] 10)
  | TAbs type trm  ((3λ<:_./ _) [0, 10] 10)
  | App trm trm    (infixl  200)
  | TApp trm type  (infixl τ 200)


subsection ‹Lifting and Substitution›

text ‹
One of the central operations of $\lambda$-calculus is {\it substitution}.
In order to avoid that free variables in a term or type get ``captured''
when substituting it for a variable occurring in the scope of a binder,
we have to increment the indices of its free variables during substitution.
This is done by the lifting functions τ n k› and ↑ n k›
for types and terms, respectively, which increment the indices of all free
variables with indices ≥ k› by @{term n}. The lifting functions on
types and terms are defined by
›

primrec liftT :: "nat  nat  type  type" (τ)
where
  "τ n k (TVar i) = (if i < k then TVar i else TVar (i + n))"
| "τ n k Top = Top"
| "τ n k (T  U) = τ n k T  τ n k U"
| "τ n k (∀<:T. U) = (∀<:τ n k T. τ n (k + 1) U)"

primrec lift :: "nat  nat  trm  trm" ()
where
  " n k (Var i) = (if i < k then Var i else Var (i + n))"
| " n k (λ:T. t) = (λ:τ n k T.  n (k + 1) t)"
| " n k (λ<:T. t) = (λ<:τ n k T.  n (k + 1) t)"
| " n k (s  t) =  n k s   n k t"
| " n k (t τ T) =  n k t τ τ n k T"

text ‹
It is useful to also define an ``unlifting'' function τ n k› for
decrementing all free variables with indices ≥ k› by @{term n}.
Moreover, we need several substitution functions, denoted by
\mbox{T[k ↦τ S]τ}, \mbox{t[k ↦τ S]›}, and \mbox{t[k ↦ s]›},
which substitute type variables in types, type variables in terms,
and term variables in terms, respectively. They are defined as follows:
›

primrec substTT :: "type  nat  type  type"  (‹_[_ τ _]τ [300, 0, 0] 300)
where
  "(TVar i)[k τ S]τ =
     (if k < i then TVar (i - 1) else if i = k then τ k 0 S else TVar i)"
| "Top[k τ S]τ = Top"
| "(T  U)[k τ S]τ = T[k τ S]τ  U[k τ S]τ"
| "(∀<:T. U)[k τ S]τ = (∀<:T[k τ S]τ. U[k+1 τ S]τ)"

primrec decT :: "nat  nat  type  type"  (τ)
where
  "τ 0 k T = T"
| "τ (Suc n) k T = τ n k (T[k τ Top]τ)"

primrec subst :: "trm  nat  trm  trm"  (‹_[_  _] [300, 0, 0] 300)
where
  "(Var i)[k  s] = (if k < i then Var (i - 1) else if i = k then  k 0 s else Var i)"
| "(t  u)[k  s] = t[k  s]  u[k  s]"
| "(t τ T)[k  s] = t[k  s] τ τ 1 k T"
| "(λ:T. t)[k  s] = (λ:τ 1 k T. t[k+1  s])"
| "(λ<:T. t)[k  s] = (λ<:τ 1 k T. t[k+1  s])"

primrec substT :: "trm  nat  type  trm"    (‹_[_ τ _] [300, 0, 0] 300)
where
  "(Var i)[k τ S] = (if k < i then Var (i - 1) else Var i)"
| "(t  u)[k τ S] = t[k τ S]  u[k τ S]"
| "(t τ T)[k τ S] = t[k τ S] τ T[k τ S]τ"
| "(λ:T. t)[k τ S] = (λ:T[k τ S]τ. t[k+1 τ S])"
| "(λ<:T. t)[k τ S] = (λ<:T[k τ S]τ. t[k+1 τ S])"

text ‹
Lifting and substitution extends to typing contexts as follows:
›

primrec liftE :: "nat  nat  env  env" (e)
where
  "e n k [] = []"
| "e n k (B  Γ) = mapB (τ n (k + Γ)) B  e n k Γ"

primrec substE :: "env  nat  type  env"  (‹_[_ τ _]e [300, 0, 0] 300)
where
  "[][k τ T]e = []"
| "(B  Γ)[k τ T]e = mapB (λU. U[k + Γ τ T]τ) B  Γ[k τ T]e"

primrec decE :: "nat  nat  env  env"  (e)
where
  "e 0 k Γ = Γ"
| "e (Suc n) k Γ = e n k (Γ[k τ Top]e)"

text ‹
Note that in a context of the form @{term "B  Γ"}, all variables in @{term B} with
indices smaller than the length of @{term Γ} refer to entries in @{term Γ} and therefore
must not be affected by substitution and lifting. This is the reason why an
additional offset @{term "Γ"} needs to be added to the index @{term k}
in the second clauses of the above functions. Some standard properties of lifting
and substitution, which can be proved by structural induction on terms and types,
are proved below. Properties of this kind are
quite standard for encodings using de Bruijn indices and can also be found in
papers by Barras and Werner cite"Barras-Werner-JAR" and Nipkow cite"Nipkow-JAR01".
›

lemma liftE_length [simp]: "e n k Γ = Γ"
  by (induct Γ) simp_all

lemma substE_length [simp]: "Γ[k τ U]e = Γ"
  by (induct Γ) simp_all

lemma liftE_nth [simp]:
  "(e n k Γ)i = map_option (mapB (τ n (k + Γ - i - 1))) (Γi)"
proof (induct Γ arbitrary: i)
  case Nil
  then show ?case 
    by simp
next
  case (Cons a Γ)
  then show ?case
    by (cases i) auto
qed

lemma substE_nth [simp]:
  "(Γ[0 τ T]e)i = map_option (mapB (λU. U[Γ - i - 1 τ T]τ)) (Γi)"
proof (induct Γ arbitrary: i)
  case Nil
  then show ?case
    by simp
next
  case (Cons a Γ)
  then show ?case 
    by (cases i) auto
qed

lemma liftT_liftT [simp]:
  "i  j  j  i + m  τ n j (τ m i T) = τ (m + n) i T"
  by (induct T arbitrary: i j m n) simp_all

lemma liftT_liftT' [simp]:
  "i + m  j  τ n j (τ m i T) = τ m i (τ n (j - m) T)"
proof (induct T arbitrary: i j m n)
  case (TyAll T1 T2)
  then have "Suc j - m = Suc (j - m)"
    by arith
  with TyAll show ?case
    by simp
qed auto

lemma lift_size [simp]: "size (τ n k T) = size T"
  by (induct T arbitrary: k) simp_all

lemma liftT0 [simp]: "τ 0 i T = T"
  by (induct T arbitrary: i) simp_all

lemma lift0 [simp]: " 0 i t = t"
  by (induct t arbitrary: i) simp_all

theorem substT_liftT [simp]:
  "k  k'  k' < k + n  (τ n k T)[k' τ U]τ = τ (n - 1) k T"
  by (induct T arbitrary: k k') simp_all

theorem liftT_substT [simp]:
  "k  k'  τ n k (T[k' τ U]τ) = τ n k T[k' + n τ U]τ"
  by (induct T arbitrary: k k') auto

theorem liftT_substT' [simp]: "k' < k 
  τ n k (T[k' τ U]τ) = τ n (k + 1) T[k' τ τ n (k - k') U]τ"
  by (induct T arbitrary: k k') auto

lemma liftT_substT_Top [simp]:
  "k  k'  τ n k' (T[k τ Top]τ) = τ n (Suc k') T[k τ Top]τ"
  by (induct T arbitrary: k k') auto

lemma liftT_substT_strange:
  "τ n k T[n + k τ U]τ = τ n (Suc k) T[k τ τ n 0 U]τ"
proof (induct T arbitrary: n k)
  case (TyAll T1 T2)
  then have " τ n (Suc k) T2[Suc (n + k) τ U]τ = τ n (Suc (Suc k)) T2[Suc k τ τ n 0 U]τ"
    by (metis add_Suc_right)
  with TyAll show ?case
    by simp
qed auto

lemma lift_lift [simp]:
  "k  k'  k'  k + n   n' k' ( n k t) =  (n + n') k t"
  by (induct t arbitrary: k k') simp_all

lemma substT_substT:
  "i  j  T[Suc j τ V]τ[i τ U[j - i τ V]τ]τ = T[i τ U]τ[j τ V]τ"
proof (induct T arbitrary: i j U V)
  case (TyAll T1 T2)
  then have "T2[Suc (Suc j) τ V]τ[Suc i τ U[j - i τ V]τ]τ =
             T2[Suc i τ U]τ[Suc j τ V]τ"
    by (metis Suc_le_mono diff_Suc_Suc)
  with TyAll show ?case
    by auto
qed auto


subsection ‹Well-formedness›

text ‹
\label{sec:wf}
The subtyping and typing judgements to be defined in \secref{sec:subtyping}
and \secref{sec:typing} may only operate on types and contexts that
are well-formed. Intuitively, a type @{term T} is well-formed with respect to a
context @{term Γ}, if all variables occurring in it are defined in @{term Γ}.
More precisely, if @{term T} contains a type variable @{term "TVar i"}, then
the @{term i}th element of @{term Γ} must exist and have the form @{term "TVarB U"}.
›

inductive
  well_formed :: "env  type  bool"  (‹_ wf _› [50, 50] 50)
  where
    wf_TVar: "Γi = TVarB T  Γ wf TVar i"
  | wf_Top: "Γ wf Top"
  | wf_arrow: "Γ wf T  Γ wf U  Γ wf T  U"
  | wf_all: "Γ wf T  TVarB T  Γ wf U  Γ wf (∀<:T. U)"

text ‹
A context @{term "Γ"} is well-formed, if all types occurring in it only refer to type variables
declared ``further to the right'':
›

inductive
  well_formedE :: "env  bool"  (‹_ wf [50] 50)
  and well_formedB :: "env  binding  bool"  (‹_ wfB _› [50, 50] 50)
  where
    "Γ wfB B  Γ wf type_ofB B"
  | wf_Nil: "[] wf"
  | wf_Cons: "Γ wfB B  Γ wf  B  Γ wf"

text ‹
The judgement Γ ⊢wfB B›, which denotes well-formedness of the binding @{term B}
with respect to context @{term Γ}, is just an abbreviation for Γ ⊢wf type_ofB B›.
We now present a number of properties of the well-formedness judgements that will be used
in the proofs in the following sections.
›

inductive_cases well_formed_cases:
  "Γ wf TVar i"
  "Γ wf Top"
  "Γ wf T  U"
  "Γ wf (∀<:T. U)"

inductive_cases well_formedE_cases:
  "B  Γ wf"

lemma wf_TVarB: "Γ wf T  Γ wf  TVarB T  Γ wf"
  by (rule wf_Cons) simp_all

lemma wf_VarB: "Γ wf T  Γ wf  VarB T  Γ wf"
  by (rule wf_Cons) simp_all

lemma map_is_TVarb:
  "map is_TVarB Γ' = map is_TVarB Γ 
    Γi = TVarB T  T. Γ'i = TVarB T"
proof (induct Γ arbitrary: Γ' T i)
  case Nil
  then show ?case
    by auto
next
  case (Cons a Γ)
  obtain z Γ'' where "Γ' = z  Γ''"
    using Cons.prems(1) by auto
  with Cons  show ?case
    by (cases z) (auto split: nat.splits)
qed

text ‹
A type that is well-formed in a context @{term Γ} is also well-formed in another context
@{term Γ'} that contains type variable bindings at the same positions as @{term Γ}:
›

lemma wf_equallength:
  assumes H: "Γ wf T"
  shows "map is_TVarB Γ' = map is_TVarB Γ  Γ' wf T" using H
  by (induct arbitrary: Γ') (auto intro: well_formed.intros dest: map_is_TVarb)

text ‹
A well-formed context of the form @{term "Δ @ B  Γ"} remains well-formed if we replace
the binding @{term B} by another well-formed binding @{term B'}:
›

lemma wfE_replace:
  "Δ @ B  Γ wf  Γ wfB B'  is_TVarB B' = is_TVarB B 
    Δ @ B'  Γ wf"
proof (induct Δ)
  case Nil
  then show ?case
    by (metis append_Nil well_formedE_cases wf_Cons)
next
  case (Cons a Δ)
  then show ?case
    using wf_Cons wf_equallength by (auto elim!: well_formedE_cases)
qed

text ‹
The following weakening lemmas can easily be proved by structural induction on
types and contexts:
›

lemma wf_weaken:
  assumes H: "Δ @ Γ wf T"
  shows "e (Suc 0) 0 Δ @ B  Γ wf τ (Suc 0) Δ T"
  using H
proof (induct "Δ @ Γ" T arbitrary: Δ)
  case tv: (wf_TVar i T)
  show ?case
  proof (cases "i < Δ")
    case True
    with tv show ?thesis
      by (simp add: wf_TVar)
  next
    case False
    then have "Suc i - Δ = Suc (i - Δ)"
      using Suc_diff_le linorder_not_less by blast
    with tv False show ?thesis
      by (simp add: wf_TVar)
  qed
next
  case wf_Top
  then show ?case
    using well_formed.wf_Top by auto
next
  case (wf_arrow T U)
  then show ?case
    by (simp add: well_formed.wf_arrow)
next
  case (wf_all T U)
  then show ?case
    using well_formed.wf_all by force
qed 

lemma wf_weaken': "Γ wf T  Δ @ Γ wf τ Δ 0 T"
proof (induct Δ)
  case Nil
  then show ?case 
by auto
next
  case (Cons a Δ)
  then show ?case
    by (metis liftT_liftT add_0_right wf_weaken liftE.simps append_Cons 
        append_Nil le_add1 list.size(3,4))
qed

lemma wfE_weaken: "Δ @ Γ wf  Γ wfB B  e (Suc 0) 0 Δ @ B  Γ wf"
proof (induct Δ)
  case Nil
  then show ?case
    by (simp add: wf_Cons)
next
  case (Cons a Δ)
  then have "e (Suc 0) 0 Δ @ B  Γ wfB mapB (τ (Suc 0) Δ) a"
    by (cases a) (use wf_weaken in auto elim!: well_formedE_cases)
  with Cons show ?case
    using well_formedE_cases wf_Cons by auto
qed

text ‹
Intuitively, lemma wf_weaken› states that a type @{term T} which is well-formed
in a context is still well-formed in a larger context, whereas lemma wfE_weaken›
states that a well-formed context remains well-formed when extended with a
well-formed binding. Owing to the encoding of variables using de Bruijn
indices, the statements of the above lemmas involve additional lifting functions.
The typing judgement, which will be described in \secref{sec:typing}, involves
the lookup of variables in a context. It has already been pointed out earlier that each
entry in a context may only depend on types declared ``further to the right''. To ensure that
a type @{term T} stored at position @{term i} in an environment @{term Γ} is valid in the full
environment, as opposed to the smaller environment consisting only of the entries in
@{term Γ} at positions greater than @{term i}, we need to increment the indices of all
free type variables in @{term T} by @{term "Suc i"}:
›

lemma wf_liftB:
  assumes H: "Γ wf"
  shows "Γi = VarB T  Γ wf τ (Suc i) 0 T"
  using H
proof (induct arbitrary: i)
  case wf_Nil
  then show ?case
    by auto
next
  case (wf_Cons Γ B)
then have "j. Γj = VarB T  B  Γ wf τ (Suc (Suc j)) 0 T"
    by (metis Suc_eq_plus1 add_0 append_Nil zero_le liftE.simps(1)
        liftT_liftT list.size(3) wf_weaken)
  with wf_Cons wf_weaken[where B="VarB T" and Δ="[]"] show ?case
    by (simp split: nat.split_asm)
qed

text ‹
We also need lemmas stating that substitution of well-formed types preserves the well-formedness
of types and contexts:
›

theorem wf_subst:
  "Δ @ B  Γ wf T  Γ wf U  Δ[0 τ U]e @ Γ wf T[Δ τ U]τ"
proof (induct T arbitrary: Δ)
  case (TVar n Δ)
  then have 1: "x. Δ @ B  Γ wf TVar x; x = Δ
        Δ[0 τ U]e @ Γ wf τ Δ 0 U"
    by (metis substE_length wf_weaken')
  have 2: "m. n - Δ = Suc m  n - Suc Δ = m"
    by (metis Suc_diff_Suc nat.inject zero_less_Suc zero_less_diff)
  show ?case
    using TVar
    by (auto simp: wf_TVar 1 2 elim!: well_formed_cases split: nat.split_asm)
next
  case Top
  then show ?case
    using wf_Top by auto
next
  case (Fun T1 T2)
  then show ?case
    by (metis substTT.simps(3) well_formed_cases(3) wf_arrow)
next
  case (TyAll T1 T2)
  then have "(TVarB T1  Δ)[0 τ U]e @ Γ wf T2[TVarB T1  Δ τ U]τ"
    by (metis append_Cons well_formed_cases(4))
  with TyAll wf_all show ?case
    by (auto elim!: well_formed_cases)
qed

theorem wfE_subst: "Δ @ B  Γ wf  Γ wf U  Δ[0 τ U]e @ Γ wf"
proof (induct Δ)
  case Nil
  then show ?case
    by (auto elim!: well_formedE_cases)
next
  case (Cons a Δ)
  show ?case
  proof (cases a)
    case (VarB x1)
    with Cons wf_VarB wf_subst show ?thesis
      by (auto elim!: well_formedE_cases)
  next
    case (TVarB x2)
    with Cons wf_TVarB wf_subst show ?thesis
      by (auto elim!: well_formedE_cases)
  qed
qed


subsection ‹Subtyping›

text ‹
\label{sec:subtyping}
We now come to the definition of the subtyping judgement Γ ⊢ T <: U›.
›

inductive
  subtyping :: "env  type  type  bool"  (‹_ / _ <: _› [50, 50, 50] 50)
where
  SA_Top: "Γ wf  Γ wf S  Γ  S <: Top"
| SA_refl_TVar: "Γ wf  Γ wf TVar i  Γ  TVar i <: TVar i"
| SA_trans_TVar: "Γi = TVarB U 
    Γ  τ (Suc i) 0 U <: T  Γ  TVar i <: T"
| SA_arrow: "Γ  T1 <: S1  Γ  S2 <: T2  Γ  S1  S2 <: T1  T2"
| SA_all: "Γ  T1 <: S1  TVarB T1  Γ  S2 <: T2 
    Γ  (∀<:S1. S2) <: (∀<:T1. T2)"

text ‹
The rules SA_Top› and SA_refl_TVar›, which appear at the leaves of
the derivation tree for a judgement @{term "Γ  T <: U"}, contain additional
side conditions ensuring the well-formedness of the contexts and types involved.
In order for the rule SA_trans_TVar› to be applicable, the context @{term Γ}
must be of the form \mbox{@{term "Γ1 @ B  Γ2"}}, where @{term "Γ1"} has the length @{term i}.
Since the indices of variables in @{term B} can only refer to variables defined in
@{term "Γ2"}, they have to be incremented by @{term "Suc i"} to ensure that they point
to the right variables in the larger context Γ›.
›

lemma wf_subtype_env:
  assumes PQ: "Γ  P <: Q"
  shows "Γ wf" using PQ
  by induct assumption+

lemma wf_subtype:
  assumes PQ: "Γ  P <: Q"
  shows "Γ wf P  Γ wf Q" using PQ
  by induct (auto intro: well_formed.intros elim!: wf_equallength)

lemma wf_subtypeE:
  assumes H: "Γ  T <: U"
  and H': "Γ wf  Γ wf T  Γ wf U  P"
  shows "P"
  using H H' wf_subtype wf_subtype_env by blast

text ‹
By induction on the derivation of @{term "Γ  T <: U"}, it can easily be shown
that all types and contexts occurring in a subtyping judgement must be well-formed:
›

lemma wf_subtype_conj:
  "Γ  T <: U  Γ wf  Γ wf T  Γ wf U"
  by (erule wf_subtypeE) iprover

text ‹
By induction on types, we can prove that the subtyping relation is reflexive:
›

lemma subtype_refl: ― ‹A.1›
  "Γ wf  Γ wf T  Γ  T <: T"
  by (induct T arbitrary: Γ) (blast intro:
    subtyping.intros wf_Nil wf_TVarB elim: well_formed_cases)+

text ‹
The weakening lemma for the subtyping relation is proved in two steps:
by induction on the derivation of the subtyping relation, we first prove
that inserting a single type into the context preserves subtyping:
›

lemma subtype_weaken:
  assumes H: "Δ @ Γ  P <: Q"
  and wf: "Γ wfB B"
  shows "e 1 0 Δ @ B  Γ  τ 1 Δ P <: τ 1 Δ Q" using H
proof (induct "Δ @ Γ" P Q arbitrary: Δ)
  case SA_Top
  with wf show ?case
    by (auto intro: subtyping.SA_Top wfE_weaken wf_weaken)
next
  case SA_refl_TVar
  with wf show ?case
    by (auto intro!: subtyping.SA_refl_TVar wfE_weaken dest: wf_weaken)
next
  case (SA_trans_TVar i U T)
  thus ?case
  proof (cases "i < Δ")
    case True
    with SA_trans_TVar
    have "(e 1 0 Δ @ B  Γ)i = TVarB (τ 1 (Δ - Suc i) U)"
      by simp
    moreover from True SA_trans_TVar
    have "e 1 0 Δ @ B  Γ 
      τ (Suc i) 0 (τ 1 (Δ - Suc i) U) <: τ 1 Δ T"
      by simp
    ultimately have "e 1 0 Δ @ B  Γ  TVar i <: τ 1 Δ T"
      by (rule subtyping.SA_trans_TVar)
    with True show ?thesis by simp
  next
    case False
    then have "Suc i - Δ = Suc (i - Δ)" by arith
    with False SA_trans_TVar have "(e 1 0 Δ @ B  Γ)Suc i = TVarB U"
      by simp
    moreover from False SA_trans_TVar
    have "e 1 0 Δ @ B  Γ  τ (Suc (Suc i)) 0 U <: τ 1 Δ T"
      by simp
    ultimately have "e 1 0 Δ @ B  Γ  TVar (Suc i) <: τ 1 Δ T"
      by (rule subtyping.SA_trans_TVar)
    with False show ?thesis by simp
  qed
next
  case SA_arrow
  thus ?case by simp (iprover intro: subtyping.SA_arrow)
next
  case (SA_all T1 S1 S2 T2 Δ)
  with SA_all(4) [of "TVarB T1  Δ"]
  show ?case by simp (iprover intro: subtyping.SA_all)
qed

text ‹
All cases are trivial, except for the SA_trans_TVar› case, which
requires a case distinction on whether the index of the variable is smaller
than @{term "Δ"}.
The stronger result that appending a new context @{term Δ} to a context
@{term Γ} preserves subtyping can be proved by induction on @{term Δ},
using the previous result in the induction step:
›

lemma subtype_weaken': ― ‹A.2›
  "Γ  P <: Q  Δ @ Γ wf  Δ @ Γ  τ Δ 0 P <: τ Δ 0 Q"
proof (induct Δ)
  case Nil
  then show ?case
    by simp 
next
  case (Cons a Δ)
  then have "a  Δ @ Γ  τ 1 0 (τ Δ 0 P) <: τ 1 0 (τ Δ 0 Q)"
    using subtype_weaken[of "[]" "Δ @ Γ", where B="a"] liftT_liftT
    by (fastforce elim!: well_formedE_cases)
  then show ?case
    by (auto elim!: well_formedE_cases)
qed

text ‹
An unrestricted transitivity rule has the disadvantage that it can
be applied in any situation. In order to make the above definition of the
subtyping relation {\it syntax-directed}, the transitivity rule SA_trans_TVar›
is restricted to the case where the type on the left-hand side of the <:›
operator is a variable. However, the unrestricted transitivity rule
can be derived from this definition.
In order for the proof to go through, we have to simultaneously prove
another property called {\it narrowing}.
The two properties are proved by nested induction. The outer induction
is on the size of the type @{term Q}, whereas the two inner inductions for
proving transitivity and narrowing are on the derivation of the
subtyping judgements. The transitivity property is needed in the proof of
narrowing, which is by induction on the derivation of \mbox{@{term "Δ @ TVarB Q  Γ  M <: N"}}.
In the case corresponding to the rule SA_trans_TVar›, we must prove
\mbox{@{term "Δ @ TVarB P  Γ  TVar i <: T"}}. The only interesting case
is the one where @{term "i = Δ"}. By induction hypothesis, we know that
@{term "Δ @ TVarB P  Γ  τ (i+1) 0 Q <: T"} and
@{term "(Δ @ TVarB Q  Γ)i = TVarB Q"}.
By assumption, we have @{term "Γ  P <: Q"} and hence 
\mbox{@{term "Δ @ TVarB P  Γ  τ (i+1) 0 P <: τ (i+1) 0 Q"}} by weakening.
Since @{term "τ (i+1) 0 Q"} has the same size as @{term Q}, we can use
the transitivity property, which yields
@{term "Δ @ TVarB P  Γ  τ (i+1) 0 P <: T"}. The claim then follows
easily by an application of SA_trans_TVar›.
›

lemma subtype_trans: ― ‹A.3›
  "Γ  S <: Q  Γ  Q <: T  Γ  S <: T"
  "Δ @ TVarB Q  Γ  M <: N  Γ  P <: Q 
     Δ @ TVarB P  Γ  M <: N"
  using wf_measure_size
proof (induct Q arbitrary: Γ S T Δ P M N rule: wf_induct_rule)
  case (less Q)
  have tr: "Γ  Q' <: T  size Q = size Q'  Γ  S <: T"
    if "Γ  S <: Q'" for Γ S T Q'
    using that
  proof (induct arbitrary: T)
    case SA_Top
    from SA_Top(3) show ?case
      by cases (auto intro: subtyping.SA_Top SA_Top)
  next
    case SA_refl_TVar show ?case by fact
  next
    case SA_trans_TVar
    thus ?case by (auto intro: subtyping.SA_trans_TVar)
  next
    case (SA_arrow Γ T1 S1 S2 T2)
    note SA_arrow' = SA_arrow
    from SA_arrow(5) show ?case
    proof cases
      case SA_Top
      with SA_arrow show ?thesis
        by (auto intro: subtyping.SA_Top wf_arrow elim: wf_subtypeE)
    next
      case (SA_arrow T1' T2')
      from SA_arrow SA_arrow' have "Γ  S1  S2 <: T1'  T2'"
        by (auto intro!: subtyping.SA_arrow intro: less(1) [of "T1"] less(1) [of "T2"])
      with SA_arrow show ?thesis by simp
    qed
  next
    case (SA_all Γ T1 S1 S2 T2)
    note SA_all' = SA_all
    from SA_all(5) show ?case
    proof cases
      case SA_Top
      with SA_all show ?thesis by (auto intro!:
            subtyping.SA_Top wf_all intro: wf_equallength elim: wf_subtypeE)
    next
      case (SA_all T1' T2')
      from SA_all SA_all' have "Γ  T1' <: S1"
        by - (rule less(1), simp_all)
      moreover from SA_all SA_all' have "TVarB T1'  Γ  S2 <: T2"
        by - (rule less(2) [of _ "[]", simplified], simp_all)
      with SA_all SA_all' have "TVarB T1'  Γ  S2 <: T2'"
        by - (rule less(1), simp_all)
      ultimately have "Γ  (∀<:S1. S2) <: (∀<:T1'. T2')"
        by (rule subtyping.SA_all)
      with SA_all show ?thesis by simp
    qed
  qed
  {
    case 1
    thus ?case using refl by (rule tr)
  next
    case 2
    from 2(1) show "Δ @ TVarB P  Γ  M <: N"
    proof (induct "Δ @ TVarB Q  Γ" M N arbitrary: Δ)
      case SA_Top
      with 2 show ?case by (auto intro!: subtyping.SA_Top
            intro: wf_equallength wfE_replace elim!: wf_subtypeE)
    next
      case SA_refl_TVar
      with 2 show ?case by (auto intro!: subtyping.SA_refl_TVar
            intro: wf_equallength wfE_replace elim!: wf_subtypeE)
    next
      case (SA_trans_TVar i U T)
      show ?case
      proof (cases "i < Δ")
        case True
        with SA_trans_TVar show ?thesis
          by (auto intro!: subtyping.SA_trans_TVar)
      next
        case False
        note False' = False
        show ?thesis
        proof (cases "i = Δ")
          case True
          from SA_trans_TVar have "(Δ @ [TVarB P]) @ Γ wf"
            by (auto elim!: wf_subtypeE)
          with Γ  P <: Q
          have "(Δ @ [TVarB P]) @ Γ  τ Δ @ [TVarB P] 0 P <: τ Δ @ [TVarB P] 0 Q"
            by (rule subtype_weaken')
          with SA_trans_TVar True False have "Δ @ TVarB P  Γ  τ (Suc Δ) 0 P <: T"
            by - (rule tr, simp+)
          with True and False and SA_trans_TVar show ?thesis
            by (auto intro!: subtyping.SA_trans_TVar)
        next
          case False
          with False' have "i - Δ = Suc (i - Δ - 1)" by arith
          with False False' SA_trans_TVar show ?thesis
            by (simp add: subtyping.SA_trans_TVar)
        qed
      qed
    next
      case SA_arrow
      thus ?case by (auto intro!: subtyping.SA_arrow)
    next
      case (SA_all T1 S1 S2 T2)
      thus ?case
        using subtyping.SA_all by auto
    qed
  }
qed

text ‹
In the proof of the preservation theorem presented in \secref{sec:evaluation},
we will also need a substitution theorem, which is proved by
induction on the subtyping derivation:
›

lemma substT_subtype: ― ‹A.10›
  assumes H: "Δ @ TVarB Q  Γ  S <: T"
  shows "Γ  P <: Q  Δ[0 τ P]e @ Γ  S[Δ τ P]τ <: T[Δ τ P]τ"
  using H
proof (induct "Δ @ TVarB Q  Γ" S T arbitrary: Δ)
  case (SA_Top S)
  then show ?case
    by (simp add: subtyping.SA_Top wfE_subst wf_subst wf_subtype)
next
  case (SA_refl_TVar i)
  then show ?case
    using subtype_refl wfE_subst wf_subst wf_subtype by presburger
next
  case §: (SA_trans_TVar i U T)
  show ?case 
  proof -
    have "Δ[0 τ P]e @ Γ  τ Δ 0 P <: T[Δ τ P]τ"
      if "i = Δ"
      using that § 
      by simp (smt (verit, best) substE_length subtype_trans(1) subtype_weaken'
          wf_subtype_env)
    moreover have "Δ[0 τ P]e @ Γ  TVar (i - Suc 0) <: T[Δ τ P]τ"
      if "Δ < i"
    proof (cases "i - Δ")
      case 0
      with that show ?thesis
        by linarith
    next
      case (Suc n)
      then have "i - Suc Δ = n"
        by simp
      with § SA_trans_TVar Suc show ?thesis by simp
    qed
    moreover have "Δ[0 τ P]e @ Γ  TVar i <: T[Δ τ P]τ"
      if "i < Δ"
    proof -
      have "Suc (Δ - Suc 0) = Δ"
        using that by linarith
      with that § show ?thesis
        by (simp add: SA_trans_TVar split: nat.split_asm)
    qed
    ultimately show ?thesis
      by auto
  qed
next
  case (SA_arrow T1 S1 S2 T2)
  then show ?case
    by (simp add: subtyping.SA_arrow)
next
  case §: (SA_all T1 S1 S2 T2)
  then show ?case
    by (simp add: SA_all)
qed

lemma subst_subtype:
  assumes H: "Δ @ VarB V  Γ  T <: U"
  shows "e 1 0 Δ @ Γ  τ 1 Δ T <: τ 1 Δ U"
  using H
proof (induct "Δ @ VarB V  Γ" T U arbitrary: Δ)
  case (SA_Top S)
  then show ?case
    by (simp add: subtyping.SA_Top wfE_subst wf_Top wf_subst)
next
  case (SA_refl_TVar i)
  then show ?case
    by (metis One_nat_def decE.simps decT.simps subtype_refl wfE_subst wf_Top
        wf_subst)
next
  case §: (SA_trans_TVar i U T)
  show ?case
  proof -
    have "Δ[0 τ Top]e @ Γ  Top <: T[Δ τ Top]τ" if "i = Δ"
      using that § by (simp split: nat.split_asm)
    moreover have "Δ[0 τ Top]e @ Γ  TVar (i - Suc 0) <: T[Δ τ Top]τ"
      if "Δ < i"
    proof (cases "i - Δ")
      case 0
      with that show ?thesis
        by linarith
    next
      case (Suc n)
      then have "i - Suc Δ = n"
        by simp
      with § SA_trans_TVar Suc show ?thesis by simp
    qed
    moreover have "Δ[0 τ Top]e @ Γ  TVar i <: T[Δ τ Top]τ"
      if "Δ > i"
    proof -
      have "Suc (Δ - Suc 0) = Δ"
        using that by linarith
      with that § show ?thesis
        by (simp add: SA_trans_TVar split: nat.split_asm)
    qed
    ultimately show ?thesis
      by auto
  qed
next
  case (SA_arrow T1 S1 S2 T2)
  then show ?case
    by (simp add: subtyping.SA_arrow)
next
  case §: (SA_all T1 S1 S2 T2)
  then show ?case
    by (simp add: SA_all)
qed


subsection ‹Typing›

text ‹
\label{sec:typing}
We are now ready to give a definition of the typing judgement Γ ⊢ t : T›.
›

inductive
  typing :: "env  trm  type  bool"    (‹_ / _ : _› [50, 50, 50] 50)
where
  T_Var: "Γ wf  Γi = VarB U  T = τ (Suc i) 0 U  Γ  Var i : T"
| T_Abs: "VarB T1  Γ  t2 : T2  Γ  (λ:T1. t2) : T1  τ 1 0 T2"
| T_App: "Γ  t1 : T11  T12  Γ  t2 : T11  Γ  t1  t2 : T12"
| T_TAbs: "TVarB T1  Γ  t2 : T2  Γ  (λ<:T1. t2) : (∀<:T1. T2)"
| T_TApp: "Γ  t1 : (∀<:T11. T12)  Γ  T2 <: T11 
    Γ  t1 τ T2 : T12[0 τ T2]τ"
| T_Sub: "Γ  t : S  Γ  S <: T  Γ  t : T"

text ‹
Note that in the rule T_Var›, the indices of the type @{term U} looked up in
the context @{term Γ} need to be incremented in order for the type to be well-formed
with respect to @{term Γ}. In the rule T_Abs›, the type @{term "T2"} of the
abstraction body @{term "t2"} may not contain the variable with index 0›,
since it is a term variable. To compensate for the disappearance of the context
element @{term "VarB T1"} in the conclusion of thy typing rule, the indices of all
free type variables in @{term "T2"} have to be decremented by 1›.
›

theorem wf_typeE1:
  assumes H: "Γ  t : T"
  shows "Γ wf" using H
  by induct (blast elim: well_formedE_cases)+

theorem wf_typeE2:
  assumes H: "Γ  t : T"
  shows "Γ wf T" using H
proof induct
  case (T_Var Γ i U T)
  then show ?case
    by (simp add: wf_liftB)
next
  case (T_Abs T1 Γ t2 T2)
  then have "Γ wf T2[0 τ Top]τ"
    by (metis append_Nil list.size(3) substE.simps(1) wf_Top wf_subst)
  with T_Abs wf_arrow wf_typeE1 show ?case
    by (metis One_nat_def decT.simps(1,2) type_ofB.simps(1) well_formedE_cases)
next
  case (T_App Γ t1 T11 T12 t2)
  then show ?case
    using well_formed_cases(3) by blast
next
  case (T_TAbs T1 Γ t2 T2)
  then show ?case
    by (metis type_ofB.simps(2) well_formedE_cases wf_all wf_typeE1)
next
  case (T_TApp Γ t1 T11 T12 T2)
  then show ?case
    by (metis append_Nil list.size(3) substE.simps(1) well_formed_cases(4) wf_subst
        wf_subtype)
next
  case (T_Sub Γ t S T)
  then show ?case
    by (auto elim: wf_subtypeE)
qed
 
text ‹
Like for the subtyping judgement, we can again prove that all types and contexts
involved in a typing judgement are well-formed:
›
lemma wf_type_conj: "Γ  t : T  Γ wf  Γ wf T"
  by (frule wf_typeE1, drule wf_typeE2) iprover

text ‹
The narrowing theorem for the typing judgement states that replacing the type
of a variable in the context by a subtype preserves typability:
›

lemma narrow_type: ― ‹A.7›
  assumes H: "Δ @ TVarB Q  Γ  t : T"
  shows "Γ  P <: Q  Δ @ TVarB P  Γ  t : T"
  using H
proof (induct "Δ @ TVarB Q  Γ" t T arbitrary: Δ)
  case §: (T_Var i U T)
  show ?case
  proof (intro T_Var)
    show "Δ @ TVarB P  Γ wf"
      using §
      by (metis is_TVarB.simps(2) type_ofB.simps(2) wfE_replace wf_subtypeE)
  next
    show "(Δ @ TVarB P  Γ)i = VarB U"
    proof (cases "i < Δ")
      case True
      with § show ?thesis
        by simp
    next
      case False
      with § show ?thesis
        by (simp split: nat.splits)
    qed
  next
    show "T = τ (Suc i) 0 U"
      by (simp add: "§.hyps")
  qed
next
  case (T_Abs T1 t2 T2)
  then show ?case
    using typing.T_Abs by auto
next
  case (T_TApp t1 T11 T12 T2)
  then show ?case
    using subtype_trans(2) typing.T_TApp by blast
next
  case (T_Sub t S T)
  then show ?case
    using subtype_trans(2) typing.T_Sub by blast
qed (auto intro: typing.intros)

lemma subtype_refl':
  assumes t: "Γ  t : T"
  shows "Γ  T <: T"
  using subtype_refl t wf_typeE1 wf_typeE2 by blast

lemma Abs_type: ― ‹A.13(1)›
  assumes H: "Γ  (λ:S. s) : T"
  shows "Γ  T <: U  U' 
    (S'. Γ  U <: S  VarB S  Γ  s : S' 
      Γ  τ 1 0 S' <: U'  P)  P"
  using H
proof (induct Γ "λ:S. s" T arbitrary: U U' S s P)
  case (T_Abs T1 Γ t2 T2)
  from Γ  T1  τ 1 0 T2 <: U  U'
  obtain ty1: "Γ  U <: T1" and ty2: "Γ  τ 1 0 T2 <: U'"
    by cases simp_all
  from ty1 VarB T1  Γ  t2 : T2 ty2
  show ?case by (rule T_Abs)
next
  case (T_Sub Γ S' T)
  from Γ  S' <: T and Γ  T <: U  U'
  have "Γ  S' <: U  U'" by (rule subtype_trans(1))
  then show ?case
    by (rule T_Sub) (rule T_Sub(5))
qed

lemma Abs_type':
  assumes H: "Γ  (λ:S. s) : U  U'"
    and R: "S'. Γ  U <: S  VarB S  Γ  s : S' 
    Γ  τ 1 0 S' <: U'  P"
  shows "P"
  using Abs_type H R subtype_refl' by blast

lemma TAbs_type: ― ‹A.13(2)›
  assumes H: "Γ  (λ<:S. s) : T"
  shows "Γ  T <: (∀<:U. U') 
    (S'. Γ  U <: S  TVarB U  Γ  s : S' 
      TVarB U  Γ  S' <: U'  P)  P"
  using H
proof (induct Γ "λ<:S. s" T arbitrary: U U' S s P)
  case (T_TAbs T1 Γ t2 T2)
  from Γ  (∀<:T1. T2) <: (∀<:U. U')
  obtain ty1: "Γ  U <: T1" and ty2: "TVarB U  Γ  T2 <: U'"
    by cases simp_all
  from TVarB T1  Γ  t2 : T2
  have "TVarB U  Γ  t2 : T2" using ty1
    by (rule narrow_type [of "[]", simplified])
  with ty1 show ?case using ty2 by (rule T_TAbs)
next
  case (T_Sub Γ S' T)
  from Γ  S' <: T and Γ  T <: (∀<:U. U')
  have "Γ  S' <: (∀<:U. U')" by (rule subtype_trans(1))
  then show ?case
    by (rule T_Sub) (rule T_Sub(5))
qed

lemma TAbs_type':
  assumes H: "Γ  (λ<:S. s) : (∀<:U. U')"
    and R: "S'. Γ  U <: S  TVarB U  Γ  s : S' 
    TVarB U  Γ  S' <: U'  P"
  shows "P" using H subtype_refl' [OF H]
  by (rule TAbs_type) (rule R)

lemma T_eq: "Γ  t : T  T = T'  Γ  t : T'" by simp

text ‹
The weakening theorem states that inserting a binding @{term B}
does not affect typing:
›

lemma type_weaken:
  assumes H: "Δ @ Γ  t : T"
  shows "Γ wfB B 
    e 1 0 Δ @ B  Γ   1 Δ t : τ 1 Δ T" using H
proof (induct "Δ @ Γ" t T arbitrary: Δ)
  case §: (T_Var i U T)
  show ?case
  proof -
    have "e (Suc 0) 0 Δ @ B  Γ  Var i : τ (Suc 0) Δ T"
      if "i < Δ"
      using § that
      by (intro T_Var) (auto simp: elim!: wfE_weaken)
    moreover have "e (Suc 0) 0 Δ @ B  Γ  Var (Suc i) : τ (Suc 0) Δ T"
      if "¬ i < Δ"
      using § that
      by (intro T_Var) (auto simp: Suc_diff_le elim!: wfE_weaken)
    ultimately show ?thesis
      by auto
  qed
next
  case (T_Abs T1 t2 T2)
  then show ?case
    using typing.T_Abs by simp
next
  case (T_App t1 T11 T12 t2)
  then show ?case
    using typing.T_App by force
next
  case (T_TAbs T1 t2 T2)
  then show ?case
    using typing.T_TAbs by force
next
  case §: (T_TApp t1 T11 T12 T2)
  show ?case
  proof (cases Δ)
    case Nil
    with § liftT_substT_strange [of _ 0] show ?thesis
     apply simp
      by (metis One_nat_def T_TApp append_Nil liftE.simps(1) list.size(3) subtype_weaken)
  next
    case (Cons a list)
    with § show ?thesis
    by (metis T_TApp diff_Suc_1' diff_Suc_Suc length_Cons lift.simps(5) liftT.simps(4)
        liftT_substT' subtype_weaken zero_less_Suc)
  qed
next
  case (T_Sub t S T)
  with subtype_weaken typing.T_Sub show ?case
    by blast
qed

text ‹
We can strengthen this result, so as to mean that concatenating a new context
@{term Δ} to the context @{term Γ} preserves typing:
›

lemma type_weaken': ― ‹A.5(6)›
  "Γ  t : T  Δ @ Γ wf  Δ @ Γ   Δ 0 t : τ Δ 0 T"
proof (induct Δ)
  case Nil
  then show ?case
    by simp
next
  case (Cons a Δ)
  with type_weaken [where B=a, of "[]"] show ?case
    by (fastforce simp: elim!: well_formedE_cases)
qed

text ‹
This property is proved by structural induction on the context @{term Δ},
using the previous result in the induction step. In the proof of the preservation
theorem, we will need two substitution theorems for term and type variables,
both of which are proved by induction on the typing derivation.
Since term and type variables are stored in the same context, we again have to
decrement the free type variables in @{term Δ} and @{term T} by 1›
in the substitution rule for term variables in order to compensate for the
disappearance of the variable.
›

theorem subst_type: ― ‹A.8›
  assumes H: "Δ @ VarB U  Γ  t : T"
  shows "Γ  u : U 
    e 1 0 Δ @ Γ  (subst t (length Δ) u) : τ 1 Δ T" using H
proof (induct "Δ @ VarB U  Γ" t T arbitrary: Δ)
  case §: (T_Var i U T)
  show ?case
  proof -
    have "Δ[0 τ Top]e @ Γ   Δ 0 u : T[Δ τ Top]τ"
      if "i = Δ"
      using § that type_weaken' wfE_subst wf_Top by fastforce
    moreover have "Δ[0 τ Top]e @ Γ  Var (i - Suc 0) : T[Δ τ Top]τ"
      if "Δ < i"
      using § that
      by (simp split: nat_diff_split_asm nat.split_asm add: T_Var wfE_subst wf_Top)
    moreover have "Δ[0 τ Top]e @ Γ  Var i : T[Δ τ Top]τ"
      if "Δ > i"
    proof -
      have "Suc (Δ - Suc 0) = Δ"
        using that by force
      then show ?thesis
        using § that wfE_subst wf_Top by (intro T_Var) auto
  qed
    ultimately show ?thesis
      by auto
  qed
next
  case §: (T_Abs T1 t2 T2)
  then show ?case
    by (simp add: T_Abs [THEN T_eq] substT_substT [symmetric])
next
  case (T_App t1 T11 T12 t2)
  then show ?case
    by (simp add: typing.T_App)
next
  case §: (T_TAbs T1 t2 T2)
  then show ?case
    by (simp add: typing.T_TAbs)
next
  case §: (T_TApp t1 T11 T12 T2)
  then show ?case
    by (auto intro!: T_TApp [THEN T_eq] dest: subst_subtype simp flip: substT_substT)
next
  case (T_Sub t S T)
  then show ?case
    using subst_subtype typing.T_Sub by blast
qed

theorem substT_type: ― ‹A.11›
  assumes H: "Δ @ TVarB Q  Γ  t : T"
  shows "Γ  P <: Q 
    Δ[0 τ P]e @ Γ  t[Δ τ P] : T[Δ τ P]τ" using H
proof (induct "Δ @ TVarB Q  Γ" t T arbitrary: Δ)
  case §: (T_Var i U T)
  show ?case
  proof -
    have "Δ[0 τ P]e @ Γ  Var (i - Suc 0) : T[Δ τ P]τ"
      if "Δ < i"
      using § that
      by (simp split: nat_diff_split_asm nat.split_asm add: T_Var wfE_subst wf_subtype)
    moreover have "Δ[0 τ P]e @ Γ  Var i : T[Δ τ P]τ"
      if "Δ = i"
      using § that by (intro T_Var [where U="(U[Δ - Suc i τ P]τ)"]) auto
    moreover have "Δ[0 τ P]e @ Γ  Var i : T[Δ τ P]τ"
      if "Δ > i"
    proof -
      have "Suc (Δ - Suc 0) = Δ"
        using that by auto
      with § that show ?thesis
        by (simp add: T_Var wfE_subst wf_subtype)
    qed
    ultimately show ?thesis
      by fastforce
  qed
next
  case §: (T_Abs T1 t2 T2)
  then show ?case
    by (simp add: T_Abs [THEN T_eq] substT_substT [symmetric])
next
  case (T_TApp t1 T11 T12 T2)
  then show ?case
    using substT_substT[of "0" "Δ" T12 P T2] substT_subtype
      typing.T_TApp[of _ _ _ "T12[Suc Δ τ P]τ" "T2[Δ τ P]τ"]
    by auto
next
  case (T_Sub t S T)
  then show ?case
    using substT_subtype typing.T_Sub by blast
qed (auto simp: typing.T_App typing.T_TAbs)


subsection ‹Evaluation›

text ‹
\label{sec:evaluation}
For the formalization of the evaluation strategy, it is useful to first define
a set of {\it canonical values} that are not evaluated any further. The canonical
values of call-by-value \fsub{} are exactly the abstractions over term and type variables:
›

inductive_set
  "value" :: "trm set"
where
  Abs: "(λ:T. t)  value"
| TAbs: "(λ<:T. t)  value"

text ‹
The notion of a @{term value} is now used in the defintion of the evaluation
relation \mbox{t ⟼ t'›}. There are several ways for defining this evaluation
relation: Aydemir et al.\ cite"PoplMark" advocate the use of {\it evaluation
contexts} that allow to separate the description of the ``immediate'' reduction rules,
i.e.\ $\beta$-reduction, from the description of the context in which these reductions
may occur in. The rationale behind this approach is to keep the formalization more modular.
We will take a closer look at this style of presentation in section
\secref{sec:evaluation-ctxt}. For the rest of this section, we will use a different
approach: both the ``immediate'' reductions and the reduction context are described
within the same inductive definition, where the context is described by additional
congruence rules.
›

inductive
  eval :: "trm  trm  bool"  (infixl  50)
where
  E_Abs: "v2  value  (λ:T11. t12)  v2  t12[0  v2]"
| E_TAbs: "(λ<:T11. t12) τ T2  t12[0 τ T2]"
| E_App1: "t  t'  t  u  t'  u"
| E_App2: "v  value  t  t'  v  t  v  t'"
| E_TApp: "t  t'  t τ T  t' τ T"

text ‹
Here, the rules E_Abs› and E_TAbs› describe the ``immediate'' reductions,
whereas E_App1›, E_App2›, and E_TApp› are additional congruence
rules describing reductions in a context. The most important theorems of this section
are the {\it preservation} theorem, stating that the reduction of a well-typed term
does not change its type, and the {\it progress} theorem, stating that reduction of
a well-typed term does not ``get stuck'' -- in other words, every well-typed, closed
term @{term t} is either a value, or there is a term @{term t'} to which @{term t}
can be reduced. The preservation theorem
is proved by induction on the derivation of @{term "Γ  t : T"}, followed by a case
distinction on the last rule used in the derivation of @{term "t  t'"}.
›

theorem preservation: ― ‹A.20›
  assumes H: "Γ  t : T"
  shows "t  t'  Γ  t' : T" using H
proof (induct arbitrary: t')
  case (T_Var Γ i U T t')
  from Var i  t'
  show ?case by cases
next
  case (T_Abs T1 Γ t2 T2 t')
  from (λ:T1. t2)  t'
  show ?case by cases
next
  case (T_App Γ t1 T11 T12 t2 t')
  from t1  t2  t'
  show ?case
  proof cases
    case (E_Abs T11' t12)
    with T_App have "Γ  (λ:T11'. t12) : T11  T12" by simp
    then obtain S'
      where T11: "Γ  T11 <: T11'"
      and t12: "VarB T11'  Γ  t12 : S'"
      and S': "Γ  S'[0 τ Top]τ <: T12" by (rule Abs_type' [simplified]) blast
    from Γ  t2 : T11
    have "Γ  t2 : T11'" using T11 by (rule T_Sub)
    with t12 have "Γ  t12[0  t2] : S'[0 τ Top]τ"
      by (rule subst_type [where Δ="[]", simplified])
    hence "Γ  t12[0  t2] : T12" using S' by (rule T_Sub)
    with E_Abs show ?thesis by simp
  next
    case (E_App1 t'')
    from t1  t''
    have "Γ  t'' : T11  T12" by (rule T_App)
    hence "Γ  t''  t2 : T12" using Γ  t2 : T11
      by (rule typing.T_App)
    with E_App1 show ?thesis by simp
  next
    case (E_App2 t'')
    from t2  t''
    have "Γ  t'' : T11" by (rule T_App)
    with T_App(1) have "Γ  t1  t'' : T12"
      by (rule typing.T_App)
    with E_App2 show ?thesis by simp
  qed
next
  case (T_TAbs T1 Γ t2 T2 t')
  from (λ<:T1. t2)  t'
  show ?case by cases
next
  case (T_TApp Γ t1 T11 T12 T2 t')
  from t1 τ T2  t'
  show ?case
  proof cases
    case (E_TAbs T11' t12)
    with T_TApp have "Γ  (λ<:T11'. t12) : (∀<:T11. T12)" by simp
    then obtain S'
      where "TVarB T11  Γ  t12 : S'"
      and "TVarB T11  Γ  S' <: T12" by (rule TAbs_type') blast
    hence "TVarB T11  Γ  t12 : T12" by (rule T_Sub)
    hence "Γ  t12[0 τ T2] : T12[0 τ T2]τ" using T_TApp(3)
      by (rule substT_type [where Δ="[]", simplified])
    with E_TAbs show ?thesis by simp
  next
    case (E_TApp t'')
    from t1  t''
    have "Γ  t'' : (∀<:T11. T12)" by (rule T_TApp)
    hence "Γ  t'' τ T2 : T12[0 τ T2]τ" using Γ  T2 <: T11
      by (rule typing.T_TApp)
    with E_TApp show ?thesis by simp
  qed
next
  case (T_Sub Γ t S T t')
  from t  t'
  have "Γ  t' : S" by (rule T_Sub)
  then show ?case using Γ  S <: T
    by (rule typing.T_Sub)
qed

text ‹
The progress theorem is also proved by induction on the derivation of
@{term "[]  t : T"}. In the induction steps, we need the following two lemmas
about {\it canonical forms}
stating that closed values of types @{term "T1  T2"} and @{term "∀<:T1. T2"}
must be abstractions over term and type variables, respectively.
›

lemma Fun_canonical: ― ‹A.14(1)›
  assumes ty: "[]  v : T1  T2"
  shows "v  value  t S. v = (λ:S. t)" using ty
proof (induct "[]::env" v "T1  T2" arbitrary: T1 T2)
  case T_Abs
  show ?case by iprover
next
  case (T_App t1 T11 t2 T1 T2)
  from t1  t2  value
  show ?case by cases
next
  case (T_TApp t1 T11 T12 T2 T1 T2')
  from t1 τ T2  value
  show ?case by cases
next
  case (T_Sub t S T1 T2)
  from []  S <: T1  T2
  obtain S1 S2 where S: "S = S1  S2"
    by cases (auto simp add: T_Sub)
  show ?case by (rule T_Sub S)+
qed simp

lemma TyAll_canonical: ― ‹A.14(3)›
  assumes ty: "[]  v : (∀<:T1. T2)"
  shows "v  value  t S. v = (λ<:S. t)" using ty
proof (induct "[]::env" v "∀<:T1. T2" arbitrary: T1 T2)
  case (T_App t1 T11 t2 T1 T2)
  from t1  t2  value
  show ?case by cases
next
  case T_TAbs
  show ?case by iprover
next
  case (T_TApp t1 T11 T12 T2 T1 T2')
  from t1 τ T2  value
  show ?case by cases
next
  case (T_Sub t S T1 T2)
  from []  S <: (∀<:T1. T2)
  obtain S1 S2 where S: "S = (∀<:S1. S2)"
    by cases (auto simp add: T_Sub)
  show ?case by (rule T_Sub S)+
qed simp

theorem progress:
  assumes ty: "[]  t : T"
  shows "t  value  (t'. t  t')" using ty
proof (induct "[]::env" t T)
  case T_Var
  thus ?case by simp
next
  case T_Abs
  from value.Abs show ?case ..
next
  case (T_App t1 T11 T12 t2)
  hence "t1  value  (t'. t1  t')" by simp
  thus ?case
  proof
    assume t1_val: "t1  value"
    with T_App obtain t S where t1: "t1 = (λ:S. t)"
      by (auto dest!: Fun_canonical)
    from T_App have "t2  value  (t'. t2  t')" by simp
    thus ?thesis
    proof
      assume "t2  value"
      with t1 have "t1  t2  t[0  t2]"
        by simp (rule eval.intros)
      thus ?thesis by iprover
    next
      assume "t'. t2  t'"
      then obtain t' where "t2  t'" by iprover
      with t1_val have "t1  t2  t1  t'" by (rule eval.intros)
      thus ?thesis by iprover
    qed
  next
    assume "t'. t1  t'"
    then obtain t' where "t1  t'" ..
    hence "t1  t2  t'  t2" by (rule eval.intros)
    thus ?thesis by iprover
  qed
next
  case T_TAbs
  from value.TAbs show ?case ..
next
  case (T_TApp t1 T11 T12 T2)
  hence "t1  value  (t'. t1  t')" by simp
  thus ?case
  proof
    assume "t1  value"
    with T_TApp obtain t S where "t1 = (λ<:S. t)"
      by (auto dest!: TyAll_canonical)
    hence "t1 τ T2  t[0 τ T2]" by simp (rule eval.intros)
    thus ?thesis by iprover
  next
    assume "t'. t1  t'"
    then obtain t' where "t1  t'" ..
    hence "t1 τ T2  t' τ T2" by (rule eval.intros)
    thus ?thesis by iprover
  qed
next
  case (T_Sub t S T)
  show ?case by (rule T_Sub)
qed

end