# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1291017669 0
# Node ID 35c570891a3a107ee913edcaee3dad4a2392d6e6
# Parent  98dc38c250bbbc3e77b964e9dfe390915dc991d1
isarfied some of the high-level proofs

diff -r 98dc38c250bb -r 35c570891a3a Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Mon Nov 29 05:17:41 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Mon Nov 29 08:01:09 2010 +0000
@@ -100,51 +100,47 @@
 apply(simp add: mem_permute_iff)
 done
 
-lemma yy1:
-  assumes "(p \<bullet> bs) \<sharp>* bs" "finite bs"
-  shows "p \<bullet> bs \<inter> bs = {}"
-using assms
-apply(auto simp add: fresh_star_def)
-apply(simp add: fresh_def supp_finite_atom_set)
-done
-
-lemma abs_rename_set:
+lemma Abs_rename_set:
   fixes x::"'a::fs"
-  assumes "(p \<bullet> bs) \<sharp>* x" "(p \<bullet> bs) \<sharp>* bs" "finite bs"
+  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  and     b: "finite bs"
   shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y"
-using yy assms
-apply -
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bs" in meta_spec)
-apply(auto simp add: yy1)
-apply(rule_tac x="q \<bullet> x" in exI)
-apply(subgoal_tac "(q \<bullet> ([bs]set. x)) = [bs]set. x")
-apply(simp)
-apply(rule supp_perm_eq)
-apply(rule fresh_star_supp_conv)
-apply(simp add: fresh_star_def)
-apply(simp add: Abs_fresh_iff)
-apply(auto)
-done
+proof -
+  from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)   
+  with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+  have "[bs]set. x =  q \<bullet> ([bs]set. x)"
+    apply(rule perm_supp_eq[symmetric])
+    using a **
+    unfolding fresh_star_Pair
+    unfolding Abs_fresh_star_iff
+    unfolding fresh_star_def
+    by auto
+  also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp
+  also have "\<dots> = [p \<bullet> bs]set. (q \<bullet> x)" using * by simp
+  finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" .
+  then show "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" by blast
+qed
 
-lemma abs_rename_res:
+lemma Abs_rename_res:
   fixes x::"'a::fs"
-  assumes "(p \<bullet> bs) \<sharp>* x" "(p \<bullet> bs) \<sharp>* bs" "finite bs"
+  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  and     b: "finite bs"
   shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y"
-using yy assms
-apply -
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="bs" in meta_spec)
-apply(auto simp add: yy1)
-apply(rule_tac x="q \<bullet> x" in exI)
-apply(subgoal_tac "(q \<bullet> ([bs]res. x)) = [bs]res. x")
-apply(simp)
-apply(rule supp_perm_eq)
-apply(rule fresh_star_supp_conv)
-apply(simp add: fresh_star_def)
-apply(simp add: Abs_fresh_iff)
-apply(auto)
-done
+proof -
+  from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) 
+  with yy obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+  have "[bs]res. x =  q \<bullet> ([bs]res. x)"
+    apply(rule perm_supp_eq[symmetric])
+    using a **
+    unfolding fresh_star_Pair
+    unfolding Abs_fresh_star_iff
+    unfolding fresh_star_def
+    by auto
+  also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp
+  also have "\<dots> = [p \<bullet> bs]res. (q \<bullet> x)" using * by simp
+  finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" .
+  then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast
+qed
 
 lemma zz0:
   assumes "p \<bullet> bs = q \<bullet> bs"
@@ -155,7 +151,7 @@
 
 lemma zz:
   fixes bs::"atom list"
-  assumes "set bs \<inter> (p \<bullet> (set bs)) = {}"
+  assumes "(p \<bullet> (set bs)) \<inter> (set bs) = {}"
   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"
 using assms
 apply(induct bs)
@@ -195,39 +191,26 @@
 apply(auto simp add: fresh_def supp_of_atom_list)[1]
 done
 
-lemma zz1:
-  assumes "(p \<bullet> (set bs)) \<sharp>* bs" 
-  shows "(set bs) \<inter> (p \<bullet> (set bs)) = {}"
-using assms
-apply(auto simp add: fresh_star_def)
-apply(simp add: fresh_def supp_of_atom_list)
-done
-
-lemma abs_rename_list:
+lemma Abs_rename_list:
   fixes x::"'a::fs"
