src/HOL/Library/Char_ord.thy
changeset 68028 1f9f973eed2a
parent 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Library/Char_ord.thy	Tue Apr 24 14:17:57 2018 +0000
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Tue Apr 24 14:17:58 2018 +0000
     1.3 @@ -11,27 +11,29 @@
     1.4  instantiation char :: linorder
     1.5  begin
     1.6  
     1.7 -definition "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
     1.8 -definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
     1.9 +definition less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool"
    1.10 +  where "c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)"
    1.11 +
    1.12 +definition less_char :: "char \<Rightarrow> char \<Rightarrow> bool"
    1.13 +  where "c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)"
    1.14 +
    1.15  
    1.16  instance
    1.17    by standard (auto simp add: less_eq_char_def less_char_def)
    1.18  
    1.19  end
    1.20  
    1.21 -lemma less_eq_char_simps:
    1.22 -  "0 \<le> c"
    1.23 -  "Char k \<le> 0 \<longleftrightarrow> numeral k mod 256 = (0 :: nat)"
    1.24 -  "Char k \<le> Char l \<longleftrightarrow> numeral k mod 256 \<le> (numeral l mod 256 :: nat)"
    1.25 -  for c :: char
    1.26 -  by (simp_all add: Char_def less_eq_char_def)
    1.27 +lemma less_eq_char_simp [simp]:
    1.28 +  "Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
    1.29 +    \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
    1.30 +      \<le> foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
    1.31 +  by (simp add: less_eq_char_def)
    1.32  
    1.33 -lemma less_char_simps:
    1.34 -  "\<not> c < 0"
    1.35 -  "0 < Char k \<longleftrightarrow> (0 :: nat) < numeral k mod 256"
    1.36 -  "Char k < Char l \<longleftrightarrow> numeral k mod 256 < (numeral l mod 256 :: nat)"
    1.37 -  for c :: char
    1.38 -  by (simp_all add: Char_def less_char_def)
    1.39 +lemma less_char_simp [simp]:
    1.40 +  "Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
    1.41 +    \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
    1.42 +      < foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
    1.43 +  by (simp add: less_char_def)
    1.44  
    1.45  instantiation char :: distrib_lattice
    1.46  begin
    1.47 @@ -44,39 +46,4 @@
    1.48  
    1.49  end
    1.50  
    1.51 -instantiation String.literal :: linorder
    1.52 -begin
    1.53 -
    1.54 -context includes literal.lifting
    1.55 -begin
    1.56 -
    1.57 -lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
    1.58 -  is "ord.lexordp (<)" .
    1.59 -
    1.60 -lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
    1.61 -  is "ord.lexordp_eq (<)" .
    1.62 -
    1.63 -instance
    1.64 -proof -
    1.65 -  interpret linorder "ord.lexordp_eq (<)" "ord.lexordp (<) :: string \<Rightarrow> string \<Rightarrow> bool"
    1.66 -    by (rule linorder.lexordp_linorder[where less_eq="(\<le>)"]) unfold_locales
    1.67 -  show "PROP ?thesis"
    1.68 -    by intro_classes (transfer, simp add: less_le_not_le linear)+
    1.69 -qed
    1.70 -
    1.71  end
    1.72 -
    1.73 -end
    1.74 -
    1.75 -lemma less_literal_code [code]:
    1.76 -  "(<) = (\<lambda>xs ys. ord.lexordp (<) (String.explode xs) (String.explode ys))"
    1.77 -  by (simp add: less_literal.rep_eq fun_eq_iff)
    1.78 -
    1.79 -lemma less_eq_literal_code [code]:
    1.80 -  "(\<le>) = (\<lambda>xs ys. ord.lexordp_eq (<) (String.explode xs) (String.explode ys))"
    1.81 -  by (simp add: less_eq_literal.rep_eq fun_eq_iff)
    1.82 -
    1.83 -lifting_update literal.lifting
    1.84 -lifting_forget literal.lifting
    1.85 -
    1.86 -end