theory Terms
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs"
begin

atom_decl name

text {* primrec seems to be genarally faster than fun *}

section {*** lets with binding patterns ***}

datatype rtrm1 =
  rVr1 "name"
| rAp1 "rtrm1" "rtrm1"
| rLm1 "name" "rtrm1"        --"name is bound in trm1"
| rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"
and bp =
  BUnit
| BVr "name"
| BPr "bp" "bp"

(* to be given by the user *)

primrec 
  bv1
where
  "bv1 (BUnit) = {}"
| "bv1 (BVr x) = {atom x}"
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"

(* needs to be calculated by the package *)
primrec 
  rfv_trm1 and rfv_bp
where
  "rfv_trm1 (rVr1 x) = {atom x}"
| "rfv_trm1 (rAp1 t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2)"
| "rfv_trm1 (rLm1 x t) = (rfv_trm1 t) - {atom x}"
| "rfv_trm1 (rLt1 bp t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2 - bv1 bp)"
| "rfv_bp (BUnit) = {}"
| "rfv_bp (BVr x) = {atom x}"
| "rfv_bp (BPr b1 b2) = (rfv_bp b1) \<union> (rfv_bp b2)"

(* needs to be stated by the package *)
instantiation 
  rtrm1 and bp :: pt
begin

primrec
  permute_rtrm1 and permute_bp
where
  "permute_rtrm1 pi (rVr1 a) = rVr1 (pi \<bullet> a)"
| "permute_rtrm1 pi (rAp1 t1 t2) = rAp1 (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)"
| "permute_rtrm1 pi (rLm1 a t) = rLm1 (pi \<bullet> a) (permute_rtrm1 pi t)"
| "permute_rtrm1 pi (rLt1 bp t1 t2) = rLt1 (permute_bp pi bp) (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)"
| "permute_bp pi (BUnit) = BUnit"
| "permute_bp pi (BVr a) = BVr (pi \<bullet> a)"
| "permute_bp pi (BPr bp1 bp2) = BPr (permute_bp pi bp1) (permute_bp pi bp2)"

lemma pt_rtrm1_bp_zero:
  fixes t::rtrm1
  and   b::bp
  shows "0 \<bullet> t = t"
  and   "0 \<bullet> b = b"
apply(induct t and b rule: rtrm1_bp.inducts)
apply(simp_all)
done

lemma pt_rtrm1_bp_plus:
  fixes t::rtrm1
  and   b::bp
  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
  and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
apply(induct t and b rule: rtrm1_bp.inducts)
apply(simp_all)
done

instance
apply default
apply(simp_all add: pt_rtrm1_bp_zero pt_rtrm1_bp_plus)
done

end

inductive
  alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)
where
  a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)"
| a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2"
| a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s"
| a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2"

lemma alpha1_inj:
"(rVr1 a \<approx>1 rVr1 b) = (a = b)"
"(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"
"(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s)))"
"(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))))"
apply -
apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
done

(* Shouyld we derive it? But bv is given by the user? *)
lemma bv1_eqvt[eqvt]:
  shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
  apply (induct x)
apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt)
done

lemma rfv_trm1_eqvt[eqvt]:
  shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
  apply (induct t)
  apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
  done


