|
1 theory LFex |
|
2 imports Nominal "../QuotMain" |
|
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 KIND = kind / akind |
|
77 by (rule alpha_equivps) |
|
78 |
|
79 quotient TY = ty / aty |
|
80 and TRM = trm / atrm |
|
81 by (auto intro: alpha_equivps) |
|
82 |
|
83 print_quotients |
|
84 |
|
85 quotient_def |
|
86 TYP :: "KIND" |
|
87 where |
|
88 "TYP \<equiv> Type" |
|
89 |
|
90 quotient_def |
|
91 KPI :: "TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND" |
|
92 where |
|
93 "KPI \<equiv> KPi" |
|
94 |
|
95 quotient_def |
|
96 TCONST :: "ident \<Rightarrow> TY" |
|
97 where |
|
98 "TCONST \<equiv> TConst" |
|
99 |
|
100 quotient_def |
|
101 TAPP :: "TY \<Rightarrow> TRM \<Rightarrow> TY" |
|
102 where |
|
103 "TAPP \<equiv> TApp" |
|
104 |
|
105 quotient_def |
|
106 TPI :: "TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY" |
|
107 where |
|
108 "TPI \<equiv> TPi" |
|
109 |
|
110 (* FIXME: does not work with CONST *) |
|
111 quotient_def |
|
112 CONS :: "ident \<Rightarrow> TRM" |
|
113 where |
|
114 "CONS \<equiv> Const" |
|
115 |
|
116 quotient_def |
|
117 VAR :: "name \<Rightarrow> TRM" |
|
118 where |
|
119 "VAR \<equiv> Var" |
|
120 |
|
121 quotient_def |
|
122 APP :: "TRM \<Rightarrow> TRM \<Rightarrow> TRM" |
|
123 where |
|
124 "APP \<equiv> App" |
|
125 |
|
126 quotient_def |
|
127 LAM :: "TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM" |
|
128 where |
|
129 "LAM \<equiv> Lam" |
|
130 |
|
131 thm TYP_def |
|
132 thm KPI_def |
|
133 thm TCONST_def |
|
134 thm TAPP_def |
|
135 thm TPI_def |
|
136 thm VAR_def |
|
137 thm CONS_def |
|
138 thm APP_def |
|
139 thm LAM_def |
|
140 |
|
141 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *) |
|
142 quotient_def |
|
143 FV_kind :: "KIND \<Rightarrow> name set" |
|
144 where |
|
145 "FV_kind \<equiv> fv_kind" |
|
146 |
|
147 quotient_def |
|
148 FV_ty :: "TY \<Rightarrow> name set" |
|
149 where |
|
150 "FV_ty \<equiv> fv_ty" |
|
151 |
|
152 quotient_def |
|
153 FV_trm :: "TRM \<Rightarrow> name set" |
|
154 where |
|
155 "FV_trm \<equiv> fv_trm" |
|
156 |
|
157 thm FV_kind_def |
|
158 thm FV_ty_def |
|
159 thm FV_trm_def |
|
160 |
|
161 (* FIXME: does not work yet *) |
|
162 overloading |
|
163 perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" (unchecked) |
|
164 perm_ty \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" (unchecked) |
|
165 perm_trm \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" (unchecked) |
|
166 begin |
|
167 |
|
168 quotient_def |
|
169 perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND" |
|
170 where |
|
171 "perm_kind \<equiv> (perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)" |
|
172 |
|
173 quotient_def |
|
174 perm_ty :: "'x prm \<Rightarrow> TY \<Rightarrow> TY" |
|
175 where |
|
176 "perm_ty \<equiv> (perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)" |
|
177 |
|
178 quotient_def |
|
179 perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
|
180 where |
|
181 "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
|
182 |
|
183 (* TODO/FIXME: Think whether these RSP theorems are true. *) |
|
184 lemma kpi_rsp[quotient_rsp]: |
|
185 "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry |
|
186 lemma tconst_rsp[quotient_rsp]: |
|
187 "(op = ===> aty) TConst TConst" sorry |
|
188 lemma tapp_rsp[quotient_rsp]: |
|
189 "(aty ===> atrm ===> aty) TApp TApp" sorry |
|
190 lemma tpi_rsp[quotient_rsp]: |
|
191 "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry |
|
192 lemma var_rsp[quotient_rsp]: |
|
193 "(op = ===> atrm) Var Var" sorry |
|
194 lemma app_rsp[quotient_rsp]: |
|
195 "(atrm ===> atrm ===> atrm) App App" sorry |
|
196 lemma const_rsp[quotient_rsp]: |
|
197 "(op = ===> atrm) Const Const" sorry |
|
198 lemma lam_rsp[quotient_rsp]: |
|
199 "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry |
|
200 |
|
201 lemma perm_kind_rsp[quotient_rsp]: |
|
202 "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry |
|
203 lemma perm_ty_rsp[quotient_rsp]: |
|
204 "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry |
|
205 lemma perm_trm_rsp[quotient_rsp]: |
|
206 "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry |
|
207 |
|
208 lemma fv_ty_rsp[quotient_rsp]: |
|
209 "(aty ===> op =) fv_ty fv_ty" sorry |
|
210 lemma fv_kind_rsp[quotient_rsp]: |
|
211 "(akind ===> op =) fv_kind fv_kind" sorry |
|
212 lemma fv_trm_rsp[quotient_rsp]: |
|
213 "(atrm ===> op =) fv_trm fv_trm" sorry |
|
214 |
|
215 |
|
216 thm akind_aty_atrm.induct |
|
217 thm kind_ty_trm.induct |
|
218 |
|
219 ML {* |
|
220 val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM} |
|
221 val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps} |
|
222 val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot |
|
223 val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quot |
|
224 *} |
|
225 |
|
226 lemma |
|
227 assumes a0: |
|
228 "P1 TYP TYP" |
|
229 and a1: |
|
230 "\<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> |
|
231 \<Longrightarrow> P1 (KPI A x K) (KPI A' x K')" |
|
232 and a2: |
|
233 "\<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'); |
|
234 x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K')" |
|
235 and a3: |
|
236 "\<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j)" |
|
237 and a4: |
|
238 "\<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')" |
|
239 and a5: |
|
240 "\<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')" |
|
241 and a6: |
|
242 "\<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'); |
|
243 x \<notin> FV_ty B'; x \<notin> FV_ty B' - {x'}\<rbrakk> \<Longrightarrow> P2 (TPI A x B) (TPI A' x' B')" |
|
244 and a7: |
|
245 "\<And>i j m. i = j \<Longrightarrow> P3 (CONS i) (m (CONS j))" |
|
246 and a8: |
|
247 "\<And>x y m. x = y \<Longrightarrow> P3 (VAR x) (m (VAR y))" |
|
248 and a9: |
|
249 "\<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')" |
|
250 and a10: |
|
251 "\<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')" |
|
252 and a11: |
|
253 "\<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'); |
|
254 x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')" |
|
255 shows "((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
|
256 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
|
257 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
|
258 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
|
259 apply - |
|
260 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
|
261 apply(tactic {* regularize_tac @{context} 1 *}) |
|
262 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) |
|
263 apply(fold perm_kind_def perm_ty_def perm_trm_def) |
|
264 apply(tactic {* clean_tac @{context} 1 *}) |
|
265 (* |
|
266 Profiling: |
|
267 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
|
268 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
|
269 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *} |
|
270 ML_prf {* PolyML.profiling 1 *} |
|
271 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
|
272 *) |
|
273 done |
|
274 |
|
275 (* Does not work: |
|
276 lemma |
|
277 assumes a0: "P1 TYP" |
|
278 and a1: "\<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind)" |
|
279 and a2: "\<And>id. P2 (TCONST id)" |
|
280 and a3: "\<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm)" |
|
281 and a4: "\<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2)" |
|
282 and a5: "\<And>id. P3 (CONS id)" |
|
283 and a6: "\<And>name. P3 (VAR name)" |
|
284 and a7: "\<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2)" |
|
285 and a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)" |
|
286 shows "P1 mkind \<and> P2 mty \<and> P3 mtrm" |
|
287 using a0 a1 a2 a3 a4 a5 a6 a7 a8 |
|
288 *) |
|
289 |
|
290 lemma "\<lbrakk>P TYP; |
|
291 \<And>ty name kind. \<lbrakk>Q ty; P kind\<rbrakk> \<Longrightarrow> P (KPI ty name kind); |
|
292 \<And>id. Q (TCONST id); |
|
293 \<And>ty trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> Q (TAPP ty trm); |
|
294 \<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2); |
|
295 \<And>id. R (CONS id); \<And>name. R (VAR name); |
|
296 \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2); |
|
297 \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk> |
|
298 \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm" |
|
299 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
|
300 done |
|
301 |
|
302 print_quotients |
|
303 |
|
304 end |
|
305 |
|
306 |
|
307 |