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
authorChristian Urban <urbanc@in.tum.de>
Thu, 22 Apr 2010 05:16:23 +0200
changeset 1933 9eab1dfc14d2
parent 1932 2b0cc308fd6a
child 1934 8f6e68dc6cbc
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
Nominal-General/Nominal2_Atoms.thy
Nominal-General/Nominal2_Base.thy
Nominal-General/Nominal2_Eqvt.thy
Nominal/Abs.thy
Nominal/Ex/TypeSchemes.thy
Nominal/Nominal2_FSet.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 \<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])