# Theory Basis

(*  Author:     Stefan Berghofer, TU Muenchen, 2005
*)

theory Basis
imports Main
begin

section â€¹General Utilitiesâ€º

text â€¹
This section introduces some general utilities that will be useful later on in
the formalization of System \fsub{}.

The following rewrite rules are useful for simplifying mutual induction rules.
â€º

lemma True_simps:
"(True âŸ¹ PROP P) â‰¡ PROP P"
"(PROP P âŸ¹ True) â‰¡ PROP Trueprop True"
"(â‹€x. True) â‰¡ PROP Trueprop True"
apply -
apply rule
apply (erule meta_mp)
apply (rule TrueI)
apply assumption
apply rule
apply (rule TrueI)
apply assumption
apply rule
apply (rule TrueI)+
done

text â€¹
Unfortunately, the standard introduction and elimination rules for bounded
universal and existential quantifier do not work properly for sets of pairs.
â€º

lemma ballpI: "(â‹€x y. (x, y) âˆˆ A âŸ¹ P x y) âŸ¹ âˆ€(x, y) âˆˆ A. P x y"
by blast

lemma bpspec: "âˆ€(x, y) âˆˆ A. P x y âŸ¹ (x, y) âˆˆ A âŸ¹ P x y"
by blast

lemma ballpE: "âˆ€(x, y) âˆˆ A. P x y âŸ¹ (P x y âŸ¹ Q) âŸ¹
((x, y) âˆ‰ A âŸ¹ Q) âŸ¹ Q"
by blast

lemma bexpI: "P x y âŸ¹ (x, y) âˆˆ A âŸ¹ âˆƒ(x, y) âˆˆ A. P x y"
by blast

lemma bexpE: "âˆƒ(x, y) âˆˆ A. P x y âŸ¹
(â‹€x y. (x, y) âˆˆ A âŸ¹ P x y âŸ¹ Q) âŸ¹ Q"
by blast

lemma ball_eq_sym: "âˆ€(x, y) âˆˆ S. f x y = g x y âŸ¹ âˆ€(x, y) âˆˆ S. g x y = f x y"
by auto

lemma wf_measure_size: "wf (measure size)" by simp

notation
Some ("âŒŠ_âŒ‹")

notation
None ("âŠ¥")

notation
length ("âˆ¥_âˆ¥")

notation
Cons ("_ âˆ·/ _" [66, 65] 65)

text â€¹
The following variant of the standard â€¹nthâ€º function returns
â€¹âŠ¥â€º if the index is out of range.
â€º

primrec
nth_el :: "'a list â‡’ nat â‡’ 'a option" ("_âŸ¨_âŸ©" [90, 0] 91)
where
| "(x # xs)âŸ¨iâŸ© = (case i of 0 â‡’ âŒŠxâŒ‹ | Suc j â‡’ xs âŸ¨jâŸ©)"

apply (induct xs arbitrary: i)
apply simp
apply (case_tac i)
apply simp_all
done

lemma [simp]: "âˆ¥xsâˆ¥ â‰¤ i âŸ¹ (xs @ ys)âŸ¨iâŸ© = ysâŸ¨i - âˆ¥xsâˆ¥âŸ©"
apply (induct xs arbitrary: i)
apply simp
apply (case_tac i)
apply simp_all
done

text â€¹Association listsâ€º

primrec assoc :: "('a Ã— 'b) list â‡’ 'a â‡’ 'b option" ("_âŸ¨_âŸ©â‡©?" [90, 0] 91)
where

primrec unique :: "('a Ã— 'b) list â‡’ bool"
where
"unique [] = True"
| "unique (x # xs) = (xsâŸ¨fst xâŸ©â‡©? = âŠ¥ âˆ§ unique xs)"

by (induct ps) (auto split: if_split_asm)

lemma map_assoc_None [simp]:
by (induct ps) auto

no_syntax
"_Map" :: "maplets => 'a â‡€ 'b"  ("(1[_])")

end


# Theory POPLmark

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

theory POPLmark
imports Basis
begin

section â€¹Formalization of the basic calculusâ€º

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

subsection â€¹Types and Termsâ€º

text â€¹
The types of System \fsub{} are represented by the following datatype:
â€º

datatype type =
TVar nat
| Top
| Fun type type    (infixr "â†’" 200)
| TyAll type type  ("(3âˆ€<:_./ _)" [0, 10] 10)

text â€¹
The subtyping and typing judgements depend on a {\it context} (or environment) @{term Î“}
containing bindings for term and type variables. A context is a list of bindings,
where the @{term i}th element @{term "Î“âŸ¨iâŸ©"} corresponds to the variable
with index @{term i}.
â€º

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

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

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

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

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

text â€¹
The following datatype represents the terms of System \fsub{}:
â€º

datatype trm =
Var nat
| Abs type trm   ("(3Î»:_./ _)" [0, 10] 10)
| TAbs type trm  ("(3Î»<:_./ _)" [0, 10] 10)
| App trm trm    (infixl "âˆ™" 200)
| TApp trm type  (infixl "âˆ™â‡©Ï„" 200)

subsection â€¹Lifting and Substitutionâ€º

text â€¹
One of the central operations of $\lambda$-calculus is {\it substitution}.
In order to avoid that free variables in a term or type get captured''
when substituting it for a variable occurring in the scope of a binder,
we have to increment the indices of its free variables during substitution.
This is done by the lifting functions â€¹â†‘â‡©Ï„ n kâ€º and â€¹â†‘ n kâ€º
for types and terms, respectively, which increment the indices of all free
variables with indices â€¹â‰¥ kâ€º by @{term n}. The lifting functions on
types and terms are defined by
â€º

primrec liftT :: "nat â‡’ nat â‡’ type â‡’ type" ("â†‘â‡©Ï„")
where
"â†‘â‡©Ï„ n k (TVar i) = (if i < k then TVar i else TVar (i + n))"
| "â†‘â‡©Ï„ n k Top = Top"
| "â†‘â‡©Ï„ n k (T â†’ U) = â†‘â‡©Ï„ n k T â†’ â†‘â‡©Ï„ n k U"
| "â†‘â‡©Ï„ n k (âˆ€<:T. U) = (âˆ€<:â†‘â‡©Ï„ n k T. â†‘â‡©Ï„ n (k + 1) U)"

primrec lift :: "nat â‡’ nat â‡’ trm â‡’ trm" ("â†‘")
where
"â†‘ n k (Var i) = (if i < k then Var i else Var (i + n))"
| "â†‘ n k (Î»:T. t) = (Î»:â†‘â‡©Ï„ n k T. â†‘ n (k + 1) t)"
| "â†‘ n k (Î»<:T. t) = (Î»<:â†‘â‡©Ï„ n k T. â†‘ n (k + 1) t)"
| "â†‘ n k (s âˆ™ t) = â†‘ n k s âˆ™ â†‘ n k t"
| "â†‘ n k (t âˆ™â‡©Ï„ T) = â†‘ n k t âˆ™â‡©Ï„ â†‘â‡©Ï„ n k T"

text â€¹
It is useful to also define an unlifting'' function â€¹â†“â‡©Ï„ n kâ€º for
decrementing all free variables with indices â€¹â‰¥ kâ€º by @{term n}.
Moreover, we need several substitution functions, denoted by
which substitute type variables in types, type variables in terms,
and term variables in terms, respectively. They are defined as follows:
â€º

