author  haftmann 
Wed, 02 Jan 2008 15:14:17 +0100  
changeset 25764  878c37886eed 
parent 25502  9200b36280c0 
child 27368  9f90ac19e32b 
permissions  rwrr 
15737  1 
(* Title: HOL/Library/Char_ord.thy 
2 
ID: $Id$ 

22805  3 
Author: Norbert Voelker, Florian Haftmann 
15737  4 
*) 
5 

17200  6 
header {* Order on characters *} 
15737  7 

8 
theory Char_ord 

22805  9 
imports Product_ord Char_nat 
15737  10 
begin 
11 

25764  12 
instantiation nibble :: linorder 
13 
begin 

14 

15 
definition 

16 
nibble_less_eq_def: "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m" 

17 

18 
definition 

19 
nibble_less_def: "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m" 

20 

21 
instance proof 

23394  22 
fix n :: nibble 
23 
show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto 

22805  24 
next 
25 
fix n m q :: nibble 

26 
assume "n \<le> m" 

23394  27 
and "m \<le> q" 
22805  28 
then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto 
29 
next 

30 
fix n m :: nibble 

31 
assume "n \<le> m" 

23394  32 
and "m \<le> n" 
33 
then show "n = m" 

34 
unfolding nibble_less_eq_def nibble_less_def 

35 
by (auto simp add: nat_of_nibble_eq) 

22805  36 
next 
37 
fix n m :: nibble 

38 
show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m" 

23394  39 
unfolding nibble_less_eq_def nibble_less_def less_le 
40 
by (auto simp add: nat_of_nibble_eq) 

22805  41 
next 
42 
fix n m :: nibble 

43 
show "n \<le> m \<or> m \<le> n" 

23394  44 
unfolding nibble_less_eq_def by auto 
22805  45 
qed 
15737  46 

25764  47 
end 
48 

49 
instantiation nibble :: distrib_lattice 

50 
begin 

51 

52 
definition 

25502  53 
"(inf \<Colon> nibble \<Rightarrow> _) = min" 
25764  54 

55 
definition 

25502  56 
"(sup \<Colon> nibble \<Rightarrow> _) = max" 
25764  57 

58 
instance by default (auto simp add: 

23394  59 
inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1) 
15737  60 

25764  61 
end 
62 

63 
instantiation char :: linorder 

64 
begin 

65 

66 
definition 

67 
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> 

68 
n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)" 

69 

70 
definition 

71 
char_less_def [code func del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow> 

72 
n1 < n2 \<or> n1 = n2 \<and> m1 < m2)" 

73 

74 
instance 

22805  75 
by default (auto simp: char_less_eq_def char_less_def split: char.splits) 
76 

25764  77 
end 
15737  78 

25764  79 
instantiation char :: distrib_lattice 
80 
begin 

81 

82 
definition 

25502  83 
"(inf \<Colon> char \<Rightarrow> _) = min" 
25764  84 

85 
definition 

25502  86 
"(sup \<Colon> char \<Rightarrow> _) = max" 
25764  87 

88 
instance by default (auto simp add: 

23394  89 
inf_char_def sup_char_def min_max.sup_inf_distrib1) 
22483  90 

25764  91 
end 
92 

22805  93 
lemma [simp, code func]: 
94 
shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2" 

95 
and char_less_simp: "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2" 

96 
unfolding char_less_eq_def char_less_def by simp_all 

21871
9ce66839d9f1
added code generation syntax for some char combinators
haftmann
parents:
21404
diff
changeset

97 

17200  98 
end 