Theory POPLmarkRecord

(*  Title:      POPLmark/POPLmarkRecord.thy
    Author:     Stefan Berghofer, TU Muenchen, 2005
*)

theory POPLmarkRecord
imports Basis
begin

section ‹Extending the calculus with records›

text ‹
\label{sec:record-calculus}
We now describe how the calculus introduced in the previous section can
be extended with records. An important point to note is that many of the
definitions and proofs developed for the simple calculus can be reused.
›


subsection ‹Types and Terms›

text ‹
In order to represent records, we also need a type of {\it field names}.
For this purpose, we simply use the type of {\it strings}. We extend the
datatype of types of System \fsub{} by a new constructor ‹RcdT›
representing record types.
›

type_synonym name = string

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

type_synonym fldT = "name × type"
type_synonym rcdT = "(name × type) list"

datatype binding = VarB type | TVarB type

type_synonym env = "binding list"

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 ‹
A record type is essentially an association list, mapping names of record fields
to their types.
The types of bindings and environments remain unchanged. The datatype ‹trm›
of terms is extended with three new constructors ‹Rcd›, ‹Proj›,
and ‹LET›, denoting construction of a new record, selection of
a specific field of a record (projection), and matching of a record against
a pattern, respectively. A pattern, represented by datatype ‹pat›,
can be either a variable matching any value of a given type, or a nested
record pattern. Due to the encoding of variables using de Bruijn indices,
a variable pattern only consists of a type.
›

datatype pat = PVar type | PRcd "(name × pat) list"

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)
  | Rcd "(name × trm) list"
  | Proj trm name  ("(_.._)" [90, 91] 90)
  | LET pat trm trm ("(LET (_ =/ _)/ IN (_))" 10)

type_synonym fld = "name × trm"
type_synonym rcd = "(name × trm) list"
type_synonym fpat = "name × pat"
type_synonym rpat = "(name × pat) list"

text ‹
In order to motivate the typing and evaluation rules for the ‹LET›, it is
important to note that an expression of the form
@{text [display] "LET PRcd [(l1, PVar T1), …, (ln, PVar Tn)] = Rcd [(l1, v1), …, (ln, vn)] IN t"}
can be treated like a nested abstraction ‹(λ:T1. … λ:Tn. t) ∙ v1 ∙ … ∙ vn›
›


subsection ‹Lifting and Substitution›

primrec psize :: "pat ⇒ nat" ("∥_∥p")
  and rsize :: "rpat ⇒ nat" ("∥_∥r")
  and fsize :: "fpat ⇒ nat" ("∥_∥f")
where
  "∥PVar T∥p = 1"
| "∥PRcd fs∥p = ∥fs∥r"
| "∥[]∥r = 0"
| "∥f ∷ fs∥r = ∥f∥f + ∥fs∥r"
| "∥(l, p)∥f = ∥p∥p"

primrec liftT :: "nat ⇒ nat ⇒ type ⇒ type" ("↑τ")
  and liftrT :: "nat ⇒ nat ⇒ rcdT ⇒ rcdT" ("↑rτ")
  and liftfT :: "nat ⇒ nat ⇒ fldT ⇒ fldT" ("↑fτ")
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)"
| "↑τ n k (RcdT fs) = RcdT (↑rτ n k fs)"
| "↑rτ n k [] = []"
| "↑rτ n k (f ∷ fs) = ↑fτ n k f ∷ ↑rτ n k fs"
| "↑fτ n k (l, T) = (l, ↑τ n k T)"

primrec liftp :: "nat ⇒ nat ⇒ pat ⇒ pat" ("↑p")
  and liftrp :: "nat ⇒ nat ⇒ rpat ⇒ rpat" ("↑rp")
  and liftfp :: "nat ⇒ nat ⇒ fpat ⇒ fpat" ("↑fp")
where
  "↑p n k (PVar T) = PVar (↑τ n k T)"
| "↑p n k (PRcd fs) = PRcd (↑rp n k fs)"
| "↑rp n k [] = []"
| "↑rp n k (f ∷ fs) = ↑fp n k f ∷ ↑rp n k fs"
| "↑fp n k (l, p) = (l, ↑p n k p)"

primrec lift :: "nat ⇒ nat ⇒ trm ⇒ trm" ("↑")
  and liftr :: "nat ⇒ nat ⇒ rcd ⇒ rcd" ("↑r")
  and liftf :: "nat ⇒ nat ⇒ fld ⇒ fld" ("↑f")
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"
| "↑ n k (Rcd fs) = Rcd (↑r n k fs)"
| "↑ n k (t..a) = (↑ n k t)..a"
| "↑ n k (LET p = t IN u) = (LET ↑p n k p = ↑ n k t IN ↑ n (k + ∥p∥p) u)"
| "↑r n k [] = []"
| "↑r n k (f ∷ fs) = ↑f n k f ∷ ↑r n k fs"
| "↑f n k (l, t) = (l, ↑ n k t)"

primrec substTT :: "type ⇒ nat ⇒ type ⇒ type"  ("_[_ ↦τ _]τ" [300, 0, 0] 300)
  and substrTT :: "rcdT ⇒ nat ⇒ type ⇒ rcdT"  ("_[_ ↦τ _]rτ" [300, 0, 0] 300)
  and substfTT :: "fldT ⇒ nat ⇒ type ⇒ fldT"  ("_[_ ↦τ _]fτ" [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]τ)"
