diff -r b53e98bfb298 -r b96e8cf86891 Nominal/Nominal2_FSet.thy --- a/Nominal/Nominal2_FSet.thy Fri Apr 30 15:34:26 2010 +0100 +++ b/Nominal/Nominal2_FSet.thy Fri Apr 30 15:36:02 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 \ {||}) = ({||} :: 'a::pt fset)" - "p \ finsert (x :: 'a :: pt) xs = finsert (p \ x) (p \ xs)" +lemma permute_fset[simp, eqvt]: + fixes S::"('a::pt) fset" + shows "(p \ {||}) = ({||} ::('a::pt) fset)" + and "p \ finsert x S = finsert (p \ x) (p \ S)" by (lifting permute_list.simps) lemma fmap_eqvt[eqvt]: - shows "p \ (fmap f l) = fmap (p \ f) (p \ l)" + shows "p \ (fmap f S) = fmap (p \ f) (p \ S)" by (lifting map_eqvt) lemma fset_to_set_eqvt[eqvt]: - shows "p \ (fset_to_set x) = fset_to_set (p \ x)" + shows "p \ (fset_to_set S) = fset_to_set (p \ 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 \ 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 \ 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 \ 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 \ 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