lemma alpha1_eqvt:
  shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
  apply (induct t s rule: alpha1.inducts)
  apply (simp_all add:eqvts alpha1_inj)
  apply (erule exE)
  apply (rule_tac x="pi \<bullet> pia" in exI)
  apply (simp add: alpha_gen)
  apply(erule conjE)+
  apply(rule conjI)
  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt rfv_trm1_eqvt)
  apply(rule conjI)
  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
  apply(simp add: atom_eqvt Diff_eqvt rfv_trm1_eqvt insert_eqvt empty_eqvt)
  apply(simp add: permute_eqvt[symmetric])
  apply (erule exE)
  apply (rule_tac x="pi \<bullet> pia" in exI)
  apply (simp add: alpha_gen)
  apply(erule conjE)+
  apply(rule conjI)
  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
  apply(simp add: rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
  apply(rule conjI)
  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
  apply(simp add: atom_eqvt rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
  apply(simp add: permute_eqvt[symmetric])
  done

lemma alpha1_equivp: "equivp alpha1" 
  sorry

quotient_type trm1 = rtrm1 / alpha1
  by (rule alpha1_equivp)

quotient_definition
  "Vr1 :: name \<Rightarrow> trm1"
as
  "rVr1"

quotient_definition
  "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
as
  "rAp1"

quotient_definition
  "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"
as
  "rLm1"

quotient_definition
  "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
as
  "rLt1"

quotient_definition
  "fv_trm1 :: trm1 \<Rightarrow> atom set"
as
  "rfv_trm1"

lemma alpha_rfv1:
  shows "t \<approx>1 s \<Longrightarrow> rfv_trm1 t = rfv_trm1 s"
  apply(induct rule: alpha1.induct)
  apply(simp_all add: alpha_gen.simps)
  done

lemma [quot_respect]:
 "(op = ===> alpha1) rVr1 rVr1"
 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"
 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1"
 "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"
apply (auto intro: alpha1.intros)
apply(rule a3) apply (rule_tac x="0" in exI)
apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
apply(rule a4) apply assumption apply (rule_tac x="0" in exI)
apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
done

lemma [quot_respect]:
  "(op = ===> alpha1 ===> alpha1) permute permute"
apply auto
apply (rule alpha1_eqvt)
apply simp
done

lemma [quot_respect]:
  "(alpha1 ===> op =) rfv_trm1 rfv_trm1"
apply (simp add: alpha_rfv1)
done

lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]

instantiation trm1 and bp :: pt
begin

quotient_definition
  "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
as
  "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"

lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]

instance
apply default
apply(induct_tac [!] x rule: trm1_bp_inducts(1))
apply(simp_all)
done

end

lemmas fv_trm1 = rfv_trm1_rfv_bp.simps[quot_lifted]

lemmas fv_trm1_eqvt = rfv_trm1_eqvt[quot_lifted]

lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

lemma lm1_supp_pre:
  shows "(supp (atom x, t)) supports (Lm1 x t) "
apply(simp add: supports_def)
apply(fold fresh_def)
apply(simp add: fresh_Pair swap_fresh_fresh)
apply(clarify)
apply(subst swap_at_base_simps(3))
apply(simp_all add: fresh_atom)
done

lemma lt1_supp_pre:
  shows "(supp (x, t, s)) supports (Lt1 t x s) "
apply(simp add: supports_def)
apply(fold fresh_def)
apply(simp add: fresh_Pair swap_fresh_fresh)
done

lemma bp_supp: "finite (supp (bp :: bp))"
  apply (induct bp)
  apply(simp_all add: supp_def)
  apply (fold supp_def)
  apply (simp add: supp_at_base)
  apply(simp add: Collect_imp_eq)
  apply(simp add: Collect_neg_eq[symmetric])
  apply (fold supp_def)
  apply (simp)
  done

instance trm1 :: fs
apply default
apply(induct_tac x rule: trm1_bp_inducts(1))
apply(simp_all)
apply(simp add: supp_def alpha1_INJ eqvts)
apply(simp add: supp_def[symmetric] supp_at_base)
apply(simp only: supp_def alpha1_INJ eqvts permute_trm1)
apply(simp add: Collect_imp_eq Collect_neg_eq)
apply(rule supports_finite)
apply(rule lm1_supp_pre)
apply(simp add: supp_Pair supp_atom)
apply(rule supports_finite)
apply(rule lt1_supp_pre)
apply(simp add: supp_Pair supp_atom bp_supp)
done

lemma supp_fv:
  shows "supp t = fv_trm1 t"
apply(induct t rule: trm1_bp_inducts(1))
apply(simp_all)
apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
apply(simp only: supp_at_base[simplified supp_def])
apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
apply(simp add: Collect_imp_eq Collect_neg_eq)
apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
apply(simp add: supp_Abs fv_trm1)
apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
apply(simp add: alpha1_INJ)
apply(simp add: Abs_eq_iff)
apply(simp add: alpha_gen.simps)
apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
apply(simp add: supp_Abs fv_trm1)
apply(simp (no_asm) add: supp_def)
apply(simp add: alpha1_INJ)
apply(simp add: Abs_eq_iff)
apply(simp add: alpha_gen)
apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)
apply(simp add: Collect_imp_eq Collect_neg_eq)
done

lemma trm1_supp:
  "supp (Vr1 x) = {atom x}"
  "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
  "supp (Lm1 x t) = (supp t) - {atom x}"
  "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
  by (simp_all only: supp_fv fv_trm1)