| "(RcdT fs)[k ↦τ S]τ = RcdT (fs[k ↦τ S]rτ)"
| "[][k ↦τ S]rτ = []"
| "(f ∷ fs)[k ↦τ S]rτ = f[k ↦τ S]fτ ∷ fs[k ↦τ S]rτ"
| "(l, T)[k ↦τ S]fτ = (l, T[k ↦τ S]τ)"

primrec substpT :: "pat ⇒ nat ⇒ type ⇒ pat"  ("_[_ ↦τ _]p" [300, 0, 0] 300)
  and substrpT :: "rpat ⇒ nat ⇒ type ⇒ rpat"  ("_[_ ↦τ _]rp" [300, 0, 0] 300)
  and substfpT :: "fpat ⇒ nat ⇒ type ⇒ fpat"  ("_[_ ↦τ _]fp" [300, 0, 0] 300)
where
  "(PVar T)[k ↦τ S]p = PVar (T[k ↦τ S]τ)"
| "(PRcd fs)[k ↦τ S]p = PRcd (fs[k ↦τ S]rp)"
| "[][k ↦τ S]rp = []"
| "(f ∷ fs)[k ↦τ S]rp = f[k ↦τ S]fp ∷ fs[k ↦τ S]rp"
| "(l, p)[k ↦τ S]fp = (l, p[k ↦τ S]p)"

primrec decp :: "nat ⇒ nat ⇒ pat ⇒ pat"  ("↓p")
where
  "↓p 0 k p = p"
| "↓p (Suc n) k p = ↓p n k (p[k ↦τ Top]p)"

text ‹
In addition to the lifting and substitution functions already needed for the
basic calculus, we also have to define lifting and substitution functions
for patterns, which we denote by @{term "↑p n k p"} and @{term "T[k ↦τ S]p"},
respectively. The extension of the existing lifting and substitution
functions to records is fairly standard.
›

primrec subst :: "trm ⇒ nat ⇒ trm ⇒ trm"  ("_[_ ↦ _]" [300, 0, 0] 300)
  and substr :: "rcd ⇒ nat ⇒ trm ⇒ rcd"  ("_[_ ↦ _]r" [300, 0, 0] 300)
  and substf :: "fld ⇒ nat ⇒ trm ⇒ fld"  ("_[_ ↦ _]f" [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] ∙τ T[k ↦τ Top]τ"
| "(λ:T. t)[k ↦ s] = (λ:T[k ↦τ Top]τ. t[k+1 ↦ s])"
| "(λ<:T. t)[k ↦ s] = (λ<:T[k ↦τ Top]τ. t[k+1 ↦ s])"
| "(Rcd fs)[k ↦ s] = Rcd (fs[k ↦ s]r)"
| "(t..a)[k ↦ s] = (t[k ↦ s])..a"
| "(LET p = t IN u)[k ↦ s] = (LET ↓p 1 k p = t[k ↦ s] IN u[k + ∥p∥p ↦ s])"
| "[][k ↦ s]r = []"
| "(f ∷ fs)[k ↦ s]r = f[k ↦ s]f ∷ fs[k ↦ s]r"
| "(l, t)[k ↦ s]f = (l, t[k ↦ s])"

text ‹
Note that the substitution function on terms is defined simultaneously
with a substitution function @{term "fs[k ↦ s]r"} on records (i.e.\ lists
of fields), and a substitution function @{term "f[k ↦ s]f"} on fields.
To avoid conflicts with locally bound variables, we have to add an offset
@{term "∥p∥p"} to @{term k} when performing substitution in the body of
the ‹LET› binder, where @{term "∥p∥p"} is the number of variables
in the pattern @{term p}.
›

primrec substT :: "trm ⇒ nat ⇒ type ⇒ trm"  ("_[_ ↦τ _]" [300, 0, 0] 300)
  and substrT :: "rcd ⇒ nat ⇒ type ⇒ rcd"  ("_[_ ↦τ _]r" [300, 0, 0] 300)
  and substfT :: "fld ⇒ nat ⇒ type ⇒ fld"  ("_[_ ↦τ _]f" [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])"
| "(Rcd fs)[k ↦τ S] = Rcd (fs[k ↦τ S]r)"
| "(t..a)[k ↦τ S] = (t[k ↦τ S])..a"
| "(LET p = t IN u)[k ↦τ S] =
     (LET p[k ↦τ S]p = t[k ↦τ S] IN u[k + ∥p∥p ↦τ S])"
| "[][k ↦τ S]r = []"
| "(f ∷ fs)[k ↦τ S]r = f[k ↦τ S]f ∷ fs[k ↦τ S]r"
| "(l, t)[k ↦τ S]f = (l, t[k ↦τ S])"

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"

text ‹
For the formalization of the reduction
rules for ‹LET›, we need a function \mbox{‹t[k ↦s us]›}
for simultaneously substituting terms @{term us} for variables with
consecutive indices:
›

primrec substs :: "trm ⇒ nat ⇒ trm list ⇒ trm"  ("_[_ ↦s _]" [300, 0, 0] 300)
where
  "t[k ↦s []] = t"
| "t[k ↦s u ∷ us] = t[k + ∥us∥ ↦ u][k ↦s us]"

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

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

primrec decrT :: "nat ⇒ nat ⇒ rcdT ⇒ rcdT"  ("↓rτ")
where
  "↓rτ 0 k fTs = fTs"
| "↓rτ (Suc n) k fTs = ↓rτ n k (fTs[k ↦τ Top]rτ)"

text ‹
The lemmas about substitution and lifting are very similar to those needed
for the simple calculus without records, with the difference that most
of them have to be proved simultaneously with a suitable property for
records.
›

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⟩)"
  apply (induct Γ arbitrary: i)
  apply simp
  apply simp
  apply (case_tac i)
  apply simp
  apply simp
  done

