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 Tp = 1"
| "PRcd fsp = fsr"
| "[]r = 0"
| "f  fsr = ff + fsr"
| "(l, p)f = pp"

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 + pp) 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 + pp  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 "pp"} to @{term k} when performing substitution in the body of
the LET› binder, where @{term "pp"} 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 + pp τ 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)"
  by (induct Γ arbitrary: i) (auto split: nat.splits)

lemma substE_nth [simp]:
  "(Γ[0 τ T]e)i = map_option (mapB (λU. U[Γ - i - 1 τ T]τ)) (Γi)"
  by (induct Γ arbitrary: i) (auto split: nat.splits)

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)"
proof (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)
qed (auto simp: Suc_diff_le)

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τ"
  by (induct T and rT and fT arbitrary: k k' and k k' and k k'
    rule: liftT.induct liftrT.induct liftfT.induct) auto

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τ"
proof (induct T and rT and fT arbitrary: k k' and k k' and k k'
        rule: liftT.induct liftrT.induct liftfT.induct)
qed auto

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τ"
proof (induct T and rT and fT arbitrary: k k' and k k' and k k'
    rule: liftT.induct liftrT.induct liftfT.induct)
qed auto

theorem liftE_substE [simp]:
  "k  k'  e n k (Γ[k' τ U]e) = e n k Γ[k' + n τ U]e"
proof (induct Γ)
  case Nil
  then show ?case
    by auto
next
  case (Cons a Γ)
  then show ?case
    by (cases a) (simp_all add: ac_simps)
qed

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τ"
proof (induct T and rT and fT arbitrary: n k and n k and n k
    rule: liftT.induct liftrT.induct liftfT.induct)
  case (TyAll x1 x2)
  then show ?case
    by (metis add.commute add_Suc liftT.simps(4) plus_1_eq_Suc substTT.simps(4))
qed auto

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 pp = pp"
  "rp n k fsr = fsr"
  "fp n k ff = ff"
  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 Γ"
proof (induct Γ arbitrary: k k')
  case Nil
  then show ?case by auto
next
  case (Cons a Γ)
  then show ?case
    by (cases a) auto
qed

lemma liftE_liftE' [simp]:
  "i + m  j  e n j (e m i Γ) = e m i (e n (j - m) Γ)"
proof (induct Γ arbitrary: i j m n)
  case Nil
  then show ?case by auto
next
  case (Cons a Γ)
  then show ?case
    by (cases a) auto
qed

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τ"
proof (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)
  case (TyAll x1 x2)
  then show ?case
    by (metis Suc_eq_plus1 diff_Suc_Suc not_less_eq_eq substTT.simps(4))
qed auto

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"
proof (induct Γ)
  case Nil
  then show ?case by auto
next
  case (Cons a Γ)
  then show ?case
    by (cases a) (simp_all add: substT_substT [symmetric])
qed

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 Γ"
  by (induct n arbitrary: B Γ; case_tac B; force)

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 Γ"
  by (induct m arbitrary: n) auto

theorem decE_liftE [simp]:
  "k  k'  k' + m  k + n  e m k' (e n k Γ) = e (n - m) k Γ"
proof (induct Γ arbitrary: k k')
  case Nil
  then show ?case by auto
next
  case (Cons a Γ)
  then show ?case 
    by (cases a) auto
qed

theorem liftE0 [simp]: "e 0 k Γ = Γ"
proof (induct Γ)
  case Nil
  then show ?case by auto
next
  case (Cons a Γ)
  then show ?case 
    by (cases a) auto
qed

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 fsl? = ) = (fsl? = )"
  by (induct fs rule: list.induct) auto

lemma liftrT_assoc_Some: "fsl? = T  rτ n k fsl? = τ n k T"
  by (induct fs rule: list.induct) auto

lemma liftrp_assoc_None [simp]: "(rp n k fpsl? = ) = (fpsl? = )"
  by (induct fps rule: list.induct) auto

lemma liftr_assoc_None [simp]: "(r n k fsl? = ) = (fsl? = )"
  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? = ) = (fsa? = )"
  by (induct fs rule: list.induct) auto

lemma substrTT_assoc_Some [simp]:
  "fsa? = T  fs[k τ U]rτa? = T[k τ U]τ"
  by (induct fs rule: list.induct) auto

lemma substrT_assoc_None [simp]: "(fs[k τ P]rl? = ) = (fsl? = )"
  by (induct fs rule: list.induct) auto

lemma substrp_assoc_None [simp]: "(fps[k τ U]rpl? = ) = (fpsl? = )"
  by (induct fps rule: list.induct) auto

lemma substr_assoc_None [simp]: "(fs[k  u]rl? = ) = (fsl? = )"
  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"
proof (induct Γ arbitrary: Γ' T i)
  case Nil
  then show ?case by auto
next
  case (Cons a Γ)
  then have "z . is_TVarB z  T. z = TVarB T"
    by (metis binding.exhaust is_TVarB.simps(1))
  with Cons show ?case by (auto split: nat.split_asm)
qed

lemma wf_equallength:
  assumes H: "Γ wf T"
  shows "map is_TVarB Γ' = map is_TVarB Γ  Γ' wf T" using H
proof (induct arbitrary: Γ')
  case (wf_TVar Γ i T)
  then show ?case
    using map_is_TVarb well_formed.wf_TVar by blast
next
  case (wf_RcdT fs Γ)
  then show ?case
    by (simp add: split_beta well_formed.wf_RcdT)
qed (fastforce intro: well_formed.intros)+

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 Δ)
  have "a  Δ @ B'  Γ wf"
  proof (rule wf_Cons)
    have §: "Δ @ B  Γ wf" "Δ @ B  Γ wfB a"
      using Cons.prems(1) well_formedE_cases by auto
    with Cons.prems wf_equallength show "Δ @ B'  Γ wfB a"
      by auto
    show "Δ @ B'  Γ wf"
      by (simp add: "§" Cons)
  qed
  with Cons well_formedE_cases show ?case by auto
qed

lemma wf_weaken:
  assumes H: "Δ @ Γ wf T"
  shows "e (Suc 0) 0 Δ @ B  Γ wf τ (Suc 0) Δ T"
  using H
proof (induct "Δ @ Γ" T arbitrary: Δ)
  case (wf_TVar i T)
  show ?case
  proof (cases "i < Δ")
    case True
    with wf_TVar show ?thesis
      by (force intro: well_formed.wf_TVar)
  next
    case False
    then have "Suc i - Δ = Suc (i - Δ)"
      using Suc_diff_le leI by blast
    with wf_TVar show ?thesis
      by (force intro: well_formed.wf_TVar)
  qed
next
  case (wf_RcdT fs)
  then show ?case
    by (fastforce dest: liftrT_setD intro: well_formed.wf_RcdT)
qed (fastforce intro: well_formed.intros)+

lemma wf_weaken': "Γ wf T  Δ @ Γ wf τ Δ 0 T"
proof (induct Δ)
  case Nil
  then show ?case
    by simp
next
  case (Cons a Δ)
  with wf_weaken [of "[]"]  show ?case
    by fastforce
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 Δ)
  show ?case
  proof (cases a)
    case (VarB x1)
    with Cons have "VarB (τ (Suc 0) Δ x1)  e (Suc 0) 0 Δ @ B  Γ wf"
      by (metis append_Cons type_ofB.simps(1) well_formedE_cases wf_Cons wf_weaken)
    with VarB show ?thesis 
      by simp
  next
    case (TVarB x2)
    with Cons have "TVarB (τ (Suc 0) Δ x2)  e (Suc 0) 0 Δ @ B  Γ wf"
      by (metis append_Cons type_ofB.simps(2) well_formedE_cases wf_Cons wf_weaken)
    with TVarB show ?thesis
      by simp
  qed
