# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1290798203 0
# Node ID 1eac050a36f4bd539d50d9a68eb6720a96256bc3
# Parent  cb16f22bc660ad007065a4f9cda217650e9a40d6
completely different method fro deriving the exhaust lemma

diff -r cb16f22bc660 -r 1eac050a36f4 Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Fri Nov 26 10:53:55 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Fri Nov 26 19:03:23 2010 +0000
@@ -293,6 +293,100 @@
 done
 
 
+text {*
+  tests by cu
+*}
+
+
+lemma test3:
+  fixes c::"'a::fs"
+  assumes a: "y = Let2 x1 x2 trm1 trm2"
+  and b: "\<forall>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<longrightarrow> P"
+  shows "P"
+using b[simplified a]
+apply -
+apply(subgoal_tac "\<exists>q::perm. (q \<bullet> {atom x1, atom x2}) \<sharp>* (c, x1, x2, trm1, trm2)")
+apply(erule exE)
+apply(drule_tac p="- q" in permute_boolI)
+apply(perm_simp)
+apply(simp only: foo.eq_iff)
+apply(drule_tac x="x1" in spec)
+apply(drule_tac x="x2" in spec)
+apply(simp)
+apply(drule mp)
+apply(rule conjI)
+defer
+apply(rule_tac p="q" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel)
+apply(rule conjI)
+prefer 2
+apply(rule_tac x="(atom x2 \<rightleftharpoons> atom (q \<bullet> x2)) \<bullet> trm2" in exI)
+apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"])
+apply(simp)
+apply(simp add: fresh_star_def)
+apply(simp add: fresh_def supp_Pair)
+apply(simp)
+apply(case_tac "x1=x2")
+apply(simp)
+apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"])
+apply(simp)
+apply(simp add: fresh_star_def)
+apply(simp add: fresh_def supp_Pair)
+apply(simp)
+apply(rule exI)
+apply(rule refl)
+apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"])
+apply(simp)
+apply(simp add: fresh_star_def)
+apply(simp add: fresh_def supp_Pair)
+apply(simp)
+apply(simp add: flip_def[symmetric] atom_eqvt)
+apply(subgoal_tac "q \<bullet> x2 \<noteq> x1")
+apply(simp)
+apply(subst Abs_swap2[where a="atom x1" and b="atom (q \<bullet> x1)"])
+apply(simp)
+apply(subgoal_tac " atom (q \<bullet> x1) \<notin> supp ((x2 \<leftrightarrow> q \<bullet> x2) \<bullet> trm1)")
+apply(simp add: fresh_star_def)
+apply(simp add: fresh_star_def)
+apply(simp add: fresh_def supp_Pair)
+apply(erule conjE)+
+apply(rule_tac p="(x2 \<leftrightarrow> q \<bullet> x2)" in permute_boolE)
+apply(simp add: mem_eqvt Not_eqvt atom_eqvt supp_eqvt)
+apply(subgoal_tac "q \<bullet> x2 \<noteq> q \<bullet> x1")
+apply(subgoal_tac "x2 \<noteq> q \<bullet> x1")
+apply(simp)
+apply(simp add: supp_at_base)
+apply(simp)
+apply(simp)
+apply(rule exI)
+apply(rule refl)
+apply(simp add: fresh_star_def)
+apply(simp add: fresh_def supp_Pair)
+apply(simp add: supp_at_base)
+apply(simp)
+defer
+apply(rule_tac p="q" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel fresh_star_prod)
+apply(simp)
+apply(rule at_set_avoiding3[where x="()", simplified])
+apply(simp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: fresh_star_def fresh_Unit)
+done
+
+lemma test4:
+  fixes c::"'a::fs"
+  assumes a: "y = Let2 x1 x2 trm1 trm2"
+  and b: "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+apply(rule test3)
+apply(rule a)
+using b
+apply(auto)
+done
+
+
 end
 
 
diff -r cb16f22bc660 -r 1eac050a36f4 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Fri Nov 26 10:53:55 2010 +0000
+++ b/Nominal/Nominal2_Abs.thy	Fri Nov 26 19:03:23 2010 +0000
@@ -525,11 +525,11 @@
 
 lemma Abs_fresh_star:
   fixes x::"'a::fs"
-  shows "as \<sharp>* Abs_set as x"
-  and   "as \<sharp>* Abs_res as x"
-  and   "set bs \<sharp>* Abs_lst bs x"
+  shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x"
+  and   "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_res as' x"
+  and   "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* Abs_lst bs' x"
   unfolding fresh_star_def
-  by(simp_all add: Abs_fresh_iff)
+  by(auto simp add: Abs_fresh_iff)
 
 
 section {* Infrastructure for building tuples of relations and functions *}