src/HOL/ex/StringEx.thy
author kleing
Sat, 01 Mar 2003 16:45:51 +0100
changeset 13840 399c8103a98f
parent 11586 d8a7f6318457
child 16417 9bc16273c2d4
permissions -rw-r--r--
keep a copy of generated files in repository
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11020
wenzelm
parents: 10916
diff changeset
     1
wenzelm
parents: 10916
diff changeset
     2
header {* String examples *}
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     3
10916
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
     4
theory StringEx = Main:
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
     5
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
     6
lemma "hd ''ABCD'' = CHR ''A''"
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
     7
  by simp
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
     8
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
     9
lemma "hd ''ABCD'' \<noteq> CHR ''B''"
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    10
  by simp
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    11
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    12
lemma "''ABCD'' \<noteq> ''ABCX''"
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    13
  by simp
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    14
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    15
lemma "''ABCD'' = ''ABCD''"
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    16
  by simp
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    17
11586
wenzelm
parents: 11020
diff changeset
    18
lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' \<noteq>
wenzelm
parents: 11020
diff changeset
    19
  ''ABCDEFGHIJKLMNOPQRSTUVWXY''"
10916
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    20
  by simp
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    21
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    22
lemma "set ''Foobar'' = {CHR ''F'', CHR ''a'', CHR ''b'', CHR ''o'', CHR ''r''}"
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    23
  by (simp add: insert_commute)
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    24
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    25
lemma "set ''Foobar'' = ?X"
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    26
  by (simp add: insert_commute)
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    27
df4a70b6ad7b tuned examples;
wenzelm
parents: 5199
diff changeset
    28
end