--- 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>
--- 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
--- 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)
--- 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)
--- 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)
--- 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
--- 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"]]