
diff -r d0fb94035969 -r 87b735f86060 Tutorial/Tutorial1.thy
--- a/Tutorial/Tutorial1.thy	Thu Jan 20 23:19:30 2011 +0100
+++ b/Tutorial/Tutorial1.thy	Fri Jan 21 00:55:28 2011 +0100
@@ -61,7 +61,6 @@
           \<bullet>       bullet    (permutations)
 *}
 
-
 theory Tutorial1
 imports Lambda
 begin
@@ -665,25 +664,26 @@
   shows "<t, []> \<mapsto>* <t', []>"
 using a 
 proof (induct)
-  case (e_Lam x t)
-  (* no assumptions *)
+  case (e_Lam x t) 
+  -- {* no assumptions *}
   show "<Lam [x].t, []> \<mapsto>* <Lam [x].t, []>" sorry
 next
-  case (e_App t1 x t t2 v' v)
-  (* all assumptions in this case *)
+  case (e_App t1 x t t2 v' v) 
+  -- {* all assumptions in this case *}
   have a1: "t1 \<Down> Lam [x].t" by fact
   have ih1: "<t1, []> \<mapsto>* <Lam [x].t, []>" by fact
   have a2: "t2 \<Down> v'" by fact
   have ih2: "<t2, []> \<mapsto>* <v', []>" by fact
   have a3: "t[x::=v'] \<Down> v" by fact
   have ih3: "<t[x::=v'], []> \<mapsto>* <v, []>" by fact
-  (* your details *)
+  -- {* your reasoning *}
   show "<App t1 t2, []> \<mapsto>* <v, []>" sorry
 qed
 
 text {* 
   Again the automatic tools in Isabelle can discharge automatically 
-  of the routine work in these proofs. We can write: *}
+  of the routine work in these proofs. We can write: 
+*}
 
 theorem eval_implies_machines_ctx:
   assumes a: "t \<Down> t'"
@@ -697,6 +697,7 @@
   shows "<t, []> \<mapsto>* <t', []>"
 using a eval_implies_machines_ctx by simp
 
+section {* Types *}
 
 nominal_datatype ty =
   tVar "string"
@@ -706,9 +707,7 @@
 text {* 
   Having defined them as nominal datatypes gives us additional
   definitions and theorems that come with types (see below).
-  *}
-
-text {* 
+ 
   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.
@@ -717,12 +716,14 @@
 
 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
@@ -732,9 +733,9 @@
 
 
 text {*
-  The predicate 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:
+  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
@@ -747,7 +748,9 @@
   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 *}
+text {* 
+  We can also prove that every variable is fresh for a type. 
+*}
 
 lemma ty_fresh:
   fixes x::"name"
@@ -757,10 +760,10 @@
    (simp_all add: ty.fresh pure_fresh)
 
 text {* 
-  In order to state the weakening lemma in a convenient form, we overload
-  the subset-notation and define the abbreviation below. Abbreviations behave
-  like definitions, except that they are always automatically folded and
-  unfolded.
+  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
@@ -768,13 +771,11 @@
 where
   "\<Gamma>1 \<sqsubseteq> \<Gamma>2 \<equiv> \<forall>x. x \<in> set \<Gamma>1 \<longrightarrow> x \<in> set \<Gamma>2"
 
-text {***************************************************************** 
+
+subsection {* EXERCISE 4 *}
 
-  4.) Exercise
-  ------------
-
+text {*
   Fill in the details and give a proof of the weakening lemma. 
-
 *}
 
 lemma 
@@ -799,74 +800,73 @@
   have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact
 
   show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry
-qed (auto)
+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 
-  smoothly through. Painful variable renamings seem to be necessary. 
-  But the proof using renamings is horribly complicated. It is really 
-  interesting whether people who claim this proof is  trivial, routine 
-  or obvious had this proof in mind. 
-
-  BTW: The following two commands help already with showing that validity 
-  and typing are invariant under variable (permutative) renamings. 
+  through smoothly. Painful variable renamings seem to be necessary. 
+  But the proof using renamings is horribly complicated (see below). 
 *}
 
 equivariance valid
 equivariance typing
 
-lemma not_to_be_tried_at_home_weakening: 
+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)
-  case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
+  -- {* 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)
-  have "Lam [c].((c \<leftrightarrow> x) \<bullet> t) = Lam [x].t" using fc1 (* we then alpha-rename the lambda-abstraction *)
+  -- {* 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
-  have "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" (* we can then alpha-rename our original goal *)
+  -- {* we can then alpha rename the goal *}
+  have "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" 
   proof - 
-    (* we 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)" 
+    -- {* 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)
+        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))" 
+    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)	
+        by (auto simp add: fresh_permute_left atom_eqvt valid.eqvt)	
     qed
