diff -r 3485111c7d62 -r e8736c1cdd7f Tutorial/Tutorial2s.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Tutorial2s.thy	Sat Jan 22 16:04:40 2011 -0600
@@ -0,0 +1,354 @@
+
+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
+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