--- a/Nominal/Term9.thy	Tue Mar 23 07:04:27 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-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 (Datatype.the_info @{theory} "Term9.rlam9") 2 *}
-print_theorems
-
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "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