Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Nominal/LFex.thy
changeset 1027 163d6917af62
parent 1022 cc5830c452c4
child 1036 aaac8274f08c
equal deleted inserted replaced
1026:278253330b6a 1027:163d6917af62 
    78     akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
 
    78     akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
 
    79 and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
 
    79 and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
 
    80 and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
 
    80 and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
 
    81 where
 
    81 where
 
    82   a1: "(Type) \<approx>ki (Type)"
 
    82   a1: "(Type) \<approx>ki (Type)"
 
    83 | a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')"
 
    83 | a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
 
    84 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
 
    84 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
 
    85 | a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
 
    85 | a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
 
    86 | a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')"
 
    86 | a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>ty (TPi A' b B')"
 
    87 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
 
    87 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
 
    88 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
 
    88 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
 
    89 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
 
    89 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
 
    90 | a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')"
 
    90 | a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
 
    91 
       
    92 (*
 
       
    93 function(sequential)
 
       
    94     akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
 
       
    95 and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
 
       
    96 and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
 
       
    97 where
 
       
    98   a1: "(Type) \<approx>ki (Type) = True"
 
       
    99 | a2: "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
 
       
   100 | "_ \<approx>ki _ = False"
 
       
   101 | a3: "(TConst i) \<approx>ty (TConst j) = (i = j)"
 
       
   102 | a4: "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
 
       
   103 | a5: "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
 
       
   104 | "_ \<approx>ty _ = False"
 
       
   105 | a6: "(Const i) \<approx>tr (Const j) = (i = j)"
 
       
   106 | a7: "(Var x) \<approx>tr (Var y) = (x = y)"
 
       
   107 | a8: "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
 
       
   108 | a9: "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
 
       
   109 | "_ \<approx>tr _ = False"
 
       
   110 apply (pat_completeness)
 
       
   111 apply simp_all
 
       
   112 done
 
       
   113 termination
 
       
   114 by (size_change)
 
       
   115 *)
 
       
   116 
    91 
   117 lemma akind_aty_atrm_inj:
 
    92 lemma akind_aty_atrm_inj:
 
   118   "(Type) \<approx>ki (Type) = True"
 
    93   "(Type) \<approx>ki (Type) = True"
 
   119   "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"
 
    94   "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>ty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K')))"
 
   120   "(TConst i) \<approx>ty (TConst j) = (i = j)"
 
    95   "(TConst i) \<approx>ty (TConst j) = (i = j)"
 
   121   "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
 
    96   "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
 
   122   "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"
 
    97   "((TPi A a B) \<approx>ty (TPi A' b B')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))))"
 
   123   "(Const i) \<approx>tr (Const j) = (i = j)"
 
    98   "(Const i) \<approx>tr (Const j) = (i = j)"
 
   124   "(Var x) \<approx>tr (Var y) = (x = y)"
 
    99   "(Var x) \<approx>tr (Var y) = (x = y)"
 
   125   "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
 
   100   "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
 
   126   "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"
 
   101   "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))))"
 
   127 apply -
 
   102 apply -
 
   128 apply (simp add: akind_aty_atrm.intros)
 
   103 apply (simp add: akind_aty_atrm.intros)
 
   129 
   104 
   130 apply rule apply (erule akind.cases) apply simp apply blast
 
   105 apply rule apply (erule akind.cases) apply simp apply blast
 
   131 apply (simp only: akind_aty_atrm.intros)
 
   106 apply (simp only: akind_aty_atrm.intros)
 
   165   "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
 
   140   "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
 
   166   "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
 
   141   "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
 
   167   "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
 
   142   "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
 
   168 apply(induct rule: akind_aty_atrm.inducts)
 
   143 apply(induct rule: akind_aty_atrm.inducts)
 
   169 apply (simp_all add: akind_aty_atrm.intros)
 
   144 apply (simp_all add: akind_aty_atrm.intros)
 
   170 apply(rule a2)
 
   145 apply (simp_all add: akind_aty_atrm_inj)
 
   171 apply simp
 
   146 apply (rule alpha_gen_atom_eqvt)
 
   172 apply(erule conjE)
 
   147 apply (simp add: rfv_eqvt)
 
   173 apply(erule exE)
 
   148 apply assumption
 
   174 apply(erule conjE)
 
   149 apply (rule alpha_gen_atom_eqvt)
 
   175 apply(rule_tac x="pi \<bullet> pia" in exI)
 
   150 apply (simp add: rfv_eqvt)
 
   176 apply(rule conjI)
 
   151 apply assumption
 
   177 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
 
   152 apply (rule alpha_gen_atom_eqvt)
 
   178 apply(simp add: eqvts atom_eqvt)
 
   153 apply (simp add: rfv_eqvt)
 
   179 apply(rule conjI)
 
   154 apply assumption
 
   180 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
 
       
   181 apply(simp add: eqvts atom_eqvt)
 
       
   182 apply(simp add: permute_eqvt[symmetric])
 
       
   183 apply(rule a5)
 
       
   184 apply simp
 
       
   185 apply(erule conjE)
 
       
   186 apply(erule exE)
 
       
   187 apply(erule conjE)
 
       
   188 apply(rule_tac x="pi \<bullet> pia" in exI)
 
       
   189 apply(rule conjI)
 
       
   190 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
 
       
   191 apply(simp add: eqvts atom_eqvt)
 
       
   192 apply(rule conjI)
 
       
   193 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
 
       
   194 apply(simp add: eqvts atom_eqvt)
 
       
   195 apply(simp add: permute_eqvt[symmetric])
 
       
   196 apply(rule a9)
 
       
   197 apply simp
 
       
   198 apply(erule conjE)
 
       
   199 apply(erule exE)
 
       
   200 apply(erule conjE)
 
       
   201 apply(rule_tac x="pi \<bullet> pia" in exI)
 
       
   202 apply(rule conjI)
 
       
   203 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
 
       
   204 apply(simp add: eqvts atom_eqvt)
 
       
   205 apply(rule conjI)
 
       
   206 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
 
       
   207 apply(simp add: eqvts atom_eqvt)
 
       
   208 apply(simp add: permute_eqvt[symmetric])
 
       
   209 done
 
   155 done
 
   210 
   156 
   211 lemma al_refl:
 
   157 lemma al_refl:
 
   212   fixes K::"kind" 
   158   fixes K::"kind" 
   213   and   A::"ty"
 
   159   and   A::"ty"
 
   218   apply(induct K and A and M rule: kind_ty_trm.inducts)
 
   164   apply(induct K and A and M rule: kind_ty_trm.inducts)
 
   219   apply(auto intro: akind_aty_atrm.intros)
 
   165   apply(auto intro: akind_aty_atrm.intros)
 
   220   apply (rule a2)
 
   166   apply (rule a2)
 
   221   apply auto
 
   167   apply auto
 
   222   apply(rule_tac x="0" in exI)
 
   168   apply(rule_tac x="0" in exI)
 
   223   apply(simp_all add: fresh_star_def fresh_zero_perm)
 
   169   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
 
   224   apply (rule a5)
 
   170   apply (rule a5)
 
   225   apply auto
 
   171   apply auto
 
   226   apply(rule_tac x="0" in exI)
 
   172   apply(rule_tac x="0" in exI)
 
   227   apply(simp_all add: fresh_star_def fresh_zero_perm)
 
   173   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
 
   228   apply (rule a9)
 
   174   apply (rule a9)
 
   229   apply auto
 
   175   apply auto
 
   230   apply(rule_tac x="0" in exI)
 
   176   apply(rule_tac x="0" in exI)
 
   231   apply(simp_all add: fresh_star_def fresh_zero_perm)
 
   177   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
 
       
   178   done
 
       
   179 
       
   180 lemma al_sym:
 
       
   181   fixes K K'::"kind" and A A'::"ty" and M M'::"trm"
 
       
   182   shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"
 
       
   183   and   "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A"
 
       
   184   and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"
 
       
   185   apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts)
 
       
   186   apply(simp_all add: akind_aty_atrm.intros)
 
       
   187   apply (simp_all add: akind_aty_atrm_inj)
 
       
   188   apply(rule alpha_gen_atom_sym)
 
       
   189   apply(rule alpha_eqvt)
 
       
   190   apply(assumption)+
 
       
   191   apply(rule alpha_gen_atom_sym)
 
       
   192   apply(rule alpha_eqvt)
 
       
   193   apply(assumption)+
 
       
   194   apply(rule alpha_gen_atom_sym)
 
       
   195   apply(rule alpha_eqvt)
 
       
   196   apply(assumption)+
 
       
   197   done
 
       
   198 
       
   199 lemma al_trans:
 
       
   200   fixes K K' K''::"kind" and A A' A''::"ty" and M M' M''::"trm"
 
       
   201   shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"
 
       
   202   and   "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A'' \<Longrightarrow> A \<approx>ty A''"
 
       
   203   and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''"
 
       
   204   apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: akind_aty_atrm.inducts)
 
       
   205   apply(simp_all add: akind_aty_atrm.intros)
 
       
   206   apply(erule akind.cases)
 
       
   207   apply(simp_all add: akind_aty_atrm.intros)
 
       
   208   apply(simp add: akind_aty_atrm_inj)
 
       
   209   apply(rule alpha_gen_atom_trans)
 
       
   210   apply(rule alpha_eqvt)
 
       
   211   apply(assumption)+
 
       
   212   apply(rotate_tac 4)
 
       
   213   apply(erule aty.cases)
 
       
   214   apply(simp_all add: akind_aty_atrm.intros)
 
       
   215   apply(rotate_tac 3)
 
       
   216   apply(erule aty.cases)
 
       
   217   apply(simp_all add: akind_aty_atrm.intros)
 
       
   218   apply(simp add: akind_aty_atrm_inj)
 
       
   219   apply(rule alpha_gen_atom_trans)
 
       
   220   apply(rule alpha_eqvt)
 
       
   221   apply(assumption)+
 
       
   222   apply(rotate_tac 4)
 
       
   223   apply(erule atrm.cases)
 
       
   224   apply(simp_all add: akind_aty_atrm.intros)
 
       
   225   apply(rotate_tac 3)
 
       
   226   apply(erule atrm.cases)
 
       
   227   apply(simp_all add: akind_aty_atrm.intros)
 
       
   228   apply(simp add: akind_aty_atrm_inj)
 
       
   229   apply(rule alpha_gen_atom_trans)
 
       
   230   apply(rule alpha_eqvt)
 
       
   231   apply(assumption)+
 
   232   done
 
   232   done
 
   233 
   233 
   234 lemma alpha_equivps:
 
   234 lemma alpha_equivps:
 
   235   shows "equivp akind"
 
   235   shows "equivp akind"
 
   236   and   "equivp aty"
 
   236   and   "equivp aty"
 
   237   and   "equivp atrm"
 
   237   and   "equivp atrm"
 
   238 sorry
 
   238   apply(rule equivpI)
 
       
   239   unfolding reflp_def symp_def transp_def
 
       
   240   apply(auto intro: al_refl al_sym al_trans)
 
       
   241   apply(rule equivpI)
 
       
   242   unfolding reflp_def symp_def transp_def
 
       
   243   apply(auto intro: al_refl al_sym al_trans)
 
       
   244   apply(rule equivpI)
 
       
   245   unfolding reflp_def symp_def transp_def
 
       
   246   apply(auto intro: al_refl al_sym al_trans)
 
       
   247   done
 
   239 
   248 
   240 quotient_type KIND = kind / akind
 
   249 quotient_type KIND = kind / akind
 
   241   by (rule alpha_equivps)
 
   250   by (rule alpha_equivps)
 
   242 
   251 
   243 quotient_type
 
   252 quotient_type
 
   310 lemma alpha_rfv:
 
   319 lemma alpha_rfv:
 
   311   shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>
 
   320   shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>
 
   312      (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
 
   321      (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
 
   313      (t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"
 
   322      (t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"
 
   314   apply(rule akind_aty_atrm.induct)
 
   323   apply(rule akind_aty_atrm.induct)
 
   315   apply(simp_all)
 
   324   apply(simp_all add: alpha_gen)
 
   316   done
 
   325   done
 
   317 
   326 
   318 lemma perm_rsp[quot_respect]:
 
   327 lemma perm_rsp[quot_respect]:
 
   319   "(op = ===> akind ===> akind) permute permute"
 
   328   "(op = ===> akind ===> akind) permute permute"
 
   320   "(op = ===> aty ===> aty) permute permute"
 
   329   "(op = ===> aty ===> aty) permute permute"
 
   338   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   347   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   339 
   348 
   340 lemma kpi_rsp[quot_respect]: 
   349 lemma kpi_rsp[quot_respect]: 
   341   "(aty ===> op = ===> akind ===> akind) KPi KPi"
 
   350   "(aty ===> op = ===> akind ===> akind) KPi KPi"
 
   342   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
 
   351   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
 
   343   apply (rule a2) apply simp
 
   352   apply (rule a2) apply assumption
 
   344   apply (rule_tac x="0" in exI)
 
   353   apply (rule_tac x="0" in exI)
 
   345   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
 
   354   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
 
   346   done
 
   355   done
 
   347 
   356 
   348 lemma tpi_rsp[quot_respect]: 
   357 lemma tpi_rsp[quot_respect]: 
   349   "(aty ===> op = ===> aty ===> aty) TPi TPi"
 
   358   "(aty ===> op = ===> aty ===> aty) TPi TPi"
 
   350   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
 
   359   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
 
   351   apply (rule a5) apply simp
 
   360   apply (rule a5) apply assumption
 
   352   apply (rule_tac x="0" in exI)
 
   361   apply (rule_tac x="0" in exI)
 
   353   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
 
   362   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
 
   354   done
 
   363   done
 
   355 lemma lam_rsp[quot_respect]: 
   364 lemma lam_rsp[quot_respect]: 
   356   "(aty ===> op = ===> atrm ===> atrm) Lam Lam"
 
   365   "(aty ===> op = ===> atrm ===> atrm) Lam Lam"
 
   357   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
 
   366   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
 
   358   apply (rule a9) apply simp
 
   367   apply (rule a9) apply assumption
 
   359   apply (rule_tac x="0" in exI)
 
   368   apply (rule_tac x="0" in exI)
 
   360   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
 
   369   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
 
   361   done
 
   370   done
 
   362 
   371 
   363 lemma rfv_ty_rsp[quot_respect]: 
   372 lemma rfv_ty_rsp[quot_respect]: 
   364   "(aty ===> op =) rfv_ty rfv_ty"
 
   373   "(aty ===> op =) rfv_ty rfv_ty"
 
   365   by (simp add: alpha_rfv)
 
   374   by (simp add: alpha_rfv)
 
   368   by (simp add: alpha_rfv)
 
   377   by (simp add: alpha_rfv)
 
   369 lemma rfv_trm_rsp[quot_respect]:
 
   378 lemma rfv_trm_rsp[quot_respect]:
 
   370   "(atrm ===> op =) rfv_trm rfv_trm"
 
   379   "(atrm ===> op =) rfv_trm rfv_trm"
 
   371   by (simp add: alpha_rfv)
 
   380   by (simp add: alpha_rfv)
 
   372 
   381 
   373 lemma KIND_TY_TRM_induct: "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
 
   382 thm kind_ty_trm.induct
 
       
   383 
       
   384 lemma KIND_TY_TRM_induct: 
       
   385   fixes P10 :: "KIND \<Rightarrow> bool" and P20 :: "TY \<Rightarrow> bool" and P30 :: "TRM \<Rightarrow> bool"
 
       
   386   shows
 
       
   387 "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
 
   374  \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
 
   388  \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
 
   375  \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
 
   389  \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
 
   376  \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
 
   390  \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
 
   377  \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
 
   391  \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
 
   378 \<Longrightarrow> P10 kind \<and> P20 ty \<and> P30 trm"
 
   392 \<Longrightarrow> P10 kind \<and> P20 ty \<and> P30 trm"
 
   450 apply (simp_all add: perm_zero_ok perm_add_ok)
 
   464 apply (simp_all add: perm_zero_ok perm_add_ok)
 
   451 done
 
   465 done
 
   452 
   466 
   453 end
 
   467 end
 
   454 
   468 
   455 lemma "\<lbrakk>P10 TYP TYP;
 
       
   456  \<And>A A' K x K' x'.
 
       
   457     \<lbrakk>(A :: TY) = A'; P20 A A';
 
       
   458      \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
 
       
   459           (fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>
 
       
   460     \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
 
       
   461  \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
 
       
   462  \<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');
 
       
   463  \<And>A A' B x B' x'.
 
       
   464     \<lbrakk>A = A'; P20 A A';
 
       
   465      \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
 
       
   466           (fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>
 
       
   467     \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
 
       
   468  \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
 
       
   469  \<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');
 
       
   470  \<And>A A' M x M' x'.
 
       
   471     \<lbrakk>A = A'; P20 A A';
 
       
   472      \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
 
       
   473           (fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>
 
       
   474     \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
 
       
   475 \<Longrightarrow> (x10 = x20 \<longrightarrow> P10 x10 x20) \<and>
 
       
   476    (x30 = x40 \<longrightarrow> P20 x30 x40) \<and> (x50 = x60 \<longrightarrow> P30 x50 x60)"
 
       
   477 by (lifting akind_aty_atrm.induct)
 
       
   478 
       
   479 lemma AKIND_ATY_ATRM_inducts:
 
   469 lemma AKIND_ATY_ATRM_inducts:
 
   480 "\<lbrakk>x10 = x20; P10 TYP TYP;
 
   470 "\<lbrakk>z1 = z2; P1 TYP TYP;
 
   481  \<And>A A' K x K' x'.
 
   471  \<And>A A' a K b K'.
 
   482     \<lbrakk>A = A'; P20 A A';
 
   472     \<lbrakk>A = A'; P2 A A';
 
   483      \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
 
   473      \<exists>pi. ({atom a},
 
   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>
 
   474            K) \<approx>gen (\<lambda>x1 x2.
 
   485     \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
 
   475                       x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
 
   486  \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
 
   476     \<Longrightarrow> P1 (KPI A a K) (KPI A' b K');
 
   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');
 
   477  \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
 
   488  \<And>A A' B x B' x'.
 
   478  \<And>A A' M M'.
 
   489     \<lbrakk>A = A'; P20 A A';
 
   479     \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
 
   490      \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
 
   480     \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
 
   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>
 
   481  \<And>A A' a B b B'.
 
   492     \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
 
   482     \<lbrakk>A = A'; P2 A A';
 
   493  \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
 
   483      \<exists>pi. ({atom a},
 
   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');
 
   484            B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
 
   495  \<And>A A' M x M' x'.
 
   485     \<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
 
   496     \<lbrakk>A = A'; P20 A A';
 
   486  \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
 
   497      \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
 
   487  \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
 
   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>
 
   488  \<And>M M' N N'.
 
   499     \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
 
   489     \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
 
   500 \<Longrightarrow> P10 x10 x20"
 
   490     \<Longrightarrow> P3 (APP M N) (APP M' N');
 
   501 "\<lbrakk>x30 = x40; P10 TYP TYP;
 
   491  \<And>A A' a M b M'.
 
   502  \<And>A A' K x K' x'.
 
   492     \<lbrakk>A = A'; P2 A A';
 
   503     \<lbrakk>A = A'; P20 A A';
 
   493      \<exists>pi. ({atom a},
 
   504      \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
 
   494            M) \<approx>gen (\<lambda>x1 x2.
 
   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>
 
   495                       x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
 
   506     \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
 
   496     \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
 
   507  \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
 
   497 \<Longrightarrow> P1 z1 z2"
 
   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');
 
   498 "\<lbrakk>z3 = z4; P1 TYP TYP;
 
   509  \<And>A A' B x B' x'.
 
   499  \<And>A A' a K b K'.
 
   510     \<lbrakk>A = A'; P20 A A';
 
   500     \<lbrakk>A = A'; P2 A A';
 
   511      \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
 
   501      \<exists>pi. ({atom a},
 
   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>
 
   502            K) \<approx>gen (\<lambda>x1 x2.
 
   513     \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
 
   503                       x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
 
   514  \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
 
   504     \<Longrightarrow> P1 (KPI A a K) (KPI A' b K');
 
   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');
 
   505  \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
 
   516  \<And>A A' M x M' x'.
 
   506  \<And>A A' M M'.
 
   517     \<lbrakk>A = A'; P20 A A';
 
   507     \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
 
   518      \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
 
   508     \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
 
   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>
 
   509  \<And>A A' a B b B'.
 
   520     \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
 
   510     \<lbrakk>A = A'; P2 A A';
 
   521  \<Longrightarrow> P20 x30 x40"
 
   511      \<exists>pi. ({atom a},
 
   522 "\<lbrakk>x50 = x60; P10 TYP TYP;
 
   512            B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
 
   523  \<And>A A' K x K' x'.
 
   513     \<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
 
   524     \<lbrakk>A = A'; P20 A A';
 
   514  \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
 
   525      \<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
 
   515  \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
 
   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>
 
   516  \<And>M M' N N'.
 
   527     \<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
 
   517     \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
 
   528  \<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
 
   518     \<Longrightarrow> P3 (APP M N) (APP M' N');
 
   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');
 
   519  \<And>A A' a M b M'.
 
   530  \<And>A A' B x B' x'.
 
   520     \<lbrakk>A = A'; P2 A A';
 
   531     \<lbrakk>A = A'; P20 A A';
 
   521      \<exists>pi. ({atom a},
 
   532      \<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
 
   522            M) \<approx>gen (\<lambda>x1 x2.
 
   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>
 
   523                       x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
 
   534     \<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
 
   524     \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
 
   535  \<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
 
   525 \<Longrightarrow> P2 z3 z4"
 
   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');
 
   526 "\<lbrakk>z5 = z6; P1 TYP TYP;
 
   537  \<And>A A' M x M' x'.
 
   527  \<And>A A' a K b K'.
 
   538     \<lbrakk>A = A'; P20 A A';
 
   528     \<lbrakk>A = A'; P2 A A';
 
   539      \<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
 
   529      \<exists>pi. ({atom a},
 
   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>
 
   530            K) \<approx>gen (\<lambda>x1 x2.
 
   541     \<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
 
   531                       x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
 
   542 \<Longrightarrow> P30 x50 x60"
 
   532     \<Longrightarrow> P1 (KPI A a K) (KPI A' b K');
 
   543 by (lifting akind_aty_atrm.inducts)
 
   533  \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
 
   544 
   534  \<And>A A' M M'.
 
       
   535     \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
 
       
   536     \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
 
       
   537  \<And>A A' a B b B'.
 
       
   538     \<lbrakk>A = A'; P2 A A';
 
       
   539      \<exists>pi. ({atom a},
 
       
   540            B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
 
       
   541     \<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
 
       
   542  \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
 
       
   543  \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
 
       
   544  \<And>M M' N N'.
 
       
   545     \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
 
       
   546     \<Longrightarrow> P3 (APP M N) (APP M' N');
 
       
   547  \<And>A A' a M b M'.
 
       
   548     \<lbrakk>A = A'; P2 A A';
 
       
   549      \<exists>pi. ({atom a},
 
       
   550            M) \<approx>gen (\<lambda>x1 x2.
 
       
   551                       x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
 
       
   552     \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
 
       
   553 \<Longrightarrow> P3 z5 z6"
 
       
   554 unfolding alpha_gen
 
       
   555 apply (lifting akind_aty_atrm.inducts[unfolded alpha_gen])
 
       
   556 done
 
       
   557 
       
   558 thm akind_aty_atrm_inj
 
   545 lemma KIND_TY_TRM_INJECT:
 
   559 lemma KIND_TY_TRM_INJECT:
 
   546   "(TYP) = (TYP) = True"
 
   560   "(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')))"
 
   561   "(KPI A x K) = (KPI A' x' K') = (A = A' \<and> (\<exists>pi. ({atom x}, K) \<approx>gen (op =) fv_kind pi ({atom x'}, K')))"
 
   548   "(TCONST i) = (TCONST j) = (i = j)"
 
   562   "(TCONST i) = (TCONST j) = (i = j)"
 
   549   "(TAPP A M) = (TAPP A' M') = (A = A' \<and> M = M')"
 
   563   "(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'))"
 
   564   "(TPI A x B) = (TPI A' x' B') = (A = A' \<and> (\<exists>pi. ({atom x}, B) \<approx>gen (op =) fv_ty pi ({atom x'}, B')))"
 
   551   "(CONS i) = (CONS j) = (i = j)"
 
   565   "(CONS i) = (CONS j) = (i = j)"
 
   552   "(VAR x) = (VAR y) = (x = y)"
 
   566   "(VAR x) = (VAR y) = (x = y)"
 
   553   "(APP M N) = (APP M' N') = (M = M' \<and> N = N')"
 
   567   "(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'))"
 
   568   "(LAM A x M) = (LAM A' x' M') = (A = A' \<and> (\<exists>pi. ({atom x}, M) \<approx>gen (op =) fv_trm pi ({atom x'}, M')))"
 
   555 by (lifting akind_aty_atrm_inj)
 
   569 unfolding alpha_gen
 
       
   570 by (lifting akind_aty_atrm_inj[unfolded alpha_gen])
 
   556 
   571 
   557 lemma fv_kind_ty_trm:
 
   572 lemma fv_kind_ty_trm:
 
   558  "fv_kind TYP = {}"
 
   573  "fv_kind TYP = {}"
 
   559  "fv_kind (KPI A x K) = fv_ty A \<union> (fv_kind K - {atom x})"
 
   574  "fv_kind (KPI A x K) = fv_ty A \<union> (fv_kind K - {atom x})"
 
   560  "fv_ty (TCONST i) = {atom i}"
 
   575  "fv_ty (TCONST i) = {atom i}"
 
   629  "fv_ty t2 = supp t2"
 
   644  "fv_ty t2 = supp t2"
 
   630  "fv_trm t3 = supp t3"
 
   645  "fv_trm t3 = supp t3"
 
   631 apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)
 
   646 apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)
 
   632 apply (simp_all add: supp_kind_ty_trm_easy)
 
   647 apply (simp_all add: supp_kind_ty_trm_easy)
 
   633 apply (simp_all add: fv_kind_ty_trm)
 
   648 apply (simp_all add: fv_kind_ty_trm)
 
   634 apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abst {atom name} kind)")
 
   649 apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abs {atom name} kind)")
 
   635 apply(simp add: supp_Abst Set.Un_commute)
 
   650 apply(simp add: supp_Abs Set.Un_commute)
 
   636 apply(simp (no_asm) add: supp_def)
 
   651 apply(simp (no_asm) add: supp_def)
 
   637 apply(simp add: KIND_TY_TRM_INJECT)
 
   652 apply(simp add: KIND_TY_TRM_INJECT)
 
   638 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
 
   653 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] alpha_gen)
 
   639 apply(simp add: abs_eq alpha_gen)
 
   654 apply(simp add: Abs_eq_iff alpha_gen)
 
   640 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
 
   655 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
 
   641 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric])
 
       
   642 apply (fold supp_def)
 
       
   643 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
 
   656 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
 
   644 apply (rule refl)
 
   657 apply (rule refl)
 
   645 apply(subst Set.Un_commute)
 
       
   646 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
 
       
   647 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
 
       
   648 apply (rule refl)
 
       
   649 prefer 2
 
       
   650 apply(simp add: eqvts supp_eqvt atom_eqvt)
 
       
   651 sorry (* Stuck *)
 
   658 sorry (* Stuck *)
 
   652 
   659 
   653 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abst {atom x} K)) \<union> supp A"
 
   660 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"
 
   654 (*apply (subst supp_Pair[symmetric])*)
 
   661 (*apply (subst supp_Pair[symmetric])*)
 
   655 unfolding supp_def
 
   662 unfolding supp_def
 
   656 apply (simp add: permute_set_eq)
 
   663 apply (simp add: permute_set_eq)
 
   657 apply(subst abs_eq)
 
   664 apply(subst Abs_eq_iff)
 
   658 apply(subst KIND_TY_TRM_INJECT)
 
   665 apply(subst KIND_TY_TRM_INJECT)
 
   659 apply(simp only: supp_fv)
 
   666 apply(simp only: alpha_gen supp_fv)
 
   660 apply simp
 
   667 apply simp
 
   661 apply (simp_all add: Collect_imp_eq Collect_neg_eq)
 
   668 apply (simp_all add: Collect_imp_eq Collect_neg_eq)
 
   662 apply(subst Set.Un_commute)
 
   669 apply(subst Set.Un_commute)
 
   663 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
 
   670 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
 
   664 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
 
   671 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
 
   665 apply (rule refl)
 
   672 apply (rule refl)
 
   666 prefer 2
 
   673 prefer 2
 
   667 apply (rule refl)
 
   674 apply (rule refl)
 
   668 sorry (* Stuck *)
 
   675 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
 
       
   676 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*} )
 
       
   677 apply (rule refl)
 
       
   678 apply (simp_all)
 
       
   679 apply (simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric])
 
       
   680 sorry (* should be true... *)
 
   669 
   681 
   670 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
 
   682 lemma supp_kpi: "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
 
   671 apply(subst supp_kpi_pre)
 
   683 apply(subst supp_kpi_pre)
 
   672 apply(subst supp_Abst)
 
   684 apply(subst supp_Abs)
 
   673 apply (simp only: Set.Un_commute)
 
   685 apply (simp only: Set.Un_commute)
 
   674 done
 
   686 done
 
   675 
   687 
   676 lemma supp_kind_ty_trm:
 
   688 lemma supp_kind_ty_trm:
 
   677  "supp TYP = {}"
 
   689  "supp TYP = {}"
nominal2