theory Weakening
imports "HOL-Nominal.Nominal"
begin
text \<open>
A simple proof of the Weakening Property in the simply-typed
lambda-calculus. The proof is simple, because we can make use
of the variable convention.\<close>
atom_decl name
text \<open>Terms and Types\<close>
nominal_datatype lam =
Var "name"
| App "lam" "lam"
| Lam "\name\lam" ("Lam [_]._" [100,100] 100)
nominal_datatype ty =
TVar "string"
| TArr "ty" "ty" ("_ \ _" [100,100] 100)
lemma ty_fresh:
fixes x::"name"
and T::"ty"
shows "x\T"
by (nominal_induct T rule: ty.strong_induct)
(auto simp add: fresh_string)
text \<open>
Valid contexts (at the moment we have no type for finite
sets yet, therefore typing-contexts are lists).\<close>
inductive
valid :: "(name\ty) list \ bool"
where
v1[intro]: "valid []"
| v2[intro]: "\valid \;x\\\\ valid ((x,T)#\)"
equivariance valid
text\<open>Typing judgements\<close>
inductive
typing :: "(name\ty) list\lam\ty\bool" ("_ \ _ : _" [60,60,60] 60)
where
t_Var[intro]: "\valid \; (x,T)\set \\ \ \ \ Var x : T"
| t_App[intro]: "\\ \ t1 : T1\T2; \ \ t2 : T1\ \ \ \ App t1 t2 : T2"
| t_Lam[intro]: "\x\\;(x,T1)#\ \ t : T2\ \ \ \ Lam [x].t : T1\T2"
text \<open>
We derive the strong induction principle for the typing
relation (this induction principle has the variable convention
already built-in).\<close>
equivariance typing
nominal_inductive typing
by (simp_all add: abs_fresh ty_fresh)
text \<open>Abbreviation for the notion of subcontexts.\<close>
abbreviation
"sub_context" :: "(name\ty) list \ (name\ty) list \ bool" ("_ \ _" [60,60] 60)
where
"\1 \ \2 \ \x T. (x,T)\set \1 \ (x,T)\set \2"
text \<open>Now it comes: The Weakening Lemma\<close>
text \<open>
The first version is, after setting up the induction,
completely automatic except for use of atomize.\<close>
lemma weakening_version1:
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
assumes a: "\1 \ t : T"
and b: "valid \2"
and c: "\1 \ \2"
shows "\2 \ t : T"
using a b c
by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
(auto | atomize)+
text \<open>
The second version gives the details for the variable
and lambda case.\<close>
lemma weakening_version2:
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
and t ::"lam"
and \<tau> ::"ty"
assumes a: "\1 \ t : T"
and b: "valid \2"
and c: "\1 \ \2"
shows "\2 \ t : T"
using a b c
proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
case (t_Var \<Gamma>1 x T) (* variable case *)
have "\1 \ \2" by fact
moreover
have "valid \2" by fact
moreover
have "(x,T)\ set \1" by fact
ultimately show "\2 \ Var x : T" by auto
next
case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
have vc: "x\\2" by fact (* variable convention *)
have ih: "\valid ((x,T1)#\2); (x,T1)#\1 \ (x,T1)#\2\ \ (x,T1)#\2 \ t:T2" by fact
have "\1 \ \2" by fact
then have "(x,T1)#\1 \ (x,T1)#\2" by simp
moreover
have "valid \2" by fact
then have "valid ((x,T1)#\2)" using vc by (simp add: v2)
ultimately have "(x,T1)#\2 \ t : T2" using ih by simp
with vc show "\2 \ Lam [x].t : T1\T2" by auto
qed (auto) (* app case *)
text\<open>
The original induction principle for the typing relation
is not strong enough - even this simple lemma fails to be
simple ;o)\<close>
lemma weakening_not_straigh_forward:
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
assumes a: "\1 \ t : T"
and b: "valid \2"
and c: "\1 \ \2"
shows "\2 \ t : T"
using a b c
proof (induct arbitrary: \<Gamma>2)
case (t_Var \<Gamma>1 x T) (* variable case still works *)
have "\1 \ \2" by fact
moreover
have "valid \2" by fact
moreover
have "(x,T) \ (set \1)" by fact
ultimately show "\2 \ Var x : T" by auto
next
case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
(* These are all assumptions available in this case*)
have a0: "x\\1" by fact
have a1: "(x,T1)#\1 \ t : T2" by fact
have a2: "\1 \ \2" by fact
have a3: "valid \2" by fact
have ih: "\\3. \valid \3; (x,T1)#\1 \ \3\ \ \3 \ t : T2" by fact
have "(x,T1)#\1 \ (x,T1)#\2" using a2 by simp
moreover
have "valid ((x,T1)#\2)" using v2 (* fails *)
oops
text\<open>
To show that the proof with explicit renaming is not simple,
here is the proof without using the variable convention. It
crucially depends on the equivariance property of the typing
relation.
\<close>
lemma weakening_with_explicit_renaming:
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
assumes a: "\1 \ t : T"
and b: "valid \2"
and c: "\1 \ \2"
shows "\2 \ t : T"
using a b c
proof (induct arbitrary: \<Gamma>2)
case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
have fc0: "x\\1" by fact
have ih: "\\3. \valid \3; (x,T1)#\1 \ \3\ \ \3 \ t : T2" by fact
obtain c::"name" where fc1: "c\(x,t,\1,\2)" (* we obtain a fresh name *)
by (rule exists_fresh) (auto simp add: fs_name1)
have "Lam [c].([(c,x)]\t) = Lam [x].t" using fc1 (* we then alpha-rename the lambda-abstraction *)
by (auto simp add: lam.inject alpha fresh_prod fresh_atm)
moreover
have "\2 \ Lam [c].([(c,x)]\t) : T1 \ T2" (* we can then alpha-rename our original goal *)
proof -
(* we establish (x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2) and valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2)) *)
have "(x,T1)#\1 \ (x,T1)#([(c,x)]\\2)"
proof -
have "\1 \ \2" by fact
then have "[(c,x)]\((x,T1)#\1 \ (x,T1)#([(c,x)]\\2))" using fc0 fc1
by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
then show "(x,T1)#\1 \ (x,T1)#([(c,x)]\\2)" by (rule perm_boolE)
qed
moreover
have "valid ((x,T1)#([(c,x)]\\2))"
proof -
have "valid \2" by fact
then show "valid ((x,T1)#([(c,x)]\\2))" using fc1
by (auto intro!: v2 simp add: fresh_left calc_atm eqvts)
qed
(* these two facts give us by induction hypothesis the following *)
ultimately have "(x,T1)#([(c,x)]\\2) \ t : T2" using ih by simp
(* we now apply renamings to get to our goal *)
then have "[(c,x)]\((x,T1)#([(c,x)]\\2) \ t : T2)" by (rule perm_boolI)
then have "(c,T1)#\2 \ ([(c,x)]\t) : T2" using fc1
by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
then show "\2 \ Lam [c].([(c,x)]\t) : T1 \ T2" using fc1 by auto
qed
ultimately show "\2 \ Lam [x].t : T1 \ T2" by simp
qed (auto) (* var and app cases *)
text \<open>
Moral: compare the proof with explicit renamings to weakening_version1
and weakening_version2, and imagine you are proving something more substantial
than the weakening lemma.\<close>
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
