src/HOL/ex/StringEx.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17388 495c799df31d
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
wenzelm@17388
     1
(* $Id$ *)
wenzelm@11020
     2
wenzelm@11020
     3
header {* String examples *}
wenzelm@5199
     4
haftmann@16417
     5
theory StringEx imports Main begin
wenzelm@10916
     6
wenzelm@10916
     7
lemma "hd ''ABCD'' = CHR ''A''"
wenzelm@10916
     8
  by simp
wenzelm@10916
     9
wenzelm@10916
    10
lemma "hd ''ABCD'' \<noteq> CHR ''B''"
wenzelm@10916
    11
  by simp
wenzelm@10916
    12
wenzelm@10916
    13
lemma "''ABCD'' \<noteq> ''ABCX''"
wenzelm@10916
    14
  by simp
wenzelm@10916
    15
wenzelm@10916
    16
lemma "''ABCD'' = ''ABCD''"
wenzelm@10916
    17
  by simp
wenzelm@10916
    18
wenzelm@11586
    19
lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' \<noteq>
wenzelm@11586
    20
  ''ABCDEFGHIJKLMNOPQRSTUVWXY''"
wenzelm@10916
    21
  by simp
wenzelm@10916
    22
wenzelm@10916
    23
lemma "set ''Foobar'' = {CHR ''F'', CHR ''a'', CHR ''b'', CHR ''o'', CHR ''r''}"
wenzelm@10916
    24
  by (simp add: insert_commute)
wenzelm@10916
    25
wenzelm@10916
    26
lemma "set ''Foobar'' = ?X"
wenzelm@10916
    27
  by (simp add: insert_commute)
wenzelm@10916
    28
wenzelm@10916
    29
end