diff -r 92dc6cfa3a95 -r 3772bb3bd7ce Nominal/Abs_equiv.thy
--- a/Nominal/Abs_equiv.thy	Wed Aug 25 22:55:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,244 +0,0 @@
-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