src/HOL/Library/Char_ord.thy
changeset 25764 878c37886eed
parent 25502 9200b36280c0
child 27368 9f90ac19e32b
     1.1 --- a/src/HOL/Library/Char_ord.thy	Wed Jan 02 15:14:15 2008 +0100
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Wed Jan 02 15:14:17 2008 +0100
     1.3 @@ -9,10 +9,16 @@
     1.4  imports Product_ord Char_nat
     1.5  begin
     1.6  
     1.7 -instance nibble :: linorder
     1.8 -  nibble_less_eq_def: "n \<le> m \<equiv> nat_of_nibble n \<le> nat_of_nibble m"
     1.9 -  nibble_less_def: "n < m \<equiv> nat_of_nibble n < nat_of_nibble m"
    1.10 -proof
    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 +
    1.17 +definition
    1.18 +  nibble_less_def: "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
    1.19 +
    1.20 +instance proof
    1.21    fix n :: nibble
    1.22    show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
    1.23  next
    1.24 @@ -38,27 +44,52 @@
    1.25      unfolding nibble_less_eq_def by auto
    1.26  qed
    1.27  
    1.28 -instance nibble :: distrib_lattice
    1.29 +end
    1.30 +
    1.31 +instantiation nibble :: distrib_lattice
    1.32 +begin
    1.33 +
    1.34 +definition
    1.35    "(inf \<Colon> nibble \<Rightarrow> _) = min"
    1.36 +
    1.37 +definition
    1.38    "(sup \<Colon> nibble \<Rightarrow> _) = max"
    1.39 -  by default (auto simp add:
    1.40 +
    1.41 +instance by default (auto simp add:
    1.42      inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    1.43  
    1.44 -instance char :: linorder
    1.45 -  char_less_eq_def: "c1 \<le> c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    1.46 -    n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    1.47 -  char_less_def:    "c1 < c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    1.48 -    n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    1.49 +end
    1.50 +
    1.51 +instantiation char :: linorder
    1.52 +begin
    1.53 +
    1.54 +definition
    1.55 +  char_less_eq_def [code func del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    1.56 +    n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
    1.57 +
    1.58 +definition
    1.59 +  char_less_def [code func del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    1.60 +    n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
    1.61 +
    1.62 +instance
    1.63    by default (auto simp: char_less_eq_def char_less_def split: char.splits)
    1.64  
    1.65 -lemmas [code func del] = char_less_eq_def char_less_def
    1.66 +end
    1.67  
    1.68 -instance char :: distrib_lattice
    1.69 +instantiation char :: distrib_lattice
    1.70 +begin
    1.71 +
    1.72 +definition
    1.73    "(inf \<Colon> char \<Rightarrow> _) = min"
    1.74 +
    1.75 +definition
    1.76    "(sup \<Colon> char \<Rightarrow> _) = max"
    1.77 -  by default (auto simp add:
    1.78 +
    1.79 +instance   by default (auto simp add:
    1.80      inf_char_def sup_char_def min_max.sup_inf_distrib1)
    1.81  
    1.82 +end
    1.83 +
    1.84  lemma [simp, code func]:
    1.85    shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    1.86    and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"