148 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast |
148 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast |
149 apply (simp only: akind_aty_atrm.intros) |
149 apply (simp only: akind_aty_atrm.intros) |
150 done |
150 done |
151 |
151 |
152 (* TODO: ask Stefan why 'induct' goes wrong, commented out commands should work *) |
152 (* TODO: ask Stefan why 'induct' goes wrong, commented out commands should work *) |
153 lemma rfv_eqvt_tmp: |
|
154 "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1)) \<and> |
|
155 ((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2)) \<and> |
|
156 ((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))" |
|
157 thm kind_ty_trm.induct |
|
158 (*apply(induct t1 t2 t3 rule: kind_ty_trm.inducts)*) |
|
159 apply(rule kind_ty_trm.induct[of |
|
160 "\<lambda>t1. ((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))" |
|
161 "\<lambda>t2. ((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))" |
|
162 "\<lambda>t3. ((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"]) |
|
163 apply(simp_all add: union_eqvt Diff_eqvt) |
|
164 apply(simp_all add: permute_set_eq atom_eqvt) |
|
165 done |
|
166 |
153 |
167 lemma rfv_eqvt[eqvt]: |
154 lemma rfv_eqvt[eqvt]: |
168 "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))" |
155 "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))" |
169 "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))" |
156 "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))" |
170 "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))" |
157 "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))" |
171 (*apply(induct t1 t2 t3 rule: kind_ty_trm.inducts)*) |
158 apply(induct t1 and t2 and t3 rule: kind_ty_trm.inducts) |
172 apply(simp_all only: rfv_eqvt_tmp) |
159 apply(simp_all add: union_eqvt Diff_eqvt) |
|
160 apply(simp_all add: permute_set_eq atom_eqvt) |
173 done |
161 done |
174 |
162 |
175 lemma alpha_eqvt: |
163 lemma alpha_eqvt: |
176 "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)" |
164 "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)" |
177 "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)" |
165 "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)" |
348 "(op = ===> atrm) Const Const" |
336 "(op = ===> atrm) Const Const" |
349 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done |
337 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done |
350 |
338 |
351 lemma kpi_rsp[quot_respect]: |
339 lemma kpi_rsp[quot_respect]: |
352 "(aty ===> op = ===> akind ===> akind) KPi KPi" |
340 "(aty ===> op = ===> akind ===> akind) KPi KPi" |
353 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry |
341 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) |
|
342 apply (rule a2) apply simp |
|
343 apply (rule_tac x="0" in exI) |
|
344 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv) |
|
345 done |
|
346 |
354 lemma tpi_rsp[quot_respect]: |
347 lemma tpi_rsp[quot_respect]: |
355 "(aty ===> op = ===> aty ===> aty) TPi TPi" |
348 "(aty ===> op = ===> aty ===> aty) TPi TPi" |
356 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry |
349 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) |
|
350 apply (rule a5) apply simp |
|
351 apply (rule_tac x="0" in exI) |
|
352 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv) |
|
353 done |
357 lemma lam_rsp[quot_respect]: |
354 lemma lam_rsp[quot_respect]: |
358 "(aty ===> op = ===> atrm ===> atrm) Lam Lam" |
355 "(aty ===> op = ===> atrm ===> atrm) Lam Lam" |
359 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry |
356 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) |
|
357 apply (rule a9) apply simp |
|
358 apply (rule_tac x="0" in exI) |
|
359 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv) |
|
360 done |
360 |
361 |
361 lemma rfv_ty_rsp[quot_respect]: |
362 lemma rfv_ty_rsp[quot_respect]: |
362 "(aty ===> op =) rfv_ty rfv_ty" |
363 "(aty ===> op =) rfv_ty rfv_ty" |
363 by (simp add: alpha_rfv) |
364 by (simp add: alpha_rfv) |
364 lemma rfv_kind_rsp[quot_respect]: |
365 lemma rfv_kind_rsp[quot_respect]: |
413 apply (induct rule: KIND_TY_TRM_induct) |
414 apply (induct rule: KIND_TY_TRM_induct) |
414 apply simp_all |
415 apply simp_all |
415 done |
416 done |
416 |
417 |
417 lemma perm_add_ok: "((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> (x1 :: KIND))) \<and> ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2) \<and> ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)" |
418 lemma perm_add_ok: "((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> (x1 :: KIND))) \<and> ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2) \<and> ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)" |
418 apply(induct_tac [!] rule: KIND_TY_TRM_induct) |
419 apply(rule KIND_TY_TRM_induct[of |
|
420 "\<lambda>x1. ((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> x1))" |
|
421 "\<lambda>x2. ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2)" |
|
422 "\<lambda>x3. ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)"]) |
419 apply (simp_all) |
423 apply (simp_all) |
420 (* Sth went wrong... *) |
|
421 sorry |
424 sorry |
422 |
425 |
423 instance |
426 instance |
424 apply default |
427 apply default |
425 apply (simp_all add: perm_zero_ok perm_add_ok) |
428 apply (simp_all add: perm_zero_ok perm_add_ok) |