# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272701746 -3600
# Node ID 7ee9a2fefc77435c640fabbdd735506c88a108e5
# Parent  2ceec1b4b015c333659b7f82bfc4e51fc251c2bb# Parent  7c8242a02f3912165d96079018211445305f6f77
merged

diff -r 7c8242a02f39 -r 7ee9a2fefc77 Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Fri Apr 30 15:45:39 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Sat May 01 09:15:46 2010 +0100
@@ -1067,10 +1067,17 @@
   unfolding fresh_def supp_def 
   unfolding MOST_iff_cofinite by simp
 
+lemma supp_subset_fresh:
+  assumes a: "\<And>a. a \<sharp> x \<Longrightarrow> a \<sharp> y"
+  shows "supp y \<subseteq> supp x"
+  using a
+  unfolding fresh_def
+  by blast
+
 lemma fresh_fun_app:
   assumes "a \<sharp> f" and "a \<sharp> x" 
   shows "a \<sharp> f x"
-  using assms 
+  using assms
   unfolding fresh_conv_MOST
   unfolding permute_fun_app_eq 
   by (elim MOST_rev_mp, simp)
@@ -1081,22 +1088,22 @@
   unfolding fresh_def
   by auto
 
+text {* support of equivariant functions *}
+
 lemma supp_fun_eqvt:
-  assumes a: "\<forall>p. p \<bullet> f = f"
+  assumes a: "\<And>p. p \<bullet> f = f"
   shows "supp f = {}"
   unfolding supp_def 
   using a by simp
 
-
 lemma fresh_fun_eqvt_app:
-  assumes a: "\<forall>p. p \<bullet> f = f"
+  assumes a: "\<And>p. p \<bullet> f = f"
   shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
 proof -
   from a have "supp f = {}" by (simp add: supp_fun_eqvt)
   then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
     unfolding fresh_def
-    using supp_fun_app 
-    by auto
+    using supp_fun_app by auto
 qed
 
 
diff -r 7c8242a02f39 -r 7ee9a2fefc77 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 30 15:45:39 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sat May 01 09:15:46 2010 +0100
@@ -156,6 +156,16 @@
   shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
   by (perm_simp add: permute_minus_cancel) (rule refl)
 
+lemma Bex_eqvt[eqvt]:
+  shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+  unfolding Bex_def
+  by (perm_simp) (rule refl)
+
+lemma Ball_eqvt[eqvt]:
+  shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+  unfolding Ball_def
+  by (perm_simp) (rule refl)
+
 lemma empty_eqvt[eqvt]:
   shows "p \<bullet> {} = {}"
   unfolding empty_def
@@ -206,6 +216,11 @@
   unfolding vimage_def
   by (perm_simp) (rule refl)
 
+lemma Union_eqvt[eqvt]:
+  shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
+  unfolding Union_eq 
+  by (perm_simp) (rule refl)
+
 lemma finite_permute_iff:
   shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
   unfolding permute_set_eq_vimage
diff -r 7c8242a02f39 -r 7ee9a2fefc77 Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Fri Apr 30 15:45:39 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Sat May 01 09:15:46 2010 +0100
@@ -467,4 +467,85 @@
   qed
 qed
 
+
+section {* Support of Finite Sets of Finitely Supported Elements *}
+
+lemma Union_fresh:
+  shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
+  unfolding Union_image_eq[symmetric]
+  apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)
+  apply(perm_simp)
+  apply(rule refl)
+  apply(assumption)
+  done
+
+lemma Union_supports_set:
+  shows "(\<Union>x \<in> S. supp x) supports S"
+  apply(simp add: supports_def fresh_def[symmetric])
+  apply(rule allI)+
+  apply(rule impI)
+  apply(erule conjE)
+  apply(simp add: permute_set_eq)
+  apply(auto)
+  apply(subgoal_tac "(a \<rightleftharpoons> b) \<bullet> xa = xa")(*A*)
+  apply(simp)
+  apply(rule swap_fresh_fresh)
+  apply(force)
+  apply(force)
+  apply(rule_tac x="x" in exI)
+  apply(simp)
+  apply(rule sym)
+  apply(rule swap_fresh_fresh)
+  apply(auto)
+  done
+
+lemma Union_of_fin_supp_sets:
+  fixes S::"('a::fs set)"
+  assumes fin: "finite S"   
+  shows "finite (\<Union>x\<in>S. supp x)"
+  using fin by (induct) (auto simp add: finite_supp)
+
+lemma Union_included_in_supp:
+  fixes S::"('a::fs set)"
+  assumes fin: "finite S"
+  shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
+proof -
+  have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
+    apply(rule supp_finite_atom_set[symmetric])
+    apply(rule Union_of_fin_supp_sets)
+    apply(rule fin)
+    done
+  also have "\<dots> \<subseteq> supp S"
+    apply(rule supp_subset_fresh)
+    apply(simp add: Union_fresh)
+    done
+  finally show ?thesis .
+qed
+
+lemma supp_of_fin_sets:
+  fixes S::"('a::fs set)"
+  assumes fin: "finite S"
+  shows "(supp S) = (\<Union>x\<in>S. supp x)"
+apply(rule subset_antisym)
+apply(rule supp_is_subset)
+apply(rule Union_supports_set)
+apply(rule Union_of_fin_supp_sets[OF fin])
+apply(rule Union_included_in_supp[OF fin])
+done
+
+lemma supp_of_fin_union:
+  fixes S T::"('a::fs) set"
+  assumes fin1: "finite S"
+  and     fin2: "finite T"
+  shows "supp (S \<union> T) = supp S \<union> supp T"
+  using fin1 fin2
+  by (simp add: supp_of_fin_sets)
+
+lemma supp_of_fin_insert:
+  fixes S::"('a::fs) set"
+  assumes fin:  "finite S"
+  shows "supp (insert x S) = supp x \<union> supp S"
+  using fin
+  by (simp add: supp_of_fin_sets)
+
 end
