# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266918434 -3600
# Node ID c74c8ba46db7dba6f410fd37f26c7e74dad3ab14
# Parent  2bbfbc9a81fcf86268c8911c9abb65b62cec2070
All works in LF but will require renaming.

diff -r 2bbfbc9a81fc -r c74c8ba46db7 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Tue Feb 23 09:34:41 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Tue Feb 23 10:47:14 2010 +0100
@@ -1,5 +1,5 @@
 theory LFex
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"
 begin
 
 atom_decl name
@@ -59,6 +59,37 @@
 
 end
 
+(*
+setup {* snd o define_raw_perms ["kind", "ty", "trm"] ["LFex.kind", "LFex.ty", "LFex.trm"] *}
+local_setup {*
+  snd o define_fv_alpha "LFex.kind"
+  [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
+   [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
+   [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+notation
+    alpha_kind  ("_ \<approx>ki _" [100, 100] 100)
+and alpha_ty    ("_ \<approx>ty _" [100, 100] 100)
+and alpha_trm   ("_ \<approx>tr _" [100, 100] 100)
+thm fv_kind_fv_ty_fv_trm.simps alpha_kind_alpha_ty_alpha_trm.intros
+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)) *}
+thm alphas_inj
+
+lemma alphas_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)"
+sorry
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_equivp}, []),
+  (build_equivps [@{term alpha_kind}, @{term alpha_ty}, @{term alpha_trm}]
+     @{thm kind_ty_trm.induct} @{thm alpha_kind_alpha_ty_alpha_trm.induct} 
+     @{thms kind.inject ty.inject trm.inject} @{thms alphas_inj}
+     @{thms kind.distinct ty.distinct trm.distinct}
+     @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases}
+     @{thms alphas_eqvt} ctxt)) ctxt)) *}
+thm alphas_equivp
+*)
+
 primrec
     rfv_kind :: "kind \<Rightarrow> atom set"
 and rfv_ty   :: "ty \<Rightarrow> atom set"