--- a/Tutorial/Tutorial2.thy Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,384 +0,0 @@
-
-theory Tutorial2
-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 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
-
-
-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" (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 only:)
-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) -- {* again the 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
-
- show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry
-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 blast
- then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base)
- then show "False" by simp
-qed
-
-end