--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Tutorial2.thy Fri Jan 21 21:58:51 2011 +0100
@@ -0,0 +1,277 @@
+theory Tutorial2
+imports Tutorial1
+begin
+
+(* fixme: put height example here *)
+
+
+section {* Types *}
+
+nominal_datatype ty =
+ tVar "string"
+| tArr "ty" "ty" ("_ \<rightarrow> _" [100, 100] 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 4 *}
+
+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 *}
+
+
+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 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.)
+*}
+
+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 -- {* has 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.
+*}
+
+
+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 *}
+
+
+text {* unbind / inconsistency example *}
+
+inductive
+ unbind :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _" [60, 60] 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'"
+
+lemma unbind_simple:
+ shows "Lam [x].Var x \<mapsto> Var x"
+ by auto
+
+equivariance unbind
+
+nominal_inductive unbind
+ avoids u_Lam: "x"
+ sorry
+
+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
+
+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)
+qed
+
+end