# HG changeset patch # User Christian Urban # Date 1272436353 -7200 # Node ID fc5ce7f22b7400cce4f6dfb8ede0f5ee1889b156 # Parent 40db835442a03e3502ada233bd3966ebd6bb0f31 use the more general type-class at_base diff -r 40db835442a0 -r fc5ce7f22b74 Nominal-General/Nominal2_Base.thy --- a/Nominal-General/Nominal2_Base.thy Wed Apr 28 08:24:46 2010 +0200 +++ b/Nominal-General/Nominal2_Base.thy Wed Apr 28 08:32:33 2010 +0200 @@ -1188,7 +1188,7 @@ apply(simp add: atom_image_cong) done -lemma supp_finite_at_set: +lemma supp_finite_set_at_base: assumes a: "finite S" shows "supp S = atom ` S" proof - @@ -1199,11 +1199,11 @@ finally show "supp S = atom ` S" by simp qed -lemma supp_at_insert: +lemma supp_at_base_insert: fixes a::"'a::at_base" assumes a: "finite S" shows "supp (insert a S) = supp a \ supp S" - using a by (simp add: supp_finite_at_set supp_at_base) + using a by (simp add: supp_finite_set_at_base supp_at_base) section {* library functions for the nominal infrastructure *} use "nominal_library.ML" diff -r 40db835442a0 -r fc5ce7f22b74 Nominal/Nominal2_FSet.thy --- a/Nominal/Nominal2_FSet.thy Wed Apr 28 08:24:46 2010 +0200 +++ b/Nominal/Nominal2_FSet.thy Wed Apr 28 08:32:33 2010 +0200 @@ -80,11 +80,11 @@ done lemma supp_at_finsert: - fixes S::"('a::at) fset" - shows "supp (finsert x S) = supp x \ supp S" + fixes a::"'a::at_base" + shows "supp (finsert a S) = supp a \ supp S" apply (subst supp_fset_to_set[symmetric]) apply (simp add: supp_finite_atom_set) - apply (simp add: supp_at_insert[OF fin_fset_to_set]) + apply (simp add: supp_at_base_insert[OF fin_fset_to_set]) apply (simp add: supp_fset_to_set) done @@ -92,7 +92,7 @@ "supp {||} = {}" by (simp add: supp_def eqvts) -instance fset :: (at) fs +instance fset :: (at_base) fs apply (default) apply (induct_tac x rule: fset_induct) apply (simp add: supp_fempty) @@ -101,8 +101,9 @@ done lemma supp_at_fset: - "supp (fset :: 'a :: at fset) = fset_to_set (fmap atom fset)" - apply (induct fset) + fixes S::"('a::at_base) fset" + 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_at_base)