# HG changeset patch
# User hoelzl
# Date 1311079128 -7200
# Node ID 1165fe965da89c9ed56063a2f4872791cb34d0c5
# Parent  ab93d0190a5d9b5a3c6539332850846cc03cda09
rename Fin to enat

diff -r ab93d0190a5d -r 1165fe965da8 src/HOL/HOLCF/FOCUS/Buffer_adm.thy
--- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Tue Jul 19 14:38:29 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Tue Jul 19 14:38:48 2011 +0200
@@ -8,7 +8,7 @@
 imports Buffer Stream_adm
 begin
 
-declare Fin_0 [simp]
+declare enat_0 [simp]
 
 lemma BufAC_Asm_d2: "a\<leadsto>s:BufAC_Asm ==> ? d. a=Md d"
 by (drule BufAC_Asm_unfold [THEN iffD1], auto)
@@ -116,7 +116,7 @@
 done
 
 (*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
-lemma BufAC_Cmt_2stream_monoP: "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> 
+lemma BufAC_Cmt_2stream_monoP: "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> enat (l i) < #x --> 
                      (x,f\<cdot>x):down_iterate BufAC_Cmt_F i --> 
                      (s,f\<cdot>s):down_iterate BufAC_Cmt_F i"
 apply (rule_tac x="%i. 2*i" in exI)
@@ -139,10 +139,10 @@
        \<lbrakk>f \<in> BufEq;
           \<forall>x s. s \<in> BufAC_Asm \<longrightarrow>
                 x \<sqsubseteq> s \<longrightarrow>
-                Fin (2 * i) < #x \<longrightarrow>
+                enat (2 * i) < #x \<longrightarrow>
                 (x, f\<cdot>x) \<in> down_iterate BufAC_Cmt_F i \<longrightarrow>
                 (s, f\<cdot>s) \<in> down_iterate BufAC_Cmt_F i;
-          Md d\<leadsto>\<bullet>\<leadsto>xa \<in> BufAC_Asm; Fin (2 * i) < #ya; f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>t;
+          Md d\<leadsto>\<bullet>\<leadsto>xa \<in> BufAC_Asm; enat (2 * i) < #ya; f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>t;
           (ya, t) \<in> down_iterate BufAC_Cmt_F i; ya \<sqsubseteq> xa\<rbrakk>
        \<Longrightarrow> (xa, rt\<cdot>(f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>xa))) \<in> down_iterate BufAC_Cmt_F i
 *)
