src/HOL/Library/Char_ord.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (19 months ago)
changeset 67951 655aa11359dc
parent 67399 eab6ce8368fa
child 68028 1f9f973eed2a
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
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
wenzelm@63462
     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:
wenzelm@63462
    23
  "0 \<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)"
wenzelm@63462
    26
  for c :: char
haftmann@62597
    27
  by (simp_all add: Char_def less_eq_char_def)
haftmann@51160
    28
haftmann@62597
    29
lemma less_char_simps:
wenzelm@63462
    30
  "\<not> c < 0"
haftmann@62597
    31
  "0 < Char k \<longleftrightarrow> (0 :: nat) < numeral k mod 256"
haftmann@62597
    32
  "Char k < Char l \<longleftrightarrow> numeral k mod 256 < (numeral l mod 256 :: nat)"
wenzelm@63462
    33
  for c :: char
haftmann@62597
    34
  by (simp_all add: Char_def less_char_def)
wenzelm@63462
    35
haftmann@25764
    36
instantiation char :: distrib_lattice
haftmann@25764
    37
begin
haftmann@25764
    38
wenzelm@61076
    39
definition "(inf :: char \<Rightarrow> _) = min"
wenzelm@61076
    40
definition "(sup :: char \<Rightarrow> _) = max"
haftmann@25764
    41
wenzelm@60679
    42
instance
wenzelm@60679
    43
  by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
haftmann@22483
    44
haftmann@25764
    45
end
haftmann@25764
    46
Andreas@54595
    47
instantiation String.literal :: linorder
Andreas@54595
    48
begin
Andreas@54595
    49
wenzelm@63462
    50
context includes literal.lifting
wenzelm@63462
    51
begin
wenzelm@63462
    52
wenzelm@63462
    53
lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
nipkow@67399
    54
  is "ord.lexordp (<)" .
wenzelm@63462
    55
wenzelm@63462
    56
lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
nipkow@67399
    57
  is "ord.lexordp_eq (<)" .
Andreas@54595
    58
Andreas@54595
    59
instance
Andreas@54595
    60
proof -
nipkow@67399
    61
  interpret linorder "ord.lexordp_eq (<)" "ord.lexordp (<) :: string \<Rightarrow> string \<Rightarrow> bool"
nipkow@67399
    62
    by (rule linorder.lexordp_linorder[where less_eq="(\<le>)"]) unfold_locales
Andreas@54595
    63
  show "PROP ?thesis"
wenzelm@63462
    64
    by intro_classes (transfer, simp add: less_le_not_le linear)+
Andreas@54595
    65
qed
Andreas@54595
    66
Andreas@54595
    67
end
wenzelm@63462
    68
Andreas@55426
    69
end
Andreas@54595
    70
wenzelm@63462
    71
lemma less_literal_code [code]:
nipkow@67399
    72
  "(<) = (\<lambda>xs ys. ord.lexordp (<) (String.explode xs) (String.explode ys))"
wenzelm@63462
    73
  by (simp add: less_literal.rep_eq fun_eq_iff)
Andreas@54595
    74
Andreas@54595
    75
lemma less_eq_literal_code [code]:
nipkow@67399
    76
  "(\<le>) = (\<lambda>xs ys. ord.lexordp_eq (<) (String.explode xs) (String.explode ys))"
wenzelm@63462
    77
  by (simp add: less_eq_literal.rep_eq fun_eq_iff)
Andreas@54595
    78
Andreas@55426
    79
lifting_update literal.lifting
Andreas@55426
    80
lifting_forget literal.lifting
Andreas@55426
    81
wenzelm@17200
    82
end