# HG changeset patch # User Christian Urban # Date 1271906183 -7200 # Node ID 9eab1dfc14d2fdc1b9b4506565595a9355f1f248 # Parent 2b0cc308fd6abe08571f075e0b65b4cf6faf28c9 moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms diff -r 2b0cc308fd6a -r 9eab1dfc14d2 Nominal-General/Nominal2_Atoms.thy --- a/Nominal-General/Nominal2_Atoms.thy Wed Apr 21 21:52:30 2010 +0200 +++ b/Nominal-General/Nominal2_Atoms.thy Thu Apr 22 05:16:23 2010 +0200 @@ -5,6 +5,7 @@ *) theory Nominal2_Atoms imports Nominal2_Base + Nominal2_Eqvt uses ("nominal_atoms.ML") begin @@ -20,6 +21,8 @@ assumes atom_eq_iff [simp]: "atom a = atom b \ a = b" assumes atom_eqvt: "p \ (atom a) = atom (p \ a)" +declare atom_eqvt[eqvt] + class at = at_base + assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" @@ -75,6 +78,62 @@ thus ?thesis .. qed +lemma atom_image_cong: + fixes X Y::"('a::at_base) set" + shows "(atom ` X = atom ` Y) = (X = Y)" + apply(rule inj_image_eq_iff) + apply(simp add: inj_on_def) + done + +lemma atom_image_supp: + "supp S = supp (atom ` S)" + apply(simp add: supp_def) + apply(simp add: image_eqvt) + apply(subst (2) permute_fun_def) + apply(simp add: atom_eqvt) + apply(simp add: atom_image_cong) + done + +lemma supp_finite_at_set: + fixes S::"('a::at) set" + assumes a: "finite S" + shows "supp S = atom ` S" + apply(rule finite_supp_unique) + apply(simp add: supports_def) + apply(rule allI)+ + apply(rule impI) + apply(rule swap_fresh_fresh) + apply(simp add: fresh_def) + apply(simp add: atom_image_supp) + apply(subst supp_finite_atom_set) + apply(rule finite_imageI) + apply(simp add: a) + apply(simp) + apply(simp add: fresh_def) + apply(simp add: atom_image_supp) + apply(subst supp_finite_atom_set) + apply(rule finite_imageI) + apply(simp add: a) + apply(simp) + apply(rule finite_imageI) + apply(simp add: a) + apply(drule swap_set_in) + apply(assumption) + apply(simp) + apply(simp add: image_eqvt) + apply(simp add: permute_fun_def) + apply(simp add: atom_eqvt) + apply(simp add: atom_image_cong) + done + +lemma supp_at_insert: + fixes S::"('a::at) set" + assumes a: "finite S" + shows "supp (insert a S) = supp a \ supp S" + using a + apply (simp add: supp_finite_at_set) + apply (simp add: supp_at_base) + done section {* A swapping operation for concrete atoms *} diff -r 2b0cc308fd6a -r 9eab1dfc14d2 Nominal-General/Nominal2_Base.thy --- a/Nominal-General/Nominal2_Base.thy Wed Apr 21 21:52:30 2010 +0200 +++ b/Nominal-General/Nominal2_Base.thy Thu Apr 22 05:16:23 2010 +0200 @@ -809,22 +809,6 @@ qed qed -section {* Support for finite sets of atoms *} - - -lemma supp_finite_atom_set: - fixes S::"atom set" - assumes "finite S" - shows "supp S = S" - apply(rule finite_supp_unique) - apply(simp add: supports_def) - apply(simp add: swap_set_not_in) - apply(rule assms) - apply(simp add: swap_set_in) -done - - - section {* Finitely-supported types *} class fs = pt + @@ -860,6 +844,24 @@ instance atom :: fs by default (simp add: supp_atom) +section {* Support for finite sets of atoms *} + +lemma supp_finite_atom_set: + fixes S::"atom set" + assumes "finite S" + shows "supp S = S" + apply(rule finite_supp_unique) + apply(simp add: supports_def) + apply(simp add: swap_set_not_in) + apply(rule assms) + apply(simp add: swap_set_in) +done + +lemma supp_atom_insert: + fixes S::"atom set" + assumes a: "finite S" + shows "supp (insert a S) = supp a \ supp S" + using a by (simp add: supp_finite_atom_set supp_atom) section {* Type @{typ perm} is finitely-supported. *} diff -r 2b0cc308fd6a -r 9eab1dfc14d2 Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Wed Apr 21 21:52:30 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Thu Apr 22 05:16:23 2010 +0200 @@ -6,7 +6,7 @@ (contains many, but not all such lemmas). *) theory Nominal2_Eqvt -imports Nominal2_Base Nominal2_Atoms +imports Nominal2_Base uses ("nominal_thmdecls.ML") ("nominal_permeq.ML") ("nominal_eqvt.ML") @@ -259,7 +259,7 @@ empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt - atom_eqvt add_perm_eqvt + add_perm_eqvt lemmas [eqvt_raw] = permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) diff -r 2b0cc308fd6a -r 9eab1dfc14d2 Nominal/Abs.thy --- a/Nominal/Abs.thy Wed Apr 21 21:52:30 2010 +0200 +++ b/Nominal/Abs.thy Thu Apr 22 05:16:23 2010 +0200 @@ -2,8 +2,8 @@ imports "../Nominal-General/Nominal2_Atoms" "../Nominal-General/Nominal2_Eqvt" "../Nominal-General/Nominal2_Supp" - "Nominal2_FSet" "Quotient" + "Quotient_List" "Quotient_Product" begin @@ -397,13 +397,12 @@ section {* BELOW is stuff that may or may not be needed *} - lemma supp_atom_image: fixes as::"'a::at_base set" shows "supp (atom ` as) = supp as" apply(simp add: supp_def) apply(simp add: image_eqvt) -apply(simp add: atom_eqvt_raw) +apply(simp add: eqvts_raw) apply(simp add: atom_image_cong) done diff -r 2b0cc308fd6a -r 9eab1dfc14d2 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Wed Apr 21 21:52:30 2010 +0200 +++ b/Nominal/Ex/TypeSchemes.thy Thu Apr 22 05:16:23 2010 +0200 @@ -108,10 +108,9 @@ apply (simp add: fin_fset_to_set) apply (simp add: finite_supp) apply (simp add: eqvts finite_supp) - apply (subst atom_eqvt_raw[symmetric]) - apply (subst fmap_eqvt[symmetric]) - apply (subst fset_to_set_eqvt[symmetric]) - apply (simp only: fresh_star_permute_iff) + apply (rule_tac p=" -p" in permute_boolE) + apply(simp add: eqvts) + apply(simp add: permute_fun_def atom_eqvt) apply (simp add: fresh_star_def) apply clarify apply (simp add: fresh_def) diff -r 2b0cc308fd6a -r 9eab1dfc14d2 Nominal/Nominal2_FSet.thy --- a/Nominal/Nominal2_FSet.thy Wed Apr 21 21:52:30 2010 +0200 +++ b/Nominal/Nominal2_FSet.thy Thu Apr 22 05:16:23 2010 +0200 @@ -71,55 +71,6 @@ apply (simp add: atom_fmap_cong) done -lemma supp_atom_insert: - "finite (xs :: atom set) \ supp (insert x xs) = supp x \ supp xs" - apply (simp add: supp_finite_atom_set) - apply (simp add: supp_atom) - done - -lemma atom_image_cong: - shows "(atom ` X = atom ` Y) = (X = Y)" - apply(rule inj_image_eq_iff) - apply(simp add: inj_on_def) - done - -lemma atom_eqvt_raw: - fixes p::"perm" - shows "(p \ atom) = atom" - apply(perm_simp) - apply(simp) - done - -lemma supp_finite_at_set: - fixes S::"('a :: at) set" - assumes a: "finite S" - shows "supp S = atom ` S" - apply(rule finite_supp_unique) - apply(simp add: supports_def) - apply (rule finite_induct[OF a]) - apply (simp add: eqvts) - apply (simp) - apply clarify - apply (subst atom_image_cong[symmetric]) - apply (subst atom_eqvt_raw[symmetric]) - apply (subst eqvts[symmetric]) - apply (rule swap_set_not_in) - apply simp_all - apply(rule finite_imageI) - apply(rule a) - apply (subst atom_image_cong[symmetric]) - apply (subst atom_eqvt_raw[symmetric]) - apply (subst eqvts[symmetric]) - apply (rule swap_set_in) - apply simp_all - done - -lemma supp_at_insert: - "finite (xs :: ('a :: at) set) \ supp (insert x xs) = supp x \ supp xs" - apply (simp add: supp_finite_at_set) - apply (simp add: supp_at_base) - done - lemma supp_atom_finsert: "supp (finsert (x :: atom) S) = supp x \ supp S" apply (subst supp_fset_to_set[symmetric]) @@ -129,7 +80,8 @@ done lemma supp_at_finsert: - "supp (finsert (x :: 'a :: at) S) = supp x \ supp S" + fixes S::"('a::at) fset" + shows "supp (finsert x S) = supp x \ 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])