lemma trm1_induct_strong:
  assumes "\<And>name b. P b (Vr1 name)"
  and     "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
  and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
  and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
  shows   "P a rtrma"
sorry

section {*** lets with single assignments ***}

datatype rtrm2 =
  rVr2 "name"
| rAp2 "rtrm2" "rtrm2"
| rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)"
| rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)"
and rassign =
  rAs "name" "rtrm2"

(* to be given by the user *)
primrec 
  rbv2
where
  "rbv2 (rAs x t) = {atom x}"

(* needs to be calculated by the package *)
primrec
  fv_rtrm2 and fv_rassign
where
  "fv_rtrm2 (rVr2 x) = {atom x}"
| "fv_rtrm2 (rAp2 t1 t2) = (fv_rtrm2 t1) \<union> (fv_rtrm2 t2)"
| "fv_rtrm2 (rLm2 x t) = (fv_rtrm2 t) - {atom x}"
| "fv_rtrm2 (rLt2 as t) = (fv_rtrm2 t - rbv2 as) \<union> (fv_rassign as)"
| "fv_rassign (rAs x t) = fv_rtrm2 t"

(* needs to be stated by the package *)
instantiation
  rtrm2 and rassign :: pt
begin

primrec
  permute_rtrm2 and permute_rassign
where
  "permute_rtrm2 pi (rVr2 a) = rVr2 (pi \<bullet> a)"
| "permute_rtrm2 pi (rAp2 t1 t2) = rAp2 (permute_rtrm2 pi t1) (permute_rtrm2 pi t2)"
| "permute_rtrm2 pi (rLm2 a t) = rLm2 (pi \<bullet> a) (permute_rtrm2 pi t)"
| "permute_rtrm2 pi (rLt2 as t) = rLt2 (permute_rassign pi as) (permute_rtrm2 pi t)"
| "permute_rassign pi (rAs a t) = rAs (pi \<bullet> a) (permute_rtrm2 pi t)"

lemma pt_rtrm2_rassign_zero:
  fixes t::rtrm2
  and   b::rassign
  shows "0 \<bullet> t = t"
  and   "0 \<bullet> b = b"
apply(induct t and b rule: rtrm2_rassign.inducts)
apply(simp_all)
done

lemma pt_rtrm2_rassign_plus:
  fixes t::rtrm2
  and   b::rassign
  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
  and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
apply(induct t and b rule: rtrm2_rassign.inducts)
apply(simp_all)
done

instance
apply default
apply(simp_all add: pt_rtrm2_rassign_zero pt_rtrm2_rassign_plus)
done


end

inductive
  alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
and
  alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100)
where
  a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)"
| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2"
| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s"
| a4: "\<lbrakk>\<exists>pi. ((rbv2 bt, t) \<approx>gen alpha2 fv_rtrm2 pi ((rbv2 bs), s));
        \<exists>pi. ((rbv2 bt, bt) \<approx>gen alpha2a fv_rassign pi (rbv2 bs, bs))\<rbrakk>
        \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s"
| a5: "\<lbrakk>a = b; t \<approx>2 s\<rbrakk> \<Longrightarrow> rAs a t \<approx>2a rAs b s" (* This way rbv2 can be lifted *)

lemma alpha2_equivp:
  "equivp alpha2"
  "equivp alpha2a"
  sorry

quotient_type
  trm2 = rtrm2 / alpha2
and
  assign = rassign / alpha2a
  by (auto intro: alpha2_equivp)



section {*** lets with many assignments ***}

datatype trm3 =
  Vr3 "name"
| Ap3 "trm3" "trm3"
| Lm3 "name" "trm3" --"bind (name) in (trm3)"
| Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)"
and assigns =
  ANil
| ACons "name" "trm3" "assigns"

(* to be given by the user *)
primrec 
  bv3
where
  "bv3 ANil = {}"
| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"

primrec
  fv_trm3 and fv_assigns
where
  "fv_trm3 (Vr3 x) = {atom x}"
| "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)"
| "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {atom x}"
| "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)"
| "fv_assigns (ANil) = {}"
| "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)"

(* needs to be stated by the package *)
instantiation
 trm3 and assigns :: pt
begin

primrec
  permute_trm3 and permute_assigns
where
  "permute_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)"
