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]"