src/HOL/Library/Char_ord.thy
changeset 62597 b3f2b8c906a6
parent 61076 bdc1e2f0a86a
child 63462 c1fe30f2bc32
     1.1 --- a/src/HOL/Library/Char_ord.thy	Fri Mar 11 17:20:14 2016 +0100
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Sat Mar 12 22:04:52 2016 +0100
     1.3 @@ -8,28 +8,6 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -instantiation nibble :: linorder
     1.8 -begin
     1.9 -
    1.10 -definition "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
    1.11 -definition "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
    1.12 -
    1.13 -instance
    1.14 -  by standard (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
    1.15 -
    1.16 -end
    1.17 -
    1.18 -instantiation nibble :: distrib_lattice
    1.19 -begin
    1.20 -
    1.21 -definition "(inf :: nibble \<Rightarrow> _) = min"
    1.22 -definition "(sup :: nibble \<Rightarrow> _) = max"
    1.23 -
    1.24 -instance
    1.25 -  by standard (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
    1.26 -
    1.27 -end
    1.28 -
    1.29  instantiation char :: linorder
    1.30  begin
    1.31  
    1.32 @@ -37,40 +15,22 @@
    1.33  definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
    1.34  
    1.35  instance
    1.36 -  by standard (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
    1.37 +  by standard (auto simp add: less_eq_char_def less_char_def)
    1.38  
    1.39  end
    1.40  
    1.41 -lemma less_eq_char_Char:
    1.42 -  "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    1.43 -proof -
    1.44 -  {
    1.45 -    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
    1.46 -      \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2"
    1.47 -    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
    1.48 -    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
    1.49 -  }
    1.50 -  note * = this
    1.51 -  show ?thesis
    1.52 -    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
    1.53 -    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.54 -qed
    1.55 +lemma less_eq_char_simps:
    1.56 +  "(0 :: char) \<le> c"
    1.57 +  "Char k \<le> 0 \<longleftrightarrow> numeral k mod 256 = (0 :: nat)"
    1.58 +  "Char k \<le> Char l \<longleftrightarrow> numeral k mod 256 \<le> (numeral l mod 256 :: nat)"
    1.59 +  by (simp_all add: Char_def less_eq_char_def)
    1.60  
    1.61 -lemma less_char_Char:
    1.62 -  "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    1.63 -proof -
    1.64 -  {
    1.65 -    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
    1.66 -      < nat_of_nibble n2 * 16 + nat_of_nibble m2"
    1.67 -    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
    1.68 -    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
    1.69 -  }
    1.70 -  note * = this
    1.71 -  show ?thesis
    1.72 -    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
    1.73 -    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.74 -qed
    1.75 -
    1.76 +lemma less_char_simps:
    1.77 +  "\<not> c < (0 :: char)"
    1.78 +  "0 < Char k \<longleftrightarrow> (0 :: nat) < numeral k mod 256"
    1.79 +  "Char k < Char l \<longleftrightarrow> numeral k mod 256 < (numeral l mod 256 :: nat)"
    1.80 +  by (simp_all add: Char_def less_char_def)
    1.81 +  
    1.82  instantiation char :: distrib_lattice
    1.83  begin
    1.84  
    1.85 @@ -111,14 +71,4 @@
    1.86  lifting_update literal.lifting
    1.87  lifting_forget literal.lifting
    1.88  
    1.89 -text \<open>Legacy aliasses\<close>
    1.90 -
    1.91 -lemmas nibble_less_eq_def = less_eq_nibble_def
    1.92 -lemmas nibble_less_def = less_nibble_def
    1.93 -lemmas char_less_eq_def = less_eq_char_def
    1.94 -lemmas char_less_def = less_char_def
    1.95 -lemmas char_less_eq_simp = less_eq_char_Char
    1.96 -lemmas char_less_simp = less_char_Char
    1.97 -
    1.98  end
    1.99 -