--- a/NEWS Thu Jun 25 07:34:30 2009 +0200
+++ b/NEWS Thu Jun 25 14:59:29 2009 +0200
@@ -62,6 +62,9 @@
* Simplified interfaces of datatype module. INCOMPATIBILITY.
+* Abbreviation "arbitrary" of "undefined" has disappeared; use "undefined" directly.
+INCOMPATIBILITY.
+
*** ML ***
--- a/src/HOL/HOL.thy Thu Jun 25 07:34:30 2009 +0200
+++ b/src/HOL/HOL.thy Thu Jun 25 14:59:29 2009 +0200
@@ -198,9 +198,6 @@
axiomatization
undefined :: 'a
-abbreviation (input)
- "arbitrary \<equiv> undefined"
-
subsubsection {* Generic classes and algebraic operations *}
--- a/src/HOL/Library/Fin_Fun.thy Thu Jun 25 07:34:30 2009 +0200
+++ b/src/HOL/Library/Fin_Fun.thy Thu Jun 25 14:59:29 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)
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Thu Jun 25 07:34:30 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Thu Jun 25 14:59:29 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 }