--- a/src/HOL/Nominal/Examples/Contexts.thy Thu Dec 20 00:19:40 2007 +0100
+++ b/src/HOL/Nominal/Examples/Contexts.thy Thu Dec 20 01:07:21 2007 +0100
@@ -1,4 +1,4 @@
-(* $Id: *)
+(* $Id$ *)
theory Contexts
imports "../Nominal"
@@ -19,20 +19,18 @@
atom_decl name
-text {* terms *}
-
+text {* Terms *}
nominal_datatype lam =
Var "name"
| App "lam" "lam"
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
-text {* contexts - the context-lambda does not bind anything *}
-
+text {* Contexts - the lambda case in contexts does not bind a name *}
nominal_datatype ctx =
Hole
| CAppL "ctx" "lam"
| CAppR "lam" "ctx"
- | CLam "name" "ctx" ("CLam [_]._" [100,100] 100)
+ | CLam "name" "ctx" ("CLam [_]._" [100,100] 100)
text {* Capture-avoiding substitution and three lemmas *}
@@ -61,17 +59,10 @@
by (nominal_induct t avoiding: x y t' rule: lam.inducts)
(auto simp add: abs_fresh fresh_prod fresh_atm)
-lemma subst_swap:
- fixes x y::"name"
- and t t'::"lam"
- shows "y\<sharp>t \<Longrightarrow> ([(y,x)]\<bullet>t)[y::=t'] = t[x::=t']"
-by (nominal_induct t avoiding: x y t' rule: lam.inducts)
- (auto simp add: lam.inject calc_atm fresh_atm abs_fresh)
-
text {*
- The operation that fills one term into a hole. While
- contexts are not alpha-equivalence classes, the filling
- operation produces an alpha-equivalent lambda-term.
+ Replace is the operation that fills a term into a hole. While
+ contexts themselves are not alpha-equivalence classes, the
+ filling operation produces an alpha-equivalent lambda-term.
*}
consts
@@ -81,13 +72,15 @@
"Hole<t> = t"
"(CAppL E t')<t> = App (E<t>) t'"
"(CAppR t' E)<t> = App t' (E<t>)"
- "(CLam [x].E)<t> = Lam [x].(E<t>)"
+ "(CLam [x].E)<t> = Lam [x].(E<t>)"
by (rule TrueI)+
+
lemma alpha_test:
shows "(CLam [x].Hole)<Var x> = (CLam [y].Hole)<Var y>"
by (auto simp add: alpha lam.inject calc_atm fresh_atm)
+
lemma replace_eqvt[eqvt]:
fixes pi:: "name prm"
shows "pi\<bullet>(E<e>) = (pi\<bullet>E)<(pi\<bullet>e)>"
@@ -101,7 +94,8 @@
by (induct E rule: ctx.weak_induct)
(auto simp add: fresh_prod abs_fresh)
-text {* composition of two contexts *}
+
+text {* Composition of two contexts *}
consts
ctx_replace :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _" [100,100] 100)
@@ -124,7 +118,7 @@
by (induct E1 rule: ctx.weak_induct)
(auto simp add: fresh_prod)
-text {* beta-reduction via contexts *}
+text {* Beta-reduction via contexts *}
inductive
ctx_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>x _" [80,80] 80)
@@ -136,7 +130,7 @@
nominal_inductive ctx_red
by (simp_all add: replace_fresh subst_fresh abs_fresh)
-text {* beta-reduction via congruence rules *}
+text {* Beta-reduction via congruence rules *}
inductive
cong_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>o _" [80,80] 80)
@@ -151,7 +145,7 @@
nominal_inductive cong_red
by (simp_all add: subst_fresh abs_fresh)
-text {* the proof that shows both relations are equal *}
+text {* The proof that shows both relations are equal *}
lemma cong_red_ctx:
assumes a: "t \<longrightarrow>o t'"
--- a/src/HOL/Nominal/Examples/ROOT.ML Thu Dec 20 00:19:40 2007 +0100
+++ b/src/HOL/Nominal/Examples/ROOT.ML Thu Dec 20 01:07:21 2007 +0100
@@ -18,7 +18,8 @@
"Crary",
"SOS",
"LocalWeakening",
- "Support"
+ "Support",
+ "Contexts"
];
-setmp quick_and_dirty true use_thy "VC_Compatible";
\ No newline at end of file
+setmp quick_and_dirty true use_thy "VC_Condition";
\ No newline at end of file
--- a/src/HOL/Nominal/Examples/VC_Compatible.thy Thu Dec 20 00:19:40 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,184 +0,0 @@
-(* $Id$ *)
-
-theory VC_Compatible
-imports "../Nominal"
-begin
-
-text {*
- We give here two examples that show if we use the variable
- convention carelessly in rule inductions, we might end
- up with faulty lemmas. The point is that the examples
- are not variable-convention compatible and therefore in the
- nominal package one is protected from such bogus reasoning.
-*}
-
-text {*
- We define alpha-equated lambda-terms as usual. *}
-atom_decl name
-
-nominal_datatype lam =
- Var "name"
- | App "lam" "lam"
- | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
-
-text {*
- The inductive relation 'unbind' unbinds the top-most
- binders of a lambda-term; this relation is obviously
- not a function, since it does not respect alpha-
- equivalence. However as a relation 'unbind' is ok and
- a similar relation has been used in our formalisation
- of the algorithm W. *}
-inductive
- unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60)
-where
- u_var: "(Var a) \<mapsto> [],(Var a)"
-| u_app: "(App t1 t2) \<mapsto> [],(App t1 t2)"
-| u_lam: "t\<mapsto>xs,t' \<Longrightarrow> (Lam [x].t) \<mapsto> (x#xs),t'"
-
-text {*
- We can show that Lam [x].Lam [x].Var x unbinds to [x,x],Var x
- and also to [z,y],Var y (though the proof for the second is a
- bit clumsy). *}
-lemma unbind_lambda_lambda1:
- shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
-by (auto intro: unbind.intros)
-
-lemma unbind_lambda_lambda2:
- shows "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)"
-proof -
- have "Lam [x].Lam [x].(Var x) = Lam [y].Lam [z].(Var z)"
- by (auto simp add: lam.inject alpha calc_atm abs_fresh fresh_atm)
- moreover
- have "Lam [y].Lam [z].(Var z) \<mapsto> [y,z],(Var z)"
- by (auto intro: unbind.intros)
- ultimately
- show "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" by simp
-qed
-
-text {* Unbind is equivariant ...*}
-equivariance unbind
-
-text {*
- ... but it is not variable-convention compatible (see Urban,
- Berghofer, Norrish [2007] for more details). This condition
- requires for rule u_lam to have the binder x being not a free variable
- in the rule's conclusion. Because this condition is not satisfied,
- Isabelle will not derive a strong induction principle for 'unbind'
- - that means Isabelle does not allow us to use the variable
- convention in induction proofs over 'unbind'. We can, however,
- force Isabelle to derive the strengthening induction principle
- and see what happens. *}
-
-nominal_inductive unbind
- sorry
-
-text {*
- To obtain a faulty lemma, we introduce the function 'bind'
- which takes a list of names and abstracts away these names in
- a given lambda-term. *}
-fun
- bind :: "name list \<Rightarrow> lam \<Rightarrow> lam"
-where
- "bind [] t = t"
-| "bind (x#xs) t = Lam [x].(bind xs t)"
-
-text {*
- Although not necessary for our main argument below, we can
- easily prove that bind undoes the unbinding. *}
-lemma bind_unbind:
- assumes a: "t \<mapsto> xs,t'"
- shows "t = bind xs t'"
-using a by (induct) (auto)
-
-text {*
- The next lemma shows by induction on xs that if x is a free
- variable in t and x does not occur in xs, then x is a free
- variable in bind xs t. In the nominal tradition we formulate
- 'is a free variable in' as 'is not fresh for'. *}
-lemma free_variable:
- fixes x::"name"
- assumes a: "\<not>(x\<sharp>t)" and b: "x\<sharp>xs"
- shows "\<not>(x\<sharp>bind xs t)"
-using a b
-by (induct xs)
- (auto simp add: fresh_list_cons abs_fresh fresh_atm)
-
-text {*
- Now comes the faulty lemma. It is derived using the
- variable convention (i.e. our strong induction principle).
- This faulty lemma states that if t unbinds to x::xs and t',
- and x is a free variable in t', then it is also a free
- variable in bind xs t'. We show this lemma by assuming that
- the binder x is fresh w.r.t. to the xs unbound previously. *}
-
-lemma faulty1:
- assumes a: "t\<mapsto>(x#xs),t'"
- shows "\<not>(x\<sharp>t') \<Longrightarrow> \<not>(x\<sharp>bind xs t')"
-using a
-by (nominal_induct t xs'\<equiv>"x#xs" t' avoiding: xs rule: unbind.strong_induct)
- (simp_all add: free_variable)
-
-text {*
- Obviously the faulty lemma does not hold, for example, in
- case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). Therefore,
- we can prove False. *}
-
-lemma false1:
- shows "False"
-proof -
- have "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
- and "\<not>(x\<sharp>Var x)" by (simp_all add: unbind_lambda_lambda1 fresh_atm)
- then have "\<not>(x\<sharp>(bind [x] (Var x)))" by (rule faulty1)
- moreover
- have "x\<sharp>(bind [x] (Var x))" by (simp add: abs_fresh)
- ultimately
- show "False" by simp
-qed
-
-text {*
- The next example is slightly simpler, but looks more
- contrived than 'unbind'. This example, caled 'strip' just
- strips off the top-most binders from lambdas. *}
-
-inductive
- strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60)
-where
- s_var: "(Var a) \<rightarrow> (Var a)"
-| s_app: "(App t1 t2) \<rightarrow> (App t1 t2)"
-| s_lam: "t \<rightarrow> t' \<Longrightarrow> (Lam [x].t) \<rightarrow> t'"
-
-text {*
- The relation is equivariant but we have to use again
- sorry to derive a strong induction principle. *}
-
-equivariance strip
-
-nominal_inductive strip
- sorry
-
-text {*
- The faulty lemma shows that a variable that is fresh
- for a term is also fresh for the term after striping. *}
-
-lemma faulty2:
- fixes x::"name"
- assumes a: "t \<rightarrow> t'"
- shows "x\<sharp>t \<Longrightarrow> x\<sharp>t'"
-using a
-by (nominal_induct t t'\<equiv>t' avoiding: t' rule: strip.strong_induct)
- (auto simp add: abs_fresh)
-
-text {*
- Obviously Lam [x].Var x is a counter example to this lemma. *}
-
-lemma false2:
- shows "False"
-proof -
- have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros)
- moreover
- have "x\<sharp>Lam [x].(Var x)" by (simp add: abs_fresh)
- ultimately have "x\<sharp>(Var x)" by (simp only: faulty2)
- then show "False" by (simp add: fresh_atm)
-qed
-
-end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy Thu Dec 20 01:07:21 2007 +0100
@@ -0,0 +1,184 @@
+(* $Id$ *)
+
+theory VC_Compatible
+imports "../Nominal"
+begin
+
+text {*
+ We give here two examples that show if we use the variable
+ convention carelessly in rule inductions, we might end
+ up with faulty lemmas. The point is that the examples
+ are not variable-convention compatible and therefore in the
+ nominal package one is protected from such bogus reasoning.
+*}
+
+text {*
+ We define alpha-equated lambda-terms as usual. *}
+atom_decl name
+
+nominal_datatype lam =
+ Var "name"
+ | App "lam" "lam"
+ | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
+
+text {*
+ The inductive relation 'unbind' unbinds the top-most
+ binders of a lambda-term; this relation is obviously
+ not a function, since it does not respect alpha-
+ equivalence. However as a relation 'unbind' is ok and
+ a similar relation has been used in our formalisation
+ of the algorithm W. *}
+inductive
+ unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60)
+where
+ u_var: "(Var a) \<mapsto> [],(Var a)"
+| u_app: "(App t1 t2) \<mapsto> [],(App t1 t2)"
+| u_lam: "t\<mapsto>xs,t' \<Longrightarrow> (Lam [x].t) \<mapsto> (x#xs),t'"
+
+text {*
+ We can show that Lam [x].Lam [x].Var x unbinds to [x,x],Var x
+ and also to [z,y],Var y (though the proof for the second is a
+ bit clumsy). *}
+lemma unbind_lambda_lambda1:
+ shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
+by (auto intro: unbind.intros)
+
+lemma unbind_lambda_lambda2:
+ shows "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)"
+proof -
+ have "Lam [x].Lam [x].(Var x) = Lam [y].Lam [z].(Var z)"
+ by (auto simp add: lam.inject alpha calc_atm abs_fresh fresh_atm)
+ moreover
+ have "Lam [y].Lam [z].(Var z) \<mapsto> [y,z],(Var z)"
+ by (auto intro: unbind.intros)
+ ultimately
+ show "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" by simp
+qed
+
+text {* Unbind is equivariant ...*}
+equivariance unbind
+
+text {*
+ ... but it is not variable-convention compatible (see Urban,
+ Berghofer, Norrish [2007] for more details). This condition
+ requires for rule u_lam to have the binder x being not a free variable
+ in the rule's conclusion. Because this condition is not satisfied,
+ Isabelle will not derive a strong induction principle for 'unbind'
+ - that means Isabelle does not allow us to use the variable
+ convention in induction proofs over 'unbind'. We can, however,
+ force Isabelle to derive the strengthening induction principle
+ and see what happens. *}
+
+nominal_inductive unbind
+ sorry
+
+text {*
+ To obtain a faulty lemma, we introduce the function 'bind'
+ which takes a list of names and abstracts away these names in
+ a given lambda-term. *}
+fun
+ bind :: "name list \<Rightarrow> lam \<Rightarrow> lam"
+where
+ "bind [] t = t"
+| "bind (x#xs) t = Lam [x].(bind xs t)"
+
+text {*
+ Although not necessary for our main argument below, we can
+ easily prove that bind undoes the unbinding. *}
+lemma bind_unbind:
+ assumes a: "t \<mapsto> xs,t'"
+ shows "t = bind xs t'"
+using a by (induct) (auto)
+
+text {*
+ The next lemma shows by induction on xs that if x is a free
+ variable in t and x does not occur in xs, then x is a free
+ variable in bind xs t. In the nominal tradition we formulate
+ 'is a free variable in' as 'is not fresh for'. *}
+lemma free_variable:
+ fixes x::"name"
+ assumes a: "\<not>(x\<sharp>t)" and b: "x\<sharp>xs"
+ shows "\<not>(x\<sharp>bind xs t)"
+using a b
+by (induct xs)
+ (auto simp add: fresh_list_cons abs_fresh fresh_atm)
+
+text {*
+ Now comes the faulty lemma. It is derived using the
+ variable convention (i.e. our strong induction principle).
+ This faulty lemma states that if t unbinds to x::xs and t',
+ and x is a free variable in t', then it is also a free
+ variable in bind xs t'. We show this lemma by assuming that
+ the binder x is fresh w.r.t. to the xs unbound previously. *}
+
+lemma faulty1:
+ assumes a: "t\<mapsto>(x#xs),t'"
+ shows "\<not>(x\<sharp>t') \<Longrightarrow> \<not>(x\<sharp>bind xs t')"
+using a
+by (nominal_induct t xs'\<equiv>"x#xs" t' avoiding: xs rule: unbind.strong_induct)
+ (simp_all add: free_variable)
+
+text {*
+ Obviously the faulty lemma does not hold, for example, in
+ case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). Therefore,
+ we can prove False. *}
+
+lemma false1:
+ shows "False"
+proof -
+ have "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
+ and "\<not>(x\<sharp>Var x)" by (simp_all add: unbind_lambda_lambda1 fresh_atm)
+ then have "\<not>(x\<sharp>(bind [x] (Var x)))" by (rule faulty1)
+ moreover
+ have "x\<sharp>(bind [x] (Var x))" by (simp add: abs_fresh)
+ ultimately
+ show "False" by simp
+qed
+
+text {*
+ The next example is slightly simpler, but looks more
+ contrived than 'unbind'. This example, caled 'strip' just
+ strips off the top-most binders from lambdas. *}
+
+inductive
+ strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60)
+where
+ s_var: "(Var a) \<rightarrow> (Var a)"
+| s_app: "(App t1 t2) \<rightarrow> (App t1 t2)"
+| s_lam: "t \<rightarrow> t' \<Longrightarrow> (Lam [x].t) \<rightarrow> t'"
+
+text {*
+ The relation is equivariant but we have to use again
+ sorry to derive a strong induction principle. *}
+
+equivariance strip
+
+nominal_inductive strip
+ sorry
+
+text {*
+ The faulty lemma shows that a variable that is fresh
+ for a term is also fresh for the term after striping. *}
+
+lemma faulty2:
+ fixes x::"name"
+ assumes a: "t \<rightarrow> t'"
+ shows "x\<sharp>t \<Longrightarrow> x\<sharp>t'"
+using a
+by (nominal_induct t t'\<equiv>t' avoiding: t' rule: strip.strong_induct)
+ (auto simp add: abs_fresh)
+
+text {*
+ Obviously Lam [x].Var x is a counter example to this lemma. *}
+
+lemma false2:
+ shows "False"
+proof -
+ have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros)
+ moreover
+ have "x\<sharp>Lam [x].(Var x)" by (simp add: abs_fresh)
+ ultimately have "x\<sharp>(Var x)" by (simp only: faulty2)
+ then show "False" by (simp add: fresh_atm)
+qed
+
+end
\ No newline at end of file
--- a/src/HOL/Nominal/Examples/Weakening.thy Thu Dec 20 00:19:40 2007 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy Thu Dec 20 01:07:21 2007 +0100
@@ -1,11 +1,10 @@
(* $Id$ *)
theory Weakening
-imports "../Nominal"
+ imports "../Nominal"
begin
section {* Weakening Example for the Simply-Typed Lambda-Calculus *}
-(*================================================================*)
atom_decl name
@@ -28,7 +27,8 @@
text {*
Valid contexts (at the moment we have no type for finite
- sets yet; therefore typing-contexts are lists). *}
+ sets yet; therefore typing-contexts are lists).
+ *}
inductive
valid :: "(name\<times>ty) list \<Rightarrow> bool"
where
@@ -46,9 +46,10 @@
| t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2"
text {*
- We automatically derive the strong induction principle
- for the typing relation (this induction principle has the
- variable convention already built in). *}
+ We derive the strong induction principle for the typing
+ relation (this induction principle has the variable convention
+ already built in).
+ *}
equivariance typing
nominal_inductive typing
by (simp_all add: abs_fresh ty_fresh)
@@ -60,11 +61,11 @@
"\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2"
text {* Now it comes: The Weakening Lemma *}
-(*========================================*)
text {*
The first version is, after setting up the induction,
- quite automatic except for use of atomize. *}
+ completely automatic except for use of atomize.
+ *}
lemma weakening_version1:
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
assumes a: "\<Gamma>1 \<turnstile> t : T"
@@ -77,7 +78,8 @@
text {*
The second version gives all details for the variable
- and lambda case. *}
+ and lambda case.
+ *}
lemma weakening_version2:
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
and t ::"lam"
@@ -111,7 +113,8 @@
text{*
The original induction principle for the typing relation
is not strong enough - even this simple lemma fails to be
- simple ;o) *}
+ simple ;o)
+ *}
lemma weakening_not_straigh_forward:
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
assumes a: "\<Gamma>1 \<turnstile> t : T"
@@ -140,8 +143,7 @@
have "valid ((x,T1)#\<Gamma>2)" using v2 (* fails *)
oops
-text{*
- The complete proof without using the variable convention. *}
+text{* The complete proof without using the variable convention. *}
lemma weakening_with_explicit_renaming:
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
assumes a: "\<Gamma>1 \<turnstile> t : T"
@@ -189,6 +191,7 @@
text {*
Compare the proof with explicit renamings to version1 and version2,
and imagine you are proving something more substantial than the
- weakening lemma. *}
+ weakening lemma.
+ *}
end
\ No newline at end of file