author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63462  c1fe30f2bc32 
child 67399  eab6ce8368fa 
permissions  rwrr 
15737  1 
(* Title: HOL/Library/Char_ord.thy 
22805  2 
Author: Norbert Voelker, Florian Haftmann 
15737  3 
*) 
4 

60500  5 
section \<open>Order on characters\<close> 
15737  6 

7 
theory Char_ord 

63462  8 
imports Main 
15737  9 
begin 
10 

25764  11 
instantiation char :: linorder 
12 
begin 

13 

60679  14 
definition "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2" 
15 
definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2" 

25764  16 

60679  17 
instance 
62597  18 
by standard (auto simp add: less_eq_char_def less_char_def) 
22805  19 

25764  20 
end 
15737  21 

62597  22 
lemma less_eq_char_simps: 
63462  23 
"0 \<le> c" 
62597  24 
"Char k \<le> 0 \<longleftrightarrow> numeral k mod 256 = (0 :: nat)" 
25 
"Char k \<le> Char l \<longleftrightarrow> numeral k mod 256 \<le> (numeral l mod 256 :: nat)" 

63462  26 
for c :: char 
62597  27 
by (simp_all add: Char_def less_eq_char_def) 
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset

28 

62597  29 
lemma less_char_simps: 
63462  30 
"\<not> c < 0" 
62597  31 
"0 < Char k \<longleftrightarrow> (0 :: nat) < numeral k mod 256" 
32 
"Char k < Char l \<longleftrightarrow> numeral k mod 256 < (numeral l mod 256 :: nat)" 

63462  33 
for c :: char 
62597  34 
by (simp_all add: Char_def less_char_def) 
63462  35 

25764  36 
instantiation char :: distrib_lattice 
37 
begin 

38 

61076  39 
definition "(inf :: char \<Rightarrow> _) = min" 
40 
definition "(sup :: char \<Rightarrow> _) = max" 

25764  41 

60679  42 
instance 
43 
by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2) 

22483  44 

25764  45 
end 
46 

54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

47 
instantiation String.literal :: linorder 
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

48 
begin 
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

49 

63462  50 
context includes literal.lifting 
51 
begin 

52 

53 
lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" 

54 
is "ord.lexordp op <" . 

55 

56 
lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" 

57 
is "ord.lexordp_eq op <" . 

54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

58 

a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

59 
instance 
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

60 
proof  
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

61 
interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool" 
63462  62 
by (rule linorder.lexordp_linorder[where less_eq="op \<le>"]) unfold_locales 
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

63 
show "PROP ?thesis" 
63462  64 
by intro_classes (transfer, simp add: less_le_not_le linear)+ 
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

65 
qed 
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

66 

a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

67 
end 
63462  68 

55426
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
54863
diff
changeset

69 
end 
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

70 

63462  71 
lemma less_literal_code [code]: 
57437  72 
"op < = (\<lambda>xs ys. ord.lexordp op < (String.explode xs) (String.explode ys))" 
63462  73 
by (simp add: less_literal.rep_eq fun_eq_iff) 
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

74 

a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

75 
lemma less_eq_literal_code [code]: 
57437  76 
"op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))" 
63462  77 
by (simp add: less_eq_literal.rep_eq fun_eq_iff) 
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset

78 

55426
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
54863
diff
changeset

79 
lifting_update literal.lifting 
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
54863
diff
changeset

80 
lifting_forget literal.lifting 
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
54863
diff
changeset

81 

17200  82 
end 