author  haftmann 
Thu, 26 Apr 2007 13:33:15 +0200  
changeset 22805  1166a966e7b4 
parent 22483  86064f2f2188 
child 22845  5f9138bcb3d7 
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 

22805  12 
instance nibble :: linorder 
13 
nibble_less_eq_def: "n \<le> m \<equiv> nat_of_nibble n \<le> nat_of_nibble m" 

14 
nibble_less_def: "n < m \<equiv> nat_of_nibble n < nat_of_nibble m" 

15 
proof 

16 
fix n :: nibble show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto 

17 
next 

18 
fix n m q :: nibble 

19 
assume "n \<le> m" 

20 
and "m \<le> q" 

21 
then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto 

22 
next 

23 
fix n m :: nibble 

24 
assume "n \<le> m" 

25 
and "m \<le> n" 

26 
then show "n = m" unfolding nibble_less_eq_def nibble_less_def by (auto simp add: nat_of_nibble_eq) 

27 
next 

28 
fix n m :: nibble 

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

30 
unfolding nibble_less_eq_def nibble_less_def less_le by (auto simp add: nat_of_nibble_eq) 

31 
next 

32 
fix n m :: nibble 

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

34 
unfolding nibble_less_eq_def by auto 

35 
qed 

15737  36 

22805  37 
instance nibble :: distrib_lattice 
38 
"inf \<equiv> min" 

39 
"sup \<equiv> max" 

40 
by default 

41 
(auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1) 

15737  42 

19736  43 
instance char :: linorder 
22805  44 
char_less_eq_def: "c1 \<le> c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow> 
45 
n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2" 

46 
char_less_def: "c1 < c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow> 

47 
n1 < n2 \<or> n1 = n2 \<and> m1 < m2" 

48 
by default (auto simp: char_less_eq_def char_less_def split: char.splits) 

49 

50 
lemmas [code nofunc] = char_less_eq_def char_less_def 

15737  51 

22483  52 
instance char :: distrib_lattice 
53 
"inf \<equiv> min" 

54 
"sup \<equiv> max" 

22805  55 
by default 
22483  56 
(auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1) 
57 

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

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

61 
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

62 

17200  63 
end 