moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
theory Abs_equivimports Absbegin(* below is a construction site for showing that in the single-binder case, the old and new alpha equivalence coincide*)fun alpha1where "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"notation alpha1 ("_ \<approx>abs1 _")fun alpha2where "alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))"notation alpha2 ("_ \<approx>abs2 _")lemma alpha_old_new: assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b" shows "({a}, x) \<approx>abs ({b}, y)"using aapply(simp)apply(erule disjE)apply(simp)apply(rule exI)apply(rule alpha_gen_refl)apply(simp)apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)apply(simp add: alpha_gen)apply(simp add: fresh_def)apply(rule conjI)apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in permute_eq_iff[THEN iffD1])apply(rule trans)apply(simp add: Diff_eqvt supp_eqvt)apply(subst swap_set_not_in)backapply(simp)apply(simp)apply(simp add: permute_set_eq)apply(rule conjI)apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])apply(simp add: permute_self)apply(simp add: Diff_eqvt supp_eqvt)apply(simp add: permute_set_eq)apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")apply(simp add: fresh_star_def fresh_def)apply(blast)apply(simp add: supp_swap)apply(simp add: eqvts)donelemma perm_induct_test: fixes P :: "perm => bool" assumes fin: "finite (supp p)" assumes zero: "P 0" assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" assumes plus: "\<And>p1 p2. \<lbrakk>supp p1 \<inter> supp p2 = {}; P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)" shows "P p"using finapply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct)oopslemma ii: assumes "\<forall>x \<in> A. p \<bullet> x = x" shows "p \<bullet> A = A"using assmsapply(auto)apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_bound inf_Int_eq mem_def mem_permute_iff)apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_apply eqvt_bound eqvt_lambda inf_Int_eq mem_def mem_permute_iff permute_minus_cancel(2) permute_pure)donelemma alpha_abs_Pair: shows "(bs, (x1, x2)) \<approx>gen (\<lambda>(x1,x2) (y1,y2). x1=y1 \<and> x2=y2) (\<lambda>(x,y). supp x \<union> supp y) p (cs, (y1, y2)) \<longleftrightarrow> ((bs, x1) \<approx>gen (op=) supp p (cs, y1) \<and> (bs, x2) \<approx>gen (op=) supp p (cs, y2))" apply(simp add: alpha_gen) apply(simp add: fresh_star_def) apply(simp add: ball_Un Un_Diff) apply(rule iffI) apply(simp) defer apply(simp) apply(rule conjI) apply(clarify) apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) apply(rule sym) apply(rule ii) apply(simp add: fresh_def supp_perm) apply(clarify) apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) apply(simp add: fresh_def supp_perm) apply(rule sym) apply(rule ii) apply(simp) donelemma yy: assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2" shows "S1 = S2"using assmsapply (metis insert_Diff_single insert_absorb)donelemma kk: assumes a: "p \<bullet> x = y" shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"using aapply(auto)apply(rule_tac p="- p" in permute_boolE)apply(simp add: mem_eqvt supp_eqvt)donelemma ww: assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" "sort_of a = sort_of b" shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x"apply(subgoal_tac "(supp x) supports x")apply(simp add: supports_def)using assmsapply -apply(drule_tac x="a" in spec)deferapply(rule supp_supports)apply(auto)apply(rotate_tac 1)apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolI)apply(simp add: mem_eqvt supp_eqvt)donelemma alpha_abs_sym: assumes a: "({a}, x) \<approx>abs ({b}, y)" shows "({b}, y) \<approx>abs ({a}, x)"using aapply(simp)apply(erule exE)apply(rule_tac x="- p" in exI)apply(simp add: alpha_gen)apply(simp add: fresh_star_def fresh_minus_perm)apply (metis permute_minus_cancel(2))donelemma alpha_abs_trans: assumes a: "({a1}, x1) \<approx>abs ({a2}, x2)" assumes b: "({a2}, x2) \<approx>abs ({a3}, x3)" shows "({a1}, x1) \<approx>abs ({a3}, x3)"using a bapply(simp)apply(erule exE)+apply(rule_tac x="pa + p" in exI)apply(simp add: alpha_gen)apply(simp add: fresh_star_def fresh_plus_perm)donelemma alpha_equal: assumes a: "({a}, x) \<approx>abs ({a}, y)" shows "(a, x) \<approx>abs1 (a, y)"using aapply(simp)apply(erule exE)apply(simp add: alpha_gen)apply(erule conjE)+apply(case_tac "a \<notin> supp x")apply(simp)apply(subgoal_tac "supp x \<sharp>* p")apply(drule supp_perm_eq)apply(simp)apply(simp)apply(simp)apply(case_tac "a \<notin> supp y")apply(simp)apply(drule supp_perm_eq)apply(clarify)apply(simp (no_asm_use))apply(simp)apply(simp)apply(drule yy)apply(simp)apply(simp)apply(simp)apply(case_tac "a \<sharp> p")apply(subgoal_tac "supp y \<sharp>* p")apply(drule supp_perm_eq)apply(clarify)apply(simp (no_asm_use))apply(metis)apply(auto simp add: fresh_star_def)[1]apply(frule_tac kk)apply(drule_tac x="a" in bspec)apply(simp)apply(simp add: fresh_def)apply(simp add: supp_perm)apply(subgoal_tac "((p \<bullet> a) \<sharp> p)")apply(simp add: fresh_def supp_perm)apply(simp add: fresh_star_def)donelemma alpha_unequal: assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" "a \<noteq> b" shows "(a, x) \<approx>abs1 (b, y)"using aapply -apply(subgoal_tac "a \<notin> supp x - {a}")apply(subgoal_tac "b \<notin> supp x - {a}")deferapply(simp add: alpha_gen)apply(simp)apply(drule_tac abs_swap1)apply(assumption)apply(simp only: insert_eqvt empty_eqvt swap_atom_simps)apply(simp only: abs_eq_iff)apply(drule alphas_abs_sym)apply(rotate_tac 4)apply(drule_tac alpha_abs_trans)apply(assumption)apply(drule alpha_equal)apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolE)apply(simp add: fresh_eqvt)apply(simp add: fresh_def)donelemma alpha_new_old: assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" shows "(a, x) \<approx>abs1 (b, y)"using aapply(case_tac "a=b")apply(simp only: alpha_equal)apply(drule alpha_unequal)apply(simp)apply(simp)apply(simp)doneend