rename Fin to enat
authorhoelzl
Tue Jul 19 14:38:48 2011 +0200 (2011-07-19)
changeset 439241165fe965da8
parent 43923 ab93d0190a5d
child 43925 f651cb053927
rename Fin to enat
src/HOL/HOLCF/FOCUS/Buffer_adm.thy
src/HOL/HOLCF/FOCUS/Fstream.thy
src/HOL/HOLCF/FOCUS/Fstreams.thy
src/HOL/HOLCF/FOCUS/Stream_adm.thy
src/HOL/HOLCF/Library/Stream.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Extended_Real.thy
     1.1 --- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Tue Jul 19 14:38:29 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Tue Jul 19 14:38:48 2011 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Buffer Stream_adm
     1.5  begin
     1.6  
     1.7 -declare Fin_0 [simp]
     1.8 +declare enat_0 [simp]
     1.9  
    1.10  lemma BufAC_Asm_d2: "a\<leadsto>s:BufAC_Asm ==> ? d. a=Md d"
    1.11  by (drule BufAC_Asm_unfold [THEN iffD1], auto)
    1.12 @@ -116,7 +116,7 @@
    1.13  done
    1.14  
    1.15  (*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
    1.16 -lemma BufAC_Cmt_2stream_monoP: "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> 
    1.17 +lemma BufAC_Cmt_2stream_monoP: "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> enat (l i) < #x --> 
    1.18                       (x,f\<cdot>x):down_iterate BufAC_Cmt_F i --> 
    1.19                       (s,f\<cdot>s):down_iterate BufAC_Cmt_F i"
    1.20  apply (rule_tac x="%i. 2*i" in exI)
    1.21 @@ -139,10 +139,10 @@
    1.22         \<lbrakk>f \<in> BufEq;
    1.23            \<forall>x s. s \<in> BufAC_Asm \<longrightarrow>
    1.24                  x \<sqsubseteq> s \<longrightarrow>
    1.25 -                Fin (2 * i) < #x \<longrightarrow>
    1.26 +                enat (2 * i) < #x \<longrightarrow>
    1.27                  (x, f\<cdot>x) \<in> down_iterate BufAC_Cmt_F i \<longrightarrow>
    1.28                  (s, f\<cdot>s) \<in> down_iterate BufAC_Cmt_F i;
    1.29 -          Md d\<leadsto>\<bullet>\<leadsto>xa \<in> BufAC_Asm; Fin (2 * i) < #ya; f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>t;
    1.30 +          Md d\<leadsto>\<bullet>\<leadsto>xa \<in> BufAC_Asm; enat (2 * i) < #ya; f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>t;
    1.31            (ya, t) \<in> down_iterate BufAC_Cmt_F i; ya \<sqsubseteq> xa\<rbrakk>
    1.32         \<Longrightarrow> (xa, rt\<cdot>(f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>xa))) \<in> down_iterate BufAC_Cmt_F i
    1.33  *)
    1.34 @@ -158,11 +158,11 @@
    1.35  apply (erule subst)
    1.36  (*
    1.37   1. \<And>i d xa ya t ff ffa.
    1.38 -       \<lbrakk>f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya; Fin (2 * i) < #ya;
    1.39 +       \<lbrakk>f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya; enat (2 * i) < #ya;
    1.40            (ya, ffa\<cdot>ya) \<in> down_iterate BufAC_Cmt_F i; ya \<sqsubseteq> xa; f \<in> BufEq;
    1.41            \<forall>x s. s \<in> BufAC_Asm \<longrightarrow>
    1.42                  x \<sqsubseteq> s \<longrightarrow>
    1.43 -                Fin (2 * i) < #x \<longrightarrow>
    1.44 +                enat (2 * i) < #x \<longrightarrow>
    1.45                  (x, f\<cdot>x) \<in> down_iterate BufAC_Cmt_F i \<longrightarrow>
    1.46                  (s, f\<cdot>s) \<in> down_iterate BufAC_Cmt_F i;
    1.47            xa \<in> BufAC_Asm; ff \<in> BufEq; ffa \<in> BufEq\<rbrakk>
     2.1 --- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Tue Jul 19 14:38:29 2011 +0200
     2.2 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Tue Jul 19 14:38:48 2011 +0200
     2.3 @@ -144,13 +144,13 @@
     2.4  by (simp add: fscons_def)
     2.5  
     2.6  lemma slen_fscons_eq:
     2.7 -        "(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)"
     2.8 +        "(enat (Suc n) < #x) = (? a y. x = a~> y & enat n < #y)"
     2.9  apply (simp add: fscons_def2 slen_scons_eq)
    2.10  apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
    2.11  done
    2.12  
    2.13  lemma slen_fscons_eq_rev:
    2.14 -        "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))"
    2.15 +        "(#x < enat (Suc (Suc n))) = (!a y. x ~= a~> y | #y < enat (Suc n))"
    2.16  apply (simp add: fscons_def2 slen_scons_eq_rev)
    2.17  apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
    2.18  apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
    2.19 @@ -163,7 +163,7 @@
    2.20  done
    2.21  
    2.22  lemma slen_fscons_less_eq:
    2.23 -        "(#(a~> y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))"
    2.24 +        "(#(a~> y) < enat (Suc (Suc n))) = (#y < enat (Suc n))"
    2.25  apply (subst slen_fscons_eq_rev)
    2.26  apply (fast dest!: fscons_inject [THEN iffD1])
    2.27  done
     3.1 --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jul 19 14:38:29 2011 +0200
     3.2 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jul 19 14:38:48 2011 +0200
     3.3 @@ -28,7 +28,7 @@
     3.4  
     3.5  definition
     3.6    jth           :: "nat => 'a fstream => 'a" where
     3.7 -  "jth = (%n s. if Fin n < #s then THE a. i_th n s = Def a else undefined)"
     3.8 +  "jth = (%n s. if enat n < #s then THE a. i_th n s = Def a else undefined)"
     3.9  
    3.10  definition
    3.11    first         :: "'a fstream => 'a" where
    3.12 @@ -36,7 +36,7 @@
    3.13  
    3.14  definition
    3.15    last          :: "'a fstream => 'a" where
    3.16 -  "last = (%s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else undefined))"
    3.17 +  "last = (%s. case #s of enat n => (if n~=0 then jth (THE k. Suc k = n) s else undefined))"
    3.18  
    3.19  
    3.20  abbreviation
    3.21 @@ -54,7 +54,7 @@
    3.22  lemma ft_fsingleton[simp]: "ft$(<a>) = Def a"
    3.23  by (simp add: fsingleton_def2)
    3.24  
    3.25 -lemma slen_fsingleton[simp]: "#(<a>) = Fin 1"
    3.26 +lemma slen_fsingleton[simp]: "#(<a>) = enat 1"
    3.27  by (simp add: fsingleton_def2 enat_defs)
    3.28  
    3.29  lemma slen_fstreams[simp]: "#(<a> ooo s) = iSuc (#s)"
    3.30 @@ -62,17 +62,17 @@
    3.31  
    3.32  lemma slen_fstreams2[simp]: "#(s ooo <a>) = iSuc (#s)"
    3.33  apply (cases "#s")
    3.34 -apply (auto simp add: iSuc_Fin)
    3.35 +apply (auto simp add: iSuc_enat)
    3.36  apply (insert slen_sconc [of _ s "Suc 0" "<a>"], auto)
    3.37  by (simp add: sconc_def)
    3.38  
    3.39  lemma j_th_0_fsingleton[simp]:"jth 0 (<a>) = a"
    3.40  apply (simp add: fsingleton_def2 jth_def)
    3.41 -by (simp add: i_th_def Fin_0)
    3.42 +by (simp add: i_th_def enat_0)
    3.43  
    3.44  lemma jth_0[simp]: "jth 0 (<a> ooo s) = a"  
    3.45  apply (simp add: fsingleton_def2 jth_def)
    3.46 -by (simp add: i_th_def Fin_0)
    3.47 +by (simp add: i_th_def enat_0)
    3.48  
    3.49  lemma first_sconc[simp]: "first (<a> ooo s) = a"
    3.50  by (simp add: first_def)
    3.51 @@ -80,12 +80,12 @@
    3.52  lemma first_fsingleton[simp]: "first (<a>) = a"
    3.53  by (simp add: first_def)
    3.54  
    3.55 -lemma jth_n[simp]: "Fin n = #s ==> jth n (s ooo <a>) = a"
    3.56 +lemma jth_n[simp]: "enat n = #s ==> jth n (s ooo <a>) = a"
    3.57  apply (simp add: jth_def, auto)
    3.58  apply (simp add: i_th_def rt_sconc1)
    3.59  by (simp add: enat_defs split: enat.splits)
    3.60  
    3.61 -lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a"
    3.62 +lemma last_sconc[simp]: "enat n = #s ==> last (s ooo <a>) = a"
    3.63  apply (simp add: last_def)
    3.64  apply (simp add: enat_defs split:enat.splits)
    3.65  by (drule sym, auto)
    3.66 @@ -102,13 +102,13 @@
    3.67  lemma last_infinite[simp]:"#s = \<infinity> ==> last s = undefined"
    3.68  by (simp add: last_def)
    3.69  
    3.70 -lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
    3.71 +lemma jth_slen_lemma1:"n <= k & enat n = #s ==> jth k s = undefined"
    3.72  by (simp add: jth_def enat_defs split:enat.splits, auto)
    3.73  
    3.74  lemma jth_UU[simp]:"jth n UU = undefined" 
    3.75  by (simp add: jth_def)
    3.76  
    3.77 -lemma ext_last:"[|s ~= UU; Fin (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s" 
    3.78 +lemma ext_last:"[|s ~= UU; enat (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s" 
    3.79  apply (simp add: last_def)
    3.80  apply (case_tac "#s", auto)
    3.81  apply (simp add: fsingleton_def2)
     4.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 19 14:38:29 2011 +0200
     4.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 19 14:38:48 2011 +0200
     4.3 @@ -10,14 +10,14 @@
     4.4  
     4.5  definition
     4.6    stream_monoP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where
     4.7 -  "stream_monoP F = (\<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
     4.8 +  "stream_monoP F = (\<exists>Q i. \<forall>P s. enat i \<le> #s \<longrightarrow>
     4.9                      (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P))"
    4.10  
    4.11  definition
    4.12    stream_antiP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where
    4.13    "stream_antiP F = (\<forall>P x. \<exists>Q i.
    4.14 -                (#x  < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
    4.15 -                (Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
    4.16 +                (#x  < enat i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
    4.17 +                (enat i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
    4.18                  (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P))))"
    4.19  
    4.20  definition
    4.21 @@ -57,7 +57,7 @@
    4.22  lemma flatstream_adm_lemma:
    4.23    assumes 1: "Porder.chain Y"
    4.24    assumes 2: "!i. P (Y i)"
    4.25 -  assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|]
    4.26 +  assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. enat k < #((Y j)::'a::flat stream)|]
    4.27    ==> P(LUB i. Y i))"
    4.28    shows "P(LUB i. Y i)"
    4.29  apply (rule increasing_chain_adm_lemma [of _ P, OF 1 2])
    4.30 @@ -79,7 +79,7 @@
    4.31  
    4.32  (* should be without reference to stream length? *)
    4.33  lemma flatstream_admI: "[|(!!Y. [| Porder.chain Y; !i. P (Y i); 
    4.34 - !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P"
    4.35 + !k. ? j. enat k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P"
    4.36  apply (unfold adm_def)
    4.37  apply (intro strip)
    4.38  apply (erule (1) flatstream_adm_lemma)
    4.39 @@ -88,12 +88,12 @@
    4.40  
    4.41  
    4.42  (* context (theory "Extended_Nat");*)
    4.43 -lemma ile_lemma: "Fin (i + j) <= x ==> Fin i <= x"
    4.44 +lemma ile_lemma: "enat (i + j) <= x ==> enat i <= x"
    4.45    by (rule order_trans) auto
    4.46  
    4.47  lemma stream_monoP2I:
    4.48  "!!X. stream_monoP F ==> !i. ? l. !x y. 
    4.49 -  Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i"
    4.50 +  enat l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i"
    4.51  apply (unfold stream_monoP_def)
    4.52  apply (safe)
    4.53  apply (rule_tac x="i*ia" in exI)
    4.54 @@ -120,7 +120,7 @@
    4.55  done
    4.56  
    4.57  lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y. 
    4.58 - Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;
    4.59 + enat l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;
    4.60      down_cont F |] ==> adm (%x. x:gfp F)"
    4.61  apply (erule INTER_down_iterate_is_gfp [THEN ssubst]) (* cont *)
    4.62  apply (simp (no_asm))
    4.63 @@ -153,7 +153,7 @@
    4.64  apply (intro strip)
    4.65  apply (erule allE, erule all_dupE, erule exE, erule exE)
    4.66  apply (erule conjE)
    4.67 -apply (case_tac "#x < Fin i")
    4.68 +apply (case_tac "#x < enat i")
    4.69  apply ( fast)
    4.70  apply (unfold linorder_not_less)
    4.71  apply (drule (1) mp)
     5.1 --- a/src/HOL/HOLCF/Library/Stream.thy	Tue Jul 19 14:38:29 2011 +0200
     5.2 +++ b/src/HOL/HOLCF/Library/Stream.thy	Tue Jul 19 14:38:48 2011 +0200
     5.3 @@ -23,7 +23,7 @@
     5.4  
     5.5  definition
     5.6    slen :: "'a stream \<Rightarrow> enat"  ("#_" [1000] 1000) where
     5.7 -  "#s = (if stream_finite s then Fin (LEAST n. stream_take n\<cdot>s = s) else \<infinity>)"
     5.8 +  "#s = (if stream_finite s then enat (LEAST n. stream_take n\<cdot>s = s) else \<infinity>)"
     5.9  
    5.10  
    5.11  (* concatenation *)
    5.12 @@ -39,7 +39,7 @@
    5.13  definition
    5.14    sconc :: "'a stream => 'a stream => 'a stream"  (infixr "ooo" 65) where
    5.15    "s1 ooo s2 = (case #s1 of
    5.16 -                  Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
    5.17 +                  enat n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
    5.18                 | \<infinity>     \<Rightarrow> s1)"
    5.19  
    5.20  primrec constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream"
    5.21 @@ -51,7 +51,7 @@
    5.22  definition
    5.23    constr_sconc  :: "'a stream => 'a stream => 'a stream" where (* constructive *)
    5.24    "constr_sconc s1 s2 = (case #s1 of
    5.25 -                          Fin n \<Rightarrow> constr_sconc' n s1 s2
    5.26 +                          enat n \<Rightarrow> constr_sconc' n s1 s2
    5.27                          | \<infinity>    \<Rightarrow> s1)"
    5.28  
    5.29  
    5.30 @@ -332,7 +332,7 @@
    5.31  lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = iSuc (#xs)"
    5.32  apply (case_tac "stream_finite (x && xs)")
    5.33  apply (simp add: slen_def, auto)
    5.34 -apply (simp add: stream.finite_def, auto simp add: iSuc_Fin)
    5.35 +apply (simp add: stream.finite_def, auto simp add: iSuc_enat)
    5.36  apply (rule Least_Suc2, auto)
    5.37  (*apply (drule sym)*)
    5.38  (*apply (drule sym scons_eq_UU [THEN iffD1],simp)*)
    5.39 @@ -340,13 +340,13 @@
    5.40  apply (simp add: slen_def, auto)
    5.41  by (drule stream_finite_lemma1,auto)
    5.42  
    5.43 -lemma slen_less_1_eq: "(#x < Fin (Suc 0)) = (x = \<bottom>)"
    5.44 -by (cases x, auto simp add: Fin_0 iSuc_Fin[THEN sym])
    5.45 +lemma slen_less_1_eq: "(#x < enat (Suc 0)) = (x = \<bottom>)"
    5.46 +by (cases x, auto simp add: enat_0 iSuc_enat[THEN sym])
    5.47  
    5.48  lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)"
    5.49  by (cases x, auto)
    5.50  
    5.51 -lemma slen_scons_eq: "(Fin (Suc n) < #x) = (? a y. x = a && y &  a ~= \<bottom> &  Fin n < #y)"
    5.52 +lemma slen_scons_eq: "(enat (Suc n) < #x) = (? a y. x = a && y &  a ~= \<bottom> &  enat n < #y)"
    5.53  apply (auto, case_tac "x=UU",auto)
    5.54  apply (drule stream_exhaust_eq [THEN iffD1], auto)
    5.55  apply (case_tac "#y") apply simp_all
    5.56 @@ -359,18 +359,18 @@
    5.57  lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \<infinity>"
    5.58  by (simp add: slen_def)
    5.59  
    5.60 -lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < Fin (Suc n))"
    5.61 +lemma slen_scons_eq_rev: "(#x < enat (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < enat (Suc n))"
    5.62   apply (cases x, auto)
    5.63     apply (simp add: zero_enat_def)
    5.64 -  apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
    5.65 - apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
    5.66 +  apply (case_tac "#stream") apply (simp_all add: iSuc_enat)
    5.67 + apply (case_tac "#stream") apply (simp_all add: iSuc_enat)
    5.68  done
    5.69  
    5.70  lemma slen_take_lemma4 [rule_format]:
    5.71 -  "!s. stream_take n$s ~= s --> #(stream_take n$s) = Fin n"
    5.72 -apply (induct n, auto simp add: Fin_0)
    5.73 +  "!s. stream_take n$s ~= s --> #(stream_take n$s) = enat n"
    5.74 +apply (induct n, auto simp add: enat_0)
    5.75  apply (case_tac "s=UU", simp)
    5.76 -by (drule stream_exhaust_eq [THEN iffD1], auto simp add: iSuc_Fin)
    5.77 +by (drule stream_exhaust_eq [THEN iffD1], auto simp add: iSuc_enat)
    5.78  
    5.79  (*
    5.80  lemma stream_take_idempotent [simp]:
    5.81 @@ -390,37 +390,37 @@
    5.82  by (simp add: chain_def,simp)
    5.83  *)
    5.84  
    5.85 -lemma slen_take_eq: "ALL x. (Fin n < #x) = (stream_take n\<cdot>x ~= x)"
    5.86 +lemma slen_take_eq: "ALL x. (enat n < #x) = (stream_take n\<cdot>x ~= x)"
    5.87  apply (induct_tac n, auto)
    5.88 -apply (simp add: Fin_0, clarsimp)
    5.89 +apply (simp add: enat_0, clarsimp)
    5.90  apply (drule not_sym)
    5.91  apply (drule slen_empty_eq [THEN iffD1], simp)
    5.92  apply (case_tac "x=UU", simp)
    5.93  apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
    5.94  apply (erule_tac x="y" in allE, auto)
    5.95 -apply (simp_all add: not_less iSuc_Fin)
    5.96 +apply (simp_all add: not_less iSuc_enat)
    5.97  apply (case_tac "#y") apply simp_all
    5.98  apply (case_tac "x=UU", simp)
    5.99  apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
   5.100  apply (erule_tac x="y" in allE, simp)
   5.101  apply (case_tac "#y") by simp_all
   5.102  
   5.103 -lemma slen_take_eq_rev: "(#x <= Fin n) = (stream_take n\<cdot>x = x)"
   5.104 +lemma slen_take_eq_rev: "(#x <= enat n) = (stream_take n\<cdot>x = x)"
   5.105  by (simp add: linorder_not_less [symmetric] slen_take_eq)
   5.106  
   5.107 -lemma slen_take_lemma1: "#x = Fin n ==> stream_take n\<cdot>x = x"
   5.108 +lemma slen_take_lemma1: "#x = enat n ==> stream_take n\<cdot>x = x"
   5.109  by (rule slen_take_eq_rev [THEN iffD1], auto)
   5.110  
   5.111  lemma slen_rt_mono: "#s2 <= #s1 ==> #(rt$s2) <= #(rt$s1)"
   5.112  apply (cases s1)
   5.113   by (cases s2, simp+)+
   5.114  
   5.115 -lemma slen_take_lemma5: "#(stream_take n$s) <= Fin n"
   5.116 +lemma slen_take_lemma5: "#(stream_take n$s) <= enat n"
   5.117  apply (case_tac "stream_take n$s = s")
   5.118   apply (simp add: slen_take_eq_rev)
   5.119  by (simp add: slen_take_lemma4)
   5.120  
   5.121 -lemma slen_take_lemma2: "!x. ~stream_finite x --> #(stream_take i\<cdot>x) = Fin i"
   5.122 +lemma slen_take_lemma2: "!x. ~stream_finite x --> #(stream_take i\<cdot>x) = enat i"
   5.123  apply (simp add: stream.finite_def, auto)
   5.124  by (simp add: slen_take_lemma4)
   5.125  
   5.126 @@ -443,16 +443,16 @@
   5.127  lemma iterate_lemma: "F$(iterate n$F$x) = iterate n$F$(F$x)"
   5.128  by (insert iterate_Suc2 [of n F x], auto)
   5.129  
   5.130 -lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i$rt$x)"
   5.131 +lemma slen_rt_mult [rule_format]: "!x. enat (i + j) <= #x --> enat j <= #(iterate i$rt$x)"
   5.132  apply (induct i, auto)
   5.133  apply (case_tac "x=UU", auto simp add: zero_enat_def)
   5.134  apply (drule stream_exhaust_eq [THEN iffD1], auto)
   5.135  apply (erule_tac x="y" in allE, auto)
   5.136 -apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_Fin)
   5.137 +apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_enat)
   5.138  by (simp add: iterate_lemma)
   5.139  
   5.140  lemma slen_take_lemma3 [rule_format]:
   5.141 -  "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> stream_take n\<cdot>x = stream_take n\<cdot>y"
   5.142 +  "!(x::'a::flat stream) y. enat n <= #x --> x << y --> stream_take n\<cdot>x = stream_take n\<cdot>y"
   5.143  apply (induct_tac n, auto)
   5.144  apply (case_tac "x=UU", auto)
   5.145  apply (simp add: zero_enat_def)
   5.146 @@ -478,7 +478,7 @@
   5.147  apply (subgoal_tac "stream_take n$s ~=s")
   5.148   apply (insert slen_take_lemma4 [of n s],auto)
   5.149  apply (cases s, simp)
   5.150 -by (simp add: slen_take_lemma4 iSuc_Fin)
   5.151 +by (simp add: slen_take_lemma4 iSuc_enat)
   5.152  
   5.153  (* ----------------------------------------------------------------------- *)
   5.154  (* theorems about smap                                                     *)
   5.155 @@ -546,7 +546,7 @@
   5.156  lemma i_rt_mono: "x << s ==> i_rt n x  << i_rt n s"
   5.157  by (simp add: i_rt_def monofun_rt_mult)
   5.158  
   5.159 -lemma i_rt_ij_lemma: "Fin (i + j) <= #x ==> Fin j <= #(i_rt i x)"
   5.160 +lemma i_rt_ij_lemma: "enat (i + j) <= #x ==> enat j <= #(i_rt i x)"
   5.161  by (simp add: i_rt_def slen_rt_mult)
   5.162  
   5.163  lemma slen_i_rt_mono: "#s2 <= #s1 ==> #(i_rt n s2) <= #(i_rt n s1)"
   5.164 @@ -573,7 +573,7 @@
   5.165    apply (simp_all add: zero_enat_def)
   5.166    done
   5.167  
   5.168 -lemma i_rt_lemma_slen: "#s=Fin n ==> i_rt n s = UU"
   5.169 +lemma i_rt_lemma_slen: "#s=enat n ==> i_rt n s = UU"
   5.170  by (simp add: i_rt_slen slen_take_lemma1)
   5.171  
   5.172  lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s"
   5.173 @@ -581,15 +581,15 @@
   5.174   apply (cases s, auto simp del: i_rt_Suc)
   5.175  by (simp add: i_rt_Suc_back stream_finite_rt_eq)+
   5.176  
   5.177 -lemma take_i_rt_len_lemma: "ALL sl x j t. Fin sl = #x & n <= sl &
   5.178 -                            #(stream_take n$x) = Fin t & #(i_rt n x)= Fin j
   5.179 -                                              --> Fin (j + t) = #x"
   5.180 +lemma take_i_rt_len_lemma: "ALL sl x j t. enat sl = #x & n <= sl &
   5.181 +                            #(stream_take n$x) = enat t & #(i_rt n x)= enat j
   5.182 +                                              --> enat (j + t) = #x"
   5.183  apply (induct n, auto)
   5.184   apply (simp add: zero_enat_def)
   5.185  apply (case_tac "x=UU",auto)
   5.186   apply (simp add: zero_enat_def)
   5.187  apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
   5.188 -apply (subgoal_tac "EX k. Fin k = #y",clarify)
   5.189 +apply (subgoal_tac "EX k. enat k = #y",clarify)
   5.190   apply (erule_tac x="k" in allE)
   5.191   apply (erule_tac x="y" in allE,auto)
   5.192   apply (erule_tac x="THE p. Suc p = t" in allE,auto)
   5.193 @@ -602,8 +602,8 @@
   5.194  done
   5.195  
   5.196  lemma take_i_rt_len:
   5.197 -"[| Fin sl = #x; n <= sl; #(stream_take n$x) = Fin t; #(i_rt n x) = Fin j |] ==>
   5.198 -    Fin (j + t) = #x"
   5.199 +"[| enat sl = #x; n <= sl; #(stream_take n$x) = enat t; #(i_rt n x) = enat j |] ==>
   5.200 +    enat (j + t) = #x"
   5.201  by (blast intro: take_i_rt_len_lemma [rule_format])
   5.202  
   5.203  
   5.204 @@ -704,7 +704,7 @@
   5.205  by (drule stream_exhaust_eq [THEN iffD1],auto)
   5.206  
   5.207  lemma ex_sconc [rule_format]:
   5.208 -  "ALL k y. #x = Fin k --> (EX w. stream_take k$w = x & i_rt k w = y)"
   5.209 +  "ALL k y. #x = enat k --> (EX w. stream_take k$w = x & i_rt k w = y)"
   5.210  apply (case_tac "#x")
   5.211   apply (rule stream_finite_ind [of x],auto)
   5.212    apply (simp add: stream.finite_def)
   5.213 @@ -713,12 +713,12 @@
   5.214  apply (erule_tac x="y" in allE,auto)
   5.215  by (rule_tac x="a && w" in exI,auto)
   5.216  
   5.217 -lemma rt_sconc1: "Fin n = #x ==> i_rt n (x ooo y) = y"
   5.218 +lemma rt_sconc1: "enat n = #x ==> i_rt n (x ooo y) = y"
   5.219  apply (simp add: sconc_def split: enat.splits, arith?,auto)
   5.220  apply (rule someI2_ex,auto)
   5.221  by (drule ex_sconc,simp)
   5.222  
   5.223 -lemma sconc_inj2: "\<lbrakk>Fin n = #x; x ooo y = x ooo z\<rbrakk> \<Longrightarrow> y = z"
   5.224 +lemma sconc_inj2: "\<lbrakk>enat n = #x; x ooo y = x ooo z\<rbrakk> \<Longrightarrow> y = z"
   5.225  apply (frule_tac y=y in rt_sconc1)
   5.226  by (auto elim: rt_sconc1)
   5.227  
   5.228 @@ -734,7 +734,7 @@
   5.229   apply (simp add: i_rt_slen)
   5.230  by (simp add: sconc_def)
   5.231  
   5.232 -lemma stream_take_sconc [simp]: "Fin n = #x ==> stream_take n$(x ooo y) = x"
   5.233 +lemma stream_take_sconc [simp]: "enat n = #x ==> stream_take n$(x ooo y) = x"
   5.234  apply (simp add: sconc_def)
   5.235  apply (cases "#x")
   5.236  apply auto
   5.237 @@ -743,7 +743,7 @@
   5.238  
   5.239  lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y"
   5.240  apply (cases "#x",auto)
   5.241 - apply (simp add: sconc_def iSuc_Fin)
   5.242 + apply (simp add: sconc_def iSuc_enat)
   5.243   apply (rule someI2_ex)
   5.244    apply (drule ex_sconc, simp)
   5.245   apply (rule someI2_ex, auto)
   5.246 @@ -799,9 +799,9 @@
   5.247  by (cases s, auto)
   5.248  
   5.249  lemma i_th_sconc_lemma [rule_format]:
   5.250 -  "ALL x y. Fin n < #x --> i_th n (x ooo y) = i_th n x"
   5.251 +  "ALL x y. enat n < #x --> i_th n (x ooo y) = i_th n x"
   5.252  apply (induct_tac n, auto)
   5.253 -apply (simp add: Fin_0 i_th_def)
   5.254 +apply (simp add: enat_0 i_th_def)
   5.255  apply (simp add: slen_empty_eq ft_sconc)
   5.256  apply (simp add: i_th_def)
   5.257  apply (case_tac "x=UU",auto)
   5.258 @@ -849,7 +849,7 @@
   5.259  (* ----------------------------------------------------------------------- *)
   5.260  
   5.261  lemma slen_sconc_finite1:
   5.262 -  "[| #(x ooo y) = \<infinity>; Fin n = #x |] ==> #y = \<infinity>"
   5.263 +  "[| #(x ooo y) = \<infinity>; enat n = #x |] ==> #y = \<infinity>"
   5.264  apply (case_tac "#y ~= \<infinity>",auto)
   5.265  apply (drule_tac y=y in rt_sconc1)
   5.266  apply (insert stream_finite_i_rt [of n "x ooo y"])
   5.267 @@ -877,7 +877,7 @@
   5.268  
   5.269  (* ----------------------------------------------------------------------- *)
   5.270  
   5.271 -lemma slen_sconc_mono3: "[| Fin n = #x; Fin k = #(x ooo y) |] ==> n <= k"
   5.272 +lemma slen_sconc_mono3: "[| enat n = #x; enat k = #(x ooo y) |] ==> n <= k"
   5.273  apply (insert slen_mono [of "x" "x ooo y"])
   5.274  apply (cases "#x") apply simp_all
   5.275  apply (cases "#(x ooo y)") apply simp_all
   5.276 @@ -887,10 +887,10 @@
   5.277     subsection "finite slen"
   5.278  (* ----------------------------------------------------------------------- *)
   5.279  
   5.280 -lemma slen_sconc: "[| Fin n = #x; Fin m = #y |] ==> #(x ooo y) = Fin (n + m)"
   5.281 +lemma slen_sconc: "[| enat n = #x; enat m = #y |] ==> #(x ooo y) = enat (n + m)"
   5.282  apply (case_tac "#(x ooo y)")
   5.283   apply (frule_tac y=y in rt_sconc1)
   5.284 - apply (insert take_i_rt_len [of "THE j. Fin j = #(x ooo y)" "x ooo y" n n m],simp)
   5.285 + apply (insert take_i_rt_len [of "THE j. enat j = #(x ooo y)" "x ooo y" n n m],simp)
   5.286   apply (insert slen_sconc_mono3 [of n x _ y],simp)
   5.287  by (insert sconc_finite [of x y],auto)
   5.288  
   5.289 @@ -956,7 +956,7 @@
   5.290    defer 1
   5.291    apply (simp add: constr_sconc_def del: scons_sconc)
   5.292    apply (case_tac "#s")
   5.293 -   apply (simp add: iSuc_Fin)
   5.294 +   apply (simp add: iSuc_enat)
   5.295     apply (case_tac "a=UU",auto simp del: scons_sconc)
   5.296     apply (simp)
   5.297    apply (simp add: sconc_def)
     6.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:38:29 2011 +0200
     6.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:38:48 2011 +0200
     6.3 @@ -27,8 +27,8 @@
     6.4  
     6.5  typedef (open) enat = "UNIV :: nat option set" ..
     6.6   
     6.7 -definition Fin :: "nat \<Rightarrow> enat" where
     6.8 -  "Fin n = Abs_enat (Some n)"
     6.9 +definition enat :: "nat \<Rightarrow> enat" where
    6.10 +  "enat n = Abs_enat (Some n)"
    6.11   
    6.12  instantiation enat :: infinity
    6.13  begin
    6.14 @@ -36,27 +36,27 @@
    6.15    instance proof qed
    6.16  end
    6.17   
    6.18 -rep_datatype Fin "\<infinity> :: enat"
    6.19 +rep_datatype enat "\<infinity> :: enat"
    6.20  proof -
    6.21 -  fix P i assume "\<And>j. P (Fin j)" "P \<infinity>"
    6.22 +  fix P i assume "\<And>j. P (enat j)" "P \<infinity>"
    6.23    then show "P i"
    6.24    proof induct
    6.25      case (Abs_enat y) then show ?case
    6.26        by (cases y rule: option.exhaust)
    6.27 -         (auto simp: Fin_def infinity_enat_def)
    6.28 +         (auto simp: enat_def infinity_enat_def)
    6.29    qed
    6.30 -qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject)
    6.31 +qed (auto simp add: enat_def infinity_enat_def Abs_enat_inject)
    6.32  
    6.33 -declare [[coercion "Fin::nat\<Rightarrow>enat"]]
    6.34 +declare [[coercion "enat::nat\<Rightarrow>enat"]]
    6.35  
    6.36 -lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)"
    6.37 +lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
    6.38  by (cases x) auto
    6.39  
    6.40 -lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = \<infinity>)"
    6.41 +lemma not_enat_eq [iff]: "(ALL y. x ~= enat y) = (x = \<infinity>)"
    6.42  by (cases x) auto
    6.43  
    6.44 -primrec the_Fin :: "enat \<Rightarrow> nat"
    6.45 -where "the_Fin (Fin n) = n"
    6.46 +primrec the_enat :: "enat \<Rightarrow> nat"
    6.47 +where "the_enat (enat n) = n"
    6.48  
    6.49  subsection {* Constructors and numbers *}
    6.50  
    6.51 @@ -64,28 +64,28 @@
    6.52  begin
    6.53  
    6.54  definition
    6.55 -  "0 = Fin 0"
    6.56 +  "0 = enat 0"
    6.57  
    6.58  definition
    6.59 -  [code_unfold]: "1 = Fin 1"
    6.60 +  [code_unfold]: "1 = enat 1"
    6.61  
    6.62  definition
    6.63 -  [code_unfold, code del]: "number_of k = Fin (number_of k)"
    6.64 +  [code_unfold, code del]: "number_of k = enat (number_of k)"
    6.65  
    6.66  instance ..
    6.67  
    6.68  end
    6.69  
    6.70  definition iSuc :: "enat \<Rightarrow> enat" where
    6.71 -  "iSuc i = (case i of Fin n \<Rightarrow> Fin (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
    6.72 +  "iSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
    6.73  
    6.74 -lemma Fin_0: "Fin 0 = 0"
    6.75 +lemma enat_0: "enat 0 = 0"
    6.76    by (simp add: zero_enat_def)
    6.77  
    6.78 -lemma Fin_1: "Fin 1 = 1"
    6.79 +lemma enat_1: "enat 1 = 1"
    6.80    by (simp add: one_enat_def)
    6.81  
    6.82 -lemma Fin_number: "Fin (number_of k) = number_of k"
    6.83 +lemma enat_number: "enat (number_of k) = number_of k"
    6.84    by (simp add: number_of_enat_def)
    6.85  
    6.86  lemma one_iSuc: "1 = iSuc 0"
    6.87 @@ -124,11 +124,11 @@
    6.88  lemma number_ne_Infty [simp]: "number_of k \<noteq> (\<infinity>::enat)"
    6.89    by (simp add: number_of_enat_def)
    6.90  
    6.91 -lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)"
    6.92 +lemma iSuc_enat: "iSuc (enat n) = enat (Suc n)"
    6.93    by (simp add: iSuc_def)
    6.94  
    6.95 -lemma iSuc_number_of: "iSuc (number_of k) = Fin (Suc (number_of k))"
    6.96 -  by (simp add: iSuc_Fin number_of_enat_def)
    6.97 +lemma iSuc_number_of: "iSuc (number_of k) = enat (Suc (number_of k))"
    6.98 +  by (simp add: iSuc_enat number_of_enat_def)
    6.99  
   6.100  lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
   6.101    by (simp add: iSuc_def)
   6.102 @@ -153,11 +153,11 @@
   6.103  begin
   6.104  
   6.105  definition [nitpick_simp]:
   6.106 -  "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
   6.107 +  "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | enat m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | enat n \<Rightarrow> enat (m + n)))"
   6.108  
   6.109  lemma plus_enat_simps [simp, code]:
   6.110    fixes q :: enat
   6.111 -  shows "Fin m + Fin n = Fin (m + n)"
   6.112 +  shows "enat m + enat n = enat (m + n)"
   6.113      and "\<infinity> + q = \<infinity>"
   6.114      and "q + \<infinity> = \<infinity>"
   6.115    by (simp_all add: plus_enat_def split: enat.splits)
   6.116 @@ -182,7 +182,7 @@
   6.117  lemma plus_enat_number [simp]:
   6.118    "(number_of k \<Colon> enat) + number_of l = (if k < Int.Pls then number_of l
   6.119      else if l < Int.Pls then number_of k else number_of (k + l))"
   6.120 -  unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
   6.121 +  unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ enat] ..
   6.122  
   6.123  lemma iSuc_number [simp]:
   6.124    "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
   6.125 @@ -191,7 +191,7 @@
   6.126  
   6.127  lemma iSuc_plus_1:
   6.128    "iSuc n = n + 1"
   6.129 -  by (cases n) (simp_all add: iSuc_Fin one_enat_def)
   6.130 +  by (cases n) (simp_all add: iSuc_enat one_enat_def)
   6.131    
   6.132  lemma plus_1_iSuc:
   6.133    "1 + q = iSuc q"
   6.134 @@ -213,14 +213,14 @@
   6.135  begin
   6.136  
   6.137  definition times_enat_def [nitpick_simp]:
   6.138 -  "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
   6.139 -    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
   6.140 +  "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | enat m \<Rightarrow>
   6.141 +    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | enat n \<Rightarrow> enat (m * n)))"
   6.142  
   6.143  lemma times_enat_simps [simp, code]:
   6.144 -  "Fin m * Fin n = Fin (m * n)"
   6.145 +  "enat m * enat n = enat (m * n)"
   6.146    "\<infinity> * \<infinity> = (\<infinity>::enat)"
   6.147 -  "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
   6.148 -  "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
   6.149 +  "\<infinity> * enat n = (if n = 0 then 0 else \<infinity>)"
   6.150 +  "enat m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
   6.151    unfolding times_enat_def zero_enat_def
   6.152    by (simp_all split: enat.split)
   6.153  
   6.154 @@ -257,21 +257,21 @@
   6.155  lemma mult_iSuc_right: "m * iSuc n = m + m * n"
   6.156    unfolding iSuc_plus_1 by (simp add: algebra_simps)
   6.157  
   6.158 -lemma of_nat_eq_Fin: "of_nat n = Fin n"
   6.159 +lemma of_nat_eq_enat: "of_nat n = enat n"
   6.160    apply (induct n)
   6.161 -  apply (simp add: Fin_0)
   6.162 -  apply (simp add: plus_1_iSuc iSuc_Fin)
   6.163 +  apply (simp add: enat_0)
   6.164 +  apply (simp add: plus_1_iSuc iSuc_enat)
   6.165    done
   6.166  
   6.167  instance enat :: number_semiring
   6.168  proof
   6.169    fix n show "number_of (int n) = (of_nat n :: enat)"
   6.170 -    unfolding number_of_enat_def number_of_int of_nat_id of_nat_eq_Fin ..
   6.171 +    unfolding number_of_enat_def number_of_int of_nat_id of_nat_eq_enat ..
   6.172  qed
   6.173  
   6.174  instance enat :: semiring_char_0 proof
   6.175 -  have "inj Fin" by (rule injI) simp
   6.176 -  then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_Fin)
   6.177 +  have "inj enat" by (rule injI) simp
   6.178 +  then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
   6.179  qed
   6.180  
   6.181  lemma imult_is_0[simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
   6.182 @@ -287,31 +287,31 @@
   6.183  begin
   6.184  
   6.185  definition diff_enat_def:
   6.186 -"a - b = (case a of (Fin x) \<Rightarrow> (case b of (Fin y) \<Rightarrow> Fin (x - y) | \<infinity> \<Rightarrow> 0)
   6.187 +"a - b = (case a of (enat x) \<Rightarrow> (case b of (enat y) \<Rightarrow> enat (x - y) | \<infinity> \<Rightarrow> 0)
   6.188            | \<infinity> \<Rightarrow> \<infinity>)"
   6.189  
   6.190  instance ..
   6.191  
   6.192  end
   6.193  
   6.194 -lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)"
   6.195 +lemma idiff_enat_enat[simp,code]: "enat a - enat b = enat (a - b)"
   6.196  by(simp add: diff_enat_def)
   6.197  
   6.198  lemma idiff_Infty[simp,code]: "\<infinity> - n = (\<infinity>::enat)"
   6.199  by(simp add: diff_enat_def)
   6.200  
   6.201 -lemma idiff_Infty_right[simp,code]: "Fin a - \<infinity> = 0"
   6.202 +lemma idiff_Infty_right[simp,code]: "enat a - \<infinity> = 0"
   6.203  by(simp add: diff_enat_def)
   6.204  
   6.205  lemma idiff_0[simp]: "(0::enat) - n = 0"
   6.206  by (cases n, simp_all add: zero_enat_def)
   6.207  
   6.208 -lemmas idiff_Fin_0[simp] = idiff_0[unfolded zero_enat_def]
   6.209 +lemmas idiff_enat_0[simp] = idiff_0[unfolded zero_enat_def]
   6.210  
   6.211  lemma idiff_0_right[simp]: "(n::enat) - 0 = n"
   6.212  by (cases n) (simp_all add: zero_enat_def)
   6.213  
   6.214 -lemmas idiff_Fin_0_right[simp] = idiff_0_right[unfolded zero_enat_def]
   6.215 +lemmas idiff_enat_0_right[simp] = idiff_0_right[unfolded zero_enat_def]
   6.216  
   6.217  lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
   6.218  by(auto simp: zero_enat_def)
   6.219 @@ -320,9 +320,9 @@
   6.220  by(simp add: iSuc_def split: enat.split)
   6.221  
   6.222  lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n"
   6.223 -by(simp add: one_enat_def iSuc_Fin[symmetric] zero_enat_def[symmetric])
   6.224 +by(simp add: one_enat_def iSuc_enat[symmetric] zero_enat_def[symmetric])
   6.225  
   6.226 -(*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_enat_def]*)
   6.227 +(*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*)
   6.228  
   6.229  subsection {* Ordering *}
   6.230  
   6.231 @@ -330,16 +330,16 @@
   6.232  begin
   6.233  
   6.234  definition [nitpick_simp]:
   6.235 -  "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
   6.236 +  "m \<le> n = (case n of enat n1 \<Rightarrow> (case m of enat m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
   6.237      | \<infinity> \<Rightarrow> True)"
   6.238  
   6.239  definition [nitpick_simp]:
   6.240 -  "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
   6.241 +  "m < n = (case m of enat m1 \<Rightarrow> (case n of enat n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
   6.242      | \<infinity> \<Rightarrow> False)"
   6.243  
   6.244  lemma enat_ord_simps [simp]:
   6.245 -  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   6.246 -  "Fin m < Fin n \<longleftrightarrow> m < n"
   6.247 +  "enat m \<le> enat n \<longleftrightarrow> m \<le> n"
   6.248 +  "enat m < enat n \<longleftrightarrow> m < n"
   6.249    "q \<le> (\<infinity>::enat)"
   6.250    "q < (\<infinity>::enat) \<longleftrightarrow> q \<noteq> \<infinity>"
   6.251    "(\<infinity>::enat) \<le> q \<longleftrightarrow> q = \<infinity>"
   6.252 @@ -347,11 +347,11 @@
   6.253    by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)
   6.254  
   6.255  lemma enat_ord_code [code]:
   6.256 -  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   6.257 -  "Fin m < Fin n \<longleftrightarrow> m < n"
   6.258 +  "enat m \<le> enat n \<longleftrightarrow> m \<le> n"
   6.259 +  "enat m < enat n \<longleftrightarrow> m < n"
   6.260    "q \<le> (\<infinity>::enat) \<longleftrightarrow> True"
   6.261 -  "Fin m < \<infinity> \<longleftrightarrow> True"
   6.262 -  "\<infinity> \<le> Fin n \<longleftrightarrow> False"
   6.263 +  "enat m < \<infinity> \<longleftrightarrow> True"
   6.264 +  "\<infinity> \<le> enat n \<longleftrightarrow> False"
   6.265    "(\<infinity>::enat) < q \<longleftrightarrow> False"
   6.266    by simp_all
   6.267  
   6.268 @@ -380,10 +380,10 @@
   6.269  lemma ile0_eq [simp]: "n \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0"
   6.270  by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   6.271  
   6.272 -lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m \<Longrightarrow> R"
   6.273 +lemma Infty_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
   6.274    by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   6.275  
   6.276 -lemma Infty_ilessE [elim!]: "\<infinity> < Fin m \<Longrightarrow> R"
   6.277 +lemma Infty_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
   6.278    by simp
   6.279  
   6.280  lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)"
   6.281 @@ -413,10 +413,10 @@
   6.282  lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
   6.283    by (simp add: iSuc_def less_eq_enat_def less_enat_def split: enat.splits)
   6.284  
   6.285 -lemma Suc_ile_eq: "Fin (Suc m) \<le> n \<longleftrightarrow> Fin m < n"
   6.286 +lemma Suc_ile_eq: "enat (Suc m) \<le> n \<longleftrightarrow> enat m < n"
   6.287    by (cases n) auto
   6.288  
   6.289 -lemma iless_Suc_eq [simp]: "Fin m < iSuc n \<longleftrightarrow> Fin m \<le> n"
   6.290 +lemma iless_Suc_eq [simp]: "enat m < iSuc n \<longleftrightarrow> enat m \<le> n"
   6.291    by (auto simp add: iSuc_def less_enat_def split: enat.splits)
   6.292  
   6.293  lemma imult_Infty: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
   6.294 @@ -433,7 +433,7 @@
   6.295  
   6.296  
   6.297  lemma min_enat_simps [simp]:
   6.298 -  "min (Fin m) (Fin n) = Fin (min m n)"
   6.299 +  "min (enat m) (enat n) = enat (min m n)"
   6.300    "min q 0 = 0"
   6.301    "min 0 q = 0"
   6.302    "min q (\<infinity>::enat) = q"
   6.303 @@ -441,28 +441,28 @@
   6.304    by (auto simp add: min_def)
   6.305  
   6.306  lemma max_enat_simps [simp]:
   6.307 -  "max (Fin m) (Fin n) = Fin (max m n)"
   6.308 +  "max (enat m) (enat n) = enat (max m n)"
   6.309    "max q 0 = q"
   6.310    "max 0 q = q"
   6.311    "max q \<infinity> = (\<infinity>::enat)"
   6.312    "max \<infinity> q = (\<infinity>::enat)"
   6.313    by (simp_all add: max_def)
   6.314  
   6.315 -lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   6.316 +lemma enat_ile: "n \<le> enat m \<Longrightarrow> \<exists>k. n = enat k"
   6.317    by (cases n) simp_all
   6.318  
   6.319 -lemma Fin_iless: "n < Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   6.320 +lemma enat_iless: "n < enat m \<Longrightarrow> \<exists>k. n = enat k"
   6.321    by (cases n) simp_all
   6.322  
   6.323 -lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   6.324 +lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. enat k < Y j"
   6.325  apply (induct_tac k)
   6.326 - apply (simp (no_asm) only: Fin_0)
   6.327 + apply (simp (no_asm) only: enat_0)
   6.328   apply (fast intro: le_less_trans [OF i0_lb])
   6.329  apply (erule exE)
   6.330  apply (drule spec)
   6.331  apply (erule exE)
   6.332  apply (drule ileI1)
   6.333 -apply (rule iSuc_Fin [THEN subst])
   6.334 +apply (rule iSuc_enat [THEN subst])
   6.335  apply (rule exI)
   6.336  apply (erule (1) le_less_trans)
   6.337  done
   6.338 @@ -481,46 +481,46 @@
   6.339  
   6.340  end
   6.341  
   6.342 -lemma finite_Fin_bounded:
   6.343 -  assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> Fin n"
   6.344 +lemma finite_enat_bounded:
   6.345 +  assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> enat n"
   6.346    shows "finite A"
   6.347  proof (rule finite_subset)
   6.348 -  show "finite (Fin ` {..n})" by blast
   6.349 +  show "finite (enat ` {..n})" by blast
   6.350  
   6.351 -  have "A \<subseteq> {..Fin n}" using le_fin by fastsimp
   6.352 -  also have "\<dots> \<subseteq> Fin ` {..n}"
   6.353 +  have "A \<subseteq> {..enat n}" using le_fin by fastsimp
   6.354 +  also have "\<dots> \<subseteq> enat ` {..n}"
   6.355      by (rule subsetI) (case_tac x, auto)
   6.356 -  finally show "A \<subseteq> Fin ` {..n}" .
   6.357 +  finally show "A \<subseteq> enat ` {..n}" .
   6.358  qed
   6.359  
   6.360  
   6.361  subsection {* Well-ordering *}
   6.362  
   6.363 -lemma less_FinE:
   6.364 -  "[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P"
   6.365 +lemma less_enatE:
   6.366 +  "[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P"
   6.367  by (induct n) auto
   6.368  
   6.369  lemma less_InftyE:
   6.370 -  "[| n < \<infinity>; !!k. n = Fin k ==> P |] ==> P"
   6.371 +  "[| n < \<infinity>; !!k. n = enat k ==> P |] ==> P"
   6.372  by (induct n) auto
   6.373  
   6.374  lemma enat_less_induct:
   6.375    assumes prem: "!!n. \<forall>m::enat. m < n --> P m ==> P n" shows "P n"
   6.376  proof -
   6.377 -  have P_Fin: "!!k. P (Fin k)"
   6.378 +  have P_enat: "!!k. P (enat k)"
   6.379      apply (rule nat_less_induct)
   6.380      apply (rule prem, clarify)
   6.381 -    apply (erule less_FinE, simp)
   6.382 +    apply (erule less_enatE, simp)
   6.383      done
   6.384    show ?thesis
   6.385    proof (induct n)
   6.386      fix nat
   6.387 -    show "P (Fin nat)" by (rule P_Fin)
   6.388 +    show "P (enat nat)" by (rule P_enat)
   6.389    next
   6.390      show "P \<infinity>"
   6.391        apply (rule prem, clarify)
   6.392        apply (erule less_InftyE)
   6.393 -      apply (simp add: P_Fin)
   6.394 +      apply (simp add: P_enat)
   6.395        done
   6.396    qed
   6.397  qed
   6.398 @@ -560,7 +560,7 @@
   6.399    { assume "x \<in> A" then show "x \<le> Sup A"
   6.400        unfolding Sup_enat_def by (cases "finite A") auto }
   6.401    { assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
   6.402 -      unfolding Sup_enat_def using finite_Fin_bounded by auto }
   6.403 +      unfolding Sup_enat_def using finite_enat_bounded by auto }
   6.404  qed (simp_all add: inf_enat_def sup_enat_def)
   6.405  end
   6.406  
     7.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Jul 19 14:38:29 2011 +0200
     7.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Jul 19 14:38:48 2011 +0200
     7.3 @@ -55,7 +55,7 @@
     7.4    instance ..
     7.5  end
     7.6  
     7.7 -definition "ereal_of_enat n = (case n of Fin n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
     7.8 +definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
     7.9  
    7.10  declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
    7.11  declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]