author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 40967 | 5eb59b62e7de |
child 58249 | 180f1b3508ed |
permissions | -rw-r--r-- |
40967
5eb59b62e7de
avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle;
wenzelm
parents:
39246
diff
changeset
|
1 |
(* Author: Ning Zhang and Christian Urban |
17505 | 2 |
|
3 |
Example theory involving Unicode characters (UTF-8 encoding) -- both |
|
4 |
formal and informal ones. |
|
5 |
*) |
|
6 |
||
7 |
header {* A Chinese theory *} |
|
8 |
||
17553 | 9 |
theory Chinese imports Main begin |
17505 | 10 |
|
11 |
text{* 数学家能把咖啡变成理论,如今中国的数学家也可 |
|
12 |
以在伊莎贝拉的帮助下把茶变成理论. |
|
13 |
||
14 |
伊莎贝拉-世界数学家的新宠,现今能识别中文,成为 |
|
15 |
中国数学家理论推导的得力助手. |
|
16 |
||
17 |
*} |
|
18 |
||
19 |
datatype shuzi = |
|
20 |
One ("一") |
|
21 |
| Two ("二") |
|
22 |
| Three ("三") |
|
23 |
| Four ("四") |
|
24 |
| Five ("五") |
|
25 |
| Six ("六") |
|
26 |
| Seven ("七") |
|
27 |
| Eight ("八") |
|
28 |
| Nine ("九") |
|
29 |
| Ten ("十") |
|
30 |
||
39246 | 31 |
primrec translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100) where |
17505 | 32 |
"|一| = 1" |
39246 | 33 |
|"|二| = 2" |
34 |
|"|三| = 3" |
|
35 |
|"|四| = 4" |
|
36 |
|"|五| = 5" |
|
37 |
|"|六| = 6" |
|
38 |
|"|七| = 7" |
|
39 |
|"|八| = 8" |
|
40 |
|"|九| = 9" |
|
41 |
|"|十| = 10" |
|
17505 | 42 |
|
43 |
thm translate.simps |
|
44 |
||
45 |
lemma "|四| + |六| = |十|" |
|
46 |
by simp |
|
47 |
||
48 |
end |