qed

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 simp
next
  case (wf_Cons Γ B i)
  show ?case
  proof -
    have "VarB T  Γ wf τ (Suc 0) 0 T" if "Γ wf T"
      by (metis append_self_conv2 liftE.simps(1) list.size(3) wf_weaken that)
    moreover have "B  Γ wf τ (Suc (Suc k)) 0 T" if "Γk = VarB T" for k
      using that 
      by (metis One_nat_def Suc_eq_plus1 append_self_conv2 less_eq_nat.simps(1)
          liftE.simps(1) liftT_liftT(1) list.size(3) wf_Cons.hyps(3) wf_weaken)
    ultimately show ?thesis
      using wf_Cons by (auto split: nat.split_asm)
  qed
qed

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]τ"
proof (induct T and rT and fT arbitrary: Δ and Δ and Δ
    rule: liftT.induct liftrT.induct liftfT.induct)
  case (TVar i Δ)
  show ?case
  proof (cases "i  Δ")
    case True
    with TVar.prems have "Δ[0 τ U]e @ Γ wf τ Δ 0 U"
      by (metis substE_length wf_weaken')
    with TVar True show ?thesis
      by (auto elim!: well_formed_cases simp add: wf_TVar split: nat.split_asm)
  next
    case False
    then have "Δ  i - 1"
      by simp
    with TVar False show ?thesis
      by (auto elim!: well_formed_cases simp: wf_TVar split: nat_diff_split_asm nat.split_asm)
  qed
next
  case Top
  then show ?case
    by (simp add: wf_Top)
next
  case (Fun x1 x2)
  then show ?case
    by (metis substTT.simps(3) well_formed_cases(3) wf_arrow)
next
  case (TyAll type1 type2 Δ)
  then have "(TVarB type1  Δ)[0 τ U]e @ Γ wf type2[TVarB type1  Δ τ U]τ"
    by (metis append_Cons well_formed_cases(4))
  with TyAll show ?case
    using wf_all by (force simp: elim!: well_formed_cases)
next
  case (RcdT x)
  then show ?case
    by (force simp: intro!: wf_RcdT dest: substrT_setD elim: well_formed_cases)
qed (auto simp: split_beta)

theorem wf_dec: "Δ @ Γ wf T  Γ wf τ Δ 0 T"
proof (induct Δ arbitrary: T)
  case Nil
  then show ?case by auto
next
  case (Cons a Δ)
  with wf_subst(1) [of "[]"] wf_Top show ?case
    by force
qed

theorem wfE_subst: "Δ @ B  Γ wf  Γ wf U  Δ[0 τ U]e @ Γ wf"
proof (induct Δ)
  case Nil
  then show ?case
    using well_formedE_cases by auto
next
  case (Cons a Δ)
  show ?case
  proof (cases a)
    case (VarB x)
    with Cons have "VarB (x[Δ τ U]τ)  Δ[0 τ U]e @ Γ wf"
      by (metis append_Cons type_ofB.simps(1) well_formedE_cases wf_VarB wf_subst(1))
    then show ?thesis
      using VarB by force
  next
    case (TVarB x)
    with Cons have "TVarB (x[Δ τ U]τ)  Δ[0 τ U]e @ Γ wf"
      by (metis append_Cons type_ofB.simps(2) well_formedE_cases wf_TVarB wf_subst(1))
    with TVarB show ?thesis
      by simp
  qed
qed
 
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"
  using H H' wf_subtype wf_subtype_env by force

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 elim: well_formed_cases)+

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"
proof (induct Δ)
  case Nil
  then show ?case 
    by auto
next
  case (Cons a Δ)
  then have "Δ @ Γ wfB a" "Δ @ Γ wf"
    using well_formedE_cases by auto
  with Cons show ?case
    using subtype_weaken [where B="a" and Γ="Δ @ Γ"]
    by (metis Suc_eq_plus1 append_Cons append_Nil bot_nat_0.extremum length_Cons
        liftE.simps(1) liftT_liftT(1) list.size(3))
qed

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 (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
    next
      case (SA_Rcd Γ fs1 fs2)
      note SA_Rcd' = SA_Rcd
      from SA_Rcd(5) show ?case
      proof cases
        case SA_Top
        with SA_Rcd show ?thesis by (auto intro!: subtyping.SA_Top)
      next
        case (SA_Rcd fs2')
        note Γ wf
        moreover note Γ wf RcdT fs1
        moreover note unique fs2'
        moreover have "(l, T)set fs2'. S. (l, S)set fs1  Γ  S <: T"
        proof (rule ballpI)
          fix l T
          assume lT: "(l, T)  set fs2'"
          with SA_Rcd obtain U where
            fs2: "(l, U)  set fs2" and UT: "Γ  U <: T" by blast
          with SA_Rcd SA_Rcd' obtain S where
            fs1: "(l, S)  set fs1" and SU: "Γ  S <: U" by blast
          from SA_Rcd SA_Rcd' fs2 have "(U, Q)  measure size" by simp
          hence "Γ  S <: T" using SU UT by (rule less(1))
          with fs1 show "S. (l, S)set fs1  Γ  S <: T" by blast
        qed
        ultimately have "Γ  RcdT fs1 <: RcdT fs2'" by (rule subtyping.SA_Rcd)
        with SA_Rcd show ?thesis by simp
      qed
    qed
  }
  note tr = this
  {
    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 intro: wfE_replace 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 - (rule subtyping.SA_trans_TVar, simp+)
        qed
      qed
    next
      case SA_arrow
      thus ?case by (auto intro!: subtyping.SA_arrow)
    next
      case (SA_all T1 S1 S2 T2)
      thus ?case by (auto intro: subtyping.SA_all
        SA_all(4) [of "TVarB T1  Δ", simplified])
    next
      case (SA_Rcd fs fs')
      from Γ  P <: Q have "Γ wf P" by (rule wf_subtypeE)
      with SA_Rcd have "Δ @ TVarB P  Γ wf"
        by - (rule wfE_replace, simp+)
      moreover from SA_Rcd have "Δ @ TVarB Q  Γ wf RcdT fs" by simp
      hence "Δ @ TVarB P  Γ wf RcdT fs" by (rule wf_equallength) simp_all
      moreover note unique fs'
      moreover from SA_Rcd
      have "(l, T)set fs'. S. (l, S)set fs  Δ @ TVarB P  Γ  S <: T"
        by blast
      ultimately show ?case by (rule subtyping.SA_Rcd)
    qed
  }
qed

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(1) wf_subtype)
next
  case (SA_refl_TVar i)
  then show ?case
    by (meson subtype_refl(1) wfE_subst wf_subst(1) wf_subtypeE)
next
  case (SA_trans_TVar i U T Δ)
  have "Δ[0 τ P]e @ Γ  τ Δ 0 P <: T[Δ τ P]τ"
    if "i = Δ"
  proof -
    have "Δ[0 τ P]e @ Γ  τ Δ 0 U <: T[Δ τ P]τ; 
     Δ[0 τ P]e @ Γ  τ Δ[0 τ P]e 0 P <: τ Δ[0 τ P]e 0 U
     Δ[0 τ P]e @ Γ  τ Δ 0 P <: T[Δ τ P]τ"
      by (metis substE_length subtype_trans(1))
    then show ?thesis
      using SA_trans_TVar that wf_subtype_env
      by (fastforce dest: subtype_weaken' [where Γ=Γ and Δ="Δ[0 τ P]e"])
  qed
  moreover have "Δ[0 τ P]e @ Γ  TVar (i - Suc 0) <: T[Δ τ P]τ"
    if "Δ < i"
  proof (intro subtyping.SA_trans_TVar)
    show "(Δ[0 τ P]e @ Γ)i - Suc 0 = TVarB U"
      using SA_trans_TVar that
      by (auto split: nat.split_asm nat_diff_split)
  next
    show "Δ[0 τ P]e @ Γ  τ (Suc (i - Suc 0)) 0 U <: T[Δ τ P]τ"
      using SA_trans_TVar that by fastforce
  qed
  moreover have "Δ[0 τ P]e @ Γ  TVar i <: T[Δ τ P]τ"
    if "Δ > i"
  proof (intro subtyping.SA_trans_TVar)
    show "(Δ[0 τ P]e @ Γ)i = TVarB (U[Δ - Suc i τ P]τ)"
      using that SA_trans_TVar by (simp split: nat.split_asm nat_diff_split)
  next
    show "Δ[0 τ P]e @ Γ  τ (Suc i) 0 (U[Δ - Suc i τ P]τ) <: T[Δ τ P]τ"
      using SA_trans_TVar 
      by (metis Suc_leI zero_le le_add_diff_inverse2 liftT_substT(1) that)
  qed
  ultimately show ?case
    by auto
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: subtyping.SA_all)
next
  case (SA_Rcd fs fs')
  have "Δ[0 τ P]e @ Γ wf"
    using SA_Rcd wfE_subst by (meson wf_subtypeE)
  moreover have "Δ[0 τ P]e @ Γ wf RcdT (fs[Δ τ P]rτ)"
    using SA_Rcd.hyps(2) SA_Rcd.prems wf_subst(1) wf_subtype by fastforce
  moreover have "unique (fs'[Δ τ P]rτ)"
    using SA_Rcd.hyps(3) by auto
  moreover have "(l, T)  set (fs'[Δ τ P]rτ). S. (l, S)  set (fs[Δ τ P]rτ)  Δ[0 τ P]e @ Γ  S <: T"
    using SA_Rcd by (smt (verit) ballpI case_prodD substrT_set substrT_setD)
  ultimately show ?case
    by (simp add: subtyping.SA_Rcd)
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(1))
next
  case (SA_refl_TVar i)
  then show ?case
    by (metis One_nat_def decE.simps decT.simps subtype_refl(1) wfE_subst
        wf_Top wf_subst(1))
next
  case (SA_trans_TVar i U T)
  then have *: "Δ > i
     Δ[0 τ Top]e @ Γ 
         τ (Suc i) 0 (U[Δ - Suc i τ Top]τ) <: T[Δ τ Top]τ"
    by (metis One_nat_def Suc_leI bot_nat_0.extremum decE.simps(1,2) decT.simps(1,2)
        le_add_diff_inverse2 liftT_substT(1))
  show ?case
    using SA_trans_TVar
    by (auto simp add: * split: nat_diff_split intro!: subtyping.SA_trans_TVar)
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: subtyping.SA_all)
next
  case (SA_Rcd fs fs')
  have "Δ[0 τ Top]e @ Γ wf"
    using SA_Rcd.hyps(1) wfE_subst wf_Top by auto
  moreover have "Δ[0 τ Top]e @ Γ wf RcdT (fs[Δ τ Top]rτ)"
    using SA_Rcd.hyps(2) wf_Top wf_subst(1) by fastforce
  moreover have "unique (fs'[Δ τ Top]rτ)"
    by (simp add: SA_Rcd.hyps)
  moreover have "(l, T) set (fs'[Δ τ Top]rτ). S. (l, S)  set (fs[Δ τ Top]rτ)  Δ[0 τ Top]e @ Γ  S <: T"
    using SA_Rcd
    by (smt (verit) One_nat_def ballpI case_prodD decE.simps(1,2) decT.simps(1,2)
        substrT_set substrT_setD)
  ultimately show ?case
    by (simp add: subtyping.SA_Rcd)
qed


subsection ‹Typing›

text ‹
In the formalization of the type checking rule for the LET› binder,
we use an additional judgement ⊢ p : T ⇒ Δ› for checking whether a
given pattern @{term p} is compatible with the type @{term T} of an object that
is to be matched against this pattern. The judgement will be defined simultaneously
with a judgement \mbox{⊢ ps [:] Ts ⇒ Δ›} for type checking field patterns.
Apart from checking the type, the judgement also returns a list of bindings @{term Δ},
which can be thought of as a ``flattened'' list of types of the variables occurring
in the pattern. Since typing environments are extended ``to the left'', the bindings
in @{term Δ} appear in reverse order.
›

inductive
  ptyping :: "pat  type  env  bool"  ( _ : _  _› [50, 50, 50] 50)
  and ptypings :: "rpat  rcdT  env  bool"  ( _ [:] _  _› [50, 50, 50] 50)
where
  P_Var: " PVar T : T  [VarB T]"
| P_Rcd: " fps [:] fTs  Δ   PRcd fps : RcdT fTs  Δ"
| P_Nil: " [] [:] []  []"
| P_Cons: " p : T  Δ1   fps [:] fTs  Δ2  fpsl? =  
     ((l, p)  fps) [:] ((l, T)  fTs)  e Δ1 0 Δ2 @ Δ1"

text ‹
The definition of the typing judgement for terms is extended with the rules T_Let›,
@{term "T_Rcd"}, and @{term "T_Proj"} for pattern matching, record construction and
field selection, respectively. The above typing judgement for patterns is used in
the rule T_Let›. The typing judgement for terms is defined simultaneously
with a typing judgement Γ ⊢ fs [:] fTs› for record fields.
›

inductive
  typing :: "env  trm  type  bool"  (‹_  _ : _› [50, 50, 50] 50)
  and typings :: "env  rcd  rcdT  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"
| T_Let: "Γ  t1 : T1   p : T1  Δ  Δ @ Γ  t2 : T2 
    Γ  (LET p = t1 IN t2) : τ Δ 0 T2"
| T_Rcd: "Γ  fs [:] fTs  Γ  Rcd fs : RcdT fTs"
| T_Proj: "Γ  t : RcdT fTs  fTsl? = T  Γ  t..l : T"
| T_Nil: "Γ wf  Γ  [] [:] []"
| T_Cons: "Γ  t : T  Γ  fs [:] fTs  fsl? =  
    Γ  (l, t)  fs [:] (l, T)  fTs"

theorem wf_typeE1:
  "Γ  t : T  Γ wf"
  "Γ  fs [:] fTs  Γ wf"
  by (induct set: typing typings) (blast elim: well_formedE_cases)+

theorem wf_typeE2:
  "Γ  t : T  Γ wf T"
  "Γ'  fs [:] fTs  ((l, T)  set fTs. Γ' wf T) 
     unique fTs  (l. (fsl? = ) = (fTsl? = ))"
proof (induct set: typing typings)
  case (T_Abs T1 Γ t2 T2)
  have "[] = 0" and "Γ wf T1"
    using T_Abs.hyps(1) well_formedE_cases wf_typeE1(1) by fastforce+
  then show ?case
    by (metis One_nat_def T_Abs.hyps(2) append_Cons append_Nil length_Cons wf_arrow wf_dec)
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(1))
next
  case (T_TApp Γ t1 T11 T12 T2)
  then show ?case
    by (metis append_Nil length_0_conv substE_length well_formed_cases(4)
        wf_subst(1) wf_subtype)
next
  case (T_Proj Γ t fTs l T)
  then show ?case
    by (metis assoc_set snd_eqD split_beta well_formed_cases(5))
qed (auto simp: wf_subtype wf_dec wf_RcdT wf_liftB)

lemmas ptyping_induct = ptyping_ptypings.inducts(1)
  [of _ _ _ _ "λx y z. True", simplified True_simps, consumes 1,
   case_names P_Var P_Rcd]

lemmas ptypings_induct = ptyping_ptypings.inducts(2)
  [of _ _ _ "λx y z. True", simplified True_simps, consumes 1,
   case_names P_Nil P_Cons]

lemmas typing_induct = typing_typings.inducts(1)
  [of _ _ _ _ "λx y z. True", simplified True_simps, consumes 1,
   case_names T_Var T_Abs T_App T_TAbs T_TApp T_Sub T_Let T_Rcd T_Proj]

lemmas typings_induct = typing_typings.inducts(2)
  [of _ _ _ "λx y z. True", simplified True_simps, consumes 1,
   case_names T_Nil T_Cons]

lemma narrow_type: ― ‹A.7›
  "Δ @ TVarB Q  Γ  t : T 
     Γ  P <: Q  Δ @ TVarB P  Γ  t : T"
  "Δ @ TVarB Q  Γ  ts [:] Ts 
     Γ  P <: Q  Δ @ TVarB P  Γ  ts [:] Ts"
