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 (Datatype.the_info @{theory} "Term7.rtrm7") 1 *}
thm permute_rtrm7.simps

local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "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