--- a/Tutorial/Tutorial1.thy Fri Jan 21 00:55:28 2011 +0100
+++ b/Tutorial/Tutorial1.thy Fri Jan 21 21:58:51 2011 +0100
@@ -5,26 +5,26 @@
====================================
Nominal Isabelle is a definitional extension of Isabelle/HOL, which
- means it does not add any new axioms to higher-order logic. It merely
+ means it does not add any new axioms to higher-order logic. It just
adds new definitions and an infrastructure for 'nominal resoning'.
The jEdit Interface
-------------------
- The Isabelle theorem prover comes with an interface for the jEdit.
+ The Isabelle theorem prover comes with an interface for jEdit.
Unlike many other theorem prover interfaces (e.g. ProofGeneral) where you
- try to advance a 'checked' region in a proof script, this interface immediately
- checks the whole buffer. The text you type is also immediately checked
- as you type. Malformed text or unfinished proofs are highlighted in red
- with a little red 'stop' signal on the left-hand side. If you drag the
- 'red-box' cursor over a line, the Output window gives further feedback.
+ advance a 'checked' region in a proof script, this interface immediately
+ checks the whole buffer. The text you type is also immediately checked.
+ Malformed text or unfinished proofs are highlighted in red with a little
+ red 'stop' signal on the left-hand side. If you drag the 'red-box' cursor
+ over a line, the Output window gives further feedback.
Note: If a section is not parsed correctly, the work-around is to cut it
out and paste it back into the text (cut-out: Ctrl + X; paste in: Ctrl + V;
Cmd is Ctrl on the Mac)
- Nominal Isabelle and the interface can be started on the command line with
+ Nominal Isabelle and jEdit can be started by typing on the command line
isabelle jedit -l HOL-Nominal2
isabelle jedit -l HOL-Nominal2 A.thy B.thy ...
@@ -55,10 +55,10 @@
: \<in>
~: \<notin>
- For nominal two important symbols are
+ For nominal the following two symbols have a special meaning
- \<sharp> sharp (freshness)
- \<bullet> bullet (permutations)
+ \<sharp> sharp (freshness)
+ \<bullet> bullet (permutation application)
*}
theory Tutorial1
@@ -70,11 +70,10 @@
text {*
All formal developments in Isabelle are part of a theory. A theory
needs to have a name and must import some pre-existing theory. The
- imported theory will normally be the theory Nominal2 (which contains
- many useful concepts like set-theory, lists, nominal theory etc).
- For the purpose of the tutorial we import the theory Lambda.thy which
- contains already some useful definitions for (alpha-equated) lambda
- terms.
+ imported theory will normally be Nominal2 (which provides many useful
+ concepts like set-theory, lists, nominal things etc). For the purpose
+ of this tutorial we import the theory Lambda.thy, which contains
+ already some useful definitions for (alpha-equated) lambda terms.
*}
@@ -135,16 +134,22 @@
term "atom (x::name)" -- {* atom is an overloded function *}
text {*
- Lam [x].Var is the syntax we made up for lambda abstractions. You can have
- your own syntax, if you prefer (but \<lambda> is already taken up for Isabelle's
- functions). We also came up with "name". If you prefer, you can call
- it "ident" or have more than one type for (object language) variables.
+ Lam [x].Var is the syntax we made up for lambda abstractions. If you
+ prefer, you can have your own syntax (but \<lambda> is already taken up for
+ Isabelle's functions). We also came up with the type "name" for variables.
+ You can introduce your own types of object variables using the
+ command atom_decl:
+*}
+atom_decl ident
+atom_decl ty_var
+
+text {*
Isabelle provides some useful colour feedback about its constants (black),
free variables (blue) and bound variables (green).
*}
-term "True" -- {* a constant that is defined in HOL...written in black *}
+term "True" -- {* a constant defined somewhere...written in black *}
term "true" -- {* not recognised as a constant, therefore it is interpreted
as a free variable, written in blue *}
term "\<forall>x. P x" -- {* x is bound (green), P is free (blue) *}
@@ -262,15 +267,16 @@
Examples are
*}
+
+
lemma alpha_equ:
shows "Lam [x].Var x = Lam [y].Var y"
by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)
lemma Lam_freshness:
- assumes a: "x \<noteq> y"
- and b: "atom y \<sharp> Lam [x].t"
- shows "atom y \<sharp> t"
- using a b by (simp add: lam.fresh Abs_fresh_iff)
+ assumes a: "atom y \<sharp> Lam [x].t"
+ shows "(y = x) \<or> (y \<noteq> x \<and> atom y \<sharp> t)"
+ using a by (auto simp add: lam.fresh Abs_fresh_iff)
lemma neutral_element:
fixes x::"nat"
@@ -500,20 +506,20 @@
assumes a: "t1 \<longrightarrow>b* t2"
shows "t1 \<longrightarrow>b** t2"
using a
-by (induct) (auto intro: beta_star2.intros)
+ by (induct) (auto intro: beta_star2.intros)
lemma
assumes a: "t1 \<longrightarrow>b* t2"
and b: "t2 \<longrightarrow>b* t3"
shows "t1 \<longrightarrow>b* t3"
-using a b
-by (induct) (auto intro: beta_star1.intros)
+ using a b
+ by (induct) (auto intro: beta_star1.intros)
lemma
assumes a: "t1 \<longrightarrow>b** t2"
shows "t1 \<longrightarrow>b* t2"
-using a
-by (induct) (auto intro: bs1_trans2 beta_star1.intros)
+ using a
+ by (induct) (auto intro: bs1_trans2 beta_star1.intros)
inductive
eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60)
@@ -556,13 +562,10 @@
term "CAppL"
term "CAppL \<box> (Var x)"
-text {*
+subsection {* MINI EXERCISE *}
- 1.) MINI EXERCISE
- -----------------
-
+text {*
Try and see what happens if you apply a Hole to a Hole?
-
*}
type_synonym ctxs = "ctx list"
@@ -593,14 +596,13 @@
proof(induct)
case (ms1 e1 Es1)
have c: "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
- show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry
+ then show "<e1, Es1> \<mapsto>* <e3, Es3>" by simp
next
case (ms2 e1 Es1 e2 Es2 e2' Es2')
have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact
have d1: "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact
have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact
-
- show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry
+ show "<e1, Es1> \<mapsto>* <e3, Es3>" using d1 d2 ih by blast
qed
text {*
@@ -658,7 +660,6 @@
shows "val t'"
using a by (induct) (auto)
-
theorem
assumes a: "t \<Down> t'"
shows "<t, []> \<mapsto>* <t', []>"
@@ -666,7 +667,7 @@
proof (induct)
case (e_Lam x t)
-- {* no assumptions *}
- show "<Lam [x].t, []> \<mapsto>* <Lam [x].t, []>" sorry
+ show "<Lam [x].t, []> \<mapsto>* <Lam [x].t, []>" by auto
next
case (e_App t1 x t t2 v' v)
-- {* all assumptions in this case *}
@@ -697,230 +698,6 @@
shows "<t, []> \<mapsto>* <t', []>"
using a eval_implies_machines_ctx by simp
-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. Freshness 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
- * (x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) and
- ** valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)) *}
- have *: "(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 **: "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 stron 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 {* Function Definitions: Filling a Lambda-Term into a Context *}
@@ -1003,8 +780,7 @@
shows "E \<odot> \<box> = E"
by (induct E) (simp_all)
-lemma odot_assoc:
- fixes E1 E2 E3::"ctx"
+lemma odot_assoc: (* fixme call compose *)
shows "(E1 \<odot> E2) \<odot> E3 = E1 \<odot> (E2 \<odot> E3)"
by (induct E1) (simp_all)
@@ -1114,7 +890,6 @@
(auto simp add: lam.fresh fresh_at_base)
lemma fresh_fact:
- fixes z::"name"
assumes a: "atom z \<sharp> s"
and b: "z = y \<or> atom z \<sharp> t"
shows "atom z \<sharp> t[y ::= s]"
--- /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
--- a/Tutorial/Tutorial4.thy Fri Jan 21 00:55:28 2011 +0100
+++ b/Tutorial/Tutorial4.thy Fri Jan 21 21:58:51 2011 +0100
@@ -1,6 +1,5 @@
-
theory Tutorial4
-imports Tutorial1
+imports Tutorial1 Tutorial2
begin
section {* The CBV Reduction Relation (Small-Step Semantics) *}
@@ -136,22 +135,28 @@
lemma machines_implies_cbvs_ctx:
assumes a: "<e, Es> \<mapsto>* <e', Es'>"
shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
-using a
-by (induct) (auto dest: machine_implies_cbvs_ctx)
+using a machine_implies_cbvs_ctx
+by (induct) (blast)+
text {*
So whenever we let the CL machine start in an initial
state and it arrives at a final state, then there exists
- a corresponding cbv-reduction sequence. *}
+ a corresponding cbv-reduction sequence.
+*}
corollary machines_implies_cbvs:
assumes a: "<e, []> \<mapsto>* <e', []>"
shows "e \<longrightarrow>cbv* e'"
-using a by (auto dest: machines_implies_cbvs_ctx)
+proof -
+ have "[]\<down>\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* []\<down>\<lbrakk>e'\<rbrakk>"
+ using a machines_implies_cbvs_ctx by blast
+ then show "e \<longrightarrow>cbv* e'" by simp
+qed
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 two auxiliary lemmas.
+*}
lemma eval_val:
assumes a: "val t"
@@ -160,16 +165,15 @@
lemma e_App_elim:
assumes a: "App t1 t2 \<Down> v"
- shows "\<exists>x t v'. t1 \<Down> Lam [x].t \<and> t2 \<Down> v' \<and> t[x::=v'] \<Down> v"
+ obtains x t v' where "t1 \<Down> Lam [x].t" "t2 \<Down> v'" "t[x::=v'] \<Down> v"
using a by (cases) (auto simp add: lam.eq_iff lam.distinct)
-text {******************************************************************
-
- 10.) Exercise
- -------------
+
+subsection {* EXERCISE *}
- Complete the first case in the proof below.
-
+text {*
+ Complete the first and second case in the
+ proof below.
*}
lemma cbv_eval:
@@ -180,8 +184,9 @@
case (cbv1 v x t t3)
have a1: "val v" by fact
have a2: "t[x ::= v] \<Down> t3" by fact
-
- show "App (Lam [x].t) v \<Down> t3" sorry
+ 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
next
case (cbv2 t t' t2 t3)
have ih: "\<And>t3. t' \<Down> t3 \<Longrightarrow> t \<Down> t3" by fact
@@ -189,10 +194,10 @@
then obtain x t'' v'
where a1: "t' \<Down> Lam [x].t''"
and a2: "t2 \<Down> v'"
- and a3: "t''[x ::= v'] \<Down> t3" using e_App_elim by blast
+ 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
-qed (auto dest!: e_App_elim)
+qed (auto elim!: e_App_elim)
text {*
@@ -206,7 +211,8 @@
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. *}
+ by a cbv-reduction sequence, then t evaluates to this value.
+*}
lemma cbvs_implies_eval:
assumes a: "t \<longrightarrow>cbv* v" "val v"
@@ -216,15 +222,16 @@
text {*
All facts tied together give us the desired property about
- K machines. *}
+ machines.
+*}
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 by (simp add: machines_implies_cbvs)
- then show "t1 \<Down> t2" using b by (simp add: cbvs_implies_eval)
+ have "t1 \<longrightarrow>cbv* t2" using a machines_implies_cbvs by simp
+ then show "t1 \<Down> t2" using b cbvs_implies_eval by simp
qed
lemma valid_elim:
@@ -252,9 +259,9 @@
by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)
lemma type_substitution_aux:
- assumes a: "(\<Delta> @ [(x, T')] @ \<Gamma>) \<turnstile> e : T"
+ assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T"
and b: "\<Gamma> \<turnstile> e' : T'"
- shows "(\<Delta> @ \<Gamma>) \<turnstile> e[x ::= e'] : T"
+ shows "\<Delta> @ \<Gamma> \<turnstile> e[x ::= e'] : T"
using a b
proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
case (t_Var y T x e' \<Delta>)
@@ -264,40 +271,42 @@
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)
+ with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using eq a4 by (auto intro: weakening)
}
moreover
{ assume ineq: "x \<noteq> y"
from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp
- then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" using ineq a4 by auto
+ 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)+
corollary type_substitution:
- assumes a: "(x,T') # \<Gamma> \<turnstile> e : T"
+ assumes a: "(x, T') # \<Gamma> \<turnstile> e : T"
and b: "\<Gamma> \<turnstile> e' : T'"
- shows "\<Gamma> \<turnstile> e[x::=e'] : T"
+ shows "\<Gamma> \<turnstile> e[x ::= e'] : T"
using a b type_substitution_aux[where \<Delta>="[]"]
-by (auto)
+by auto
lemma t_App_elim:
assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"
- shows "\<exists>T'. \<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<and> \<Gamma> \<turnstile> t2 : T'"
+ obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" "\<Gamma> \<turnstile> t2 : T'"
using a
by (cases) (auto simp add: lam.eq_iff lam.distinct)
+text {* we have not yet generated strong elimination rules *}
lemma t_Lam_elim:
assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T"
and fc: "atom x \<sharp> \<Gamma>"
- shows "\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> (x, T1) # \<Gamma> \<turnstile> t : T2"
+ obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2"
using ty fc
apply(cases)
apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)
apply(auto simp add: Abs1_eq_iff)
-apply(rule_tac p="(x \<leftrightarrow> xa)" in permute_boolE)
+apply(rotate_tac 3)
+apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)
apply(perm_simp)
-apply(simp add: flip_def swap_fresh_fresh ty_fresh)
+apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)
done
theorem cbv_type_preservation:
@@ -306,7 +315,7 @@
shows "\<Gamma> \<turnstile> t' : T"
using a b
by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)
- (auto dest!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)
+ (auto elim!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)
corollary cbvs_type_preservation:
assumes a: "t \<longrightarrow>cbv* t'"
@@ -316,15 +325,17 @@
by (induct) (auto intro: cbv_type_preservation)
text {*
- The Type-Preservation Property for the Machine and Evaluation Relation. *}
+ The type-preservation property for the machine and
+ evaluation relation.
+*}
theorem machine_type_preservation:
assumes a: "<t, []> \<mapsto>* <t', []>"
and b: "\<Gamma> \<turnstile> t : T"
shows "\<Gamma> \<turnstile> t' : T"
proof -
- from a have "t \<longrightarrow>cbv* t'" by (simp add: machines_implies_cbvs)
- then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: cbvs_type_preservation)
+ have "t \<longrightarrow>cbv* t'" using a machines_implies_cbvs by simp
+ then show "\<Gamma> \<turnstile> t' : T" using b cbvs_type_preservation by simp
qed
theorem eval_type_preservation:
@@ -332,8 +343,8 @@
and b: "\<Gamma> \<turnstile> t : T"
shows "\<Gamma> \<turnstile> t' : T"
proof -
- from a have "<t, []> \<mapsto>* <t', []>" by (simp add: eval_implies_machines)
- then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation)
+ have "<t, []> \<mapsto>* <t', []>" using a eval_implies_machines by simp
+ then show "\<Gamma> \<turnstile> t' : T" using b machine_type_preservation by simp
qed
text {* The Progress Property *}
@@ -341,7 +352,7 @@
lemma canonical_tArr:
assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"
and b: "val t"
- shows "\<exists>x t'. t = Lam [x].t'"
+ obtains x t' where "t = Lam [x].t'"
using b a by (induct) (auto)
theorem progress:
@@ -349,6 +360,11 @@
shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"
using a
by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)
- (auto intro: cbv.intros dest!: canonical_tArr)
+ (auto elim: canonical_tArr)
+text {*
+ Done!
+*}
+end
+