@@ -158,11 +158,11 @@
 apply (erule subst)
 (*
  1. \<And>i d xa ya t ff ffa.
-       \<lbrakk>f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya; Fin (2 * i) < #ya;
+       \<lbrakk>f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya; enat (2 * i) < #ya;
           (ya, ffa\<cdot>ya) \<in> down_iterate BufAC_Cmt_F i; ya \<sqsubseteq> xa; f \<in> BufEq;
           \<forall>x s. s \<in> BufAC_Asm \<longrightarrow>
                 x \<sqsubseteq> s \<longrightarrow>
-                Fin (2 * i) < #x \<longrightarrow>
+                enat (2 * i) < #x \<longrightarrow>
                 (x, f\<cdot>x) \<in> down_iterate BufAC_Cmt_F i \<longrightarrow>
                 (s, f\<cdot>s) \<in> down_iterate BufAC_Cmt_F i;
           xa \<in> BufAC_Asm; ff \<in> BufEq; ffa \<in> BufEq\<rbrakk>
diff -r ab93d0190a5d -r 1165fe965da8 src/HOL/HOLCF/FOCUS/Fstream.thy
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Tue Jul 19 14:38:29 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Tue Jul 19 14:38:48 2011 +0200
@@ -144,13 +144,13 @@
 by (simp add: fscons_def)
 
 lemma slen_fscons_eq:
-        "(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)"
+        "(enat (Suc n) < #x) = (? a y. x = a~> y & enat n < #y)"
 apply (simp add: fscons_def2 slen_scons_eq)
 apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
 done
 
 lemma slen_fscons_eq_rev:
-        "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))"
+        "(#x < enat (Suc (Suc n))) = (!a y. x ~= a~> y | #y < enat (Suc n))"
 apply (simp add: fscons_def2 slen_scons_eq_rev)
 apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
 apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
@@ -163,7 +163,7 @@
 done
 
 lemma slen_fscons_less_eq:
-        "(#(a~> y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))"
+        "(#(a~> y) < enat (Suc (Suc n))) = (#y < enat (Suc n))"
 apply (subst slen_fscons_eq_rev)
 apply (fast dest!: fscons_inject [THEN iffD1])
 done
diff -r ab93d0190a5d -r 1165fe965da8 src/HOL/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jul 19 14:38:29 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jul 19 14:38:48 2011 +0200
@@ -28,7 +28,7 @@
 
 definition
   jth           :: "nat => 'a fstream => 'a" where
-  "jth = (%n s. if Fin n < #s then THE a. i_th n s = Def a else undefined)"
+  "jth = (%n s. if enat n < #s then THE a. i_th n s = Def a else undefined)"
 
 definition
   first         :: "'a fstream => 'a" where
@@ -36,7 +36,7 @@
 
 definition
   last          :: "'a fstream => 'a" where
-  "last = (%s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else undefined))"
+  "last = (%s. case #s of enat n => (if n~=0 then jth (THE k. Suc k = n) s else undefined))"
 
 
 abbreviation
@@ -54,7 +54,7 @@
 lemma ft_fsingleton[simp]: "ft$(<a>) = Def a"
 by (simp add: fsingleton_def2)
 
-lemma slen_fsingleton[simp]: "#(<a>) = Fin 1"
+lemma slen_fsingleton[simp]: "#(<a>) = enat 1"
 by (simp add: fsingleton_def2 enat_defs)
 
 lemma slen_fstreams[simp]: "#(<a> ooo s) = iSuc (#s)"
@@ -62,17 +62,17 @@
 
 lemma slen_fstreams2[simp]: "#(s ooo <a>) = iSuc (#s)"
 apply (cases "#s")
-apply (auto simp add: iSuc_Fin)
+apply (auto simp add: iSuc_enat)
 apply (insert slen_sconc [of _ s "Suc 0" "<a>"], auto)
 by (simp add: sconc_def)
 
 lemma j_th_0_fsingleton[simp]:"jth 0 (<a>) = a"
 apply (simp add: fsingleton_def2 jth_def)
-by (simp add: i_th_def Fin_0)
+by (simp add: i_th_def enat_0)
 
 lemma jth_0[simp]: "jth 0 (<a> ooo s) = a"  
 apply (simp add: fsingleton_def2 jth_def)
-by (simp add: i_th_def Fin_0)
+by (simp add: i_th_def enat_0)
 
 lemma first_sconc[simp]: "first (<a> ooo s) = a"
 by (simp add: first_def)
@@ -80,12 +80,12 @@
 lemma first_fsingleton[simp]: "first (<a>) = a"
 by (simp add: first_def)
 
-lemma jth_n[simp]: "Fin n = #s ==> jth n (s ooo <a>) = a"
+lemma jth_n[simp]: "enat n = #s ==> jth n (s ooo <a>) = a"
 apply (simp add: jth_def, auto)
 apply (simp add: i_th_def rt_sconc1)
 by (simp add: enat_defs split: enat.splits)
 
-lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a"
+lemma last_sconc[simp]: "enat n = #s ==> last (s ooo <a>) = a"
 apply (simp add: last_def)
 apply (simp add: enat_defs split:enat.splits)
 by (drule sym, auto)
@@ -102,13 +102,13 @@
 lemma last_infinite[simp]:"#s = \<infinity> ==> last s = undefined"
 by (simp add: last_def)
 
-lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
+lemma jth_slen_lemma1:"n <= k & enat n = #s ==> jth k s = undefined"
 by (simp add: jth_def enat_defs split:enat.splits, auto)
 
 lemma jth_UU[simp]:"jth n UU = undefined" 
 by (simp add: jth_def)
 
-lemma ext_last:"[|s ~= UU; Fin (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s" 
+lemma ext_last:"[|s ~= UU; enat (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s" 
 apply (simp add: last_def)
 apply (case_tac "#s", auto)
 apply (simp add: fsingleton_def2)
diff -r ab93d0190a5d -r 1165fe965da8 src/HOL/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 19 14:38:29 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 19 14:38:48 2011 +0200
@@ -10,14 +10,14 @@
 
 definition
   stream_monoP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where
-  "stream_monoP F = (\<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
+  "stream_monoP F = (\<exists>Q i. \<forall>P s. enat i \<le> #s \<longrightarrow>
                     (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P))"
 
 definition
   stream_antiP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where
   "stream_antiP F = (\<forall>P x. \<exists>Q i.
-                (#x  < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
-                (Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
+                (#x  < enat i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
+                (enat i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
                 (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P))))"
 
 definition
@@ -57,7 +57,7 @@
 lemma flatstream_adm_lemma:
   assumes 1: "Porder.chain Y"
   assumes 2: "!i. P (Y i)"
-  assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|]
+  assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. enat k < #((Y j)::'a::flat stream)|]
   ==> P(LUB i. Y i))"
   shows "P(LUB i. Y i)"
 apply (rule increasing_chain_adm_lemma [of _ P, OF 1 2])
@@ -79,7 +79,7 @@
 
 (* should be without reference to stream length? *)
 lemma flatstream_admI: "[|(!!Y. [| Porder.chain Y; !i. P (Y i); 
- !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P"
+ !k. ? j. enat k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P"
 apply (unfold adm_def)
 apply (intro strip)
 apply (erule (1) flatstream_adm_lemma)
@@ -88,12 +88,12 @@
 
 
 (* context (theory "Extended_Nat");*)
-lemma ile_lemma: "Fin (i + j) <= x ==> Fin i <= x"
+lemma ile_lemma: "enat (i + j) <= x ==> enat i <= x"
   by (rule order_trans) auto
 
 lemma stream_monoP2I:
 "!!X. stream_monoP F ==> !i. ? l. !x y. 
-  Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i"
+  enat l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i"
 apply (unfold stream_monoP_def)
 apply (safe)
 apply (rule_tac x="i*ia" in exI)
@@ -120,7 +120,7 @@
 done
 
 lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y. 
- Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;
+ enat l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;
     down_cont F |] ==> adm (%x. x:gfp F)"
 apply (erule INTER_down_iterate_is_gfp [THEN ssubst]) (* cont *)
 apply (simp (no_asm))
@@ -153,7 +153,7 @@
 apply (intro strip)
 apply (erule allE, erule all_dupE, erule exE, erule exE)
 apply (erule conjE)
