# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268316607 -3600
# Node ID d59f851926c5509ba1e22d7c6e474c00cb9af916
# Parent  b452e11e409f5c9e0d6347eed97a7f8441a36e11
finally the proof that new and old alpha agree

diff -r b452e11e409f -r d59f851926c5 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Thu Mar 11 10:22:24 2010 +0100
+++ b/Nominal/Abs.thy	Thu Mar 11 15:10:07 2010 +0100
@@ -592,110 +592,130 @@
 done
 
 lemma ww:
-  assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b"
+  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)
-apply(simp)
-sorry
+defer
+apply(rule supp_supports)
+apply(auto)
+apply(rotate_tac 1)
+apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolE)
+apply(simp add: mem_eqvt supp_eqvt)
+done
 
+lemma zz:
+  assumes "p \<bullet> x \<noteq> p \<bullet> y"
+  shows "x \<noteq> y"
+using assms
+apply(auto)
+done
 
-lemma
-  assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b"
-  shows "(a, x) \<approx>abs1 (b, y)"
+lemma alpha_abs_sym:
+  assumes a: "({a}, x) \<approx>abs ({b}, y)"
+  shows "({b}, y) \<approx>abs ({a}, x)"
 using a
-apply(case_tac "a = b")
+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 "b \<notin> supp x \<and> b \<notin> supp y")
-apply(simp)
-apply(drule tt1)
-apply(clarify)
+apply(case_tac "a \<notin> supp x")
 apply(simp)
-apply(simp)
-apply(erule disjE)
-apply(case_tac "b \<in> supp y")
-apply(drule_tac yy)
+apply(subgoal_tac "supp x \<sharp>* p")
+apply(drule tt1)
 apply(simp)
 apply(simp)
 apply(simp)
-apply(case_tac "b \<sharp> p")
-apply(subgoal_tac "supp y \<sharp>* p")
-apply(drule tt1)
-apply(clarify)
-apply(drule sym)
-apply(drule sym)
-apply(simp)
-apply(auto simp add: fresh_star_def)[1]
-apply(frule_tac kk)
-apply(drule_tac x="b" in bspec)
-apply(simp)
-apply(simp add: fresh_def)
-apply(simp add: supp_perm)
-apply(subgoal_tac "((p \<bullet> b) \<sharp> p)")
-apply(simp add: fresh_def supp_perm)
-apply(simp add: fresh_star_def)
+apply(case_tac "a \<notin> supp y")
 apply(simp)
 apply(drule tt1)
 apply(clarify)
-apply(drule sym)
-apply(drule sym)
+apply(simp (no_asm_use))
 apply(simp)
-apply(case_tac "b \<in> supp x")
-apply(drule_tac yy)
+apply(simp)
+apply(drule yy)
 apply(simp)
 apply(simp)
 apply(simp)
-apply(case_tac "b \<sharp> p")
+apply(case_tac "a \<sharp> p")
 apply(subgoal_tac "supp y \<sharp>* p")
 apply(drule tt1)
 apply(clarify)
-apply(drule sym)
-apply(drule sym)
-apply(simp)
+apply(simp (no_asm_use))
+apply(metis)
 apply(auto simp add: fresh_star_def)[1]
 apply(frule_tac kk)
-apply(drule_tac x="b" in bspec)
+apply(drule_tac x="a" in bspec)
 apply(simp)
 apply(simp add: fresh_def)
 apply(simp add: supp_perm)
-apply(subgoal_tac "((p \<bullet> b) \<sharp> p)")
+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 sym)
-apply(drule sym)
-apply(subgoal_tac "supp x \<sharp>* p")
-apply(drule tt1)
-apply(clarify)
+apply(drule_tac alpha_abs_swap)
+apply(assumption)
+apply(simp only: insert_eqvt empty_eqvt swap_atom_simps)
+apply(drule alpha_abs_sym)
+apply(rotate_tac 4)
+apply(drule_tac alpha_abs_trans)
+apply(assumption)
+apply(drule alpha_equal)
+apply(simp)
+apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolI)
+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)
-apply(erule exE)
-apply(simp add: alpha_gen)
-apply(erule conjE)+
-apply(simp add: fresh_def)
-apply(rule conjI)
-defer
-apply(clarify)
-apply(subgoal_tac "a=b")
-prefer 2
-apply(blast)
-apply(simp)
-apply(clarify)
-apply(subgoal_tac "b \<notin> supp x")
-prefer 2
-apply(blast)
-apply(subgoal_tac "a \<notin> supp (p \<bullet> x)")
-prefer 2
-apply(blast)
-oops
-
+done
 
 fun
   distinct_perms 
diff -r b452e11e409f -r d59f851926c5 Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Thu Mar 11 10:22:24 2010 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Thu Mar 11 15:10:07 2010 +0100
@@ -12,7 +12,6 @@
 
 section {* Logical Operators *}
 
-
 lemma eq_eqvt:
   shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
   unfolding permute_eq_iff permute_bool_def ..
@@ -214,7 +213,6 @@
   "p \<bullet> (snd x) = snd (p \<bullet> x)"
  by (cases x) simp
 
-
 section {* Units *}
 
 lemma supp_unit:
@@ -245,7 +243,7 @@
 
   (* datatypes *)
   permute_prod.simps append_eqvt rev_eqvt set_eqvt
-  fst_eqvt snd_eqvt
+  fst_eqvt snd_eqvt Pair_eqvt
 
   (* sets *)
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt