theory Abs_equiv

imports Abs

begin

(* 

  below is a construction site for showing that in the

  single-binder case, the old and new alpha equivalence 

  coincide

*)

fun

  alpha1

where

  "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

  alpha2

where

  "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 a

apply(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)

back

apply(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)

done

lemma 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 fin

apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct)

oops

lemma ii:

  assumes "\<forall>x \<in> A. p \<bullet> x = x"

  shows "p \<bullet> A = A"

using assms

apply(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)

done

lemma 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)

  done

lemma yy:

  assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"

  shows "S1 = S2"

using assms

apply (metis insert_Diff_single insert_absorb)

done

lemma kk:

  assumes a: "p \<bullet> x = y"

  shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"

using a

apply(auto)

apply(rule_tac p="- p" in permute_boolE)

apply(simp add: mem_eqvt supp_eqvt)

done

lemma 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 assms

apply -

apply(drule_tac x="a" in spec)

defer

apply(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)

done

lemma alpha_abs_sym:

  assumes a: "({a}, x) \<approx>abs ({b}, y)"

  shows "({b}, y) \<approx>abs ({a}, x)"

using a

apply(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))

done

lemma 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 b

apply(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)

done

lemma alpha_equal:

  assumes a: "({a}, x) \<approx>abs ({a}, y)" 

  shows "(a, x) \<approx>abs1 (a, y)"

using a

apply(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)

done

lemma 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 a

apply -

apply(subgoal_tac "a \<notin> supp x - {a}")

apply(subgoal_tac "b \<notin> supp x - {a}")

defer

apply(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)

done

lemma 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 a

apply(case_tac "a=b")

apply(simp only: alpha_equal)

apply(drule alpha_unequal)

apply(simp)

apply(simp)

apply(simp)

done

end