--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Examples/Support.thy Mon Oct 08 05:23:47 2007 +0200
@@ -0,0 +1,124 @@
+(* $Id$ *)
+
+theory Support
+imports "../Nominal"
+begin
+
+text {*
+
+ An example showing that in general
+
+ x\<sharp>(A \<union> B) does not imply x\<sharp>A and x\<sharp>B
+
+ The example shows that with A set to the set of
+ even atoms and B to the set of odd even atoms.
+ Then A \<union> B, that is the set of all atoms, has
+ empty support. The sets A, respectively B, have
+ the set of all atoms as support.
+
+*}
+
+atom_decl atom
+
+abbreviation
+ EVEN :: "atom set"
+where
+ "EVEN \<equiv> {atom n | n. \<exists>i. n=2*i}"
+
+abbreviation
+ ODD :: "atom set"
+where
+ "ODD \<equiv> {atom n | n. \<exists>i. n=2*i+1}"
+
+lemma even_or_odd:
+ fixes n::"nat"
+ shows "\<exists>i. (n = 2*i) \<or> (n=2*i+1)"
+ by (induct n) (presburger)+
+
+lemma EVEN_union_ODD:
+ shows "EVEN \<union> ODD = UNIV"
+proof -
+ have "EVEN \<union> ODD = (\<lambda>n. atom n) ` {n. \<exists>i. n = 2*i} \<union> (\<lambda>n. atom n) ` {n. \<exists>i. n = 2*i+1}" by auto
+ also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i} \<union> {n. \<exists>i. n = 2*i+1})" by auto
+ also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i \<or> n = 2*i+1})" by auto
+ also have "\<dots> = (\<lambda>n. atom n) ` (UNIV::nat set)" using even_or_odd by auto
+ also have "\<dots> = (UNIV::atom set)" using atom.exhaust
+ by (rule_tac surj_range) (auto simp add: surj_def)
+ finally show "EVEN \<union> ODD = UNIV" by simp
+qed
+
+lemma EVEN_intersect_ODD:
+ shows "EVEN \<inter> ODD = {}"
+ using even_or_odd
+ by (auto) (presburger)
+
+lemma UNIV_subtract:
+ shows "UNIV - EVEN = ODD"
+ and "UNIV - ODD = EVEN"
+ using EVEN_union_ODD EVEN_intersect_ODD
+ by (blast)+
+
+lemma EVEN_ODD_infinite:
+ shows "infinite EVEN"
+ and "infinite ODD"
+apply(simp add: infinite_iff_countable_subset)
+apply(rule_tac x="\<lambda>n. atom (2*n)" in exI)
+apply(auto simp add: inj_on_def)[1]
+apply(simp add: infinite_iff_countable_subset)
+apply(rule_tac x="\<lambda>n. atom (2*n+1)" in exI)
+apply(auto simp add: inj_on_def)
+done
+
+(* A set S that is infinite and coinfinite has all atoms as its support *)
+lemma supp_infinite_coinfinite:
+ fixes S::"atom set"
+ assumes a: "infinite S"
+ and b: "infinite (UNIV-S)"
+ shows "(supp S) = (UNIV::atom set)"
+proof -
+ have "\<forall>(x::atom). x\<in>(supp S)"
+ proof
+ fix x::"atom"
+ show "x\<in>(supp S)"
+ proof (cases "x\<in>S")
+ case True
+ have "x\<in>S" by fact
+ hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
+ with b have "infinite {b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
+ hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
+ then show "x\<in>(supp S)" by (simp add: supp_def)
+ next
+ case False
+ have "x\<notin>S" by fact
+ hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
+ with a have "infinite {b\<in>S. [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
+ hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
+ then show "x\<in>(supp S)" by (simp add: supp_def)
+ qed
+ qed
+ then show "(supp S) = (UNIV::atom set)" by auto
+qed
+
+lemma EVEN_ODD_supp:
+ shows "supp EVEN = (UNIV::atom set)"
+ and "supp ODD = (UNIV::atom set)"
+ using supp_infinite_coinfinite UNIV_subtract EVEN_ODD_infinite
+ by simp_all
+
+lemma UNIV_supp:
+ shows "supp (UNIV::atom set) = ({}::atom set)"
+proof -
+ have "\<forall>(x::atom) (y::atom). [(x,y)]\<bullet>UNIV = (UNIV::atom set)"
+ by (auto simp add: perm_set_def calc_atm)
+ then show "supp (UNIV::atom set) = ({}::atom set)"
+ by (simp add: supp_def)
+qed
+
+theorem EVEN_ODD_freshness:
+ fixes x::"atom"
+ shows "x\<sharp>(EVEN \<union> ODD)"
+ and "\<not>x\<sharp>EVEN"
+ and "\<not>x\<sharp>ODD"
+ by (auto simp only: fresh_def EVEN_union_ODD EVEN_ODD_supp UNIV_supp)
+
+end
\ No newline at end of file