Changed 'bounded unique existential quantifiers' from a constant to syntax translation.
authorhoelzl
Thu Feb 04 14:45:08 2010 +0100 (2010-02-04)
changeset 349995312d2ffee3b
parent 34998 5e492a862b34
child 35000 ab23493e1f0f
child 35007 8c339c73495c
child 35026 02850d0b95ac
child 35073 534005fff7fe
Changed 'bounded unique existential quantifiers' from a constant to syntax translation.
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Feb 04 13:36:52 2010 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Feb 04 14:45:08 2010 +0100
     1.3 @@ -5906,7 +5906,7 @@
     1.4        using c and zero_le_dist[of x y] by auto
     1.5      hence "y = x" by auto
     1.6    }
     1.7 -  ultimately show ?thesis unfolding Bex1_def using `x\<in>s` by blast+
     1.8 +  ultimately show ?thesis using `x\<in>s` by blast+
     1.9  qed
    1.10  
    1.11  subsection{* Edelstein fixed point theorem.                                            *}
    1.12 @@ -5923,7 +5923,7 @@
    1.13      hence "x = y" using `x\<in>s` and dist[THEN bspec[where x=x], THEN bspec[where x=y]]
    1.14        unfolding g[THEN bspec[where x=x], OF `x\<in>s`]
    1.15        unfolding g[THEN bspec[where x=y], OF `y\<in>s`] by auto  }
    1.16 -  thus ?thesis unfolding Bex1_def using `x\<in>s` and g by blast+
    1.17 +  thus ?thesis using `x\<in>s` and g by blast+
    1.18  next
    1.19    case True
    1.20    then obtain x where [simp]:"x\<in>s" and "g x \<noteq> x" by auto
    1.21 @@ -6028,7 +6028,7 @@
    1.22    { fix x assume "x\<in>s" "g x = x" "x\<noteq>a"
    1.23      hence "False" using dist[THEN bspec[where x=a], THEN bspec[where x=x]]
    1.24        using `g a = a` and `a\<in>s` by auto  }
    1.25 -  ultimately show "\<exists>!x\<in>s. g x = x" unfolding Bex1_def using `a\<in>s` by blast
    1.26 +  ultimately show "\<exists>!x\<in>s. g x = x" using `a\<in>s` by blast
    1.27  qed
    1.28  
    1.29  end
     2.1 --- a/src/HOL/Set.thy	Thu Feb 04 13:36:52 2010 +0100
     2.2 +++ b/src/HOL/Set.thy	Thu Feb 04 14:45:08 2010 +0100
     2.3 @@ -161,14 +161,12 @@
     2.4  consts
     2.5    Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
     2.6    Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
     2.7 -  Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
     2.8  
     2.9  local
    2.10  
    2.11  defs
    2.12    Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
    2.13    Bex_def:      "Bex A P        == EX x. x:A & P(x)"
    2.14 -  Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
    2.15  
    2.16  syntax
    2.17    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
    2.18 @@ -195,7 +193,7 @@
    2.19  translations
    2.20    "ALL x:A. P"  == "Ball A (%x. P)"
    2.21    "EX x:A. P"   == "Bex A (%x. P)"
    2.22 -  "EX! x:A. P"  == "Bex1 A (%x. P)"
    2.23 +  "EX! x:A. P"  => "EX! x. x:A & P"
    2.24    "LEAST x:A. P" => "LEAST x. x:A & P"
    2.25  
    2.26  syntax (output)