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