(* $Id: StringEx.thy,v 1.6 2005/09/14 20:08:09 wenzelm Exp $ *) header {* String examples *} theory StringEx imports Main begin lemma "hd ''ABCD'' = CHR ''A''" by simp lemma "hd ''ABCD'' ≠ CHR ''B''" by simp lemma "''ABCD'' ≠ ''ABCX''" by simp lemma "''ABCD'' = ''ABCD''" by simp lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ≠ ''ABCDEFGHIJKLMNOPQRSTUVWXY''" by simp lemma "set ''Foobar'' = {CHR ''F'', CHR ''a'', CHR ''b'', CHR ''o'', CHR ''r''}" by (simp add: insert_commute) lemma "set ''Foobar'' = ?X" by (simp add: insert_commute) end
lemma
hd ''ABCD'' = CHR ''A''
lemma
hd ''ABCD'' ≠ CHR ''B''
lemma
''ABCD'' ≠ ''ABCX''
lemma
''ABCD'' = ''ABCD''
lemma
''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ≠ ''ABCDEFGHIJKLMNOPQRSTUVWXY''
lemma
set ''Foobar'' = {CHR ''F'', CHR ''a'', CHR ''b'', CHR ''o'', CHR ''r''}
lemma
set ''Foobar'' = {CHR ''F'', CHR ''a'', CHR ''b'', CHR ''o'', CHR ''r''}