--- 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: