author  nipkow 
Sun, 26 Aug 2012 10:20:26 +0200  
changeset 48926  8d7778a19857 
parent 37765  26bdfb7b680b 
child 51160  599ff65b85e2 
permissions  rwrr 
15737  1 
(* Title: HOL/Library/Char_ord.thy 
22805  2 
Author: Norbert Voelker, Florian Haftmann 
15737  3 
*) 
4 

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

7 
theory Char_ord 

48926  8 
imports Char_nat 
15737  9 
begin 
10 

25764  11 
instantiation nibble :: linorder 
12 
begin 

13 

14 
definition 

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

16 

17 
definition 

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

19 

20 
instance proof 

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

22805  23 
next 
24 
fix n m q :: nibble 

25 
assume "n \<le> m" 

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

29 
fix n m :: nibble 

30 
assume "n \<le> m" 

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

33 
unfolding nibble_less_eq_def nibble_less_def 

34 
by (auto simp add: nat_of_nibble_eq) 

22805  35 
next 
36 
fix n m :: nibble 

27682  37 
show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n" 
23394  38 
unfolding nibble_less_eq_def nibble_less_def less_le 
39 
by (auto simp add: nat_of_nibble_eq) 

22805  40 
next 
41 
fix n m :: nibble 

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

23394  43 
unfolding nibble_less_eq_def by auto 
22805  44 
qed 
15737  45 

25764  46 
end 
47 

48 
instantiation nibble :: distrib_lattice 

49 
begin 

50 

51 
definition 

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

54 
definition 

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

57 
instance by default (auto simp add: 

23394  58 
inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1) 
15737  59 

25764  60 
end 
61 

62 
instantiation char :: linorder 

63 
begin 

64 

65 
definition 

37765  66 
char_less_eq_def: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow> 
25764  67 
n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)" 
68 

69 
definition 

37765  70 
char_less_def: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow> 
25764  71 
n1 < n2 \<or> n1 = n2 \<and> m1 < m2)" 
72 

73 
instance 

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

25764  76 
end 
15737  77 

25764  78 
instantiation char :: distrib_lattice 
79 
begin 

80 

81 
definition 

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

84 
definition 

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

87 
instance by default (auto simp add: 

23394  88 
inf_char_def sup_char_def min_max.sup_inf_distrib1) 
22483  89 

25764  90 
end 
91 

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

95 
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

96 

17200  97 
end 