lemma substE_nth [simp]:
  "(Γ[0 ↦τ T]e)⟨i⟩ = map_option (mapB (λU. U[∥Γ∥ - i - 1 ↦τ T]τ)) (Γ⟨i⟩)"
  apply (induct Γ arbitrary: i)
  apply simp
  apply simp
  apply (case_tac i)
  apply simp
  apply simp
  done

lemma liftT_liftT [simp]:
  "i ≤ j ⟹ j ≤ i + m ⟹ ↑τ n j (↑τ m i T) = ↑τ (m + n) i T"
  "i ≤ j ⟹ j ≤ i + m ⟹ ↑rτ n j (↑rτ m i rT) = ↑rτ (m + n) i rT"
  "i ≤ j ⟹ j ≤ i + m ⟹ ↑fτ n j (↑fτ m i fT) = ↑fτ (m + n) i fT"
  by (induct T and rT and fT arbitrary: i j m n and i j m n and i j m n
    rule: liftT.induct liftrT.induct liftfT.induct) simp_all

lemma liftT_liftT' [simp]:
  "i + m ≤ j ⟹ ↑τ n j (↑τ m i T) = ↑τ m i (↑τ n (j - m) T)"
  "i + m ≤ j ⟹ ↑rτ n j (↑rτ m i rT) = ↑rτ m i (↑rτ n (j - m) rT)"
  "i + m ≤ j ⟹ ↑fτ n j (↑fτ m i fT) = ↑fτ m i (↑fτ n (j - m) fT)"
  apply (induct T and rT and fT arbitrary: i j m n and i j m n and i j m n
    rule: liftT.induct liftrT.induct liftfT.induct)
  apply simp_all
  apply arith
  apply (subgoal_tac "Suc j - m = Suc (j - m)")
  apply simp
  apply arith
  done

lemma lift_size [simp]:
  "size (↑τ n k T) = size T"
  "size_list (size_prod (λx. 0) size) (↑rτ n k rT) = size_list (size_prod (λx. 0) size) rT"
  "size_prod (λx. 0) size (↑fτ n k fT) = size_prod (λx. 0) size fT"
  by (induct T and rT and fT arbitrary: k and k and k
    rule: liftT.induct liftrT.induct liftfT.induct) simp_all

lemma liftT0 [simp]:
  "↑τ 0 i T = T"
  "↑rτ 0 i rT = rT"
  "↑fτ 0 i fT = fT"
  by (induct T and rT and fT arbitrary: i and i and i
    rule: liftT.induct liftrT.induct liftfT.induct) simp_all

lemma liftp0 [simp]:
  "↑p 0 i p = p"
  "↑rp 0 i fs = fs"
  "↑fp 0 i f = f"
  by (induct p and fs and f arbitrary: i and i and i
    rule: liftp.induct liftrp.induct liftfp.induct) simp_all

lemma lift0 [simp]:
  "↑ 0 i t = t"
  "↑r 0 i fs = fs"
  "↑f 0 i f = f"
  by (induct t and fs and f arbitrary: i and i and i
    rule: lift.induct liftr.induct liftf.induct) simp_all

theorem substT_liftT [simp]:
  "k ≤ k' ⟹ k' < k + n ⟹ (↑τ n k T)[k' ↦τ U]τ = ↑τ (n - 1) k T"
  "k ≤ k' ⟹ k' < k + n ⟹ (↑rτ n k rT)[k' ↦τ U]rτ = ↑rτ (n - 1) k rT"
  "k ≤ k' ⟹ k' < k + n ⟹ (↑fτ n k fT)[k' ↦τ U]fτ = ↑fτ (n - 1) k fT"
  by (induct T and rT and fT arbitrary: k k' and k k' and k k'
    rule: liftT.induct liftrT.induct liftfT.induct) simp_all

theorem liftT_substT [simp]:
  "k ≤ k' ⟹ ↑τ n k (T[k' ↦τ U]τ) = ↑τ n k T[k' + n ↦τ U]τ"
  "k ≤ k' ⟹ ↑rτ n k (rT[k' ↦τ U]rτ) = ↑rτ n k rT[k' + n ↦τ U]rτ"
  "k ≤ k' ⟹ ↑fτ n k (fT[k' ↦τ U]fτ) = ↑fτ n k fT[k' + n ↦τ U]fτ"
  apply (induct T and rT and fT arbitrary: k k' and k k' and k k'
    rule: liftT.induct liftrT.induct liftfT.induct)
  apply simp_all
  done

