theory Tutorial2imports Lambdabeginsection {* Height of a Lambda-Term *}text {* The theory Lambda defines the notions of capture-avoiding substitution and the height of lambda terms. *}thm height.simpsthm subst.simpssubsection {* 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 height_subst: shows "height (t[x ::= t']) \<le> height t - 1 + height t'"proof (induct t rule: lam.induct) case (Var y) show "height (Var y[x ::= t']) \<le> height (Var y) - 1 + height t'" sorrynext case (App t1 t2) have ih1: "height (t1[x::=t']) \<le> (height t1) - 1 + height t'" by fact have ih2: "height (t2[x::=t']) \<le> (height t2) - 1 + height t'" by fact show "height ((App t1 t2)[x ::= t']) \<le> height (App t1 t2) - 1 + height t'" sorry next case (Lam y t1) have ih: "height (t1[x::=t']) \<le> height t1 - 1 + height t'" by fact -- {* the definition of capture-avoiding substitution *} thm subst.simps show "height ((Lam [y].t1)[x ::= t']) \<le> height (Lam [y].t1) - 1 + height t'" sorryqedtext {* The point is that substitutions can only be moved under a binder provided certain freshness conditions are satisfied. The structural induction above does not say anything about such freshness conditions. Fortunately, Nominal derives automatically some stronger induction principle for lambda terms which has the usual variable convention build in. In the proof below, we use this stronger induction principle. The variable and application case are as before.*}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 simpnext 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 have vc: "atom y \<sharp> x" "atom y \<sharp> t'" by fact+ -- {* usual variable convention *} show "height ((Lam [y].t1)[x ::= t']) \<le> height (Lam [y].t1) - 1 + height t'" sorryqedsection {* 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 cproof (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" sorrynext 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" sorryqed (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 validequivariance typinglemma 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 cproof (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 simpqed (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.inductthm 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 cproof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct) case (t_Var \<Gamma>1 x T) -- {* again the 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 autonext 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 show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorryqed (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 autotext {* 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 unbindnominal_inductive unbind avoids u_Lam: "x" sorrytext {* 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 bproof (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 simpqedtext {* 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 simpqedend