-apply (case_tac "#x < Fin i")
+apply (case_tac "#x < enat i")
 apply ( fast)
 apply (unfold linorder_not_less)
 apply (drule (1) mp)
diff -r ab93d0190a5d -r 1165fe965da8 src/HOL/HOLCF/Library/Stream.thy
--- a/src/HOL/HOLCF/Library/Stream.thy	Tue Jul 19 14:38:29 2011 +0200
+++ b/src/HOL/HOLCF/Library/Stream.thy	Tue Jul 19 14:38:48 2011 +0200
@@ -23,7 +23,7 @@
 
 definition
   slen :: "'a stream \<Rightarrow> enat"  ("#_" [1000] 1000) where
-  "#s = (if stream_finite s then Fin (LEAST n. stream_take n\<cdot>s = s) else \<infinity>)"
+  "#s = (if stream_finite s then enat (LEAST n. stream_take n\<cdot>s = s) else \<infinity>)"
 
 
 (* concatenation *)
@@ -39,7 +39,7 @@
 definition
   sconc :: "'a stream => 'a stream => 'a stream"  (infixr "ooo" 65) where
   "s1 ooo s2 = (case #s1 of
-                  Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
+                  enat n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
                | \<infinity>     \<Rightarrow> s1)"
 
 primrec constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream"
@@ -51,7 +51,7 @@
 definition
   constr_sconc  :: "'a stream => 'a stream => 'a stream" where (* constructive *)
   "constr_sconc s1 s2 = (case #s1 of
-                          Fin n \<Rightarrow> constr_sconc' n s1 s2
+                          enat n \<Rightarrow> constr_sconc' n s1 s2
                         | \<infinity>    \<Rightarrow> s1)"
 
 
@@ -332,7 +332,7 @@
 lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = iSuc (#xs)"
 apply (case_tac "stream_finite (x && xs)")
 apply (simp add: slen_def, auto)
-apply (simp add: stream.finite_def, auto simp add: iSuc_Fin)
+apply (simp add: stream.finite_def, auto simp add: iSuc_enat)
 apply (rule Least_Suc2, auto)
 (*apply (drule sym)*)
 (*apply (drule sym scons_eq_UU [THEN iffD1],simp)*)
@@ -340,13 +340,13 @@
 apply (simp add: slen_def, auto)
 by (drule stream_finite_lemma1,auto)
 
-lemma slen_less_1_eq: "(#x < Fin (Suc 0)) = (x = \<bottom>)"
-by (cases x, auto simp add: Fin_0 iSuc_Fin[THEN sym])
+lemma slen_less_1_eq: "(#x < enat (Suc 0)) = (x = \<bottom>)"
+by (cases x, auto simp add: enat_0 iSuc_enat[THEN sym])
 
 lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)"
 by (cases x, auto)
 
-lemma slen_scons_eq: "(Fin (Suc n) < #x) = (? a y. x = a && y &  a ~= \<bottom> &  Fin n < #y)"
+lemma slen_scons_eq: "(enat (Suc n) < #x) = (? a y. x = a && y &  a ~= \<bottom> &  enat n < #y)"
 apply (auto, case_tac "x=UU",auto)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (case_tac "#y") apply simp_all
@@ -359,18 +359,18 @@
 lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \<infinity>"
 by (simp add: slen_def)
 
-lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < Fin (Suc n))"
+lemma slen_scons_eq_rev: "(#x < enat (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < enat (Suc n))"
  apply (cases x, auto)
    apply (simp add: zero_enat_def)
-  apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
- apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
+  apply (case_tac "#stream") apply (simp_all add: iSuc_enat)
+ apply (case_tac "#stream") apply (simp_all add: iSuc_enat)
 done
 
 lemma slen_take_lemma4 [rule_format]:
-  "!s. stream_take n$s ~= s --> #(stream_take n$s) = Fin n"
-apply (induct n, auto simp add: Fin_0)
+  "!s. stream_take n$s ~= s --> #(stream_take n$s) = enat n"
+apply (induct n, auto simp add: enat_0)
 apply (case_tac "s=UU", simp)
-by (drule stream_exhaust_eq [THEN iffD1], auto simp add: iSuc_Fin)
+by (drule stream_exhaust_eq [THEN iffD1], auto simp add: iSuc_enat)
 
 (*
 lemma stream_take_idempotent [simp]:
@@ -390,37 +390,37 @@
 by (simp add: chain_def,simp)
 *)
 
-lemma slen_take_eq: "ALL x. (Fin n < #x) = (stream_take n\<cdot>x ~= x)"
+lemma slen_take_eq: "ALL x. (enat n < #x) = (stream_take n\<cdot>x ~= x)"
 apply (induct_tac n, auto)
-apply (simp add: Fin_0, clarsimp)
+apply (simp add: enat_0, clarsimp)
 apply (drule not_sym)
 apply (drule slen_empty_eq [THEN iffD1], simp)
 apply (case_tac "x=UU", simp)
 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
 apply (erule_tac x="y" in allE, auto)
-apply (simp_all add: not_less iSuc_Fin)
+apply (simp_all add: not_less iSuc_enat)
 apply (case_tac "#y") apply simp_all
 apply (case_tac "x=UU", simp)
 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
 apply (erule_tac x="y" in allE, simp)
 apply (case_tac "#y") by simp_all
 
