1(*  Author:     Ning Zhang and Christian Urban
2
3Example theory involving Unicode characters (UTF-8 encoding) -- both
4formal and informal ones.
5*)
6
7section \<open>A Chinese theory\<close>
8
9theory Chinese imports Main begin
10
11text\<open>���������������������������������,������������������������������
12       ������������������������������������������������.  
13
14       ������������-������������������������,���������������������,������
15       ������������������������������������������.
16
17\<close>
18
19datatype shuzi =
20    One   ("���")
21  | Two   ("���")
22  | Three ("���") 
23  | Four  ("���")
24  | Five  ("���")
25  | Six   ("���")
26  | Seven ("���")
27  | Eight ("���")
28  | Nine  ("���")
29  | Ten   ("���")
30
31primrec 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"
42
43thm translate.simps
44
45lemma "|���| + |���| = |���|"
46  by simp 
47
48end
49