proof (induct "Δ @ TVarB Q  Γ" t T and "Δ @ TVarB Q  Γ" ts Ts
      arbitrary: Δ and Δ set: typing typings)
  case (T_Var i U T)
  show ?case 
  proof (intro typing_typings.T_Var)
    show "Δ @ TVarB P  Γ wf"
      using T_Var by (elim wfE_replace wf_subtypeE; simp)
    show "(Δ @ TVarB P  Γ)i = VarB U"
      using T_Var by (cases "i < Δ") (auto split: nat.splits)
  next
    show "T = τ (Suc i) 0 U"
      using T_Var.hyps(3) by blast
  qed
next
  case (T_Abs T1 t2 T2)
  then show ?case
    using typing_typings.T_Abs by force
next
  case (T_TApp t1 T11 T12 T2)
  then show ?case
    using subtype_trans(2) typing_typings.T_TApp by blast
next
  case (T_Sub t S T)
  then show ?case
    using subtype_trans(2) typing_typings.T_Sub by blast
next
  case T_Nil
  then show ?case
    by (metis is_TVarB.simps(2) type_ofB.simps(2) typing_typings.T_Nil wfE_replace
        wf_subtypeE)
qed (auto simp: typing_typings.intros)

lemma typings_setD:
  assumes H: "Γ  fs [:] fTs"
  shows "(l, T)  set fTs  t. fsl? = t  Γ  t : T"
  using H
  by (induct arbitrary: l T rule: typings_induct) fastforce+

lemma subtype_refl':
  assumes t: "Γ  t : T"
  shows "Γ  T <: T"
  using subtype_refl(1) t wf_typeE1(1) wf_typeE2(1) by force

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
    using T_Sub.hyps(2) T_Sub.prems(2) by blast
qed

lemma Abs_type':
  assumes "Γ  (λ:S. s) : U  U'"
  and "S'. Γ  U <: S  VarB S  Γ  s : S'  Γ  τ 1 0 S' <: U'  P"
  shows "P"
  using Abs_type assms 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])
  then show ?case
    using T_TAbs ty1 ty2 by blast
next
  case (T_Sub Γ S' T)
  from Γ  S' <: T and Γ  T <: (∀<:U. U')
  have "Γ  S' <: (∀<:U. U')" by (rule subtype_trans(1))
  with T_Sub show ?case
    by metis
qed

lemma TAbs_type':
  assumes "Γ  (λ<:S. s) : (∀<:U. U')"
  and "S'. Γ  U <: S  TVarB U  Γ  s : S'  TVarB U  Γ  S' <: U'  P"
  shows "P"
  using assms TAbs_type subtype_refl' by blast

text ‹
In the proof of the preservation theorem, the following elimination rule
for typing judgements on record types will be useful:
›


lemma Rcd_type1: ― ‹A.13(3)›
  assumes "Γ  t : T"
  shows "t = Rcd fs  Γ  T <: RcdT fTs 
     (l, U)  set fTs. u. fsl? = u  Γ  u : U"
  using assms
proof (induct arbitrary: fs fTs rule: typing_induct)
  case (T_Sub Γ t S T)
  then show ?case
    using subtype_trans(1) by blast
next
  case (T_Rcd Γ gs gTs)
  then show ?case
    by (force dest: typings_setD intro: T_Sub elim: subtyping.cases)
qed blast+

lemma Rcd_type1':
  assumes H: "Γ  Rcd fs : RcdT fTs"
  shows "(l, U)  set fTs. u. fsl? = u  Γ  u : U"
  using H refl subtype_refl' [OF H]
  by (rule Rcd_type1)

text ‹
Intuitively, this means that for a record @{term "Rcd fs"} of type @{term "RcdT fTs"},
each field with name @{term l} associated with a type @{term U} in @{term "fTs"}
must correspond to a field in @{term fs} with value @{term u}, where @{term u} has
type @{term U}. Thanks to the subsumption rule T_Sub›, the typing judgement
for terms is not sensitive to the order of record fields. For example,
@{term [display] "Γ  Rcd [(l1, t1), (l2, t2), (l3, t3)] : RcdT [(l2, T2), (l1, T1)]"}
provided that Γ ⊢ ti : Ti. Note however that this does not imply
@{term [display] "Γ  [(l1, t1), (l2, t2), (l3, t3)] [:] [(l2, T2), (l1, T1)]"}
In order for this statement to hold, we need to remove the field @{term "l3"}
and exchange the order of the fields @{term "l1"} and @{term "l2"}. This gives rise
to the following variant of the above elimination rule:
›

lemma Rcd_type2_aux:
  "Γ  T <: RcdT fTs; (l, U)set fTs. u. fsl? = u  Γ  u : U
     Γ  map (λ(l, T). (l, the (fsl?))) fTs [:] fTs"
proof (induct fTs rule: list.induct)
  case Nil
  then show ?case
    using T_Nil wf_subtypeE by force
next
  case (Cons p list)
  have "Γ  (a, the (fsa?))  map (λ(l, T). (l, the (fsl?))) list [:] (a, b)  list"
    if "p = (a, b)"
    for a b
  proof (rule T_Cons)
    show "Γ  the (fsa?) : b"
      using Cons.prems(2) that by auto
    have "Γ  RcdT ((a, b)  list) <: RcdT list"
    proof (intro SA_Rcd)
      show "Γ wf"
        using Cons.prems(1) wf_subtypeE by blast
      have *: "Γ wf RcdT (p  list)"
        using Cons.prems(1) wf_subtypeE by blast
      with that show "Γ wf RcdT ((a, b)  list)"
        by auto
      show "unique list"
        using * well_formed_cases(5) by fastforce
      show "(l, T)set list. S. (l, S)  set ((a, b)  list)  Γ  S <: T"
        using Cons.prems(2) subtype_refl' by fastforce
    qed 
    with Cons
    show "Γ  map (λ(l, T). (l, the (fsl?))) list [:] list"
      by (metis (no_types, lifting) list.set_intros(2) subtype_trans(1) that)
    then show "map (λ(l, T). (l, the (fsl?))) lista? = "
      using Cons.prems(1) that well_formed_cases(5) wf_subtype by fastforce
  qed
  then show ?case
    by (auto split: prod.splits)
qed

lemma Rcd_type2:
  "Γ  Rcd fs : T  Γ  T <: RcdT fTs 
     Γ  map (λ(l, T). (l, the (fsl?))) fTs [:] fTs"
  by (simp add: Rcd_type1 Rcd_type2_aux)

lemma Rcd_type2':
  assumes H: "Γ  Rcd fs : RcdT fTs"
  shows "Γ  map (λ(l, T). (l, the (fsl?))) fTs [:] fTs"
  using H subtype_refl' [OF H]
  by (rule Rcd_type2)

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

lemma ptyping_length [simp]:
  " p : T  Δ  pp = Δ"
  " fps [:] fTs  Δ  fpsr = Δ"
  by (induct set: ptyping ptypings) simp_all

lemma lift_ptyping:
  " p : T  Δ   p n k p : τ n k T  e n k Δ"
  " fps [:] fTs  Δ   rp n k fps [:] rτ n k fTs  e n k Δ"
proof (induct set: ptyping ptypings)
  case P_Nil
  then show ?case
    by (simp add: ptyping_ptypings.P_Nil)
next
  case (P_Cons p T Δ1 fps fTs Δ2 l)
  then show ?case
    using P_Cons.hyps(2) ptyping_ptypings.P_Cons by fastforce
qed (auto simp: ptyping.simps)

lemma type_weaken:
  "Δ @ Γ  t : T  Γ wfB B 
     e 1 0 Δ @ B  Γ   1 Δ t : τ 1 Δ T"
  "Δ @ Γ  fs [:] fTs  Γ wfB B 
     e 1 0 Δ @ B  Γ  r 1 Δ fs [:] rτ 1 Δ fTs"
