--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/LFex.thy	Thu Feb 25 07:48:33 2010 +0100
@@ -0,0 +1,236 @@
+theory LFex
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp"
+begin
+
+atom_decl name
+atom_decl ident
+
+datatype rkind =
+    Type
+  | KPi "rty" "name" "rkind"
+and rty =
+    TConst "ident"
+  | TApp "rty" "rtrm"
+  | TPi "rty" "name" "rty"
+and rtrm =
+    Const "ident"
+  | Var "name"
+  | App "rtrm" "rtrm"
+  | Lam "rty" "name" "rtrm"
+
+
+setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}
+
+local_setup {*
+  snd o define_fv_alpha "LFex.rkind"
+  [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
+   [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
+   [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+notation
+    alpha_rkind  ("_ \<approx>ki _" [100, 100] 100)
+and alpha_rty    ("_ \<approx>ty _" [100, 100] 100)
+and alpha_rtrm   ("_ \<approx>tr _" [100, 100] 100)
+thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros
+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)) *}
+thm alpha_rkind_alpha_rty_alpha_rtrm_inj
+
+lemma rfv_eqvt[eqvt]:
+  "((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))"
+  "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))"
+  "((pi\<bullet>fv_rtrm t3) = fv_rtrm (pi\<bullet>t3))"
+apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts)
+apply(simp_all add: union_eqvt Diff_eqvt)
+apply(simp_all add: permute_set_eq atom_eqvt)
+done
+
+lemma alpha_eqvt:
+  "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
+  "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
+  "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
+apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
+apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
+apply (rule alpha_gen_atom_eqvt)
+apply (simp add: rfv_eqvt)
+apply assumption
+apply (rule alpha_gen_atom_eqvt)
+apply (simp add: rfv_eqvt)
+apply assumption
+apply (rule alpha_gen_atom_eqvt)
+apply (simp add: rfv_eqvt)
+apply assumption
+done
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []),
+  (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}]
+     @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} 
+     @{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}
+     @{thms rkind.distinct rty.distinct rtrm.distinct}
+     @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases}
+     @{thms alpha_eqvt} ctxt)) ctxt)) *}
+thm alpha_equivps
+
+local_setup  {* define_quotient_type
+  [(([], @{binding kind}, NoSyn), (@{typ rkind}, @{term alpha_rkind})),
+   (([], @{binding ty},   NoSyn), (@{typ rty},   @{term alpha_rty}  )),
+   (([], @{binding trm},  NoSyn), (@{typ rtrm},  @{term alpha_rtrm} ))]
+  (ALLGOALS (resolve_tac @{thms alpha_equivps}))
+*}
+
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("TYP", @{term Type}))
+ |> snd o (Quotient_Def.quotient_lift_const ("KPI", @{term KPi}))
+ |> snd o (Quotient_Def.quotient_lift_const ("TCONST", @{term TConst}))
+ |> snd o (Quotient_Def.quotient_lift_const ("TAPP", @{term TApp}))
+ |> snd o (Quotient_Def.quotient_lift_const ("TPI", @{term TPi}))
+ |> snd o (Quotient_Def.quotient_lift_const ("CONS", @{term Const}))
+ |> snd o (Quotient_Def.quotient_lift_const ("VAR", @{term Var}))
+ |> snd o (Quotient_Def.quotient_lift_const ("APP", @{term App}))
+ |> snd o (Quotient_Def.quotient_lift_const ("LAM", @{term Lam}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *}
+print_theorems
+
+local_setup {* prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}]
+  (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *}
+local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}]
+  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
+local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}]
+  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
+local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}]
+  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
+ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}
+  @{thms rfv_rsp} @{thms alpha_equivps} 1 *}
+local_setup {* prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *}
+
+lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted]
+
+thm rkind_rty_rtrm.inducts
+lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted]
+
+instantiation kind and ty and trm :: pt
+begin
+
+quotient_definition
+  "permute_kind :: perm \<Rightarrow> kind \<Rightarrow> kind"
+is
+  "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"
+
+quotient_definition
+  "permute_ty :: perm \<Rightarrow> ty \<Rightarrow> ty"
+is
+  "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"
+
+quotient_definition
+  "permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm"
+is
+  "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"
+
+instance by default (simp_all add:
+  permute_rkind_permute_rty_permute_rtrm_zero[quot_lifted]
+  permute_rkind_permute_rty_permute_rtrm_append[quot_lifted])
+
+end
+
+(*
+Lifts, but slow and not needed?.
+lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+*)
+
+lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]
+
+lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+
+lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]
+
+lemmas fv_eqvt = rfv_eqvt[quot_lifted]
+
+lemma supports:
+  "{} supports TYP"
+  "(supp (atom i)) supports (TCONST i)"
+  "(supp A \<union> supp M) supports (TAPP A M)"
+  "(supp (atom i)) supports (CONS i)"
+  "(supp (atom x)) supports (VAR x)"
+  "(supp M \<union> supp N) supports (APP M N)"
+  "(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPI ty na ki)"
+  "(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPI ty na ty2)"
+  "(supp ty \<union> supp (atom na) \<union> supp trm) supports (LAM ty na trm)"
+apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh)
+apply(rule_tac [!] allI)+
+apply(rule_tac [!] impI)
+apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
+apply(simp_all add: fresh_atom)
+done
+
+lemma kind_ty_trm_fs:
+  "finite (supp (x\<Colon>kind))"
+  "finite (supp (y\<Colon>ty))"
+  "finite (supp (z\<Colon>trm))"
+apply(induct x and y and z rule: kind_ty_trm_inducts)
+apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
+apply(simp_all add: supp_atom)
+done
+
+instance kind and ty and trm :: fs
+apply(default)
+apply(simp_all only: kind_ty_trm_fs)
+done
+
+lemma supp_eqs:
+  "supp TYP = {}"
+  "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"
+  "supp (TCONST i) = {atom i}"
+  "supp (TAPP A M) = supp A \<union> supp M"
+  "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)"
+  "supp (CONS i) = {atom i}"
+  "supp (VAR x) = {atom x}"
+  "supp (APP M N) = supp M \<union> supp N"
+  "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"
+  apply(simp_all (no_asm) add: supp_def)
+  apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen)
+  apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric])
+  apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute)
+  apply(simp_all add: supp_at_base[simplified supp_def])
+  done
+
+lemma supp_fv:
+  "supp t1 = fv_kind t1"
+  "supp t2 = fv_ty t2"
+  "supp t3 = fv_trm t3"
+  apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts)
+  apply(simp_all (no_asm) only: supp_eqs fv_kind_ty_trm)
+  apply(simp_all)
+  apply(subst supp_eqs)
+  apply(simp_all add: supp_Abs)
+  apply(subst supp_eqs)
+  apply(simp_all add: supp_Abs)
+  apply(subst supp_eqs)
+  apply(simp_all add: supp_Abs)
+  done
+
+lemma supp_rkind_rty_rtrm:
+  "supp TYP = {}"
+  "supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
+  "supp (TCONST i) = {atom i}"
+  "supp (TAPP A M) = supp A \<union> supp M"
+  "supp (TPI A x B) = supp A \<union> (supp B - {atom x})"
+  "supp (CONS i) = {atom i}"
+  "supp (VAR x) = {atom x}"
+  "supp (APP M N) = supp M \<union> supp N"
+  "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
+  by (simp_all only: supp_fv fv_kind_ty_trm)
+
+end
+
+
+
+