| author | wenzelm |
| Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) | |
| changeset 58889 | 5b7a9633cfa8 |
| parent 58310 | 91ea607a34d8 |
| child 61343 | 5b5656a63bd6 |
| permissions | -rw-r--r-- |
1 (* Author: Ning Zhang and Christian Urban
3 Example theory involving Unicode characters (UTF-8 encoding) -- both
4 formal and informal ones.
5 *)
7 section {* A Chinese theory *}
9 theory Chinese imports Main begin
11 text{* 数学家能把咖啡变成理论,如今中国的数学家也可
12 以在伊莎贝拉的帮助下把茶变成理论.
14 伊莎贝拉-世界数学家的新宠,现今能识别中文,成为
15 中国数学家理论推导的得力助手.
17 *}
19 datatype shuzi =
20 One ("一")
21 | Two ("二")
22 | Three ("三")
23 | Four ("四")
24 | Five ("五")
25 | Six ("六")
26 | Seven ("七")
27 | Eight ("八")
28 | Nine ("九")
29 | Ten ("十")
31 primrec translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100) where
32 "|一| = 1"
33 |"|二| = 2"
34 |"|三| = 3"
35 |"|四| = 4"
36 |"|五| = 5"
37 |"|六| = 6"
38 |"|七| = 7"
39 |"|八| = 8"
40 |"|九| = 9"
41 |"|十| = 10"
43 thm translate.simps
45 lemma "|四| + |六| = |十|"
46 by simp
48 end