# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295643531 -3600
# Node ID ddc05a611005f036f038b2f1c19484a9c7170d0c
# Parent  87b735f860606edadcc4172a9ce1a8511e6da7c9
added unbind example

diff -r 87b735f86060 -r ddc05a611005 Tutorial/Tutorial1.thy
--- a/Tutorial/Tutorial1.thy	Fri Jan 21 00:55:28 2011 +0100
+++ b/Tutorial/Tutorial1.thy	Fri Jan 21 21:58:51 2011 +0100
@@ -5,26 +5,26 @@
   ====================================
 
   Nominal Isabelle is a definitional extension of Isabelle/HOL, which
-  means it does not add any new axioms to higher-order logic. It merely
+  means it does not add any new axioms to higher-order logic. It just
   adds new definitions and an infrastructure for 'nominal resoning'.
 
 
   The jEdit Interface
   -------------------
 
-  The Isabelle theorem prover comes with an interface for the jEdit. 
+  The Isabelle theorem prover comes with an interface for jEdit. 
   Unlike many other theorem prover interfaces (e.g. ProofGeneral) where you 
-  try to advance a 'checked' region in a proof script, this interface immediately 
-  checks the whole buffer. The text you type is also immediately checked
-  as you type. Malformed text or unfinished proofs are highlighted in red 
-  with a little red 'stop' signal on the left-hand side. If you drag the 
-  'red-box' cursor over a line, the Output window gives further feedback. 
+  advance a 'checked' region in a proof script, this interface immediately 
+  checks the whole buffer. The text you type is also immediately checked. 
+  Malformed text or unfinished proofs are highlighted in red with a little 
+  red 'stop' signal on the left-hand side. If you drag the 'red-box' cursor 
+  over a line, the Output window gives further feedback. 
 
   Note: If a section is not parsed correctly, the work-around is to cut it 
   out and paste it back into the text (cut-out: Ctrl + X; paste in: Ctrl + V;
   Cmd is Ctrl on the Mac)
 
-  Nominal Isabelle and the interface can be started on the command line with
+  Nominal Isabelle and jEdit can be started by typing on the command line
 
      isabelle jedit -l HOL-Nominal2
      isabelle jedit -l HOL-Nominal2 A.thy B.thy ...
@@ -55,10 +55,10 @@
           :       \<in>
           ~:      \<notin>
 
-  For nominal two important symbols are
+  For nominal the following two symbols have a special meaning
 
-          \<sharp>       sharp     (freshness)
-          \<bullet>       bullet    (permutations)
+        \<sharp>    sharp     (freshness)
+        \<bullet>    bullet    (permutation application)
 *}
 
 theory Tutorial1
@@ -70,11 +70,10 @@
 text {*
   All formal developments in Isabelle are part of a theory. A theory 
   needs to have a name and must import some pre-existing theory. The 
-  imported theory will normally be the theory Nominal2 (which  contains 
-  many useful concepts like set-theory, lists, nominal theory etc).
-  For the purpose of the tutorial we import the theory Lambda.thy which
-  contains already some useful definitions for (alpha-equated) lambda 
-  terms.
+  imported theory will normally be Nominal2 (which provides many useful 
+  concepts like set-theory, lists, nominal things etc). For the purpose 
+  of this tutorial we import the theory Lambda.thy, which contains 
+  already some useful definitions for (alpha-equated) lambda terms.
 *}
 
 
@@ -135,16 +134,22 @@
 term "atom (x::name)"  -- {* atom is an overloded function *}
 
 text {* 
-  Lam [x].Var is the syntax we made up for lambda abstractions. You can have
-  your own syntax, if you prefer (but \<lambda> is already taken up for Isabelle's
-  functions). We also came up with "name". If you prefer, you can call
-  it "ident" or have more than one type for (object language) variables.
+  Lam [x].Var is the syntax we made up for lambda abstractions. If you
+  prefer, you can have your own syntax (but \<lambda> is already taken up for 
+  Isabelle's functions). We also came up with the type "name" for variables. 
+  You can introduce your own types of object variables using the 
+  command atom_decl: 
+*}
 
+atom_decl ident
+atom_decl ty_var
+
+text {*
   Isabelle provides some useful colour feedback about its constants (black), 
   free variables (blue) and bound variables (green).
 *}
 
-term "True"    -- {* a constant that is defined in HOL...written in black *}
+term "True"    -- {* a constant defined somewhere...written in black *}
 term "true"    -- {* not recognised as a constant, therefore it is interpreted
                      as a free variable, written in blue *}
 term "\<forall>x. P x" -- {* x is bound (green), P is free (blue) *}
@@ -262,15 +267,16 @@
   Examples are
 *}
 
