# HG changeset patch
# User haftmann
# Date 1204054693 -3600
# Node ID cbe6f8af8db2ee7afeecb53c6f63bcd238a5c245
# Parent  ae2bf929e33c2318371180b71958b1c5c67e5235
char and nibble are finite

diff -r ae2bf929e33c -r cbe6f8af8db2 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Feb 26 20:38:12 2008 +0100
+++ b/src/HOL/List.thy	Tue Feb 26 20:38:13 2008 +0100
@@ -3158,9 +3158,30 @@
     Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
   | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
 
+lemma UNIV_nibble:
+  "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
+    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
+proof (rule UNIV_eq_I)
+  fix x show "x \<in> ?A" by (cases x) simp_all
+qed
+
+instance nibble :: finite
+  by default (simp add: UNIV_nibble)
+
+declare UNIV_nibble [code func]
+ 
 datatype char = Char nibble nibble
   -- "Note: canonical order of character encoding coincides with standard term ordering"
 
+lemma UNIV_char:
+  "UNIV = image (split Char) (UNIV \<times> UNIV)"
+proof (rule UNIV_eq_I)
+  fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
+qed
+
+instance char :: finite
+  by default (simp add: UNIV_char)
+
 types string = "char list"
 
 syntax