nominal2: comparison Quot/Nominal/Terms.thy

equal deleted inserted replaced

-:789fbba5c23f
+:3f36936f1280
 theory Terms
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"
 begin
 atom_decl name
 text {* primrec seems to be genarally faster than fun *}
 where
 "bv1 (BUnit) = {}"
 | "bv1 (BVr x) = {atom x}"
 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
-(* needs to be calculated by the package *)
+local_setup {* define_raw_fv "Terms.rtrm1"
-primrec
+[[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
-rfv_trm1 and rfv_bp
+[[], [[]], [[], []]]] *}
-where
+print_theorems
-"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)"
 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 rfv_trm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s"
+| 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 rfv_trm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2"
+| 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 rfv_trm1 pi ({atom ab}, s)))"
+"(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 rfv_trm1 pi ((bv1 b2), s2))))"
+"(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)
 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]:
+lemma fv_rtrm1_eqvt[eqvt]:
-shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
+shows "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
 apply (induct t)
 apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
 done
 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(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 rfv_trm1_eqvt insert_eqvt empty_eqvt)
+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: rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
+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 rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
+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
 "rLt1"
 quotient_definition
 "fv_trm1 :: trm1 \<Rightarrow> atom set"
 is
-"rfv_trm1"
+"fv_rtrm1"
 lemma alpha_rfv1:
-shows "t \<approx>1 s \<Longrightarrow> rfv_trm1 t = rfv_trm1 s"
+shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
 apply(induct rule: alpha1.induct)
 apply(simp_all add: alpha_gen.simps)
 done
 lemma [quot_respect]:
 apply (rule alpha1_eqvt)
 apply simp
 done
 lemma [quot_respect]:
-"(alpha1 ===> op =) rfv_trm1 rfv_trm1"
+"(alpha1 ===> op =) fv_rtrm1 fv_rtrm1"
 apply (simp add: alpha_rfv1)
 done
 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
 apply(simp_all)
 done
 end
-lemmas fv_trm1 = rfv_trm1_rfv_bp.simps[quot_lifted]
+lemmas fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
-lemmas fv_trm1_eqvt = rfv_trm1_eqvt[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) "
 primrec
 rbv2
 where
 "rbv2 (rAs x t) = {atom x}"
-(* needs to be calculated by the package *)
+local_setup {* define_raw_fv "Terms.rtrm2"
-primrec
+[[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],
-fv_rtrm2 and fv_rassign
+[[[(NONE, 0)], []]]] *}
-where
+print_theorems
-"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"
 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
 inductive
 alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
 bv3
 where
 "bv3 ANil = {}"
 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
-primrec
+local_setup {* define_raw_fv "Terms.trm3"
-fv_trm3 and fv_assigns
+[[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
-where
+[[], [[(NONE, 0)], [], []]]] *}
-"fv_trm3 (Vr3 x) = {atom x}"
+print_theorems
-| "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)"
 setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}
 inductive
 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)
 datatype trm4 =
 Vr4 "name"
 | Ap4 "trm4" "trm4 list"
 | Lm4 "name" "trm4"  --"bind (name) in (trm)"
+print_theorems
 thm trm4.recs
-primrec
+local_setup {* define_raw_fv "Terms.trm4" [
-fv_trm4 and fv_trm4_list
+[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]]  ] *}
-where
+print_theorems
-"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)"
 (* 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"] *}
 rbv5
 where
 "rbv5 rLnil = {}"
 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
-primrec
+local_setup {* define_raw_fv "Terms.rtrm5" [
-rfv_trm5 and rfv_lts
+[[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE, 0)], [], []]]  ] *}
-where
+print_theorems
-"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)"
 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
 print_theorems
 inductive
 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));
+| a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2));
-\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2))\<rbrakk>
+\<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 rfv_trm5 pi (rbv5 l2, t2))) \<and>
+"(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 rfv_lts pi (rbv5 l2, l2))))"
+(\<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
 "rLcons"
 quotient_definition
 "fv_trm5 :: trm5 \<Rightarrow> atom set"
 is
-"rfv_trm5"
+"fv_rtrm5"
 quotient_definition
 "fv_lts :: lts \<Rightarrow> atom set"
 is
-"rfv_lts"
+"fv_rlts"
 quotient_definition
 "bv5 :: lts \<Rightarrow> atom set"
 is
 "rbv5"
 lemma rbv5_eqvt:
 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
 sorry
-lemma rfv_trm5_eqvt:
+lemma fv_rtrm5_eqvt:
-"pi \<bullet> (rfv_trm5 x) = rfv_trm5 (pi \<bullet> x)"
+"pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
 sorry
-lemma rfv_lts_eqvt:
+lemma fv_rlts_eqvt:
-"pi \<bullet> (rfv_lts x) = rfv_lts (pi \<bullet> x)"
+"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 (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(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 rfv_trm5_eqvt)
+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 rfv_lts_eqvt)
+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 rfv_lts_eqvt)
+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> rfv_trm5 t = rfv_trm5 s)"
+"(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
-"(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)"
+"(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:
 apply(induct rule: alpha5_alphalts.inducts(2))
 apply(simp_all)
 done
 lemma [quot_respect]:
-"(alphalts ===> op =) rfv_lts rfv_lts"
+"(alphalts ===> op =) fv_rlts fv_rlts"
-"(alpha5 ===> op =) rfv_trm5 rfv_trm5"
+"(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"
 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]
+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)
 where
 "rbv6 (rVr6 n) = {}"
 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
-primrec
+local_setup {* define_raw_fv "Terms.rtrm6" [
-rfv_trm6
+[[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}
-where
+print_theorems
-"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"
 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 rfv_trm6 pi ({atom b}, s))) \<Longrightarrow> rLm6 a t \<approx>6 rLm6 b s"
+| 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 rfv_trm6 pi ((rbv6 t2), s2))) \<Longrightarrow> rLt6 t1 s1 \<approx>6 rLt6 t2 s2"
+| 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
 "rLt6"
 quotient_definition
 "fv_trm6 :: trm6 \<Rightarrow> atom set"
 is
-"rfv_trm6"
+"fv_rtrm6"
 quotient_definition
 "bv6 :: trm6 \<Rightarrow> atom set"
 is
 "rbv6"
 apply (simp add: alpha_gen fresh_star_def)
 apply (rule a1)
 apply (rule refl)
 done
-lemma [quot_respect]:"(alpha6 ===> op =) rfv_trm6 rfv_trm6"
+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)
 where
 "rbv7 (rVr7 n) = {atom n}"
 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
-primrec
+local_setup {* define_raw_fv "Terms.rtrm7" [
-rfv_trm7
+[[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}
-where
+print_theorems
-"rfv_trm7 (rVr7 n) = {atom n}"
-| "rfv_trm7 (rLm7 n t) = (rfv_trm7 t) - {atom n}"
-| "rfv_trm7 (rLt7 l r) = (rfv_trm7 l) \<union> (rfv_trm7 r - rbv7 l)"
 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 rfv_trm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
+| 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 rfv_trm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
+| 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 = rfv_trm7 x"
+lemma bvfv7: "rbv7 x = fv_rtrm7 x"
 apply induct
 apply simp_all
 done
 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
 rbv8
 where
 "rbv8 (Bar0 x) = {}"
 | "rbv8 (Bar1 v x b) = {atom v}"
-primrec
+local_setup {* define_raw_fv "Terms.rfoo8" [
-rfv_foo8 and rfv_bar8
+[[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
-where
+print_theorems
-"rfv_foo8 (Foo0 x) = {atom x}"
-| "rfv_foo8 (Foo1 b t) = (rfv_foo8 t - rbv8 b) \<union> (rfv_bar8 b)"
-| "rfv_bar8 (Bar0 x) = {atom x}"
-| "rfv_bar8 (Bar1 v x t) = {atom v} \<union> (rfv_bar8 t - {atom x})"
-print_theorems
 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}
 print_theorems
 inductive
 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 rfv_foo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
+| 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 rfv_bar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 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 rfv_bar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> rfv_bar8 x = rfv_bar8 y"
+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 =) rfv_bar8 rfv_bar8"
+lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8"
-apply simp apply clarify apply (simp add: rfv_bar8_rsp_hlp)
+apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp)
 done
-lemma "(alpha8f ===> op =) rfv_foo8 rfv_foo8"
+lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8"
 apply simp apply clarify
 apply (erule alpha8f_alpha8b.inducts(1))
-apply (simp_all add: alpha_gen rfv_bar8_rsp_hlp)
+apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
 done
 rbv9
 where
 "rbv9 (Var9 x) = {}"
 | "rbv9 (Lam9 x b) = {atom x}"
-primrec
+local_setup {* define_raw_fv "Terms.rlam9" [
-rfv_lam9 and rfv_bla9
+[[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *}
-where
+print_theorems
-"rfv_lam9 (Var9 x) = {atom x}"
-| "rfv_lam9 (Lam9 b t) = (rfv_lam9 t - {atom b})"
-| "rfv_bla9 (Bla9 l r) = (rfv_lam9 r - rbv9 l) \<union> rfv_lam9 l"
 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 rfv_lam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2"
+| 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 rfv_lam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>9b Bla9 b2 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
 "Bla9"
 quotient_definition
 "fv_lam9 :: lam9 \<Rightarrow> atom set"
 is
-"rfv_lam9"
+"fv_rlam9"
 quotient_definition
 "fv_bla9 :: bla9 \<Rightarrow> atom set"
 is
-"rfv_bla9"
+"fv_rbla9"
 quotient_definition
 "bv9 :: lam9 \<Rightarrow> atom set"
 is
 "rbv9"
 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
-rfv_ty
+fv_tyS
-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)"
+"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 =) rfv_ty pi (atoms xs2, T2))
+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)

changeset 1180	3f36936f1280
parent 1179	789fbba5c23f
child 1181	788a59d2d7aa