theory Tutorial2
imports Tutorial1
begin

(* fixme: put height example here *)


section {* Types *}

nominal_datatype ty =
  tVar "string"
| tArr "ty" "ty" ("_ \<rightarrow> _" [100, 100] 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 4 *}

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


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 a stronger induction principle that
  has the usual "variable convention" already build in. The
  following command derives this induction principle for us.
  (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 -- {* has 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.
*}
  

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


text {* unbind / inconsistency example *}

inductive
  unbind :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _" [60, 60] 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'"

lemma unbind_simple:
  shows "Lam [x].Var x \<mapsto> Var x"
  by auto

equivariance unbind

nominal_inductive unbind
  avoids u_Lam: "x"
  sorry

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

lemma
  shows "False"
proof -
  have "atom x \<sharp> Lam [x]. Var x" by (simp add: lam.fresh)
  then have "atom x \<sharp> Var x" using unbind_fake unbind_simple by auto
  then show "False" by (simp add: lam.fresh fresh_at_base)
qed

end