src/HOL/Main.thy
author berghofe
Fri Apr 19 14:51:33 2002 +0200 (2002-04-19)
changeset 13093 ab0335307905
parent 12554 671b4d632c34
child 13367 ad307f0d80db
permissions -rw-r--r--
code generator: wfrec combinator is now implemented by ML function wf_rec.
nipkow@10519
     1
(*  Title:      HOL/Main.thy
nipkow@10519
     2
    ID:         $Id$
wenzelm@12024
     3
    Author:     Stefan Berghofer, Tobias Nipkow and Markus Wenzel, TU Muenchen
wenzelm@12024
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@10519
     5
*)
wenzelm@9619
     6
wenzelm@12024
     7
header {* Main HOL *}
wenzelm@12024
     8
wenzelm@12024
     9
theory Main = Map + Hilbert_Choice:
wenzelm@9650
    10
wenzelm@12024
    11
text {*
wenzelm@12024
    12
  Theory @{text Main} includes everything.  Note that theory @{text
wenzelm@12024
    13
  PreList} already includes most HOL theories.
wenzelm@12024
    14
*}
wenzelm@12024
    15
wenzelm@12024
    16
text {* Belongs to theory List. *}
wenzelm@10261
    17
declare lists_mono [mono]
wenzelm@10261
    18
declare map_cong [recdef_cong]
wenzelm@10386
    19
lemmas rev_induct [case_names Nil snoc] = rev_induct
wenzelm@10386
    20
  and rev_cases [case_names Nil snoc] = rev_exhaust
wenzelm@9768
    21
wenzelm@12024
    22
wenzelm@12024
    23
subsection {* Characters and strings *}
wenzelm@12024
    24
wenzelm@12024
    25
datatype nibble =
wenzelm@12024
    26
    Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
wenzelm@12024
    27
  | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
wenzelm@12024
    28
wenzelm@12024
    29
datatype char = Char nibble nibble
wenzelm@12024
    30
  -- "Note: canonical order of character encoding coincides with standard term ordering"
wenzelm@12024
    31
wenzelm@12024
    32
types string = "char list"
wenzelm@12024
    33
wenzelm@12024
    34
syntax
wenzelm@12024
    35
  "_Char" :: "xstr => char"    ("CHR _")
wenzelm@12024
    36
  "_String" :: "xstr => string"    ("_")
wenzelm@12024
    37
wenzelm@12024
    38
parse_ast_translation {*
wenzelm@12024
    39
  let
wenzelm@12024
    40
    val constants = Syntax.Appl o map Syntax.Constant;
wenzelm@12024
    41
wenzelm@12024
    42
    fun mk_nib n = "Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10));
wenzelm@12024
    43
    fun mk_char c =
wenzelm@12024
    44
      if Symbol.is_ascii c andalso Symbol.is_printable c then
wenzelm@12024
    45
        constants ["Char", mk_nib (ord c div 16), mk_nib (ord c mod 16)]
wenzelm@12024
    46
      else error ("Printable ASCII character expected: " ^ quote c);
wenzelm@12024
    47
wenzelm@12024
    48
    fun mk_string [] = Syntax.Constant "Nil"
wenzelm@12024
    49
      | mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs];
wenzelm@12024
    50
wenzelm@12024
    51
    fun char_ast_tr [Syntax.Variable xstr] =
wenzelm@12024
    52
        (case Syntax.explode_xstr xstr of
wenzelm@12024
    53
          [c] => mk_char c
wenzelm@12024
    54
        | _ => error ("Single character expected: " ^ xstr))
wenzelm@12024
    55
      | char_ast_tr asts = raise AST ("char_ast_tr", asts);
wenzelm@12024
    56
wenzelm@12024
    57
    fun string_ast_tr [Syntax.Variable xstr] =
wenzelm@12024
    58
        (case Syntax.explode_xstr xstr of
wenzelm@12024
    59
          [] => constants [Syntax.constrainC, "Nil", "string"]
wenzelm@12024
    60
        | cs => mk_string cs)
wenzelm@12024
    61
      | string_ast_tr asts = raise AST ("string_tr", asts);
wenzelm@12024
    62
  in [("_Char", char_ast_tr), ("_String", string_ast_tr)] end;
wenzelm@12024
    63
*}
wenzelm@12024
    64
wenzelm@12024
    65
print_ast_translation {*
wenzelm@12024
    66
  let
wenzelm@12024
    67
    fun dest_nib (Syntax.Constant c) =
wenzelm@12024
    68
        (case explode c of
wenzelm@12024
    69
          ["N", "i", "b", "b", "l", "e", h] =>
wenzelm@12024
    70
            if "0" <= h andalso h <= "9" then ord h - ord "0"
wenzelm@12024
    71
            else if "A" <= h andalso h <= "F" then ord h - ord "A" + 10
wenzelm@12024
    72
            else raise Match
wenzelm@12024
    73
        | _ => raise Match)
wenzelm@12024
    74
      | dest_nib _ = raise Match;
wenzelm@12024
    75
wenzelm@12024
    76
    fun dest_chr c1 c2 =
wenzelm@12024
    77
      let val c = chr (dest_nib c1 * 16 + dest_nib c2)
wenzelm@12024
    78
      in if Symbol.is_printable c then c else raise Match end;
wenzelm@12024
    79
wenzelm@12024
    80
    fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
wenzelm@12024
    81
      | dest_char _ = raise Match;
wenzelm@12024
    82
wenzelm@12024
    83
    fun xstr cs = Syntax.Appl [Syntax.Constant "_xstr", Syntax.Variable (Syntax.implode_xstr cs)];
wenzelm@12024
    84
wenzelm@12024
    85
    fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", xstr [dest_chr c1 c2]]
wenzelm@12024
    86
      | char_ast_tr' _ = raise Match;
wenzelm@12024
    87
wenzelm@12024
    88
    fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
wenzelm@12024
    89
            xstr (map dest_char (Syntax.unfold_ast "_args" args))]
wenzelm@12024
    90
      | list_ast_tr' ts = raise Match;
wenzelm@12024
    91
  in [("Char", char_ast_tr'), ("@list", list_ast_tr')] end;
wenzelm@12024
    92
*}
wenzelm@12024
    93
wenzelm@12024
    94
wenzelm@12024
    95
subsection {* Configuration of the code generator *}
berghofe@11533
    96
berghofe@11533
    97
types_code
berghofe@11533
    98
  "bool"  ("bool")
berghofe@12439
    99
  "*"     ("(_ */ _)")
berghofe@12439
   100
  "list"  ("_ list")
berghofe@11533
   101
berghofe@11533
   102
consts_code
berghofe@11533
   103
  "op ="    ("(_ =/ _)")
berghofe@11533
   104
berghofe@11533
   105
  "True"    ("true")
berghofe@11533
   106
  "False"   ("false")
berghofe@11533
   107
  "Not"     ("not")
berghofe@11533
   108
  "op |"    ("(_ orelse/ _)")
berghofe@11533
   109
  "op &"    ("(_ andalso/ _)")
berghofe@11533
   110
  "If"      ("(if _/ then _/ else _)")
berghofe@11533
   111
berghofe@11533
   112
  "Pair"    ("(_,/ _)")
berghofe@11533
   113
  "fst"     ("fst")
berghofe@11533
   114
  "snd"     ("snd")
berghofe@11533
   115
berghofe@11533
   116
  "Nil"     ("[]")
berghofe@11533
   117
  "Cons"    ("(_ ::/ _)")
berghofe@12439
   118
berghofe@13093
   119
  "wfrec"   ("wf'_rec?")
berghofe@13093
   120
berghofe@13093
   121
ML {* fun wf_rec f x = f (wf_rec f) x; *}
berghofe@13093
   122
berghofe@12554
   123
lemma [code]: "((n::nat) < 0) = False" by simp
berghofe@12554
   124
declare less_Suc_eq [code]
berghofe@12554
   125
wenzelm@9650
   126
end