--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Term7.thy	Thu Feb 25 14:14:08 2010 +0100
@@ -0,0 +1,50 @@
+theory Term7
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+begin
+
+atom_decl name
+
+(* example with a respectful bn function defined over the type itself *)
+
+datatype rtrm7 =
+  rVr7 "name"
+| rLm7 "name" "rtrm7" --"bind left in right"
+| rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)"
+
+primrec
+  rbv7
+where
+  "rbv7 (rVr7 n) = {atom n}"
+| "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
+| "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
+
+setup {* snd o define_raw_perms ["rtrm7"] ["Term7.rtrm7"] *}
+thm permute_rtrm7.simps
+
+local_setup {* snd o define_fv_alpha "Term7.rtrm7" [
+  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}
+print_theorems
+notation
+  alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100)
+thm alpha_rtrm7.intros
+thm fv_rtrm7.simps
+inductive
+  alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"
+| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
+| a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
+
+lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
+  apply simp
+  apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
+  apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI)
+  apply simp
+  apply (rule a3)
+  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+  apply (simp_all add: alpha_gen fresh_star_def)
+  apply (rule a1)
+  apply (rule refl)
+done
+
+end