diff -r a6f3e1b08494 -r b6873d123f9b Tutorial/Tutorial1.thy
--- a/Tutorial/Tutorial1.thy	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,738 +0,0 @@
-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 Tutorial1
-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" sorry
-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)" sorry
-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'" sorry
-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
-  
-  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>" sorry
-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, []> \<mapsto>* <t', []>"
-using a 
-proof (induct)
-  case (e_Lam x t) 
-  -- {* no assumptions *}
-  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 *}
-  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 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: 
-*}
-
-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 ctx_compose:
-  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>" sorry
-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>" sorry
-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>" 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 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>" sorry
-next
-  case (Cons E Es1)
-  have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
-
-  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 
-  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  
-