--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Term9.thy	Thu Feb 25 14:14:08 2010 +0100
@@ -0,0 +1,78 @@
+theory Term9
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+begin
+
+atom_decl name
+
+datatype rlam9 =
+  Var9 "name"
+| Lam9 "name" "rlam9" --"bind name in rlam"
+and rbla9 =
+  Bla9 "rlam9" "rlam9" --"bind bv(first) in second"
+
+primrec
+  rbv9
+where
+  "rbv9 (Var9 x) = {}"
+| "rbv9 (Lam9 x b) = {atom x}"
+
+setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Term9.rlam9", "Term9.rbla9"] *}
+print_theorems
+
+local_setup {* snd o define_fv_alpha "Term9.rlam9" [
+  [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *}
+notation
+  alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and
+  alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100)
+thm alpha_rlam9_alpha_rbla9.intros
+
+
+inductive
+  alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)
+and
+  alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)"
+| a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2"
+| a3: "b1 \<approx>9l b2 \<Longrightarrow> (\<exists>pi. (((rbv9 b1), t1) \<approx>gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>9b Bla9 b2 t2"
+
+quotient_type
+  lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b
+sorry
+
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9})))
+*}
+print_theorems
+
+instantiation lam9 and bla9 :: pt
+begin
+
+quotient_definition
+  "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9"
+is
+  "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9"
+
+quotient_definition
+  "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9"
+is
+  "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9"
+
+instance
+sorry
+
+end
+
+lemma "\<lbrakk>b1 = b2; \<exists>pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \<and> (fv_lam9 t1 - bv9 b1) \<sharp>* pi \<and> pi \<bullet> t1 = t2\<rbrakk>
+ \<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2"
+apply (lifting a3[unfolded alpha_gen])
+apply injection
+sorry
+
+end