--- a/Tutorial/Tutorial2.thy Sat Jan 22 15:07:36 2011 -0600
+++ b/Tutorial/Tutorial2.thy Sat Jan 22 16:04:40 2011 -0600
@@ -1,15 +1,93 @@
+
theory Tutorial2
-imports Tutorial1
+imports Lambda
begin
-(* fixme: put height example here *)
+section {* Height of a Lambda-Term *}
+
+text {*
+ The theory Lambda defines the notions of capture-avoiding
+ substitution and the height of lambda terms.
+*}
+
+thm height.simps
+thm subst.simps
+
+subsection {* EXERCISE 7 *}
+
+text {*
+ Lets prove a property about the height of substitutions.
+
+ Assume that the height of a lambda-term is always greater
+ or equal to 1.
+*}
+
+lemma height_ge_one:
+ shows "1 \<le> height t"
+by (induct t rule: lam.induct) (auto)
+
+text {* Remove the sorries *}
+
+theorem height_subst:
+ shows "height (t[x ::= t']) \<le> height t - 1 + height t'"
+proof (induct t rule: lam.induct)
+ case (Var y)
+ show "height (Var y[x ::= t']) \<le> height (Var y) - 1 + height t'" sorry
+next
+ case (App t1 t2)
+ have ih1: "height (t1[x::=t']) \<le> (height t1) - 1 + height t'" by fact
+ have ih2: "height (t2[x::=t']) \<le> (height t2) - 1 + height t'" by fact
+
+ show "height ((App t1 t2)[x ::= t']) \<le> height (App t1 t2) - 1 + height t'" sorry
+next
+ case (Lam y t1)
+ have ih: "height (t1[x::=t']) \<le> height t1 - 1 + height t'" by fact
+ -- {* the definition of capture-avoiding substitution *}
+ thm subst.simps
+
+ show "height ((Lam [y].t1)[x ::= t']) \<le> height (Lam [y].t1) - 1 + height t'" sorry
+qed
-section {* Types *}
+text {*
+ The point is that substitutions can only be moved under a binder
+ provided certain freshness conditions are satisfied. The structural
+ induction above does not say anything about such freshness conditions.
+
+ Fortunately, Nominal derives automatically some stronger induction
+ principle for lambda terms which has the usual variable convention
+ build in.
+
+ In the proof below, we use this stronger induction principle. The
+ variable and application case are as before.
+*}
+
+
+theorem
+ shows "height (t[x ::= t']) \<le> height t - 1 + height t'"
+proof (nominal_induct t avoiding: x t' rule: lam.strong_induct)
+ case (Var y)
+ have "1 \<le> height t'" using height_ge_one by simp
+ then show "height (Var y[x ::= t']) \<le> height (Var y) - 1 + height t'" by simp
+next
+ case (App t1 t2)
+ have ih1: "height (t1[x::=t']) \<le> (height t1) - 1 + height t'"
+ and ih2: "height (t2[x::=t']) \<le> (height t2) - 1 + height t'" by fact+
+ then show "height ((App t1 t2)[x ::= t']) \<le> height (App t1 t2) - 1 + height t'" by simp
+next
+ case (Lam y t1)
+ have ih: "height (t1[x::=t']) \<le> height t1 - 1 + height t'" by fact
+ have vc: "atom y \<sharp> x" "atom y \<sharp> t'" by fact+ -- {* usual variable convention *}
+
+ show "height ((Lam [y].t1)[x ::= t']) \<le> height (Lam [y].t1) - 1 + height t'" sorry
+qed
+
+
+section {* Types and the Weakening Lemma *}
nominal_datatype ty =
tVar "string"
-| tArr "ty" "ty" ("_ \<rightarrow> _" [100, 100] 100)
+| tArr "ty" "ty" (infixr "\<rightarrow>" 100)
text {*
@@ -19,7 +97,6 @@
We next define the type of typing contexts, a predicate that
defines valid contexts (i.e. lists that contain only unique
variables) and the typing judgement.
-
*}
type_synonym ty_ctx = "(name \<times> ty) list"
@@ -79,7 +156,7 @@
"\<Gamma>1 \<sqsubseteq> \<Gamma>2 \<equiv> \<forall>x. x \<in> set \<Gamma>1 \<longrightarrow> x \<in> set \<Gamma>2"
-subsection {* EXERCISE 4 *}
+subsection {* EXERCISE 8 *}
text {*
Fill in the details and give a proof of the weakening lemma.
@@ -107,7 +184,7 @@
have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact
show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry
-qed (auto) -- {* the application case *}
+qed (auto) -- {* the application case is automatic*}
text {*
@@ -170,10 +247,10 @@
text {*
- The remedy is to use a stronger induction principle that
+ The remedy is to use again a stronger induction principle that
has the usual "variable convention" already build in. The
- following command derives this induction principle for us.
- (We shall explain what happens here later.)
+ following command derives this induction principle for the typing
+ relation. (We shall explain what happens here later.)
*}
nominal_inductive typing
@@ -184,7 +261,7 @@
text {* Compare the two induction principles *}
thm typing.induct
-thm typing.strong_induct -- {* has the additional assumption {atom x} \<sharp> c *}
+thm typing.strong_induct -- {* note the additional assumption {atom x} \<sharp> c *}
text {*
We can use the stronger induction principle by replacing
@@ -198,7 +275,8 @@
Try now the proof.
*}
-
+
+subsection {* EXERCISE 9 *}
lemma weakening:
assumes a: "\<Gamma>1 \<turnstile> t : T"
@@ -207,7 +285,7 @@
shows "\<Gamma>2 \<turnstile> t : T"
using a b c
proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)
- case (t_Var \<Gamma>1 x T) -- {* variable case is as before *}
+ case (t_Var \<Gamma>1 x T) -- {* again the variable case is as before *}
have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact
moreover
have "valid \<Gamma>2" by fact
@@ -221,34 +299,56 @@
have a0: "atom x \<sharp> \<Gamma>1" by fact
have a1: "valid \<Gamma>2" by fact
have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact
- have "valid ((x, T1) # \<Gamma>2)" using a1 vc by auto
- moreover
- have "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # \<Gamma>2" using a2 by auto
- ultimately
- have "(x, T1) # \<Gamma>2 \<turnstile> t : T2" using ih by simp
- then show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" using vc by auto
+
+ show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry
qed (auto) -- {* app case *}
-text {* unbind / inconsistency example *}
+
+section {* Unbind and an Inconsistency Example *}
+
+text {*
+ You might wonder why we had to discharge some proof
+ obligations in order to obtain the stronger induction
+ principle for the typing relation. (Remember for
+ lambda terms this stronger induction principle is
+ derived automatically.)
+
+ This proof obligation is really needed, because if we
+ assume universally a stronger induction principle, then
+ in some cases we can derive false. This is "shown" below.
+*}
+
inductive
- unbind :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _" [60, 60] 60)
+ unbind :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixr "\<mapsto>" 60)
where
u_Var[intro]: "Var x \<mapsto> Var x"
| u_App[intro]: "App t1 t2 \<mapsto> App t1 t2"
| u_Lam[intro]: "t \<mapsto> t' \<Longrightarrow> Lam [x].t \<mapsto> t'"
+text {* It is clear that the following judgement holds. *}
+
lemma unbind_simple:
shows "Lam [x].Var x \<mapsto> Var x"
by auto
+text {*
+ Now lets derive the strong induction principle for unbind.
+ The point is that we cannot establish the proof obligations,
+ therefore we force Isabelle to accept them by using "sorry".
+*}
+
equivariance unbind
-
nominal_inductive unbind
avoids u_Lam: "x"
sorry
+text {*
+ Using the stronger induction principle, we can establish
+ th follwoing bogus property.
+*}
+
lemma unbind_fake:
fixes y::"name"
assumes a: "t \<mapsto> t'"
@@ -265,12 +365,20 @@
then show "atom y \<sharp> t'" using ih by simp
qed
+text {*
+ And from this follows the inconsitency:
+*}
+
lemma
shows "False"
proof -
have "atom x \<sharp> Lam [x]. Var x" by (simp add: lam.fresh)
- then have "atom x \<sharp> Var x" using unbind_fake unbind_simple by auto
- then show "False" by (simp add: lam.fresh fresh_at_base)
+ moreover
+ have "Lam [x]. Var x \<mapsto> Var x" using unbind_simple by auto
+ ultimately
+ have "atom x \<sharp> Var x" using unbind_fake by auto
+ then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base)
+ then show "False" by simp
qed
end