-lemma slen_take_eq_rev: "(#x <= Fin n) = (stream_take n\<cdot>x = x)"
+lemma slen_take_eq_rev: "(#x <= enat n) = (stream_take n\<cdot>x = x)"
 by (simp add: linorder_not_less [symmetric] slen_take_eq)
 
-lemma slen_take_lemma1: "#x = Fin n ==> stream_take n\<cdot>x = x"
+lemma slen_take_lemma1: "#x = enat n ==> stream_take n\<cdot>x = x"
 by (rule slen_take_eq_rev [THEN iffD1], auto)
 
 lemma slen_rt_mono: "#s2 <= #s1 ==> #(rt$s2) <= #(rt$s1)"
 apply (cases s1)
  by (cases s2, simp+)+
 
-lemma slen_take_lemma5: "#(stream_take n$s) <= Fin n"
+lemma slen_take_lemma5: "#(stream_take n$s) <= enat n"
 apply (case_tac "stream_take n$s = s")
  apply (simp add: slen_take_eq_rev)
 by (simp add: slen_take_lemma4)
 
-lemma slen_take_lemma2: "!x. ~stream_finite x --> #(stream_take i\<cdot>x) = Fin i"
+lemma slen_take_lemma2: "!x. ~stream_finite x --> #(stream_take i\<cdot>x) = enat i"
 apply (simp add: stream.finite_def, auto)
 by (simp add: slen_take_lemma4)
 
@@ -443,16 +443,16 @@
 lemma iterate_lemma: "F$(iterate n$F$x) = iterate n$F$(F$x)"
 by (insert iterate_Suc2 [of n F x], auto)
 
-lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i$rt$x)"
+lemma slen_rt_mult [rule_format]: "!x. enat (i + j) <= #x --> enat j <= #(iterate i$rt$x)"
 apply (induct i, auto)
 apply (case_tac "x=UU", auto simp add: zero_enat_def)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (erule_tac x="y" in allE, auto)
-apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_Fin)
+apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_enat)
 by (simp add: iterate_lemma)
 
 lemma slen_take_lemma3 [rule_format]:
-  "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> stream_take n\<cdot>x = stream_take n\<cdot>y"
+  "!(x::'a::flat stream) y. enat n <= #x --> x << y --> stream_take n\<cdot>x = stream_take n\<cdot>y"
 apply (induct_tac n, auto)
 apply (case_tac "x=UU", auto)
 apply (simp add: zero_enat_def)
@@ -478,7 +478,7 @@
 apply (subgoal_tac "stream_take n$s ~=s")
  apply (insert slen_take_lemma4 [of n s],auto)
 apply (cases s, simp)
-by (simp add: slen_take_lemma4 iSuc_Fin)
+by (simp add: slen_take_lemma4 iSuc_enat)
 
 (* ----------------------------------------------------------------------- *)
 (* theorems about smap                                                     *)
@@ -546,7 +546,7 @@
 lemma i_rt_mono: "x << s ==> i_rt n x  << i_rt n s"
 by (simp add: i_rt_def monofun_rt_mult)
 
-lemma i_rt_ij_lemma: "Fin (i + j) <= #x ==> Fin j <= #(i_rt i x)"
+lemma i_rt_ij_lemma: "enat (i + j) <= #x ==> enat j <= #(i_rt i x)"
 by (simp add: i_rt_def slen_rt_mult)
 
 lemma slen_i_rt_mono: "#s2 <= #s1 ==> #(i_rt n s2) <= #(i_rt n s1)"
@@ -573,7 +573,7 @@
   apply (simp_all add: zero_enat_def)
   done
 
-lemma i_rt_lemma_slen: "#s=Fin n ==> i_rt n s = UU"
+lemma i_rt_lemma_slen: "#s=enat n ==> i_rt n s = UU"
 by (simp add: i_rt_slen slen_take_lemma1)
 
 lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s"
@@ -581,15 +581,15 @@
  apply (cases s, auto simp del: i_rt_Suc)
 by (simp add: i_rt_Suc_back stream_finite_rt_eq)+
 
-lemma take_i_rt_len_lemma: "ALL sl x j t. Fin sl = #x & n <= sl &
-                            #(stream_take n$x) = Fin t & #(i_rt n x)= Fin j
-                                              --> Fin (j + t) = #x"
+lemma take_i_rt_len_lemma: "ALL sl x j t. enat sl = #x & n <= sl &
+                            #(stream_take n$x) = enat t & #(i_rt n x)= enat j
+                                              --> enat (j + t) = #x"
 apply (induct n, auto)
  apply (simp add: zero_enat_def)
 apply (case_tac "x=UU",auto)
  apply (simp add: zero_enat_def)
 apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
-apply (subgoal_tac "EX k. Fin k = #y",clarify)
+apply (subgoal_tac "EX k. enat k = #y",clarify)
  apply (erule_tac x="k" in allE)
  apply (erule_tac x="y" in allE,auto)
  apply (erule_tac x="THE p. Suc p = t" in allE,auto)
@@ -602,8 +602,8 @@
 done
 
 lemma take_i_rt_len:
-"[| Fin sl = #x; n <= sl; #(stream_take n$x) = Fin t; #(i_rt n x) = Fin j |] ==>
-    Fin (j + t) = #x"
+"[| enat sl = #x; n <= sl; #(stream_take n$x) = enat t; #(i_rt n x) = enat j |] ==>
+    enat (j + t) = #x"
 by (blast intro: take_i_rt_len_lemma [rule_format])
 
 
