1 theory LFex

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

     3 begin

     4 

     5 atom_decl name

     6 atom_decl ident

     7 

     8 datatype rkind =

     9     Type

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

    11 and rty =

    12     TConst "ident"

    13   | TApp "rty" "rtrm"

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

    15 and rtrm =

    16     Const "ident"

    17   | Var "name"

    18   | App "rtrm" "rtrm"

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

    20 

    21 

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

    23 

    24 local_setup {*

    25   snd o define_fv_alpha "LFex.rkind"

    26   [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],

    27    [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],

    28    [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}

    29 notation

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

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

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

    33 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros

    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)) *}

    35 thm alpha_rkind_alpha_rty_alpha_rtrm_inj

    36 

    37 lemma rfv_eqvt[eqvt]:

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

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

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

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

    42 apply(simp_all add: union_eqvt Diff_eqvt)

    43 apply(simp_all add: permute_set_eq atom_eqvt)

    44 done

    45 

    46 lemma alpha_eqvt:

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

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

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

    50 apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)

    51 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)

    52 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)

    53 apply (rule alpha_gen_atom_eqvt)

    54 apply (simp add: rfv_eqvt)

    55 apply assumption

    56 apply (rule alpha_gen_atom_eqvt)

    57 apply (simp add: rfv_eqvt)

    58 apply assumption

    59 apply (rule alpha_gen_atom_eqvt)

    60 apply (simp add: rfv_eqvt)

    61 apply assumption

    62 done

    63 

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

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

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

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

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

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

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

    71 thm alpha_equivps

    72 

    73 local_setup  {* define_quotient_type

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

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

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

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

    78 *}

    79 

    80 local_setup {*

    81 (fn ctxt => ctxt

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

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

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

   203   done

   204 

   205 lemma supp_fv:

   206   "supp t1 = fv_kind t1"

   207   "supp t2 = fv_ty t2"

   208   "supp t3 = fv_trm t3"

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

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

   211   apply(simp_all)

   212   apply(subst supp_eqs)

   213   apply(simp_all add: supp_Abs)

   214   apply(subst supp_eqs)

   215   apply(simp_all add: supp_Abs)

   216   apply(subst supp_eqs)

   217   apply(simp_all add: supp_Abs)

   218   done

   219 

   220 lemma supp_rkind_rty_rtrm:

   221   "supp TYP = {}"

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

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

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

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

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

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

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

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

   230   by (simp_all only: supp_fv fv_kind_ty_trm)

   231 

   232 end

   233 

   234 

   235 

   236