src/HOL/Library/Char_ord.thy
author haftmann
Sat Mar 12 22:04:52 2016 +0100 (2016-03-12)
changeset 62597 b3f2b8c906a6
parent 61076 bdc1e2f0a86a
child 63462 c1fe30f2bc32
permissions -rw-r--r--
model characters directly as range 0..255
* * *
operate on syntax terms rather than asts
nipkow@15737
     1
(*  Title:      HOL/Library/Char_ord.thy
haftmann@22805
     2
    Author:     Norbert Voelker, Florian Haftmann
nipkow@15737
     3
*)
nipkow@15737
     4
wenzelm@60500
     5
section \<open>Order on characters\<close>
nipkow@15737
     6
nipkow@15737
     7
theory Char_ord
haftmann@51160
     8
imports Main
nipkow@15737
     9
begin
nipkow@15737
    10
haftmann@25764
    11
instantiation char :: linorder
haftmann@25764
    12
begin
haftmann@25764
    13
wenzelm@60679
    14
definition "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
wenzelm@60679
    15
definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
haftmann@25764
    16
wenzelm@60679
    17
instance
haftmann@62597
    18
  by standard (auto simp add: less_eq_char_def less_char_def)
haftmann@22805
    19
haftmann@25764
    20
end
nipkow@15737
    21
haftmann@62597
    22
lemma less_eq_char_simps:
haftmann@62597
    23
  "(0 :: char) \<le> c"
haftmann@62597
    24
  "Char k \<le> 0 \<longleftrightarrow> numeral k mod 256 = (0 :: nat)"
haftmann@62597
    25
  "Char k \<le> Char l \<longleftrightarrow> numeral k mod 256 \<le> (numeral l mod 256 :: nat)"
haftmann@62597
    26
  by (simp_all add: Char_def less_eq_char_def)
haftmann@51160
    27
haftmann@62597
    28
lemma less_char_simps:
haftmann@62597
    29
  "\<not> c < (0 :: char)"
haftmann@62597
    30
  "0 < Char k \<longleftrightarrow> (0 :: nat) < numeral k mod 256"
haftmann@62597
    31
  "Char k < Char l \<longleftrightarrow> numeral k mod 256 < (numeral l mod 256 :: nat)"
haftmann@62597
    32
  by (simp_all add: Char_def less_char_def)
haftmann@62597
    33
  
haftmann@25764
    34
instantiation char :: distrib_lattice
haftmann@25764
    35
begin
haftmann@25764
    36
wenzelm@61076
    37
definition "(inf :: char \<Rightarrow> _) = min"
wenzelm@61076
    38
definition "(sup :: char \<Rightarrow> _) = max"
haftmann@25764
    39
wenzelm@60679
    40
instance
wenzelm@60679
    41
  by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
haftmann@22483
    42
haftmann@25764
    43
end
haftmann@25764
    44
Andreas@54595
    45
instantiation String.literal :: linorder
Andreas@54595
    46
begin
Andreas@54595
    47
Andreas@55426
    48
context includes literal.lifting begin
Andreas@54595
    49
lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
Andreas@54595
    50
lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
Andreas@54595
    51
Andreas@54595
    52
instance
Andreas@54595
    53
proof -
Andreas@54595
    54
  interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool"
Andreas@54595
    55
    by(rule linorder.lexordp_linorder[where less_eq="op \<le>"])(unfold_locales)
Andreas@54595
    56
  show "PROP ?thesis"
Andreas@54595
    57
    by(intro_classes)(transfer, simp add: less_le_not_le linear)+
Andreas@54595
    58
qed
Andreas@54595
    59
Andreas@54595
    60
end
Andreas@55426
    61
end
Andreas@54595
    62
Andreas@54595
    63
lemma less_literal_code [code]: 
haftmann@57437
    64
  "op < = (\<lambda>xs ys. ord.lexordp op < (String.explode xs) (String.explode ys))"
Andreas@54595
    65
by(simp add: less_literal.rep_eq fun_eq_iff)
Andreas@54595
    66
Andreas@54595
    67
lemma less_eq_literal_code [code]:
haftmann@57437
    68
  "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))"
Andreas@54595
    69
by(simp add: less_eq_literal.rep_eq fun_eq_iff)
Andreas@54595
    70
Andreas@55426
    71
lifting_update literal.lifting
Andreas@55426
    72
lifting_forget literal.lifting
Andreas@55426
    73
wenzelm@17200
    74
end