# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266425495 -3600
# Node ID 3c32f91fa77107ce8162af0b1598d153c4acb0aa
# Parent  788a59d2d7aae1022c691703055c97331e84e942
Terms2 with bindings for binders synchronized with bindings they are used in.

diff -r 788a59d2d7aa -r 3c32f91fa771 Quot/Nominal/Terms2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Nominal/Terms2.thy	Wed Feb 17 17:51:35 2010 +0100
@@ -0,0 +1,1141 @@
+theory Terms
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"
+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)"
+
+local_setup {* define_raw_fv "Terms.rtrm1"
+  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
+   [[], [[]], [[], []]]] *}
+print_theorems
+
+setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}
+
+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 fv_rtrm1 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 fv_rtrm1 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 fv_rtrm1 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 fv_rtrm1 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 fv_rtrm1_eqvt[eqvt]:
+    "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
+    "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
+  apply (induct t and b)
+  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 fv_rtrm1_eqvt)
+  apply(rule conjI)
+  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
+  apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_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: fv_rtrm1_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 fv_rtrm1_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"
+is
+  "rVr1"
+
+quotient_definition
+  "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
+is
+  "rAp1"
+
+quotient_definition
+  "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"
+is
+  "rLm1"
+
+quotient_definition
+  "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
+is
+  "rLt1"
+
+quotient_definition
+  "fv_trm1 :: trm1 \<Rightarrow> atom set"
+is
+  "fv_rtrm1"
+
+lemma alpha_rfv1:
+  shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
+  apply(induct rule: alpha1.induct)
+  apply(simp_all add: alpha_gen.simps)
+  sorry
+
+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 simp add: alpha1_inj)
+apply (rule_tac x="0" in exI)
+apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
+apply (rule_tac x="0" in exI)
+apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1)
+done
+
+lemma [quot_respect]:
+  "(op = ===> alpha1 ===> alpha1) permute permute"
+  by (simp add: alpha1_eqvt)
+
+lemma [quot_respect]:
+  "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1"
+  by (simp add: alpha_rfv1)
+
+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"
+is
+  "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 = fv_rtrm1_fv_bp.simps[quot_lifted]
+
+lemmas fv_trm1_eqvt = fv_rtrm1_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*)
+sorry
+
+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)"
+sorry (*  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; bv1 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}"
+
+local_setup {* define_raw_fv "Terms.rtrm2"
+  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]],
+   [[[], []]]] *}
+print_theorems
+
+setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
+
+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)"
+
+local_setup {* define_raw_fv "Terms.trm3"
+  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv3}, 0)], [(SOME @{term bv3}, 0)]]],
+   [[], [[], [], []]]] *}
+print_theorems
+
+setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}
+
+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)"
+print_theorems
+
+thm trm4.recs
+
+local_setup {* define_raw_fv "Terms.trm4" [
+  [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]]  ] *}
+print_theorems
+
+(* there cannot be a clause for lists, as *)
+(* permutations are  already defined in Nominal (also functions, options, and so on) *)
+setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *}
+
+(* "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)"
+
+local_setup {* define_raw_fv "Terms.rtrm5" [
+  [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ] *}
+print_theorems
+
+setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
+print_theorems
+
+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 fv_rtrm5 pi (rbv5 l2, t2)); 
+        \<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts 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 fv_rtrm5 pi (rbv5 l2, t2))) \<and>
+         (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts 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"
+is
+  "rVr5"
+
+quotient_definition
+  "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
+is
+  "rAp5"
+
+quotient_definition
+  "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
+is
+  "rLt5"
+
+quotient_definition
+  "Lnil :: lts"
+is
+  "rLnil"
+
+quotient_definition
+  "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
+is
+  "rLcons"
+
+quotient_definition
+   "fv_trm5 :: trm5 \<Rightarrow> atom set"
+is
+  "fv_rtrm5"
+
+quotient_definition
+   "fv_lts :: lts \<Rightarrow> atom set"
+is
+  "fv_rlts"
+
+quotient_definition
+   "bv5 :: lts \<Rightarrow> atom set"
+is
+  "rbv5"
+
+lemma rbv5_eqvt:
+  "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
+sorry
+
+lemma fv_rtrm5_eqvt:
+  "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
+sorry
+
+lemma fv_rlts_eqvt:
+  "pi \<bullet> (fv_rlts x) = fv_rlts (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 fv_rtrm5_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 fv_rtrm5_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 fv_rlts_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 fv_rlts_eqvt)
+  apply (subst permute_eqvt[symmetric])
+  apply (simp)
+  done
+
+lemma alpha5_rfv:
+  "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
+  "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts 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 =) fv_rlts fv_rlts"
+  "(alpha5 ===> op =) fv_rtrm5 fv_rtrm5"
+  "(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 (clarify) apply (rule conjI)
+  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 (clarify) apply (rule conjI)
+  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"
+is
+  "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
+
+quotient_definition
+  "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
+is
+  "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] = fv_rtrm5_fv_rlts.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"
+
+local_setup {* define_raw_fv "Terms.rtrm6" [
+  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *}
+print_theorems 
+
+setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}
+print_theorems
+
+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 fv_rtrm6 pi ({atom b}, s))) \<Longrightarrow> rLm6 a t \<approx>6 rLm6 b s"
+| a3: "(\<exists>pi. (((rbv6 t1), s1) \<approx>gen alpha6 fv_rtrm6 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"
+is
+  "rVr6"
+
+quotient_definition
+  "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6"
+is
+  "rLm6"
+
+quotient_definition
+  "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
+is
+  "rLt6"
+
+quotient_definition
+   "fv_trm6 :: trm6 \<Rightarrow> atom set"
+is
+  "fv_rtrm6"
+
+quotient_definition
+   "bv6 :: trm6 \<Rightarrow> atom set"
+is
+  "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 =) fv_rtrm6 fv_rtrm6"
+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"
+is
+  "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"
+
+local_setup {* define_raw_fv "Terms.rtrm7" [
+  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *}
+print_theorems 
+
+setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}
+print_theorems
+
+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 bvfv7: "rbv7 x = fv_rtrm7 x"
+  apply induct
+  apply simp_all
+sorry (*done*)
+
+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
+
+
+
+
+
+datatype rfoo8 =
+  Foo0 "name"
+| Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo"
+and rbar8 =
+  Bar0 "name"
+| Bar1 "name" "name" "rbar8" --"bind second name in b"
+
+primrec
+  rbv8
+where
+  "rbv8 (Bar0 x) = {}"
+| "rbv8 (Bar1 v x b) = {atom v}"
+
+local_setup {* define_raw_fv "Terms.rfoo8" [
+  [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+print_theorems 
+
+setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}
+print_theorems
+
+inductive
+  alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
+and
+  alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"
+| a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"
+| a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
+| a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"
+
+lemma "(alpha8b ===> op =) rbv8 rbv8"
+  apply simp apply clarify
+  apply (erule alpha8f_alpha8b.inducts(2))
+  apply (simp_all)
+done
+
+lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y"
+  apply (erule alpha8f_alpha8b.inducts(2))
+  apply (simp_all add: alpha_gen)
+done
+lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8"
+  apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp)
+done
+
+lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8"
+  apply simp apply clarify
+  apply (erule alpha8f_alpha8b.inducts(1))
+  apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
+sorry (*done*)
+
+
+
+
+
+
+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}"
+
+local_setup {* define_raw_fv "Terms.rlam9" [
+  [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *}
+print_theorems
+
+setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}
+print_theorems
+
+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
+
+quotient_definition
+  "qVar9 :: name \<Rightarrow> lam9"
+is
+  "Var9"
+
+quotient_definition
+  "qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9"
+is
+  "Lam9"
+
+quotient_definition
+  "qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9"
+is
+  "Bla9"
+
+quotient_definition
+  "fv_lam9 :: lam9 \<Rightarrow> atom set"
+is
+  "fv_rlam9"
+
+quotient_definition
+  "fv_bla9 :: bla9 \<Rightarrow> atom set"
+is
+  "fv_rbla9"
+
+quotient_definition
+  "bv9 :: lam9 \<Rightarrow> atom set"
+is
+  "rbv9"
+
+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
+
+
+
+
+
+
+
+
+text {* type schemes *} 
+datatype ty = 
+  Var "name" 
+| Fun "ty" "ty"
+
+setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *}
+print_theorems
+
+datatype tyS = 
+  All "name set" "ty" 
+
+setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
+print_theorems
+
+abbreviation
+  "atoms xs \<equiv> {atom x| x. x \<in> xs}"
+
+local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *}
+print_theorems 
+
+(*
+doesn't work yet
+local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *}
+print_theorems
+*)
+
+primrec
+  fv_tyS
+where 
+  "fv_tyS (All xs T) = (fv_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 =) fv_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