-    (* these two facts give us by induction hypothesis the following *)
+    -- {* 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 *)
+    -- {* 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 *)
+qed (auto) -- {* var and app cases, luckily, are automatic *}
 
 
 text {* 
-  The remedy to the complicated proof of the weakening proof
-  shown above is to use a stronger induction principle that
-  has the usual variable convention already build in. The
+  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
@@ -875,21 +875,21 @@
   by (simp_all add: fresh_Pair lam.fresh ty_fresh)
 
 text {* Compare the two induction principles *}
+
 thm typing.induct
-thm typing.strong_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)
+      proof (induct arbitrary: \<Gamma>2)
 
   with 
   
-  proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)
+      proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)
 
   Try now the proof.
-
 *}
   
 
@@ -900,7 +900,7 @@
   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 *)
+  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 
@@ -909,27 +909,28 @@
   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 *)
+  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
-
-  show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry
-qed (auto) (* app case *)
+  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 {***************************************************************** 
-
-  Function Definitions: Filling a Lambda-Term into a Context
-  ----------------------------------------------------------
-
+section {* Function Definitions: Filling a Lambda-Term into a Context *}
+ 
+text {*
   Many functions over datatypes can be defined by recursion on the
   structure. For this purpose, Isabelle provides "fun". To use it one needs 
   to give a name for the function, its type, optionally some pretty-syntax 
   and then some equations defining the function. Like in "inductive",
   "fun" expects that more than one such equation is separated by "|".
-
 *}
 
 fun
@@ -941,90 +942,82 @@
 
 text {* 
   After this definition Isabelle will be able to simplify
-  statements like: *}
+  statements like: 
+*}
 
 lemma 
   shows "(CAppL \<box> (Var x))\<lbrakk>Var y\<rbrakk> = App (Var y) (Var x)"
   by simp
 
-
 fun 
- ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<cdot> _" [101,100] 100)
+ ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<odot> _" [99,98] 99)
 where
-  "\<box> \<cdot> E' = E'"
-| "(CAppL E t') \<cdot> E' = CAppL (E \<cdot> E') t'"
-| "(CAppR t' E) \<cdot> E' = CAppR t' (E \<cdot> E')"
+  "\<box> \<odot> E' = E'"
+| "(CAppL E t') \<odot> E' = CAppL (E \<odot> E') t'"
+| "(CAppR t' E) \<odot> E' = CAppR t' (E \<odot> E')"
 
 fun
   ctx_composes :: "ctxs \<Rightarrow> ctx" ("_\<down>" [110] 110)
 where
     "[]\<down> = \<box>"
-  | "(E # Es)\<down> = (Es\<down>) \<cdot> E"
+  | "(E # Es)\<down> = (Es\<down>) \<odot> E"
 
 text {*  
   Notice that we not just have given a pretty syntax for the functions, but
-  also some precedences..The numbers inside the [\<dots>] stand for the precedences
+  also some precedences. The numbers inside the [\<dots>] stand for the precedences
   of the arguments; the one next to it the precedence of the whole term.
   
-  This means we have to write (Es1 \<cdot> Es2) \<cdot> Es3 otherwise Es1 \<cdot> Es2 \<cdot> Es3 is
-  interpreted as Es1 \<cdot> (Es2 \<cdot> Es3).
+  This means we have to write (Es1 \<odot> Es2) \<odot> Es3 otherwise Es1 \<odot> Es2 \<odot> Es3 is
+  interpreted as Es1 \<odot> (Es2 \<odot> Es3).
 *}
 
