author  wenzelm 
Thu, 14 Jun 2007 23:04:39 +0200  
changeset 23394  474ff28210c0 
parent 22845  5f9138bcb3d7 
child 25502  9200b36280c0 
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 

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

22805  18 
next 
19 
fix n m q :: nibble 

20 
assume "n \<le> m" 

23394  21 
and "m \<le> q" 
22805  22 
then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto 
23 
next 

24 
fix n m :: nibble 

25 
assume "n \<le> m" 

23394  26 
and "m \<le> n" 
27 
then show "n = m" 

28 
unfolding nibble_less_eq_def nibble_less_def 

29 
by (auto simp add: nat_of_nibble_eq) 

22805  30 
next 
31 
fix n m :: nibble 

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

23394  33 
unfolding nibble_less_eq_def nibble_less_def less_le 
34 
by (auto simp add: nat_of_nibble_eq) 

22805  35 
next 
36 
fix n m :: nibble 

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

23394  38 
unfolding nibble_less_eq_def by auto 
22805  39 
qed 
15737  40 

22805  41 
instance nibble :: distrib_lattice 
23394  42 
"inf \<equiv> min" 
43 
"sup \<equiv> max" 

44 
by default (auto simp add: 

45 
inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1) 

15737  46 

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

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

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

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

53 

22845  54 
lemmas [code func del] = char_less_eq_def char_less_def 
15737  55 

22483  56 
instance char :: distrib_lattice 
23394  57 
"inf \<equiv> min" 
58 
"sup \<equiv> max" 

59 
by default (auto simp add: 

60 
inf_char_def sup_char_def min_max.sup_inf_distrib1) 

22483  61 

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

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

65 
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

66 

17200  67 
end 