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 1237 38eb2bd9ad3a
parent 1236 ca3c69545a78
child 1238 c88159ffa7a3
equal deleted inserted replaced
1236:ca3c69545a78 1237:38eb2bd9ad3a 
    67   [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
 
    67   [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
 
    68    [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
 
    68    [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
 
    69    [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
 
    69    [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
 
    70 notation
 
    70 notation
 
    71     alpha_rkind  ("_ \<approx>ki _" [100, 100] 100)
 
    71     alpha_rkind  ("_ \<approx>ki _" [100, 100] 100)
 
    72 and alpha_rty    ("_ \<approx>rty _" [100, 100] 100)
 
    72 and alpha_rty    ("_ \<approx>ty _" [100, 100] 100)
 
    73 and alpha_rtrm   ("_ \<approx>tr _" [100, 100] 100)
 
    73 and alpha_rtrm   ("_ \<approx>tr _" [100, 100] 100)
 
    74 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros
 
    74 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros
 
    75 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *}
 
    75 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *}
 
    76 thm alphas_inj
 
    76 thm alphas_inj
 
    77 
    77 
   105 | "fv_rtrm (Var x) = {atom x}"
 
   105 | "fv_rtrm (Var x) = {atom x}"
 
   106 | "fv_rtrm (App M N) = (fv_rtrm M) \<union> (fv_rtrm N)"
 
   106 | "fv_rtrm (App M N) = (fv_rtrm M) \<union> (fv_rtrm N)"
 
   107 | "fv_rtrm (Lam A x M) = (fv_rty A) \<union> ((fv_rtrm M) - {atom x})"
 
   107 | "fv_rtrm (Lam A x M) = (fv_rty A) \<union> ((fv_rtrm M) - {atom x})"
 
   108 
   108 
   109 inductive
 
   109 inductive
 
   110     arkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
 
   110     alpha_rkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
 
   111 and arty   :: "rty \<Rightarrow> rty \<Rightarrow> bool"     ("_ \<approx>rty _" [100, 100] 100)
 
   111 and alpha_rty   :: "rty \<Rightarrow> rty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
 
   112 and artrm  :: "rtrm \<Rightarrow> rtrm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
 
   112 and alpha_rtrm  :: "rtrm \<Rightarrow> rtrm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
 
   113 where
 
   113 where
 
   114   a1: "(Type) \<approx>ki (Type)"
 
   114   a1: "(Type) \<approx>ki (Type)"
 
   115 | a2: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, K) \<approx>gen arkind fv_rkind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
 
   115 | a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, K) \<approx>gen alpha_rkind fv_rkind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
 
   116 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>rty (TConst j)"
 
   116 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
 
   117 | a4: "\<lbrakk>A \<approx>rty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>rty (TApp A' M')"
 
   117 | a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
 
   118 | a5: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, B) \<approx>gen arty fv_rty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>rty (TPi A' b B')"
 
   118 | a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, B) \<approx>gen alpha_rty fv_rty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>ty (TPi A' b B')"
 
   119 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
 
   119 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
 
   120 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
 
   120 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
 
   121 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
 
   121 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
 
   122 | a9: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, M) \<approx>gen artrm fv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
 
   122 | a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, M) \<approx>gen alpha_rtrm fv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
 
   123 
   123 
   124 lemma arkind_arty_artrm_inj:
 
   124 lemma alpha_rkind_alpha_rty_alpha_rtrm_inj:
 
   125   "(Type) \<approx>ki (Type) = True"
 
   125   "(Type) \<approx>ki (Type) = True"
 
   126   "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>rty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen arkind fv_rkind pi ({atom b}, K')))"
 
   126   "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>ty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen alpha_rkind fv_rkind pi ({atom b}, K')))"
 
   127   "(TConst i) \<approx>rty (TConst j) = (i = j)"
 
   127   "(TConst i) \<approx>ty (TConst j) = (i = j)"
 
   128   "(TApp A M) \<approx>rty (TApp A' M') = (A \<approx>rty A' \<and> M \<approx>tr M')"
 
   128   "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
 
   129   "((TPi A a B) \<approx>rty (TPi A' b B')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen arty fv_rty pi ({atom b}, B'))))"
 
   129   "((TPi A a B) \<approx>ty (TPi A' b B')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen alpha_rty fv_rty pi ({atom b}, B'))))"
 
   130   "(Const i) \<approx>tr (Const j) = (i = j)"
 
   130   "(Const i) \<approx>tr (Const j) = (i = j)"
 
   131   "(Var x) \<approx>tr (Var y) = (x = y)"
 
   131   "(Var x) \<approx>tr (Var y) = (x = y)"
 
   132   "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
 
   132   "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
 
   133   "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen artrm fv_rtrm pi ({atom b}, M'))))"
 
   133   "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen alpha_rtrm fv_rtrm pi ({atom b}, M'))))"
 
   134 apply -
 
   134 apply -
 
   135 apply (simp add: arkind_arty_artrm.intros)
 
   135 apply (simp add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   136 
   136 
   137 apply rule apply (erule arkind.cases) apply simp apply blast
 
   137 apply rule apply (erule alpha_rkind.cases) apply simp apply blast
 
   138 apply (simp only: arkind_arty_artrm.intros)
 
   138 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   139 
   139 
   140 apply rule apply (erule arty.cases) apply simp apply simp apply simp
 
   140 apply rule apply (erule alpha_rty.cases) apply simp apply simp apply simp
 
   141 apply (simp only: arkind_arty_artrm.intros)
 
   141 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   142 
   142 
   143 apply rule apply (erule arty.cases) apply simp apply simp apply simp
 
   143 apply rule apply (erule alpha_rty.cases) apply simp apply simp apply simp
 
   144 apply (simp only: arkind_arty_artrm.intros)
 
   144 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   145 
   145 
   146 apply rule apply (erule arty.cases) apply simp apply simp apply blast
 
   146 apply rule apply (erule alpha_rty.cases) apply simp apply simp apply blast
 
   147 apply (simp only: arkind_arty_artrm.intros)
 
   147 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   148 
   148 
   149 apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
 
   149 apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
 
   150 apply (simp only: arkind_arty_artrm.intros)
 
   150 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   151 
   151 
   152 apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
 
   152 apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
 
   153 apply (simp only: arkind_arty_artrm.intros)
 
   153 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   154 
   154 
   155 apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
 
   155 apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
 
   156 apply (simp only: arkind_arty_artrm.intros)
 
   156 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   157 
   157 
   158 apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
 
   158 apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
 
   159 apply (simp only: arkind_arty_artrm.intros)
 
   159 apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   160 done
 
   160 done
 
   161 
   161 
   162 lemma rfv_eqvt[eqvt]:
 
   162 lemma rfv_eqvt[eqvt]:
 
   163   "((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))"
 
   163   "((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))"
 
   164   "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))"
 
   164   "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))"
 
   168 apply(simp_all add: permute_set_eq atom_eqvt)
 
   168 apply(simp_all add: permute_set_eq atom_eqvt)
 
   169 done
 
   169 done
 
   170 
   170 
   171 lemma alpha_eqvt:
 
   171 lemma alpha_eqvt:
 
   172   "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
 
   172   "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
 
   173   "t2 \<approx>rty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>rty (pi \<bullet> s2)"
 
   173   "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
 
   174   "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
 
   174   "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
 
   175 apply(induct rule: arkind_arty_artrm.inducts)
 
   175 apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
 
   176 apply (simp_all add: arkind_arty_artrm.intros)
 
   176 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   177 apply (simp_all add: arkind_arty_artrm_inj)
 
   177 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
 
   178 apply (rule alpha_gen_atom_eqvt)
 
   178 apply (rule alpha_gen_atom_eqvt)
 
   179 apply (simp add: rfv_eqvt)
 
   179 apply (simp add: rfv_eqvt)
 
   180 apply assumption
 
   180 apply assumption
 
   181 apply (rule alpha_gen_atom_eqvt)
 
   181 apply (rule alpha_gen_atom_eqvt)
 
   182 apply (simp add: rfv_eqvt)
 
   182 apply (simp add: rfv_eqvt)
 
   189 lemma al_refl:
 
   189 lemma al_refl:
 
   190   fixes K::"rkind" 
   190   fixes K::"rkind" 
   191   and   A::"rty"
 
   191   and   A::"rty"
 
   192   and   M::"rtrm"
 
   192   and   M::"rtrm"
 
   193   shows "K \<approx>ki K"
 
   193   shows "K \<approx>ki K"
 
   194   and   "A \<approx>rty A"
 
   194   and   "A \<approx>ty A"
 
   195   and   "M \<approx>tr M"
 
   195   and   "M \<approx>tr M"
 
   196   apply(induct K and A and M rule: rkind_rty_rtrm.inducts)
 
   196   apply(induct K and A and M rule: rkind_rty_rtrm.inducts)
 
   197   apply(auto intro: arkind_arty_artrm.intros)
 
   197   apply(auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   198   apply (rule a2)
 
   198   apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(2))
 
   199   apply auto
 
   199   apply auto
 
   200   apply(rule_tac x="0" in exI)
 
   200   apply(rule_tac x="0" in exI)
 
   201   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
 
   201   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
 
   202   apply (rule a5)
 
   202   apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(5))
 
   203   apply auto
 
   203   apply auto
 
   204   apply(rule_tac x="0" in exI)
 
   204   apply(rule_tac x="0" in exI)
 
   205   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
 
   205   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
 
   206   apply (rule a9)
 
   206   apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(9))
 
   207   apply auto
 
   207   apply auto
 
   208   apply(rule_tac x="0" in exI)
 
   208   apply(rule_tac x="0" in exI)
 
   209   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
 
   209   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
 
   210   done
 
   210   done
 
   211 
   211 
   212 lemma al_sym:
 
   212 lemma al_sym:
 
   213   fixes K K'::"rkind" and A A'::"rty" and M M'::"rtrm"
 
   213   fixes K K'::"rkind" and A A'::"rty" and M M'::"rtrm"
 
   214   shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"
 
   214   shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"
 
   215   and   "A \<approx>rty A' \<Longrightarrow> A' \<approx>rty A"
 
   215   and   "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A"
 
   216   and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"
 
   216   and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"
 
   217   apply(induct K K' and A A' and M M' rule: arkind_arty_artrm.inducts)
 
   217   apply(induct K K' and A A' and M M' rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
 
   218   apply(simp_all add: arkind_arty_artrm.intros)
 
   218   apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   219   apply (simp_all add: arkind_arty_artrm_inj)
 
   219   apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
 
   220   apply(erule alpha_gen_compose_sym)
 
   220   apply(erule alpha_gen_compose_sym)
 
   221   apply(erule alpha_eqvt)
 
   221   apply(erule alpha_eqvt)
 
   222   apply(erule alpha_gen_compose_sym)
 
   222   apply(erule alpha_gen_compose_sym)
 
   223   apply(erule alpha_eqvt)
 
   223   apply(erule alpha_eqvt)
 
   224   apply(erule alpha_gen_compose_sym)
 
   224   apply(erule alpha_gen_compose_sym)
 
   226   done
 
   226   done
 
   227 
   227 
   228 lemma al_trans:
 
   228 lemma al_trans:
 
   229   fixes K K' K''::"rkind" and A A' A''::"rty" and M M' M''::"rtrm"
 
   229   fixes K K' K''::"rkind" and A A' A''::"rty" and M M' M''::"rtrm"
 
   230   shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"
 
   230   shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"
 
   231   and   "A \<approx>rty A' \<Longrightarrow> A' \<approx>rty A'' \<Longrightarrow> A \<approx>rty A''"
 
   231   and   "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A'' \<Longrightarrow> A \<approx>ty A''"
 
   232   and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''"
 
   232   and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''"
 
   233   apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: arkind_arty_artrm.inducts)
 
   233   apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
 
   234   apply(simp_all add: arkind_arty_artrm.intros)
 
   234   apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   235   apply(erule arkind.cases)
 
   235   apply(erule alpha_rkind.cases)
 
   236   apply(simp_all add: arkind_arty_artrm.intros)
 
   236   apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   237   apply(simp add: arkind_arty_artrm_inj)
 
   237   apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
 
   238   apply(erule alpha_gen_compose_trans)
 
   238   apply(erule alpha_gen_compose_trans)
 
   239   apply(assumption)
 
   239   apply(assumption)
 
   240   apply(erule alpha_eqvt)
 
   240   apply(erule alpha_eqvt)
 
   241   apply(rotate_tac 4)
 
   241   apply(rotate_tac 4)
 
   242   apply(erule arty.cases)
 
   242   apply(erule alpha_rty.cases)
 
   243   apply(simp_all add: arkind_arty_artrm.intros)
 
   243   apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   244   apply(rotate_tac 3)
 
   244   apply(rotate_tac 3)
 
   245   apply(erule arty.cases)
 
   245   apply(erule alpha_rty.cases)
 
   246   apply(simp_all add: arkind_arty_artrm.intros)
 
   246   apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   247   apply(simp add: arkind_arty_artrm_inj)
 
   247   apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
 
   248   apply(erule alpha_gen_compose_trans)
 
   248   apply(erule alpha_gen_compose_trans)
 
   249   apply(assumption)
 
   249   apply(assumption)
 
   250   apply(erule alpha_eqvt)
 
   250   apply(erule alpha_eqvt)
 
   251   apply(rotate_tac 4)
 
   251   apply(rotate_tac 4)
 
   252   apply(erule artrm.cases)
 
   252   apply(erule alpha_rtrm.cases)
 
   253   apply(simp_all add: arkind_arty_artrm.intros)
 
   253   apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   254   apply(rotate_tac 3)
 
   254   apply(rotate_tac 3)
 
   255   apply(erule artrm.cases)
 
   255   apply(erule alpha_rtrm.cases)
 
   256   apply(simp_all add: arkind_arty_artrm.intros)
 
   256   apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   257   apply(simp add: arkind_arty_artrm_inj)
 
   257   apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
 
   258   apply(erule alpha_gen_compose_trans)
 
   258   apply(erule alpha_gen_compose_trans)
 
   259   apply(assumption)
 
   259   apply(assumption)
 
   260   apply(erule alpha_eqvt)
 
   260   apply(erule alpha_eqvt)
 
   261   done
 
   261   done
 
   262 
   262 
   263 lemma alpha_equivps:
 
   263 lemma alpha_equivps:
 
   264   shows "equivp arkind"
 
   264   shows "equivp alpha_rkind"
 
   265   and   "equivp arty"
 
   265   and   "equivp alpha_rty"
 
   266   and   "equivp artrm"
 
   266   and   "equivp alpha_rtrm"
 
   267   apply(rule equivpI)
 
   267   apply(rule equivpI)
 
   268   unfolding reflp_def symp_def transp_def
 
   268   unfolding reflp_def symp_def transp_def
 
   269   apply(auto intro: al_refl al_sym al_trans)
 
   269   apply(auto intro: al_refl al_sym al_trans)
 
   270   apply(rule equivpI)
 
   270   apply(rule equivpI)
 
   271   unfolding reflp_def symp_def transp_def
 
   271   unfolding reflp_def symp_def transp_def
 
   273   apply(rule equivpI)
 
   273   apply(rule equivpI)
 
   274   unfolding reflp_def symp_def transp_def
 
   274   unfolding reflp_def symp_def transp_def
 
   275   apply(auto intro: al_refl al_sym al_trans)
 
   275   apply(auto intro: al_refl al_sym al_trans)
 
   276   done
 
   276   done
 
   277 
   277 
   278 quotient_type RKIND = rkind / arkind
 
   278 quotient_type RKIND = rkind / alpha_rkind
 
   279   by (rule alpha_equivps)
 
   279   by (rule alpha_equivps)
 
   280 
   280 
   281 quotient_type
 
   281 quotient_type
 
   282     RTY = rty / arty and
 
   282     RTY = rty / alpha_rty and
 
   283     RTRM = rtrm / artrm
 
   283     RTRM = rtrm / alpha_rtrm
 
   284   by (auto intro: alpha_equivps)
 
   284   by (auto intro: alpha_equivps)
 
   285 
   285 
   286 quotient_definition
 
   286 quotient_definition
 
   287    "TYP :: RKIND"
 
   287    "TYP :: RKIND"
 
   288 is
 
   288 is
 
   345 is
 
   345 is
 
   346   "fv_rtrm"
 
   346   "fv_rtrm"
 
   347 
   347 
   348 lemma alpha_rfv:
 
   348 lemma alpha_rfv:
 
   349   shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and>
 
   349   shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and>
 
   350      (t1 \<approx>rty s1 \<longrightarrow> fv_rty t1 = fv_rty s1) \<and>
 
   350      (t1 \<approx>ty s1 \<longrightarrow> fv_rty t1 = fv_rty s1) \<and>
 
   351      (t2 \<approx>tr s2 \<longrightarrow> fv_rtrm t2 = fv_rtrm s2)"
 
   351      (t2 \<approx>tr s2 \<longrightarrow> fv_rtrm t2 = fv_rtrm s2)"
 
   352   apply(rule arkind_arty_artrm.induct)
 
   352   apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct)
 
   353   apply(simp_all add: alpha_gen)
 
   353   apply(simp_all add: alpha_gen)
 
   354   done
 
   354   done
 
   355 
   355 
   356 lemma perm_rsp[quot_respect]:
 
   356 lemma perm_rsp[quot_respect]:
 
   357   "(op = ===> arkind ===> arkind) permute permute"
 
   357   "(op = ===> alpha_rkind ===> alpha_rkind) permute permute"
 
   358   "(op = ===> arty ===> arty) permute permute"
 
   358   "(op = ===> alpha_rty ===> alpha_rty) permute permute"
 
   359   "(op = ===> artrm ===> artrm) permute permute"
 
   359   "(op = ===> alpha_rtrm ===> alpha_rtrm) permute permute"
 
   360   by (simp_all add:alpha_eqvt)
 
   360   by (simp_all add:alpha_eqvt)
 
   361 
   361 
   362 lemma tconst_rsp[quot_respect]: 
   362 lemma tconst_rsp[quot_respect]: 
   363   "(op = ===> arty) TConst TConst"
 
   363   "(op = ===> alpha_rty) TConst TConst"
 
   364   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   364   apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
 
   365 lemma tapp_rsp[quot_respect]: 
   365 lemma tapp_rsp[quot_respect]: 
   366   "(arty ===> artrm ===> arty) TApp TApp" 
   366   "(alpha_rty ===> alpha_rtrm ===> alpha_rty) TApp TApp" 
   367   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   367   apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
 
   368 lemma var_rsp[quot_respect]: 
   368 lemma var_rsp[quot_respect]: 
   369   "(op = ===> artrm) Var Var"
 
   369   "(op = ===> alpha_rtrm) Var Var"
 
   370   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   370   apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
 
   371 lemma app_rsp[quot_respect]: 
   371 lemma app_rsp[quot_respect]: 
   372   "(artrm ===> artrm ===> artrm) App App"
 
   372   "(alpha_rtrm ===> alpha_rtrm ===> alpha_rtrm) App App"
 
   373   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   373   apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
 
   374 lemma const_rsp[quot_respect]: 
   374 lemma const_rsp[quot_respect]: 
   375   "(op = ===> artrm) Const Const"
 
   375   "(op = ===> alpha_rtrm) Const Const"
 
   376   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
 
   376   apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
 
   377 
   377 
   378 lemma kpi_rsp[quot_respect]: 
   378 lemma kpi_rsp[quot_respect]: 
   379   "(arty ===> op = ===> arkind ===> arkind) KPi KPi"
 
   379   "(alpha_rty ===> op = ===> alpha_rkind ===> alpha_rkind) KPi KPi"
 
   380   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
 
   380   apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   381   apply (rule a2) apply assumption
 
   381   apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(2)) apply simp_all
 
   382   apply (rule_tac x="0" in exI)
 
   382   apply (rule_tac x="0" in exI)
 
   383   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
 
   383   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
 
   384   done
 
   384   done
 
   385 
   385 
   386 lemma tpi_rsp[quot_respect]: 
   386 lemma tpi_rsp[quot_respect]: 
   387   "(arty ===> op = ===> arty ===> arty) TPi TPi"
 
   387   "(alpha_rty ===> op = ===> alpha_rty ===> alpha_rty) TPi TPi"
 
   388   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
 
   388   apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   389   apply (rule a5) apply assumption
 
   389   apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(5)) apply simp_all
 
   390   apply (rule_tac x="0" in exI)
 
   390   apply (rule_tac x="0" in exI)
 
   391   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
 
   391   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
 
   392   done
 
   392   done
 
   393 lemma lam_rsp[quot_respect]: 
   393 lemma lam_rsp[quot_respect]: 
   394   "(arty ===> op = ===> artrm ===> artrm) Lam Lam"
 
   394   "(alpha_rty ===> op = ===> alpha_rtrm ===> alpha_rtrm) Lam Lam"
 
   395   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
 
   395   apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
   396   apply (rule a9) apply assumption
 
   396   apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(9)) apply simp_all
 
   397   apply (rule_tac x="0" in exI)
 
   397   apply (rule_tac x="0" in exI)
 
   398   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
 
   398   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
 
   399   done
 
   399   done
 
   400 
   400 
   401 lemma fv_rty_rsp[quot_respect]: 
   401 lemma fv_rty_rsp[quot_respect]: 
   402   "(arty ===> op =) fv_rty fv_rty"
 
   402   "(alpha_rty ===> op =) fv_rty fv_rty"
 
   403   by (simp add: alpha_rfv)
 
   403   by (simp add: alpha_rfv)
 
   404 lemma fv_rkind_rsp[quot_respect]:
 
   404 lemma fv_rkind_rsp[quot_respect]:
 
   405   "(arkind ===> op =) fv_rkind fv_rkind"
 
   405   "(alpha_rkind ===> op =) fv_rkind fv_rkind"
 
   406   by (simp add: alpha_rfv)
 
   406   by (simp add: alpha_rfv)
 
   407 lemma fv_rtrm_rsp[quot_respect]:
 
   407 lemma fv_rtrm_rsp[quot_respect]:
 
   408   "(artrm ===> op =) fv_rtrm fv_rtrm"
 
   408   "(alpha_rtrm ===> op =) fv_rtrm fv_rtrm"
 
   409   by (simp add: alpha_rfv)
 
   409   by (simp add: alpha_rfv)
 
   410 
   410 
   411 thm rkind_rty_rtrm.induct
 
   411 thm rkind_rty_rtrm.induct
 
   412 lemmas RKIND_RTY_RTRM_induct = rkind_rty_rtrm.induct[quot_lifted]
 
   412 lemmas RKIND_RTY_RTRM_induct = rkind_rty_rtrm.induct[quot_lifted]
 
   413 
   413 
   452 apply (simp_all add: perm_zero_ok perm_add_ok)
 
   452 apply (simp_all add: perm_zero_ok perm_add_ok)
 
   453 done
 
   453 done
 
   454 
   454 
   455 end
 
   455 end
 
   456 
   456 
   457 lemmas ARKIND_ARTY_ARTRM_inducts = arkind_arty_artrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
   457 lemmas ALPHA_RKIND_ALPHA_RTY_ALPHA_RTRM_inducts = alpha_rkind_alpha_rty_alpha_rtrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
   458 
   458 
   459 lemmas RKIND_RTY_RTRM_INJECT = arkind_arty_artrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
   459 lemmas RKIND_RTY_RTRM_INJECT = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
   460 
   460 
   461 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]
 
   461 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]
 
   462 
   462 
   463 lemmas fv_eqvt = rfv_eqvt[quot_lifted]
 
   463 lemmas fv_eqvt = rfv_eqvt[quot_lifted]
 
   464 
   464
nominal2