@@ -704,7 +704,7 @@
 by (drule stream_exhaust_eq [THEN iffD1],auto)
 
 lemma ex_sconc [rule_format]:
-  "ALL k y. #x = Fin k --> (EX w. stream_take k$w = x & i_rt k w = y)"
+  "ALL k y. #x = enat k --> (EX w. stream_take k$w = x & i_rt k w = y)"
 apply (case_tac "#x")
  apply (rule stream_finite_ind [of x],auto)
   apply (simp add: stream.finite_def)
@@ -713,12 +713,12 @@
 apply (erule_tac x="y" in allE,auto)
 by (rule_tac x="a && w" in exI,auto)
 
-lemma rt_sconc1: "Fin n = #x ==> i_rt n (x ooo y) = y"
+lemma rt_sconc1: "enat n = #x ==> i_rt n (x ooo y) = y"
 apply (simp add: sconc_def split: enat.splits, arith?,auto)
 apply (rule someI2_ex,auto)
 by (drule ex_sconc,simp)
 
-lemma sconc_inj2: "\<lbrakk>Fin n = #x; x ooo y = x ooo z\<rbrakk> \<Longrightarrow> y = z"
+lemma sconc_inj2: "\<lbrakk>enat n = #x; x ooo y = x ooo z\<rbrakk> \<Longrightarrow> y = z"
 apply (frule_tac y=y in rt_sconc1)
 by (auto elim: rt_sconc1)
 
@@ -734,7 +734,7 @@
  apply (simp add: i_rt_slen)
 by (simp add: sconc_def)
 
-lemma stream_take_sconc [simp]: "Fin n = #x ==> stream_take n$(x ooo y) = x"
+lemma stream_take_sconc [simp]: "enat n = #x ==> stream_take n$(x ooo y) = x"
 apply (simp add: sconc_def)
 apply (cases "#x")
 apply auto
@@ -743,7 +743,7 @@
 
 lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y"
 apply (cases "#x",auto)
- apply (simp add: sconc_def iSuc_Fin)
+ apply (simp add: sconc_def iSuc_enat)
  apply (rule someI2_ex)
   apply (drule ex_sconc, simp)
  apply (rule someI2_ex, auto)
@@ -799,9 +799,9 @@
 by (cases s, auto)
 
 lemma i_th_sconc_lemma [rule_format]:
-  "ALL x y. Fin n < #x --> i_th n (x ooo y) = i_th n x"
+  "ALL x y. enat n < #x --> i_th n (x ooo y) = i_th n x"
 apply (induct_tac n, auto)
-apply (simp add: Fin_0 i_th_def)
+apply (simp add: enat_0 i_th_def)
 apply (simp add: slen_empty_eq ft_sconc)
 apply (simp add: i_th_def)
 apply (case_tac "x=UU",auto)
@@ -849,7 +849,7 @@
 (* ----------------------------------------------------------------------- *)
 
 lemma slen_sconc_finite1:
-  "[| #(x ooo y) = \<infinity>; Fin n = #x |] ==> #y = \<infinity>"
+  "[| #(x ooo y) = \<infinity>; enat n = #x |] ==> #y = \<infinity>"
 apply (case_tac "#y ~= \<infinity>",auto)
 apply (drule_tac y=y in rt_sconc1)
 apply (insert stream_finite_i_rt [of n "x ooo y"])
@@ -877,7 +877,7 @@
 
 (* ----------------------------------------------------------------------- *)
 
-lemma slen_sconc_mono3: "[| Fin n = #x; Fin k = #(x ooo y) |] ==> n <= k"
+lemma slen_sconc_mono3: "[| enat n = #x; enat k = #(x ooo y) |] ==> n <= k"
 apply (insert slen_mono [of "x" "x ooo y"])
 apply (cases "#x") apply simp_all
 apply (cases "#(x ooo y)") apply simp_all
@@ -887,10 +887,10 @@
    subsection "finite slen"
 (* ----------------------------------------------------------------------- *)
 
-lemma slen_sconc: "[| Fin n = #x; Fin m = #y |] ==> #(x ooo y) = Fin (n + m)"
+lemma slen_sconc: "[| enat n = #x; enat m = #y |] ==> #(x ooo y) = enat (n + m)"
 apply (case_tac "#(x ooo y)")
  apply (frule_tac y=y in rt_sconc1)
- apply (insert take_i_rt_len [of "THE j. Fin j = #(x ooo y)" "x ooo y" n n m],simp)
+ apply (insert take_i_rt_len [of "THE j. enat j = #(x ooo y)" "x ooo y" n n m],simp)
  apply (insert slen_sconc_mono3 [of n x _ y],simp)
 by (insert sconc_finite [of x y],auto)
 
@@ -956,7 +956,7 @@
   defer 1
   apply (simp add: constr_sconc_def del: scons_sconc)
   apply (case_tac "#s")
-   apply (simp add: iSuc_Fin)
+   apply (simp add: iSuc_enat)
    apply (case_tac "a=UU",auto simp del: scons_sconc)
    apply (simp)
   apply (simp add: sconc_def)
diff -r ab93d0190a5d -r 1165fe965da8 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:38:29 2011 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:38:48 2011 +0200
@@ -27,8 +27,8 @@
 
 typedef (open) enat = "UNIV :: nat option set" ..
  