primrec substTT :: "type â‡’ nat â‡’ type â‡’ type"  ("_[_ â†¦â‡©Ï„ _]â‡©Ï„" [300, 0, 0] 300)
where
(if k < i then TVar (i - 1) else if i = k then â†‘â‡©Ï„ k 0 S else TVar i)"

primrec decT :: "nat â‡’ nat â‡’ type â‡’ type"  ("â†“â‡©Ï„")
where
"â†“â‡©Ï„ 0 k T = T"

primrec subst :: "trm â‡’ nat â‡’ trm â‡’ trm"  ("_[_ â†¦ _]" [300, 0, 0] 300)
where
"(Var i)[k â†¦ s] = (if k < i then Var (i - 1) else if i = k then â†‘ k 0 s else Var i)"
| "(t âˆ™ u)[k â†¦ s] = t[k â†¦ s] âˆ™ u[k â†¦ s]"
| "(Î»:T. t)[k â†¦ s] = (Î»:â†“â‡©Ï„ 1 k T. t[k+1 â†¦ s])"
| "(Î»<:T. t)[k â†¦ s] = (Î»<:â†“â‡©Ï„ 1 k T. t[k+1 â†¦ s])"

primrec substT :: "trm â‡’ nat â‡’ type â‡’ trm"    ("_[_ â†¦â‡©Ï„ _]" [300, 0, 0] 300)
where
"(Var i)[k â†¦â‡©Ï„ S] = (if k < i then Var (i - 1) else Var i)"

text â€¹
Lifting and substitution extends to typing contexts as follows:
â€º

primrec liftE :: "nat â‡’ nat â‡’ env â‡’ env" ("â†‘â‡©e")
where
"â†‘â‡©e n k [] = []"
| "â†‘â‡©e n k (B âˆ· Î“) = mapB (â†‘â‡©Ï„ n (k + âˆ¥Î“âˆ¥)) B âˆ· â†‘â‡©e n k Î“"

primrec substE :: "env â‡’ nat â‡’ type â‡’ env"  ("_[_ â†¦â‡©Ï„ _]â‡©e" [300, 0, 0] 300)
where

primrec decE :: "nat â‡’ nat â‡’ env â‡’ env"  ("â†“â‡©e")
where
"â†“â‡©e 0 k Î“ = Î“"

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

lemma liftE_length [simp]: "âˆ¥â†‘â‡©e n k Î“âˆ¥ = âˆ¥Î“âˆ¥"
by (induct Î“) simp_all

by (induct Î“) simp_all

lemma liftE_nth [simp]:
apply (induct Î“ arbitrary: i)
apply simp
apply simp
apply (case_tac i)
apply simp
apply simp
done

lemma substE_nth [simp]:
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"
by (induct T arbitrary: i j m n) simp_all

lemma liftT_liftT' [simp]:
"i + m â‰¤ j âŸ¹ â†‘â‡©Ï„ n j (â†‘â‡©Ï„ m i T) = â†‘â‡©Ï„ m i (â†‘â‡©Ï„ n (j - m) T)"
apply (induct T arbitrary: i j m n)
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"
by (induct T arbitrary: k) simp_all

lemma liftT0 [simp]: "â†‘â‡©Ï„ 0 i T = T"
by (induct T arbitrary: i) simp_all

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