theorem liftT_substT' [simp]:
  "k' < k ⟹
     ↑τ n k (T[k' ↦τ U]τ) = ↑τ n (k + 1) T[k' ↦τ ↑τ n (k - k') U]τ"
  "k' < k ⟹
     ↑rτ n k (rT[k' ↦τ U]rτ) = ↑rτ n (k + 1) rT[k' ↦τ ↑τ n (k - k') U]rτ"
  "k' < k ⟹
     ↑fτ n k (fT[k' ↦τ U]fτ) = ↑fτ n (k + 1) fT[k' ↦τ ↑τ n (k - k') U]fτ"
  apply (induct T and rT and fT arbitrary: k k' and k k' and k k'
    rule: liftT.induct liftrT.induct liftfT.induct)
  apply simp_all
  apply arith
  done

lemma liftT_substT_Top [simp]:
  "k ≤ k' ⟹ ↑τ n k' (T[k ↦τ Top]τ) = ↑τ n (Suc k') T[k ↦τ Top]τ"
  "k ≤ k' ⟹ ↑rτ n k' (rT[k ↦τ Top]rτ) = ↑rτ n (Suc k') rT[k ↦τ Top]rτ"
  "k ≤ k' ⟹ ↑fτ n k' (fT[k ↦τ Top]fτ) = ↑fτ n (Suc k') fT[k ↦τ Top]fτ"
  apply (induct T and rT and fT arbitrary: k k' and k k' and k k'
    rule: liftT.induct liftrT.induct liftfT.induct)
  apply simp_all
  apply arith
  done

theorem liftE_substE [simp]:
  "k ≤ k' ⟹ ↑e n k (Γ[k' ↦τ U]e) = ↑e n k Γ[k' + n ↦τ U]e"
  apply (induct Γ arbitrary: k k' and k k' and k k')
  apply simp_all
  apply (case_tac a)
  apply (simp_all add: ac_simps)
  done

lemma liftT_decT [simp]:
  "k ≤ k' ⟹ ↑τ n k' (↓τ m k T) = ↓τ m k (↑τ n (m + k') T)"
  by (induct m arbitrary: T) simp_all

lemma liftT_substT_strange:
  "↑τ n k T[n + k ↦τ U]τ = ↑τ n (Suc k) T[k ↦τ ↑τ n 0 U]τ"
  "↑rτ n k rT[n + k ↦τ U]rτ = ↑rτ n (Suc k) rT[k ↦τ ↑τ n 0 U]rτ"
  "↑fτ n k fT[n + k ↦τ U]fτ = ↑fτ n (Suc k) fT[k ↦τ ↑τ n 0 U]fτ"
  apply (induct T and rT and fT arbitrary: n k and n k and n k
    rule: liftT.induct liftrT.induct liftfT.induct)
  apply simp_all
  apply (thin_tac "⋀x. PROP P x" for P :: "_ ⇒ prop")
  apply (drule_tac x=n in meta_spec)
  apply (drule_tac x="Suc k" in meta_spec)
  apply simp
  done

lemma liftp_liftp [simp]:
  "k ≤ k' ⟹ k' ≤ k + n ⟹ ↑p n' k' (↑p n k p) = ↑p (n + n') k p"
  "k ≤ k' ⟹ k' ≤ k + n ⟹ ↑rp n' k' (↑rp n k rp) = ↑rp (n + n') k rp"
  "k ≤ k' ⟹ k' ≤ k + n ⟹ ↑fp n' k' (↑fp n k fp) = ↑fp (n + n') k fp"
  by (induct p and rp and fp arbitrary: k k' and k k' and k k'
    rule: liftp.induct liftrp.induct liftfp.induct) simp_all

lemma liftp_psize[simp]:
  "∥↑p n k p∥p = ∥p∥p"
  "∥↑rp n k fs∥r = ∥fs∥r"
  "∥↑fp n k f∥f = ∥f∥f"
  by (induct p and fs and f rule: liftp.induct liftrp.induct liftfp.induct) simp_all

lemma lift_lift [simp]:
  "k ≤ k' ⟹ k' ≤ k + n ⟹ ↑ n' k' (↑ n k t) = ↑ (n + n') k t"
  "k ≤ k' ⟹ k' ≤ k + n ⟹ ↑r n' k' (↑r n k fs) = ↑r (n + n') k fs"
  "k ≤ k' ⟹ k' ≤ k + n ⟹ ↑f n' k' (↑f n k f) = ↑f (n + n') k f"
 by (induct t and fs and f arbitrary: k k' and k k' and k k'
   rule: lift.induct liftr.induct liftf.induct) simp_all

lemma liftE_liftE [simp]:
  "k ≤ k' ⟹ k' ≤ k + n ⟹ ↑e n' k' (↑e n k Γ) = ↑e (n + n') k Γ"
  apply (induct Γ arbitrary: k k')
  apply simp_all
  apply (case_tac a)
  apply simp_all
  done

lemma liftE_liftE' [simp]:
  "i + m ≤ j ⟹ ↑e n j (↑e m i Γ) = ↑e m i (↑e n (j - m) Γ)"
  apply (induct Γ arbitrary: i j m n)
  apply simp_all
  apply (case_tac a)
  apply simp_all
  done

lemma substT_substT:
  "i ≤ j ⟹
     T[Suc j ↦τ V]τ[i ↦τ U[j - i ↦τ V]τ]τ = T[i ↦τ U]τ[j ↦τ V]τ"
  "i ≤ j ⟹
     rT[Suc j ↦τ V]rτ[i ↦τ U[j - i ↦τ V]τ]rτ = rT[i ↦τ U]rτ[j ↦τ V]rτ"
  "i ≤ j ⟹
     fT[Suc j ↦τ V]fτ[i ↦τ U[j - i ↦τ V]τ]fτ = fT[i ↦τ U]fτ[j ↦τ V]fτ"
  apply (induct T and rT and fT arbitrary: i j U V and i j U V and i j U V
    rule: liftT.induct liftrT.induct liftfT.induct)
  apply (simp_all add: diff_Suc split: nat.split)
  apply (thin_tac "⋀x. PROP P x" for P :: "_ ⇒ prop")
  apply (drule_tac x="Suc i" in meta_spec)
  apply (drule_tac x="Suc j" in meta_spec)
  apply simp
  done

lemma substT_decT [simp]:
  "k ≤ j ⟹ (↓τ i k T)[j ↦τ U]τ = ↓τ i k (T[i + j ↦τ U]τ)"
  by (induct i arbitrary: T j) (simp_all add: substT_substT [symmetric])

lemma substT_decT' [simp]:
  "i ≤ j ⟹ ↓τ k (Suc j) T[i ↦τ Top]τ = ↓τ k j (T[i ↦τ Top]τ)"
  by (induct k arbitrary: i j T) (simp_all add: substT_substT [of _ _ _ _ Top, simplified])

lemma substE_substE:
  "i ≤ j ⟹ Γ[Suc j ↦τ V]e[i ↦τ U[j - i ↦τ V]τ]e = Γ[i ↦τ U]e[j ↦τ V]e"
  apply (induct Γ)
  apply (case_tac [2] a)
  apply (simp_all add: substT_substT [symmetric])
  done

lemma substT_decE [simp]:
  "i ≤ j ⟹ ↓e k (Suc j) Γ[i ↦τ Top]e = ↓e k j (Γ[i ↦τ Top]e)"
  by (induct k arbitrary: i j Γ) (simp_all add: substE_substE [of _ _ _ _ Top, simplified])

lemma liftE_app [simp]: "↑e n k (Γ @ Δ) = ↑e n (k + ∥Δ∥) Γ @ ↑e n k Δ"
  by (induct Γ arbitrary: k) (simp_all add: ac_simps)

lemma substE_app [simp]:
  "(Γ @ Δ)[k ↦τ T]e = Γ[k + ∥Δ∥ ↦τ T]e @ Δ[k ↦τ T]e"
  by (induct Γ) (simp_all add: ac_simps)

lemma substs_app [simp]: "t[k ↦s ts @ us] = t[k + ∥us∥ ↦s ts][k ↦s us]"
  by (induct ts arbitrary: t k) (simp_all add: ac_simps)

theorem decE_Nil [simp]: "↓e n k [] = []"
  by (induct n) simp_all

theorem decE_Cons [simp]:
  "↓e n k (B ∷ Γ) = mapB (↓τ n (k + ∥Γ∥)) B ∷ ↓e n k Γ"
  apply (induct n arbitrary: B Γ)
  apply (case_tac B)
  apply (case_tac [3] B)
  apply simp_all
  done

theorem decE_app [simp]:
  "↓e n k (Γ @ Δ) = ↓e n (k + ∥Δ∥) Γ @ ↓e n k Δ"
  by (induct n arbitrary: Γ Δ) simp_all

theorem decT_liftT [simp]:
  "k ≤ k' ⟹ k' + m ≤ k + n ⟹ ↓τ m k' (↑τ n k Γ) = ↑τ (n - m) k Γ"
  apply (induct m arbitrary: n)
  apply (subgoal_tac [2] "k' + m ≤ k + (n - Suc 0)")
  apply simp_all
  done

theorem decE_liftE [simp]:
  "k ≤ k' ⟹ k' + m ≤ k + n ⟹ ↓e m k' (↑e n k Γ) = ↑e (n - m) k Γ"
  apply (induct Γ arbitrary: k k')
  apply (case_tac [2] a)
  apply simp_all
  done

theorem liftE0 [simp]: "↑e 0 k Γ = Γ"
  apply (induct Γ)
  apply (case_tac [2] a)
  apply simp_all
  done

lemma decT_decT [simp]: "↓τ n k (↓τ n' (k + n) T) = ↓τ (n + n') k T"
  by (induct n arbitrary: k T) simp_all

lemma decE_decE [simp]: "↓e n k (↓e n' (k + n) Γ) = ↓e (n + n') k Γ"
  by (induct n arbitrary: k Γ) simp_all

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

lemma liftrT_assoc_None [simp]: "(↑rτ n k fs⟨l⟩? = ⊥) = (fs⟨l⟩? = ⊥)"
  by (induct fs rule: list.induct) auto

lemma liftrT_assoc_Some: "fs⟨l⟩? = ⌊T⌋ ⟹ ↑rτ n k fs⟨l⟩? = ⌊↑τ n k T⌋"
  by (induct fs rule: list.induct) auto

lemma liftrp_assoc_None [simp]: "(↑rp n k fps⟨l⟩? = ⊥) = (fps⟨l⟩? = ⊥)"
  by (induct fps rule: list.induct) auto

lemma liftr_assoc_None [simp]: "(↑r n k fs⟨l⟩? = ⊥) = (fs⟨l⟩? = ⊥)"
  by (induct fs rule: list.induct) auto

lemma unique_liftrT [simp]: "unique (↑rτ n k fs) = unique fs"
  by (induct fs rule: list.induct) auto

lemma substrTT_assoc_None [simp]: "(fs[k ↦τ U]rτ⟨a⟩? = ⊥) = (fs⟨a⟩? = ⊥)"
  by (induct fs rule: list.induct) auto

lemma substrTT_assoc_Some [simp]:
  "fs⟨a⟩? = ⌊T⌋ ⟹ fs[k ↦τ U]rτ⟨a⟩? = ⌊T[k ↦τ U]τ⌋"
  by (induct fs rule: list.induct) auto

lemma substrT_assoc_None [simp]: "(fs[k ↦τ P]r⟨l⟩? = ⊥) = (fs⟨l⟩? = ⊥)"
  by (induct fs rule: list.induct) auto

lemma substrp_assoc_None [simp]: "(fps[k ↦τ U]rp⟨l⟩? = ⊥) = (fps⟨l⟩? = ⊥)"
  by (induct fps rule: list.induct) auto

lemma substr_assoc_None [simp]: "(fs[k ↦ u]r⟨l⟩? = ⊥) = (fs⟨l⟩? = ⊥)"
  by (induct fs rule: list.induct) auto

lemma unique_substrT [simp]: "unique (fs[k ↦τ U]rτ) = unique fs"
  by (induct fs rule: list.induct) auto

lemma liftrT_set: "(a, T) ∈ set fs ⟹ (a, ↑τ n k T) ∈ set (↑rτ n k fs)"
  by (induct fs rule: list.induct) auto

lemma liftrT_setD:
  "(a, T) ∈ set (↑rτ n k fs) ⟹ ∃T'. (a, T') ∈ set fs ∧ T = ↑τ n k T'"
  by (induct fs rule: list.induct) auto

lemma substrT_set: "(a, T) ∈ set fs ⟹ (a, T[k ↦τ U]τ) ∈ set (fs[k ↦τ U]rτ)"
  by (induct fs rule: list.induct) auto

lemma substrT_setD:
  "(a, T) ∈ set (fs[k ↦τ U]rτ) ⟹ ∃T'. (a, T') ∈ set fs ∧ T = T'[k ↦τ U]τ"
  by (induct fs rule: list.induct) auto


subsection ‹Well-formedness›

text ‹
The definition of well-formedness is extended with a rule stating that a
record type @{term "RcdT fs"} is well-formed, if for all fields @{term "(l, T)"}
contained in the list @{term fs}, the type @{term T} is well-formed, and
all labels @{term l} in @{term fs} are {\it unique}.
›

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)"
| wf_RcdT: "unique fs ⟹ ∀(l, T)∈set fs. Γ ⊢wf T ⟹ Γ ⊢wf RcdT fs"

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"

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

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⌋"
  apply (induct Γ arbitrary: Γ' T i)
  apply simp
  apply (auto split: nat.split_asm)
  apply (case_tac z)
  apply simp_all
  done

lemma wf_equallength:
  assumes H: "Γ ⊢wf T"
  shows "map is_TVarB Γ' = map is_TVarB Γ ⟹ Γ' ⊢wf T" using H
  apply (induct arbitrary: Γ')
  apply (auto intro: well_formed.intros dest: map_is_TVarb)+
  apply (fastforce intro: well_formed.intros)
  done

lemma wfE_replace:
  "Δ @ B ∷ Γ ⊢wf ⟹ Γ ⊢wfB B' ⟹ is_TVarB B' = is_TVarB B ⟹
     Δ @ B' ∷ Γ ⊢wf"
  apply (induct Δ)
  apply simp
  apply (erule wf_Cons)
  apply (erule well_formedE_cases)
  apply assumption
  apply simp
  apply (erule well_formedE_cases)
  apply (rule wf_Cons)
  apply (case_tac a)
  apply simp
  apply (rule wf_equallength)
  apply assumption
  apply simp
  apply simp
  apply (rule wf_equallength)
  apply assumption
  apply simp
  apply simp
  done

lemma wf_weaken:
  assumes H: "Δ @ Γ ⊢wf T"
  shows "↑e (Suc 0) 0 Δ @ B ∷ Γ ⊢wf ↑τ (Suc 0) ∥Δ∥ T"
  using H
  apply (induct "Δ @ Γ" T arbitrary: Δ)
  apply simp_all
  apply (rule conjI)
  apply (rule impI)
  apply (rule wf_TVar)
  apply simp
  apply (rule impI)
  apply (rule wf_TVar)
  apply (subgoal_tac "Suc i - ∥Δ∥ = Suc (i - ∥Δ∥)")
  apply simp
  apply arith
  apply (rule wf_Top)
  apply (rule wf_arrow)
  apply simp
  apply simp
  apply (rule wf_all)
  apply simp
  apply simp
  ― ‹records›
  apply (rule wf_RcdT)
  apply simp
  apply (rule ballpI)
  apply (drule liftrT_setD)
  apply (erule exE conjE)+
  apply (drule_tac x=l and y="T[∥Δ∥ ↦τ Top]τ" in bpspec)
  apply simp+
  done

lemma wf_weaken': "Γ ⊢wf T ⟹ Δ @ Γ ⊢wf ↑τ ∥Δ∥ 0 T"
  apply (induct Δ)
  apply simp_all
  apply (drule_tac B=a in wf_weaken [of "[]", simplified])
  apply simp
  done

lemma wfE_weaken: "Δ @ Γ ⊢wf ⟹ Γ ⊢wfB B ⟹ ↑e (Suc 0) 0 Δ @ B ∷ Γ ⊢wf"
  apply (induct Δ)
  apply simp
  apply (rule wf_Cons)
  apply assumption+
  apply simp
  apply (rule wf_Cons)
  apply (erule well_formedE_cases)
  apply (case_tac a)
  apply simp
  apply (rule wf_weaken)
  apply assumption
  apply simp
  apply (rule wf_weaken)
  apply assumption
  apply (erule well_formedE_cases)
  apply simp
  done

lemma wf_liftB:
  assumes H: "Γ ⊢wf"
  shows "Γ⟨i⟩ = ⌊VarB T⌋ ⟹ Γ ⊢wf ↑τ (Suc i) 0 T"
  using H
  apply (induct arbitrary: i)
  apply simp
  apply (simp split: nat.split_asm)
  apply (frule_tac B="VarB T" in wf_weaken [of "[]", simplified])
  apply simp+
  apply (rename_tac nat)
  apply (drule_tac x=nat in meta_spec)
  apply simp
  apply (frule_tac T="↑τ (Suc nat) 0 T" in wf_weaken [of "[]", simplified])
  apply simp
  done

theorem wf_subst:
  "Δ @ B ∷ Γ ⊢wf T ⟹ Γ ⊢wf U ⟹ Δ[0 ↦τ U]e @ Γ ⊢wf T[∥Δ∥ ↦τ U]τ"
  "∀(l, T) ∈ set (rT::rcdT). Δ @ B ∷ Γ ⊢wf T ⟹ Γ ⊢wf U ⟹
     ∀(l, T) ∈ set rT. Δ[0 ↦τ U]e @ Γ ⊢wf T[∥Δ∥ ↦τ U]τ"
  "Δ @ B ∷ Γ ⊢wf snd (fT::fldT) ⟹ Γ ⊢wf U ⟹
     Δ[0 ↦τ U]e @ Γ ⊢wf snd fT[∥Δ∥ ↦τ U]τ"
  apply (induct T and rT and fT arbitrary: Δ and Δ and Δ
    rule: liftT.induct liftrT.induct liftfT.induct)
  apply (rename_tac nat Δ)
  apply simp_all
  apply (rule conjI)
  apply (rule impI)
  apply (drule_tac Γ=Γ and Δ="Δ[0 ↦τ U]e" in wf_weaken')
  apply simp
  apply (rule impI conjI)+
  apply (erule well_formed_cases)
  apply (rule wf_TVar)
  apply (simp split: nat.split_asm)
  apply (subgoal_tac "∥Δ∥ ≤ nat - Suc 0")
  apply (rename_tac nata)
  apply (subgoal_tac "nat - Suc ∥Δ∥ = nata")
  apply (simp (no_asm_simp))
  apply arith
  apply arith
  apply (rule impI)
  apply (erule well_formed_cases)
  apply (rule wf_TVar)
  apply simp
  apply (rule wf_Top)
  apply (erule well_formed_cases)
  apply (rule wf_arrow)
  apply simp+
  apply (rename_tac type1 type2 Δ)
  apply (erule well_formed_cases)
  apply (rule wf_all)
  apply simp
  apply (thin_tac "⋀x. PROP P x" for P :: "_ ⇒ prop")
  apply (drule_tac x="TVarB type1 ∷ Δ" in meta_spec)
  apply simp
  apply (erule well_formed_cases)
  apply (rule wf_RcdT)
  apply simp
  apply (rule ballpI)
  apply (drule substrT_setD)
  apply (erule exE conjE)+
  apply (drule meta_spec)
  apply (drule meta_mp)
  apply assumption
  apply (thin_tac "∀x ∈ S. P x" for S P)
  apply (drule bpspec)
  apply assumption
  apply simp
  apply (simp add: split_paired_all)
  done

theorem wf_dec: "Δ @ Γ ⊢wf T ⟹ Γ ⊢wf ↓τ ∥Δ∥ 0 T"
  apply (induct Δ arbitrary: T)
  apply simp
  apply simp
  apply (drule wf_subst(1) [of "[]", simplified])
  apply (rule wf_Top)
  apply simp
  done

theorem wfE_subst: "Δ @ B ∷ Γ ⊢wf ⟹ Γ ⊢wf U ⟹ Δ[0 ↦τ U]e @ Γ ⊢wf"
  apply (induct Δ)
  apply simp
  apply (erule well_formedE_cases)
  apply assumption
  apply simp
  apply (case_tac a)
  apply (erule well_formedE_cases)
  apply (rule wf_Cons)
  apply simp
  apply (rule wf_subst)
  apply assumption+
  apply simp
  apply (erule well_formedE_cases)
  apply (rule wf_Cons)
  apply simp
  apply (rule wf_subst)
  apply assumption+
  done

subsection ‹Subtyping›

text ‹
The definition of the subtyping judgement is extended with a rule ‹SA_Rcd› stating
that a record type @{term "RcdT fs"} is a subtype of @{term "RcdT fs'"}, if
for all fields \mbox{@{term "(l, T)"}} contained in @{term fs'}, there exists a
corresponding field @{term "(l, S)"} such that @{term S} is a subtype of @{term T}.
If the list @{term fs'} is empty, ‹SA_Rcd› can appear as a leaf in
the derivation tree of the subtyping judgement. Therefore, the introduction
rule needs an additional premise @{term "Γ ⊢wf"} to make sure that only
subtyping judgements with well-formed contexts are derivable. Moreover,
since @{term fs} can contain additional fields not present in @{term fs'},
we also have to require that the type @{term "RcdT fs"} is well-formed.
In order to ensure that the type @{term "RcdT fs'"} is well-formed, too,
we only have to require that labels in @{term fs'} are unique, since,
by induction on the subtyping derivation, all types contained in @{term fs'}
are already well-formed.
›

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)"
| SA_Rcd: "Γ ⊢wf ⟹ Γ ⊢wf RcdT fs ⟹ unique fs' ⟹
    ∀(l, T)∈set fs'. ∃S. (l, S)∈set fs ∧ Γ ⊢ S <: T ⟹ Γ ⊢ RcdT fs <: RcdT fs'"

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"
  apply (rule H')
  apply (rule wf_subtype_env)
  apply (rule H)
  apply (rule wf_subtype [OF H, THEN conjunct1])
  apply (rule wf_subtype [OF H, THEN conjunct2])
  done

lemma subtype_refl: ― ‹A.1›
  "Γ ⊢wf ⟹ Γ ⊢wf T ⟹ Γ ⊢ T <: T"
  "Γ ⊢wf ⟹ ∀(l::name, T)∈set fTs. Γ ⊢wf T ⟶ Γ ⊢ T <: T"
  "Γ ⊢wf ⟹ Γ ⊢wf snd (fT::fldT) ⟹ Γ ⊢ snd fT <: snd fT"
  by (induct T and fTs and fT arbitrary: Γ and Γ and Γ
    rule: liftT.induct liftrT.induct liftfT.induct,
    simp_all add: split_paired_all, simp_all)
    (blast intro: subtyping.intros wf_Nil wf_TVarB bexpI intro!: ballpI
       elim: well_formed_cases ballpE elim!: bexpE)+

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)
next
  case (SA_Rcd fs fs')
  with wf have "↑e (Suc 0) 0 Δ @ B ∷ Γ ⊢wf" by simp (rule wfE_weaken)
  moreover from ‹Δ @ Γ ⊢wf RcdT fs›
  have "↑e (Suc 0) 0 Δ @ B ∷ Γ ⊢wf ↑τ (Suc 0) ∥Δ∥ (RcdT fs)"
    by (rule wf_weaken)
  hence "↑e (Suc 0) 0 Δ @ B ∷ Γ ⊢wf RcdT (↑rτ (Suc 0) ∥Δ∥ fs)" by simp
  moreover from SA_Rcd have "unique (↑rτ (Suc 0) ∥Δ∥ fs')" by simp
  moreover have "∀(l, T)∈set (↑rτ (Suc 0) ∥Δ∥ fs').
    ∃S. (l, S)∈set (↑rτ (Suc 0) ∥Δ∥ fs) ∧ ↑e (Suc 0) 0 Δ @ B ∷ Γ ⊢ S <: T"
  proof (rule ballpI)
    fix l T
    assume "(l, T) ∈ set (↑rτ (Suc 0) ∥Δ∥ fs')"
    then obtain T' where "(l, T') ∈ set fs'" and T: "T = ↑τ (Suc 0) ∥Δ∥ T'"
      by (blast dest: liftrT_setD)
    with SA_Rcd obtain S where
      lS: "(l, S) ∈ set fs"
      and ST: "↑e (Suc 0) 0 Δ @ B ∷ Γ ⊢ ↑τ (Suc 0) ∥Δ∥ S <: ↑τ (Suc 0) ∥Δ∥ (T[∥Δ∥ ↦τ Top]τ)"
      by fastforce
    with T have "↑e (Suc 0) 0 Δ @ B ∷ Γ ⊢ ↑τ (Suc 0) ∥Δ∥ S <: ↑τ (Suc 0) ∥Δ∥ T'"
      by simp
    moreover from lS have "(l, ↑τ (Suc 0) ∥Δ∥ S) ∈ set (↑rτ (Suc 0) ∥Δ∥ fs)"
      by (rule liftrT_set)
    moreover note T
    ultimately show "∃S. (l, S)∈set (↑rτ (Suc 0) ∥Δ∥ fs) ∧ ↑e (Suc 0) 0 Δ @ B ∷ Γ ⊢ S <: T"
      by auto
  qed
  ultimately have "↑e (Suc 0) 0 Δ @ B ∷ Γ ⊢ RcdT (↑rτ (Suc 0) ∥Δ∥ fs) <: RcdT (↑rτ (Suc 0) ∥Δ∥ fs')"
    by (rule subtyping.SA_Rcd)
  thus ?case by simp
qed

lemma subtype_weaken': ― ‹A.2›
  "Γ ⊢ P <: Q ⟹ Δ @ Γ ⊢wf ⟹ Δ @ Γ ⊢ ↑τ ∥Δ∥ 0 P <: ↑τ ∥Δ∥ 0 Q"
  apply (induct Δ)
  apply simp_all
  apply (erule well_formedE_cases)
  apply simp
  apply (drule_tac B="a" and Γ="Δ @ Γ" in subtype_weaken [of "[]", simplified])
  apply simp_all
  done

lemma fieldT_size [simp]:
  "(a, T) ∈ set fs ⟹ size T < Suc (size_list (size_prod (λx. 0) size) fs)"
  by (induct fs arbitrary: a T rule: list.induct) fastforce+

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)
  {
    fix Γ S T Q'
    assume "Γ ⊢ S <: Q'"
    then have "Γ ⊢ Q' <: T ⟹ size Q = size Q' ⟹ Γ ⊢ S <: T"
    proof (induct arbitrary: T)
      case SA_Top
      from SA_Top(3) show ?case
        by cases (