src/HOL/Library/Char_ord.thy
 changeset 51160 599ff65b85e2 parent 48926 8d7778a19857 child 54595 a2eeeb335a48
1.1 --- a/src/HOL/Library/Char_ord.thy	Fri Feb 15 15:22:16 2013 +0100
1.2 +++ b/src/HOL/Library/Char_ord.thy	Fri Feb 15 11:47:33 2013 +0100
1.3 @@ -5,43 +5,20 @@
1.4  header {* Order on characters *}
1.6  theory Char_ord
1.7 -imports Char_nat
1.8 +imports Main
1.9  begin
1.11  instantiation nibble :: linorder
1.12  begin
1.14  definition
1.15 -  nibble_less_eq_def: "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
1.16 +  "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
1.18  definition
1.19 -  nibble_less_def: "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
1.20 +  "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
1.22  instance proof
1.23 -  fix n :: nibble
1.24 -  show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
1.25 -next
1.26 -  fix n m q :: nibble
1.27 -  assume "n \<le> m"
1.28 -    and "m \<le> q"
1.29 -  then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto
1.30 -next
1.31 -  fix n m :: nibble
1.32 -  assume "n \<le> m"
1.33 -    and "m \<le> n"
1.34 -  then show "n = m"
1.35 -    unfolding nibble_less_eq_def nibble_less_def
1.36 -    by (auto simp add: nat_of_nibble_eq)
1.37 -next
1.38 -  fix n m :: nibble
1.39 -  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
1.40 -    unfolding nibble_less_eq_def nibble_less_def less_le
1.41 -    by (auto simp add: nat_of_nibble_eq)
1.42 -next
1.43 -  fix n m :: nibble
1.44 -  show "n \<le> m \<or> m \<le> n"
1.45 -    unfolding nibble_less_eq_def by auto
1.46 -qed
1.47 +qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
1.49  end
1.51 @@ -54,8 +31,8 @@
1.52  definition
1.53    "(sup \<Colon> nibble \<Rightarrow> _) = max"
1.55 -instance by default (auto simp add:
1.56 -    inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
1.57 +instance proof
1.58 +qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
1.60  end
1.62 @@ -63,18 +40,46 @@
1.63  begin
1.65  definition
1.66 -  char_less_eq_def: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
1.67 -    n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
1.68 +  "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
1.70  definition
1.71 -  char_less_def: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
1.72 -    n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
1.73 +  "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
1.75 -instance
1.76 -  by default (auto simp: char_less_eq_def char_less_def split: char.splits)
1.77 +instance proof
1.78 +qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
1.80  end
1.82 +lemma less_eq_char_Char:
1.83 +  "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
1.84 +proof -
1.85 +  {
1.86 +    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
1.87 +      \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2"
1.88 +    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
1.89 +    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
1.90 +  }
1.91 +  note * = this
1.92 +  show ?thesis
1.93 +    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
1.94 +    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: *)
1.95 +qed
1.96 +
1.97 +lemma less_char_Char:
1.98 +  "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
1.99 +proof -
1.100 +  {
1.101 +    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
1.102 +      < nat_of_nibble n2 * 16 + nat_of_nibble m2"
1.103 +    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
1.104 +    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
1.105 +  }
1.106 +  note * = this
1.107 +  show ?thesis
1.108 +    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
1.109 +    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: *)
1.110 +qed
1.112  instantiation char :: distrib_lattice
1.113  begin
1.115 @@ -84,14 +89,19 @@
1.116  definition
1.117    "(sup \<Colon> char \<Rightarrow> _) = max"
1.119 -instance   by default (auto simp add:
1.120 -    inf_char_def sup_char_def min_max.sup_inf_distrib1)
1.121 +instance proof
1.122 +qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
1.124  end
1.126 -lemma [simp, code]:
1.127 -  shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
1.128 -  and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
1.129 -  unfolding char_less_eq_def char_less_def by simp_all
1.130 +text {* Legacy aliasses *}
1.132 +lemmas nibble_less_eq_def = less_eq_nibble_def
1.133 +lemmas nibble_less_def = less_nibble_def
1.134 +lemmas char_less_eq_def = less_eq_char_def
1.135 +lemmas char_less_def = less_char_def
1.136 +lemmas char_less_eq_simp = less_eq_char_Char
1.137 +lemmas char_less_simp = less_char_Char
1.139  end