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