147 apply (simp only: akind_aty_atrm.intros) |
147 apply (simp only: akind_aty_atrm.intros) |
148 |
148 |
149 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast |
149 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast |
150 apply (simp only: akind_aty_atrm.intros) |
150 apply (simp only: akind_aty_atrm.intros) |
151 done |
151 done |
152 |
|
153 (* TODO: ask Stefan why 'induct' goes wrong, commented out commands should work *) |
|
154 |
152 |
155 lemma rfv_eqvt[eqvt]: |
153 lemma rfv_eqvt[eqvt]: |
156 "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))" |
154 "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))" |
157 "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))" |
155 "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))" |
158 "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))" |
156 "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))" |
589 apply (case_tac "(a \<rightleftharpoons> b) \<bullet> A = A") |
587 apply (case_tac "(a \<rightleftharpoons> b) \<bullet> A = A") |
590 apply (case_tac "supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x}") |
588 apply (case_tac "supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x}") |
591 apply simp_all |
589 apply simp_all |
592 sorry |
590 sorry |
593 |
591 |
594 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A" |
592 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abst {atom x} K)) \<union> supp A" |
595 apply (subst supp_Pair[symmetric]) |
593 apply (subst supp_Pair[symmetric]) |
596 unfolding supp_def |
594 unfolding supp_def |
597 apply (simp add: permute_set_eq) |
595 apply (simp add: permute_set_eq) |
598 apply(subst abs_eq) |
596 apply(subst abs_eq) |
599 apply(subst KIND_TY_TRM_INJECT) |
597 apply(subst KIND_TY_TRM_INJECT) |
600 apply(simp only: supp_fv) |
598 apply(simp only: supp_fv) |
601 apply simp |
599 apply simp |
602 apply (unfold supp_def) |
600 apply (unfold supp_def) |
603 sorry |
601 sorry |
604 |
602 |
|
603 lemma KIND_TY_TRM_fs: |
|
604 "finite (supp (x\<Colon>KIND))" |
|
605 "finite (supp (y\<Colon>TY))" |
|
606 "finite (supp (z\<Colon>TRM))" |
|
607 apply(induct x and y and z rule: KIND_TY_TRM_inducts) |
|
608 sorry |
|
609 |
|
610 instance KIND and TY and TRM :: fs |
|
611 apply(default) |
|
612 apply(simp_all only: KIND_TY_TRM_fs) |
|
613 done |
|
614 |
605 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
615 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
606 apply(subst supp_kpi_pre) |
616 apply(subst supp_kpi_pre) |
607 thm supp_Abs |
617 apply(subst supp_Abst) |
608 (*apply(simp add: supp_Abs)*) |
618 apply (simp only: Set.Un_commute) |
609 sorry |
619 done |
610 |
620 |
611 lemma supp_kind_ty_trm: |
621 lemma supp_kind_ty_trm: |
612 "supp TYP = {}" |
622 "supp TYP = {}" |
613 "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
623 "supp (KPI A x K) = supp A \<union> (supp K - {atom x})" |
614 "supp (TCONST i) = {atom i}" |
624 "supp (TCONST i) = {atom i}" |
619 "supp (APP M N) = supp M \<union> supp N" |
629 "supp (APP M N) = supp M \<union> supp N" |
620 "supp (LAM A x M) = supp A \<union> (supp M - {atom x})" |
630 "supp (LAM A x M) = supp A \<union> (supp M - {atom x})" |
621 apply - |
631 apply - |
622 apply (simp add: supp_def) |
632 apply (simp add: supp_def) |
623 apply (simp add: supp_kpi) |
633 apply (simp add: supp_kpi) |
624 apply (simp add: supp_def) (* need ty.distinct lifted *) |
634 apply (simp add: supp_def KIND_TY_TRM_INJECT) apply (fold supp_def) apply (rule supp_at_base) |
|
635 apply (simp add: supp_def permute_ktt KIND_TY_TRM_INJECT Collect_imp_eq Collect_neg_eq) |
|
636 defer |
|
637 apply (simp add: supp_def KIND_TY_TRM_INJECT) apply (fold supp_def) apply (rule supp_at_base) |
|
638 apply (simp add: supp_def KIND_TY_TRM_INJECT) apply (fold supp_def) apply (rule supp_at_base) |
|
639 apply (simp add: supp_def permute_ktt KIND_TY_TRM_INJECT Collect_imp_eq Collect_neg_eq) |
625 sorry |
640 sorry |
626 |
641 |
627 |
642 |
628 end |
643 end |
629 |
644 |