# HG changeset patch
# User nipkow
# Date 1298749245 -3600
# Node ID c3b6e69da3862adf5473049a2c58267bc0b83bac
# Parent  b2b5b965b59c81428bcd7ada3ead70ba613bb01a
added a few lemmas by Andreas Lochbihler

diff -r b2b5b965b59c -r c3b6e69da386 src/HOL/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Sat Feb 26 20:16:44 2011 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Sat Feb 26 20:40:45 2011 +0100
@@ -83,11 +83,11 @@
 lemma jth_n[simp]: "Fin 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: inat_defs split: inat_splits)
+by (simp add: inat_defs split: inat.splits)
 
 lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a"
 apply (simp add: last_def)
-apply (simp add: inat_defs split:inat_splits)
+apply (simp add: inat_defs split:inat.splits)
 by (drule sym, auto)
 
 lemma last_fsingleton[simp]: "last (<a>) = a"
@@ -103,7 +103,7 @@
 by (simp add: last_def)
 
 lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
-by (simp add: jth_def inat_defs split:inat_splits, auto)
+by (simp add: jth_def inat_defs split:inat.splits, auto)
 
 lemma jth_UU[simp]:"jth n UU = undefined" 
 by (simp add: jth_def)
diff -r b2b5b965b59c -r c3b6e69da386 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Sat Feb 26 20:16:44 2011 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy	Sat Feb 26 20:40:45 2011 +0100
@@ -32,6 +32,10 @@
 by (cases x) auto
 
 
+primrec the_Fin :: "inat \<Rightarrow> nat"
+where "the_Fin (Fin n) = n"
+
+
 subsection {* Constructors and numbers *}
 
 instantiation inat :: "{zero, one, number}"
@@ -283,6 +287,12 @@
 lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::inat) - n = 0"
 by(auto simp: zero_inat_def)
 
+lemma iSuc_minus_iSuc [simp]: "iSuc n - iSuc m = n - m"
+by(simp add: iSuc_def split: inat.split)
+
+lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n"
+by(simp add: one_inat_def iSuc_Fin[symmetric] zero_inat_def[symmetric])
+
 (*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_inat_def]*)
 
 
@@ -488,6 +498,4 @@
 lemmas inat_defs = zero_inat_def one_inat_def number_of_inat_def iSuc_def
   plus_inat_def less_eq_inat_def less_inat_def
 
-lemmas inat_splits = inat.splits
-
 end