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