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
--- 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 \<longleftrightarrow> a = b"
assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> 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 \<union> 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 *}
--- 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 \<union> supp S"
+ using a by (simp add: supp_finite_atom_set supp_atom)
section {* Type @{typ perm} is finitely-supported. *}
--- 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 *)
--- 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
--- 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)
--- 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) \<Longrightarrow> supp (insert x xs) = supp x \<union> 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 \<bullet> 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) \<Longrightarrow> supp (insert x xs) = supp x \<union> 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 \<union> 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 \<union> supp S"
+ fixes S::"('a::at) fset"
+ shows "supp (finsert x S) = supp x \<union> 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])