1 theory LFex |
|
2 imports Nominal "../Quotient_List" |
|
3 begin |
|
4 |
|
5 atom_decl name ident |
|
6 |
|
7 nominal_datatype kind = |
|
8 Type |
|
9 | KPi "ty" "name" "kind" |
|
10 and ty = |
|
11 TConst "ident" |
|
12 | TApp "ty" "trm" |
|
13 | TPi "ty" "name" "ty" |
|
14 and trm = |
|
15 Const "ident" |
|
16 | Var "name" |
|
17 | App "trm" "trm" |
|
18 | Lam "ty" "name" "trm" |
|
19 |
|
20 function |
|
21 fv_kind :: "kind \<Rightarrow> name set" |
|
22 and fv_ty :: "ty \<Rightarrow> name set" |
|
23 and fv_trm :: "trm \<Rightarrow> name set" |
|
24 where |
|
25 "fv_kind (Type) = {}" |
|
26 | "fv_kind (KPi A x K) = (fv_ty A) \<union> ((fv_kind K) - {x})" |
|
27 | "fv_ty (TConst i) = {}" |
|
28 | "fv_ty (TApp A M) = (fv_ty A) \<union> (fv_trm M)" |
|
29 | "fv_ty (TPi A x B) = (fv_ty A) \<union> ((fv_ty B) - {x})" |
|
30 | "fv_trm (Const i) = {}" |
|
31 | "fv_trm (Var x) = {x}" |
|
32 | "fv_trm (App M N) = (fv_trm M) \<union> (fv_trm N)" |
|
33 | "fv_trm (Lam A x M) = (fv_ty A) \<union> ((fv_trm M) - {x})" |
|
34 sorry |
|
35 |
|
36 termination fv_kind sorry |
|
37 |
|
38 inductive |
|
39 akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100) |
|
40 and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100) |
|
41 and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100) |
|
42 where |
|
43 a1: "(Type) \<approx>ki (Type)" |
|
44 | a21: "\<lbrakk>A \<approx>ty A'; K \<approx>ki K'\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x K')" |
|
45 | a22: "\<lbrakk>A \<approx>ty A'; K \<approx>ki ([(x,x')]\<bullet>K'); x \<notin> (fv_ty A'); x \<notin> ((fv_kind K') - {x'})\<rbrakk> |
|
46 \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')" |
|
47 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)" |
|
48 | a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')" |
|
49 | a51: "\<lbrakk>A \<approx>ty A'; B \<approx>ty B'\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x B')" |
|
50 | a52: "\<lbrakk>A \<approx>ty A'; B \<approx>ty ([(x,x')]\<bullet>B'); x \<notin> (fv_ty B'); x \<notin> ((fv_ty B') - {x'})\<rbrakk> |
|
51 \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')" |
|
52 | a6: "i = j \<Longrightarrow> (Const i) \<approx>trm (Const j)" |
|
53 | a7: "x = y \<Longrightarrow> (Var x) \<approx>trm (Var y)" |
|
54 | a8: "\<lbrakk>M \<approx>trm M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')" |
|
55 | a91: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x M')" |
|
56 | a92: "\<lbrakk>A \<approx>ty A'; M \<approx>tr ([(x,x')]\<bullet>M'); x \<notin> (fv_ty B'); x \<notin> ((fv_trm M') - {x'})\<rbrakk> |
|
57 \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')" |
|
58 |
|
59 lemma al_refl: |
|
60 fixes K::"kind" |
|
61 and A::"ty" |
|
62 and M::"trm" |
|
63 shows "K \<approx>ki K" |
|
64 and "A \<approx>ty A" |
|
65 and "M \<approx>tr M" |
|
66 apply(induct K and A and M rule: kind_ty_trm.inducts) |
|
67 apply(auto intro: akind_aty_atrm.intros) |
|
68 done |
|
69 |
|
70 lemma alpha_equivps: |
|
71 shows "equivp akind" |
|
72 and "equivp aty" |
|
73 and "equivp atrm" |
|
74 sorry |
|
75 |
|
76 quotient_type KIND = kind / akind |
|
77 by (rule alpha_equivps) |
|
78 |
|
79 quotient_type |
|
80 TY = ty / aty and |
|
81 TRM = trm / atrm |
|
82 by (auto intro: alpha_equivps) |
|
83 |
|
84 quotient_definition |
|
85 "TYP :: KIND" |
|
86 is |
|
87 "Type" |
|
88 |
|
89 quotient_definition |
|
90 "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND" |
|
91 is |
|
92 "KPi" |
|
93 |
|
94 quotient_definition |
|
95 "TCONST :: ident \<Rightarrow> TY" |
|
96 is |
|
97 "TConst" |
|
98 |
|
99 quotient_definition |
|
100 "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY" |
|
101 is |
|
102 "TApp" |
|
103 |
|
104 quotient_definition |
|
105 "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY" |
|
106 is |
|
107 "TPi" |
|
108 |
|
109 (* FIXME: does not work with CONST *) |
|
110 quotient_definition |
|
111 "CONS :: ident \<Rightarrow> TRM" |
|
112 is |
|
113 "Const" |
|
114 |
|
115 quotient_definition |
|
116 "VAR :: name \<Rightarrow> TRM" |
|
117 is |
|
118 "Var" |
|
119 |
|
120 quotient_definition |
|
121 "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM" |
|
122 is |
|
123 "App" |
|
124 |
|
125 quotient_definition |
|
126 "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM" |
|
127 is |
|
128 "Lam" |
|
129 |
|
130 thm TYP_def |
|
131 thm KPI_def |
|
132 thm TCONST_def |
|
133 thm TAPP_def |
|
134 thm TPI_def |
|
135 thm VAR_def |
|
136 thm CONS_def |
|
137 thm APP_def |
|
138 thm LAM_def |
|
139 |
|
140 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *) |
|
141 quotient_definition |
|
142 "FV_kind :: KIND \<Rightarrow> name set" |
|
143 is |
|
144 "fv_kind" |
|
145 |
|
146 quotient_definition |
|
147 "FV_ty :: TY \<Rightarrow> name set" |
|
148 is |
|
149 "fv_ty" |
|
150 |
|
151 quotient_definition |
|
152 "FV_trm :: TRM \<Rightarrow> name set" |
|
153 is |
|
154 "fv_trm" |
|
155 |
|
156 thm FV_kind_def |
|
157 thm FV_ty_def |
|
158 thm FV_trm_def |
|
159 |
|
160 (* FIXME: does not work yet *) |
|
161 overloading |
|
162 perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" (unchecked) |
|
163 perm_ty \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" (unchecked) |
|
164 perm_trm \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" (unchecked) |
|
165 begin |
|
166 |
|
167 quotient_definition |
|
168 "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" |
|
169 is |
|
170 "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)" |
|
171 |
|
172 quotient_definition |
|
173 "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" |
|
174 is |
|
175 "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)" |
|
176 |
|
177 quotient_definition |
|
178 "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
|
179 is |
|
180 "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
|
181 |
|
182 end |
|
183 |
|
184 (* TODO/FIXME: Think whether these RSP theorems are true. *) |
|
185 lemma kpi_rsp[quot_respect]: |
|
186 "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry |
|
187 lemma tconst_rsp[quot_respect]: |
|
188 "(op = ===> aty) TConst TConst" sorry |
|
189 lemma tapp_rsp[quot_respect]: |
|
190 "(aty ===> atrm ===> aty) TApp TApp" sorry |
|
191 lemma tpi_rsp[quot_respect]: |
|
192 "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry |
|
193 lemma var_rsp[quot_respect]: |
|
194 "(op = ===> atrm) Var Var" sorry |
|
195 lemma app_rsp[quot_respect]: |
|
196 "(atrm ===> atrm ===> atrm) App App" sorry |
|
197 lemma const_rsp[quot_respect]: |
|
198 "(op = ===> atrm) Const Const" sorry |
|
199 lemma lam_rsp[quot_respect]: |
|
200 "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry |
|
201 |
|
202 lemma perm_kind_rsp[quot_respect]: |
|
203 "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry |
|
204 lemma perm_ty_rsp[quot_respect]: |
|
205 "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry |
|
206 lemma perm_trm_rsp[quot_respect]: |
|
207 "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry |
|
208 |
|
209 lemma fv_ty_rsp[quot_respect]: |
|
210 "(aty ===> op =) fv_ty fv_ty" sorry |
|
211 lemma fv_kind_rsp[quot_respect]: |
|
212 "(akind ===> op =) fv_kind fv_kind" sorry |
|
213 lemma fv_trm_rsp[quot_respect]: |
|
214 "(atrm ===> op =) fv_trm fv_trm" sorry |
|
215 |
|
216 |
|
217 thm akind_aty_atrm.induct |
|
218 thm kind_ty_trm.induct |
|
219 |
|
220 |
|
221 lemma |
|
222 assumes a0: |
|
223 "P1 TYP TYP" |
|
224 and a1: |
|
225 "\<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> |
|
226 \<Longrightarrow> P1 (KPI A x K) (KPI A' x K')" |
|
227 and a2: |
|
228 "\<And>A A' K K' x x'. \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); |
|
229 x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K')" |
|
230 and a3: |
|
231 "\<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j)" |
|
232 and a4: |
|
233 "\<And>A A' M M'. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P2 (TAPP A M) (TAPP A' M')" |
|
234 and a5: |
|
235 "\<And>A A' B B' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = B'; P2 B B'\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x B')" |
|
236 and a6: |
|
237 "\<And>A A' B x x' B'. \<lbrakk>(A ::TY) = A'; P2 A A'; (B ::TY) = ([(x, x')] \<bullet> B'); P2 B ([(x, x')] \<bullet> B'); |
|
238 x \<notin> FV_ty B'; x \<notin> FV_ty B' - {x'}\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x' B')" |
|
239 and a7: |
|
240 "\<And>i j m. i = j \<Longrightarrow> P3 (CONS i) (m (CONS j))" |
|
241 and a8: |
|
242 "\<And>x y m. x = y \<Longrightarrow> P3 (VAR x) (m (VAR y))" |
|
243 and a9: |
|
244 "\<And>M m M' N N'. \<lbrakk>(M :: TRM) = m M'; P3 M (m M'); (N :: TRM) = N'; P3 N N'\<rbrakk> \<Longrightarrow> P3 (APP M N) (APP M' N')" |
|
245 and a10: |
|
246 "\<And>A A' M M' x. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x M')" |
|
247 and a11: |
|
248 "\<And>A A' M x x' M' B'. \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); |
|
249 x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')" |
|
250 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
|
251 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
|
252 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
|
253 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
|
254 apply(lifting_setup akind_aty_atrm.induct) |
|
255 defer |
|
256 apply injection |
|
257 apply cleaning |
|
258 apply (simp only: ball_reg_eqv[OF KIND_equivp] ball_reg_eqv[OF TRM_equivp] ball_reg_eqv[OF TY_equivp]) |
|
259 apply (rule ball_reg_right)+ |
|
260 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
261 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
262 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
263 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
264 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
265 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
266 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
267 apply simp |
|
268 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
269 apply simp |
|
270 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
271 apply simp |
|
272 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
273 apply simp |
|
274 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
275 apply simp |
|
276 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
277 apply simp |
|
278 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
279 apply simp |
|
280 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
281 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
282 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
283 defer |
|
284 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
285 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
286 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
287 defer |
|
288 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
289 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
290 defer |
|
291 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
292 apply simp |
|
293 apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
294 apply simp |
|
295 apply simp |
|
296 apply regularize+ |
|
297 done |
|
298 |
|
299 (* Does not work: |
|
300 lemma |
|
301 assumes a0: "P1 TYP" |
|
302 and a1: "\<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind)" |
|
303 and a2: "\<And>id. P2 (TCONST id)" |
|
304 and a3: "\<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm)" |
|
305 and a4: "\<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2)" |
|
306 and a5: "\<And>id. P3 (CONS id)" |
|
307 and a6: "\<And>name. P3 (VAR name)" |
|
308 and a7: "\<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2)" |
|
309 and a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)" |
|
310 shows "P1 mkind \<and> P2 mty \<and> P3 mtrm" |
|
311 using a0 a1 a2 a3 a4 a5 a6 a7 a8 |
|
312 *) |
|
313 |
|
314 |
|
315 lemma "\<lbrakk>P TYP; |
|
316 \<And>ty name kind. \<lbrakk>Q ty; P kind\<rbrakk> \<Longrightarrow> P (KPI ty name kind); |
|
317 \<And>id. Q (TCONST id); |
|
318 \<And>ty trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> Q (TAPP ty trm); |
|
319 \<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2); |
|
320 \<And>id. R (CONS id); \<And>name. R (VAR name); |
|
321 \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2); |
|
322 \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk> |
|
323 \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm" |
|
324 apply(lifting kind_ty_trm.induct) |
|
325 done |
|
326 |
|
327 end |
|
328 |
|
329 |
|
330 |
|
331 |
|