# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295561970 -3600
# Node ID d0fb940359693ff913e1906766c74b28e14a59c6
# Parent  52e1e98edb34a40346e5fbd1a3fff39d9fa54a17
first split of tutorrial theory

diff -r 52e1e98edb34 -r d0fb94035969 Tutorial/Tutorial1.thy
--- a/Tutorial/Tutorial1.thy	Wed Jan 19 23:58:12 2011 +0100
+++ b/Tutorial/Tutorial1.thy	Thu Jan 20 23:19:30 2011 +0100
@@ -1,21 +1,18 @@
 
 header {* 
 
-  Nominal Isabelle Tutorial
-  =========================
-
-  There will be hands-on exercises throughout the tutorial. Therefore
-  it would be good if you have your own laptop.
+  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 merely
   adds new definitions and an infrastructure for 'nominal resoning'.
 
 
-  The Interface
-  -------------
+  The jEdit Interface
+  -------------------
 
-  The Isabelle theorem prover comes with an interface for jEdit interface. 
+  The Isabelle theorem prover comes with an interface for the 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
@@ -64,6 +61,7 @@
           \<bullet>       bullet    (permutations)
 *}
 
+
 theory Tutorial1
 imports Lambda
 begin
@@ -72,12 +70,12 @@
 
 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 (as indicated 
-  above). The imported theory will normally be the theory Nominal2 (which 
-  contains many useful concepts like set-theory, lists, nominal theory etc).
-
+  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.
+  contains already some useful definitions for (alpha-equated) lambda 
+  terms.
 *}
 
 