-definition Fin :: "nat \<Rightarrow> enat" where
-  "Fin n = Abs_enat (Some n)"
+definition enat :: "nat \<Rightarrow> enat" where
+  "enat n = Abs_enat (Some n)"
  
 instantiation enat :: infinity
 begin
@@ -36,27 +36,27 @@
   instance proof qed
 end
  
-rep_datatype Fin "\<infinity> :: enat"
+rep_datatype enat "\<infinity> :: enat"
 proof -
-  fix P i assume "\<And>j. P (Fin j)" "P \<infinity>"
+  fix P i assume "\<And>j. P (enat j)" "P \<infinity>"
   then show "P i"
   proof induct
     case (Abs_enat y) then show ?case
       by (cases y rule: option.exhaust)
-         (auto simp: Fin_def infinity_enat_def)
+         (auto simp: enat_def infinity_enat_def)
   qed
-qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject)
+qed (auto simp add: enat_def infinity_enat_def Abs_enat_inject)
 
-declare [[coercion "Fin::nat\<Rightarrow>enat"]]
+declare [[coercion "enat::nat\<Rightarrow>enat"]]
 
-lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)"
+lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
 by (cases x) auto
 
-lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = \<infinity>)"
+lemma not_enat_eq [iff]: "(ALL y. x ~= enat y) = (x = \<infinity>)"
 by (cases x) auto
 
-primrec the_Fin :: "enat \<Rightarrow> nat"
-where "the_Fin (Fin n) = n"
+primrec the_enat :: "enat \<Rightarrow> nat"
+where "the_enat (enat n) = n"
 
 subsection {* Constructors and numbers *}
 
@@ -64,28 +64,28 @@
 begin
 
 definition
-  "0 = Fin 0"
+  "0 = enat 0"
 
 definition
-  [code_unfold]: "1 = Fin 1"
+  [code_unfold]: "1 = enat 1"
 
 definition
-  [code_unfold, code del]: "number_of k = Fin (number_of k)"
+  [code_unfold, code del]: "number_of k = enat (number_of k)"
 
 instance ..
 
 end
 
 definition iSuc :: "enat \<Rightarrow> enat" where
-  "iSuc i = (case i of Fin n \<Rightarrow> Fin (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
+  "iSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
 
-lemma Fin_0: "Fin 0 = 0"
+lemma enat_0: "enat 0 = 0"
   by (simp add: zero_enat_def)
 
-lemma Fin_1: "Fin 1 = 1"
+lemma enat_1: "enat 1 = 1"
   by (simp add: one_enat_def)
 
-lemma Fin_number: "Fin (number_of k) = number_of k"
+lemma enat_number: "enat (number_of k) = number_of k"
   by (simp add: number_of_enat_def)
 
 lemma one_iSuc: "1 = iSuc 0"
@@ -124,11 +124,11 @@
 lemma number_ne_Infty [simp]: "number_of k \<noteq> (\<infinity>::enat)"
   by (simp add: number_of_enat_def)
 
-lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)"
+lemma iSuc_enat: "iSuc (enat n) = enat (Suc n)"
   by (simp add: iSuc_def)
 
-lemma iSuc_number_of: "iSuc (number_of k) = Fin (Suc (number_of k))"
-  by (simp add: iSuc_Fin number_of_enat_def)
+lemma iSuc_number_of: "iSuc (number_of k) = enat (Suc (number_of k))"
+  by (simp add: iSuc_enat number_of_enat_def)
 
 lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
   by (simp add: iSuc_def)
@@ -153,11 +153,11 @@
 begin
 
 definition [nitpick_simp]:
-  "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
+  "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | enat m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | enat n \<Rightarrow> enat (m + n)))"
 
 lemma plus_enat_simps [simp, code]:
   fixes q :: enat
-  shows "Fin m + Fin n = Fin (m + n)"
+  shows "enat m + enat n = enat (m + n)"
     and "\<infinity> + q = \<infinity>"
     and "q + \<infinity> = \<infinity>"
   by (simp_all add: plus_enat_def split: enat.splits)
@@ -182,7 +182,7 @@
 lemma plus_enat_number [simp]:
   "(number_of k \<Colon> enat) + number_of l = (if k < Int.Pls then number_of l
     else if l < Int.Pls then number_of k else number_of (k + l))"
-  unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
+  unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ enat] ..
 
 lemma iSuc_number [simp]:
   "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
@@ -191,7 +191,7 @@
 
 lemma iSuc_plus_1:
   "iSuc n = n + 1"
-  by (cases n) (simp_all add: iSuc_Fin one_enat_def)
+  by (cases n) (simp_all add: iSuc_enat one_enat_def)
   
 lemma plus_1_iSuc:
   "1 + q = iSuc q"
@@ -213,14 +213,14 @@
 begin
 
 definition times_enat_def [nitpick_simp]:
-  "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
-    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
+  "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | enat m \<Rightarrow>
+    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | enat n \<Rightarrow> enat (m * n)))"
 
 lemma times_enat_simps [simp, code]:
-  "Fin m * Fin n = Fin (m * n)"
+  "enat m * enat n = enat (m * n)"
   "\<infinity> * \<infinity> = (\<infinity>::enat)"
-  "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
-  "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
+  "\<infinity> * enat n = (if n = 0 then 0 else \<infinity>)"
+  "enat m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
   unfolding times_enat_def zero_enat_def
   by (simp_all split: enat.split)
 
@@ -257,21 +257,21 @@
 lemma mult_iSuc_right: "m * iSuc n = m + m * n"
   unfolding iSuc_plus_1 by (simp add: algebra_simps)
 
-lemma of_nat_eq_Fin: "of_nat n = Fin n"
+lemma of_nat_eq_enat: "of_nat n = enat n"
   apply (induct n)
-  apply (simp add: Fin_0)
-  apply (simp add: plus_1_iSuc iSuc_Fin)
+  apply (simp add: enat_0)
+  apply (simp add: plus_1_iSuc iSuc_enat)
   done
 
 instance enat :: number_semiring
 proof
   fix n show "number_of (int n) = (of_nat n :: enat)"
-    unfolding number_of_enat_def number_of_int of_nat_id of_nat_eq_Fin ..
+    unfolding number_of_enat_def number_of_int of_nat_id of_nat_eq_enat ..
 qed
 
 instance enat :: semiring_char_0 proof
-  have "inj Fin" by (rule injI) simp
-  then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_Fin)
+  have "inj enat" by (rule injI) simp
+  then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
 qed
 
 lemma imult_is_0[simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
@@ -287,31 +287,31 @@
 begin
 
 definition diff_enat_def:
-"a - b = (case a of (Fin x) \<Rightarrow> (case b of (Fin y) \<Rightarrow> Fin (x - y) | \<infinity> \<Rightarrow> 0)
+"a - b = (case a of (enat x) \<Rightarrow> (case b of (enat y) \<Rightarrow> enat (x - y) | \<infinity> \<Rightarrow> 0)
           | \<infinity> \<Rightarrow> \<infinity>)"
 
 instance ..
 
 end
 
-lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)"
+lemma idiff_enat_enat[simp,code]: "enat a - enat b = enat (a - b)"
 by(simp add: diff_enat_def)
 
 lemma idiff_Infty[simp,code]: "\<infinity> - n = (\<infinity>::enat)"
 by(simp add: diff_enat_def)
 
-lemma idiff_Infty_right[simp,code]: "Fin a - \<infinity> = 0"
+lemma idiff_Infty_right[simp,code]: "enat a - \<infinity> = 0"
 by(simp add: diff_enat_def)
 
 lemma idiff_0[simp]: "(0::enat) - n = 0"
 by (cases n, simp_all add: zero_enat_def)
 
-lemmas idiff_Fin_0[simp] = idiff_0[unfolded zero_enat_def]
+lemmas idiff_enat_0[simp] = idiff_0[unfolded zero_enat_def]
 
 lemma idiff_0_right[simp]: "(n::enat) - 0 = n"
 by (cases n) (simp_all add: zero_enat_def)
 
-lemmas idiff_Fin_0_right[simp] = idiff_0_right[unfolded zero_enat_def]
+lemmas idiff_enat_0_right[simp] = idiff_0_right[unfolded zero_enat_def]
 
 lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
 by(auto simp: zero_enat_def)
@@ -320,9 +320,9 @@
 by(simp add: iSuc_def split: enat.split)
 
 lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n"
-by(simp add: one_enat_def iSuc_Fin[symmetric] zero_enat_def[symmetric])
+by(simp add: one_enat_def iSuc_enat[symmetric] zero_enat_def[symmetric])
 
-(*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_enat_def]*)
+(*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*)
 
 subsection {* Ordering *}
 
@@ -330,16 +330,16 @@
 begin
 
 definition [nitpick_simp]:
-  "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
+  "m \<le> n = (case n of enat n1 \<Rightarrow> (case m of enat m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
     | \<infinity> \<Rightarrow> True)"
 
 definition [nitpick_simp]:
-  "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
+  "m < n = (case m of enat m1 \<Rightarrow> (case n of enat n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
     | \<infinity> \<Rightarrow> False)"
 
 lemma enat_ord_simps [simp]:
-  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
-  "Fin m < Fin n \<longleftrightarrow> m < n"
+  "enat m \<le> enat n \<longleftrightarrow> m \<le> n"
+  "enat m < enat n \<longleftrightarrow> m < n"
   "q \<le> (\<infinity>::enat)"
   "q < (\<infinity>::enat) \<longleftrightarrow> q \<noteq> \<infinity>"
   "(\<infinity>::enat) \<le> q \<longleftrightarrow> q = \<infinity>"
@@ -347,11 +347,11 @@
   by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)
 
 lemma enat_ord_code [code]:
-  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
-  "Fin m < Fin n \<longleftrightarrow> m < n"
+  "enat m \<le> enat n \<longleftrightarrow> m \<le> n"
+  "enat m < enat n \<longleftrightarrow> m < n"
   "q \<le> (\<infinity>::enat) \<longleftrightarrow> True"
-  "Fin m < \<infinity> \<longleftrightarrow> True"
-  "\<infinity> \<le> Fin n \<longleftrightarrow> False"
+  "enat m < \<infinity> \<longleftrightarrow> True"
+  "\<infinity> \<le> enat n \<longleftrightarrow> False"
   "(\<infinity>::enat) < q \<longleftrightarrow> False"
   by simp_all
 
@@ -380,10 +380,10 @@
 lemma ile0_eq [simp]: "n \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0"
 by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
 
-lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m \<Longrightarrow> R"
+lemma Infty_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
   by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
 
