# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295730456 21600
# Node ID 3485111c7d62251a5089e1823c6adfcef38f1289
# Parent  2abc8cb46a5c437d394440f773b37003db6368ee
cleaned up tutorial1...added solution file

diff -r 2abc8cb46a5c -r 3485111c7d62 Tutorial/Tutorial1.thy
--- a/Tutorial/Tutorial1.thy	Sat Jan 22 12:46:01 2011 -0600
+++ b/Tutorial/Tutorial1.thy	Sat Jan 22 15:07:36 2011 -0600
@@ -60,6 +60,7 @@
         \<bullet>    bullet    (permutation application)
 *}
 
+
 theory Tutorial1
 imports Lambda
 begin
@@ -460,13 +461,15 @@
 proof(induct)
   case (ms1 e1 Es1)
   have c: "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
-  then show "<e1, Es1> \<mapsto>* <e3, Es3>" by simp
+  
+  show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry
 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>" using d1 d2 ih by blast
+
+  show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry
 qed
 
 text {* 
@@ -584,41 +587,6 @@
 qed
 
 
-theorem 
-  assumes a: "t \<Down> t'"
-  shows "<t, Es> \<mapsto>* <t', Es>"
-using a 
-proof (induct arbitrary: Es)
-  case (e_Lam x t Es) 
-  -- {* no assumptions *}
-  show "<Lam [x].t, Es> \<mapsto>* <Lam [x].t, Es>" by auto
-next
-  case (e_App t1 x t t2 v' v Es) 
-  -- {* all assumptions in this case *}
-  have a1: "t1 \<Down> Lam [x].t" by fact
-  have ih1: "\<And>Es. <t1, Es> \<mapsto>* <Lam [x].t, Es>" by fact
-  have a2: "t2 \<Down> v'" by fact
-  have ih2: "\<And>Es. <t2, Es> \<mapsto>* <v', Es>" by fact
-  have a3: "t[x::=v'] \<Down> v" by fact
-  have ih3: "\<And>Es. <t[x::=v'], Es> \<mapsto>* <v, Es>" by fact
-  -- {* your reasoning *}
-  have "<App t1 t2, Es> \<mapsto>* <t1, CAppL \<box> t2 # Es>" by auto
-  moreover
-  have "<t1, CAppL \<box> t2 # Es> \<mapsto>* <Lam [x].t, CAppL \<box> t2 # Es>" using ih1 by auto 
-  moreover
-  have "<Lam [x].t, CAppL \<box> t2 # Es> \<mapsto>* <t2, CAppR (Lam [x].t) \<box> # Es>" by auto
-  moreover
-  have "<t2, CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <v', CAppR (Lam [x].t) \<box> # Es>" 
-  using ih2 by auto
-  moreover
-  have "val v'" using a2 eval_to_val by auto
-  then have "<v', CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <t[x::=v'], Es>" by auto
-  moreover
-  have "<t[x::=v'], Es> \<mapsto>* <v, Es>" using ih3 by auto
-  ultimately show "<App t1 t2, Es> \<mapsto>* <v, Es>" by blast
-qed
-
-
 text {* 
   Again the automatic tools in Isabelle can discharge automatically 
   of the routine work in these proofs. We can write: 
@@ -637,7 +605,6 @@
 using a eval_implies_machines_ctx by simp
 
 
-
 section {* Function Definitions: Filling a Lambda-Term into a Context *}
  
 text {*
@@ -666,7 +633,7 @@
   by simp
 
 fun 
- ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<odot> _" [99,98] 99)
+ ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" (infixr "\<odot>" 99)
 where
   "\<box> \<odot> E' = E'"
 | "(CAppL E t') \<odot> E' = CAppL (E \<odot> E') t'"
@@ -715,11 +682,19 @@
   show "((CAppR t' E1) \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
 qed
 
+
+subsection {* EXERCISE 6 *}
+
+text {*
+  Remove the sorries in the ctx_append proof below. You can make 
+  use of the following two properties.    
+*}
+
 lemma neut_hole:
   shows "E \<odot> \<box> = E"
 by (induct E) (simp_all)
 
-lemma odot_assoc: (* fixme call compose *)
+lemma compose_assoc:  
   shows "(E1 \<odot> E2) \<odot> E3 = E1 \<odot> (E2 \<odot> E3)"
 by (induct E1) (simp_all)
 
@@ -735,7 +710,6 @@
   show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" sorry
 qed
 
-
 text {* 
   The last proof involves several steps of equational reasoning.
   Isar provides some convenient means to express such equational 
@@ -743,7 +717,6 @@
   construction. 
 *}
 
-
 lemma 
   shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
 proof (induct Es1)
@@ -752,14 +725,14 @@
 next
   case (Cons E Es1)
   have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
-  have "((E # Es1) @ Es2)\<down> = (Es1 @ Es2)\<down> \<odot> E" by simp
+  have "((E # Es1) @ Es2)\<down> = (E # (Es1 @ Es2))\<down>" by simp
+  also have "\<dots> = (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> (Es1\<down> \<odot> E)" using compose_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
 
 
-
 end  
 
diff -r 2abc8cb46a5c -r 3485111c7d62 Tutorial/Tutorial1s.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Tutorial1s.thy	Sat Jan 22 15:07:36 2011 -0600
@@ -0,0 +1,752 @@
+
+header {* 
+
+  Nominal Isabelle Tutorial at POPL'11
+  ====================================
+
+  Nominal Isabelle is a definitional extension of Isabelle/HOL, which
+  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 jEdit. 
+  Unlike many other theorem prover interfaces (e.g. ProofGeneral) where you 
+  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 jEdit can be started by typing on the command line
+
+     isabelle jedit -l HOL-Nominal2
+     isabelle jedit -l HOL-Nominal2 A.thy B.thy ...
+
+
+  Symbols
+  ------- 
+
+  Symbols can considerably improve the readability of your statements and proofs. 
+  They can be input by just typing 'name-of-symbol' where 'name-of-symbol' is the 
+  usual latex name of that symbol. A little window will then appear in which 
+  you can select the symbol. With `Escape' you can ignore any suggestion.
+  
+  There are some handy short-cuts for frequently used symbols. 
+  For example 
+
+      short-cut  symbol
+
+          =>      \<Rightarrow>
+          ==>     \<Longrightarrow>
+          -->     \<longrightarrow>
+          !       \<forall>        
+          ?       \<exists>
+          /\      \<and>
+          \/      \<or>
+          ~       \<not>
+          ~=      \<noteq>
+          :       \<in>
+          ~:      \<notin>
+
+  For nominal the following two symbols have a special meaning
+
+        \<sharp>    sharp     (freshness)
+        \<bullet>    bullet    (permutation application)
+*}
+
+theory Tutorial1s
+imports Lambda
+begin
+
+section {* Theories *}
+
+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 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.
+*}
+
+
+
+section {* Types *}
+
+text {*
+  Isabelle is based on simple types including some polymorphism. It also 
+  includes overloading, which means that sometimes explicit type annotations 
+  need to be given.
+
+    - Base types include: nat, bool, string, lam (defined in the Lambda theory)
+
+    - Type formers include: 'a list, ('a \<times> 'b), 'c set   
+
+    - Type variables are written like in ML with an apostrophe: 'a, 'b, \<dots>
+
+  Types known to Isabelle can be queried using the command "typ".
+*}
+
+typ nat
+typ bool
+typ string           
+typ lam           -- {* alpha-equated lambda terms defined in Lambda.thy *}
+typ name          -- {* type of (object) variables defined in Lambda.thy *}
+typ "('a \<times> 'b)"   -- {* pair type *}
+typ "'c set"      -- {* set type *}
+typ "'a list"     -- {* list type *}
+typ "lam \<Rightarrow> nat"   -- {* type of functions from lambda terms to natural numbers *}
+
+
+text {* Some malformed types - note the "stop" signal on the left margin *}
+
+(*
+typ boolean     -- {* undeclared type *} 
+typ set         -- {* type argument missing *}
+*)
+
+
+section {* Terms *}
+
+text {*
+   Every term in Isabelle needs to be well-typed. However they can have 
+   polymorphic type. Whether a term is accepted can be queried using
+   the command "term". 
+*}
+
+term c                 -- {* a variable of polymorphic type *}
+term "1::nat"          -- {* the constant 1 in natural numbers *}
+term 1                 -- {* the constant 1 with polymorphic type *}
+term "{1, 2, 3::nat}"  -- {* the set containing natural numbers 1, 2 and 3 *}
+term "[1, 2, 3]"       -- {* the list containing the polymorphic numbers 1, 2 and 3 *}
+term "(True, ''c'')"   -- {* a pair consisting of the boolean true and the string "c" *}
+term "Suc 0"           -- {* successor of 0, in other words 1::nat *}
+term "Lam [x].Var x"   -- {* a lambda-term *}
+term "App t1 t2"       -- {* another lambda-term *}
+term "x::name"         -- {* an (object) variable of type name *}
+term "atom (x::name)"  -- {* atom is an overloded function *}
+
+text {* 
+  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 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) *}
+
+
+text {* Formulae in Isabelle/HOL are terms of type bool *}
+
+term "True"
+term "True \<and> False"
+term "True \<or> B"
+term "{1,2,3} = {3,2,1}"
+term "\<forall>x. P x"
+term "A \<longrightarrow> B"
+term "atom a \<sharp> t"   -- {* freshness in Nominal *}
+
+text {*
+  When working with Isabelle, one deals with an object logic (that is HOL) and 
+  Isabelle's rule framework (called Pure). Occasionally one has to pay attention 
+  to this fact. But for the moment we ignore this completely.
+*}
+
+term "A \<longrightarrow> B"  -- {* versus *}
+term "A \<Longrightarrow> B"
+
+term "\<forall>x. P x"  -- {* versus *}
+term "\<And>x. P x"
+
+
+section {* Inductive Definitions: Evaluation Relation *}
+
+text {*
+  In this section we want to define inductively the evaluation
+  relation and for cbv-reduction relation.
+
+  Inductive definitions in Isabelle start with the keyword "inductive" 
+  and a predicate name.  One can optionally provide a type for the predicate. 
+  Clauses of the inductive predicate are introduced by "where" and more than 
+  two clauses need to be separated by "|". One can also give a name to each 
+  clause and indicate that it should be added to the hints database ("[intro]"). 
+  A typical clause has some premises and a conclusion. This is written in 
+  Isabelle as:
+
+   "premise \<Longrightarrow> conclusion"
+   "premise1 \<Longrightarrow> premise2 \<Longrightarrow> \<dots> premisen \<Longrightarrow> conclusion"
+
+  There is an alternative way of writing the latter clause as
+
+   "\<lbrakk>premise1; premise2; \<dots> premisen\<rbrakk> \<Longrightarrow> conclusion"
+
+  If no premise is present, then one just writes
+
+   "conclusion"
+
+  Below we give two definitions for the transitive closure
+*}
+
+inductive
+  eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60) 
+where
+  e_Lam[intro]:  "Lam [x].t \<Down> Lam [x].t"
+| e_App[intro]:  "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v"
+
+text {* 
+  Values and cbv are also defined using inductive.  
+*}
+
+inductive
+  val :: "lam \<Rightarrow> bool" 
+where
+  v_Lam[intro]:   "val (Lam [x].t)"
+
+section {* Theorems *}
+
+text {*
+  A central concept in Isabelle is that of theorems. Isabelle's theorem
+  database can be queried using 
+*}
+
+thm e_App
+thm e_Lam
+thm conjI
+thm conjunct1
+
+text {* 
+  Notice that theorems usually contain schematic variables (e.g. ?P, ?Q, \<dots>). 
+  These schematic variables can be substituted with any term (of the right type 
+  of course). 
+
+  When defining the predicates beta_star, Isabelle provides us automatically 
+  with the following theorems that state how they can be introduced and what 
+  constitutes an induction over them. 
+*}
+
+thm eval.intros
+thm eval.induct
+
+
+section {* Lemmas / Theorems / Corollaries *}
+
+text {*
+  Whether to use lemma, theorem or corollary makes no semantic difference 
+  in Isabelle. 
+
+  A lemma starts with "lemma" and consists of a statement ("shows \<dots>") and 
+  optionally a lemma name, some type-information for variables ("fixes \<dots>") 
+  and some assumptions ("assumes \<dots>"). 
+
+  Lemmas also need to have a proof, but ignore this 'detail' for the moment.
+
+  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: "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"
+  shows "x + 0 = x"
+  by simp
+
+text {*
+  Note that in the last statement, the explicit type annotation is important 
+  in order for Isabelle to be able to figure out what 0 stands for (e.g. a 
+  natural number, a vector, etc) and which lemmas to apply.
+*}
+
+
+section {* Isar Proofs *}
+
+text {*
+  Isar is a language for writing formal proofs that can be understood by humans 
+  and by Isabelle. An Isar proof can be thought of as a sequence of 'stepping stones' 
+  that start with some assumptions and lead to the goal to be established. Every such 
+  stepping stone is introduced by "have" followed by the statement of the stepping 
+  stone. An exception is the goal to be proved, which need to be introduced with "show".
+
+      have "statement"  \<dots>
+      show "goal_to_be_proved" \<dots>
+
+  Since proofs usually do not proceed in a linear fashion, labels can be given 
+  to every stepping stone and they can be used later to explicitly refer to this 
+  corresponding stepping stone ("using").
+
+      have label: "statement1"  \<dots>
+      \<dots>
+      have "later_statement" using label \<dots>
+
+  Each stepping stone (or have-statement) needs to have a justification. The 
+  simplest justification is "sorry" which admits any stepping stone, even false 
+  ones (this is good during the development of proofs). 
+
+      have "outrageous_false_statement" sorry
+
+  Assumptions can be 'justified' using "by fact". 
+
+      have "assumption" by fact
+
+  Derived facts can be justified using 
+
+      have "statement" by simp    -- simplification 
+      have "statement" by auto    -- proof search and simplification 
+      have "statement" by blast   -- only proof search 
+
+  If facts or lemmas are needed in order to justify a have-statement, then
+  one can feed these facts into the proof by using "using label \<dots>" or 
+  "using theorem-name \<dots>". More than one label at a time is allowed. For
+  example
+
+      have "statement" using label1 label2 theorem_name by auto
+
+  Induction proofs in Isar are set up by indicating over which predicate(s) 
+  the induction proceeds ("using a b") followed by the command "proof (induct)". 
+  In this way, Isabelle uses defaults for which induction should be performed. 
+  These defaults can be overridden by giving more information, like the variable 
+  over which a structural induction should proceed, or a specific induction principle, 
+  such as well-founded inductions. 
+
+  After the induction is set up, the proof proceeds by cases. In Isar these 
+  cases can be given in any order. Most commonly they are started with "case" and the 
+  name of the case, and optionally some legible names for the variables used inside 
+  the case. 
+
+  In each "case", we need to establish a statement introduced by "show". Once 
+  this has been done, the next case can be started using "next". When all cases 
+  are completed, the proof can be finished using "qed".
+
+  This means a typical induction proof has the following pattern
+
+     proof (induct)
+       case \<dots>
+       \<dots>
+       show \<dots>
+     next
+       case \<dots>
+       \<dots>
+       show \<dots>
+     \<dots>
+     qed
+
+   Two very simple example proofs are as follows.
+*}
+
+subsection {* EXERCISE 1 *}
+
+lemma eval_val:
+  assumes a: "val t"
+  shows "t \<Down> t"
+using a
+proof (induct)
+  case (v_Lam x t)
+  show "Lam [x]. t \<Down> Lam [x]. t" by auto
+qed
+
+subsection {* EXERCISE 2 *}
+
+text {* Fill the gaps in the proof below. *}
+
+lemma eval_to_val:
+  assumes a: "t \<Down> t'"
+  shows "val t'"
+using a
+proof (induct)
+  case (e_Lam x t)
+  show "val (Lam [x].t)" by auto
+next
+  case (e_App t1 x t t2 v v')
+  -- {* all assumptions in this case *}
+  have "t1 \<Down> Lam [x].t" by fact
+  have ih1: "val (Lam [x]. t)" by fact
+  have "t2 \<Down> v" by fact
+  have ih2: "val v" by fact
+  have "t [x ::= v] \<Down> v'" by fact
+  have ih3: "val v'" by fact
+
+  show "val v'" using ih3 by auto
+qed
+
+
+section {* Datatypes: Evaluation Contexts*}
+
+text {*
+  Datatypes can be defined in Isabelle as follows: we have to provide the name 
+  of the datatype and a list its type-constructors. Each type-constructor needs 
+  to have the information about the types of its arguments, and optionally 
+  can also contain some information about pretty syntax. For example, we like
+  to write "\<box>" for holes.
+*}
+  
+datatype ctx = 
+    Hole ("\<box>")  
+  | CAppL "ctx" "lam"
+  | CAppR "lam" "ctx"
+
+text {* Now Isabelle knows about: *}
+
+typ ctx
+term "\<box>"
+term "CAppL"
+term "CAppL \<box> (Var x)"
+
+subsection {* MINI EXERCISE *}
+
+text {*
+  Try and see what happens if you apply a Hole to a Hole? 
+*}
+
+
+section {* Machines for Evaluation *}
+
+type_synonym ctxs = "ctx list"
+
+inductive
+  machine :: "lam \<Rightarrow> ctxs \<Rightarrow>lam \<Rightarrow> ctxs \<Rightarrow> bool" ("<_,_> \<mapsto> <_,_>" [60, 60, 60, 60] 60)
+where
+  m1: "<App t1 t2, Es> \<mapsto> <t1, (CAppL \<box> t2) # Es>"
+| m2: "val v \<Longrightarrow> <v, (CAppL \<box> t2) # Es> \<mapsto> <t2, (CAppR v \<box>) # Es>"
+| m3: "val v \<Longrightarrow> <v, (CAppR (Lam [x].t) \<box>) # Es> \<mapsto> <t[x ::= v], Es>"
+
+text {*
+  Since the machine defined above only performs a single reduction,
+  we need to define the transitive closure of this machine. *}
+
+inductive 
+  machines :: "lam \<Rightarrow> ctxs \<Rightarrow> lam \<Rightarrow> ctxs \<Rightarrow> bool" ("<_,_> \<mapsto>* <_,_>" [60, 60, 60, 60] 60)
+where
+  ms1: "<t,Es> \<mapsto>* <t,Es>"
+| ms2: "\<lbrakk><t1,Es1> \<mapsto> <t2,Es2>; <t2,Es2> \<mapsto>* <t3,Es3>\<rbrakk> \<Longrightarrow> <t1,Es1> \<mapsto>* <t3,Es3>"
+
+declare machine.intros[intro] machines.intros[intro]
+
+section {* EXERCISE 3 *}
+
+text {*
+  We need to show that the machines-relation is transitive.
+  Fill in the gaps below.   
+*}
+
+lemma ms3[intro]:
+  assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" 
+  and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
+  shows "<e1, Es1> \<mapsto>* <e3, Es3>"
+using a b
+proof(induct)
+  case (ms1 e1 Es1)
+  have c: "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
+  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
+  have d3: "<e2, Es2> \<mapsto>* <e3, Es3>" using ih d1 by auto
+  show "<e1, Es1> \<mapsto>* <e3, Es3>" using d2 d3 by auto
+qed
+
+text {* 
+  Just like gotos in the Basic programming language, labels often reduce 
+  the readability of proofs. Therefore one can use in Isar the notation
+  "then have" in order to feed a have-statement to the proof of 
+  the next have-statement. This is used in teh second case below.
+*}
+ 
+lemma 
+  assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" 
+  and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
+  shows "<e1, Es1> \<mapsto>* <e3, Es3>"
+using a b
+proof(induct)
+  case (ms1 e1 Es1)
+  show "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
+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 "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact
+  then have d3: "<e2, Es2> \<mapsto>* <e3, Es3>" using ih by simp
+  have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact
+  show "<e1, Es1> \<mapsto>* <e3, Es3>" using d2 d3 by auto
+qed
+
+text {* 
+  The label ih2 cannot be got rid of in this way, because it is used 
+  two lines below and we cannot rearange them. We can still avoid the
+  label by feeding a sequence of facts into a proof using the 
+  "moreover"-chaining mechanism:
+
+   have "statement_1" \<dots>
+   moreover
+   have "statement_2" \<dots>
+   \<dots>
+   moreover
+   have "statement_n" \<dots>
+   ultimately have "statement" \<dots>
+
+  In this chain, all "statement_i" can be used in the proof of the final 
+  "statement". With this we can simplify our proof further to:
+*}
+
+lemma 
+  assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" 
+  and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
+  shows "<e1, Es1> \<mapsto>* <e3, Es3>"
+using a b
+proof(induct)
+  case (ms1 e1 Es1)
+  show "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
+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 "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact
+  then have "<e2, Es2> \<mapsto>* <e3, Es3>" using ih by simp
+  moreover
+  have "<e1, Es1> \<mapsto> <e2, Es2>" by fact
+  ultimately show "<e1, Es1> \<mapsto>* <e3, Es3>" by auto
+qed
+
+
+text {* 
+  While automatic proof procedures in Isabelle are not able to prove statements
+  like "P = NP" assuming usual definitions for P and NP, they can automatically
+  discharge the lemmas we just proved. For this we only have to set up the induction
+  and auto will take care of the rest. This means we can write:
+*}
+
+lemma 
+  assumes a: "val t"
+  shows "t \<Down> t"
+using a by (induct) (auto)
+
+lemma 
+  assumes a: "t \<Down> t'"
+  shows "val t'"
+using a by (induct) (auto)
+
+lemma
+  assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" 
+  and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
+  shows "<e1, Es1> \<mapsto>* <e3, Es3>"
+using a b by (induct) (auto)
+
+
+section {* EXERCISE 4 *}
+
+text {*
+  The point of the machine is that it simulates the evaluation
+  relation. Therefore we like to prove the following:
+*}
+
+theorem 
+  assumes a: "t \<Down> t'"
+  shows "<t, Es> \<mapsto>* <t', Es>"
+using a 
+proof (induct arbitrary: Es)
+  case (e_Lam x t Es) 
+  -- {* no assumptions *}
+  show "<Lam [x].t, Es> \<mapsto>* <Lam [x].t, Es>" by auto
+next
+  case (e_App t1 x t t2 v' v Es) 
+  -- {* all assumptions in this case *}
+  have a1: "t1 \<Down> Lam [x].t" by fact
+  have ih1: "\<And>Es. <t1, Es> \<mapsto>* <Lam [x].t, Es>" by fact
+  have a2: "t2 \<Down> v'" by fact
+  have ih2: "\<And>Es. <t2, Es> \<mapsto>* <v', Es>" by fact
+  have a3: "t[x::=v'] \<Down> v" by fact
+  have ih3: "\<And>Es. <t[x::=v'], Es> \<mapsto>* <v, Es>" by fact
+  -- {* your reasoning *}
+  have "<App t1 t2, Es> \<mapsto>* <t1, CAppL \<box> t2 # Es>" by auto
+  moreover
+  have "<t1, CAppL \<box> t2 # Es> \<mapsto>* <Lam [x].t, CAppL \<box> t2 # Es>" using ih1 by auto 
+  moreover
+  have "<Lam [x].t, CAppL \<box> t2 # Es> \<mapsto>* <t2, CAppR (Lam [x].t) \<box> # Es>" by auto
+  moreover
+  have "<t2, CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <v', CAppR (Lam [x].t) \<box> # Es>" 
+  using ih2 by auto
+  moreover
+  have "val v'" using a2 eval_to_val by auto
+  then have "<v', CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <t[x::=v'], Es>" by auto
+  moreover
+  have "<t[x::=v'], Es> \<mapsto>* <v, Es>" using ih3 by auto
+  ultimately show "<App t1 t2, Es> \<mapsto>* <v, Es>" by blast
+qed
+
+
+text {* 
+  Again the automatic tools in Isabelle can discharge automatically 
+  of the routine work in these proofs. We can write: 
+*}
+
+theorem eval_implies_machines_ctx:
+  assumes a: "t \<Down> t'"
+  shows "<t, Es> \<mapsto>* <t', Es>"
+using a
+by (induct arbitrary: Es)
+   (metis eval_to_val machine.intros ms1 ms2 ms3 v_Lam)+
+
+corollary eval_implies_machines:
+  assumes a: "t \<Down> t'"
+  shows "<t, []> \<mapsto>* <t', []>"
+using a eval_implies_machines_ctx by simp
+
+
+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
+  filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100, 100] 100)
+where
+  "\<box>\<lbrakk>t\<rbrakk> = t"
+| "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
+| "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
+
+
+text {* 
+  After this definition Isabelle will be able to simplify
+  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" (infixr "\<odot>" 99)
+where
+  "\<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>) \<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
+  of the arguments; the one next to it the precedence of the whole term.
+  
+  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).
+*}
+
+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.
+*}
+
+subsection {* EXERCISE 5 *}
+
+text {* Complete the proof and remove the sorries. *}
+
+lemma
+  shows "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
+proof (induct E1)
+  case Hole
+  show "(\<box> \<odot> E2)\<lbrakk>t\<rbrakk> = \<box>\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by simp
+next
+  case (CAppL E1 t')
+  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>" using ih by simp
+next
+  case (CAppR t' E1)
+  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>" using ih by simp
+qed
+
+subsection {* EXERCISE 6 *}
+
+text {*
+  Remove the sorries in the ctx_append proof below. You can make 
+  use of the following two properties.    
+*}
+
+lemma neut_hole:
+  shows "E \<odot> \<box> = E"
+by (induct E) (simp_all)
+
+lemma compose_assoc:  
+  shows "(E1 \<odot> E2) \<odot> E3 = E1 \<odot> (E2 \<odot> E3)"
+by (induct E1) (simp_all)
+
+lemma
+  shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
+proof (induct Es1)
+  case Nil
+  show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" using neut_hole by simp
+next
+  case (Cons E Es1)
+  have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
+  have eq1: "((E # Es1) @ Es2)\<down> = (E # (Es1 @ Es2))\<down>" by simp
+  have eq2: "(E # (Es1 @ Es2))\<down> = (Es1 @ Es2)\<down> \<odot> E" by simp
+  have eq3: "(Es1 @ Es2)\<down> \<odot> E = (Es2\<down> \<odot> Es1\<down>) \<odot> E" using ih by simp
+  have eq4: "(Es2\<down> \<odot> Es1\<down>) \<odot> E = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using compose_assoc by simp
+  have eq5: "Es2\<down> \<odot> (Es1\<down> \<odot> E) = Es2\<down> \<odot> (E # Es1)\<down>" by simp
+  show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" using eq1 eq2 eq3 eq4 eq5 by (simp only:)
+qed
+
+text {* 
+  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. 
+*}
+
+lemma 
+  shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
+proof (induct Es1)
+  case Nil
+  show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" using neut_hole by simp
+next
+  case (Cons E Es1)
+  have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
+  have "((E # Es1) @ Es2)\<down> = (E # (Es1 @ Es2))\<down>" by simp
+  also have "\<dots> = (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 compose_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
+
+
+end  
+