moved String theory to main HOL;
authorwenzelm
Fri Jul 03 17:33:47 1998 +0200 (1998-07-03)
changeset 51215c1f89ae8aef
parent 5120 f7f5442c934a
child 5122 229190f9f303
moved String theory to main HOL;
src/HOL/String.ML
src/HOL/String.thy
src/HOL/ex/String.ML
src/HOL/ex/String.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/String.ML	Fri Jul 03 17:33:47 1998 +0200
     1.3 @@ -0,0 +1,20 @@
     1.4 +Goal "hd(''ABCD'') = CHR ''A''";
     1.5 +by (Simp_tac 1);
     1.6 +result();
     1.7 +
     1.8 +Goal "hd(''ABCD'') ~= CHR ''B''";
     1.9 +by (Simp_tac 1);
    1.10 +result();
    1.11 +
    1.12 +Goal "''ABCD'' ~= ''ABCX''";
    1.13 +by (Simp_tac 1);
    1.14 +result();
    1.15 +
    1.16 +Goal "''ABCD'' = ''ABCD''";
    1.17 +by (Simp_tac 1);
    1.18 +result();
    1.19 +
    1.20 +Goal
    1.21 +  "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
    1.22 +by (Simp_tac 1);
    1.23 +result();
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/String.thy	Fri Jul 03 17:33:47 1998 +0200
     2.3 @@ -0,0 +1,87 @@
     2.4 +(*  Title:      HOL/String.thy
     2.5 +    ID:         $Id$
     2.6 +
     2.7 +Hex chars and strings.
     2.8 +*)
     2.9 +
    2.10 +String = List +
    2.11 +
    2.12 +datatype
    2.13 +  nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
    2.14 +         | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
    2.15 +
    2.16 +datatype
    2.17 +  char = Char nibble nibble
    2.18 +
    2.19 +types
    2.20 +  string = char list
    2.21 +
    2.22 +syntax
    2.23 +  "_Char"       :: xstr => char       ("CHR _")
    2.24 +  "_String"     :: xstr => string     ("_")
    2.25 +
    2.26 +end
    2.27 +
    2.28 +
    2.29 +ML
    2.30 +
    2.31 +local
    2.32 +
    2.33 +  (* chars *)
    2.34 +
    2.35 +  val zero = ord "0";
    2.36 +  val ten = ord "A" - 10;
    2.37 +
    2.38 +  fun mk_nib n =
    2.39 +    Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
    2.40 +
    2.41 +  fun dest_nib (Const (c, _)) =
    2.42 +        (case explode c of
    2.43 +          ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
    2.44 +        | _ => raise Match)
    2.45 +    | dest_nib _ = raise Match;
    2.46 +
    2.47 +  fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
    2.48 +
    2.49 +
    2.50 +  fun mk_char c =
    2.51 +    Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
    2.52 +
    2.53 +  fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
    2.54 +    | dest_char _ = raise Match;
    2.55 +
    2.56 +
    2.57 +  fun char_tr (*"_Char"*) [Free (xstr, _)] =
    2.58 +        (case Syntax.explode_xstr xstr of
    2.59 +          [c] => mk_char c
    2.60 +        | _ => error ("Single character expected: " ^ xstr))
    2.61 +    | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
    2.62 +
    2.63 +  fun char_tr' (*"Char"*) [t1, t2] =
    2.64 +        Syntax.const "_Char" $ Syntax.free (Syntax.implode_xstr [dest_nibs t1 t2])
    2.65 +    | char_tr' (*"Char"*) _ = raise Match;
    2.66 +
    2.67 +
    2.68 +  (* strings *)
    2.69 +
    2.70 +  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "[]" $ Syntax.const "string"
    2.71 +    | mk_string (t :: ts) = Syntax.const "op #" $ t $ mk_string ts;
    2.72 +
    2.73 +  fun dest_string (Const ("[]", _)) = []
    2.74 +    | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs
    2.75 +    | dest_string _ = raise Match;
    2.76 +
    2.77 +
    2.78 +  fun string_tr (*"_String"*) [Free (xstr, _)] =
    2.79 +        mk_string (map mk_char (Syntax.explode_xstr xstr))
    2.80 +    | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
    2.81 +
    2.82 +  fun cons_tr' (*"op #"*) [c, cs] =
    2.83 +        Syntax.const "_String" $
    2.84 +          Syntax.free (Syntax.implode_xstr (dest_char c :: dest_string cs))
    2.85 +    | cons_tr' (*"op #"*) ts = raise Match;
    2.86 +
    2.87 +in
    2.88 +  val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
    2.89 +  val print_translation = [("Char", char_tr'), ("op #", cons_tr')];
    2.90 +end;
     3.1 --- a/src/HOL/ex/String.ML	Fri Jul 03 11:02:01 1998 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,20 +0,0 @@
     3.4 -Goal "hd(''ABCD'') = CHR ''A''";
     3.5 -by (Simp_tac 1);
     3.6 -result();
     3.7 -
     3.8 -Goal "hd(''ABCD'') ~= CHR ''B''";
     3.9 -by (Simp_tac 1);
    3.10 -result();
    3.11 -
    3.12 -Goal "''ABCD'' ~= ''ABCX''";
    3.13 -by (Simp_tac 1);
    3.14 -result();
    3.15 -
    3.16 -Goal "''ABCD'' = ''ABCD''";
    3.17 -by (Simp_tac 1);
    3.18 -result();
    3.19 -
    3.20 -Goal
    3.21 -  "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
    3.22 -by (Simp_tac 1);
    3.23 -result();
     4.1 --- a/src/HOL/ex/String.thy	Fri Jul 03 11:02:01 1998 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,87 +0,0 @@
     4.4 -(*  Title:      HOL/String.thy
     4.5 -    ID:         $Id$
     4.6 -
     4.7 -Hex chars and strings.
     4.8 -*)
     4.9 -
    4.10 -String = List +
    4.11 -
    4.12 -datatype
    4.13 -  nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
    4.14 -         | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
    4.15 -
    4.16 -datatype
    4.17 -  char = Char nibble nibble
    4.18 -
    4.19 -types
    4.20 -  string = char list
    4.21 -
    4.22 -syntax
    4.23 -  "_Char"       :: xstr => char       ("CHR _")
    4.24 -  "_String"     :: xstr => string     ("_")
    4.25 -
    4.26 -end
    4.27 -
    4.28 -
    4.29 -ML
    4.30 -
    4.31 -local
    4.32 -
    4.33 -  (* chars *)
    4.34 -
    4.35 -  val zero = ord "0";
    4.36 -  val ten = ord "A" - 10;
    4.37 -
    4.38 -  fun mk_nib n =
    4.39 -    Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
    4.40 -
    4.41 -  fun dest_nib (Const (c, _)) =
    4.42 -        (case explode c of
    4.43 -          ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
    4.44 -        | _ => raise Match)
    4.45 -    | dest_nib _ = raise Match;
    4.46 -
    4.47 -  fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
    4.48 -
    4.49 -
    4.50 -  fun mk_char c =
    4.51 -    Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
    4.52 -
    4.53 -  fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
    4.54 -    | dest_char _ = raise Match;
    4.55 -
    4.56 -
    4.57 -  fun char_tr (*"_Char"*) [Free (xstr, _)] =
    4.58 -        (case Syntax.explode_xstr xstr of
    4.59 -          [c] => mk_char c
    4.60 -        | _ => error ("Single character expected: " ^ xstr))
    4.61 -    | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
    4.62 -
    4.63 -  fun char_tr' (*"Char"*) [t1, t2] =
    4.64 -        Syntax.const "_Char" $ Syntax.free (Syntax.implode_xstr [dest_nibs t1 t2])
    4.65 -    | char_tr' (*"Char"*) _ = raise Match;
    4.66 -
    4.67 -
    4.68 -  (* strings *)
    4.69 -
    4.70 -  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "[]" $ Syntax.const "string"
    4.71 -    | mk_string (t :: ts) = Syntax.const "op #" $ t $ mk_string ts;
    4.72 -
    4.73 -  fun dest_string (Const ("[]", _)) = []
    4.74 -    | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs
    4.75 -    | dest_string _ = raise Match;
    4.76 -
    4.77 -
    4.78 -  fun string_tr (*"_String"*) [Free (xstr, _)] =
    4.79 -        mk_string (map mk_char (Syntax.explode_xstr xstr))
    4.80 -    | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
    4.81 -
    4.82 -  fun cons_tr' (*"op #"*) [c, cs] =
    4.83 -        Syntax.const "_String" $
    4.84 -          Syntax.free (Syntax.implode_xstr (dest_char c :: dest_string cs))
    4.85 -    | cons_tr' (*"op #"*) ts = raise Match;
    4.86 -
    4.87 -in
    4.88 -  val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
    4.89 -  val print_translation = [("Char", char_tr'), ("op #", cons_tr')];
    4.90 -end;