diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/Tutorial1.thy
--- a/Tutorial/Tutorial1.thy	Tue Jan 25 02:46:05 2011 +0900
+++ b/Tutorial/Tutorial1.thy	Tue Jan 25 02:51:44 2011 +0900
@@ -1,4 +1,3 @@
-
 header {* 
 
   Nominal Isabelle Tutorial at POPL'11
@@ -183,7 +182,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. 
@@ -208,15 +207,13 @@
 *}
 
 inductive
-  eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60) 
+  eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixr "\<Down>" 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 are also defined using inductive. In our case values
-  are just lambda-abstractions. 
+  Values and cbv are also defined using inductive.  
 *}
 
 inductive
@@ -224,7 +221,6 @@
 where
   v_Lam[intro]:   "val (Lam [x].t)"
 
-
 section {* Theorems *}
 
 text {*
@@ -362,6 +358,7 @@
    Two very simple example proofs are as follows.
 *}
 
+subsection {* EXERCISE 1 *}
 
 lemma eval_val:
   assumes a: "val t"
@@ -372,7 +369,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 +382,96 @@
   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
@@ -398,7 +479,22 @@
   the next have-statement. This is used in the 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 +514,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 +533,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 +581,12 @@
   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: 
@@ -589,7 +605,6 @@
 using a eval_implies_machines_ctx by simp
 
 
-
 section {* Function Definitions: Filling a Lambda-Term into a Context *}
  
 text {*
@@ -607,6 +622,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: 
@@ -617,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'"
@@ -666,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)
 
@@ -686,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 
@@ -694,7 +717,6 @@
   construction. 
 *}
 
-
 lemma 
   shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
 proof (induct Es1)
@@ -703,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