# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295721961 21600
# Node ID 2abc8cb46a5c437d394440f773b37003db6368ee
# Parent  da9bed7baf2323e05887835355395dbbc1419cfb
better version of Tutorial 1

diff -r da9bed7baf23 -r 2abc8cb46a5c Tutorial/Tutorial1.thy
--- a/Tutorial/Tutorial1.thy	Fri Jan 21 22:58:03 2011 +0100
+++ b/Tutorial/Tutorial1.thy	Sat Jan 22 12:46:01 2011 -0600
@@ -1,4 +1,3 @@
-
 header {* 
 
   Nominal Isabelle Tutorial at POPL'11
@@ -61,7 +60,6 @@
         \<bullet>    bullet    (permutation application)
 *}
 
-
 theory Tutorial1
 imports Lambda
 begin
@@ -183,7 +181,7 @@
 
 text {*
   In this section we want to define inductively the evaluation
-  relation for lambda terms.
+  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. 
@@ -213,10 +211,8 @@
   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 are also defined using inductive. In our case values
-  are just lambda-abstractions. 
+  Values and cbv are also defined using inductive.  
 *}
 
 inductive
@@ -224,7 +220,6 @@
 where
   v_Lam[intro]:   "val (Lam [x].t)"
 
-
 section {* Theorems *}
 
 text {*
@@ -362,6 +357,7 @@
    Two very simple example proofs are as follows.
 *}
 
+subsection {* EXERCISE 1 *}
 
 lemma eval_val:
   assumes a: "val t"
@@ -372,7 +368,11 @@
   show "Lam [x]. t \<Down> Lam [x]. t" sorry
 qed
 
-lemma eavl_to_val:
+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
@@ -381,16 +381,94 @@
   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
+  then show "<e1, Es1> \<mapsto>* <e3, Es3>" by simp
+next
+  case (ms2 e1 Es1 e2 Es2 e2' Es2') 
+  have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact
+  have d1: "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact
+  have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact
+  show "<e1, Es1> \<mapsto>* <e3, Es3>" using d1 d2 ih by blast
+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
@@ -398,7 +476,22 @@
   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 
@@ -418,108 +511,6 @@
   "statement". With this we can simplify our proof further to:
 *}
 
-
-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:
-*}
-
-
-
-
-section {* Datatypes: Evaluation Contexts *}
-
-text {*
-
-  Datatypes can be defined in Isabelle as follows: we have to provide the name 
-  of the datatype and 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? 
-*}
-
-type_synonym ctxs = "ctx list"
-
-inductive
-  machine :: "lam \<Rightarrow> ctxs \<Rightarrow>lam \<Rightarrow> ctxs \<Rightarrow> bool" ("<_,_> \<mapsto> <_,_>" [60, 60, 60, 60] 60)
-where
-  m1[intro]: "<App t1 t2,Es> \<mapsto> <t1,(CAppL \<box> t2) # Es>"
-| m2[intro]: "val v \<Longrightarrow> <v,(CAppL \<box> t2) # Es> \<mapsto> <t2,(CAppR v \<box>) # Es>"
-| m3[intro]: "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[intro]: "<t,Es> \<mapsto>* <t,Es>"
-| ms2[intro]: "\<lbrakk><t1,Es1> \<mapsto> <t2,Es2>; <t2,Es2> \<mapsto>* <t3,Es3>\<rbrakk> \<Longrightarrow> <t1,Es1> \<mapsto>* <t3,Es3>"
-
-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)
-  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
-  show "<e1, Es1> \<mapsto>* <e3, Es3>" using d1 d2 ih by blast
-qed
-
-text {* 
-  Just like gotos in the Basic programming language, labels can 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. In the proof below this has been used
-  in order to get rid of the labels c and d1. 
-*}
-
-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
-
 lemma 
   assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" 
   and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
@@ -539,16 +530,36 @@
 qed
 
 
-lemma ms3[intro]:
+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)
 
-lemma eval_to_val:  (* fixme: done above *)
-  assumes a: "t \<Down> t'"
-  shows "val t'"
-using a 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'"
@@ -567,10 +578,47 @@
   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
 
+
+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: 
@@ -607,6 +655,7 @@
 | "(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: 
diff -r da9bed7baf23 -r 2abc8cb46a5c Tutorial/Tutorial4.thy
--- a/Tutorial/Tutorial4.thy	Fri Jan 21 22:58:03 2011 +0100
+++ b/Tutorial/Tutorial4.thy	Sat Jan 22 12:46:01 2011 -0600
@@ -5,18 +5,62 @@
 
 section {* The CBV Reduction Relation (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: "t \<longrightarrow>cbv t' \<Longrightarrow> App t t2 \<longrightarrow>cbv App t' t2"
+| cbv3: "t \<longrightarrow>cbv t' \<Longrightarrow> App t2 t \<longrightarrow>cbv App t2 t'"
+
+inductive 
+  "cbv_star" :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>cbv* _" [60, 60] 60)
+where
+  cbvs1: "e \<longrightarrow>cbv* e"
+| cbvs2: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"
+
+declare cbv.intros[intro] cbv_star.intros[intro]
+
+subsection {* EXERCISE 3 *}
+
+text {*
+  Show that cbv* is transitive, by filling the gaps in the 
+  proof below.
+*}
+
+lemma 
+  assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"
+  shows "e1 \<longrightarrow>cbv* e3"
+using a 
+proof (induct) 
+  case (cbvs1 e1)
+  have asm: "e1 \<longrightarrow>cbv* e3" by fact
+  show "e1 \<longrightarrow>cbv* e3" sorry
+next
+  case (cbvs2 e1 e2 e3')
+  have "e1 \<longrightarrow>cbv e2" by fact
+  have "e2 \<longrightarrow>cbv* e3'" by fact
+  have "e3' \<longrightarrow>cbv* e3 \<Longrightarrow> e2 \<longrightarrow>cbv* e3" by fact
+  have "e3' \<longrightarrow>cbv* e3" by fact
+
+  show "e1 \<longrightarrow>cbv* e3" sorry
+qed 
+
+lemma cbvs3 [intro]:
+  assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"
+  shows "e1 \<longrightarrow>cbv* e3"
+using a by (induct) (auto) 
+
+
+
+
+
 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
@@ -44,7 +88,7 @@
 
 lemma better_cbv1 [intro]: 
   assumes a: "val v" 
-  shows "App (Lam [x].t) v \<longrightarrow>cbv t[x::=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
@@ -58,16 +102,8 @@
   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 *}