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