# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271878149 -7200
# Node ID f189cf2c0987c75e5e8cc3195d447031426bcbdb
# Parent  e42bd9d95f093a88fcb31ec03abb377012d41de2
moved some lemmas into the right places

diff -r e42bd9d95f09 -r f189cf2c0987 Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Wed Apr 21 17:42:57 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Wed Apr 21 21:29:09 2010 +0200
@@ -29,6 +29,11 @@
 where
   "sort_of (Atom s i) = s"
 
+primrec
+  nat_of :: "atom \<Rightarrow> nat"
+where
+  "nat_of (Atom s n) = n"
+
 
 text {* There are infinitely many atoms of each sort. *}
 lemma INFM_sort_of_eq: 
@@ -63,6 +68,11 @@
   then show ?thesis ..
 qed
 
+lemma atom_components_eq_iff:
+  fixes a b :: atom
+  shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b"
+  by (induct a, induct b, simp)
+
 section {* Sort-Respecting Permutations *}
 
 typedef perm =
@@ -459,7 +469,6 @@
   unfolding permute_set_eq
   using a by (auto simp add: swap_atom)
 
-
 subsection {* Permutations for units *}
 
 instantiation unit :: pt
@@ -800,6 +809,22 @@
   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 +
diff -r e42bd9d95f09 -r f189cf2c0987 Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Wed Apr 21 17:42:57 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Wed Apr 21 21:29:09 2010 +0200
@@ -11,6 +11,7 @@
 
 section {* Fresh-Star *}
 
+
 text {* The fresh-star generalisation of fresh is used in strong
   induction principles. *}
 
@@ -127,9 +128,8 @@
     moreover
     have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"
       using p2 unfolding q
-      apply (intro subset_trans [OF supp_plus_perm])
-      apply (auto simp add: supp_swap)
-      done
+      by (intro subset_trans [OF supp_plus_perm])
+         (auto simp add: supp_swap)
     ultimately show ?case by blast
   qed
 qed
@@ -158,20 +158,21 @@
 
 lemma at_set_avoiding2_atom:
   assumes "finite (supp c)" "finite (supp x)"
-  and     b: "xa \<sharp> x"
-  shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p"
+  and     b: "a \<sharp> x"
+  shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p"
 proof -
-  have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
-  obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p"
-    using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast
-  have c: "(p \<bullet> xa) \<sharp> c" using p1
+  have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
+  obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p"
+    using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast
+  have c: "(p \<bullet> a) \<sharp> c" using p1
     unfolding fresh_star_def Ball_def 
-    by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts)
-  hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
-  then show ?thesis by blast
+    by (erule_tac x="p \<bullet> a" in allE) (simp add: eqvts)
+  hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
+  then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
 qed
 
-section {* The freshness lemma according to Andrew Pitts *}
+
+section {* The freshness lemma according to Andy Pitts *}
 
 lemma freshness_lemma:
   fixes h :: "'a::at \<Rightarrow> 'b::pt"
@@ -339,17 +340,9 @@
 using P Q by (rule FRESH_binop_iff)
 
 
-section {* An example of a function without finite support *}
+section {* @{const nat_of} is an example of a function 
+  without finite support *}
 
-primrec
-  nat_of :: "atom \<Rightarrow> nat"
-where
-  "nat_of (Atom s n) = n"
-
-lemma atom_eq_iff:
-  fixes a b :: atom
-  shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b"
-  by (induct a, induct b, simp)
 
 lemma not_fresh_nat_of:
   shows "\<not> a \<sharp> nat_of"
@@ -368,7 +361,7 @@
   also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp
   also have "\<dots> = nat_of b" using b2 by simp
   finally have "nat_of a = nat_of b" by simp
-  with b2 have "a = b" by (simp add: atom_eq_iff)
+  with b2 have "a = b" by (simp add: atom_components_eq_iff)
   with b1 show "False" by simp
 qed
 
@@ -377,27 +370,13 @@
   using not_fresh_nat_of [unfolded fresh_def] by auto
 
 
-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
-
-text {* Induction principle for permutations *}
+section {* Induction principle for permutations *}
 
 
 lemma perm_struct_induct[consumes 1, case_names zero swap]:
   assumes S: "supp p \<subseteq> S"
-  assumes zero: "P 0"
-  assumes swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> 
-    \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
+  and zero: "P 0"
+  and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
   shows "P p"
 proof -
   have "finite (supp p)" by (simp add: finite_supp)
@@ -433,14 +412,14 @@
   qed
 qed
 
-lemma perm_struct_induct2[case_names zero swap]:
+lemma perm_simple_struct_induct[case_names zero swap]:
   assumes zero: "P 0"
-  assumes swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
+  and     swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
   shows "P p"
 by (rule_tac S="supp p" in perm_struct_induct)
    (auto intro: zero swap)
 
-lemma perm_subset_induct [consumes 1, case_names zero swap plus]:
+lemma perm_subset_induct[consumes 1, case_names zero swap plus]:
   assumes S: "supp p \<subseteq> S"
   assumes zero: "P 0"
   assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"