diff -r 7c8242a02f39 -r 7ee9a2fefc77 Nominal/NewParser.thy
diff -r 7c8242a02f39 -r 7ee9a2fefc77 Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Fri Apr 30 15:45:39 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Sat May 01 09:15:46 2010 +0100
@@ -15,7 +15,7 @@
   apply simp
   done
 
-instantiation FSet.fset :: (pt) pt
+instantiation fset :: (pt) pt
 begin
 
 quotient_definition
@@ -34,70 +34,64 @@
 
 end
 
-lemma permute_fset[eqvt]:
-  "(p \<bullet> {||}) = ({||} :: 'a::pt fset)"
-  "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
+lemma permute_fset[simp, eqvt]:
+  fixes S::"('a::pt) fset"
+  shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
+  and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"
   by (lifting permute_list.simps)
 
 lemma fmap_eqvt[eqvt]: 
-  shows "p \<bullet> (fmap f l) = fmap (p \<bullet> f) (p \<bullet> l)"
+  shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
 
 lemma fset_to_set_eqvt[eqvt]: 
-  shows "p \<bullet> (fset_to_set x) = fset_to_set (p \<bullet> x)"
+  shows "p \<bullet> (fset_to_set S) = fset_to_set (p \<bullet> S)"
   by (lifting set_eqvt)
 
-lemma fin_fset_to_set:
-  shows "finite (fset_to_set x)"
-  by (induct x) (simp_all)
+lemma fin_fset_to_set[simp]:
+  shows "finite (fset_to_set S)"
+  by (induct S) (simp_all)
 
 lemma supp_fset_to_set:
-  "supp (fset_to_set x) = supp x"
+  shows "supp (fset_to_set S) = supp S"
   apply (simp add: supp_def)
   apply (simp add: eqvts)
   apply (simp add: fset_cong)
   done
 
+lemma supp_finsert:
+  fixes x::"'a::fs"
+  shows "supp (finsert x S) = supp x \<union> supp S"
+  apply(subst supp_fset_to_set[symmetric])
+  apply(simp add: supp_fset_to_set)
+  apply(simp add: supp_of_fin_insert)
+  apply(simp add: supp_fset_to_set)
+  done
+
+lemma supp_fempty:
+  shows "supp {||} = {}"
+  unfolding supp_def
+  by simp
+
+instance fset :: (fs) fs
+  apply (default)
+  apply (induct_tac x rule: fset_induct)
+  apply (simp add: supp_fempty)
+  apply (simp add: supp_finsert)
+  apply (simp add: finite_supp)
+  done
+
 lemma atom_fmap_cong:
-  shows "(fmap atom x = fmap atom y) = (x = y)"
+  shows "fmap atom x = fmap atom y \<longleftrightarrow> x = y"
   apply(rule inj_fmap_eq_iff)
   apply(simp add: inj_on_def)
   done
 
 lemma supp_fmap_atom:
-  shows "supp (fmap atom x) = supp x"
+  shows "supp (fmap atom S) = supp S"
   unfolding supp_def
-  apply (perm_simp)
-  apply (simp add: atom_fmap_cong)
-  done
-
-lemma supp_atom_finsert:
-  "supp (finsert (x :: atom) S) = supp x \<union> supp S"
-  apply (subst supp_fset_to_set[symmetric])
-  apply (simp add: supp_finite_atom_set)
-  apply (simp add: supp_atom_insert[OF fin_fset_to_set])
-  apply (simp add: supp_fset_to_set)
-  done
-
-lemma supp_at_finsert:
-  fixes a::"'a::at_base"
-  shows "supp (finsert a S) = supp a \<union> supp S"
-  apply (subst supp_fset_to_set[symmetric])
-  apply (simp add: supp_finite_atom_set)
-  apply (simp add: supp_at_base_insert[OF fin_fset_to_set])
-  apply (simp add: supp_fset_to_set)
-  done
-
-lemma supp_fempty:
-  "supp {||} = {}"
-  by (simp add: supp_def eqvts)
-
-instance fset :: (at_base) fs
-  apply (default)
-  apply (induct_tac x rule: fset_induct)
-  apply (simp add: supp_fempty)
-  apply (simp add: supp_at_finsert)
-  apply (simp add: supp_at_base)
+  apply(perm_simp)
+  apply(simp add: atom_fmap_cong)
   done
 
 lemma supp_at_fset:
@@ -105,8 +99,9 @@
   shows "supp S = fset_to_set (fmap atom S)"
   apply (induct S)
   apply (simp add: supp_fempty)
-  apply (simp add: supp_at_finsert)
+  apply (simp add: supp_finsert)
   apply (simp add: supp_at_base)
   done
 
+
 end
diff -r 7c8242a02f39 -r 7ee9a2fefc77 Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Fri Apr 30 15:45:39 2010 +0200
+++ b/Pearl-jv/Paper.thy	Sat May 01 09:15:46 2010 +0100
@@ -30,7 +30,7 @@
 *)
 
 (* sort is used in Lists for sorting *)
-hide const sort
+hide_const sort
 
 abbreviation
   "sort \<equiv> sort_of"
diff -r 7c8242a02f39 -r 7ee9a2fefc77 Pearl/Paper.thy
--- a/Pearl/Paper.thy	Fri Apr 30 15:45:39 2010 +0200
+++ b/Pearl/Paper.thy	Sat May 01 09:15:46 2010 +0100
@@ -30,7 +30,7 @@
 *)
 
 (* sort is used in Lists for sorting *)
-hide const sort
+hide_const sort
 
 abbreviation
   "sort \<equiv> sort_of"