-  assumes "(p \<bullet> (set bs)) \<sharp>* x" "(p \<bullet> (set bs)) \<sharp>* bs" 
+  assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
   shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"
-using zz assms
-apply -
-apply(drule_tac x="bs" in meta_spec)
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac zz1)
-apply(auto)
-apply(rule_tac x="q \<bullet> x" in exI)
-apply(subgoal_tac "(q \<bullet> ([bs]lst. x)) = [bs]lst. x")
-apply(simp)
-apply(rule supp_perm_eq)
-apply(rule fresh_star_supp_conv)
-apply(simp add: fresh_star_def)
-apply(simp add: Abs_fresh_iff)
-apply(auto)
-done
-
-lemma fresh_star_list:
-  shows "as \<sharp>* (xs @ ys) \<longleftrightarrow> as \<sharp>* xs \<and> as \<sharp>* ys"
-  and   "as \<sharp>* (x # xs) \<longleftrightarrow> as \<sharp>* x \<and> as \<sharp>* xs"
-  and   "as \<sharp>* []"
-by (auto simp add: fresh_star_def fresh_Nil fresh_Cons fresh_append)
+proof -
+  from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter 
+    by (simp add: fresh_star_Pair fresh_star_set)
+  with zz obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis 
+  have "[bs]lst. x =  q \<bullet> ([bs]lst. x)"
+    apply(rule perm_supp_eq[symmetric])
+    using a **
+    unfolding fresh_star_Pair
+    unfolding Abs_fresh_star_iff
+    unfolding fresh_star_def
+    by auto
+  also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp
+  also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp
+  finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" .
+  then show "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" by blast
+qed
 
 
 lemma test6:
@@ -248,15 +231,13 @@
 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)")
 apply(erule exE)
 apply(rule assms(3))
-apply(insert abs_rename_list)[1]
+apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="[atom name]" in meta_spec)
 apply(drule_tac x="trm" in meta_spec)
-apply(simp only: fresh_star_prod set.simps)
+apply(simp only: fresh_star_Pair set.simps)
 apply(drule meta_mp)
-apply(rule TrueI)
-apply(drule meta_mp)
-apply(rule TrueI)
+apply(simp)
 apply(erule exE)
 apply(rule exI)+
 apply(perm_simp)
@@ -272,27 +253,23 @@
 apply(rule assms(4))
 apply(simp only:)
 apply(simp only: foo.eq_iff)
-apply(insert abs_rename_list)[1]
+apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="bn assg1" in meta_spec)
 apply(drule_tac x="trm1" in meta_spec)
-apply(insert abs_rename_list)[1]
+apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="bn assg2" in meta_spec)
 apply(drule_tac x="trm2" in meta_spec)
 apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
-apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
+apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)
 apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
-apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
+apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)
 apply(erule exE)+
 apply(rule exI)+
 apply(perm_simp add: tt1)
 apply(rule conjI)
-apply(simp add: fresh_star_prod fresh_star_union)
+apply(simp add: fresh_star_Pair fresh_star_Un)
 apply(erule conjE)+
 apply(rule conjI)
 apply(assumption)
@@ -313,22 +290,26 @@
 apply(rule assms(5))
 apply(simp only:)
 apply(simp only: foo.eq_iff)
-apply(insert abs_rename_list)[1]
+apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="[atom name1] @ [atom name2]" in meta_spec)
 apply(drule_tac x="trm1" in meta_spec)
-apply(insert abs_rename_list)[1]
+apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="[atom name2]" in meta_spec)
 apply(drule_tac x="trm2" in meta_spec)
 apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps set_append fresh_star_union, simp)
-apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union)
+apply(simp only: union_eqvt fresh_star_Pair fresh_star_list fresh_star_Un, simp)
+apply(auto)[1]
+apply(perm_simp)
+apply(auto simp add: fresh_star_def)[1]
+apply(perm_simp)
+apply(auto simp add: fresh_star_def)[1]
+apply(perm_simp)
+apply(auto simp add: fresh_star_def)[1]
 apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union set_append fresh_star_list, simp)
