+ −
theory Tutorial2s+ −
imports Lambda+ −
begin+ −
+ −
section {* Height of a Lambda-Term *}+ −
+ −
text {*+ −
The theory Lambda defines the notions of capture-avoiding+ −
substitution and the height of lambda terms. + −
*}+ −
+ −
thm height.simps+ −
thm subst.simps+ −
+ −
subsection {* EXERCISE 7 *}+ −
+ −
text {* + −
Lets prove a property about the height of substitutions.+ −
+ −
Assume that the height of a lambda-term is always greater + −
or equal to 1.+ −
*}+ −
+ −
lemma height_ge_one: + −
shows "1 \<le> height t"+ −
by (induct t rule: lam.induct) (auto)+ −
+ −
text {* Remove the sorries *}+ −
+ −
theorem+ −
shows "height (t[x ::= t']) \<le> height t - 1 + height t'"+ −
proof (nominal_induct t avoiding: x t' rule: lam.strong_induct)+ −
case (Var y)+ −
have "1 \<le> height t'" using height_ge_one by simp+ −
then show "height (Var y[x ::= t']) \<le> height (Var y) - 1 + height t'" by simp+ −
next + −
case (App t1 t2)+ −
have ih1: "height (t1[x::=t']) \<le> (height t1) - 1 + height t'" + −
and ih2: "height (t2[x::=t']) \<le> (height t2) - 1 + height t'" by fact++ −
then show "height ((App t1 t2)[x ::= t']) \<le> height (App t1 t2) - 1 + height t'" by simp + −
next+ −
case (Lam y t1)+ −
have ih: "height (t1[x::=t']) \<le> height t1 - 1 + height t'" by fact+ −
moreover+ −
have vc: "atom y \<sharp> x" "atom y \<sharp> t'" by fact+ -- {* usual variable convention *}+ −
ultimately + −
show "height ((Lam [y].t1)[x ::= t']) \<le> height (Lam [y].t1) - 1 + height t'" by simp+ −
qed+ −
+ −
+ −
section {* Types and the Weakening Lemma *}+ −
+ −
nominal_datatype ty =+ −
tVar "string"+ −
| tArr "ty" "ty" (infixr "\<rightarrow>" 100)+ −
+ −
+ −
text {* + −
Having defined them as nominal datatypes gives us additional+ −
definitions and theorems that come with types (see below).+ −
+ −
We next define the type of typing contexts, a predicate that+ −
defines valid contexts (i.e. lists that contain only unique+ −
variables) and the typing judgement.+ −
*}+ −
+ −
type_synonym ty_ctx = "(name \<times> ty) list"+ −
+ −
inductive+ −
valid :: "ty_ctx \<Rightarrow> bool"+ −
where+ −
v1[intro]: "valid []"+ −
| v2[intro]: "\<lbrakk>valid \<Gamma>; atom x \<sharp> \<Gamma>\<rbrakk>\<Longrightarrow> valid ((x, T) # \<Gamma>)"+ −
+ −
+ −
inductive+ −
typing :: "ty_ctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60, 60, 60] 60) + −
where+ −
t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"+ −
| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"+ −
| t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1 \<rightarrow> T2"+ −
+ −
+ −
text {*+ −
The predicate atom x \<sharp> \<Gamma>, read as x fresh for \<Gamma>, is defined by + −
Nominal Isabelle. It is defined for lambda-terms, products, lists etc. + −
For example we have:+ −
*}+ −
+ −
lemma+ −
fixes x::"name"+ −
shows "atom x \<sharp> Lam [x].t"+ −
and "atom x \<sharp> (t1, t2) \<Longrightarrow> atom x \<sharp> App t1 t2"+ −
and "atom x \<sharp> Var y \<Longrightarrow> atom x \<sharp> y" + −
and "\<lbrakk>atom x \<sharp> t1; atom x \<sharp> t2\<rbrakk> \<Longrightarrow> atom x \<sharp> (t1, t2)"+ −
and "\<lbrakk>atom x \<sharp> l1; atom x \<sharp> l2\<rbrakk> \<Longrightarrow> atom x \<sharp> (l1 @ l2)"+ −
and "atom x \<sharp> y \<Longrightarrow> x \<noteq> y"+ −
by (simp_all add: lam.fresh fresh_append fresh_at_base) + −
+ −
text {* + −
We can also prove that every variable is fresh for a type. + −
*}+ −
+ −
lemma ty_fresh:+ −
fixes x::"name"+ −
and T::"ty"+ −
shows "atom x \<sharp> T"+ −
by (induct T rule: ty.induct)+ −
(simp_all add: ty.fresh pure_fresh)+ −
+ −
text {* + −
In order to state the weakening lemma in a convenient form, we + −
using the following abbreviation. Abbreviations behave like + −
definitions, except that they are always automatically folded + −
and unfolded.+ −
*}+ −
+ −
abbreviation+ −
"sub_ty_ctx" :: "ty_ctx \<Rightarrow> ty_ctx \<Rightarrow> bool" ("_ \<sqsubseteq> _" [60, 60] 60) + −
where+ −
"\<Gamma>1 \<sqsubseteq> \<Gamma>2 \<equiv> \<forall>x. x \<in> set \<Gamma>1 \<longrightarrow> x \<in> set \<Gamma>2"+ −
+ −
+ −
subsection {* EXERCISE 8 *}+ −
+ −
text {*+ −
Fill in the details and give a proof of the weakening lemma. + −
*}+ −
+ −
lemma + −
assumes a: "\<Gamma>1 \<turnstile> t : T"+ −
and b: "valid \<Gamma>2" + −
and c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"+ −
shows "\<Gamma>2 \<turnstile> t : T"+ −
using a b c+ −
proof (induct arbitrary: \<Gamma>2)+ −
case (t_Var \<Gamma>1 x T)+ −
have a1: "valid \<Gamma>1" by fact+ −
have a2: "(x, T) \<in> set \<Gamma>1" by fact+ −
have a3: "valid \<Gamma>2" by fact+ −
have a4: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact+ −
+ −
show "\<Gamma>2 \<turnstile> Var x : T" sorry+ −
next+ −
case (t_Lam x \<Gamma>1 T1 t T2) + −
have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact+ −
have a0: "atom x \<sharp> \<Gamma>1" by fact+ −
have a1: "valid \<Gamma>2" by fact+ −
have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact+ −
+ −
show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry+ −
qed (auto) -- {* the application case is automatic*}+ −
+ −
+ −
text {* + −
Despite the frequent claim that the weakening lemma is trivial,+ −
routine or obvious, the proof in the lambda-case does not go + −
through smoothly. Painful variable renamings seem to be necessary. + −
But the proof using renamings is horribly complicated (see below). + −
*}+ −
+ −
equivariance valid+ −
equivariance typing+ −
+ −
lemma weakening_NOT_TO_BE_TRIED_AT_HOME: + −
assumes a: "\<Gamma>1 \<turnstile> t : T"+ −
and b: "valid \<Gamma>2" + −
and c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"+ −
shows "\<Gamma>2 \<turnstile> t : T"+ −
using a b c+ −
proof (induct arbitrary: \<Gamma>2)+ −
-- {* lambda case *}+ −
case (t_Lam x \<Gamma>1 T1 t T2) + −
have fc0: "atom x \<sharp> \<Gamma>1" by fact+ −
have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact+ −
-- {* we choose a fresh variable *}+ −
obtain c::"name" where fc1: "atom c \<sharp> (x, t, \<Gamma>1, \<Gamma>2)" by (rule obtain_fresh)+ −
-- {* we alpha-rename the abstraction *}+ −
have "Lam [c].((c \<leftrightarrow> x) \<bullet> t) = Lam [x].t" using fc1+ −
by (auto simp add: lam.eq_iff Abs1_eq_iff flip_def)+ −
moreover+ −
-- {* we can then alpha rename the goal *}+ −
have "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" + −
proof - + −
-- {* we need to establish *} + −
-- {* (1) (x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) *}+ −
-- {* (2) valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)) *}+ −
have "(1)": "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)" + −
proof -+ −
have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact+ −
then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" using fc0 fc1+ −
by (perm_simp) (simp add: flip_fresh_fresh)+ −
then show "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)" by (rule permute_boolE)+ −
qed+ −
moreover + −
have "(2)": "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" + −
proof -+ −
have "valid \<Gamma>2" by fact+ −
then show "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" using fc1+ −
by (auto simp add: fresh_permute_left atom_eqvt valid.eqvt) + −
qed+ −
-- {* these two facts give us by induction hypothesis the following *}+ −
ultimately have "(x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2" using ih by simp + −
-- {* we now apply renamings to get to our goal *}+ −
then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2)" by (rule permute_boolI)+ −
then have "(c, T1) # \<Gamma>2 \<turnstile> ((c \<leftrightarrow> x) \<bullet> t) : T2" using fc1+ −
by (perm_simp) (simp add: flip_fresh_fresh ty_fresh)+ −
then show "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" using fc1 by auto+ −
qed+ −
ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by (simp only:)+ −
qed (auto) -- {* var and app cases, luckily, are automatic *}+ −
+ −
+ −
text {* + −
The remedy is to use again a stronger induction principle that+ −
has the usual "variable convention" already build in. The+ −
following command derives this induction principle for the typing+ −
relation. (We shall explain what happens here later.)+ −
*}+ −
+ −
nominal_inductive typing+ −
avoids t_Lam: "x"+ −
unfolding fresh_star_def+ −
by (simp_all add: fresh_Pair lam.fresh ty_fresh)+ −
+ −
text {* Compare the two induction principles *}+ −
+ −
thm typing.induct+ −
thm typing.strong_induct -- {* note the additional assumption {atom x} \<sharp> c *}+ −
+ −
text {* + −
We can use the stronger induction principle by replacing+ −
the line+ −
+ −
proof (induct arbitrary: \<Gamma>2)+ −
+ −
with + −
+ −
proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)+ −
+ −
Try now the proof.+ −
*}+ −
+ −
subsection {* EXERCISE 9 *} + −
+ −
lemma weakening: + −
assumes a: "\<Gamma>1 \<turnstile> t : T"+ −
and b: "valid \<Gamma>2" + −
and c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"+ −
shows "\<Gamma>2 \<turnstile> t : T"+ −
using a b c+ −
proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)+ −
case (t_Var \<Gamma>1 x T) -- {* variable case is as before *}+ −
have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact + −
moreover + −
have "valid \<Gamma>2" by fact + −
moreover + −
have "(x, T)\<in> set \<Gamma>1" by fact+ −
ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto+ −
next+ −
case (t_Lam x \<Gamma>1 T1 t T2) + −
have vc: "atom x \<sharp> \<Gamma>2" by fact -- {* additional fact afforded by the strong induction *}+ −
have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact+ −
have a0: "atom x \<sharp> \<Gamma>1" by fact+ −
have a1: "valid \<Gamma>2" by fact+ −
have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact+ −
have "valid ((x, T1) # \<Gamma>2)" using a1 vc by auto+ −
moreover+ −
have "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # \<Gamma>2" using a2 by auto+ −
ultimately + −
have "(x, T1) # \<Gamma>2 \<turnstile> t : T2" using ih by simp + −
then show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" using vc by auto+ −
qed (auto) -- {* app case *}+ −
+ −
+ −
+ −
section {* Unbind and an Inconsistency Example *}+ −
+ −
text {*+ −
You might wonder why we had to discharge some proof+ −
obligations in order to obtain the stronger induction+ −
principle for the typing relation. (Remember for+ −
lambda terms this stronger induction principle is+ −
derived automatically.)+ −
+ −
This proof obligation is really needed, because if we + −
assume universally a stronger induction principle, then + −
in some cases we can derive false. This is "shown" below.+ −
*}+ −
+ −
+ −
inductive+ −
unbind :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixr "\<mapsto>" 60)+ −
where+ −
u_Var[intro]: "Var x \<mapsto> Var x"+ −
| u_App[intro]: "App t1 t2 \<mapsto> App t1 t2"+ −
| u_Lam[intro]: "t \<mapsto> t' \<Longrightarrow> Lam [x].t \<mapsto> t'"+ −
+ −
text {* It is clear that the following judgement holds. *}+ −
+ −
lemma unbind_simple:+ −
shows "Lam [x].Var x \<mapsto> Var x"+ −
by auto+ −
+ −
text {*+ −
Now lets derive the strong induction principle for unbind.+ −
The point is that we cannot establish the proof obligations,+ −
therefore we force Isabelle to accept them by using "sorry".+ −
*}+ −
+ −
equivariance unbind+ −
nominal_inductive unbind+ −
avoids u_Lam: "x"+ −
sorry+ −
+ −
text {*+ −
Using the stronger induction principle, we can establish+ −
th follwoing bogus property.+ −
*}+ −
+ −
lemma unbind_fake:+ −
fixes y::"name"+ −
assumes a: "t \<mapsto> t'"+ −
and b: "atom y \<sharp> t"+ −
shows "atom y \<sharp> t'"+ −
using a b+ −
proof (nominal_induct avoiding: y rule: unbind.strong_induct)+ −
case (u_Lam t t' x y)+ −
have ih: "atom y \<sharp> t \<Longrightarrow> atom y \<sharp> t'" by fact+ −
have asm: "atom y \<sharp> Lam [x]. t" by fact+ −
have fc: "atom x \<sharp> y" by fact+ −
then have in_eq: "x \<noteq> y" by (simp add: fresh_at_base)+ −
then have "atom y \<sharp> t" using asm by (simp add: lam.fresh)+ −
then show "atom y \<sharp> t'" using ih by simp+ −
qed+ −
+ −
text {*+ −
And from this follows the inconsitency:+ −
*}+ −
+ −
lemma+ −
shows "False"+ −
proof -+ −
have "atom x \<sharp> Lam [x]. Var x" by (simp add: lam.fresh)+ −
moreover + −
have "Lam [x]. Var x \<mapsto> Var x" using unbind_simple by auto+ −
ultimately + −
have "atom x \<sharp> Var x" using unbind_fake by auto+ −
then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base)+ −
then show "False" by simp+ −
qed+ −
+ −
end+ −