diff -r c9d3dda79fe3 -r d7dc35222afc Nominal/Abs_equiv.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Abs_equiv.thy	Fri Mar 26 16:46:40 2010 +0100
@@ -0,0 +1,244 @@
+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
\ No newline at end of file