|
24312
|
1 |
(* -*- coding: utf-8 -*- :encoding=utf-8:
|
|
17505
|
2 |
ID: $Id$
|
|
|
3 |
Author: Ning Zhang and Christian Urban
|
|
|
4 |
|
|
|
5 |
Example theory involving Unicode characters (UTF-8 encoding) -- both
|
|
|
6 |
formal and informal ones.
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
header {* A Chinese theory *}
|
|
|
10 |
|
|
17553
|
11 |
theory Chinese imports Main begin
|
|
17505
|
12 |
|
|
|
13 |
text{* 数学家能把咖啡变成理论,如今中国的数学家也可
|
|
|
14 |
以在伊莎贝拉的帮助下把茶变成理论.
|
|
|
15 |
|
|
|
16 |
伊莎贝拉-世界数学家的新宠,现今能识别中文,成为
|
|
|
17 |
中国数学家理论推导的得力助手.
|
|
|
18 |
|
|
|
19 |
*}
|
|
|
20 |
|
|
|
21 |
datatype shuzi =
|
|
|
22 |
One ("一")
|
|
|
23 |
| Two ("二")
|
|
|
24 |
| Three ("三")
|
|
|
25 |
| Four ("四")
|
|
|
26 |
| Five ("五")
|
|
|
27 |
| Six ("六")
|
|
|
28 |
| Seven ("七")
|
|
|
29 |
| Eight ("八")
|
|
|
30 |
| Nine ("九")
|
|
|
31 |
| Ten ("十")
|
|
|
32 |
|
|
|
33 |
consts
|
|
|
34 |
translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100)
|
|
|
35 |
|
|
|
36 |
primrec
|
|
|
37 |
"|一| = 1"
|
|
|
38 |
"|二| = 2"
|
|
|
39 |
"|三| = 3"
|
|
|
40 |
"|四| = 4"
|
|
|
41 |
"|五| = 5"
|
|
|
42 |
"|六| = 6"
|
|
|
43 |
"|七| = 7"
|
|
|
44 |
"|八| = 8"
|
|
|
45 |
"|九| = 9"
|
|
|
46 |
"|十| = 10"
|
|
|
47 |
|
|
|
48 |
thm translate.simps
|
|
|
49 |
|
|
|
50 |
lemma "|四| + |六| = |十|"
|
|
|
51 |
by simp
|
|
|
52 |
|
|
|
53 |
end
|