# HG changeset patch
# User haftmann
# Date 1245937356 -7200
# Node ID 2f0adf64985b86842b6d028a9ebe49a3852677e4
# Parent  a36b5e02c1abbd1fc8d1d30cb3f073f10c6c3ab9# Parent  627d142fce19b8c618276be74817069a353f5472
merged

diff -r a36b5e02c1ab -r 2f0adf64985b NEWS
--- a/NEWS	Thu Jun 25 13:40:03 2009 +0200
+++ b/NEWS	Thu Jun 25 15:42:36 2009 +0200
@@ -62,6 +62,9 @@
 
 * Simplified interfaces of datatype module.  INCOMPATIBILITY.
 
+* Abbreviation "arbitrary" of "undefined" has disappeared; use "undefined" directly.
+INCOMPATIBILITY.
+
 
 *** ML ***
 
diff -r a36b5e02c1ab -r 2f0adf64985b src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jun 25 13:40:03 2009 +0200
+++ b/src/HOL/HOL.thy	Thu Jun 25 15:42:36 2009 +0200
@@ -198,9 +198,6 @@
 axiomatization
   undefined :: 'a
 
-abbreviation (input)
-  "arbitrary \<equiv> undefined"
-
 
 subsubsection {* Generic classes and algebraic operations *}
 
diff -r a36b5e02c1ab -r 2f0adf64985b src/HOL/Library/Fin_Fun.thy
--- a/src/HOL/Library/Fin_Fun.thy	Thu Jun 25 13:40:03 2009 +0200
+++ b/src/HOL/Library/Fin_Fun.thy	Thu Jun 25 15:42:36 2009 +0200
@@ -383,7 +383,7 @@
 subsection {* Default value for FinFuns *}
 
 definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"
-where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then arbitrary else THE b. finite {a. f a \<noteq> b})"
+where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then undefined else THE b. finite {a. f a \<noteq> b})"
 
 lemma finfun_default_aux_infinite:
   fixes f :: "'a \<Rightarrow> 'b"
@@ -453,7 +453,7 @@
 lemma finite_finfun_default: "finite {a. Rep_finfun f a \<noteq> finfun_default f}"
 unfolding finfun_default_def by(simp add: finite_finfun_default_aux)
 
-lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then arbitrary else b)"
+lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
 apply(auto simp add: finfun_default_def finfun_const_def finfun_default_aux_infinite)
 apply(simp add: finfun_default_aux_def)
 done
@@ -790,10 +790,10 @@
   ultimately show ?thesis by(simp add: finfun_rec_def)
 next
   case True
-  hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = arbitrary" by(simp add: finfun_default_const)
-  let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g) \<and> finite (dom g) \<and> arbitrary \<notin> ran g"
+  hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = undefined" by(simp add: finfun_default_const)
+  let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g) \<and> finite (dom g) \<and> undefined \<notin> ran g"
   show ?thesis
-  proof(cases "c = arbitrary")
+  proof(cases "c = undefined")
     case True
     have the: "The ?the = empty"
     proof
@@ -801,10 +801,10 @@
     next
       fix g'
       assume "?the g'"
-      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g')"
-        and fin: "finite (dom g')" and g: "arbitrary \<notin> ran g'" by simp_all
-      from fin have "map_default arbitrary g' \<in> finfun" by(rule map_default_in_finfun)
-      with fg have "map_default arbitrary g' = (\<lambda>a. c)"
+      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
+        and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
+      from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
+      with fg have "map_default undefined g' = (\<lambda>a. c)"
         by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
       with True show "g' = empty"
         by -(rule map_default_inject(2)[OF _ fin g], auto)
@@ -820,10 +820,10 @@
     next
       fix g' :: "'a \<rightharpoonup> 'b"
       assume "?the g'"
-      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g')"
-        and fin: "finite (dom g')" and g: "arbitrary \<notin> ran g'" by simp_all
-      from fin have "map_default arbitrary g' \<in> finfun" by(rule map_default_in_finfun)
-      with fg have "map_default arbitrary g' = (\<lambda>a. c)"
+      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
+        and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
+      from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
+      with fg have "map_default undefined g' = (\<lambda>a. c)"
         by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
       with True False show "g' = (\<lambda>a::'a. Some c)"
         by -(rule map_default_inject(2)[OF _ fin g], auto simp add: dom_def ran_def map_default_def_raw)
diff -r a36b5e02c1ab -r 2f0adf64985b src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 25 13:40:03 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 25 15:42:36 2009 +0200
@@ -533,18 +533,18 @@
   fix x :: "'a ^ 'b"
   {
     fix e :: real assume "0 < e"
-    def a \<equiv> "x $ arbitrary"
+    def a \<equiv> "x $ undefined"
     have "a islimpt UNIV" by (rule islimpt_UNIV)
     with `0 < e` obtain b where "b \<noteq> a" and "dist b a < e"
       unfolding islimpt_approachable by auto
-    def y \<equiv> "Cart_lambda ((Cart_nth x)(arbitrary := b))"
+    def y \<equiv> "Cart_lambda ((Cart_nth x)(undefined := b))"
     from `b \<noteq> a` have "y \<noteq> x"
       unfolding a_def y_def by (simp add: Cart_eq)
     from `dist b a < e` have "dist y x < e"
       unfolding dist_vector_def a_def y_def
       apply simp
       apply (rule le_less_trans [OF setL2_le_setsum [OF zero_le_dist]])
-      apply (subst setsum_diff1' [where a=arbitrary], simp, simp, simp)
+      apply (subst setsum_diff1' [where a=undefined], simp, simp, simp)
       done
     from `y \<noteq> x` and `dist y x < e`
     have "\<exists>y\<in>UNIV. y \<noteq> x \<and> dist y x < e" by auto
@@ -2695,29 +2695,29 @@
 
 primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where
   "helper_2 beyond 0 = beyond 0" |
-  "helper_2 beyond (Suc n) = beyond (dist arbitrary (helper_2 beyond n) + 1 )"
+  "helper_2 beyond (Suc n) = beyond (dist undefined (helper_2 beyond n) + 1 )"
 
 lemma bolzano_weierstrass_imp_bounded: fixes s::"'a::metric_space set"
   assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
   shows "bounded s"
 proof(rule ccontr)
   assume "\<not> bounded s"
-  then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> dist arbitrary (beyond a) \<le> a"
-    unfolding bounded_any_center [where a=arbitrary]
-    apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> dist arbitrary x \<le> a"] by auto
-  hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. dist arbitrary (beyond a) > a"
+  then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> dist undefined (beyond a) \<le> a"
+    unfolding bounded_any_center [where a=undefined]
+    apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> dist undefined x \<le> a"] by auto
+  hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. dist undefined (beyond a) > a"
     unfolding linorder_not_le by auto
   def x \<equiv> "helper_2 beyond"
 
   { fix m n ::nat assume "m<n"
-    hence "dist arbitrary (x m) + 1 < dist arbitrary (x n)"
+    hence "dist undefined (x m) + 1 < dist undefined (x n)"
     proof(induct n)
       case 0 thus ?case by auto
     next
       case (Suc n)
-      have *:"dist arbitrary (x n) + 1 < dist arbitrary (x (Suc n))"
+      have *:"dist undefined (x n) + 1 < dist undefined (x (Suc n))"
         unfolding x_def and helper_2.simps
-	using beyond(2)[of "dist arbitrary (helper_2 beyond n) + 1"] by auto
+	using beyond(2)[of "dist undefined (helper_2 beyond n) + 1"] by auto
       thus ?case proof(cases "m < n")
 	case True thus ?thesis using Suc and * by auto
       next
@@ -2729,12 +2729,12 @@
     have "1 < dist (x m) (x n)"
     proof(cases "m<n")
       case True
-      hence "1 < dist arbitrary (x n) - dist arbitrary (x m)" using *[of m n] by auto
-      thus ?thesis using dist_triangle [of arbitrary "x n" "x m"] by arith
+      hence "1 < dist undefined (x n) - dist undefined (x m)" using *[of m n] by auto
+      thus ?thesis using dist_triangle [of undefined "x n" "x m"] by arith
     next
       case False hence "n<m" using `m\<noteq>n` by auto
-      hence "1 < dist arbitrary (x m) - dist arbitrary (x n)" using *[of n m] by auto
-      thus ?thesis using dist_triangle2 [of arbitrary "x m" "x n"] by arith
+      hence "1 < dist undefined (x m) - dist undefined (x n)" using *[of n m] by auto
+      thus ?thesis using dist_triangle2 [of undefined "x m" "x n"] by arith
     qed  } note ** = this
   { fix a b assume "x a = x b" "a \<noteq> b"
     hence False using **[of a b] by auto  }