theorem substT_liftT [simp]:
"k â‰¤ k' âŸ¹ k' < k + n âŸ¹ (â†‘â‡©Ï„ n k T)[k' â†¦â‡©Ï„ U]â‡©Ï„ = â†‘â‡©Ï„ (n - 1) k T"
by (induct T arbitrary: k k') simp_all

theorem liftT_substT [simp]:
apply (induct T arbitrary: k k')
apply simp_all
done

theorem liftT_substT' [simp]: "k' < k âŸ¹
apply (induct T arbitrary: k k')
apply simp_all
apply arith
done

lemma liftT_substT_Top [simp]:
apply (induct T arbitrary: k k')
apply simp_all
apply arith
done

lemma liftT_substT_strange:
apply (induct T arbitrary: n k)
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 lift_lift [simp]:
"k â‰¤ k' âŸ¹ k' â‰¤ k + n âŸ¹ â†‘ n' k' (â†‘ n k t) = â†‘ (n + n') k t"
by (induct t arbitrary: k k') simp_all

lemma substT_substT:
apply (induct T arbitrary: i j U V)
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

subsection â€¹Well-formednessâ€º

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

inductive
well_formed :: "env â‡’ type â‡’ bool"  ("_ âŠ¢â‡©wâ‡©f _" [50, 50] 50)
where

text â€¹
A context @{term "Î“"} is well-formed, if all types occurring in it only refer to type variables
declared further to the right'':
â€º

inductive
where

text â€¹
with respect to context @{term Î“}, is just an abbreviation for â€¹Î“ âŠ¢â‡©wâ‡©f type_ofB Bâ€º.
We now present a number of properties of the well-formedness judgements that will be used
in the proofs in the following sections.
â€º

inductive_cases well_formed_cases:

inductive_cases well_formedE_cases:

by (rule wf_Cons) simp_all

by (rule wf_Cons) simp_all

lemma map_is_TVarb:
"map is_TVarB Î“' = map is_TVarB Î“ âŸ¹
apply (induct Î“ arbitrary: Î“' T i)
apply simp
apply (auto split: nat.split_asm)
apply (case_tac z)
apply simp_all
done

text â€¹
A type that is well-formed in a context @{term Î“} is also well-formed in another context
@{term Î“'} that contains type variable bindings at the same positions as @{term Î“}:
â€º

lemma wf_equallength:
shows "map is_TVarB Î“' = map is_TVarB Î“ âŸ¹ Î“' âŠ¢â‡©wâ‡©f T" using H
by (induct arbitrary: Î“') (auto intro: well_formed.intros dest: map_is_TVarb)

text â€¹
A well-formed context of the form @{term "Î” @ B âˆ· Î“"} remains well-formed if we replace
the binding @{term B} by another well-formed binding @{term B'}:
â€º

lemma wfE_replace:
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

text â€¹
The following weakening lemmas can easily be proved by structural induction on
types and contexts:
â€º

lemma wf_weaken:
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
done

apply (induct Î”)
apply simp_all
apply (drule_tac B=a in wf_weaken [of "[]", simplified])
apply simp
done

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

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

lemma wf_liftB:
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

text â€¹
We also need lemmas stating that substitution of well-formed types preserves the well-formedness
of types and contexts:
â€º

theorem wf_subst:
apply (induct T arbitrary: Î”)
apply simp_all
apply (rule conjI)
apply (rule impI)
apply simp
apply (rule impI conjI)+
apply (erule well_formed_cases)
apply (rule wf_TVar)
apply (simp split: nat.split_asm)
apply (rename_tac nat Î” T nata)
apply (subgoal_tac "âˆ¥Î”âˆ¥ â‰¤ nat - Suc 0")
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 (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 T1 âˆ· Î”" in meta_spec)
apply simp
done

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 â€¹
\label{sec:subtyping}
We now come to the definition of the subtyping judgement â€¹Î“ âŠ¢ T <: Uâ€º.
â€º

inductive
subtyping :: "env â‡’ type â‡’ type â‡’ bool"  ("_ âŠ¢ _ <: _" [50, 50, 50] 50)
where
| SA_trans_TVar: "Î“âŸ¨iâŸ© = âŒŠTVarB UâŒ‹ âŸ¹
Î“ âŠ¢ â†‘â‡©Ï„ (Suc i) 0 U <: T âŸ¹ Î“ âŠ¢ TVar i <: T"

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

lemma wf_subtype_env:
assumes PQ: "Î“ âŠ¢ P <: Q"
by induct assumption+

lemma wf_subtype:
assumes PQ: "Î“ âŠ¢ P <: Q"
by induct (auto intro: well_formed.intros elim!: wf_equallength)

lemma wf_subtypeE:
assumes H: "Î“ âŠ¢ T <: U"
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

text â€¹
By induction on the derivation of @{term "Î“ âŠ¢ T <: U"}, it can easily be shown
that all types and contexts occurring in a subtyping judgement must be well-formed:
â€º

lemma wf_subtype_conj:
by (erule wf_subtypeE) iprover

text â€¹
By induction on types, we can prove that the subtyping relation is reflexive:
â€º

lemma subtype_refl: â€• â€¹A.1â€º
by (induct T arbitrary: Î“) (blast intro:
subtyping.intros wf_Nil wf_TVarB elim: well_formed_cases)+

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

lemma subtype_weaken:
assumes H: "Î” @ Î“ âŠ¢ P <: Q"
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 âˆ· Î“ âŠ¢
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
with SA_all(4) [of "TVarB Tâ‡©1 âˆ· Î”"]
show ?case by simp (iprover intro: subtyping.SA_all)
qed

text â€¹
All cases are trivial, except for the â€¹SA_trans_TVarâ€º case, which
requires a case distinction on whether the index of the variable is smaller
than @{term "âˆ¥Î”âˆ¥"}.
The stronger result that appending a new context @{term Î”} to a context
@{term Î“} preserves subtyping can be proved by induction on @{term Î”},
using the previous result in the induction step:
â€º

lemma subtype_weaken': â€• â€¹A.2â€º
"Î“ âŠ¢ P <: Q âŸ¹ Î” @ Î“ âŠ¢â‡©wâ‡©f âŸ¹ Î” @ Î“ âŠ¢ â†‘â‡©Ï„ âˆ¥Î”âˆ¥ 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

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

lemma subtype_trans: â€• â€¹A.3â€º
"Î“ âŠ¢ S <: Q âŸ¹ Î“ âŠ¢ Q <: T âŸ¹ Î“ âŠ¢ S <: T"
"Î” @ TVarB Q âˆ· Î“ âŠ¢ M <: N âŸ¹ Î“ âŠ¢ P <: Q âŸ¹
Î” @ TVarB P âˆ· Î“ âŠ¢ M <: N"
using wf_measure_size
proof (induct Q arbitrary: Î“ S T Î” P M N rule: wf_induct_rule)
case (less Q)
{
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
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
with SA_arrow show ?thesis by simp
qed
next
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
by - (rule less(1), simp_all)
by - (rule less(2) [of _ "[]", simplified], simp_all)
by - (rule less(1), simp_all)
by (rule subtyping.SA_all)
with SA_all 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
by (auto elim!: wf_subtypeE)
with â€¹Î“ âŠ¢ P <: Qâ€º
have "(Î” @ [TVarB P]) @ Î“ âŠ¢ â†‘â‡©Ï„ âˆ¥Î” @ [TVarB P]âˆ¥ 0 P <: â†‘â‡©Ï„ âˆ¥Î” @ [TVarB P]âˆ¥ 0 Q"
by (rule subtype_weaken')
with SA_trans_TVar True False have "Î” @ TVarB P âˆ· Î“ âŠ¢ â†‘â‡©Ï„ (Suc âˆ¥Î”âˆ¥) 0 P <: T"
by - (rule tr, simp+)
with True and False and SA_trans_TVar show ?thesis
by (auto intro!: subtyping.SA_trans_TVar)
next
case False
with False' have "i - âˆ¥Î”âˆ¥ = Suc (i - âˆ¥Î”âˆ¥ - 1)" by arith
with False False' SA_trans_TVar show ?thesis
by - (rule subtyping.SA_trans_TVar, simp+)
qed
qed
next
case SA_arrow
thus ?case by (auto intro!: subtyping.SA_arrow)
next
thus ?case by (auto intro: subtyping.SA_all
SA_all(4) [of "TVarB Tâ‡©1 âˆ· Î”", simplified])
qed
}
qed

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

lemma substT_subtype: â€• â€¹A.10â€º
assumes H: "Î” @ TVarB Q âˆ· Î“ âŠ¢ S <: T"
using H
apply (induct "Î” @ TVarB Q âˆ· Î“" S T arbitrary: Î”)
apply simp_all
apply (rule SA_Top)
apply (rule wfE_subst)
apply assumption
apply (erule wf_subtypeE)
apply assumption
apply (rule wf_subst)
apply assumption
apply (erule wf_subtypeE)
apply assumption
apply (rule impI conjI)+
apply (rule subtype_refl)
apply (rule wfE_subst)
apply assumption
apply (erule wf_subtypeE)
apply assumption
apply (erule wf_subtypeE)
apply simp
apply (rule conjI impI)+
apply (rule SA_refl_TVar)
apply (rule wfE_subst)
apply assumption
apply (erule wf_subtypeE)
apply assumption
apply (erule wf_subtypeE)
apply (drule wf_subst)
apply assumption
apply simp
apply (rule impI)
apply (rule SA_refl_TVar)
apply (rule wfE_subst)
apply assumption
apply (erule wf_subtypeE)
apply assumption
apply (erule wf_subtypeE)
apply (drule wf_subst)
apply assumption
apply simp
apply (rule conjI impI)+
apply simp
apply (erule wf_subtypeE)+
apply assumption
apply simp
apply (rule subtype_trans(1))
apply assumption+
apply (rule conjI impI)+
apply (rule SA_trans_TVar)
apply (simp split: nat.split_asm)
apply (subgoal_tac "âˆ¥Î”âˆ¥ â‰¤ i - Suc 0")
apply (rename_tac nat)
apply (subgoal_tac "i - Suc âˆ¥Î”âˆ¥ = nat")
apply (simp (no_asm_simp))
apply arith
apply arith
apply simp
apply (rule impI)
apply (rule SA_trans_TVar)
apply (simp split: nat.split_asm)
apply (subgoal_tac "Suc (âˆ¥Î”âˆ¥ - Suc 0) = âˆ¥Î”âˆ¥")
apply (simp (no_asm_simp))
apply arith
apply (rule SA_arrow)
apply simp+
apply (rule SA_all)
apply simp
apply simp
done

lemma subst_subtype:
assumes H: "Î” @ VarB V âˆ· Î“ âŠ¢ T <: U"
shows "â†“â‡©e 1 0 Î” @ Î“ âŠ¢ â†“â‡©Ï„ 1 âˆ¥Î”âˆ¥ T <: â†“â‡©Ï„ 1 âˆ¥Î”âˆ¥ U"
using H
apply (induct "Î” @ VarB V âˆ· Î“" T U arbitrary: Î”)
apply simp_all
apply (rule SA_Top)
apply (rule wfE_subst)
apply assumption
apply (rule wf_Top)
apply (rule wf_subst)
apply assumption
apply (rule wf_Top)
apply (rule impI conjI)+
apply (rule SA_Top)
apply (rule wfE_subst)
apply assumption
apply (rule wf_Top)+
apply (rule conjI impI)+
apply (rule SA_refl_TVar)
apply (rule wfE_subst)
apply assumption
apply (rule wf_Top)
apply (drule wf_subst)
apply (rule wf_Top)
apply simp
apply (rule impI)
apply (rule SA_refl_TVar)
apply (rule wfE_subst)
apply assumption
apply (rule wf_Top)
apply (drule wf_subst)
apply (rule wf_Top)
apply simp
apply (rule conjI impI)+
apply simp
apply (rule conjI impI)+
apply (simp split: nat.split_asm)
apply (rule SA_trans_TVar)
apply (subgoal_tac "âˆ¥Î”âˆ¥ â‰¤ i - Suc 0")
apply (rename_tac nat)
apply (subgoal_tac "i - Suc âˆ¥Î”âˆ¥ = nat")
apply (simp (no_asm_simp))
apply arith
apply arith
apply simp
apply (rule impI)
apply (rule SA_trans_TVar)
apply simp
apply (subgoal_tac "0 < âˆ¥Î”âˆ¥")
apply simp
apply arith
apply (rule SA_arrow)
apply simp+
apply (rule SA_all)
apply simp
apply simp
done

subsection â€¹Typingâ€º

text â€¹
\label{sec:typing}
We are now ready to give a definition of the typing judgement â€¹Î“ âŠ¢ t : Tâ€º.
â€º

inductive
typing :: "env â‡’ trm â‡’ type â‡’ bool"    ("_ âŠ¢ _ : _" [50, 50, 50] 50)
where
T_Var: "Î“ âŠ¢â‡©wâ‡©f âŸ¹ Î“âŸ¨iâŸ© = âŒŠVarB UâŒ‹ âŸ¹ T = â†‘â‡©Ï„ (Suc i) 0 U âŸ¹ Î“ âŠ¢ Var i : T"
| T_Sub: "Î“ âŠ¢ t : S âŸ¹ Î“ âŠ¢ S <: T âŸ¹ Î“ âŠ¢ t : T"

text â€¹
Note that in the rule â€¹T_Varâ€º, the indices of the type @{term U} looked up in
the context @{term Î“} need to be incremented in order for the type to be well-formed
with respect to @{term Î“}. In the rule â€¹T_Absâ€º, the type @{term "Tâ‡©2"} of the
abstraction body @{term "tâ‡©2"} may not contain the variable with index â€¹0â€º,
since it is a term variable. To compensate for the disappearance of the context
element @{term "VarB Tâ‡©1"} in the conclusion of thy typing rule, the indices of all
free type variables in @{term "Tâ‡©2"} have to be decremented by â€¹1â€º.
â€º

theorem wf_typeE1:
assumes H: "Î“ âŠ¢ t : T"
by induct (blast elim: well_formedE_cases)+

theorem wf_typeE2:
assumes H: "Î“ âŠ¢ t : T"
apply induct
apply simp
apply (rule wf_liftB)
apply assumption+
apply (drule wf_typeE1)+
apply (erule well_formedE_cases)+
apply (rule wf_arrow)
apply simp
apply simp
apply (rule wf_subst [of "[]", simplified])
apply assumption
apply (rule wf_Top)
apply (erule well_formed_cases)
apply assumption
apply (rule wf_all)
apply (drule wf_typeE1)
apply (erule well_formedE_cases)
apply simp
apply assumption
apply (erule well_formed_cases)
apply (rule wf_subst [of "[]", simplified])
apply assumption
apply (erule wf_subtypeE)
apply assumption
apply (erule wf_subtypeE)
apply assumption
done

text â€¹
Like for the subtyping judgement, we can again prove that all types and contexts
involved in a typing judgement are well-formed:
â€º
by (frule wf_typeE1, drule wf_typeE2) iprover

text â€¹
The narrowing theorem for the typing judgement states that replacing the type
of a variable in the context by a subtype preserves typability:
â€º

lemma narrow_type: â€• â€¹A.7â€º
assumes H: "Î” @ TVarB Q âˆ· Î“ âŠ¢ t : T"
shows "Î“ âŠ¢ P <: Q âŸ¹ Î” @ TVarB P âˆ· Î“ âŠ¢ t : T"
using H
apply (induct "Î” @ TVarB Q âˆ· Î“" t T arbitrary: Î”)
apply simp_all
apply (rule T_Var)
apply (erule wfE_replace)
apply (erule wf_subtypeE)
apply simp+
apply (case_tac "i < âˆ¥Î”âˆ¥")
apply simp
apply (case_tac "i = âˆ¥Î”âˆ¥")
apply simp
apply (simp split: nat.split nat.split_asm)+
apply (rule T_Abs [simplified])
apply simp
apply simp+
apply (rule T_TAbs)
apply simp
apply simp
apply (rule subtype_trans(2))
apply assumption+
apply (rule_tac S=S in T_Sub)
apply simp
apply (rule subtype_trans(2))
apply assumption+
done

lemma subtype_refl':
assumes t: "Î“ âŠ¢ t : T"
shows "Î“ âŠ¢ T <: T"
proof (rule subtype_refl)
qed

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)
obtain ty1: "Î“ âŠ¢ U <: Tâ‡©1" and ty2: "Î“ âŠ¢ â†“â‡©Ï„ 1 0 Tâ‡©2 <: U'"
by cases simp_all
show ?case by (rule T_Abs)
next
case (T_Sub Î“ S' T)
from â€¹Î“ âŠ¢ S' <: Tâ€º and â€¹Î“ âŠ¢ T <: U â†’ U'â€º
have "Î“ âŠ¢ S' <: U â†’ U'" by (rule subtype_trans(1))
then show ?case
by (rule T_Sub) (rule T_Sub(5))
qed

lemma Abs_type':
assumes H: "Î“ âŠ¢ (Î»:S. s) : U â†’ U'"
and R: "â‹€S'. Î“ âŠ¢ U <: S âŸ¹ VarB S âˆ· Î“ âŠ¢ s : S' âŸ¹
Î“ âŠ¢ â†“â‡©Ï„ 1 0 S' <: U' âŸ¹ P"
shows "P" using H subtype_refl' [OF H]
by (rule Abs_type) (rule R)

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)
obtain ty1: "Î“ âŠ¢ U <: Tâ‡©1" and ty2: "TVarB U âˆ· Î“ âŠ¢ Tâ‡©2 <: U'"
by cases simp_all
by (rule narrow_type [of "[]", simplified])
with ty1 show ?case using ty2 by (rule T_TAbs)
next
case (T_Sub Î“ S' T)
from â€¹Î“ âŠ¢ S' <: Tâ€º and â€¹Î“ âŠ¢ T <: (âˆ€<:U. U')â€º
have "Î“ âŠ¢ S' <: (âˆ€<:U. U')" by (rule subtype_trans(1))
then show ?case
by (rule T_Sub) (rule T_Sub(5))
qed

lemma TAbs_type':
assumes H: "Î“ âŠ¢ (Î»<:S. s) : (âˆ€<:U. U')"
and R: "â‹€S'. Î“ âŠ¢ U <: S âŸ¹ TVarB U âˆ· Î“ âŠ¢ s : S' âŸ¹
TVarB U âˆ· Î“ âŠ¢ S' <: U' âŸ¹ P"
shows "P" using H subtype_refl' [OF H]
by (rule TAbs_type) (rule R)

lemma T_eq: "Î“ âŠ¢ t : T âŸ¹ T = T' âŸ¹ Î“ âŠ¢ t : T'" by simp

text â€¹
The weakening theorem states that inserting a binding @{term B}
does not affect typing:
â€º

lemma type_weaken:
assumes H: "Î” @ Î“ âŠ¢ t : T"
â†‘â‡©e 1 0 Î” @ B âˆ· Î“ âŠ¢ â†‘ 1 âˆ¥Î”âˆ¥ t : â†‘â‡©Ï„ 1 âˆ¥Î”âˆ¥ T" using H
apply (induct "Î” @ Î“" t T arbitrary: Î”)
apply simp_all
apply (rule conjI)
apply (rule impI)
apply (rule T_Var)
apply (erule wfE_weaken)
apply simp+
apply (rule impI)
apply (rule T_Var)
apply (erule wfE_weaken)
apply assumption
apply (subgoal_tac "Suc i - âˆ¥Î”âˆ¥ = Suc (i - âˆ¥Î”âˆ¥)")
apply simp
apply arith
apply (rule refl)
apply (rule T_Abs [THEN T_eq])
apply simp
apply simp
apply simp
apply simp
apply (rule T_TAbs)
apply simp
apply (erule_tac T_TApp [THEN T_eq])
apply (drule subtype_weaken)
apply simp+
apply (case_tac Î”)
apply (simp add: liftT_substT_strange [of _ 0, simplified])+
apply (rule_tac S="â†‘â‡©Ï„ (Suc 0) âˆ¥Î”âˆ¥ S" in T_Sub)
apply simp
apply (drule subtype_weaken)
apply simp+
done

text â€¹
We can strengthen this result, so as to mean that concatenating a new context
@{term Î”} to the context @{term Î“} preserves typing:
â€º

lemma type_weaken': â€• â€¹A.5(6)â€º
"Î“ âŠ¢ t : T âŸ¹ Î” @ Î“ âŠ¢â‡©wâ‡©f âŸ¹ Î” @ Î“ âŠ¢ â†‘ âˆ¥Î”âˆ¥ 0 t : â†‘â‡©Ï„ âˆ¥Î”âˆ¥ 0 T"
apply (induct Î”)
apply simp
apply simp
apply (erule well_formedE_cases)
apply simp
apply (drule_tac B=a in type_weaken [of "[]", simplified])
apply simp+
done

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

theorem subst_type: â€• â€¹A.8â€º
assumes H: "Î” @ VarB U âˆ· Î“ âŠ¢ t : T"
shows "Î“ âŠ¢ u : U âŸ¹
â†“â‡©e 1 0 Î” @ Î“ âŠ¢ t[âˆ¥Î”âˆ¥ â†¦ u] : â†“â‡©Ï„ 1 âˆ¥Î”âˆ¥ T" using H
apply (induct "Î” @ VarB U âˆ· Î“" t T arbitrary: Î”)
apply simp
apply (rule conjI)
apply (rule impI)
apply simp
apply (rule wfE_subst)
apply assumption
apply (rule wf_Top)
apply simp
apply (rule impI conjI)+
apply (simp split: nat.split_asm)
apply (rule T_Var)
apply (erule wfE_subst)
apply (rule wf_Top)
apply (subgoal_tac "âˆ¥Î”âˆ¥ â‰¤ i - Suc 0")
apply (rename_tac nat)
apply (subgoal_tac "i - Suc âˆ¥Î”âˆ¥ = nat")
apply (simp (no_asm_simp))
apply arith
apply arith
apply simp
apply (rule impI)
apply (rule T_Var)
apply (erule wfE_subst)
apply (rule wf_Top)
apply simp
apply (subgoal_tac "Suc (âˆ¥Î”âˆ¥ - Suc 0) = âˆ¥Î”âˆ¥")
apply (simp (no_asm_simp))
apply arith
apply simp
apply (rule T_Abs [THEN T_eq])
apply simp
apply simp
apply simp+
apply (rule T_TAbs)
apply simp
apply simp
apply (rule T_TApp [THEN T_eq])
apply simp
apply (rule subst_subtype [simplified])
apply assumption
apply simp
apply simp
apply (rule subst_subtype [simplified])
apply assumption
done

theorem substT_type: â€• â€¹A.11â€º
assumes H: "Î” @ TVarB Q âˆ· Î“ âŠ¢ t : T"
shows "Î“ âŠ¢ P <: Q âŸ¹
apply (induct "Î” @ TVarB Q âˆ· Î“" t T arbitrary: Î”)
apply simp_all
apply (rule impI conjI)+
apply simp
apply (rule T_Var)
apply (erule wfE_subst)
apply (erule wf_subtypeE)
apply assumption
apply (simp split: nat.split_asm)
apply (subgoal_tac "âˆ¥Î”âˆ¥ â‰¤ i - Suc 0")
apply (rename_tac nat)
apply (subgoal_tac "i - Suc âˆ¥Î”âˆ¥ = nat")
apply (simp (no_asm_simp))
apply arith
apply arith
apply simp
apply (rule impI)
apply (case_tac "i = âˆ¥Î”âˆ¥")
apply simp
apply (rule T_Var)
apply (erule wfE_subst)
apply (erule wf_subtypeE)
apply assumption
apply simp
apply (subgoal_tac "i < âˆ¥Î”âˆ¥")
apply (subgoal_tac "Suc (âˆ¥Î”âˆ¥ - Suc 0) = âˆ¥Î”âˆ¥")
apply (simp (no_asm_simp))
apply arith
apply arith
apply (rule T_Abs [THEN T_eq])
apply simp
apply simp+
apply (rule T_TAbs)
apply simp
apply (rule T_TApp [THEN T_eq])
apply simp
apply (rule substT_subtype)
apply assumption
apply assumption
apply simp
apply (rule substT_subtype)
apply assumption
apply assumption
done

subsection â€¹Evaluationâ€º

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

inductive_set
"value" :: "trm set"
where
Abs: "(Î»:T. t) âˆˆ value"
| TAbs: "(Î»<:T. t) âˆˆ value"

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

inductive
eval :: "trm â‡’ trm â‡’ bool"  (infixl "âŸ¼" 50)
where
| E_App1: "t âŸ¼ t' âŸ¹ t âˆ™ u âŸ¼ t' âˆ™ u"
| E_App2: "v âˆˆ value âŸ¹ t âŸ¼ t' âŸ¹ v âˆ™ t âŸ¼ v âˆ™ t'"
| E_TApp: "t âŸ¼ t' âŸ¹ t âˆ™â‡©Ï„ T âŸ¼ t' âˆ™â‡©Ï„ T"

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

theorem preservation: â€• â€¹A.20â€º
assumes H: "Î“ âŠ¢ t : T"
shows "t âŸ¼ t' âŸ¹ Î“ âŠ¢ t' : T" using H
proof (induct arbitrary: t')
case (T_Var Î“ i U T t')
from â€¹Var i âŸ¼ t'â€º
show ?case by cases
next
show ?case by cases
next
show ?case
proof cases
then obtain S'
by (rule subst_type [where Î”="[]", simplified])
with E_Abs show ?thesis by simp
next
case (E_App1 t'')
by (rule typing.T_App)
with E_App1 show ?thesis by simp
next
case (E_App2 t'')
by (rule typing.T_App)
with E_App2 show ?thesis by simp
qed
next
show ?case by cases
next
show ?case
proof cases
then obtain S'
by (rule substT_type [where Î”="[]", simplified])
with E_TAbs show ?thesis by simp
next
case (E_TApp t'')
by (rule typing.T_TApp)
with E_TApp show ?thesis by simp
qed
next
case (T_Sub Î“ t S T t')
from â€¹t âŸ¼ t'â€º
have "Î“ âŠ¢ t' : S" by (rule T_Sub)
then show ?case using â€¹Î“ âŠ¢ S <: Tâ€º
by (rule typing.T_Sub)
qed

text â€¹
The progress theorem is also proved by induction on the derivation of
@{term "[] âŠ¢ t : T"}. In the induction steps, we need the following two lemmas
must be abstractions over term and type variables, respectively.
â€º

lemma Fun_canonical: â€• â€¹A.14(1)â€º
shows "v âˆˆ value âŸ¹ âˆƒt S. v = (Î»:S. t)" using ty
case T_Abs
show ?case by iprover
next
show ?case by cases
next
show ?case by cases
next
by cases (auto simp add: T_Sub)
show ?case by (rule T_Sub S)+
qed simp

lemma TyAll_canonical: â€• â€¹A.14(3)â€º
shows "v âˆˆ value âŸ¹ âˆƒt S. v = (Î»<:S. t)" using ty
show ?case by cases
next
case T_TAbs
show ?case by iprover
next
show ?case by cases
next
by cases (auto simp add: T_Sub)
show ?case by (rule T_Sub S)+
qed simp

theorem progress:
assumes ty: "[] âŠ¢ t : T"
shows "t âˆˆ value âˆ¨ (âˆƒt'. t âŸ¼ t')" using ty
proof (induct "[]::env" t T)
case T_Var
thus ?case by simp
next
case T_Abs
from value.Abs show ?case ..
next
thus ?case
proof
by (auto dest!: Fun_canonical)
from T_App have "tâ‡©2 âˆˆ value âˆ¨ (âˆƒt'. tâ‡©2 âŸ¼ t')" by simp
thus ?thesis
proof
by simp (rule eval.intros)
thus ?thesis by iprover
next
then obtain t' where "tâ‡©2 âŸ¼ t'" by iprover
thus ?thesis by iprover
qed
next
then obtain t' where "tâ‡©1 âŸ¼ t'" ..
thus ?thesis by iprover
qed
next
case T_TAbs
from value.TAbs show ?case ..
next
thus ?case
proof
with T_TApp obtain t S where "tâ‡©1 = (Î»<:S. t)"
by (auto dest!: TyAll_canonical)
thus ?thesis by iprover
next
then obtain t' where "tâ‡©1 âŸ¼ t'" ..
thus ?thesis by iprover
qed
next
case (T_Sub t S T)
show ?case by (rule T_Sub)
qed

end


# 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
â€º

subsection â€¹Lifting and Substitutionâ€º

primrec psize :: "pat â‡’ nat" ("âˆ¥_âˆ¥â‡©p")
and rsize :: "rpat â‡’ nat" ("âˆ¥_âˆ¥â‡©r")
and fsize :: "fpat â‡’ nat" ("âˆ¥_âˆ¥â‡©f")
where

primrec liftT :: "nat â‡’ nat â‡’ type â‡’ type" ("â†‘â‡©Ï„")
where
"â†‘â‡©Ï„ n k (TVar i) = (if i < k then TVar i else TVar (i + n))"
| "â†‘â‡©Ï„ n k Top = Top"
| "â†‘â‡©Ï„ n k (T â†’ U) = â†‘â‡©Ï„ n k T â†’ â†‘â‡©Ï„ n k U"
| "â†‘â‡©Ï„ n k (âˆ€<:T. U) = (âˆ€<:â†‘â‡©Ï„ n k T. â†‘â‡©Ï„ n (k + 1) U)"

primrec liftp :: "nat â‡’ nat â‡’ pat â‡’ pat" ("â†‘â‡©p")
where

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
(if k < i then TVar (i - 1) else if i = k then â†‘â‡©Ï„ k 0 S else TVar i)"

primrec substpT :: "pat â‡’ nat â‡’ type â‡’ pat"  ("_[_ â†¦â‡©Ï„ _]â‡©p" [300, 0, 0] 300)
and substrpT :: "rpat â‡’ nat â‡’ type â‡’ rpat"  ("_[_ â†¦â‡©Ï„ _]â‡©râ‡©p" [300, 0, 0] 300)
and substfpT :: "fpat â‡’ nat â‡’ type â‡’ fpat"  ("_[_ â†¦â‡©Ï„ _]â‡©fâ‡©p" [300, 0, 0] 300)
where

primrec decp :: "nat â‡’ nat â‡’ pat â‡’ pat"  ("â†“â‡©p")
where
"â†“â‡©p 0 k p = 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
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 â†¦â‡©Ï„ 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 = []"
| "(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)"
| "(LET p = t IN u)[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

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 u âˆ· us] = t[k + âˆ¥usâˆ¥ â†¦ u][k â†¦â‡©s us]"

primrec decT :: "nat â‡’ nat â‡’ type â‡’ type"  ("â†“â‡©Ï„")
where
"â†“â‡©Ï„ 0 k T = T"

primrec decE :: "nat â‡’ nat â‡’ env â‡’ env"  ("â†“â‡©e")
where
"â†“â‡©e 0 k Î“ = Î“"

where

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

by (induct Î“) simp_all

lemma liftE_nth [simp]:
apply (induct Î“ arbitrary: i)
apply simp
apply simp
apply (case_tac i)
apply simp
apply simp
done

lemma substE_nth [simp]:
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"
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)"
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"
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"
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"
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]:
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 âŸ¹
"k' < k âŸ¹
"k' < k âŸ¹
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]:
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]:
apply (induct Î“ arbitrary: k k' and k k' and k k')
apply simp_all
apply (case_tac a)
done

lemma liftT_decT [simp]:
by (induct m arbitrary: T) simp_all

lemma liftT_substT_strange:
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"
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]:
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 âŸ¹
"i â‰¤ j âŸ¹
"i â‰¤ j âŸ¹
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]:
by (induct i arbitrary: T j) (simp_all add: substT_substT [symmetric])

lemma substT_decT' [simp]:
by (induct k arbitrary: i j T) (simp_all add: substT_substT [of _ _ _ _ Top, simplified])

lemma substE_substE:
apply (induct Î“)
apply (case_tac  a)
done

lemma substT_decE [simp]:
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]:
by (induct Î“) (simp_all add: ac_simps)

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  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  "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  a)
apply simp_all
done

theorem liftE0 [simp]: "â†‘â‡©e 0 k Î“ = Î“"
apply (induct Î“)
apply (case_tac  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

by (induct fs rule: list.induct) auto

by (induct fs rule: list.induct) auto

by (induct fps rule: list.induct) auto

by (induct fs rule: list.induct) auto

by (induct fs rule: list.induct) auto

by (induct fs rule: list.induct) auto

lemma substrTT_assoc_Some [simp]:
by (induct fs rule: list.induct) auto

by (induct fs rule: list.induct) auto

by (induct fps rule: list.induct) auto

by (induct fs rule: list.induct) auto

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

by (induct fs rule: list.induct) auto

lemma substrT_setD:
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"  ("_ âŠ¢â‡©wâ‡©f _" [50, 50] 50)
where

inductive
where

inductive_cases well_formed_cases:

inductive_cases well_formedE_cases:

by (rule wf_Cons) simp_all

by (rule wf_Cons) simp_all

lemma map_is_TVarb:
"map is_TVarB Î“' = map is_TVarB Î“ âŸ¹
apply (induct Î“ arbitrary: Î“' T i)
apply simp
apply (auto split: nat.split_asm)
apply (case_tac z)
apply simp_all
done

lemma wf_equallength:
shows "map is_TVarB Î“' = map is_TVarB Î“ âŸ¹ Î“' âŠ¢â‡©wâ‡©f 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:
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:
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 simp+
done

apply (induct Î”)
apply simp_all
apply (drule_tac B=a in wf_weaken [of "[]", simplified])
apply simp
done

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:
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:
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 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
done

apply (induct Î” arbitrary: T)
apply simp
apply simp
apply (drule wf_subst(1) [of "[]", simplified])
apply (rule wf_Top)
apply simp
done

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
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'}
â€º

inductive
subtyping :: "env â‡’ type â‡’ type â‡’ bool"  ("_ âŠ¢ _ <: _" [50, 50, 50] 50)
where
| SA_trans_TVar: "Î“âŸ¨iâŸ© = âŒŠTVarB UâŒ‹ âŸ¹
Î“ âŠ¢ â†‘â‡©Ï„ (Suc i) 0 U <: T âŸ¹ Î“ âŠ¢ TVar i <: T"
âˆ€(l, T)âˆˆset fs'. âˆƒS. (l, S)âˆˆset fs âˆ§ Î“ âŠ¢ S <: T âŸ¹ Î“ âŠ¢ RcdT fs <: RcdT fs'"

lemma wf_subtype_env:
assumes PQ: "Î“ âŠ¢ P <: Q"
by induct assumption+

lemma wf_subtype:
assumes PQ: "Î“ âŠ¢ P <: Q"
by induct (auto intro: well_formed.intros elim!: wf_equallength)

lemma wf_subtypeE:
assumes H: "Î“ âŠ¢ T <: U"
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â€º
by (induct T and fTs and fT arbitrary: Î“ and Î“ and Î“
rule: liftT.induct liftrT.induct liftfT.induct,
(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"
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 âˆ· Î“ âŠ¢
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
with SA_all(4) [of "TVarB Tâ‡©1 âˆ· Î”"]
show ?case by simp (iprover intro: subtyping.SA_all)
next
case (SA_Rcd fs fs')
with wf have "â†‘â‡©e (Suc 0) 0 Î” @ B âˆ· Î“ âŠ¢â‡©wâ‡©f" by simp (rule wfE_weaken)
by (rule wf_weaken)
moreover from SA_Rcd have "unique (â†‘â‡©râ‡©Ï„ (Suc 0) âˆ¥Î”âˆ¥ fs')" by simp
âˆƒS. (l, S)âˆˆset (â†‘â‡©râ‡©Ï„ (Suc 0) âˆ¥Î”âˆ¥ fs) âˆ§ â†‘â‡©e (Suc 0) 0 Î” @ B âˆ· Î“ âŠ¢ S <: T"
proof (rule ballpI)
fix l T
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"
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
by (rule subtyping.SA_Rcd)
thus ?case by simp
qed

lemma subtype_weaken': â€• â€¹A.2â€º
"Î“ âŠ¢ P <: Q âŸ¹ Î” @ Î“ âŠ¢â‡©wâ‡©f âŸ¹ Î” @ Î“ âŠ¢ â†‘â‡©Ï„ âˆ¥Î”âˆ¥ 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 (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
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
with SA_arrow show ?thesis by simp
qed
next
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
by - (rule less(1), simp_all)
by - (rule less(2) [of _ "[]", simplified], simp_all)
by - (rule less(1), simp_all)
by (rule subtyping.SA_all)
with SA_all show ?thesis by simp
qed
next
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
moreover have "âˆ€(l, T)âˆˆset fsâ‡©2'. âˆƒS. (l, S)âˆˆset fsâ‡©1 âˆ§ Î“ âŠ¢ S <: T"
proof (rule ballpI)
fix l T
assume lT: "(l, T) âˆˆ set fsâ‡©2'"
with SA_Rcd obtain U where
fs2: "(l, U) âˆˆ set fsâ‡©2" and UT: "Î“ âŠ¢ U <: T" by blast
with SA_Rcd SA_Rcd' obtain S where
fs1: "(l, S) âˆˆ set fsâ‡©1" 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 fsâ‡©1 âˆ§ Î“ âŠ¢ S <: T" by blast
qed
ultimately have "Î“ âŠ¢ RcdT fsâ‡©1 <: RcdT fsâ‡©2'" 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
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
thus ?case by (auto intro: subtyping.SA_all
SA_all(4) [of "TVarB Tâ‡©1 âˆ· Î”", simplified])
next
case (SA_Rcd fs fs')
from â€¹Î“ âŠ¢ P <: Qâ€º have "Î“ âŠ¢â‡©wâ‡©f P" by (rule wf_subtypeE)
by - (rule wfE_replace, simp+)
moreover from SA_Rcd have "Î” @ TVarB Q âˆ· Î“ âŠ¢â‡©wâ‡©f RcdT fs" by simp
hence "Î” @ TVarB P âˆ· Î“ âŠ¢â‡©wâ‡©f 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 âŸ¹
using H
apply (induct "Î” @ TVarB Q âˆ· Î“" S T arbitrary: Î”)
apply simp_all
apply (rule SA_Top)
apply (rule wfE_subst)
apply assumption
apply (erule wf_subtypeE)
apply assumption
apply (rule wf_subst)
apply assumption
apply (erule wf_subtypeE)
apply assumption
apply (rule impI conjI)+
apply (rule subtype_refl)
apply (rule wfE_subst)
apply assumption
apply (erule wf_subtypeE)
apply assumption
apply (erule wf_subtypeE)
apply simp
apply (rule conjI impI)+
apply (rule SA_refl_TVar)
apply (rule wfE_subst)
apply assumption
apply (erule wf_subtypeE)
apply assumption
apply (erule wf_subtypeE)
apply (drule wf_subst)
apply assumption
apply simp
apply (rule impI)
apply (rule SA_refl_TVar)
apply (rule wfE_subst)
apply assumption
apply (erule wf_subtypeE)
apply assumption
apply (erule wf_subtypeE)
apply (drule wf_subst)
apply assumption
apply simp
apply (rule conjI impI)+
apply simp
apply (erule wf_subtypeE)+
apply assumption
apply simp
apply (rule subtype_trans(1))
apply assumption+
apply (rule conjI impI)+
apply (rule SA_trans_TVar)
apply (simp split: nat.split_asm)
apply (subgoal_tac "âˆ¥Î”âˆ¥ â‰¤ i - Suc 0")
apply (rename_tac nat)
apply (subgoal_tac "i - Suc âˆ¥Î”âˆ¥ = nat")
apply (simp (no_asm_simp))
apply arith
apply arith
apply simp
apply (rule impI)
apply (rule SA_trans_TVar)
apply (simp split: nat.split_asm)
apply (subgoal_tac "Suc (âˆ¥Î”âˆ¥ - Suc 0) = âˆ¥Î”âˆ¥")
apply (simp (no_asm_simp))
apply arith
apply (rule SA_arrow)
apply simp+
apply (rule SA_all)
apply simp
apply simp
apply (erule wf_subtypeE)
apply (rule SA_Rcd)
apply (erule wfE_subst)
apply assumption
apply (drule wf_subst)
apply assumption
apply simp
apply simp
apply (rule ballpI)
apply (drule substrT_setD)
apply (erule exE conjE)+
apply (drule bpspec)
apply assumption
apply simp
apply (erule exE)
apply (erule conjE)+
apply (rule exI)
apply (rule conjI)
apply (erule substrT_set)
apply assumption
done

lemma subst_subtype:
assumes H: "Î” @ VarB V âˆ· Î“ âŠ¢ T <: U"
shows "â†“â‡©e 1 0 Î” @ Î“ âŠ¢ â†“â‡©Ï„ 1 âˆ¥Î”âˆ¥ T <: â†“â‡©Ï„ 1 âˆ¥Î”âˆ¥ U"
using H
apply (induct "Î” @ VarB V âˆ· Î“" T U arbitrary: Î”)
apply simp_all
apply (rule SA_Top)
apply (rule wfE_subst)
apply assumption
apply (rule wf_Top)
apply (rule wf_subst)
apply assumption
apply (rule wf_Top)
apply (rule impI conjI)+
apply (rule SA_Top)
apply (rule wfE_subst)
apply assumption
apply (rule wf_Top)+
apply (rule conjI impI)+
apply (rule SA_refl_TVar)
apply (rule wfE_subst)
apply assumption
apply (rule wf_Top)
apply (drule wf_subst)
apply (rule wf_Top)
apply simp
apply (rule impI)
apply (rule SA_refl_TVar)
apply (rule wfE_subst)
apply assumption
apply (rule wf_Top)
apply (drule wf_subst)
apply (rule wf_Top)
apply simp
apply (rule conjI impI)+
apply simp
apply (rule conjI impI)+
apply (simp split: nat.split_asm)
apply (rule SA_trans_TVar)
apply (subgoal_tac "âˆ¥Î”âˆ¥ â‰¤ i - Suc 0")
apply (rename_tac nat)
apply (subgoal_tac "i - Suc âˆ¥Î”âˆ¥ = nat")
apply (simp (no_asm_simp))
apply arith
apply arith
apply simp
apply (rule impI)
apply (rule SA_trans_TVar)
apply simp
apply (subgoal_tac "0 < âˆ¥Î”âˆ¥")
apply simp
apply arith
apply (rule SA_arrow)
apply simp+
apply (rule SA_all)
apply simp
apply simp
apply (rule SA_Rcd)
apply (erule wfE_subst)
apply (rule wf_Top)
apply (drule wf_subst)
apply (rule wf_Top)
apply simp
apply simp
apply (rule ballpI)
apply (drule substrT_setD)
apply (erule exE conjE)+
apply (drule bpspec)
apply assumption
apply simp
apply (erule exE)
apply (erule conjE)+
apply (rule exI)
apply (rule conjI)
apply (erule substrT_set)
apply assumption
done

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: "âŠ¢ [] [:] [] â‡’ []"

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: "Î“ âŠ¢â‡©wâ‡©f âŸ¹ Î“âŸ¨iâŸ© = âŒŠVarB UâŒ‹ âŸ¹ T = â†‘â‡©Ï„ (Suc i) 0 U âŸ¹ Î“ âŠ¢ Var i : T"
| T_Sub: "Î“ âŠ¢ t : S âŸ¹ Î“ âŠ¢ S <: T âŸ¹ Î“ âŠ¢ t : T"
| T_Rcd: "Î“ âŠ¢ fs [:] fTs âŸ¹ Î“ âŠ¢ Rcd fs : RcdT fTs"
| T_Proj: "Î“ âŠ¢ t : RcdT fTs âŸ¹ fTsâŸ¨lâŸ©â‡©? = âŒŠTâŒ‹ âŸ¹ Î“ âŠ¢ t..l : T"
| T_Cons: "Î“ âŠ¢ t : T âŸ¹ Î“ âŠ¢ fs [:] fTs âŸ¹ fsâŸ¨lâŸ©â‡©? = âŠ¥ âŸ¹
Î“ âŠ¢ (l, t) âˆ· fs [:] (l, T) âˆ· fTs"

theorem wf_typeE1:
by (induct set: typing typings) (blast elim: well_formedE_cases)+

theorem wf_typeE2:
"Î“' âŠ¢ fs [:] fTs âŸ¹ (âˆ€(l, T) âˆˆ set fTs. Î“' âŠ¢â‡©wâ‡©f T) âˆ§
apply (induct set: typing typings)
apply simp
apply (rule wf_liftB)
apply assumption+
apply (drule wf_typeE1)+
apply (erule well_formedE_cases)+
apply (rule wf_arrow)
apply simp
apply simp
apply (rule wf_subst [of "[]", simplified])
apply assumption
apply (rule wf_Top)
apply (erule well_formed_cases)
apply assumption
apply (rule wf_all)
apply (drule wf_typeE1)
apply (erule well_formedE_cases)
apply simp
apply assumption
apply (erule well_formed_cases)
apply (rule wf_subst [of "[]", simplified])
apply assumption
apply (erule wf_subtypeE)
apply assumption
apply (erule wf_subtypeE)
apply assumption
â€• â€¹recordsâ€º
apply (erule wf_dec)
apply (erule conjE)+
apply (rule wf_RcdT)
apply assumption+
apply (erule well_formed_cases)
apply (blast dest: assoc_set)
apply simp
apply simp
done

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"
apply (induct "Î” @ TVarB Q âˆ· Î“" t T and "Î” @ TVarB Q âˆ· Î“" ts Ts
arbitrary: Î” and Î” set: typing typings)
apply simp_all
apply (rule T_Var)
apply (erule wfE_replace)
apply (erule wf_subtypeE)
apply simp+
apply (case_tac "i < âˆ¥Î”âˆ¥")
apply simp
apply (case_tac "i = âˆ¥Î”âˆ¥")
apply simp
apply (simp split: nat.split nat.split_asm)+
apply (rule T_Abs [simplified])
apply simp
apply simp+
apply (rule T_TAbs)
apply simp
apply simp
apply (rule subtype_trans(2))
apply assumption+
apply (rule_tac S=S in T_Sub)
apply simp
apply (rule subtype_trans(2))
apply assumption+
â€• â€¹recordsâ€º
apply (rule T_Let)
apply blast
apply assumption
apply simp
apply (rule T_Rcd)
apply simp
apply (rule T_Proj)
apply blast
apply assumption
apply (rule T_Nil)
apply (erule wfE_replace)
apply (erule wf_subtypeE)
apply simp+
apply (rule T_Cons)
apply simp+
done

lemma typings_setD:
assumes H: "Î“ âŠ¢ fs [:] fTs"
shows "(l, T) âˆˆ set fTs âŸ¹ âˆƒt. fsâŸ¨lâŸ©â‡©? = âŒŠtâŒ‹ âˆ§ Î“ âŠ¢ t : T"
using H
by (induct arbitrary: l T rule: typings_induct) fastforce+

lemma subtype_refl':
assumes t: "Î“ âŠ¢ t : T"
shows "Î“ âŠ¢ T <: T"
proof (rule subtype_refl)
from t show "Î“ âŠ¢â