| "permute_trm3 pi (Ap3 t1 t2) = Ap3 (permute_trm3 pi t1) (permute_trm3 pi t2)"
| "permute_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (permute_trm3 pi t)"
| "permute_trm3 pi (Lt3 as t) = Lt3 (permute_assigns pi as) (permute_trm3 pi t)"
| "permute_assigns pi (ANil) = ANil"
| "permute_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (permute_trm3 pi t) (permute_assigns pi as)"

lemma pt_trm3_assigns_zero:
  fixes t::trm3
  and   b::assigns
  shows "0 \<bullet> t = t"
  and   "0 \<bullet> b = b"
apply(induct t and b rule: trm3_assigns.inducts)
apply(simp_all)
done

lemma pt_trm3_assigns_plus:
  fixes t::trm3
  and   b::assigns
  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
  and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
apply(induct t and b rule: trm3_assigns.inducts)
apply(simp_all)
done

instance
apply default
apply(simp_all add: pt_trm3_assigns_zero pt_trm3_assigns_plus)
done


end

inductive
  alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)
and
  alpha3a :: "assigns \<Rightarrow> assigns \<Rightarrow> bool" ("_ \<approx>3a _" [100, 100] 100)
where
  a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)"
| a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"
| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha3 fv_rtrm3 pi ({atom b}, s))) \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
| a4: "\<lbrakk>\<exists>pi. ((bv3 bt, t) \<approx>gen alpha3 fv_trm3 pi ((bv3 bs), s));
        \<exists>pi. ((bv3 bt, bt) \<approx>gen alpha3a fv_assign pi (bv3 bs, bs))\<rbrakk>
        \<Longrightarrow> Lt3 bt t \<approx>3 Lt3 bs s"
| a5: "ANil \<approx>3a ANil"
| a6: "\<lbrakk>a = b; t \<approx>3 s; tt \<approx>3a st\<rbrakk> \<Longrightarrow> ACons a t tt \<approx>3a ACons b s st"

lemma alpha3_equivp:
  "equivp alpha3"
  "equivp alpha3a"
  sorry

quotient_type
  qtrm3 = trm3 / alpha3
and
  qassigns = assigns / alpha3a
  by (auto intro: alpha3_equivp)


section {*** lam with indirect list recursion ***}

datatype trm4 =
  Vr4 "name"
| Ap4 "trm4" "trm4 list"
| Lm4 "name" "trm4"  --"bind (name) in (trm)"

thm trm4.recs

primrec
  fv_trm4 and fv_trm4_list
where
  "fv_trm4 (Vr4 x) = {atom x}"
| "fv_trm4 (Ap4 t ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"
| "fv_trm4 (Lm4 x t) = (fv_trm4 t) - {atom x}"
| "fv_trm4_list ([]) = {}"
| "fv_trm4_list (t#ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"


(* needs to be stated by the package *)
(* there cannot be a clause for lists, as *) 
(* permutations are  already defined in Nominal (also functions, options, and so on) *)
instantiation
  trm4 :: pt
begin

(* does not work yet *)
primrec
  permute_trm4  and permute_trm4_list
where
  "permute_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)"
| "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute_trm4_list pi ts)"
| "permute_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (permute_trm4 pi t)"
| "permute_trm4_list pi ([]) = []"
| "permute_trm4_list pi (t#ts) = (permute_trm4 pi t) # (permute_trm4_list pi ts)"

lemma pt_trm4_list_zero:
  fixes t::trm4
  and   ts::"trm4 list"
  shows "0 \<bullet> t = t"
  and   "permute_trm4_list 0 ts = ts"
apply(induct t and ts rule: trm4.inducts)
apply(simp_all)
done

lemma pt_trm4_list_plus:
  fixes t::trm4
  and   ts::"trm4 list"
  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
  and   "(permute_trm4_list (p + q) ts) = permute_trm4_list p (permute_trm4_list q ts)"
apply(induct t and ts rule: trm4.inducts)
apply(simp_all)
done


instance
apply(default)
apply(simp_all add: pt_trm4_list_zero pt_trm4_list_plus)
done

end

(* "repairing" of the permute function *)
lemma repaired:
  fixes ts::"trm4 list"
  shows "permute_trm4_list p ts = p \<bullet> ts"
  apply(induct ts)
  apply(simp_all)
  done

thm permute_trm4_permute_trm4_list.simps
thm permute_trm4_permute_trm4_list.simps[simplified repaired]

inductive
    alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)
and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) 
where
  a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)"
| a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"
| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha4 fv_rtrm4 pi ({atom b}, s))) \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"
| a5: "[] \<approx>4list []"
| a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)"

lemma alpha4_equivp: "equivp alpha4" sorry
lemma alpha4list_equivp: "equivp alpha4list" sorry

quotient_type 
  qtrm4 = trm4 / alpha4 and
  qtrm4list = "trm4 list" / alpha4list
  by (simp_all add: alpha4_equivp alpha4list_equivp)


datatype rtrm5 =
  rVr5 "name"
| rAp5 "rtrm5" "rtrm5"
| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
and rlts =
  rLnil
| rLcons "name" "rtrm5" "rlts"

primrec
  rbv5
where
  "rbv5 rLnil = {}"
| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"

primrec
  rfv_trm5 and rfv_lts
where
  "rfv_trm5 (rVr5 n) = {atom n}"
| "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)"
| "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - rbv5 lts) \<union> (rfv_lts lts - rbv5 lts)"
| "rfv_lts (rLnil) = {}"
| "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)"

instantiation
  rtrm5 and rlts :: pt
begin

primrec
  permute_rtrm5 and permute_rlts
where
  "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)"
| "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)"
| "permute_rtrm5 pi (rLt5 ls t) = rLt5 (permute_rlts pi ls) (permute_rtrm5 pi t)"
| "permute_rlts pi (rLnil) = rLnil"
| "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)"

lemma pt_rtrm5_zero:
  fixes t::rtrm5
  and   l::rlts
  shows "0 \<bullet> t = t"
  and   "0 \<bullet> l = l"
apply(induct t and l rule: rtrm5_rlts.inducts)
apply(simp_all)
done

lemma pt_rtrm5_plus:
  fixes t::rtrm5
  and   l::rlts
  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
  and   "((p + q) \<bullet> l) = p \<bullet> (q \<bullet> l)"
apply(induct t and l rule: rtrm5_rlts.inducts)
apply(simp_all)
done

instance
apply default
apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus)
done

end

inductive
  alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
and
  alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
where
  a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
| a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2)); 
        \<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2))\<rbrakk>
        \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
| a4: "rLnil \<approx>l rLnil"
| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"

print_theorems

lemma alpha5_inj:
  "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
  "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
  "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2))) \<and>
         (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2))))"
  "rLnil \<approx>l rLnil"
  "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)"
apply -
apply (simp_all add: alpha5_alphalts.intros)
apply rule
apply (erule alpha5.cases)
apply (simp_all add: alpha5_alphalts.intros)
apply rule
apply (erule alpha5.cases)
apply (simp_all add: alpha5_alphalts.intros)
apply rule
apply (erule alpha5.cases)
apply (simp_all add: alpha5_alphalts.intros)
apply rule
apply (erule alphalts.cases)
apply (simp_all add: alpha5_alphalts.intros)
done

lemma alpha5_equivps:
  shows "equivp alpha5"
  and   "equivp alphalts"
sorry

quotient_type
  trm5 = rtrm5 / alpha5
and
  lts = rlts / alphalts
  by (auto intro: alpha5_equivps)

quotient_definition
  "Vr5 :: name \<Rightarrow> trm5"
as
  "rVr5"

quotient_definition
  "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
as
  "rAp5"

quotient_definition
  "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
as
  "rLt5"

quotient_definition
  "Lnil :: lts"
as
  "rLnil"

quotient_definition
  "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
as
  "rLcons"

quotient_definition
   "fv_trm5 :: trm5 \<Rightarrow> atom set"
as
  "rfv_trm5"

quotient_definition
   "fv_lts :: lts \<Rightarrow> atom set"
as
  "rfv_lts"

quotient_definition
   "bv5 :: lts \<Rightarrow> atom set"
as
  "rbv5"

lemma rbv5_eqvt:
  "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
sorry

lemma rfv_trm5_eqvt:
  "pi \<bullet> (rfv_trm5 x) = rfv_trm5 (pi \<bullet> x)"
sorry

lemma rfv_lts_eqvt:
  "pi \<bullet> (rfv_lts x) = rfv_lts (pi \<bullet> x)"
sorry

