29 | "rfv_ty (TConst i) = {}"

    29 | "rfv_ty (TConst i) = {atom i}"

    32 | "rfv_trm (Const i) = {}"

    32 | "rfv_trm (Const i) = {atom i}"

   114 lemma akind_aty_artm_inj:

   115 lemma akind_aty_atrm_inj:

   398 term "permute_TRM"

   422 lemma permute_ktt[simp]:

   399 thm permute_kind_permute_ty_permute_trm.simps

   400 lemma [simp]:

   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)"

   440 lemma perm_add_ok: 

   419 apply(rule KIND_TY_TRM_induct[of 

   441   "((p + q) \<bullet> (x1 :: KIND) = (p \<bullet> q \<bullet> x1))"

   420 "\<lambda>x1. ((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> x1))"

   442   "((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)"

   421 "\<lambda>x2. ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2)"

   443   "((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)"

   422 "\<lambda>x3. ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)"])

   444 apply(induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts)

   424 sorry

   446 done

   455 apply (lifting akind_aty_atrm.induct)

   477 by (lifting akind_aty_atrm.induct)

   456 done

   478 

   479 lemma AKIND_ATY_ATRM_inducts:

   480 "\<lbrakk>x10 = x20; P10 TYP TYP;

   481  \<And>A A' K x K' x'.

   482     \<lbrakk>A = A'; P20 A A';

   483      \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>

   484           (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>

   485     \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');

   486  \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);

   487  \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');

   488  \<And>A A' B x B' x'.

   489     \<lbrakk>A = A'; P20 A A';

   490      \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>

   491           (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>

   492     \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');

   493  \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);

   494  \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');

   495  \<And>A A' M x M' x'.

   496     \<lbrakk>A = A'; P20 A A';

   497      \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>

   498           (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>

   499     \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>

   500 \<Longrightarrow> P10 x10 x20"

   501 "\<lbrakk>x30 = x40; P10 TYP TYP;

   502  \<And>A A' K x K' x'.

   503     \<lbrakk>A = A'; P20 A A';

   504      \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>

   505           (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>

   506     \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');

   507  \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);

   508  \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');

   509  \<And>A A' B x B' x'.

   510     \<lbrakk>A = A'; P20 A A';

   511      \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>

   512           (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>

   513     \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');

   514  \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);

   515  \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');

   516  \<And>A A' M x M' x'.

   517     \<lbrakk>A = A'; P20 A A';

   518      \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>

   519           (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>

   520     \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>

   521  \<Longrightarrow> P20 x30 x40"

   522 "\<lbrakk>x50 = x60; P10 TYP TYP;

   523  \<And>A A' K x K' x'.

   524     \<lbrakk>A = A'; P20 A A';

   525      \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>

   526           (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>

   527     \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');

   528  \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);

   529  \<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');

   530  \<And>A A' B x B' x'.

   531     \<lbrakk>A = A'; P20 A A';

   532      \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>

   533           (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>

   534     \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');

   535  \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);

   536  \<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');

   537  \<And>A A' M x M' x'.

   538     \<lbrakk>A = A'; P20 A A';

   539      \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>

   540           (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>

   541     \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>

   542 \<Longrightarrow> P30 x50 x60"

   543 by (lifting akind_aty_atrm.inducts)

   544 

   545 lemma KIND_TY_TRM_INJECT:

   546   "(TYP) = (TYP) = True"

   547   "(KPI A x K) = (KPI A' x' K') = (A = A' \<and> (\<exists>pi. (fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and> (fv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) = K' \<and> (pi \<bullet> x) = x')))"

   548   "(TCONST i) = (TCONST j) = (i = j)"

   549   "(TAPP A M) = (TAPP A' M') = (A = A' \<and> M = M')"

   550   "(TPI A x B) = (TPI A' x' B') = ((A = A') \<and> (\<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and> (fv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) = B' \<and> (pi \<bullet> x) = x'))"

   551   "(CONS i) = (CONS j) = (i = j)"

   552   "(VAR x) = (VAR y) = (x = y)"

   553   "(APP M N) = (APP M' N') = (M = M' \<and> N = N')"

   554   "(LAM A x M) = (LAM A' x' M') = (A = A' \<and> (\<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and> (fv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) = M' \<and> (pi \<bullet> x) = x'))"

   555 by (lifting akind_aty_atrm_inj)

   556 

   557 lemma fv_kind_ty_trm:

   558  "fv_kind TYP = {}"

   559  "fv_kind (KPI A x K) = fv_ty A \<union> (fv_kind K - {atom x})"

   560  "fv_ty (TCONST i) = {atom i}"

   561  "fv_ty (TAPP A M) = fv_ty A \<union> fv_trm M"

   562  "fv_ty (TPI A x B) = fv_ty A \<union> (fv_ty B - {atom x})"

   563  "fv_trm (CONS i) = {atom i}"

   564  "fv_trm (VAR x) = {atom x}"

   565  "fv_trm (APP M N) = fv_trm M \<union> fv_trm N"

   566  "fv_trm (LAM A x M) = fv_ty A \<union> (fv_trm M - {atom x})"

   567 by(lifting rfv_kind_rfv_ty_rfv_trm.simps)

   568 

   569 lemma fv_eqvt:

   570  "(p \<bullet> fv_kind t1) = fv_kind (p \<bullet> t1)"

   571  "(p \<bullet> fv_ty t2) = fv_ty (p \<bullet> t2)"

   572  "(p \<bullet> fv_trm t3) = fv_trm (p \<bullet> t3)"

   573 by(lifting rfv_eqvt)

   574 

   575 lemma supp_fv:

   576  "fv_kind t1 = supp t1"

   577  "fv_ty t2 = supp t2"

   578  "fv_trm t3 = supp t3"

   579 apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)

   580 apply (simp_all add: fv_kind_ty_trm)

   581 apply (simp_all add: supp_def)

   582 sorry

   583 

   584 lemma

   585 "(supp ((a \<rightleftharpoons> b) \<bullet> (K::KIND)) - {atom ((a \<rightleftharpoons> b) \<bullet> (x::name))} = supp K - {atom x} \<longrightarrow>

   586 (a \<rightleftharpoons> b) \<bullet> A = (A::TY) \<longrightarrow> (\<forall>pi\<Colon>perm. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> K = K \<longrightarrow> (supp K - {atom x}) \<sharp>* pi \<longrightarrow> pi \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> x)) =

   587 (supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)} = supp K - {atom x} \<and>

   588 (\<exists>pi\<Colon>perm. (supp ((a \<rightleftharpoons> b) \<bullet> K) - {atom ((a \<rightleftharpoons> b) \<bullet> x)}) \<sharp>* pi \<and> pi \<bullet> (a \<rightleftharpoons> b) \<bullet> K = K) \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> A \<noteq> A)"

   589 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}")

   591 apply simp_all

   592 sorry

   593 

   594 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"

   595 apply (subst supp_Pair[symmetric])

   596 unfolding supp_def

   597 apply (simp add: permute_set_eq)

   598 apply(subst abs_eq)

   599 apply(subst KIND_TY_TRM_INJECT)

   600 apply(simp only: supp_fv)

   601 apply simp

   602 apply (unfold supp_def)

   603 sorry

   604 

   605 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"

   606 apply(subst supp_kpi_pre)

   607 thm supp_Abs

   608 (*apply(simp add: supp_Abs)*)

   609 sorry

   610 

   611 lemma supp_kind_ty_trm:

   612  "supp TYP = {}"

   613  "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"

   614  "supp (TCONST i) = {atom i}"

   615  "supp (TAPP A M) = supp A \<union> supp M"

   616  "supp (TPI A x B) = supp A \<union> (supp B - {atom x})"

   617  "supp (CONS i) = {atom i}"

   618  "supp (VAR x) = {atom x}"

   619  "supp (APP M N) = supp M \<union> supp N"

   620  "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"

   621 apply -

   622 apply (simp add: supp_def)

   623 apply (simp add: supp_kpi)

   624 apply (simp add: supp_def) (* need ty.distinct lifted *)

   625 sorry

   626