proof (induct "Δ @ Γ" t T and "Δ @ Γ" fs fTs arbitrary: Δ and Δ set: typing typings)
  case (T_Var i U T Δ)
  show ?case 
  proof -
    have "e (Suc 0) 0 Δ @ B  Γ  Var i : τ (Suc 0) Δ T"
      if "i < Δ"
      using that T_Var by (force simp: typing_typings.T_Var wfE_weaken)
    moreover have "e (Suc 0) 0 Δ @ B  Γ  Var (Suc i) : τ (Suc 0) Δ T"
      if "¬ i < Δ"
    proof (intro typing_typings.T_Var)
      have *: "Suc i - Δ = Suc (i - Δ)"
        using that by simp
      show "e (Suc 0) 0 Δ @ B  Γ wf"
        by (simp add: T_Var wfE_weaken)
      show "(e (Suc 0) 0 Δ @ B  Γ)Suc i = VarB U"
        using T_Var that by (simp add: * split: nat.splits)
      show "τ (Suc 0) Δ T = τ (Suc (Suc i)) 0 U"
        using T_Var.hyps(3) that by fastforce
    qed
    ultimately show ?thesis
      by auto
  qed
next
  case (T_Abs T1 t2 T2)
  then show ?case
    using typing_typings.T_Abs by force
next
  case (T_App t1 T11 T12 t2)
  then show ?case
    by (simp add: typing_typings.T_App)
next
  case (T_TAbs T1 t2 T2)
  then show ?case
    by (simp add: typing_typings.T_TAbs)
next
  case (T_TApp t1 T11 T12 T2)
  have "e (Suc 0) 0 Δ @ B  Γ  τ (Suc 0) Δ T2 <: τ (Suc 0) Δ T11"
    using subtype_weaken by (simp add: T_TApp)
  moreover have "τ (Suc 0) (Suc Δ) T12[0 τ τ (Suc 0) Δ T2]τ = τ (Suc 0) Δ (T12[0 τ T2]τ)"
    by (metis Suc_eq_plus1 add.commute diff_zero le_eq_less_or_eq liftT_substT'(1)
        liftT_substT(1) liftT_substT_strange(1) not_gr_zero)
  ultimately show ?case
    using T_TApp
    by (metis Suc_eq_plus1 add.commute add.right_neutral
        lift.simps(5) liftT.simps(4) typing_typings.T_TApp)
next
  case (T_Sub t S T)
  then show ?case
    using subtype_weaken typing_typings.T_Sub by blast
