68 @{thms rkind.distinct rty.distinct rtrm.distinct} |
68 @{thms rkind.distinct rty.distinct rtrm.distinct} |
69 @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} |
69 @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} |
70 @{thms alpha_eqvt} ctxt)) ctxt)) *} |
70 @{thms alpha_eqvt} ctxt)) ctxt)) *} |
71 thm alpha_equivps |
71 thm alpha_equivps |
72 |
72 |
73 quotient_type RKIND = rkind / alpha_rkind |
73 quotient_type kind = rkind / alpha_rkind |
74 by (rule alpha_equivps) |
74 by (rule alpha_equivps) |
75 |
75 |
76 quotient_type |
76 quotient_type |
77 RTY = rty / alpha_rty and |
77 ty = rty / alpha_rty and |
78 RTRM = rtrm / alpha_rtrm |
78 trm = rtrm / alpha_rtrm |
79 by (auto intro: alpha_equivps) |
79 by (auto intro: alpha_equivps) |
80 |
80 |
81 quotient_definition |
81 quotient_definition |
82 "TYP :: RKIND" |
82 "TYP :: kind" |
83 is |
83 is |
84 "Type" |
84 "Type" |
85 |
85 |
86 quotient_definition |
86 quotient_definition |
87 "KPI :: RTY \<Rightarrow> name \<Rightarrow> RKIND \<Rightarrow> RKIND" |
87 "KPI :: ty \<Rightarrow> name \<Rightarrow> kind \<Rightarrow> kind" |
88 is |
88 is |
89 "KPi" |
89 "KPi" |
90 |
90 |
91 quotient_definition |
91 quotient_definition |
92 "TCONST :: ident \<Rightarrow> RTY" |
92 "TCONST :: ident \<Rightarrow> ty" |
93 is |
93 is |
94 "TConst" |
94 "TConst" |
95 |
95 |
96 quotient_definition |
96 quotient_definition |
97 "TAPP :: RTY \<Rightarrow> RTRM \<Rightarrow> RTY" |
97 "TAPP :: ty \<Rightarrow> trm \<Rightarrow> ty" |
98 is |
98 is |
99 "TApp" |
99 "TApp" |
100 |
100 |
101 quotient_definition |
101 quotient_definition |
102 "TPI :: RTY \<Rightarrow> name \<Rightarrow> RTY \<Rightarrow> RTY" |
102 "TPI :: ty \<Rightarrow> name \<Rightarrow> ty \<Rightarrow> ty" |
103 is |
103 is |
104 "TPi" |
104 "TPi" |
105 |
105 |
106 (* FIXME: does not work with CONST *) |
106 (* FIXME: does not work with CONST *) |
107 quotient_definition |
107 quotient_definition |
108 "CONS :: ident \<Rightarrow> RTRM" |
108 "CONS :: ident \<Rightarrow> trm" |
109 is |
109 is |
110 "Const" |
110 "Const" |
111 |
111 |
112 quotient_definition |
112 quotient_definition |
113 "VAR :: name \<Rightarrow> RTRM" |
113 "VAR :: name \<Rightarrow> trm" |
114 is |
114 is |
115 "Var" |
115 "Var" |
116 |
116 |
117 quotient_definition |
117 quotient_definition |
118 "APP :: RTRM \<Rightarrow> RTRM \<Rightarrow> RTRM" |
118 "APP :: trm \<Rightarrow> trm \<Rightarrow> trm" |
119 is |
119 is |
120 "App" |
120 "App" |
121 |
121 |
122 quotient_definition |
122 quotient_definition |
123 "LAM :: RTY \<Rightarrow> name \<Rightarrow> RTRM \<Rightarrow> RTRM" |
123 "LAM :: ty \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" |
124 is |
124 is |
125 "Lam" |
125 "Lam" |
126 |
126 |
127 (* FIXME: print out a warning if the type contains a liftet type, like rkind \<Rightarrow> name set *) |
127 (* FIXME: print out a warning if the type contains a liftet type, like rkind \<Rightarrow> name set *) |
128 quotient_definition |
128 quotient_definition |
129 "fv_kind :: RKIND \<Rightarrow> atom set" |
129 "fv_kind :: kind \<Rightarrow> atom set" |
130 is |
130 is |
131 "fv_rkind" |
131 "fv_rkind" |
132 |
132 |
133 quotient_definition |
133 quotient_definition |
134 "fv_ty :: RTY \<Rightarrow> atom set" |
134 "fv_ty :: ty \<Rightarrow> atom set" |
135 is |
135 is |
136 "fv_rty" |
136 "fv_rty" |
137 |
137 |
138 quotient_definition |
138 quotient_definition |
139 "fv_trm :: RTRM \<Rightarrow> atom set" |
139 "fv_trm :: trm \<Rightarrow> atom set" |
140 is |
140 is |
141 "fv_rtrm" |
141 "fv_rtrm" |
142 |
142 |
143 lemma alpha_rfv: |
143 lemma alpha_rfv: |
144 shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and> |
144 shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and> |
202 lemma fv_rtrm_rsp[quot_respect]: |
202 lemma fv_rtrm_rsp[quot_respect]: |
203 "(alpha_rtrm ===> op =) fv_rtrm fv_rtrm" |
203 "(alpha_rtrm ===> op =) fv_rtrm fv_rtrm" |
204 by (simp add: alpha_rfv) |
204 by (simp add: alpha_rfv) |
205 |
205 |
206 thm rkind_rty_rtrm.induct |
206 thm rkind_rty_rtrm.induct |
207 lemmas RKIND_RTY_RTRM_induct = rkind_rty_rtrm.induct[quot_lifted] |
207 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] |
208 |
208 |
209 thm rkind_rty_rtrm.inducts |
209 thm rkind_rty_rtrm.inducts |
210 lemmas RKIND_RTY_RTRM_inducts = rkind_rty_rtrm.inducts[quot_lifted] |
210 lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted] |
211 |
211 |
212 instantiation RKIND and RTY and RTRM :: pt |
212 instantiation kind and ty and trm :: pt |
213 begin |
213 begin |
214 |
214 |
215 quotient_definition |
215 quotient_definition |
216 "permute_RKIND :: perm \<Rightarrow> RKIND \<Rightarrow> RKIND" |
216 "permute_kind :: perm \<Rightarrow> kind \<Rightarrow> kind" |
217 is |
217 is |
218 "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind" |
218 "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind" |
219 |
219 |
220 quotient_definition |
220 quotient_definition |
221 "permute_RTY :: perm \<Rightarrow> RTY \<Rightarrow> RTY" |
221 "permute_ty :: perm \<Rightarrow> ty \<Rightarrow> ty" |
222 is |
222 is |
223 "permute :: perm \<Rightarrow> rty \<Rightarrow> rty" |
223 "permute :: perm \<Rightarrow> rty \<Rightarrow> rty" |
224 |
224 |
225 quotient_definition |
225 quotient_definition |
226 "permute_RTRM :: perm \<Rightarrow> RTRM \<Rightarrow> RTRM" |
226 "permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm" |
227 is |
227 is |
228 "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm" |
228 "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm" |
229 |
229 |
230 lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted] |
230 lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted] |
231 |
231 |
232 lemma perm_zero_ok: "0 \<bullet> (x :: RKIND) = x \<and> 0 \<bullet> (y :: RTY) = y \<and> 0 \<bullet> (z :: RTRM) = z" |
232 lemma perm_zero_ok: "0 \<bullet> (x :: kind) = x \<and> 0 \<bullet> (y :: ty) = y \<and> 0 \<bullet> (z :: trm) = z" |
233 apply (induct rule: RKIND_RTY_RTRM_induct) |
233 apply (induct rule: kind_ty_trm_induct) |
234 apply (simp_all) |
234 apply (simp_all) |
235 done |
235 done |
236 |
236 |
237 lemma perm_add_ok: |
237 lemma perm_add_ok: |
238 "((p + q) \<bullet> (x1 :: RKIND) = (p \<bullet> q \<bullet> x1))" |
238 "((p + q) \<bullet> (x1 :: kind) = (p \<bullet> q \<bullet> x1))" |
239 "((p + q) \<bullet> (x2 :: RTY) = p \<bullet> q \<bullet> x2)" |
239 "((p + q) \<bullet> (x2 :: ty) = p \<bullet> q \<bullet> x2)" |
240 "((p + q) \<bullet> (x3 :: RTRM) = p \<bullet> q \<bullet> x3)" |
240 "((p + q) \<bullet> (x3 :: trm) = p \<bullet> q \<bullet> x3)" |
241 apply (induct x1 and x2 and x3 rule: RKIND_RTY_RTRM_inducts) |
241 apply (induct x1 and x2 and x3 rule: kind_ty_trm_inducts) |
242 apply (simp_all) |
242 apply (simp_all) |
243 done |
243 done |
244 |
244 |
245 instance |
245 instance |
246 apply default |
246 apply default |
247 apply (simp_all add: perm_zero_ok perm_add_ok) |
247 apply (simp_all add: perm_zero_ok perm_add_ok) |
248 done |
248 done |
249 |
249 |
250 end |
250 end |
251 |
251 |
252 lemmas ALPHA_RKIND_ALPHA_RTY_ALPHA_RTRM_inducts = alpha_rkind_alpha_rty_alpha_rtrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
252 lemmas ALPHA_kind_ALPHA_ty_ALPHA_trm_inducts = alpha_rkind_alpha_rty_alpha_rtrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
253 |
253 |
254 lemmas RKIND_RTY_RTRM_INJECT = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
254 lemmas kind_ty_trm_INJECT = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
255 |
255 |
256 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted] |
256 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted] |
257 |
257 |
258 lemmas fv_eqvt = rfv_eqvt[quot_lifted] |
258 lemmas fv_eqvt = rfv_eqvt[quot_lifted] |
259 |
259 |
286 apply(clarify) |
286 apply(clarify) |
287 apply(subst swap_at_base_simps(3)) |
287 apply(subst swap_at_base_simps(3)) |
288 apply(simp_all add: fresh_atom) |
288 apply(simp_all add: fresh_atom) |
289 done |
289 done |
290 |
290 |
291 lemma RKIND_RTY_RTRM_fs: |
291 lemma kind_ty_trm_fs: |
292 "finite (supp (x\<Colon>RKIND))" |
292 "finite (supp (x\<Colon>kind))" |
293 "finite (supp (y\<Colon>RTY))" |
293 "finite (supp (y\<Colon>ty))" |
294 "finite (supp (z\<Colon>RTRM))" |
294 "finite (supp (z\<Colon>trm))" |
295 apply(induct x and y and z rule: RKIND_RTY_RTRM_inducts) |
295 apply(induct x and y and z rule: kind_ty_trm_inducts) |
296 apply(simp_all add: supp_rkind_rty_rtrm_easy) |
296 apply(simp_all add: supp_rkind_rty_rtrm_easy) |
297 apply(rule supports_finite) |
297 apply(rule supports_finite) |
298 apply(rule supp_bind(1)) |
298 apply(rule supp_bind(1)) |
299 apply(simp add: supp_Pair supp_atom) |
299 apply(simp add: supp_Pair supp_atom) |
300 apply(rule supports_finite) |
300 apply(rule supports_finite) |
303 apply(rule supports_finite) |
303 apply(rule supports_finite) |
304 apply(rule supp_bind(3)) |
304 apply(rule supp_bind(3)) |
305 apply(simp add: supp_Pair supp_atom) |
305 apply(simp add: supp_Pair supp_atom) |
306 done |
306 done |
307 |
307 |
308 instance RKIND and RTY and RTRM :: fs |
308 instance kind and ty and trm :: fs |
309 apply(default) |
309 apply(default) |
310 apply(simp_all only: RKIND_RTY_RTRM_fs) |
310 apply(simp_all only: kind_ty_trm_fs) |
311 done |
311 done |
312 |
312 |
313 lemma supp_fv: |
313 lemma supp_fv: |
314 "supp t1 = fv_kind t1" |
314 "supp t1 = fv_kind t1" |
315 "supp t2 = fv_ty t2" |
315 "supp t2 = fv_ty t2" |
316 "supp t3 = fv_trm t3" |
316 "supp t3 = fv_trm t3" |
317 apply(induct t1 and t2 and t3 rule: RKIND_RTY_RTRM_inducts) |
317 apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts) |
318 apply (simp_all add: supp_rkind_rty_rtrm_easy) |
318 apply (simp_all add: supp_rkind_rty_rtrm_easy) |
319 apply (simp_all add: fv_kind_ty_trm) |
319 apply (simp_all add: fv_kind_ty_trm) |
320 apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)") |
320 apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)") |
321 apply(simp add: supp_Abs Set.Un_commute) |
321 apply(simp add: supp_Abs Set.Un_commute) |
322 apply(simp (no_asm) add: supp_def) |
322 apply(simp (no_asm) add: supp_def) |
323 apply(simp add: RKIND_RTY_RTRM_INJECT) |
323 apply(simp add: kind_ty_trm_INJECT) |
324 apply(simp add: Abs_eq_iff) |
324 apply(simp add: Abs_eq_iff) |
325 apply(simp add: alpha_gen) |
325 apply(simp add: alpha_gen) |
326 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt) |
326 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt) |
327 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
327 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
328 apply(subgoal_tac "supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)") |
328 apply(subgoal_tac "supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)") |
329 apply(simp add: supp_Abs Set.Un_commute) |
329 apply(simp add: supp_Abs Set.Un_commute) |
330 apply(simp (no_asm) add: supp_def) |
330 apply(simp (no_asm) add: supp_def) |
331 apply(simp add: RKIND_RTY_RTRM_INJECT) |
331 apply(simp add: kind_ty_trm_INJECT) |
332 apply(simp add: Abs_eq_iff) |
332 apply(simp add: Abs_eq_iff) |
333 apply(simp add: alpha_gen) |
333 apply(simp add: alpha_gen) |
334 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt) |
334 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt) |
335 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
335 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
336 apply(subgoal_tac "supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)") |
336 apply(subgoal_tac "supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)") |
337 apply(simp add: supp_Abs Set.Un_commute) |
337 apply(simp add: supp_Abs Set.Un_commute) |
338 apply(simp (no_asm) add: supp_def) |
338 apply(simp (no_asm) add: supp_def) |
339 apply(simp add: RKIND_RTY_RTRM_INJECT) |
339 apply(simp add: kind_ty_trm_INJECT) |
340 apply(simp add: Abs_eq_iff) |
340 apply(simp add: Abs_eq_iff) |
341 apply(simp add: alpha_gen) |
341 apply(simp add: alpha_gen) |
342 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt) |
342 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt) |
343 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
343 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) |
344 done |
344 done |
345 |
345 |
346 (* Not needed anymore *) |
346 (* Not needed anymore *) |
347 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A" |
347 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A" |
348 apply (simp add: permute_set_eq supp_def Abs_eq_iff RKIND_RTY_RTRM_INJECT) |
348 apply (simp add: permute_set_eq supp_def Abs_eq_iff kind_ty_trm_INJECT) |
349 apply (simp add: alpha_gen supp_fv) |
349 apply (simp add: alpha_gen supp_fv) |
350 apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute) |
350 apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute) |
351 done |
351 done |
352 |
352 |
353 lemma supp_rkind_rty_rtrm: |
353 lemma supp_rkind_rty_rtrm: |