--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Tutorial2s.thy Sat Jan 22 16:04:40 2011 -0600
@@ -0,0 +1,354 @@
+
+theory Tutorial2s
+imports Lambda
+begin
+
+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
+ 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
+ moreover
+ have vc: "atom y \<sharp> x" "atom y \<sharp> t'" by fact+ -- {* usual variable convention *}
+ ultimately
+ show "height ((Lam [y].t1)[x ::= t']) \<le> height (Lam [y].t1) - 1 + height t'" by simp
+qed
+
+
+section {* Types and the Weakening Lemma *}
+
+nominal_datatype ty =
+ tVar "string"
+| tArr "ty" "ty" (infixr "\<rightarrow>" 100)
+
+
+text {*
+ Having defined them as nominal datatypes gives us additional
+ definitions and theorems that come with types (see below).
+
+ 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"
+
+inductive
+ valid :: "ty_ctx \<Rightarrow> bool"
+where
+ v1[intro]: "valid []"
+| v2[intro]: "\<lbrakk>valid \<Gamma>; atom x \<sharp> \<Gamma>\<rbrakk>\<Longrightarrow> valid ((x, T) # \<Gamma>)"
+
+
+inductive
+ typing :: "ty_ctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60, 60, 60] 60)
+where
+ t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
+| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
+| t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1 \<rightarrow> T2"
+
+
+text {*
+ The predicate atom x \<sharp> \<Gamma>, read as x fresh for \<Gamma>, is defined by
+ Nominal Isabelle. It is defined for lambda-terms, products, lists etc.
+ For example we have:
+*}
+
+lemma
+ fixes x::"name"
+ shows "atom x \<sharp> Lam [x].t"
+ and "atom x \<sharp> (t1, t2) \<Longrightarrow> atom x \<sharp> App t1 t2"
+ and "atom x \<sharp> Var y \<Longrightarrow> atom x \<sharp> y"
+ and "\<lbrakk>atom x \<sharp> t1; atom x \<sharp> t2\<rbrakk> \<Longrightarrow> atom x \<sharp> (t1, t2)"
+ and "\<lbrakk>atom x \<sharp> l1; atom x \<sharp> l2\<rbrakk> \<Longrightarrow> atom x \<sharp> (l1 @ l2)"
+ and "atom x \<sharp> y \<Longrightarrow> x \<noteq> y"
+ by (simp_all add: lam.fresh fresh_append fresh_at_base)
+
+text {*
+ We can also prove that every variable is fresh for a type.
+*}
+
+lemma ty_fresh:
+ fixes x::"name"
+ and T::"ty"
+ shows "atom x \<sharp> T"
+by (induct T rule: ty.induct)
+ (simp_all add: ty.fresh pure_fresh)
+
+text {*
+ In order to state the weakening lemma in a convenient form, we
+ using the following abbreviation. Abbreviations behave like
+ definitions, except that they are always automatically folded
+ and unfolded.
+*}
+
+abbreviation
+ "sub_ty_ctx" :: "ty_ctx \<Rightarrow> ty_ctx \<Rightarrow> bool" ("_ \<sqsubseteq> _" [60, 60] 60)
+where
+ "\<Gamma>1 \<sqsubseteq> \<Gamma>2 \<equiv> \<forall>x. x \<in> set \<Gamma>1 \<longrightarrow> x \<in> set \<Gamma>2"
+
+
+subsection {* EXERCISE 8 *}
+
+text {*
+ Fill in the details and give a proof of the weakening lemma.
+*}
+
+lemma
+ assumes a: "\<Gamma>1 \<turnstile> t : T"
+ and b: "valid \<Gamma>2"
+ and c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"
+ shows "\<Gamma>2 \<turnstile> t : T"
+using a b c
+proof (induct arbitrary: \<Gamma>2)
+ case (t_Var \<Gamma>1 x T)
+ have a1: "valid \<Gamma>1" by fact
+ have a2: "(x, T) \<in> set \<Gamma>1" by fact
+ have a3: "valid \<Gamma>2" by fact
+ have a4: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact
+
+ show "\<Gamma>2 \<turnstile> Var x : T" sorry
+next
+ case (t_Lam x \<Gamma>1 T1 t T2)
+ have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact
+ 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
+
+ show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry
+qed (auto) -- {* the application case is automatic*}
+
+
+text {*
+ Despite the frequent claim that the weakening lemma is trivial,
+ routine or obvious, the proof in the lambda-case does not go
+ through smoothly. Painful variable renamings seem to be necessary.
+ But the proof using renamings is horribly complicated (see below).
+*}
+
+equivariance valid
+equivariance typing
+
+lemma weakening_NOT_TO_BE_TRIED_AT_HOME:
+ assumes a: "\<Gamma>1 \<turnstile> t : T"
+ and b: "valid \<Gamma>2"
+ and c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"
+ shows "\<Gamma>2 \<turnstile> t : T"
+using a b c
+proof (induct arbitrary: \<Gamma>2)
+ -- {* lambda case *}
+ case (t_Lam x \<Gamma>1 T1 t T2)
+ have fc0: "atom x \<sharp> \<Gamma>1" by fact
+ have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact
+ -- {* we choose a fresh variable *}
+ obtain c::"name" where fc1: "atom c \<sharp> (x, t, \<Gamma>1, \<Gamma>2)" by (rule obtain_fresh)
+ -- {* we alpha-rename the abstraction *}
+ have "Lam [c].((c \<leftrightarrow> x) \<bullet> t) = Lam [x].t" using fc1
+ by (auto simp add: lam.eq_iff Abs1_eq_iff flip_def)
+ moreover
+ -- {* we can then alpha rename the goal *}
+ have "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2"
+ proof -
+ -- {* we need to establish *}
+ -- {* (1) (x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) *}
+ -- {* (2) valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)) *}
+ have "(1)": "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)"
+ proof -
+ have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact
+ then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" using fc0 fc1
+ by (perm_simp) (simp add: flip_fresh_fresh)
+ then show "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)" by (rule permute_boolE)
+ qed
+ moreover
+ have "(2)": "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))"
+ proof -
+ have "valid \<Gamma>2" by fact
+ then show "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" using fc1
+ by (auto simp add: fresh_permute_left atom_eqvt valid.eqvt)
+ qed
+ -- {* these two facts give us by induction hypothesis the following *}
+ ultimately have "(x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2" using ih by simp
+ -- {* we now apply renamings to get to our goal *}
+ then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2)" by (rule permute_boolI)
+ then have "(c, T1) # \<Gamma>2 \<turnstile> ((c \<leftrightarrow> x) \<bullet> t) : T2" using fc1
+ by (perm_simp) (simp add: flip_fresh_fresh ty_fresh)
+ then show "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" using fc1 by auto
+ qed
+ ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp
+qed (auto) -- {* var and app cases, luckily, are automatic *}
+
+
+text {*
+ 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 the typing
+ relation. (We shall explain what happens here later.)
+*}
+
+nominal_inductive typing
+ avoids t_Lam: "x"
+ unfolding fresh_star_def
+ by (simp_all add: fresh_Pair lam.fresh ty_fresh)
+
+text {* Compare the two induction principles *}
+
+thm typing.induct
+thm typing.strong_induct -- {* note the additional assumption {atom x} \<sharp> c *}
+
+text {*
+ We can use the stronger induction principle by replacing
+ the line
+
+ proof (induct arbitrary: \<Gamma>2)
+
+ with
+
+ proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)
+
+ Try now the proof.
+*}
+
+subsection {* EXERCISE 9 *}
+
+lemma weakening:
+ assumes a: "\<Gamma>1 \<turnstile> t : T"
+ and b: "valid \<Gamma>2"
+ and c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"
+ 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 *}
+ have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact
+ moreover
+ have "valid \<Gamma>2" by fact
+ moreover
+ have "(x, T)\<in> set \<Gamma>1" by fact
+ ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto
+next
+ case (t_Lam x \<Gamma>1 T1 t T2)
+ have vc: "atom x \<sharp> \<Gamma>2" by fact -- {* additional fact afforded by the strong induction *}
+ have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact
+ 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
+qed (auto) -- {* app case *}
+
+
+
+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" (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'"
+ and b: "atom y \<sharp> t"
+ shows "atom y \<sharp> t'"
+using a b
+proof (nominal_induct avoiding: y rule: unbind.strong_induct)
+ case (u_Lam t t' x y)
+ have ih: "atom y \<sharp> t \<Longrightarrow> atom y \<sharp> t'" by fact
+ have asm: "atom y \<sharp> Lam [x]. t" by fact
+ have fc: "atom x \<sharp> y" by fact
+ then have in_eq: "x \<noteq> y" by (simp add: fresh_at_base)
+ then have "atom y \<sharp> t" using asm by (simp add: lam.fresh)
+ 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)
+ 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