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.5  
     1.6  theory Char_ord
     1.7 -imports Char_nat
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  instantiation nibble :: linorder
    1.12  begin
    1.13  
    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.17  
    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.21  
    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.48  
    1.49  end
    1.50  
    1.51 @@ -54,8 +31,8 @@
    1.52  definition
    1.53    "(sup \<Colon> nibble \<Rightarrow> _) = max"
    1.54  
    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.59  
    1.60  end
    1.61  
    1.62 @@ -63,18 +40,46 @@
    1.63  begin
    1.64  
    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.69  
    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.74  
    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.79  
    1.80  end
    1.81  
    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.111 +
   1.112  instantiation char :: distrib_lattice
   1.113  begin
   1.114  
   1.115 @@ -84,14 +89,19 @@
   1.116  definition
   1.117    "(sup \<Colon> char \<Rightarrow> _) = max"
   1.118  
   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.123  
   1.124  end
   1.125  
   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.131 +
   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.138  
   1.139  end
   1.140 +