-text {******************************************************************
-  
-  Structural Inductions over Contexts
-  ------------------------------------
-
+section {* Structural Inductions over Contexts *}
+ 
+text {*
   So far we have had a look at an induction over an inductive predicate. 
   Another important induction principle is structural inductions for 
   datatypes. To illustrate structural inductions we prove some facts
   about context composition, some of which we will need later on.
-
 *}
 
-text {******************************************************************
+subsection {* EXERCISE 5 *}
 
-  5.) EXERCISE
-  ------------
-
-  Complete the proof and remove the sorries.
-
-*}
+text {* Complete the proof and remove the sorries. *}
 
 lemma ctx_compose:
-  shows "(E1 \<cdot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
+  shows "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
 proof (induct E1)
   case Hole
-  show "\<box> \<cdot> E2\<lbrakk>t\<rbrakk> = \<box>\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
+  show "(\<box> \<odot> E2)\<lbrakk>t\<rbrakk> = \<box>\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
 next
   case (CAppL E1 t')
-  have ih: "(E1 \<cdot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact
-  show "((CAppL E1 t') \<cdot> E2)\<lbrakk>t\<rbrakk> = (CAppL E1 t')\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
+  have ih: "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact
+  show "((CAppL E1 t') \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppL E1 t')\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
 next
   case (CAppR t' E1)
-  have ih: "(E1 \<cdot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact
-  show "((CAppR t' E1) \<cdot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
+  have ih: "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact
+  show "((CAppR t' E1) \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
 qed
 
 lemma neut_hole:
-  shows "E \<cdot> \<box> = E"
+  shows "E \<odot> \<box> = E"
 by (induct E) (simp_all)
 
-lemma circ_assoc:
+lemma odot_assoc:
   fixes E1 E2 E3::"ctx"
-  shows "(E1 \<cdot> E2) \<cdot> E3 = E1 \<cdot> (E2 \<cdot> E3)"
+  shows "(E1 \<odot> E2) \<odot> E3 = E1 \<odot> (E2 \<odot> E3)"
 by (induct E1) (simp_all)
 
 lemma
-  shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<cdot> (Es1\<down>)"
+  shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
 proof (induct Es1)
   case Nil
-  show "([] @ Es2)\<down> = Es2\<down> \<cdot> []\<down>" sorry
+  show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" sorry
 next
   case (Cons E Es1)
-  have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<cdot> Es1\<down>" by fact
+  have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
 
-  show "((E # Es1) @ Es2)\<down> = Es2\<down> \<cdot> (E # Es1)\<down>" sorry
+  show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" sorry
 qed
 
 
@@ -1032,21 +1025,23 @@
   The last proof involves several steps of equational reasoning.
   Isar provides some convenient means to express such equational 
   reasoning in a much cleaner fashion using the "also have" 
-  construction. *}
+  construction. 
+*}
+
 
 lemma 
-  shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<cdot> (Es1\<down>)"
+  shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
 proof (induct Es1)
   case Nil
-  show "([] @ Es2)\<down> = Es2\<down> \<cdot> []\<down>" using neut_hole by simp
+  show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" using neut_hole by simp
 next
   case (Cons E Es1)
