src/HOL/Library/Char_ord.thy

--- a/src/HOL/Library/Char_ord.thy	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Library/Char_ord.thy	Fri Feb 15 11:47:33 2013 +0100
@@ -5,43 +5,20 @@
 header {* Order on characters *}
 
 theory Char_ord
-imports Char_nat
+imports Main
 begin
 
 instantiation nibble :: linorder
 begin
 
 definition
-  nibble_less_eq_def: "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
+  "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
 
 definition
-  nibble_less_def: "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
+  "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
 
 instance proof
-  fix n :: nibble
-  show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
-next
-  fix n m q :: nibble
-  assume "n \<le> m"
-    and "m \<le> q"
-  then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto
-next
-  fix n m :: nibble
-  assume "n \<le> m"
-    and "m \<le> n"
-  then show "n = m"
-    unfolding nibble_less_eq_def nibble_less_def
-    by (auto simp add: nat_of_nibble_eq)
-next
-  fix n m :: nibble
-  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
-    unfolding nibble_less_eq_def nibble_less_def less_le
-    by (auto simp add: nat_of_nibble_eq)
-next
-  fix n m :: nibble
-  show "n \<le> m \<or> m \<le> n"
-    unfolding nibble_less_eq_def by auto
-qed
+qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
 
 end
 
@@ -54,8 +31,8 @@
 definition
   "(sup \<Colon> nibble \<Rightarrow> _) = max"
 
-instance by default (auto simp add:
-    inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
+instance proof
+qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
 
 end
 
@@ -63,18 +40,46 @@
 begin
 
 definition
-  char_less_eq_def: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
-    n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
+  "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
 
 definition
-  char_less_def: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
-    n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
+  "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
 
-instance
-  by default (auto simp: char_less_eq_def char_less_def split: char.splits)
+instance proof
+qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
 
 end
 
+lemma less_eq_char_Char:
+  "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
+proof -
+  {
+    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
+      \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2"
+    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
+    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
+  }
+  note * = this
+  show ?thesis
+    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
+    by (auto simp add: less_eq_char_def nat_of_char_Char less_eq_nibble_def less_nibble_def not_less nat_of_nibble_eq_iff dest: *)
+qed
+
+lemma less_char_Char:
+  "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
+proof -
+  {
+    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
+      < nat_of_nibble n2 * 16 + nat_of_nibble m2"
+    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
+    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
+  }
+  note * = this
+  show ?thesis
+    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
+    by (auto simp add: less_char_def nat_of_char_Char less_eq_nibble_def less_nibble_def not_less nat_of_nibble_eq_iff dest: *)
+qed
+
 instantiation char :: distrib_lattice
 begin
 
@@ -84,14 +89,19 @@
 definition
   "(sup \<Colon> char \<Rightarrow> _) = max"
 
-instance   by default (auto simp add:
-    inf_char_def sup_char_def min_max.sup_inf_distrib1)
+instance proof
+qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
 
 end
 
-lemma [simp, code]:
-  shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
-  and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
-  unfolding char_less_eq_def char_less_def by simp_all
+text {* Legacy aliasses *}
+
+lemmas nibble_less_eq_def = less_eq_nibble_def
+lemmas nibble_less_def = less_nibble_def
+lemmas char_less_eq_def = less_eq_char_def
+lemmas char_less_def = less_char_def
+lemmas char_less_eq_simp = less_eq_char_Char
+lemmas char_less_simp = less_char_Char
 
 end
+