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