author nipkow Wed, 06 Mar 2013 12:17:52 +0100 changeset 51357 ac4c1cf1b001 parent 51356 877edf1fc5dd child 51358 0c376ef98559
extended numerals
```--- 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 @@

+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

-begin
-
-definition "0 = Fin 0"
-
-instance
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"

+
+text{* Numerals: *}
+
+
+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
```