# HG changeset patch
# User nipkow
# Date 1362568672 -3600
# Node ID ac4c1cf1b00113514ffde3464f978c588b069b97
# Parent  877edf1fc5dd3469d7448ccf2df6379f9e22888e
extended numerals

diff -r 877edf1fc5dd -r ac4c1cf1b001 src/HOL/Library/Extended.thy
--- a/src/HOL/Library/Extended.thy	Tue Mar 05 17:25:41 2013 +0100
+++ b/src/HOL/Library/Extended.thy	Wed Mar 06 12:17:52 2013 +0100
@@ -13,6 +13,7 @@
 lemmas extended_cases2 = extended.exhaust[case_product extended.exhaust]
 lemmas extended_cases3 = extended.exhaust[case_product extended_cases2]
 
+
 instantiation extended :: (order)order
 begin
 
@@ -84,6 +85,18 @@
 by (auto simp add: max_def)
 
 
+instantiation extended :: (zero)zero
+begin
+definition "0 = Fin(0::'a)"
+instance ..
+end
+
+instantiation extended :: (one)one
+begin
+definition "1 = Fin(1::'a)"
+instance ..
+end
+
 instantiation extended :: (plus)plus
 begin
 
@@ -122,18 +135,11 @@
     by (cases rule: extended_cases3[of a b c]) (auto simp: add_left_mono)
 qed
 
-instantiation extended :: (comm_monoid_add)comm_monoid_add
-begin
-
-definition "0 = Fin 0"
-
-instance
+instance extended :: (comm_monoid_add)comm_monoid_add
 proof
   fix x :: "'a extended" show "0 + x = x" unfolding zero_extended_def by(cases x)auto
 qed
 
-end
-
 instantiation extended :: (uminus)uminus
 begin
 
@@ -165,6 +171,18 @@
   "Pinf  - Pinf  = Pinf"
 by (simp_all add: minus_extended_def)
 
+
+text{* Numerals: *}
+
+instance extended :: ("{ab_semigroup_add,one}")numeral ..
+
+lemma Fin_numeral: "Fin(numeral w) = numeral w"
+  apply (induct w rule: num_induct)
+  apply (simp only: numeral_One one_extended_def)
+  apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
+  done
+
+
 instantiation extended :: (lattice)bounded_lattice
 begin