-  have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<cdot> Es1\<down>" by fact
-  have "((E # Es1) @ Es2)\<down> = (Es1 @ Es2)\<down> \<cdot> E" by simp
-  also have "\<dots> = (Es2\<down> \<cdot> Es1\<down>) \<cdot> E" using ih by simp
-  also have "\<dots> = Es2\<down> \<cdot> (Es1\<down> \<cdot> E)" using circ_assoc by simp
-  also have "\<dots> = Es2\<down> \<cdot> (E # Es1)\<down>" by simp
-  finally show "((E # Es1) @ Es2)\<down> = Es2\<down> \<cdot> (E # Es1)\<down>" by simp
+  have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
+  have "((E # Es1) @ Es2)\<down> = (Es1 @ Es2)\<down> \<odot> E" by simp
+  also have "\<dots> = (Es2\<down> \<odot> Es1\<down>) \<odot> E" using ih by simp
+  also have "\<dots> = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using odot_assoc by simp
+  also have "\<dots> = Es2\<down> \<odot> (E # Es1)\<down>" by simp
+  finally show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" by simp
 qed
 
 text {******************************************************************
@@ -1077,19 +1072,19 @@
    \<lbrakk>A; B\<rbrakk> \<Longrightarrow> "C" 
 
   Now if we want to prove a property "smth" using the case-distinctions
-  P\<^isub>1, P\<^isub>2 and P\<^isub>3 then we can use the following reasoning:
+  P1, P2 and P3 then we can use the following reasoning:
 
-    { assume "P\<^isub>1"
+    { assume "P1"
       \<dots>
       have "smth"
     }
     moreover
-    { assume "P\<^isub>2"
+    { assume "P2"
       \<dots>
       have "smth"
     }
     moreover
-    { assume "P\<^isub>3"
+    { assume "P3"
       \<dots>
       have "smth"
     }
@@ -1097,29 +1092,26 @@
 
   The blocks establish the implications
 
-    P\<^isub>1 \<Longrightarrow> smth
-    P\<^isub>2 \<Longrightarrow> smth
-    P\<^isub>3 \<Longrightarrow> smth
+    P1 \<Longrightarrow> smth
+    P2 \<Longrightarrow> smth
+    P3 \<Longrightarrow> smth
 
-  If we know that P\<^isub>1, P\<^isub>2 and P\<^isub>3 cover all the cases, that is P\<^isub>1 \<or> P\<^isub>2 \<or> P\<^isub>3 is
+  If we know that P1, P2 and P3 cover all the cases, that is P1 \<or> P2 \<or> P3 is
   true, then we have 'ultimately' established the property "smth" 
   
 *}
 
-text {******************************************************************
-  
-  7.) Exercise
-  ------------
+section {* EXERCISE 7 *}
 
+text {*
   Fill in the cases 1.2 and 1.3 and the equational reasoning 
   in the lambda-case.
 *}
 
 lemma forget:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
-apply(nominal_induct t avoiding: x s rule: lam.strong_induct)
-apply(auto simp add: lam.fresh fresh_at_base)
-done
+by (nominal_induct t avoiding: x s rule: lam.strong_induct)
+   (auto simp add: lam.fresh fresh_at_base)
 
 lemma fresh_fact:
   fixes z::"name"
@@ -1127,12 +1119,9 @@
   and b: "z = y \<or> atom z \<sharp> t"
   shows "atom z \<sharp> t[y ::= s]"
 using a b
-apply (nominal_induct t avoiding: z y s rule: lam.strong_induct)
-apply (auto simp add: lam.fresh fresh_at_base)
-done
+by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
+   (auto simp add: lam.fresh fresh_at_base)
 
-thm forget
-thm fresh_fact
 
 lemma 
   assumes a: "x \<noteq> y"
@@ -1145,20 +1134,20 @@
   have a2: "atom x \<sharp> L" by fact
   show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS")
   proof -
-    { (*Case 1.1*)
-      assume c1: "z=x"
+    { -- {* Case 1.1 *}
+      assume c1: "z = x"
       have "(1)": "?LHS = N[y::=L]" using c1 by simp
       have "(2)": "?RHS = N[y::=L]" using c1 a1 by simp
       have "?LHS = ?RHS" using "(1)" "(2)" by simp
     }
     moreover 
-    { (*Case 1.2*)
+    { -- {* Case 1.2 *}
       assume c2: "z = y" "z \<noteq> x" 
       
       have "?LHS = ?RHS" sorry
     }
     moreover 
-    { (*Case 1.3*)
+    { -- {* Case 1.3 *}
       assume c3: "z \<noteq> x" "z \<noteq> y"
       
       have "?LHS = ?RHS" sorry
@@ -1166,7 +1155,7 @@
     ultimately show "?LHS = ?RHS" by blast
   qed
 next
-  case (Lam z M1) (* case 2: lambdas *)
+  case (Lam z M1) -- {* case 2: lambdas *}
   have ih: "\<lbrakk>x \<noteq> y; atom x \<sharp> L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
   have a1: "x \<noteq> y" by fact
   have a2: "atom x \<sharp> L" by fact
@@ -1180,7 +1169,7 @@
     finally show "?LHS = ?RHS" by simp
   qed
 next
-  case (App M1 M2) (* case 3: applications *)
+  case (App M1 M2) -- {* case 3: applications *}
   then show "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp
 qed
 




