theory Tutorial2

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 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'" sorry

next    

  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'" sorry

qed

text {*

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

  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'" sorry

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

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)  -- {* 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 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

  show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry

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