1(* Formalisation of weakening using locally nameless    *)
2(* terms; the nominal infrastructure can also derive    *)
3(* strong induction principles for such representations *)
4(*                                                      *)
5(* Authors: Christian Urban and Randy Pollack           *)
6theory LocalWeakening
7  imports "HOL-Nominal.Nominal"
8begin
9
10atom_decl name
11
12text \<open>
13  Curry-style lambda terms in locally nameless 
14  representation without any binders           
15\<close>
16nominal_datatype llam = 
17    lPar "name"
18  | lVar "nat"
19  | lApp "llam" "llam"
20  | lLam "llam"
21
22text \<open>definition of vsub - at the moment a bit cumbersome\<close>
23
24lemma llam_cases:
25  "(\<exists>a. t = lPar a) \<or> (\<exists>n. t = lVar n) \<or> (\<exists>t1 t2. t = lApp t1 t2) \<or> 
26   (\<exists>t1. t = lLam t1)"
27by (induct t rule: llam.induct)
28   (auto simp add: llam.inject)
29
30nominal_primrec
31  llam_size :: "llam \<Rightarrow> nat"
32where
33  "llam_size (lPar a) = 1"
34| "llam_size (lVar n) = 1"
35| "llam_size (lApp t1 t2) = 1 + (llam_size t1) + (llam_size t2)"
36| "llam_size (lLam t) = 1 + (llam_size t)"
37by (rule TrueI)+
38
39function  
40  vsub :: "llam \<Rightarrow> nat \<Rightarrow> llam \<Rightarrow> llam"
41where
42   vsub_lPar: "vsub (lPar p) x s = lPar p"
43 | vsub_lVar: "vsub (lVar n) x s = (if n < x then (lVar n)
44                      else (if n = x then s else (lVar (n - 1))))"
45 | vsub_lApp: "vsub (lApp t u) x s = (lApp (vsub t x s) (vsub u x s))"
46 | vsub_lLam: "vsub (lLam t) x s = (lLam (vsub t (x + 1) s))"
47using llam_cases
48apply(auto simp add: llam.inject)
49apply(rotate_tac 4)
50apply(drule_tac x="a" in meta_spec)
51apply(blast)
52done
53termination by (relation "measure (llam_size \<circ> fst)") auto
54
55lemma vsub_eqvt[eqvt]:
56  fixes pi::"name prm" 
57  shows "pi\<bullet>(vsub t n s) = vsub (pi\<bullet>t) (pi\<bullet>n) (pi\<bullet>s)"
58by (induct t arbitrary: n rule: llam.induct)
59   (simp_all add: perm_nat_def)
60
61definition freshen :: "llam \<Rightarrow> name \<Rightarrow> llam" where
62  "freshen t p \<equiv> vsub t 0 (lPar p)"
63
64lemma freshen_eqvt[eqvt]:
65  fixes pi::"name prm" 
66  shows "pi\<bullet>(freshen t p) = freshen (pi\<bullet>t) (pi\<bullet>p)"
67by (simp add: vsub_eqvt freshen_def perm_nat_def)
68
69text \<open>types\<close>
70
71nominal_datatype ty =
72    TVar "nat"
73  | TArr "ty" "ty" (infix "\<rightarrow>" 200)
74
75lemma ty_fresh[simp]:
76  fixes x::"name"
77  and   T::"ty"
78  shows "x\<sharp>T"
79by (induct T rule: ty.induct) 
80   (simp_all add: fresh_nat)
81
82text \<open>valid contexts\<close>
83
84type_synonym cxt = "(name\<times>ty) list"
85
86inductive
87  valid :: "cxt \<Rightarrow> bool"
88where
89  v1[intro]: "valid []"
90| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,T)#\<Gamma>)"
91
92equivariance valid
93
94lemma v2_elim:
95  assumes a: "valid ((a,T)#\<Gamma>)"
96  shows   "a\<sharp>\<Gamma> \<and> valid \<Gamma>"
97using a by (cases) (auto)
98
99text \<open>"weak" typing relation\<close>
100
101inductive
102  typing :: "cxt\<Rightarrow>llam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60)
103where
104  t_lPar[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lPar x : T"
105| t_lApp[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lApp t1 t2 : T2"
106| t_lLam[intro]: "\<lbrakk>x\<sharp>t; (x,T1)#\<Gamma> \<turnstile> freshen t x : T2\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lLam t : T1\<rightarrow>T2"
107
108equivariance typing
109
110lemma typing_implies_valid:
111  assumes a: "\<Gamma> \<turnstile> t : T"
112  shows "valid \<Gamma>"
113using a by (induct) (auto dest: v2_elim)
114
115text \<open>
116  we have to explicitly state that nominal_inductive should strengthen 
117  over the variable x (since x is not a binder)
118\<close>
119nominal_inductive typing
120  avoids t_lLam: x
121  by (auto simp add: fresh_prod dest: v2_elim typing_implies_valid)
122  
123text \<open>strong induction principle for typing\<close>
124thm typing.strong_induct
125
126text \<open>sub-contexts\<close>
127
128abbreviation
129  "sub_context" :: "cxt \<Rightarrow> cxt \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) 
130where
131  "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x,T)\<in>set \<Gamma>1 \<longrightarrow> (x,T)\<in>set \<Gamma>2"
132
133lemma weakening_almost_automatic:
134  fixes \<Gamma>1 \<Gamma>2 :: cxt
135  assumes a: "\<Gamma>1 \<turnstile> t : T"
136  and     b: "\<Gamma>1 \<subseteq> \<Gamma>2"
137  and     c: "valid \<Gamma>2"
138shows "\<Gamma>2 \<turnstile> t : T"
139using a b c
140apply(nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
141apply(auto)
142apply(drule_tac x="(x,T1)#\<Gamma>2" in meta_spec)
143apply(auto intro!: t_lLam)
144done
145
146lemma weakening_in_more_detail:
147  fixes \<Gamma>1 \<Gamma>2 :: cxt
148  assumes a: "\<Gamma>1 \<turnstile> t : T"
149  and     b: "\<Gamma>1 \<subseteq> \<Gamma>2"
150  and     c: "valid \<Gamma>2"
151shows "\<Gamma>2 \<turnstile> t : T"
152using a b c
153proof(nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
154  case (t_lPar \<Gamma>1 x T \<Gamma>2)  (* variable case *)
155  have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 
156  moreover  
157  have "valid \<Gamma>2" by fact 
158  moreover 
159  have "(x,T)\<in> set \<Gamma>1" by fact
160  ultimately show "\<Gamma>2 \<turnstile> lPar x : T" by auto
161next
162  case (t_lLam x t T1 \<Gamma>1 T2 \<Gamma>2) (* lambda case *)
163  have vc: "x\<sharp>\<Gamma>2" "x\<sharp>t" by fact+  (* variable convention *)
164  have ih: "\<lbrakk>(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2; valid ((x,T1)#\<Gamma>2)\<rbrakk> \<Longrightarrow> (x,T1)#\<Gamma>2 \<turnstile> freshen t x : T2" by fact
165  have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
166  then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp
167  moreover
168  have "valid \<Gamma>2" by fact
169  then have "valid ((x,T1)#\<Gamma>2)" using vc by (simp add: v2)
170  ultimately have "(x,T1)#\<Gamma>2 \<turnstile> freshen t x : T2" using ih by simp
171  with vc show "\<Gamma>2 \<turnstile> lLam t : T1\<rightarrow>T2" by auto
172next 
173  case (t_lApp \<Gamma>1 t1 T1 T2 t2 \<Gamma>2)
174  then show "\<Gamma>2 \<turnstile> lApp t1 t2 : T2" by auto
175qed
176
177end
178