lemma alpha5_eqvt:
  "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
  "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
  apply(induct rule: alpha5_alphalts.inducts)
  apply (simp_all add: alpha5_inj)
  apply (erule exE)+
  apply(unfold alpha_gen)
  apply (erule conjE)+
  apply (rule conjI)
  apply (rule_tac x="x \<bullet> pi" in exI)
  apply (rule conjI)
  apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_trm5_eqvt)
  apply(rule conjI)
  apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_trm5_eqvt)
  apply (subst permute_eqvt[symmetric])
  apply (simp)
  apply (rule_tac x="x \<bullet> pia" in exI)
  apply (rule conjI)
  apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_lts_eqvt)
  apply(rule conjI)
  apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_lts_eqvt)
  apply (subst permute_eqvt[symmetric])
  apply (simp)
  done

lemma alpha5_rfv:
  "(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)"
  "(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)"
  apply(induct rule: alpha5_alphalts.inducts)
  apply(simp_all add: alpha_gen)
  done

lemma bv_list_rsp:
  shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
  apply(induct rule: alpha5_alphalts.inducts(2))
  apply(simp_all)
  done

lemma [quot_respect]:
  "(alphalts ===> op =) rfv_lts rfv_lts"
  "(alpha5 ===> op =) rfv_trm5 rfv_trm5"
  "(alphalts ===> op =) rbv5 rbv5"
  "(op = ===> alpha5) rVr5 rVr5"
  "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
  "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
  "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
  "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
  "(op = ===> alpha5 ===> alpha5) permute permute"
  "(op = ===> alphalts ===> alphalts) permute permute"
  apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
  apply (auto)
  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
  done

lemma
  shows "(alphalts ===> op =) rbv5 rbv5"
  by (simp add: bv_list_rsp)

lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]

instantiation trm5 and lts :: pt
begin

quotient_definition
  "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
as
  "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"

quotient_definition
  "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
as
  "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"

lemma trm5_lts_zero:
  "0 \<bullet> (x\<Colon>trm5) = x"
  "0 \<bullet> (y\<Colon>lts) = y"
apply(induct x and y rule: trm5_lts_inducts)
apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
done

lemma trm5_lts_plus:
  "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
  "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y"
apply(induct x and y rule: trm5_lts_inducts)
apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
done

instance
apply default
apply (simp_all add: trm5_lts_zero trm5_lts_plus)
done

end

lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]

lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

lemmas bv5[simp] = rbv5.simps[quot_lifted]

lemmas fv_trm5_lts[simp] = rfv_trm5_rfv_lts.simps[quot_lifted]

lemma lets_ok:
  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
apply (subst alpha5_INJ)
apply (rule conjI)
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
apply (simp only: alpha_gen)
apply (simp add: permute_trm5_lts fresh_star_def)
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
apply (simp only: alpha_gen)
apply (simp add: permute_trm5_lts fresh_star_def)
done

