2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"

     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp"

     8 datatype kind =

     8 datatype rkind =

    10   | KPi "ty" "name" "kind"

    10   | KPi "rty" "name" "rkind"

    11 and ty =

    11 and rty =

    13   | TApp "ty" "trm"

    13   | TApp "rty" "rtrm"

    14   | TPi "ty" "name" "ty"

    14   | TPi "rty" "name" "rty"

    15 and trm =

    15 and rtrm =

    18   | App "trm" "trm"

    18   | App "rtrm" "rtrm"

    19   | Lam "ty" "name" "trm"

    19   | Lam "rty" "name" "rtrm"

    20 

    20 

    21 instantiation kind and ty and trm :: pt

    21 

    22 begin

    22 setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}

    23 

    23 

    24 primrec

    25     permute_kind

    26 and permute_ty

    27 and permute_trm

    28 where

    29   "permute_kind pi Type = Type"

    30 | "permute_kind pi (KPi t n k) = KPi (permute_ty pi t) (pi \<bullet> n) (permute_kind pi k)"

    31 | "permute_ty pi (TConst i) = TConst (pi \<bullet> i)"

    32 | "permute_ty pi (TApp A M) = TApp (permute_ty pi A) (permute_trm pi M)"

    33 | "permute_ty pi (TPi A x B) = TPi (permute_ty pi A) (pi \<bullet> x) (permute_ty pi B)"

    34 | "permute_trm pi (Const i) = Const (pi \<bullet> i)"

    35 | "permute_trm pi (Var x) = Var (pi \<bullet> x)"

    36 | "permute_trm pi (App M N) = App (permute_trm pi M) (permute_trm pi N)"

    37 | "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \<bullet> x) (permute_trm pi M)"

    38 

    39 lemma rperm_zero_ok:

    40   "0 \<bullet> (x :: kind) = x"

    41   "0 \<bullet> (y :: ty) = y"

    42   "0 \<bullet> (z :: trm) = z"

    43 apply(induct x and y and z rule: kind_ty_trm.inducts)

    44 apply(simp_all)

    45 done

    46 

    47 lemma rperm_plus_ok:

    48  "(p + q) \<bullet> (x :: kind) = p \<bullet> q \<bullet> x"

    49  "(p + q) \<bullet> (y :: ty) = p \<bullet> q \<bullet> y"

    50  "(p + q) \<bullet> (z :: trm) = p \<bullet> q \<bullet> z"

    51 apply(induct x and y and z rule: kind_ty_trm.inducts)

    52 apply(simp_all)

    53 done

    54 

    55 instance

    56 apply default

    57 apply (simp_all only:rperm_zero_ok rperm_plus_ok)

    58 done

    59 

    60 end

    61 

    62 (*

    63 setup {* snd o define_raw_perms ["kind", "ty", "trm"] ["LFex.kind", "LFex.ty", "LFex.trm"] *}

    65   snd o define_fv_alpha "LFex.kind"

    25   snd o define_fv_alpha "LFex.rkind"

    70     alpha_kind  ("_ \<approx>ki _" [100, 100] 100)

    30     alpha_rkind  ("_ \<approx>ki _" [100, 100] 100)

    71 and alpha_ty    ("_ \<approx>ty _" [100, 100] 100)

    31 and alpha_rty    ("_ \<approx>ty _" [100, 100] 100)

    72 and alpha_trm   ("_ \<approx>tr _" [100, 100] 100)

    32 and alpha_rtrm   ("_ \<approx>tr _" [100, 100] 100)

    73 thm fv_kind_fv_ty_fv_trm.simps alpha_kind_alpha_ty_alpha_trm.intros

    33 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros

    74 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_kind_alpha_ty_alpha_trm.intros} @{thms kind.distinct ty.distinct trm.distinct kind.inject ty.inject trm.inject} @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases} ctxt)) ctxt)) *}

    34 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_rkind_alpha_rty_alpha_rtrm_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 thm alphas_inj

    35 thm alpha_rkind_alpha_rty_alpha_rtrm_inj

    76 

    77 lemma alphas_eqvt:

    78   "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"

    79   "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"

    80   "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"

    81 sorry

    82 

    83 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_equivp}, []),

    84   (build_equivps [@{term alpha_kind}, @{term alpha_ty}, @{term alpha_trm}]

    85      @{thm kind_ty_trm.induct} @{thm alpha_kind_alpha_ty_alpha_trm.induct} 

    86      @{thms kind.inject ty.inject trm.inject} @{thms alphas_inj}

    87      @{thms kind.distinct ty.distinct trm.distinct}

    88      @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases}

    89      @{thms alphas_eqvt} ctxt)) ctxt)) *}

    90 thm alphas_equivp

    91 *)

    92 

    93 primrec

    94     rfv_kind :: "kind \<Rightarrow> atom set"

    95 and rfv_ty   :: "ty \<Rightarrow> atom set"

    96 and rfv_trm  :: "trm \<Rightarrow> atom set"

    97 where

    98   "rfv_kind (Type) = {}"

    99 | "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"

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

   101 | "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"

   102 | "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"

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

   104 | "rfv_trm (Var x) = {atom x}"

   105 | "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"

   106 | "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"

   107 

   108 inductive

   109     akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)

   110 and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)

   111 and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)

   112 where

   113   a1: "(Type) \<approx>ki (Type)"

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

   115 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"

   116 | a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"

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

   118 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"

   119 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"

   120 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"

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

   122 

   123 lemma akind_aty_atrm_inj:

   124   "(Type) \<approx>ki (Type) = True"

   125   "((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')))"

   126   "(TConst i) \<approx>ty (TConst j) = (i = j)"

   127   "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"

   128   "((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'))))"

   129   "(Const i) \<approx>tr (Const j) = (i = j)"

   130   "(Var x) \<approx>tr (Var y) = (x = y)"

   131   "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"

   132   "((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'))))"

   133 apply -

   134 apply (simp add: akind_aty_atrm.intros)

   135 

   136 apply rule apply (erule akind.cases) apply simp apply blast

   137 apply (simp only: akind_aty_atrm.intros)

   138 

   139 apply rule apply (erule aty.cases) apply simp apply simp apply simp

   140 apply (simp only: akind_aty_atrm.intros)

   141 

   142 apply rule apply (erule aty.cases) apply simp apply simp apply simp

   143 apply (simp only: akind_aty_atrm.intros)

   144 

   145 apply rule apply (erule aty.cases) apply simp apply simp apply blast

   146 apply (simp only: akind_aty_atrm.intros)

   147 

   148 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast

   149 apply (simp only: akind_aty_atrm.intros)

   150 

   151 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast

   152 apply (simp only: akind_aty_atrm.intros)

   153 

   154 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast

   155 apply (simp only: akind_aty_atrm.intros)

   156 

   157 apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast

   158 apply (simp only: akind_aty_atrm.intros)

   159 done

   162   "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"

    38   "((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))"

   163   "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"

    39   "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))"

   164   "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"

    40   "((pi\<bullet>fv_rtrm t3) = fv_rtrm (pi\<bullet>t3))"

   165 apply(induct t1 and t2 and t3 rule: kind_ty_trm.inducts)

    41 apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts)

   166 apply(simp_all add:  union_eqvt Diff_eqvt)

    42 apply(simp_all add: union_eqvt Diff_eqvt)

   174 apply(induct rule: akind_aty_atrm.inducts)

    50 apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)

   175 apply (simp_all add: akind_aty_atrm.intros)

    51 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)

   176 apply (simp_all add: akind_aty_atrm_inj)

    52 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)

   188 lemma al_refl:

    64 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []),

   189   fixes K::"kind" 

    65   (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}]

   190   and   A::"ty"

    66      @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} 

   191   and   M::"trm"

    67      @{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}

   192   shows "K \<approx>ki K"

    68      @{thms rkind.distinct rty.distinct rtrm.distinct}

   193   and   "A \<approx>ty A"

    69      @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases}

   194   and   "M \<approx>tr M"

    70      @{thms alpha_eqvt} ctxt)) ctxt)) *}

   195   apply(induct K and A and M rule: kind_ty_trm.inducts)

    71 thm alpha_equivps

   196   apply(auto intro: akind_aty_atrm.intros)

    72 

   197   apply (rule a2)

    73 local_setup  {* define_quotient_type

   198   apply auto

    74   [(([], @{binding kind}, NoSyn), (@{typ rkind}, @{term alpha_rkind})),

   199   apply(rule_tac x="0" in exI)

    75    (([], @{binding ty},   NoSyn), (@{typ rty},   @{term alpha_rty}  )),

   200   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)

    76    (([], @{binding trm},  NoSyn), (@{typ rtrm},  @{term alpha_rtrm} ))]

   201   apply (rule a5)

    77   (ALLGOALS (resolve_tac @{thms alpha_equivps}))

   202   apply auto

    78 *}

   203   apply(rule_tac x="0" in exI)

    79 

   204   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)

    80 local_setup {*

   205   apply (rule a9)

    81 (fn ctxt => ctxt

   206   apply auto

    82  |> snd o (Quotient_Def.quotient_lift_const ("TYP", @{term Type}))

   207   apply(rule_tac x="0" in exI)

    83  |> snd o (Quotient_Def.quotient_lift_const ("KPI", @{term KPi}))

   208   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)

    84  |> snd o (Quotient_Def.quotient_lift_const ("TCONST", @{term TConst}))

    85  |> snd o (Quotient_Def.quotient_lift_const ("TAPP", @{term TApp}))

    86  |> snd o (Quotient_Def.quotient_lift_const ("TPI", @{term TPi}))

    87  |> snd o (Quotient_Def.quotient_lift_const ("CONS", @{term Const}))

    88  |> snd o (Quotient_Def.quotient_lift_const ("VAR", @{term Var}))

    89  |> snd o (Quotient_Def.quotient_lift_const ("APP", @{term App}))

    90  |> snd o (Quotient_Def.quotient_lift_const ("LAM", @{term Lam}))

    91  |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind}))

    92  |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty}))

    93  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *}

    94 print_theorems

    95 

    96 local_setup {* prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}]

    97   (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *}

    98 local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}]

    99   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}

   100 local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}]

   101   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}

   102 local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}]

   103   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}

   104 ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}

   105   @{thms rfv_rsp} @{thms alpha_equivps} 1 *}

   106 local_setup {* prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *}

   107 local_setup {* prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *}

   108 local_setup {* prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *}

   109 local_setup {* prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *}

   110 local_setup {* prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *}

   111 local_setup {* prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *}

   112 local_setup {* prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *}

   113 local_setup {* prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *}

   114 

   115 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted]

   116 

   117 thm rkind_rty_rtrm.inducts

   118 lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted]

   119 

   120 instantiation kind and ty and trm :: pt

   121 begin

   122 

   123 quotient_definition

   124   "permute_kind :: perm \<Rightarrow> kind \<Rightarrow> kind"

   125 is

   126   "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"

   127 

   128 quotient_definition

   129   "permute_ty :: perm \<Rightarrow> ty \<Rightarrow> ty"

   130 is

   131   "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"

   132 

   133 quotient_definition

   134   "permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm"

   135 is

   136   "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"

   137 

   138 instance by default (simp_all add:

   139   permute_rkind_permute_rty_permute_rtrm_zero[quot_lifted]

   140   permute_rkind_permute_rty_permute_rtrm_append[quot_lifted])

   141 

   142 end

   143 

   144 (*

   145 Lifts, but slow and not needed?.

   146 lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen]

   147 *)

   148 

   149 lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]

   150 

   151 lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

   152 

   153 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]

   154 

   155 lemmas fv_eqvt = rfv_eqvt[quot_lifted]

   156 

   157 lemma supports:

   158   "{} supports TYP"

   159   "(supp (atom i)) supports (TCONST i)"

   160   "(supp A \<union> supp M) supports (TAPP A M)"

   161   "(supp (atom i)) supports (CONS i)"

   162   "(supp (atom x)) supports (VAR x)"

   163   "(supp M \<union> supp N) supports (APP M N)"

   164   "(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPI ty na ki)"

   165   "(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPI ty na ty2)"

   166   "(supp ty \<union> supp (atom na) \<union> supp trm) supports (LAM ty na trm)"

   167 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh)

   168 apply(rule_tac [!] allI)+

   169 apply(rule_tac [!] impI)

   170 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})

   171 apply(simp_all add: fresh_atom)

   172 done

   173 

   174 lemma kind_ty_trm_fs:

   175   "finite (supp (x\<Colon>kind))"

   176   "finite (supp (y\<Colon>ty))"

   177   "finite (supp (z\<Colon>trm))"

   178 apply(induct x and y and z rule: kind_ty_trm_inducts)

   179 apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})

   180 apply(simp_all add: supp_atom)

   181 done

   182 

   183 instance kind and ty and trm :: fs

   184 apply(default)

   185 apply(simp_all only: kind_ty_trm_fs)

   186 done

   187 

   188 lemma supp_eqs:

   189   "supp TYP = {}"

   190   "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"

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

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

   193   "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)"

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

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

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

   197   "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"

   198   apply(simp_all (no_asm) add: supp_def)

   199   apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen)

   200   apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric])

   201   apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute)

   202   apply(simp_all add: supp_at_base[simplified supp_def])

   211 lemma al_sym:

   205 lemma supp_fv:

   212   fixes K K'::"kind" and A A'::"ty" and M M'::"trm"

   206   "supp t1 = fv_kind t1"

   213   shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"

   207   "supp t2 = fv_ty t2"

   214   and   "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A"

   208   "supp t3 = fv_trm t3"

   215   and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"

   209   apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts)

   216   apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts)

   210   apply(simp_all (no_asm) only: supp_eqs fv_kind_ty_trm)

   217   apply(simp_all add: akind_aty_atrm.intros)

   211   apply(simp_all)

   218   apply (simp_all add: akind_aty_atrm_inj)

   212   apply(subst supp_eqs)

   219   apply(erule alpha_gen_compose_sym)

   213   apply(simp_all add: supp_Abs)

   220   apply(erule alpha_eqvt)

   214   apply(subst supp_eqs)

   221   apply(erule alpha_gen_compose_sym)

   215   apply(simp_all add: supp_Abs)

   222   apply(erule alpha_eqvt)

   216   apply(subst supp_eqs)

   223   apply(erule alpha_gen_compose_sym)

   217   apply(simp_all add: supp_Abs)

   224   apply(erule alpha_eqvt)

   227 lemma al_trans:

   220 lemma supp_rkind_rty_rtrm:

   228   fixes K K' K''::"kind" and A A' A''::"ty" and M M' M''::"trm"

   221   "supp TYP = {}"

   229   shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"

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

   230   and   "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A'' \<Longrightarrow> A \<approx>ty A''"

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

   231   and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''"

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

   232   apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: akind_aty_atrm.inducts)

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

   233   apply(simp_all add: akind_aty_atrm.intros)

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

   234   apply(erule akind.cases)

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

   235   apply(simp_all add: akind_aty_atrm.intros)

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

   236   apply(simp add: akind_aty_atrm_inj)

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

   237   apply(erule alpha_gen_compose_trans)

   230   by (simp_all only: supp_fv fv_kind_ty_trm)

   238   apply(assumption)

   239   apply(erule alpha_eqvt)

   240   apply(rotate_tac 4)

   241   apply(erule aty.cases)

   242   apply(simp_all add: akind_aty_atrm.intros)

   243   apply(rotate_tac 3)

   244   apply(erule aty.cases)

   245   apply(simp_all add: akind_aty_atrm.intros)

   246   apply(simp add: akind_aty_atrm_inj)

   247   apply(erule alpha_gen_compose_trans)

   248   apply(assumption)

   249   apply(erule alpha_eqvt)

   250   apply(rotate_tac 4)

   251   apply(erule atrm.cases)

   252   apply(simp_all add: akind_aty_atrm.intros)

   253   apply(rotate_tac 3)

   254   apply(erule atrm.cases)

   255   apply(simp_all add: akind_aty_atrm.intros)

   256   apply(simp add: akind_aty_atrm_inj)

   257   apply(erule alpha_gen_compose_trans)

   258   apply(assumption)

   259   apply(erule alpha_eqvt)

   260   done

   261 

   262 lemma alpha_equivps:

   263   shows "equivp akind"

   264   and   "equivp aty"

   265   and   "equivp atrm"

   266   apply(rule equivpI)

   267   unfolding reflp_def symp_def transp_def

   268   apply(auto intro: al_refl al_sym al_trans)

   269   apply(rule equivpI)

   270   unfolding reflp_def symp_def transp_def

   271   apply(auto intro: al_refl al_sym al_trans)

   272   apply(rule equivpI)

   273   unfolding reflp_def symp_def transp_def

   274   apply(auto intro: al_refl al_sym al_trans)

   275   done

   276 

   277 quotient_type KIND = kind / akind

   278   by (rule alpha_equivps)

   279 

   280 quotient_type

   281     TY = ty / aty and

   282     TRM = trm / atrm

   283   by (auto intro: alpha_equivps)

   284 

   285 quotient_definition

   286    "TYP :: KIND"

   287 is

   288   "Type"

   289 

   290 quotient_definition

   291    "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"

   292 is

   293   "KPi"

   294 

   295 quotient_definition

   296    "TCONST :: ident \<Rightarrow> TY"

   297 is

   298   "TConst"

   299 

   300 quotient_definition

   301    "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"

   302 is

   303   "TApp"

   304 

   305 quotient_definition

   306    "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"

   307 is

   308   "TPi"

   309 

   310 (* FIXME: does not work with CONST *)

   311 quotient_definition

   312    "CONS :: ident \<Rightarrow> TRM"

   313 is

   314   "Const"

   315 

   316 quotient_definition

   317    "VAR :: name \<Rightarrow> TRM"

   318 is

   319   "Var"

   320 

   321 quotient_definition

   322    "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"

   323 is

   324   "App"

   325 

   326 quotient_definition

   327    "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"

   328 is

   329   "Lam"

   330 

   331 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)

   332 quotient_definition

   333    "fv_kind :: KIND \<Rightarrow> atom set"

   334 is

   335   "rfv_kind"

   336 

   337 quotient_definition

   338    "fv_ty :: TY \<Rightarrow> atom set"

   339 is

   340   "rfv_ty"

   341 

   342 quotient_definition

   343    "fv_trm :: TRM \<Rightarrow> atom set"

   344 is

   345   "rfv_trm"

   346 

   347 lemma alpha_rfv:

   348   shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>

   349      (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>

   350      (t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"

   351   apply(rule akind_aty_atrm.induct)

   352   apply(simp_all add: alpha_gen)

   353   done

   354 

   355 lemma perm_rsp[quot_respect]:

   356   "(op = ===> akind ===> akind) permute permute"

   357   "(op = ===> aty ===> aty) permute permute"

   358   "(op = ===> atrm ===> atrm) permute permute"

   359   by (simp_all add:alpha_eqvt)

   360 

   361 lemma tconst_rsp[quot_respect]: 

   362   "(op = ===> aty) TConst TConst"

   363   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

   364 lemma tapp_rsp[quot_respect]: 

   365   "(aty ===> atrm ===> aty) TApp TApp" 

   366   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

   367 lemma var_rsp[quot_respect]: 

   368   "(op = ===> atrm) Var Var"

   369   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

   370 lemma app_rsp[quot_respect]: 

   371   "(atrm ===> atrm ===> atrm) App App"

   372   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

   373 lemma const_rsp[quot_respect]: 

   374   "(op = ===> atrm) Const Const"

   375   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done

   376 

   377 lemma kpi_rsp[quot_respect]: 

   378   "(aty ===> op = ===> akind ===> akind) KPi KPi"

   379   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)

   380   apply (rule a2) apply assumption

   381   apply (rule_tac x="0" in exI)

   382   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)

   383   done

   384 

   385 lemma tpi_rsp[quot_respect]: 

   386   "(aty ===> op = ===> aty ===> aty) TPi TPi"

   387   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)

   388   apply (rule a5) apply assumption

   389   apply (rule_tac x="0" in exI)

   390   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)

   391   done

   392 lemma lam_rsp[quot_respect]: 

   393   "(aty ===> op = ===> atrm ===> atrm) Lam Lam"

   394   apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)

   395   apply (rule a9) apply assumption

   396   apply (rule_tac x="0" in exI)

   397   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)

   398   done

   399 

   400 lemma rfv_ty_rsp[quot_respect]: 

   401   "(aty ===> op =) rfv_ty rfv_ty"

   402   by (simp add: alpha_rfv)

   403 lemma rfv_kind_rsp[quot_respect]:

   404   "(akind ===> op =) rfv_kind rfv_kind"

   405   by (simp add: alpha_rfv)

   406 lemma rfv_trm_rsp[quot_respect]:

   407   "(atrm ===> op =) rfv_trm rfv_trm"

   408   by (simp add: alpha_rfv)

   409 

   410 thm kind_ty_trm.induct

   411 lemmas KIND_TY_TRM_induct = kind_ty_trm.induct[quot_lifted]

   412 

   413 thm kind_ty_trm.inducts

   414 lemmas KIND_TY_TRM_inducts = kind_ty_trm.inducts[quot_lifted]

   415 

   416 instantiation KIND and TY and TRM :: pt

   417 begin

   418 

   419 quotient_definition

   420   "permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"

   421 is

   422   "permute :: perm \<Rightarrow> kind \<Rightarrow> kind"

   423 

   424 quotient_definition

   425   "permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"

   426 is

   427   "permute :: perm \<Rightarrow> ty \<Rightarrow> ty"

   428 

   429 quotient_definition

   430   "permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"

   431 is

   432   "permute :: perm \<Rightarrow> trm \<Rightarrow> trm"

   433 

   434 lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted]

   435 

   436 lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"

   437 apply (induct rule: KIND_TY_TRM_induct)

   438 apply (simp_all)

   439 done

   440 

   441 lemma perm_add_ok:

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

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

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

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

   446 apply (simp_all)

   447 done

   448 

   449 instance

   450 apply default

   451 apply (simp_all add: perm_zero_ok perm_add_ok)

   452 done

   456 lemmas AKIND_ATY_ATRM_inducts = akind_aty_atrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]

   234 

   457 

   235 

   458 lemmas KIND_TY_TRM_INJECT = akind_aty_atrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

   236 

   459 

   460 lemmas fv_kind_ty_trm = rfv_kind_rfv_ty_rfv_trm.simps[quot_lifted]

   461 

   462 lemmas fv_eqvt = rfv_eqvt[quot_lifted]

   463 

   464 lemma supp_kind_ty_trm_easy:

   465  "supp TYP = {}"

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

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

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

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

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

   471 apply (simp_all add: supp_def permute_ktt KIND_TY_TRM_INJECT)

   472 apply (simp_all only: supp_at_base[simplified supp_def])

   473 apply (simp_all add: Collect_imp_eq Collect_neg_eq)

   474 done

   475 

   476 lemma supp_bind:

   477   "(supp (atom na, (ty, ki))) supports (KPI ty na ki)"

   478   "(supp (atom na, (ty, ty2))) supports (TPI ty na ty2)"

   479   "(supp (atom na, (ty, trm))) supports (LAM ty na trm)"

   480 apply(simp_all add: supports_def)

   481 apply(fold fresh_def)

   482 apply(simp_all add: fresh_Pair swap_fresh_fresh)

   483 apply(clarify)

   484 apply(subst swap_at_base_simps(3))

   485 apply(simp_all add: fresh_atom)

   486 apply(clarify)

   487 apply(subst swap_at_base_simps(3))

   488 apply(simp_all add: fresh_atom)

   489 apply(clarify)

   490 apply(subst swap_at_base_simps(3))

   491 apply(simp_all add: fresh_atom)

   492 done

   493 

   494 lemma KIND_TY_TRM_fs:

   495   "finite (supp (x\<Colon>KIND))"

   496   "finite (supp (y\<Colon>TY))"

   497   "finite (supp (z\<Colon>TRM))"

   498 apply(induct x and y and z rule: KIND_TY_TRM_inducts)

   499 apply(simp_all add: supp_kind_ty_trm_easy)

   500 apply(rule supports_finite)

   501 apply(rule supp_bind(1))

   502 apply(simp add: supp_Pair supp_atom)

   503 apply(rule supports_finite)

   504 apply(rule supp_bind(2))

   505 apply(simp add: supp_Pair supp_atom)

   506 apply(rule supports_finite)

   507 apply(rule supp_bind(3))

   508 apply(simp add: supp_Pair supp_atom)

   509 done

   510 

   511 instance KIND and TY and TRM :: fs

   512 apply(default)

   513 apply(simp_all only: KIND_TY_TRM_fs)

   514 done

   515 

   516 lemma supp_fv:

   517  "supp t1 = fv_kind t1"

   518  "supp t2 = fv_ty t2"

   519  "supp t3 = fv_trm t3"

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

   521 apply (simp_all add: supp_kind_ty_trm_easy)

   522 apply (simp_all add: fv_kind_ty_trm)

   523 apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abs {atom name} kind)")

   524 apply(simp add: supp_Abs Set.Un_commute)

   525 apply(simp (no_asm) add: supp_def)

   526 apply(simp add: KIND_TY_TRM_INJECT)

   527 apply(simp add: Abs_eq_iff)

   528 apply(simp add: alpha_gen)

   529 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt)

   530 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])

   531 apply(subgoal_tac "supp (TPI ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)")

   532 apply(simp add: supp_Abs Set.Un_commute)

   533 apply(simp (no_asm) add: supp_def)

   534 apply(simp add: KIND_TY_TRM_INJECT)

   535 apply(simp add: Abs_eq_iff)

   536 apply(simp add: alpha_gen)

   537 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)

   538 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)

   539 apply(subgoal_tac "supp (LAM ty name trm) = supp ty \<union> supp (Abs {atom name} trm)")

   540 apply(simp add: supp_Abs Set.Un_commute)

   541 apply(simp (no_asm) add: supp_def)

   542 apply(simp add: KIND_TY_TRM_INJECT)

   543 apply(simp add: Abs_eq_iff)

   544 apply(simp add: alpha_gen)

   545 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)

   546 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)

   547 done

   548 

   549 (* Not needed anymore *)

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

   551 apply (simp add: permute_set_eq supp_def Abs_eq_iff KIND_TY_TRM_INJECT)

   552 apply (simp add: alpha_gen supp_fv)

   553 apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute)

   554 done

   555 

   556 lemma supp_kind_ty_trm:

   557  "supp TYP = {}"

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

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

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

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

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

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

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

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

   566 apply (simp_all only: supp_kind_ty_trm_easy)

   567 apply (simp_all only: supp_fv fv_kind_ty_trm)

   568 done

   569 

   570 end

   571 

   572 

   573 

   574