+
+
 lemma alpha_equ:
   shows "Lam [x].Var x = Lam [y].Var y"
   by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)
 
 lemma Lam_freshness:
-  assumes a: "x \<noteq> y"
-  and     b: "atom y \<sharp> Lam [x].t"
-  shows "atom y \<sharp> t"
-  using a b by (simp add: lam.fresh Abs_fresh_iff) 
+  assumes a: "atom y \<sharp> Lam [x].t"
+  shows "(y = x) \<or> (y \<noteq> x \<and> atom y \<sharp> t)"
+  using a by (auto simp add: lam.fresh Abs_fresh_iff) 
 
 lemma neutral_element:
   fixes x::"nat"
@@ -500,20 +506,20 @@
   assumes a: "t1 \<longrightarrow>b* t2" 
   shows "t1 \<longrightarrow>b** t2"
   using a
-by (induct) (auto intro: beta_star2.intros)
+  by (induct) (auto intro: beta_star2.intros)
 
 lemma 
   assumes a: "t1 \<longrightarrow>b* t2"
   and     b: "t2 \<longrightarrow>b* t3"
   shows "t1 \<longrightarrow>b* t3"
-using a b
-by (induct) (auto intro: beta_star1.intros)
+  using a b
+  by (induct) (auto intro: beta_star1.intros)
 
 lemma
   assumes a: "t1 \<longrightarrow>b** t2"
   shows "t1 \<longrightarrow>b* t2"
-using a
-by (induct) (auto intro: bs1_trans2 beta_star1.intros)
+  using a
+  by (induct) (auto intro: bs1_trans2 beta_star1.intros)
 
 inductive
   eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60) 
@@ -556,13 +562,10 @@
 term "CAppL"
 term "CAppL \<box> (Var x)"
 
-text {* 
+subsection {* MINI EXERCISE *}
 
-  1.) MINI EXERCISE
-  -----------------
-
+text {*
   Try and see what happens if you apply a Hole to a Hole? 
-
 *}
 
 type_synonym ctxs = "ctx list"
@@ -593,14 +596,13 @@
 proof(induct)
   case (ms1 e1 Es1)
   have c: "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
-  show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry
+  then show "<e1, Es1> \<mapsto>* <e3, Es3>" by simp
 next
   case (ms2 e1 Es1 e2 Es2 e2' Es2') 
   have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact
   have d1: "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact
   have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact
-  
-  show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry
+  show "<e1, Es1> \<mapsto>* <e3, Es3>" using d1 d2 ih by blast
 qed
 
 text {* 
@@ -658,7 +660,6 @@
   shows "val t'"
 using a by (induct) (auto)
 
-
 theorem 
   assumes a: "t \<Down> t'"
   shows "<t, []> \<mapsto>* <t', []>"
@@ -666,7 +667,7 @@
 proof (induct)
   case (e_Lam x t) 
   -- {* no assumptions *}
-  show "<Lam [x].t, []> \<mapsto>* <Lam [x].t, []>" sorry
+  show "<Lam [x].t, []> \<mapsto>* <Lam [x].t, []>" by auto
 next
   case (e_App t1 x t t2 v' v) 
   -- {* all assumptions in this case *}
@@ -697,230 +698,6 @@
   shows "<t, []> \<mapsto>* <t', []>"
 using a eval_implies_machines_ctx by simp
 
-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. Freshness 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 
-           *   (x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) and 
-           **  valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)) *}
-    have *: "(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 **: "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 stron 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 {* Function Definitions: Filling a Lambda-Term into a Context *}
@@ -1003,8 +780,7 @@
   shows "E \<odot> \<box> = E"
 by (induct E) (simp_all)
 
-lemma odot_assoc:
-  fixes E1 E2 E3::"ctx"
+lemma odot_assoc: (* fixme call compose *)
   shows "(E1 \<odot> E2) \<odot> E3 = E1 \<odot> (E2 \<odot> E3)"
 by (induct E1) (simp_all)
 
@@ -1114,7 +890,6 @@
    (auto simp add: lam.fresh fresh_at_base)
 
 lemma fresh_fact:
-  fixes z::"name"
   assumes a: "atom z \<sharp> s"
   and b: "z = y \<or> atom z \<sharp> t"
   shows "atom z \<sharp> t[y ::= s]"
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
diff -r 87b735f86060 -r ddc05a611005 Tutorial/Tutorial4.thy
--- a/Tutorial/Tutorial4.thy	Fri Jan 21 00:55:28 2011 +0100
+++ b/Tutorial/Tutorial4.thy	Fri Jan 21 21:58:51 2011 +0100
@@ -1,6 +1,5 @@
-
 theory Tutorial4
-imports Tutorial1
+imports Tutorial1 Tutorial2
 begin
 
 section {* The CBV Reduction Relation (Small-Step Semantics) *}