lemma lets_ok2:
  "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
   (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
apply (subst alpha5_INJ)
apply (rule conjI)
apply (rule_tac x="0 :: perm" in exI)
apply (simp only: alpha_gen)
apply (simp add: permute_trm5_lts fresh_star_def)
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
apply (simp only: alpha_gen)
apply (simp add: permute_trm5_lts fresh_star_def)
done


lemma lets_not_ok1:
  "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
             (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
apply (subst alpha5_INJ(3))
apply(clarify)
apply (simp add: alpha_gen)
apply (simp add: permute_trm5_lts fresh_star_def)
apply (simp add: alpha5_INJ(5))
apply(clarify)
apply (simp add: alpha5_INJ(2))
apply (simp only: alpha5_INJ(1))
done

lemma distinct_helper:
  shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
  apply auto
  apply (erule alpha5.cases)
  apply (simp_all only: rtrm5.distinct)
  done

lemma distinct_helper2:
  shows "(Vr5 x) \<noteq> (Ap5 y z)"
  by (lifting distinct_helper)

lemma lets_nok:
  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
   (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
   (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
apply (subst alpha5_INJ)
apply (simp only: alpha_gen permute_trm5_lts fresh_star_def)
apply (subst alpha5_INJ(5))
apply (subst alpha5_INJ(5))
apply (simp add: distinct_helper2)
done


(* example with a bn function defined over the type itself *)
datatype rtrm6 =
  rVr6 "name"
| rLm6 "name" "rtrm6"
| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"

primrec
  rbv6
where
  "rbv6 (rVr6 n) = {}"
| "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
| "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"

primrec
  rfv_trm6
where
  "rfv_trm6 (rVr6 n) = {atom n}"
| "rfv_trm6 (rLm6 n t) = (rfv_trm6 t) - {atom n}"
| "rfv_trm6 (rLt6 l r) = (rfv_trm6 r - rbv6 l) \<union> rfv_trm6 l"

instantiation
  rtrm6 :: pt
begin

primrec
  permute_rtrm6
where
  "permute_rtrm6 pi (rVr6 a) = rVr6 (pi \<bullet> a)"
| "permute_rtrm6 pi (rLm6 n t) = rLm6 (pi \<bullet> n) (permute_rtrm6 pi t)"
| "permute_rtrm6 pi (rLt6 l r) = rLt6 (permute_rtrm6 pi l) (permute_rtrm6 pi r)"

lemma pt_rtrm6_zero:
  fixes t::rtrm6
  shows "0 \<bullet> t = t"
apply(induct t)
apply(simp_all)
done

lemma pt_rtrm6_plus:
  fixes t::rtrm6
  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
apply(induct t)
apply(simp_all)
done

instance
apply default
apply(simp_all add: pt_rtrm6_zero pt_rtrm6_plus)
done

end

inductive
  alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100)
where
  a1: "a = b \<Longrightarrow> (rVr6 a) \<approx>6 (rVr6 b)"
| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha6 rfv_trm6 pi ({atom b}, s))) \<Longrightarrow> rLm6 a t \<approx>6 rLm6 b s"
| a3: "(\<exists>pi. (((rbv6 t1), s1) \<approx>gen alpha6 rfv_trm6 pi ((rbv6 t2), s2))) \<Longrightarrow> rLt6 t1 s1 \<approx>6 rLt6 t2 s2"

lemma alpha6_equivps:
  shows "equivp alpha6"
sorry

quotient_type
  trm6 = rtrm6 / alpha6
  by (auto intro: alpha6_equivps)

quotient_definition
  "Vr6 :: name \<Rightarrow> trm6"
as
  "rVr6"

quotient_definition
  "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6"
as
  "rLm6"

quotient_definition
  "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
as
  "rLt6"

quotient_definition
   "fv_trm6 :: trm6 \<Rightarrow> atom set"
as
  "rfv_trm6"

quotient_definition
   "bv6 :: trm6 \<Rightarrow> atom set"
as
  "rbv6"

lemma [quot_respect]:
  "(op = ===> alpha6 ===> alpha6) permute permute"
apply auto (* will work with eqvt *)
sorry

(* Definitely not true , see lemma below *)

lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6"
apply simp apply clarify
apply (erule alpha6.induct)
oops

lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha6 ===> op =) rbv6 rbv6"
apply simp
apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in  exI)
apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in  exI)
apply simp
apply (rule a2)
apply (rule_tac x="(a \<leftrightarrow> b)" in  exI)
apply (simp add: alpha_gen fresh_star_def)
apply (rule a1)
apply (rule refl)
done

lemma [quot_respect]:"(alpha6 ===> op =) rfv_trm6 rfv_trm6"
apply simp apply clarify
apply (induct_tac x y rule: alpha6.induct)
apply simp_all
apply (erule exE)
apply (simp_all add: alpha_gen)
apply (erule conjE)+
apply (erule exE)
apply (erule conjE)+
apply (simp)
oops


lemma [quot_respect]: "(op = ===> alpha6) rVr6 rVr6"
by (simp_all add: a1)

lemma [quot_respect]:
 "(op = ===> alpha6 ===> alpha6) rLm6 rLm6"
 "(alpha6 ===> alpha6 ===> alpha6) rLt6 rLt6"
apply simp_all apply (clarify)
apply (rule a2)
apply (rule_tac x="0::perm" in exI)
apply (simp add: alpha_gen)
(* needs rfv6_rsp *) defer
apply clarify
apply (rule a3)
apply (rule_tac x="0::perm" in exI)
apply (simp add: alpha_gen)
(* needs rbv6_rsp *)
oops

instantiation trm6 :: pt begin

quotient_definition
  "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6"
as
  "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"

instance
apply default
sorry
end

