1theory Weakening 
2  imports "HOL-Nominal.Nominal" 
3begin
4
5text \<open>
6  A simple proof of the Weakening Property in the simply-typed 
7  lambda-calculus. The proof is simple, because we can make use
8  of the variable convention.\<close>
9
10atom_decl name 
11
12text \<open>Terms and Types\<close>
13
14nominal_datatype lam = 
15    Var "name"
16  | App "lam" "lam"
17  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
18
19nominal_datatype ty =
20    TVar "string"
21  | TArr "ty" "ty" ("_ \<rightarrow> _" [100,100] 100)
22
23lemma ty_fresh:
24  fixes x::"name"
25  and   T::"ty"
26  shows "x\<sharp>T"
27by (nominal_induct T rule: ty.strong_induct)
28   (auto simp add: fresh_string)
29
30text \<open>
31  Valid contexts (at the moment we have no type for finite 
32  sets yet, therefore typing-contexts are lists).\<close>
33
34inductive
35  valid :: "(name\<times>ty) list \<Rightarrow> bool"
36where
37    v1[intro]: "valid []"
38  | v2[intro]: "\<lbrakk>valid \<Gamma>;x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,T)#\<Gamma>)"
39
40equivariance valid
41
42text\<open>Typing judgements\<close>
43
44inductive
45  typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
46where
47    t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
48  | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
49  | t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2"
50
51text \<open>
52  We derive the strong induction principle for the typing 
53  relation (this induction principle has the variable convention 
54  already built-in).\<close>
55
56equivariance typing
57nominal_inductive typing
58  by (simp_all add: abs_fresh ty_fresh)
59
60text \<open>Abbreviation for the notion of subcontexts.\<close>
61
62abbreviation
63  "sub_context" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) 
64where
65  "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2"
66
67text \<open>Now it comes: The Weakening Lemma\<close>
68
69text \<open>
70  The first version is, after setting up the induction, 
71  completely automatic except for use of atomize.\<close>
72
73lemma weakening_version1: 
74  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
75  assumes a: "\<Gamma>1 \<turnstile> t : T" 
76  and     b: "valid \<Gamma>2" 
77  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
78  shows "\<Gamma>2 \<turnstile> t : T"
79using a b c
80by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
81   (auto | atomize)+
82
83text \<open>
84  The second version gives the details for the variable
85  and lambda case.\<close>
86
87lemma weakening_version2: 
88  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
89  and   t ::"lam"
90  and   \<tau> ::"ty"
91  assumes a: "\<Gamma>1 \<turnstile> t : T"
92  and     b: "valid \<Gamma>2" 
93  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
94  shows "\<Gamma>2 \<turnstile> t : T"
95using a b c
96proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
97  case (t_Var \<Gamma>1 x T)  (* variable case *)
98  have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 
99  moreover  
100  have "valid \<Gamma>2" by fact 
101  moreover 
102  have "(x,T)\<in> set \<Gamma>1" by fact
103  ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto
104next
105  case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
106  have vc: "x\<sharp>\<Gamma>2" by fact   (* variable convention *)
107  have ih: "\<lbrakk>valid ((x,T1)#\<Gamma>2); (x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2\<rbrakk> \<Longrightarrow> (x,T1)#\<Gamma>2 \<turnstile> t:T2" by fact
108  have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
109  then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp
110  moreover
111  have "valid \<Gamma>2" by fact
112  then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2)
113  ultimately have "(x,T1)#\<Gamma>2 \<turnstile> t : T2" using ih by simp
114  with vc show "\<Gamma>2 \<turnstile> Lam [x].t : T1\<rightarrow>T2" by auto
115qed (auto) (* app case *)
116
117text\<open>
118  The original induction principle for the typing relation
119  is not strong enough - even this simple lemma fails to be 
120  simple ;o)\<close>
121
122lemma weakening_not_straigh_forward: 
123  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
124  assumes a: "\<Gamma>1 \<turnstile> t : T"
125  and     b: "valid \<Gamma>2" 
126  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
127  shows "\<Gamma>2 \<turnstile> t : T"
128using a b c
129proof (induct arbitrary: \<Gamma>2)
130  case (t_Var \<Gamma>1 x T) (* variable case still works *)
131  have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
132  moreover
133  have "valid \<Gamma>2" by fact
134  moreover
135  have "(x,T) \<in> (set \<Gamma>1)" by fact 
136  ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto
137next
138  case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
139  (* These are all assumptions available in this case*)
140  have a0: "x\<sharp>\<Gamma>1" by fact
141  have a1: "(x,T1)#\<Gamma>1 \<turnstile> t : T2" by fact
142  have a2: "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
143  have a3: "valid \<Gamma>2" by fact
144  have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact
145  have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" using a2 by simp
146  moreover
147  have "valid ((x,T1)#\<Gamma>2)" using v2 (* fails *) 
148    oops
149  
150text\<open>
151  To show that the proof with explicit renaming is not simple, 
152  here is the proof without using the variable convention. It
153  crucially depends on the equivariance property of the typing
154  relation.
155
156\<close>
157
158lemma weakening_with_explicit_renaming: 
159  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
160  assumes a: "\<Gamma>1 \<turnstile> t : T"
161  and     b: "valid \<Gamma>2" 
162  and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"
163  shows "\<Gamma>2 \<turnstile> t : T"
164using a b c
165proof (induct arbitrary: \<Gamma>2)
166  case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
167  have fc0: "x\<sharp>\<Gamma>1" by fact
168  have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact
169  obtain c::"name" where fc1: "c\<sharp>(x,t,\<Gamma>1,\<Gamma>2)"  (* we obtain a fresh name *)
170    by (rule exists_fresh) (auto simp add: fs_name1)
171  have "Lam [c].([(c,x)]\<bullet>t) = Lam [x].t" using fc1 (* we then alpha-rename the lambda-abstraction *)
172    by (auto simp add: lam.inject alpha fresh_prod fresh_atm)
173  moreover
174  have "\<Gamma>2 \<turnstile> Lam [c].([(c,x)]\<bullet>t) : T1 \<rightarrow> T2" (* we can then alpha-rename our original goal *)
175  proof - 
176    (* we establish (x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2) and valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2)) *)
177    have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2)" 
178    proof -
179      have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
180      then have "[(c,x)]\<bullet>((x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2))" using fc0 fc1 
181        by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
182      then show "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2)" by (rule perm_boolE)
183    qed
184    moreover 
185    have "valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2))" 
186    proof -
187      have "valid \<Gamma>2" by fact
188      then show "valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2))" using fc1
189        by (auto intro!: v2 simp add: fresh_left calc_atm eqvts)
190    qed
191    (* these two facts give us by induction hypothesis the following *)
192    ultimately have "(x,T1)#([(c,x)]\<bullet>\<Gamma>2) \<turnstile> t : T2" using ih by simp 
193    (* we now apply renamings to get to our goal *)
194    then have "[(c,x)]\<bullet>((x,T1)#([(c,x)]\<bullet>\<Gamma>2) \<turnstile> t : T2)" by (rule perm_boolI)
195    then have "(c,T1)#\<Gamma>2 \<turnstile> ([(c,x)]\<bullet>t) : T2" using fc1 
196      by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
197    then show "\<Gamma>2 \<turnstile> Lam [c].([(c,x)]\<bullet>t) : T1 \<rightarrow> T2" using fc1 by auto
198  qed
199  ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp
200qed (auto) (* var and app cases *)
201
202text \<open>
203  Moral: compare the proof with explicit renamings to weakening_version1 
204  and weakening_version2, and imagine you are proving something more substantial 
205  than the weakening lemma.\<close>
206
207end
208