-apply(drule meta_mp)
-apply(simp only: union_eqvt fresh_star_prod set.simps fresh_star_union set_append fresh_star_list, simp)
+apply(perm_simp)
+apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1]
 apply(erule exE)+
 apply(rule exI)+
 apply(perm_simp add: tt1)
@@ -337,15 +318,13 @@
 apply(rule conjI)
 apply(assumption)
 apply(assumption)
-apply(simp add: fresh_star_prod)
+apply(simp add: fresh_star_Pair)
 apply(simp add: fresh_star_def)
 apply(rule at_set_avoiding1)
 apply(simp)
 apply(simp add: finite_supp)
 done
 
-
-
 lemma test5:
   fixes c::"'a::fs"
   assumes "\<And>name. y = Var name \<Longrightarrow> P" 
diff -r 98dc38c250bb -r 35c570891a3a Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Mon Nov 29 05:17:41 2010 +0000
+++ b/Nominal/Nominal2_Abs.thy	Mon Nov 29 08:01:09 2010 +0000
@@ -523,6 +523,14 @@
   unfolding supp_Abs
   by auto
 
+lemma Abs_fresh_star_iff:
+  fixes x::"'a::fs"
+  shows "as \<sharp>* Abs_set bs x \<longleftrightarrow> (as - bs) \<sharp>* x"
+  and   "as \<sharp>* Abs_res bs x \<longleftrightarrow> (as - bs) \<sharp>* x"
+  and   "as \<sharp>* Abs_lst cs x \<longleftrightarrow> (as - set cs) \<sharp>* x"
+  unfolding fresh_star_def
+  by (auto simp add: Abs_fresh_iff)
+
 lemma Abs_fresh_star:
   fixes x::"'a::fs"
   shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x"
diff -r 98dc38c250bb -r 35c570891a3a Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Nov 29 05:17:41 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Nov 29 08:01:09 2010 +0000
@@ -952,7 +952,6 @@
 
 section {* Support for finite sets of atoms *}
 
-
 lemma supp_finite_atom_set:
   fixes S::"atom set"
   assumes "finite S"
@@ -1159,6 +1158,10 @@
   shows "supp (x # xs) = supp x \<union> supp xs"
 by (simp add: supp_def Collect_imp_eq Collect_neg_eq)
 
+lemma supp_append:
+  shows "supp (xs @ ys) = supp xs \<union> supp ys"
+  by (induct xs) (auto simp add: supp_Nil supp_Cons)
+
 lemma fresh_Nil: 
   shows "a \<sharp> []"
   by (simp add: fresh_def supp_Nil)
@@ -1167,6 +1170,11 @@
   shows "a \<sharp> (x # xs) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> xs"
   by (simp add: fresh_def supp_Cons)
 
+lemma fresh_append:
+  shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
+  by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
+
+
 instance list :: (fs) fs
 apply default
 apply (induct_tac x)
@@ -1312,6 +1320,29 @@
   using fin unfolding fresh_def
   by (simp add: supp_of_finite_insert)
 
+lemma supp_set_empty:
+  shows "supp {} = {}"
+  unfolding supp_def
+  by (simp add: empty_eqvt)
+
+lemma fresh_set_empty:
+  shows "a \<sharp> {}"
+  by (simp add: fresh_def supp_set_empty)
+
+lemma supp_set:
+  fixes xs :: "('a::fs) list"
+  shows "supp (set xs) = supp xs"
+apply(induct xs)
+apply(simp add: supp_set_empty supp_Nil)
+apply(simp add: supp_Cons supp_of_finite_insert)
+done
+
+lemma fresh_set:
+  fixes xs :: "('a::fs) list"
+  shows "a \<sharp> (set xs) \<longleftrightarrow> a \<sharp> xs"
+unfolding fresh_def
+by (simp add: supp_set)
+
 
 subsection {* Type @{typ "'a fset"} is finitely supported *}
 
@@ -1364,12 +1395,23 @@
   shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x"
 by (auto simp add: fresh_star_def fresh_def)
 
-lemma fresh_star_prod:
-  fixes as::"atom set"
+lemma fresh_star_Pair:
   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
   by (auto simp add: fresh_star_def fresh_Pair)
 
