# Theory StringEx

Up to index of Isabelle/HOL/ex

theory StringEx
imports Main
begin

    (* $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''}