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