next
  case (T_Let t1 T1 p Δ t2 T2 Δ')
  then have "e (Suc 0) Δ' Δ @ e (Suc 0) 0 Δ' @ B  Γ   (Suc 0) (Δ + Δ') t2 : τ (Suc 0) (Δ + Δ') T2"
    by simp
  with T_Let 
  have "e (Suc 0) 0 Δ' @ B  Γ
           (LET p (Suc 0) Δ' p =  (Suc 0) Δ' t1 IN  (Suc 0) (Δ' + Δ) t2) : τ Δ 0 (τ (Suc 0) (Δ + Δ') T2)"
    by (metis add.commute liftE_length lift_ptyping(1) nat_1 nat_one_as_int
        typing_typings.T_Let)
  with T_Let show ?case
    by (simp add: ac_simps)
next
  case (T_Rcd fs fTs)
  then show ?case
    by (simp add: typing_typings.T_Rcd)
next
  case (T_Proj t fTs l T)
  then show ?case
    by (simp add: liftrT_assoc_Some typing_typings.T_Proj)
next
  case T_Nil
  then show ?case
    by (simp add: typing_typings.T_Nil wfE_weaken)
next
  case (T_Cons t T fs fTs l)
  then show ?case
    by (simp add: typing_typings.T_Cons)
qed

lemma type_weaken': ― ‹A.5(6)›
  "Γ  t : T  Δ @ Γ wf  Δ @ Γ   Δ 0 t : τ Δ 0 T"
proof (induct Δ)
  case Nil
  then show ?case by auto
next
  case (Cons a Δ)
  then have "Δ @ Γ wfB a" "Δ @ Γ wf"
    by (auto elim: well_formedE_cases)
  with Cons type_weaken(1)[of "[]", where B=a] show ?case
    by (metis Suc_eq_plus1 append_Cons append_Nil le_add1 le_refl length_Cons
        liftE.simps(1) liftT_liftT(1) lift_lift(1) list.size(3))
qed

text ‹
The substitution lemmas are now proved by mutual induction on the derivations of
the typing derivations for terms and lists of fields.
›

lemma subst_ptyping:
  " p : T  Δ   p[k τ U]p : T[k τ U]τ  Δ[k τ U]e"
  " fps [:] fTs  Δ   fps[k τ U]rp [:] fTs[k τ U]rτ  Δ[k τ U]e"
proof (induct set: ptyping ptypings)
  case (P_Var T)
  then show ?case
    by (simp add: ptyping.simps)
next
  case (P_Rcd fps fTs Δ)
  then show ?case
    by (simp add: ptyping_ptypings.P_Rcd)
next
  case P_Nil
  then show ?case
    by (simp add: ptyping_ptypings.P_Nil)
next
  case (P_Cons p T Δ1 fps fTs Δ2 l)
  then show ?case
    using ptyping_ptypings.P_Cons by fastforce
qed

theorem subst_type: ― ‹A.8›
  "Δ @ VarB U  Γ  t : T  Γ  u : U 
     e 1 0 Δ @ Γ  t[Δ  u] : τ 1 Δ T"
  "Δ @ VarB U  Γ  fs [:] fTs  Γ  u : U 
     e 1 0 Δ @ Γ  fs[Δ  u]r [:] rτ 1 Δ fTs"
proof (induct "Δ @ VarB U  Γ" t T and "Δ @ VarB U  Γ" fs fTs
    arbitrary: Δ and Δ set: typing typings)
  case (T_Var i U' T  Δ')
  show ?case
  proof -
    have "Δ'[0 τ Top]e @ Γ   Δ' 0 u : T[Δ' τ Top]τ"
      if "i = Δ'"
      using that T_Var type_weaken' wfE_subst wf_Top by fastforce
    moreover have "Δ'[0 τ Top]e @ Γ  Var (i - Suc 0) : T[Δ' τ Top]τ"
      if "Δ' < i"
    proof (intro typing_typings.T_Var)
      show "Δ'[0 τ Top]e @ Γ wf"
        using T_Var.hyps(1) wfE_subst wf_Top by force
      have "Δ'  i - Suc 0"
        using Δ' < i by linarith
      with T_Var that show "(Δ'[0 τ Top]e @ Γ)i - Suc 0 = VarB U'"
        using Suc_diff_Suc by (fastforce simp: split: nat.split_asm)
      show "T[Δ' τ Top]τ = τ (Suc (i - Suc 0)) 0 U'"
        using Δ' < i T_Var.hyps by auto
    qed
    moreover have "Δ'[0 τ Top]e @ Γ  Var i : T[Δ' τ Top]τ"
      if "Δ' > i"
    proof (intro typing_typings.T_Var)
      show "Δ'[0 τ Top]e @ Γ wf"
        using T_Var wfE_subst wf_Top by blast
      show "T[Δ' τ Top]τ = τ (Suc i) 0 (U'[Δ' - Suc i τ Top]τ)"
        using T_Var by (metis that Suc_leI le0 le_add_diff_inverse2 liftT_substT(1))
    qed (use that T_Var in auto)
    ultimately show ?thesis
      by auto
  qed
next
  case (T_Abs T1 t2 T2)
  then show ?case
    by (simp add: typing_typings.T_Abs [THEN T_eq] flip: substT_substT)
next
  case (T_TApp t1 T11 T12 T2)
  then show ?case
    using subst_subtype typing_typings.T_TApp
    apply simp
    by (metis diff_zero le0 substT_substT(1) typing_typings.T_TApp)
next
  case (T_Sub t S T)
  then show ?case
    using subst_subtype typing_typings.T_Sub by blast
next
  case (T_Let t1 T1 p Δ t2 T2 Δ')
  then show ?case
    apply simp
    by (metis add.commute substE_length subst_ptyping(1) typing_typings.T_Let)
next
  case T_Nil
  then show ?case
    by (simp add: typing_typings.T_Nil wfE_subst wf_Top)
qed (auto simp: typing_typings.intros)

theorem substT_type: ― ‹A.11›
  "Δ @ TVarB Q  Γ  t : T  Γ  P <: Q 
     Δ[0 τ P]e @ Γ  t[Δ τ P] : T[Δ τ P]τ"
  "Δ @ TVarB Q  Γ  fs [:] fTs  Γ  P <: Q 
     Δ[0 τ P]e @ Γ  fs[Δ τ P]r [:] fTs[Δ τ P]rτ"
proof (induct "Δ @ TVarB Q  Γ" t T and "Δ @ TVarB Q  Γ" fs fTs
              arbitrary: Δ and Δ set: typing typings)
  case (T_Var i U T Δ)
  show ?case
  proof -
    have "Δ[0 τ P]e @ Γ wf"
      if "Δ < i"
      using that
      by (meson T_Var.hyps(1) T_Var.prems wfE_subst wf_subtypeE)
    moreover have "(Δ[0 τ P]e @ Γ)i - Suc 0 = VarB U"
      if "Δ < i"
      using that T_Var Suc_diff_Suc by (force split: nat.split_asm)
    moreover have "T[Δ τ P]τ = τ (Suc (i - Suc 0)) 0 U"
      if "Δ < i"
      using that T_Var.hyps by fastforce
    moreover have "Δ[0 τ P]e @ Γ  Var i : T[Δ τ P]τ"
      if "Δ = i"
      using T_Var that by auto
    moreover have "Δ[0 τ P]e @ Γ  Var i : T[Δ τ P]τ"
      if "Δ > i"
    proof -
      have "Suc (Δ - Suc 0) = Δ"
        using that by linarith
      then have §: "τ (Suc i) 0 U[Δ τ P]τ = τ (Suc i) 0 (U[Δ - Suc i τ P]τ)"
        using that by fastforce
      show ?thesis
      proof (intro typing_typings.T_Var)
        show "Δ[0 τ P]e @ Γ wf"
          by (meson T_Var.hyps(1) T_Var.prems wfE_subst wf_subtypeE)
        show "(Δ[0 τ P]e @ Γ)i = VarB (U[Δ - Suc i τ P]τ)"
          using § that T_Var by simp
        show "T[Δ τ P]τ = τ (Suc i) 0 (U[Δ - Suc i τ P]τ)"
          using § T_Var by blast
      qed
    qed
    ultimately show ?thesis
      by (metis One_nat_def linorder_cases substT.simps(1) typing_typings.T_Var)
  qed
next
  case (T_Abs T1 t2 T2)
  then show ?case     
    by (simp add: typing_typings.T_Abs [THEN T_eq] flip: substT_substT)
next
  case (T_App t1 T11 T12 t2)
  then show ?case
    using typing_typings.T_App by auto
next
  case (T_TApp t1 T11 T12 T2)
  then show ?case
    apply (simp add: )
    by (metis minus_nat.diff_0 substT_substT(1) substT_subtype typing_typings.T_TApp
        zero_le)
next
  case (T_Sub t S T)
  then show ?case
    using substT_subtype typing_typings.T_Sub by blast
next
  case (T_Let t1 T1 p Δ t2 T2)
  then show ?case
    apply simp
    by (metis add.commute substE_length subst_ptyping(1) typing_typings.T_Let)
next
  case T_Nil
  then show ?case
    by (simp add: typing_typings.T_Nil wfE_subst wf_subtype)
qed (auto simp: typing_typings.intros)

subsection ‹Evaluation›

text ‹
\label{sec:evaluation-rcd}
The definition of canonical values is extended with a clause saying that
a record @{term "Rcd fs"} is a canonical value if all fields contain
canonical values:
›

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

text ‹
In order to formalize the evaluation rule for LET›, we introduce another
relation ⊢ p ⊳ t ⇒ ts› expressing that a pattern @{term p} matches a
term @{term t}. The relation also yields a list of terms @{term ts} corresponding
to the variables in the pattern. The relation is defined simultaneously with another
relation ⊢ fps [⊳] fs ⇒ ts› for matching a list of field patterns @{term fps}
against a list of fields @{term fs}:
›

inductive
  match :: "pat  trm  trm list  bool"  ( _  _  _› [50, 50, 50] 50)
  and matchs :: "rpat  rcd  trm list  bool"  ( _ [⊳] _  _› [50, 50, 50] 50)
where
  M_PVar: " PVar T  t  [t]"
| M_Rcd: " fps [⊳] fs  ts   PRcd fps  Rcd fs  ts"
| M_Nil: " [] [⊳] fs  []"
| M_Cons: "fsl? = t   p  t  ts   fps [⊳] fs  us 
     (l, p)  fps [⊳] fs  ts @ us"

text ‹
The rules of the evaluation relation for the calculus with records are as follows:
›

inductive
  eval :: "trm  trm  bool"  (infixl  50)
  and evals :: "rcd  rcd  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"
| E_LetV: "v  value   p  v  ts  (LET p = v IN t)  t[0 s ts]"
| E_ProjRcd: "fsl? = v  v  value  Rcd fs..l  v"
| E_Proj: "t  t'  t..l  t'..l"
| E_Rcd: "fs [⟼] fs'  Rcd fs  Rcd fs'"
| E_Let: "t  t'  (LET p = t IN u)  (LET p = t' IN u)"
| E_hd: "t  t'  (l, t)  fs [⟼] (l, t')  fs"
| E_tl: "v  value  fs [⟼] fs'  (l, v)  fs [⟼] (l, v)  fs'"

text ‹
The relation @{term "t  t'"} is defined simultaneously with
a relation \mbox{@{term "fs [⟼] fs'"}} for evaluating record fields.
The ``immediate'' reductions, namely pattern matching and projection,
are described by the rules E_LetV› and E_ProjRcd›, respectively,
whereas E_Proj›, E_Rcd›, E_Let›, E_hd› and
E_tl› are congruence rules.
›

lemmas matchs_induct = match_matchs.inducts(2)
  [of _ _ _ "λx y z. True", simplified True_simps, consumes 1,
   case_names M_Nil M_Cons]

lemmas evals_induct = eval_evals.inducts(2)
  [of _ _ "λx y. True", simplified True_simps, consumes 1,
   case_names E_hd E_tl]

lemma matchs_mono:
  assumes H: " fps [⊳] fs  ts"
  shows "fpsl? =    fps [⊳] (l, t)  fs  ts"
  using H
proof (induct rule: matchs_induct)
  case (M_Nil fs)
  then show ?case
    by (simp add: match_matchs.M_Nil)
next
  case (M_Cons fs l t p ts fps us)
  then show ?case
    by (metis assoc.simps(2) fstI match_matchs.M_Cons option.distinct(1))
qed

lemma matchs_eq:
  assumes H: " fps [⊳] fs  ts"
  shows "(l, p)  set fps. fsl? = fs'l?   fps [⊳] fs'  ts"
  using H
proof (induct rule: matchs_induct)
  case (M_Nil fs)
  then show ?case
    using match_matchs.M_Nil by auto
next
  case (M_Cons fs l t p ts fps us)
  then show ?case
    using match_matchs.M_Cons by force
qed

lemma reorder_eq:
  assumes H: " fps [:] fTs  Δ"
  shows "(l, U)set fTs. u. fsl? = u 
         (l, p)  set fps. fsl? = (map (λ(l, T). (l, the (fsl?))) fTs)l?"
  using H by (induct rule: ptypings_induct) auto

lemma matchs_reorder:
  " fps [:] fTs  Δ  (l, U)set fTs. u. fsl? = u 
     fps [⊳] fs  ts   fps [⊳] map (λ(l, T). (l, the (fsl?))) fTs  ts"
  by (rule matchs_eq [OF _ reorder_eq], assumption+)

lemma matchs_reorder':
  " fps [:] fTs  Δ  (l, U)set fTs. u. fsl? = u 
      fps [⊳] map (λ(l, T). (l, the (fsl?))) fTs  ts   fps [⊳] fs  ts"
  by (rule matchs_eq [OF _ reorder_eq [THEN ball_eq_sym]], assumption+)

theorem matchs_tl:
  assumes H: " fps [⊳] (l, t)  fs  ts"
  shows "fpsl? =    fps [⊳] fs  ts"
  using H
proof (induct fps "(l, t)  fs" ts arbitrary: l t fs rule: matchs_induct)
  case M_Nil
  then show ?case
    by (simp add: match_matchs.M_Nil)
next
  case (M_Cons l t p ts fps us)
  then show ?case
    by (metis assoc.simps(2) fst_conv match_matchs.M_Cons not_Some_eq)
qed

theorem match_length:
  " p  t  ts   p : T  Δ  ts = Δ"
  " fps [⊳] ft  ts   fps [:] fTs  Δ  ts = Δ"
  by (induct arbitrary: T Δ and fTs Δ set: match matchs)
    (erule ptyping.cases ptypings.cases, simp+)+

text ‹
In the proof of the preservation theorem
for the calculus with records, we need the following lemma relating
the matching and typing judgements for patterns,
which means that well-typed matching preserves typing. Although this property
will only be used for @{term "Γ1 = []"} later, the statement must be proved in
a more general form in order for the induction to go through.
›

theorem match_type: ― ‹A.17›
  " p : T1  Δ  Γ2  t1 : T1 
     Γ1 @ Δ @ Γ2  t2 : T2   p  t1  ts 
       e Δ 0 Γ1 @ Γ2  t2[Γ1 s ts] : τ Δ Γ1 T2"
  " fps [:] fTs  Δ  Γ2  fs [:] fTs 
     Γ1 @ Δ @ Γ2  t2 : T2   fps [⊳] fs  ts 
       e Δ 0 Γ1 @ Γ2  t2[Γ1 s ts] : τ Δ Γ1 T2"
proof (induct arbitrary: Γ1 Γ2 t1 t2 T2 ts and Γ1 Γ2 fs t2 T2 ts set: ptyping ptypings)
  case (P_Var T Γ1 Γ2 t1 t2 T2 ts)
  from P_Var have "Γ1[0 τ Top]e @ Γ2  t2[Γ1  t1] : T2[Γ1 τ Top]τ"
    by - (rule subst_type [simplified], simp_all)
  moreover from P_Var(3) have "ts = [t1]" by cases simp_all
  ultimately show ?case by simp
next
  case (P_Rcd fps fTs Δ Γ1 Γ2 t1 t2 T2 ts)
  from P_Rcd(5) obtain fs where
    t1: "t1 = Rcd fs" and fps: " fps [⊳] fs  ts" by cases simp_all
  with P_Rcd have fs: "Γ2  Rcd fs : RcdT fTs" by simp
  hence "Γ2  map (λ(l, T). (l, the (fsl?))) fTs [:] fTs"
    by (rule Rcd_type2')
  moreover note P_Rcd(4)
  moreover from fs have "(l, U)set fTs. u. fsl? = u  Γ2  u : U"
    by (rule Rcd_type1')
  hence "(l, U)set fTs. u. fsl? = u" by blast
  with P_Rcd(1) have " fps [⊳] map (λ(l, T). (l, the (fsl?))) fTs  ts"
    using fps by (rule matchs_reorder)
  ultimately show ?case by (rule P_Rcd)
next
  case (P_Nil Γ1 Γ2 fs t2 T2 ts)
  from P_Nil(3) have "ts = []" by cases simp_all
  with P_Nil show ?case by simp
next
  case (P_Cons p T Δ1 fps fTs Δ2 l Γ1 Γ2 fs t2 T2 ts)
  from P_Cons(8) obtain t ts1 ts2 where
    t: "fsl? = t" and p: " p  t  ts1" and fps: " fps [⊳] fs  ts2"
    and ts: "ts = ts1 @ ts2" by cases simp_all
  from P_Cons(6) t fps obtain fs' where
    fps': " fps [⊳] (l, t)  fs'  ts2" and tT: "Γ2  t : T" and fs': "Γ2  fs' [:] fTs"
    and l: "fs'l? = " by cases auto
  from P_Cons have "(Γ1 @ e Δ1 0 Δ2) @ Δ1 @ Γ2  t2 : T2" by simp
  with tT have ts1: "e Δ1 0 (Γ1 @ e Δ1 0 Δ2) @ Γ2 
    t2[Γ1 @ e Δ1 0 Δ2 s ts1] : τ Δ1 Γ1 @ e Δ1 0 Δ2 T2"
    using p by (rule P_Cons)
  from fps' P_Cons(5) have " fps [⊳] fs'  ts2" by (rule matchs_tl)
  with fs' ts1 [simplified]
  have "e Δ2 0 (e Δ1 Δ2 Γ1) @ Γ2  t2[Γ1 + Δ2 s ts1][e Δ1 Δ2 Γ1 s ts2] :
    τ Δ2 e Δ1 Δ2 Γ1 (τ Δ1 (Γ1 + Δ2) T2)"
    by (rule P_Cons(4))
  thus ?case by (simp add: decE_decE [of _ 0, simplified]
    match_length(2) [OF fps P_Cons(3)] ts)
qed

lemma evals_labels [simp]:
  assumes H: "fs [⟼] fs'"
  shows "(fsl? = ) = (fs'l? = )" using H
  by (induct rule: evals_induct) simp_all

theorem preservation: ― ‹A.20›
  "Γ  t : T  t  t'  Γ  t' : T"
  "Γ  fs [:] fTs  fs [⟼] fs'  Γ  fs' [:] fTs"
proof (induct arbitrary: t' and fs' set: typing typings)
  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_typings.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_typings.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_typings.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_typings.T_Sub)
next
  case (T_Let Γ t1 T1 p Δ t2 T2 t')
  from (LET p = t1 IN t2)  t'
  show ?case
  proof cases
    case (E_LetV ts)
    from T_Let (3,1,4)  p  t1  ts
    have "Γ  t2[0 s ts] : τ Δ 0 T2"
      by (rule match_type(1) [of _ _ _ _ _ "[]", simplified])
    with E_LetV show ?thesis by simp
  next
    case (E_Let t'')
    from t1  t''
    have "Γ  t'' : T1" by (rule T_Let)
    hence "Γ  (LET p = t'' IN t2) : τ Δ 0 T2" using T_Let(3,4)
      by (rule typing_typings.T_Let)
    with E_Let show ?thesis by simp
  qed
next
  case (T_Rcd Γ fs fTs t')
  from Rcd fs  t'
  obtain fs' where t': "t' = Rcd fs'" and fs: "fs [⟼] fs'"
    by cases simp_all
  from fs have "Γ  fs' [:] fTs" by (rule T_Rcd)
  hence "Γ  Rcd fs' : RcdT fTs" by (rule typing_typings.T_Rcd)
  with t' show ?case by simp
next
  case (T_Proj Γ t fTs l T t')
  from t..l  t'
  show ?case
  proof cases
    case (E_ProjRcd fs)
    with T_Proj have "Γ  Rcd fs : RcdT fTs" by simp
    hence "(l, U)set fTs. u. fsl? = u  Γ  u : U"
      by (rule Rcd_type1')
    with E_ProjRcd T_Proj show ?thesis by (fastforce dest: assoc_set)
  next
    case (E_Proj t'')
    from t  t''
    have "Γ  t'' : RcdT fTs" by (rule T_Proj)
    hence "Γ  t''..l : T" using T_Proj(3)
      by (rule typing_typings.T_Proj)
    with E_Proj show ?thesis by simp
  qed
next
  case (T_Nil Γ fs')
  from [] [⟼] fs'
  show ?case by cases
next
  case (T_Cons Γ t T fs fTs l fs')
  from (l, t)  fs [⟼] fs'
  show ?case
  proof cases
    case (E_hd t')
    from t  t'
    have "Γ  t' : T" by (rule T_Cons)
    hence "Γ  (l, t')  fs [:] (l, T)  fTs" using T_Cons(3,5)
      by (rule typing_typings.T_Cons)
    with E_hd show ?thesis by simp
  next
    case (E_tl fs'')
    note fs = fs [⟼] fs''
    note T_Cons(1)
    moreover from fs have "Γ  fs'' [:] fTs" by (rule T_Cons)
    moreover from fs T_Cons have "fs''l? = " by simp
    ultimately have "Γ  (l, t)  fs'' [:] (l, T)  fTs"
      by (rule typing_typings.T_Cons)
    with E_tl show ?thesis by simp
  qed
qed

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 rule: typing_induct)
  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)+
next
  case (T_Let t1 T1 p Δ t2 T2 T1' T2')
  from (LET p = t1 IN t2)  value
  show ?case by cases
next
  case (T_Proj t fTs l T1 T2)
  from t..l  value
  show ?case by cases
qed simp_all

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 rule: typing_induct)
  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)+
next
  case (T_Let t1 T1 p Δ t2 T2 T1' T2')
  from (LET p = t1 IN t2)  value
  show ?case by cases
next
  case (T_Proj t fTs l T1 T2)
  from t..l  value
  show ?case by cases
qed simp_all

text ‹
Like in the case of the simple calculus,
we also need a canonical values theorem for record types:
›

lemma RcdT_canonical: ― ‹A.14(2)›
  assumes ty: "[]  v : RcdT fTs"
  shows "v  value 
    fs. v = Rcd fs  ((l, t)  set fs. t  value)" using ty
proof (induct "[]::env" v "RcdT fTs" arbitrary: fTs rule: typing_induct)
  case (T_App t1 T11 t2 fTs)
  from t1  t2  value
  show ?case by cases
next
  case (T_TApp t1 T11 T12 T2 fTs)
  from t1 τ T2  value
  show ?case by cases
next
  case (T_Sub t S fTs)
  from []  S <: RcdT fTs
  obtain fTs' where S: "S = RcdT fTs'"
    by cases (auto simp add: T_Sub)
  show ?case by (rule T_Sub S)+
next
  case (T_Let t1 T1 p Δ t2 T2 fTs)
  from (LET p = t1 IN t2)  value
  show ?case by cases
next
  case (T_Rcd fs fTs)
  from Rcd fs  value
  show ?case using T_Rcd by cases simp_all
next
  case (T_Proj t fTs l fTs')
  from t..l  value
  show ?case by cases
qed simp_all

theorem reorder_prop:
  "(l, t)  set fs. P t  (l, U)set fTs. u. fsl? = u 
     (l, t)  set (map (λ(l, T). (l, the (fsl?))) fTs). P t"
proof (induct fs)
  case Nil
  then show ?case
    by auto
next
  case (Cons a fs)
  then show ?case
    by (smt (verit) assoc_set case_prod_unfold imageE list.set_map option.collapse
        option.simps(3))
qed

text ‹
Another central property needed in the proof of the progress theorem is
that well-typed matching is defined.
This means that if the pattern @{term p} is compatible with the type @{term T} of
the closed term @{term t} that it has to match, then it is always possible to extract a
list of terms @{term ts} corresponding to the variables in @{term p}.
Interestingly, this important property is missing in the description of the
{\sc PoplMark} Challenge cite"PoplMark".
›

theorem ptyping_match:
  " p : T  Δ  []  t : T  t  value 
    ts.  p  t  ts"
  " fps [:] fTs  Δ  []  fs [:] fTs 
    (l, t)  set fs. t  value  us.  fps [⊳] fs  us"
proof (induct arbitrary: t and fs set: ptyping ptypings)
  case (P_Var T t)
  show ?case by (iprover intro: M_PVar)
next
  case (P_Rcd fps fTs Δ t)
  then obtain fs where
    t: "t = Rcd fs" and fs: "(l, t)  set fs. t  value"
    by (blast dest: RcdT_canonical)
  with P_Rcd have fs': "[]  Rcd fs : RcdT fTs" by simp
  hence "[]  map (λ(l, T). (l, the (fsl?))) fTs [:] fTs"
    by (rule Rcd_type2')
  moreover from Rcd_type1' [OF fs']
  have assoc: "(l, U)set fTs. u. fsl? = u" by blast
  with fs have "(l, t)  set (map (λ(l, T). (l, the (fsl?))) fTs). t  value"
    by (rule reorder_prop)
  ultimately have "us.  fps [⊳] map (λ(l, T). (l, the (fsl?))) fTs  us"
    by (rule P_Rcd)
  then obtain us where " fps [⊳] map (λ(l, T). (l, the (fsl?))) fTs  us" ..
  with P_Rcd(1) assoc have " fps [⊳] fs  us" by (rule matchs_reorder')
  hence " PRcd fps  Rcd fs  us" by (rule M_Rcd)
  with t show ?case by fastforce
next
  case (P_Nil fs)
  show ?case by (iprover intro: M_Nil)
next
  case (P_Cons p T Δ1 fps fTs Δ2 l fs)
  from []  fs [:] (l, T)  fTs
  obtain t fs' where fs: "fs = (l, t)  fs'" and t: "[]  t : T"
    and fs': "[]  fs' [:] fTs" by cases auto
  have "((l, t)  fs')l? = t" by simp
  moreover from fs P_Cons have "t  value" by simp
  with t have "ts.  p  t  ts" by (rule P_Cons)
  then obtain ts where " p  t  ts" ..
  moreover from P_Cons fs have "(l, t)set fs'. t  value" by auto
  with fs' have "us.  fps [⊳] fs'  us" by (rule P_Cons)
  then obtain us where " fps [⊳] fs'  us" ..
  hence " fps [⊳] (l, t)  fs'  us" using P_Cons(5) by (rule matchs_mono)
  ultimately have " (l, p)  fps [⊳] (l, t)  fs'  ts @ us"
    by (rule M_Cons)
  with fs show ?case by iprover
qed

theorem progress: ― ‹A.16›
  "[]  t : T  t  value  (t'. t  t')"
  "[]  fs [:] fTs  ((l, t)  set fs. t  value)  (fs'. fs [⟼] fs')"
proof (induct "[]::env" t T and "[]::env" fs fTs set: typing typings)
  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_evals.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_evals.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_evals.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_evals.intros)
    thus ?thesis by iprover
  next
    assume "t'. t1  t'"
    then obtain t' where "t1  t'" ..
    hence "t1 τ T2  t' τ T2" by (rule eval_evals.intros)
    thus ?thesis by iprover
  qed
next
  case (T_Sub t S T)
  show ?case by (rule T_Sub)
next
  case (T_Let t1 T1 p Δ t2 T2)
  hence "t1  value  (t'. t1  t')" by simp
  thus ?case
  proof
    assume t1: "t1  value"
    with T_Let have "ts.  p  t1  ts"
      by (auto intro: ptyping_match)
    with t1 show ?thesis by (blast intro: eval_evals.intros)
  next
    assume "t'. t1  t'"
    thus ?thesis by (blast intro: eval_evals.intros)
  qed
next
  case (T_Rcd fs fTs)
  thus ?case by (blast intro: value.intros eval_evals.intros)
next
  case (T_Proj t fTs l T)
  hence "t  value  (t'. t  t')" by simp
  thus ?case
  proof
    assume tv: "t  value"
    with T_Proj obtain fs where
      t: "t = Rcd fs" and fs: "(l, t)  set fs. t  value"
      by (auto dest: RcdT_canonical)
    with T_Proj have "[]  Rcd fs : RcdT fTs" by simp
    hence "(l, U)set fTs. u. fsl? = u  []  u : U"
      by (rule Rcd_type1')
    with T_Proj obtain u where u: "fsl? = u" by (blast dest: assoc_set)
    with fs have "u  value" by (blast dest: assoc_set)
    with u t show ?case by (blast intro: eval_evals.intros)
  next
    assume "t'. t  t'"
    thus ?case by (blast intro: eval_evals.intros)
  qed
next
  case T_Nil
  show ?case by simp
next
  case (T_Cons t T fs fTs l)
  thus ?case by (auto intro: eval_evals.intros)
qed

end