diff -r 87b735f86060 -r ddc05a611005 Tutorial/Tutorial2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Tutorial2.thy	Fri Jan 21 21:58:51 2011 +0100
@@ -0,0 +1,277 @@
+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