-lemma fresh_star_union:
+lemma fresh_star_list:
+  shows "as \<sharp>* (xs @ ys) \<longleftrightarrow> as \<sharp>* xs \<and> as \<sharp>* ys"
+  and   "as \<sharp>* (x # xs) \<longleftrightarrow> as \<sharp>* x \<and> as \<sharp>* xs"
+  and   "as \<sharp>* []"
+by (auto simp add: fresh_star_def fresh_Nil fresh_Cons fresh_append)
+
+lemma fresh_star_set:
+  fixes xs::"('a::fs) list"
+  shows "as \<sharp>* set xs \<longleftrightarrow> as \<sharp>* xs"
+unfolding fresh_star_def
+by (simp add: fresh_set)
+
+lemma fresh_star_Un:
   shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
   by (auto simp add: fresh_star_def)
 
@@ -1398,9 +1440,9 @@
   shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"
   by (simp add: fresh_star_def fresh_Unit) 
 
-lemma fresh_star_prod_elim: 
+lemma fresh_star_Pair_elim: 
   shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"
-  by (rule, simp_all add: fresh_star_prod)
+  by (rule, simp_all add: fresh_star_Pair)
 
 lemma fresh_star_zero:
   shows "as \<sharp>* (0::perm)"
@@ -1427,6 +1469,15 @@
 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
 done
 
+lemma at_fresh_star_inter:
+  assumes a: "(p \<bullet> bs) \<sharp>* bs" 
+  and     b: "finite bs"
+  shows "p \<bullet> bs \<inter> bs = {}"
+using a b
+unfolding fresh_star_def
+unfolding fresh_def
+by (auto simp add: supp_finite_atom_set)
+
 
 section {* Induction principle for permutations *}
 
@@ -1525,6 +1576,12 @@
   qed
 qed
 
+lemma perm_supp_eq:
+  assumes a: "(supp p) \<sharp>* x"
+  shows "p \<bullet> x = x"
+by (rule supp_perm_eq)
+   (simp add: fresh_star_supp_conv a)
+
 
 section {* Avoiding of atom sets *}
 
@@ -1607,7 +1664,7 @@
 apply(erule_tac c="(c, x)" in at_set_avoiding)
 apply(simp add: supp_Pair)
 apply(rule_tac x="p" in exI)
-apply(simp add: fresh_star_prod)
+apply(simp add: fresh_star_Pair)
 apply(rule fresh_star_supp_conv)
 apply(auto simp add: fresh_star_def)
 done
@@ -1621,7 +1678,7 @@
 apply(erule_tac c="(c, x)" in at_set_avoiding)
 apply(simp add: supp_Pair)
 apply(rule_tac x="p" in exI)
-apply(simp add: fresh_star_prod)
+apply(simp add: fresh_star_Pair)
 apply(rule fresh_star_supp_conv)
 apply(auto simp add: fresh_star_def)
 done
diff -r 98dc38c250bb -r 35c570891a3a Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Mon Nov 29 05:17:41 2010 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Mon Nov 29 08:01:09 2010 +0000
@@ -155,15 +155,6 @@
   unfolding Ball_def
   by (perm_simp) (rule refl)
 
-lemma supp_set_empty:
-  shows "supp {} = {}"
-  unfolding supp_def
-  by (simp add: empty_eqvt)
-
-lemma fresh_set_empty:
-  shows "a \<sharp> {}"
-  by (simp add: fresh_def supp_set_empty)
-
 lemma UNIV_eqvt[eqvt]:
   shows "p \<bullet> UNIV = UNIV"
   unfolding UNIV_def
@@ -216,14 +207,6 @@
   shows "p \<bullet> finite A = finite (p \<bullet> A)"
   unfolding finite_permute_iff permute_bool_def ..
 
-lemma supp_set:
-  fixes xs :: "('a::fs) list"
-  shows "supp (set xs) = supp xs"
-apply(induct xs)
-apply(simp add: supp_set_empty supp_Nil)
-apply(simp add: supp_Cons supp_of_finite_insert)
-done
-
 
 section {* List Operations *}
 
@@ -231,14 +214,6 @@
   shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
   by (induct xs) auto
 
-lemma supp_append:
-  shows "supp (xs @ ys) = supp xs \<union> supp ys"
-  by (induct xs) (auto simp add: supp_Nil supp_Cons)
-
-lemma fresh_append:
-  shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
-  by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
-
 lemma rev_eqvt[eqvt]:
   shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
   by (induct xs) (simp_all add: append_eqvt)