@@ -85,11 +83,11 @@
 section {* Types *}
 
 text {*
-  Isabelle is based on simple types including some polymorphism. It also includes 
-  some overloading, which means that sometimes explicit type annotations need to 
-  be given.
+  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
+    - Base types include: nat, bool, string, lam (defined in the Lambda theory)
 
     - Type formers include: 'a list, ('a \<times> 'b), 'c set   
 
@@ -101,15 +99,15 @@
 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 "nat \<Rightarrow> bool"   -- {* type of functions from natural numbers to booleans *}
+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: *}
+text {* Some malformed types - note the "stop" signal on the left margin *}
 
 (*
 typ boolean     -- {* undeclared type *} 
@@ -139,10 +137,11 @@
 
 text {* 
   Lam [x].Var is the syntax we made up for lambda abstractions. You can have
-  your own syntax. We also came up with "name". If you prefer, you can call
-  it identifiers or have more than one type for (object languag) variables.
+  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.
 
-  Isabelle provides some useful colour feedback about constants (black), 
+  Isabelle provides some useful colour feedback about its constants (black), 
   free variables (blue) and bound variables (green).
 *}
 
@@ -160,7 +159,7 @@
 term "{1,2,3} = {3,2,1}"
 term "\<forall>x. P x"
 term "A \<longrightarrow> B"
-term "atom a \<sharp> t"
+term "atom a \<sharp> t"   -- {* freshness in Nominal *}
 
 text {*
   When working with Isabelle, one deals with an object logic (that is HOL) and 
@@ -179,10 +178,12 @@
 section {* Inductive Definitions: Transitive Closures of Beta-Reduction *}
 
 text {*
-  The theory Lmabda alraedy contains a definition for beta-reduction, written
+  The theory Lmabda already contains a definition for beta-reduction, written
+*}
 
-     t \<longrightarrow>b t'
+term "t \<longrightarrow>b t'"
 
+text {*
   In this section we want to define inductively the transitive closure of
   beta-reduction.
 
@@ -1195,358 +1196,6 @@
 by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
    (auto simp add: fresh_fact forget)
 
-text {******************************************************************
-  
-  The CBV Reduction Relation (Small-Step Semantics) 
-  -------------------------------------------------
-
-  In order to establish the property that the CK Machine
-  calculates a nomrmalform which corresponds to the
-  evaluation relation, we introduce the call-by-value
-  small-step semantics.
-
-*}
-
-inductive
-  cbv :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>cbv _" [60, 60] 60) 
-where
-  cbv1: "\<lbrakk>val v; atom x \<sharp> v\<rbrakk> \<Longrightarrow> App (Lam [x].t) v \<longrightarrow>cbv t[x::=v]"
-| cbv2[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t t2 \<longrightarrow>cbv App t' t2"
-| cbv3[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t2 t \<longrightarrow>cbv App t2 t'"
-
-equivariance val
-equivariance cbv
-nominal_inductive cbv
-  avoids cbv1: "x"
-  unfolding fresh_star_def
-  by (simp_all add: lam.fresh Abs_fresh_iff fresh_Pair fresh_fact)
-
-text {*
-  In order to satisfy the vc-condition we have to formulate
-  this relation with the additional freshness constraint
-  x\<sharp>v. Though this makes the definition vc-ompatible, it
-  makes the definition less useful. We can with some pain
-  show that the more restricted rule is equivalent to the
-  usual rule. *}
-
-lemma subst_rename: 
-  assumes a: "atom y \<sharp> t"
-  shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet>t)[y ::= s]"
-using a 
-apply (nominal_induct t avoiding: x y s rule: lam.strong_induct)
-apply (auto simp add: lam.fresh fresh_at_base)
-done
-
-thm subst_rename
-
-lemma better_cbv1[intro]: 
-  assumes a: "val v" 
-  shows "App (Lam [x].t) v \<longrightarrow>cbv t[x::=v]"
-proof -
-  obtain y::"name" where fs: "atom y \<sharp> (x, t, v)" by (rule obtain_fresh)
-  have "App (Lam [x].t) v = App (Lam [y].((y \<leftrightarrow> x) \<bullet> t)) v" using fs
-    by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)
-  also have "\<dots> \<longrightarrow>cbv  ((y \<leftrightarrow> x) \<bullet> t)[y ::= v]" using fs a by (auto intro: cbv1)
-  also have "\<dots> = t[x ::= v]" using fs by (simp add: subst_rename[symmetric])
-  finally show "App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]" by simp
-qed
-
-text {*
-  The transitive closure of the cbv-reduction relation: *}
-
-inductive 
-  "cbvs" :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>cbv* _" [60, 60] 60)
-where
-  cbvs1[intro]: "e \<longrightarrow>cbv* e"
-| cbvs2[intro]: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"
-
-lemma cbvs3[intro]:
-  assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"
-  shows "e1 \<longrightarrow>cbv* e3"
-using a by (induct) (auto) 
-
-text {******************************************************************
-  
-  8.) Exercise
-  ------------
-
-  If more simple exercises are needed, then complete the following proof. 
-
-*}
-
-lemma cbv_in_ctx:
-  assumes a: "t \<longrightarrow>cbv t'"
-  shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>"
-using a
-proof (induct E)
-  case Hole
-  have "t \<longrightarrow>cbv t'" by fact
-  then show "\<box>\<lbrakk>t\<rbrakk> \<longrightarrow>cbv \<box>\<lbrakk>t'\<rbrakk>" sorry
-next
-  case (CAppL E s)
-  have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact
-  have a: "t \<longrightarrow>cbv t'" by fact
-  show "(CAppL E s)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppL E s)\<lbrakk>t'\<rbrakk>" sorry
-next
-  case (CAppR s E)
-  have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact
-  have a: "t \<longrightarrow>cbv t'" by fact
-  show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" sorry
-qed
-
-  
-text {******************************************************************
-  
-  9.) Exercise
-  ------------
-
-  The point of the cbv-reduction was that we can easily relatively 
-  establish the follwoing property:
-
-*}
-
-lemma machine_implies_cbvs_ctx:
-  assumes a: "<e, Es> \<mapsto> <e', Es'>"
-  shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
-using a 
-proof (induct)
-  case (m1 t1 t2 Es)
-
-  show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>"  sorry
-next
-  case (m2 v t2 Es)
-  have "val v" by fact
-
-  show "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" sorry
-next
-  case (m3 v x t Es)
-  have "val v" by fact
- 
-  show "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" sorry
-qed
-
-text {* 
-  It is not difficult to extend the lemma above to
-  arbitrary reductions sequences of the CK machine. *}
-
-lemma machines_implies_cbvs_ctx:
-  assumes a: "<e, Es> \<mapsto>* <e', Es'>"
-  shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
-using a 
-by (induct) (auto dest: machine_implies_cbvs_ctx)
-
-text {* 
-  So whenever we let the CL machine start in an initial
-  state and it arrives at a final state, then there exists
-  a corresponding cbv-reduction sequence. *}
-
-corollary machines_implies_cbvs:
-  assumes a: "<e, []> \<mapsto>* <e', []>"
-  shows "e \<longrightarrow>cbv* e'"
-using a by (auto dest: machines_implies_cbvs_ctx)
-
-text {*
-  We now want to relate the cbv-reduction to the evaluation
-  relation. For this we need two auxiliary lemmas. *}
-
-lemma eval_val:
-  assumes a: "val t"
-  shows "t \<Down> t"
-using a by (induct) (auto)
-
-lemma e_App_elim:
-  assumes a: "App t1 t2 \<Down> v"
-  shows "\<exists>x t v'. t1 \<Down> Lam [x].t \<and> t2 \<Down> v' \<and> t[x::=v'] \<Down> v"
-using a by (cases) (auto simp add: lam.eq_iff lam.distinct) 
-
-text {******************************************************************
-  
-  10.) Exercise
-  -------------
-
-  Complete the first case in the proof below. 
-
-*}
-
-lemma cbv_eval:
-  assumes a: "t1 \<longrightarrow>cbv t2" "t2 \<Down> t3"
-  shows "t1 \<Down> t3"
-using a
-proof(induct arbitrary: t3)
-  case (cbv1 v x t t3)
-  have a1: "val v" by fact
-  have a2: "t[x ::= v] \<Down> t3" by fact
-
-  show "App (Lam [x].t) v \<Down> t3" sorry
-next
-  case (cbv2 t t' t2 t3)
-  have ih: "\<And>t3. t' \<Down> t3 \<Longrightarrow> t \<Down> t3" by fact
-  have "App t' t2 \<Down> t3" by fact
-  then obtain x t'' v' 
-    where a1: "t' \<Down> Lam [x].t''" 
-      and a2: "t2 \<Down> v'" 
-      and a3: "t''[x ::= v'] \<Down> t3" using e_App_elim by blast
-  have "t \<Down>  Lam [x].t''" using ih a1 by auto 
-  then show "App t t2 \<Down> t3" using a2 a3 by auto
-qed (auto dest!: e_App_elim)
-
-
-text {* 
-  Next we extend the lemma above to arbitray initial
-  sequences of cbv-reductions. *}
-
-lemma cbvs_eval:
-  assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3"
-  shows "t1 \<Down> t3"
-using a by (induct) (auto intro: cbv_eval)
-
-text {* 
-  Finally, we can show that if from a term t we reach a value 
-  by a cbv-reduction sequence, then t evaluates to this value. *}
-
-lemma cbvs_implies_eval:
-  assumes a: "t \<longrightarrow>cbv* v" "val v"
-  shows "t \<Down> v"
-using a
-by (induct) (auto intro: eval_val cbvs_eval)
-
-text {* 
-  All facts tied together give us the desired property about
-  K machines. *}
-
-theorem machines_implies_eval:
-  assumes a: "<t1, []> \<mapsto>* <t2, []>" 
-  and     b: "val t2" 
-  shows "t1 \<Down> t2"
-proof -
-  have "t1 \<longrightarrow>cbv* t2" using a by (simp add: machines_implies_cbvs)
-  then show "t1 \<Down> t2" using b by (simp add: cbvs_implies_eval)
-qed
-
-lemma valid_elim:
-  assumes a: "valid ((x, T) # \<Gamma>)"
-  shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>"
-using a by (cases) (auto)
-
-lemma valid_insert:
-  assumes a: "valid (\<Delta> @ [(x, T)] @ \<Gamma>)"
-  shows "valid (\<Delta> @ \<Gamma>)" 
-using a
-by (induct \<Delta>)
-   (auto simp add: fresh_append fresh_Cons dest!: valid_elim)
-
-lemma fresh_list: 
-  shows "atom y \<sharp> xs = (\<forall>x \<in> set xs. atom y \<sharp> x)"
-by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
-
-lemma context_unique:
-  assumes a1: "valid \<Gamma>"
-  and     a2: "(x, T) \<in> set \<Gamma>"
-  and     a3: "(x, U) \<in> set \<Gamma>"
-  shows "T = U" 
-using a1 a2 a3
-by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)
-
-lemma type_substitution_aux:
-  assumes a: "(\<Delta> @ [(x, T')] @ \<Gamma>) \<turnstile> e : T"
-  and     b: "\<Gamma> \<turnstile> e' : T'"
-  shows "(\<Delta> @ \<Gamma>) \<turnstile> e[x ::= e'] : T" 
-using a b 
-proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
-  case (t_Var y T x e' \<Delta>)
-  have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact
-  have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact 
-  have a3: "\<Gamma> \<turnstile> e' : T'" by fact
-  from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
-  { assume eq: "x = y"
-    from a1 a2 have "T = T'" using eq by (auto intro: context_unique)
-    with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" using eq a4 by (auto intro: weakening)
-  }
-  moreover
-  { assume ineq: "x \<noteq> y"
-    from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp
-    then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" using ineq a4 by auto
-  }
-  ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast
-qed (force simp add: fresh_append fresh_Cons)+
-
-corollary type_substitution:
-  assumes a: "(x,T') # \<Gamma> \<turnstile> e : T"
-  and     b: "\<Gamma> \<turnstile> e' : T'"
-  shows "\<Gamma> \<turnstile> e[x::=e'] : T"
-using a b type_substitution_aux[where \<Delta>="[]"]
-by (auto)
-
-lemma t_App_elim:
-  assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"
-  shows "\<exists>T'. \<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<and> \<Gamma> \<turnstile> t2 : T'"
-using a
-by (cases) (auto simp add: lam.eq_iff lam.distinct)
-
-lemma t_Lam_elim:
-  assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" 
-  and     fc: "atom x \<sharp> \<Gamma>" 
-  shows "\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> (x, T1) # \<Gamma> \<turnstile> t : T2"
-using ty fc
-apply(cases)
-apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)
-apply(auto simp add: Abs1_eq_iff)
-apply(rule_tac p="(x \<leftrightarrow> xa)" in permute_boolE)
-apply(perm_simp)
-apply(simp add: flip_def swap_fresh_fresh ty_fresh)
-done
-
-theorem cbv_type_preservation:
-  assumes a: "t \<longrightarrow>cbv t'"
-  and     b: "\<Gamma> \<turnstile> t : T" 
-  shows "\<Gamma> \<turnstile> t' : T"
-using a b
-by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)
-   (auto dest!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)
-
-corollary cbvs_type_preservation:
-  assumes a: "t \<longrightarrow>cbv* t'"
-  and     b: "\<Gamma> \<turnstile> t : T" 
-  shows "\<Gamma> \<turnstile> t' : T"
-using a b
-by (induct) (auto intro: cbv_type_preservation)
-
-text {* 
-  The Type-Preservation Property for the Machine and Evaluation Relation. *}
-
-theorem machine_type_preservation:
-  assumes a: "<t, []> \<mapsto>* <t', []>"
-  and     b: "\<Gamma> \<turnstile> t : T" 
-  shows "\<Gamma> \<turnstile> t' : T"
-proof -
-  from a have "t \<longrightarrow>cbv* t'" by (simp add: machines_implies_cbvs)
-  then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: cbvs_type_preservation)
-qed
-
-theorem eval_type_preservation:
-  assumes a: "t \<Down> t'"
-  and     b: "\<Gamma> \<turnstile> t : T" 
-  shows "\<Gamma> \<turnstile> t' : T"
-proof -
-  from a have "<t, []> \<mapsto>* <t', []>" by (simp add: eval_implies_machines)
-  then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation)
-qed
-
-text {* The Progress Property *}
-
-lemma canonical_tArr:
-  assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"
-  and     b: "val t"
-  shows "\<exists>x t'. t = Lam [x].t'"
-using b a by (induct) (auto) 
-
-theorem progress:
-  assumes a: "[] \<turnstile> t : T"
-  shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"
-using a
-by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)
-   (auto intro: cbv.intros dest!: canonical_tArr)
-
 
 
 end  
diff -r 52e1e98edb34 -r d0fb94035969 Tutorial/Tutorial4.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Tutorial4.thy	Thu Jan 20 23:19:30 2011 +0100
@@ -0,0 +1,354 @@
+
+theory Tutorial4
+imports Tutorial1
+begin
+
+section {* The CBV Reduction Relation (Small-Step Semantics) *}
+
+text {*
+  In order to help establishing the property that the CK Machine
+  calculates a nomrmalform that corresponds to the evaluation 
+  relation, we introduce the call-by-value small-step semantics.
+*}
+
+inductive
+  cbv :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>cbv _" [60, 60] 60) 
+where
+  cbv1: "\<lbrakk>val v; atom x \<sharp> v\<rbrakk> \<Longrightarrow> App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]"
+| cbv2[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t t2 \<longrightarrow>cbv App t' t2"
+| cbv3[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t2 t \<longrightarrow>cbv App t2 t'"
+
+equivariance val
+equivariance cbv
+nominal_inductive cbv
+  avoids cbv1: "x"
+  unfolding fresh_star_def
+  by (simp_all add: lam.fresh Abs_fresh_iff fresh_Pair fresh_fact)
+
+text {*
+  In order to satisfy the vc-condition we have to formulate
+  this relation with the additional freshness constraint
+  atom x \<sharp> v. Although this makes the definition vc-ompatible, it
+  makes the definition less useful. We can with a little bit of 
+  pain show that the more restricted rule is equivalent to the
+  usual rule. 
+*}
+
+lemma subst_rename: 
+  assumes a: "atom y \<sharp> t"
+  shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet> t)[y ::= s]"
+using a 
+by (nominal_induct t avoiding: x y s rule: lam.strong_induct)
+   (auto simp add: lam.fresh fresh_at_base)
+
+
+lemma better_cbv1 [intro]: 
+  assumes a: "val v" 
+  shows "App (Lam [x].t) v \<longrightarrow>cbv t[x::=v]"
+proof -
+  obtain y::"name" where fs: "atom y \<sharp> (x, t, v)" by (rule obtain_fresh)
+  have "App (Lam [x].t) v = App (Lam [y].((y \<leftrightarrow> x) \<bullet> t)) v" using fs
+    by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)
+  also have "\<dots> \<longrightarrow>cbv ((y \<leftrightarrow> x) \<bullet> t)[y ::= v]" using fs a cbv1 by auto
+  also have "\<dots> = t[x ::= v]" using fs subst_rename[symmetric] by simp
+  finally show "App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]" by simp
+qed
+
+text {*
+  The transitive closure of the cbv-reduction relation: 
+*}
+
+inductive 
+  "cbvs" :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>cbv* _" [60, 60] 60)
+where
+  cbvs1[intro]: "e \<longrightarrow>cbv* e"
+| cbvs2[intro]: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"
+
+lemma cbvs3 [intro]:
+  assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"
+  shows "e1 \<longrightarrow>cbv* e3"
+using a by (induct) (auto) 
+
+
+subsection {* EXERCISE 8 *}
+
+text {*  
+  If more simple exercises are needed, then complete the following proof. 
+*}
+
+lemma cbv_in_ctx:
+  assumes a: "t \<longrightarrow>cbv t'"
+  shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>"
+using a
+proof (induct E)
+  case Hole
+  have "t \<longrightarrow>cbv t'" by fact
+  then show "\<box>\<lbrakk>t\<rbrakk> \<longrightarrow>cbv \<box>\<lbrakk>t'\<rbrakk>" by simp
+next
+  case (CAppL E s)
+  have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact
+  moreover
+  have "t \<longrightarrow>cbv t'" by fact
+  ultimately 
+  have "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by simp
+  then show "(CAppL E s)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppL E s)\<lbrakk>t'\<rbrakk>" by auto
+next
+  case (CAppR s E)
+  have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact
+  moreover
+  have a: "t \<longrightarrow>cbv t'" by fact
+  ultimately 
+  have "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by simp
+  then show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" by auto
+qed
+
+section {* EXERCISE 9 *} 
+ 
+text {*
+  The point of the cbv-reduction was that we can easily relatively 
+  establish the follwoing property:
+*}
+
+lemma machine_implies_cbvs_ctx:
+  assumes a: "<e, Es> \<mapsto> <e', Es'>"
+  shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
+using a 
+proof (induct)
+  case (m1 t1 t2 Es)
+
+  show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>" sorry
+next
+  case (m2 v t2 Es)
+  have "val v" by fact
+
+  show "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" sorry
+next
+  case (m3 v x t Es)
+  have "val v" by fact
+ 
+  show "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" sorry
+qed
+
+text {* 
+  It is not difficult to extend the lemma above to
+  arbitrary reductions sequences of the CK machine. *}
+
+lemma machines_implies_cbvs_ctx:
+  assumes a: "<e, Es> \<mapsto>* <e', Es'>"
+  shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
+using a 
+by (induct) (auto dest: machine_implies_cbvs_ctx)
+
+text {* 
+  So whenever we let the CL machine start in an initial
+  state and it arrives at a final state, then there exists
+  a corresponding cbv-reduction sequence. *}
+
+corollary machines_implies_cbvs:
+  assumes a: "<e, []> \<mapsto>* <e', []>"
+  shows "e \<longrightarrow>cbv* e'"
+using a by (auto dest: machines_implies_cbvs_ctx)
+
+text {*
+  We now want to relate the cbv-reduction to the evaluation
+  relation. For this we need two auxiliary lemmas. *}
+
+lemma eval_val:
+  assumes a: "val t"
+  shows "t \<Down> t"
+using a by (induct) (auto)
+
+lemma e_App_elim:
+  assumes a: "App t1 t2 \<Down> v"
+  shows "\<exists>x t v'. t1 \<Down> Lam [x].t \<and> t2 \<Down> v' \<and> t[x::=v'] \<Down> v"
+using a by (cases) (auto simp add: lam.eq_iff lam.distinct) 
+
+text {******************************************************************
+  
+  10.) Exercise
+  -------------
+
+  Complete the first case in the proof below. 
+
+*}
+
+lemma cbv_eval:
+  assumes a: "t1 \<longrightarrow>cbv t2" "t2 \<Down> t3"
+  shows "t1 \<Down> t3"
+using a
+proof(induct arbitrary: t3)
+  case (cbv1 v x t t3)
+  have a1: "val v" by fact
+  have a2: "t[x ::= v] \<Down> t3" by fact
+
+  show "App (Lam [x].t) v \<Down> t3" sorry
+next
+  case (cbv2 t t' t2 t3)
+  have ih: "\<And>t3. t' \<Down> t3 \<Longrightarrow> t \<Down> t3" by fact
+  have "App t' t2 \<Down> t3" by fact
+  then obtain x t'' v' 
+    where a1: "t' \<Down> Lam [x].t''" 
+      and a2: "t2 \<Down> v'" 
+      and a3: "t''[x ::= v'] \<Down> t3" using e_App_elim by blast
+  have "t \<Down>  Lam [x].t''" using ih a1 by auto 
+  then show "App t t2 \<Down> t3" using a2 a3 by auto
+qed (auto dest!: e_App_elim)
+
+
+text {* 
+  Next we extend the lemma above to arbitray initial
+  sequences of cbv-reductions. *}
+
+lemma cbvs_eval:
+  assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3"
+  shows "t1 \<Down> t3"
+using a by (induct) (auto intro: cbv_eval)
+
+text {* 
+  Finally, we can show that if from a term t we reach a value 
+  by a cbv-reduction sequence, then t evaluates to this value. *}
+
+lemma cbvs_implies_eval:
+  assumes a: "t \<longrightarrow>cbv* v" "val v"
+  shows "t \<Down> v"
+using a
+by (induct) (auto intro: eval_val cbvs_eval)
+
+text {* 
+  All facts tied together give us the desired property about
+  K machines. *}
+
+theorem machines_implies_eval:
+  assumes a: "<t1, []> \<mapsto>* <t2, []>" 
+  and     b: "val t2" 
+  shows "t1 \<Down> t2"
+proof -
+  have "t1 \<longrightarrow>cbv* t2" using a by (simp add: machines_implies_cbvs)
+  then show "t1 \<Down> t2" using b by (simp add: cbvs_implies_eval)
+qed
+
+lemma valid_elim:
+  assumes a: "valid ((x, T) # \<Gamma>)"
+  shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>"
+using a by (cases) (auto)
+
+lemma valid_insert:
+  assumes a: "valid (\<Delta> @ [(x, T)] @ \<Gamma>)"
+  shows "valid (\<Delta> @ \<Gamma>)" 
+using a
+by (induct \<Delta>)
+   (auto simp add: fresh_append fresh_Cons dest!: valid_elim)
+
+lemma fresh_list: 
+  shows "atom y \<sharp> xs = (\<forall>x \<in> set xs. atom y \<sharp> x)"
+by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
+
+lemma context_unique:
+  assumes a1: "valid \<Gamma>"
+  and     a2: "(x, T) \<in> set \<Gamma>"
+  and     a3: "(x, U) \<in> set \<Gamma>"
+  shows "T = U" 
+using a1 a2 a3
+by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)
+
+lemma type_substitution_aux:
+  assumes a: "(\<Delta> @ [(x, T')] @ \<Gamma>) \<turnstile> e : T"
+  and     b: "\<Gamma> \<turnstile> e' : T'"
+  shows "(\<Delta> @ \<Gamma>) \<turnstile> e[x ::= e'] : T" 
+using a b 
+proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
+  case (t_Var y T x e' \<Delta>)
+  have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact
+  have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact 
+  have a3: "\<Gamma> \<turnstile> e' : T'" by fact
+  from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
+  { assume eq: "x = y"
+    from a1 a2 have "T = T'" using eq by (auto intro: context_unique)
+    with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" using eq a4 by (auto intro: weakening)
+  }
+  moreover
+  { assume ineq: "x \<noteq> y"
+    from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp
+    then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" using ineq a4 by auto
+  }
+  ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast
+qed (force simp add: fresh_append fresh_Cons)+
+
+corollary type_substitution:
+  assumes a: "(x,T') # \<Gamma> \<turnstile> e : T"
+  and     b: "\<Gamma> \<turnstile> e' : T'"
+  shows "\<Gamma> \<turnstile> e[x::=e'] : T"
+using a b type_substitution_aux[where \<Delta>="[]"]
+by (auto)
+
+lemma t_App_elim:
+  assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"
+  shows "\<exists>T'. \<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<and> \<Gamma> \<turnstile> t2 : T'"
+using a
+by (cases) (auto simp add: lam.eq_iff lam.distinct)
+
+lemma t_Lam_elim:
+  assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" 
+  and     fc: "atom x \<sharp> \<Gamma>" 
+  shows "\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> (x, T1) # \<Gamma> \<turnstile> t : T2"
+using ty fc
+apply(cases)
+apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)
+apply(auto simp add: Abs1_eq_iff)
+apply(rule_tac p="(x \<leftrightarrow> xa)" in permute_boolE)
+apply(perm_simp)
+apply(simp add: flip_def swap_fresh_fresh ty_fresh)
+done
+
+theorem cbv_type_preservation:
+  assumes a: "t \<longrightarrow>cbv t'"
+  and     b: "\<Gamma> \<turnstile> t : T" 
+  shows "\<Gamma> \<turnstile> t' : T"
+using a b
+by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)
+   (auto dest!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)
+
+corollary cbvs_type_preservation:
+  assumes a: "t \<longrightarrow>cbv* t'"
+  and     b: "\<Gamma> \<turnstile> t : T" 
+  shows "\<Gamma> \<turnstile> t' : T"
+using a b
+by (induct) (auto intro: cbv_type_preservation)
+
+text {* 
+  The Type-Preservation Property for the Machine and Evaluation Relation. *}
+
+theorem machine_type_preservation:
+  assumes a: "<t, []> \<mapsto>* <t', []>"
+  and     b: "\<Gamma> \<turnstile> t : T" 
+  shows "\<Gamma> \<turnstile> t' : T"
+proof -
+  from a have "t \<longrightarrow>cbv* t'" by (simp add: machines_implies_cbvs)
+  then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: cbvs_type_preservation)
+qed
+
+theorem eval_type_preservation:
+  assumes a: "t \<Down> t'"
+  and     b: "\<Gamma> \<turnstile> t : T" 
+  shows "\<Gamma> \<turnstile> t' : T"
+proof -
+  from a have "<t, []> \<mapsto>* <t', []>" by (simp add: eval_implies_machines)
+  then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation)
+qed
+
+text {* The Progress Property *}
+
+lemma canonical_tArr:
+  assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"
+  and     b: "val t"
+  shows "\<exists>x t'. t = Lam [x].t'"
+using b a by (induct) (auto) 
+
+theorem progress:
+  assumes a: "[] \<turnstile> t : T"
+  shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"
+using a
+by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)
+   (auto intro: cbv.intros dest!: canonical_tArr)
+
+