--- a/Tutorial/Lambda.thy Sat Jan 22 16:37:00 2011 -0600
+++ b/Tutorial/Lambda.thy Sat Jan 22 18:59:48 2011 -0600
@@ -105,18 +105,13 @@
shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
by (induct t x s rule: subst.induct) (simp_all)
-
-subsection {* Single-Step Beta-Reduction *}
-
-inductive
- beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80)
-where
- b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s"
-| b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2"
-| b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2"
-| b4[intro]: "App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]"
-
-
+lemma fresh_fact:
+ assumes a: "atom z \<sharp> s"
+ and b: "z = y \<or> atom z \<sharp> t"
+ shows "atom z \<sharp> t[y ::= s]"
+using a b
+by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
+ (auto simp add: lam.fresh fresh_at_base)
end
--- a/Tutorial/Tutorial4.thy Sat Jan 22 16:37:00 2011 -0600
+++ b/Tutorial/Tutorial4.thy Sat Jan 22 18:59:48 2011 -0600
@@ -1,6 +1,6 @@
theory Tutorial4
-imports Tutorial1 Tutorial2 Tutorial3
+imports Tutorial1 Tutorial2
begin
section {* The CBV Reduction Relation (Small-Step Semantics) *}
@@ -21,14 +21,14 @@
declare cbv.intros[intro] cbv_star.intros[intro]
-subsection {* EXERCISE 3 *}
+subsection {* EXERCISE 11 *}
text {*
Show that cbv* is transitive, by filling the gaps in the
proof below.
*}
-lemma
+lemma cbvs3 [intro]:
assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"
shows "e1 \<longrightarrow>cbv* e3"
using a
@@ -46,17 +46,9 @@
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
+ In order to help establishing the property that the machine
calculates a nomrmalform that corresponds to the evaluation
relation, we introduce the call-by-value small-step semantics.
*}
@@ -98,15 +90,9 @@
finally show "App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]" by simp
qed
-text {*
- The transitive closure of the cbv-reduction relation:
-*}
-
-
-
-subsection {* EXERCISE 8 *}
+subsection {* EXERCISE 12 *}
text {*
If more simple exercises are needed, then complete the following proof.
@@ -119,26 +105,22 @@
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
+ 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
- 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
+
+ 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
- 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
+
+ show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" sorry
qed
-section {* EXERCISE 9 *}
+section {* EXERCISE 13 *}
text {*
The point of the cbv-reduction was that we can easily relatively
@@ -167,7 +149,8 @@
text {*
It is not difficult to extend the lemma above to
- arbitrary reductions sequences of the CK machine. *}
+ arbitrary reductions sequences of the machine.
+*}
lemma machines_implies_cbvs_ctx:
assumes a: "<e, Es> \<mapsto>* <e', Es'>"
@@ -176,7 +159,7 @@
by (induct) (blast)+
text {*
- So whenever we let the CL machine start in an initial
+ So whenever we let the machine start in an initial
state and it arrives at a final state, then there exists
a corresponding cbv-reduction sequence.
*}
@@ -192,14 +175,10 @@
text {*
We now want to relate the cbv-reduction to the evaluation
- relation. For this we need two auxiliary lemmas.
+ relation. For this we need one auxiliary lemma about
+ inverting the e_App rule.
*}
-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"
@@ -207,7 +186,7 @@
using a by (cases) (auto simp add: lam.eq_iff lam.distinct)
-subsection {* EXERCISE *}
+subsection {* EXERCISE 13 *}
text {*
Complete the first and second case in the
@@ -222,9 +201,8 @@
case (cbv1 v x t t3)
have a1: "val v" by fact
have a2: "t[x ::= v] \<Down> t3" by fact
- have a3: "Lam [x].t \<Down> Lam [x].t" by auto
- have a4: "v \<Down> v" using a1 eval_val by auto
- show "App (Lam [x].t) v \<Down> t3" using a3 a4 a2 by auto
+
+ 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
@@ -233,14 +211,15 @@
where a1: "t' \<Down> Lam [x].t''"
and a2: "t2 \<Down> v'"
and a3: "t''[x ::= v'] \<Down> t3" by (rule e_App_elim)
- have "t \<Down> Lam [x].t''" using ih a1 by auto
- then show "App t t2 \<Down> t3" using a2 a3 by auto
+
+ show "App t t2 \<Down> t3" sorry
qed (auto elim!: e_App_elim)
text {*
Next we extend the lemma above to arbitray initial
- sequences of cbv-reductions. *}
+ sequences of cbv-reductions.
+*}
lemma cbvs_eval:
assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3"
@@ -250,30 +229,42 @@
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.
+
+ This proof is not by induction. So we have to set up the proof
+ with
+
+ proof -
+
+ in order to prevent Isabelle from applying a default introduction
+ rule.
*}
lemma cbvs_implies_eval:
- assumes a: "t \<longrightarrow>cbv* v" "val v"
+ assumes a: "t \<longrightarrow>cbv* v"
+ and b: "val v"
shows "t \<Down> v"
-using a
-by (induct) (auto intro: eval_val cbvs_eval)
+proof -
+ have "v \<Down> v" using b eval_val by simp
+ then show "t \<Down> v" using a cbvs_eval by auto
+qed
+
+section {* EXERCISE 15 *}
text {*
- All facts tied together give us the desired property about
- machines.
+ All facts tied together give us the desired property
+ about machines: we know that a machines transitions
+ correspond to cbvs transitions, and with the lemma
+ above they correspond to an eval judgement.
*}
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 machines_implies_cbvs by simp
- then show "t1 \<Down> t2" using b cbvs_implies_eval by simp
+proof -
+
+ show "t1 \<Down> t2" sorry
qed
-
-
-
end
--- a/Tutorial/Tutorial5.thy Sat Jan 22 16:37:00 2011 -0600
+++ b/Tutorial/Tutorial5.thy Sat Jan 22 18:59:48 2011 -0600
@@ -1,9 +1,22 @@
+
+
theory Tutorial5
imports Tutorial4
begin
+section {* Type-Preservation and Progress Lemma*}
-section {* Type Preservation (fixme separate file) *}
+text {*
+ The point of this tutorial is to prove the
+ type-preservation and progress lemma. Since
+ we now know that \<Down>, \<longrightarrow>cbv* and the machine
+ correspond to each other, we only need to
+ prove this property for one of them. We chose
+ \<longrightarrow>cbv.
+
+ First we need to establish two elimination
+ properties and two auxiliary lemmas about contexts.
+*}
lemma valid_elim:
@@ -30,6 +43,16 @@
using a1 a2 a3
by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)
+
+section {* EXERCISE 16 *}
+
+text {*
+ Next we want to show the type substitution lemma. Unfortunately,
+ we have to prove a slightly more general version of it, where
+ the variable being substituted occurs somewhere inside the
+ context.
+*}
+
lemma type_substitution_aux:
assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T"
and b: "\<Gamma> \<turnstile> e' : T'"
@@ -40,10 +63,11 @@
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)
+
+ have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" sorry
}
moreover
{ assume ineq: "x \<noteq> y"
@@ -51,15 +75,46 @@
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)+
+next
+ case (t_Lam y T1 t T2 x e' \<Delta>)
+ have a1: "atom y \<sharp> e'" by fact
+ have a2: "atom y \<sharp> \<Delta> @ [(x, T')] @ \<Gamma>" by fact
+ have a3: "\<Gamma> \<turnstile> e' : T'" by fact
+ have ih: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> ((y, T1) # \<Delta>) @ \<Gamma> \<turnstile> t [x ::= e'] : T2"
+ using t_Lam(6)[of "(y, T1) # \<Delta>"] by auto
+
+
+ show "\<Delta> @ \<Gamma> \<turnstile> (Lam [y]. t)[x ::= e'] : T1 \<rightarrow> T2" sorry
+next
+ case (t_App t1 T1 T2 t2 x e' \<Delta>)
+ have ih1: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t1 [x ::= e'] : T1 \<rightarrow> T2" using t_App(2) by auto
+ have ih2: "\<Gamma> \<turnstile> e' : T' \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t2 [x ::= e'] : T1" using t_App(4) by auto
+ have a: "\<Gamma> \<turnstile> e' : T'" by fact
+
+ show "\<Delta> @ \<Gamma> \<turnstile> App t1 t2 [x ::= e'] : T2" sorry
+qed
+
+text {*
+ From this we can derive the usual version of the substitution
+ lemma.
+*}
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>="[]"]
+using a b type_substitution_aux[of "[]"]
by auto
+
+section {* Type Preservation *}
+
+text {*
+ Finally we are in a position to establish the type preservation
+ property. We just need the following two inversion rules for
+ particualr typing instances.
+*}
+
lemma t_App_elim:
assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"
obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" "\<Gamma> \<turnstile> t2 : T'"
@@ -81,13 +136,34 @@
apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)
done
+
+section {* EXERCISE 17 *}
+
+text {*
+ Fill in the gaps in the t_Lam case. You will need
+ the type substitution lemma proved above.
+*}
+
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 elim!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)
+proof (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)
+ case (cbv1 v x t \<Gamma> T)
+ have fc: "atom x \<sharp> \<Gamma>" by fact
+ have "\<Gamma> \<turnstile> App (Lam [x]. t) v : T" by fact
+ then obtain T' where
+ *: "\<Gamma> \<turnstile> Lam [x]. t : T' \<rightarrow> T" and
+ **: "\<Gamma> \<turnstile> v : T'" by (rule t_App_elim)
+ have "(x, T') # \<Gamma> \<turnstile> t : T" using * fc by (rule t_Lam_elim) (simp add: ty.eq_iff)
+
+ show "\<Gamma> \<turnstile> t [x ::= v] : T " sorry
+qed (auto elim!: t_App_elim)
+
+text {*
+ We can easily extend this to sequences of cbv* reductions.
+*}
corollary cbvs_type_preservation:
assumes a: "t \<longrightarrow>cbv* t'"