@@ -136,22 +135,28 @@
 lemma machines_implies_cbvs_ctx:
   assumes a: "<e, Es> \<mapsto>* <e', Es'>"
   shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
-using a 
-by (induct) (auto dest: machine_implies_cbvs_ctx)
+using a machine_implies_cbvs_ctx 
+by (induct) (blast)+
 
 text {* 
   So whenever we let the CL machine start in an initial
   state and it arrives at a final state, then there exists
-  a corresponding cbv-reduction sequence. *}
+  a corresponding cbv-reduction sequence. 
+*}
 
 corollary machines_implies_cbvs:
   assumes a: "<e, []> \<mapsto>* <e', []>"
   shows "e \<longrightarrow>cbv* e'"
-using a by (auto dest: machines_implies_cbvs_ctx)
+proof - 
+  have "[]\<down>\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* []\<down>\<lbrakk>e'\<rbrakk>" 
+     using a machines_implies_cbvs_ctx by blast
+  then show "e \<longrightarrow>cbv* e'" by simp  
+qed
 
 text {*
   We now want to relate the cbv-reduction to the evaluation
-  relation. For this we need two auxiliary lemmas. *}
+  relation. For this we need two auxiliary lemmas. 
+*}
 
 lemma eval_val:
   assumes a: "val t"
@@ -160,16 +165,15 @@
 
 lemma e_App_elim:
   assumes a: "App t1 t2 \<Down> v"
-  shows "\<exists>x t v'. t1 \<Down> Lam [x].t \<and> t2 \<Down> v' \<and> t[x::=v'] \<Down> v"
+  obtains x t v' where "t1 \<Down> Lam [x].t" "t2 \<Down> v'" "t[x::=v'] \<Down> v"
 using a by (cases) (auto simp add: lam.eq_iff lam.distinct) 
 
-text {******************************************************************
-  
-  10.) Exercise
-  -------------
+
+subsection {* EXERCISE *}
 
-  Complete the first case in the proof below. 
-
+text {*
+  Complete the first and second case in the 
+  proof below. 
 *}
 
 lemma cbv_eval:
@@ -180,8 +184,9 @@
   case (cbv1 v x t t3)
   have a1: "val v" by fact
   have a2: "t[x ::= v] \<Down> t3" by fact
-
-  show "App (Lam [x].t) v \<Down> t3" sorry
+  have a3: "Lam [x].t \<Down> Lam [x].t" by auto
+  have a4: "v \<Down> v" using a1 eval_val by auto
+  show "App (Lam [x].t) v \<Down> t3" using a3 a4 a2 by auto 
 next
   case (cbv2 t t' t2 t3)
   have ih: "\<And>t3. t' \<Down> t3 \<Longrightarrow> t \<Down> t3" by fact
@@ -189,10 +194,10 @@
   then obtain x t'' v' 
     where a1: "t' \<Down> Lam [x].t''" 
       and a2: "t2 \<Down> v'" 
-      and a3: "t''[x ::= v'] \<Down> t3" using e_App_elim by blast
+      and a3: "t''[x ::= v'] \<Down> t3" by (rule e_App_elim) 
   have "t \<Down>  Lam [x].t''" using ih a1 by auto 
   then show "App t t2 \<Down> t3" using a2 a3 by auto
-qed (auto dest!: e_App_elim)
+qed (auto elim!: e_App_elim)
 
 
 text {* 
@@ -206,7 +211,8 @@
 
 text {* 
   Finally, we can show that if from a term t we reach a value 
-  by a cbv-reduction sequence, then t evaluates to this value. *}
+  by a cbv-reduction sequence, then t evaluates to this value. 
+*}
 
 lemma cbvs_implies_eval:
   assumes a: "t \<longrightarrow>cbv* v" "val v"
@@ -216,15 +222,16 @@
 
 text {* 
   All facts tied together give us the desired property about
-  K machines. *}
+  machines. 
+*}
 
 theorem machines_implies_eval:
   assumes a: "<t1, []> \<mapsto>* <t2, []>" 
   and     b: "val t2" 
   shows "t1 \<Down> t2"
 proof -
-  have "t1 \<longrightarrow>cbv* t2" using a by (simp add: machines_implies_cbvs)
-  then show "t1 \<Down> t2" using b by (simp add: cbvs_implies_eval)
+  have "t1 \<longrightarrow>cbv* t2" using a machines_implies_cbvs by simp
+  then show "t1 \<Down> t2" using b cbvs_implies_eval by simp
 qed
 
 lemma valid_elim:
@@ -252,9 +259,9 @@
 by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)
 
 lemma type_substitution_aux:
-  assumes a: "(\<Delta> @ [(x, T')] @ \<Gamma>) \<turnstile> e : T"
+  assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T"
   and     b: "\<Gamma> \<turnstile> e' : T'"
-  shows "(\<Delta> @ \<Gamma>) \<turnstile> e[x ::= e'] : T" 
+  shows "\<Delta> @ \<Gamma> \<turnstile> e[x ::= e'] : T" 
 using a b 
 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
   case (t_Var y T x e' \<Delta>)
@@ -264,40 +271,42 @@
   from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
   { assume eq: "x = y"
     from a1 a2 have "T = T'" using eq by (auto intro: context_unique)
-    with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" using eq a4 by (auto intro: weakening)
+    with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using eq a4 by (auto intro: weakening)
   }
   moreover
   { assume ineq: "x \<noteq> y"
     from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp
-    then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" using ineq a4 by auto
+    then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using ineq a4 by auto
   }
   ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast
 qed (force simp add: fresh_append fresh_Cons)+
 
 corollary type_substitution:
-  assumes a: "(x,T') # \<Gamma> \<turnstile> e : T"
+  assumes a: "(x, T') # \<Gamma> \<turnstile> e : T"
   and     b: "\<Gamma> \<turnstile> e' : T'"
-  shows "\<Gamma> \<turnstile> e[x::=e'] : T"
+  shows "\<Gamma> \<turnstile> e[x ::= e'] : T"
 using a b type_substitution_aux[where \<Delta>="[]"]
-by (auto)
+by auto
 
 lemma t_App_elim:
   assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"
-  shows "\<exists>T'. \<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<and> \<Gamma> \<turnstile> t2 : T'"
+  obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" "\<Gamma> \<turnstile> t2 : T'"
 using a
 by (cases) (auto simp add: lam.eq_iff lam.distinct)
 
+text {* we have not yet generated strong elimination rules *}
 lemma t_Lam_elim:
   assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" 
   and     fc: "atom x \<sharp> \<Gamma>" 
-  shows "\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> (x, T1) # \<Gamma> \<turnstile> t : T2"
+  obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2"
 using ty fc
 apply(cases)
 apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)
 apply(auto simp add: Abs1_eq_iff)
-apply(rule_tac p="(x \<leftrightarrow> xa)" in permute_boolE)
+apply(rotate_tac 3)
+apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)
 apply(perm_simp)
-apply(simp add: flip_def swap_fresh_fresh ty_fresh)
+apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)
 done
 
 theorem cbv_type_preservation:
@@ -306,7 +315,7 @@
   shows "\<Gamma> \<turnstile> t' : T"
 using a b
 by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)
-   (auto dest!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)
+   (auto elim!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)
 
 corollary cbvs_type_preservation:
   assumes a: "t \<longrightarrow>cbv* t'"
@@ -316,15 +325,17 @@
 by (induct) (auto intro: cbv_type_preservation)
 
 text {* 
-  The Type-Preservation Property for the Machine and Evaluation Relation. *}
+  The type-preservation property for the machine and 
+  evaluation relation. 
+*}
 
 theorem machine_type_preservation:
   assumes a: "<t, []> \<mapsto>* <t', []>"
   and     b: "\<Gamma> \<turnstile> t : T" 
   shows "\<Gamma> \<turnstile> t' : T"
 proof -
-  from a have "t \<longrightarrow>cbv* t'" by (simp add: machines_implies_cbvs)
-  then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: cbvs_type_preservation)
+  have "t \<longrightarrow>cbv* t'" using a machines_implies_cbvs by simp
+  then show "\<Gamma> \<turnstile> t' : T" using b cbvs_type_preservation by simp
 qed
 
 theorem eval_type_preservation:
@@ -332,8 +343,8 @@
   and     b: "\<Gamma> \<turnstile> t : T" 
   shows "\<Gamma> \<turnstile> t' : T"
 proof -
-  from a have "<t, []> \<mapsto>* <t', []>" by (simp add: eval_implies_machines)
-  then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation)
+  have "<t, []> \<mapsto>* <t', []>" using a eval_implies_machines by simp
+  then show "\<Gamma> \<turnstile> t' : T" using b machine_type_preservation by simp
 qed
 
 text {* The Progress Property *}
@@ -341,7 +352,7 @@
 lemma canonical_tArr:
   assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"
   and     b: "val t"
-  shows "\<exists>x t'. t = Lam [x].t'"
+  obtains x t' where "t = Lam [x].t'"
 using b a by (induct) (auto) 
 
 theorem progress:
@@ -349,6 +360,11 @@
   shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"
 using a
 by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)
-   (auto intro: cbv.intros dest!: canonical_tArr)
+   (auto elim: canonical_tArr)
 
+text {*
+  Done!
+*}
 
+end
+