-lemma Infty_ilessE [elim!]: "\<infinity> < Fin m \<Longrightarrow> R"
+lemma Infty_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
   by simp
 
 lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)"
@@ -413,10 +413,10 @@
 lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
   by (simp add: iSuc_def less_eq_enat_def less_enat_def split: enat.splits)
 
-lemma Suc_ile_eq: "Fin (Suc m) \<le> n \<longleftrightarrow> Fin m < n"
+lemma Suc_ile_eq: "enat (Suc m) \<le> n \<longleftrightarrow> enat m < n"
   by (cases n) auto
 
-lemma iless_Suc_eq [simp]: "Fin m < iSuc n \<longleftrightarrow> Fin m \<le> n"
+lemma iless_Suc_eq [simp]: "enat m < iSuc n \<longleftrightarrow> enat m \<le> n"
   by (auto simp add: iSuc_def less_enat_def split: enat.splits)
 
 lemma imult_Infty: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
@@ -433,7 +433,7 @@
 
 
 lemma min_enat_simps [simp]:
-  "min (Fin m) (Fin n) = Fin (min m n)"
+  "min (enat m) (enat n) = enat (min m n)"
   "min q 0 = 0"
   "min 0 q = 0"
   "min q (\<infinity>::enat) = q"
@@ -441,28 +441,28 @@
   by (auto simp add: min_def)
 
 lemma max_enat_simps [simp]:
-  "max (Fin m) (Fin n) = Fin (max m n)"
+  "max (enat m) (enat n) = enat (max m n)"
   "max q 0 = q"
   "max 0 q = q"
   "max q \<infinity> = (\<infinity>::enat)"
   "max \<infinity> q = (\<infinity>::enat)"
   by (simp_all add: max_def)
 
-lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k"
+lemma enat_ile: "n \<le> enat m \<Longrightarrow> \<exists>k. n = enat k"
   by (cases n) simp_all
 
-lemma Fin_iless: "n < Fin m \<Longrightarrow> \<exists>k. n = Fin k"
+lemma enat_iless: "n < enat m \<Longrightarrow> \<exists>k. n = enat k"
   by (cases n) simp_all
 
-lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
+lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. enat k < Y j"
 apply (induct_tac k)
- apply (simp (no_asm) only: Fin_0)
+ apply (simp (no_asm) only: enat_0)
  apply (fast intro: le_less_trans [OF i0_lb])
 apply (erule exE)
 apply (drule spec)
 apply (erule exE)
 apply (drule ileI1)
-apply (rule iSuc_Fin [THEN subst])
+apply (rule iSuc_enat [THEN subst])
 apply (rule exI)
 apply (erule (1) le_less_trans)
 done
@@ -481,46 +481,46 @@
 
 end
 
-lemma finite_Fin_bounded:
-  assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> Fin n"
+lemma finite_enat_bounded:
+  assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> enat n"
   shows "finite A"
 proof (rule finite_subset)
-  show "finite (Fin ` {..n})" by blast
+  show "finite (enat ` {..n})" by blast
 
-  have "A \<subseteq> {..Fin n}" using le_fin by fastsimp
-  also have "\<dots> \<subseteq> Fin ` {..n}"
+  have "A \<subseteq> {..enat n}" using le_fin by fastsimp
+  also have "\<dots> \<subseteq> enat ` {..n}"
     by (rule subsetI) (case_tac x, auto)
-  finally show "A \<subseteq> Fin ` {..n}" .
+  finally show "A \<subseteq> enat ` {..n}" .
 qed
 
 
 subsection {* Well-ordering *}
 
-lemma less_FinE:
-  "[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P"
+lemma less_enatE:
+  "[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P"
 by (induct n) auto
 
 lemma less_InftyE:
-  "[| n < \<infinity>; !!k. n = Fin k ==> P |] ==> P"
+  "[| n < \<infinity>; !!k. n = enat k ==> P |] ==> P"
 by (induct n) auto
 
 lemma enat_less_induct:
   assumes prem: "!!n. \<forall>m::enat. m < n --> P m ==> P n" shows "P n"
 proof -
-  have P_Fin: "!!k. P (Fin k)"
+  have P_enat: "!!k. P (enat k)"
     apply (rule nat_less_induct)
     apply (rule prem, clarify)
-    apply (erule less_FinE, simp)
+    apply (erule less_enatE, simp)
     done
   show ?thesis
   proof (induct n)
     fix nat
-    show "P (Fin nat)" by (rule P_Fin)
+    show "P (enat nat)" by (rule P_enat)
   next
     show "P \<infinity>"
       apply (rule prem, clarify)
       apply (erule less_InftyE)
-      apply (simp add: P_Fin)
+      apply (simp add: P_enat)
       done
   qed
 qed
@@ -560,7 +560,7 @@
   { assume "x \<in> A" then show "x \<le> Sup A"
       unfolding Sup_enat_def by (cases "finite A") auto }
   { assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
-      unfolding Sup_enat_def using finite_Fin_bounded by auto }
+      unfolding Sup_enat_def using finite_enat_bounded by auto }
 qed (simp_all add: inf_enat_def sup_enat_def)
 end
 
diff -r ab93d0190a5d -r 1165fe965da8 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Jul 19 14:38:29 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Tue Jul 19 14:38:48 2011 +0200
@@ -55,7 +55,7 @@
   instance ..
 end
 
-definition "ereal_of_enat n = (case n of Fin n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
+definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
 
 declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
 declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]