lemma lifted_induct:
"\<lbrakk>x1 = x2; \<And>a b. a = b \<Longrightarrow> P (Vr6 a) (Vr6 b);
 \<And>a t b s.
   \<exists>pi. fv_trm6 t - {atom a} = fv_trm6 s - {atom b} \<and>
        (fv_trm6 t - {atom a}) \<sharp>* pi \<and> pi \<bullet> t = s \<and> P (pi \<bullet> t) s \<Longrightarrow>
   P (Lm6 a t) (Lm6 b s);
 \<And>t1 s1 t2 s2.
   \<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and>
        (fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<and> P (pi \<bullet> s1) s2 \<Longrightarrow>
   P (Lt6 t1 s1) (Lt6 t2 s2)\<rbrakk>
 \<Longrightarrow> P x1 x2"
unfolding alpha_gen
apply (lifting alpha6.induct[unfolded alpha_gen])
apply injection
(* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *)
oops

lemma lifted_inject_a3:
 "\<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and>
    (fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<Longrightarrow> Lt6 t1 s1 = Lt6 t2 s2"
apply(lifting a3[unfolded alpha_gen])
apply injection
(* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *)
oops




(* example with a respectful bn function defined over the type itself *)
datatype rtrm7 =
  rVr7 "name"
| rLm7 "name" "rtrm7"
| 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"

primrec
  rfv_trm7
where
  "rfv_trm7 (rVr7 n) = {}"
| "rfv_trm7 (rLm7 n t) = {atom n} \<union> (rfv_trm7 t)"
| "rfv_trm7 (rLt7 l r) = (rfv_trm7 r) \<union> (rfv_trm7 l)"






text {* type schemes *} 
datatype ty = 
  Var "name" 
| Fun "ty" "ty"

instantiation
  ty :: pt
begin

primrec
  permute_ty 
where
  "permute_ty pi (Var a) = Var (pi \<bullet> a)"
| "permute_ty pi (Fun T1 T2) = Fun (permute_ty pi T1) (permute_ty pi T2)"

lemma pt_ty_zero:
  fixes T::ty
  shows "0 \<bullet> T = T"
apply(induct T rule: ty.inducts)
apply(simp_all)
done

lemma pt_ty_plus:
  fixes T::ty
  shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"
apply(induct T rule: ty.inducts)
apply(simp_all)
done

instance
apply default
apply(simp_all add: pt_ty_zero pt_ty_plus)
done

end

datatype tyS = 
  All "name set" "ty" 

instantiation
  tyS :: pt
begin

primrec
  permute_tyS 
where
  "permute_tyS pi (All xs T) = All (pi \<bullet> xs) (pi \<bullet> T)"

lemma pt_tyS_zero:
  fixes T::tyS
  shows "0 \<bullet> T = T"
apply(induct T rule: tyS.inducts)
apply(simp_all)
done

lemma pt_tyS_plus:
  fixes T::tyS
  shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"
apply(induct T rule: tyS.inducts)
apply(simp_all)
done

instance
apply default
apply(simp_all add: pt_tyS_zero pt_tyS_plus)
done

end


abbreviation
  "atoms xs \<equiv> {atom x| x. x \<in> xs}"

primrec
  rfv_ty
where
  "rfv_ty (Var n) = {atom n}"
| "rfv_ty (Fun T1 T2) = (rfv_ty T1) \<union> (rfv_ty T2)"

primrec
  rfv_tyS
where 
  "rfv_tyS (All xs T) = (rfv_ty T - atoms xs)"

inductive
  alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
where
  a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) rfv_ty pi (atoms xs2, T2)) 
        \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"

lemma
  shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"
  apply(rule a1)
  apply(simp add: alpha_gen)
  apply(rule_tac x="0::perm" in exI)
  apply(simp add: fresh_star_def)
  done

lemma
  shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"
  apply(rule a1)
  apply(simp add: alpha_gen)
  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
  apply(simp add: fresh_star_def)
  done

lemma
  shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"
  apply(rule a1)
  apply(simp add: alpha_gen)
  apply(rule_tac x="0::perm" in exI)
  apply(simp add: fresh_star_def)
  done

lemma
  assumes a: "a \<noteq> b"
  shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"
  using a
  apply(clarify)
  apply(erule alpha_tyS.cases)
  apply(simp add: alpha_gen)
  apply(erule conjE)+
  apply(erule exE)
  apply(erule conjE)+
  apply(clarify)
  apply(simp)
  apply(simp add: fresh_star_def)
  apply(auto)
  done


end
