Quellcode-Bibliothek Support.thy Sprache: Isabelle

theory Support
  imports "HOL-Nominal.Nominal"
begin

text \<open>
  An example showing that in general

  x\<sharp>(A \<union> B) does not imply  x\<sharp>A and  x\<sharp>B

  For this we set A to the set of even atoms and B to
  the set of odd atoms. Then A \<union> B, that is the set of
  all atoms, has empty support. The sets A, respectively B,
  however have the set of all atoms as their support.
\<close>

atom_decl atom

text \<open>The set of even atoms.\<close>
abbreviation
  EVEN :: "atom set"
where
  "EVEN \ {atom n | n. \i. n=2*i}"

text \<open>The set of odd atoms:\<close>
abbreviation
  ODD :: "atom set"
where
  "ODD \ {atom n | n. \i. n=2*i+1}"

text \<open>An atom is either even or odd.\<close>
lemma even_or_odd:
  fixes n :: nat
  shows "\i. (n = 2*i) \ (n=2*i+1)"
  by (induct n) (presburger)+

text \<open>
  The union of even and odd atoms is the set of all atoms.
  (Unfortunately I do not know a simpler proof of this fact.)\<close>
lemma EVEN_union_ODD:
  shows "EVEN \ ODD = UNIV"
  using even_or_odd
proof -
  have "EVEN \ ODD = (\n. atom n) ` {n. \i. n = 2*i} \ (\n. atom n) ` {n. \i. n = 2*i+1}" by auto
  also have "\ = (\n. atom n) ` ({n. \i. n = 2*i} \ {n. \i. n = 2*i+1})" by auto
  also have "\ = (\n. atom n) ` ({n. \i. n = 2*i \ n = 2*i+1})" by auto
  also have "\ = (\n. atom n) ` (UNIV::nat set)" using even_or_odd by auto
  also have "\ = (UNIV::atom set)" using atom.exhaust
    by (auto simp add: surj_def)
  finally show "EVEN \ ODD = UNIV" by simp
qed

text \<open>The sets of even and odd atoms are disjunct.\<close>
lemma EVEN_intersect_ODD:
  shows "EVEN \ ODD = {}"
  using even_or_odd
  by (auto) (presburger)

text \<open>
  The preceeding two lemmas help us to prove
  the following two useful equalities:\<close>

lemma UNIV_subtract:
  shows "UNIV - EVEN = ODD"
  and   "UNIV - ODD = EVEN"
  using EVEN_union_ODD EVEN_intersect_ODD
  by (blast)+

text \<open>The sets EVEN and ODD are infinite.\<close>
lemma EVEN_ODD_infinite:
  shows "infinite EVEN"
  and   "infinite ODD"
unfolding infinite_iff_countable_subset
proof -
  let ?f = "\n. atom (2*n)"
  have "inj ?f \ range ?f \ EVEN" by (auto simp add: inj_on_def)
  then show "\f::nat\atom. inj f \ range f \ EVEN" by (rule_tac exI)
next
  let ?f = "\n. atom (2*n+1)"
  have "inj ?f \ range ?f \ ODD" by (auto simp add: inj_on_def)
  then show "\f::nat\atom. inj f \ range f \ ODD" by (rule_tac exI)
qed

text \<open>
  A general fact about a set S of atoms that is both infinite and
  coinfinite. Then S has all atoms as its support. Steve Zdancewic
  helped with proving this fact.\<close>

lemma supp_infinite_coinfinite:
  fixes S::"atom set"
  assumes asm1: "infinite S"
  and     asm2: "infinite (UNIV-S)"
  shows "(supp S) = (UNIV::atom set)"
proof -
  have "\(x::atom). x\(supp S)"
  proof
    fix x::"atom"
    show "x\(supp S)"
    proof (cases "x\S")
      case True
      have "x\S" by fact
      hence "\b\(UNIV-S). [(x,b)]\S\S" by (auto simp add: perm_set_def calc_atm)
      with asm2 have "infinite {b\(UNIV-S). [(x,b)]\S\S}" by (rule infinite_Collection)
      hence "infinite {b. [(x,b)]\S\S}" by (rule_tac infinite_super, auto)
      then show "x\(supp S)" by (simp add: supp_def)
    next
      case False
      have "x\S" by fact
      hence "\b\S. [(x,b)]\S\S" by (auto simp add: perm_set_def calc_atm)
      with asm1 have "infinite {b\S. [(x,b)]\S\S}" by (rule infinite_Collection)
      hence "infinite {b. [(x,b)]\S\S}" by (rule_tac infinite_super, auto)
      then show "x\(supp S)" by (simp add: supp_def)
    qed
  qed
  then show "(supp S) = (UNIV::atom set)" by auto
qed

text \<open>As a corollary we get that EVEN and ODD have infinite support.\<close>
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

text \<open>
  The set of all atoms has empty support, since any swappings leaves
  this set unchanged.\<close>

lemma UNIV_supp:
  shows "supp (UNIV::atom set) = ({}::atom set)"
proof -
  have "\(x::atom) (y::atom). [(x,y)]\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

text \<open>Putting everything together.\<close>
theorem EVEN_ODD_freshness:
  fixes x::"atom"
  shows "x\(EVEN \ ODD)"
  and   "\x\EVEN"
  and   "\x\ODD"
  by (auto simp only: fresh_def EVEN_union_ODD EVEN_ODD_supp UNIV_supp)

text \<open>Moral: support is a sublte notion.\<close>

end

quality96%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.