src/HOL/ex/Chinese.thy
changeset 17505 928bd7053d6a
child 17553 d7b304d05956
equal deleted inserted replaced
17504:cc10c4b64b8e 17505:928bd7053d6a
       
     1 (* -*- coding: utf-8 -*-
       
     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 
       
    11 theory Chinese = Main:
       
    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