src/HOL/ex/Chinese.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 40967 5eb59b62e7de
child 58249 180f1b3508ed
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Author:     Ning Zhang and Christian Urban
     2 
     3 Example theory involving Unicode characters (UTF-8 encoding) -- both
     4 formal and informal ones.
     5 *)
     6 
     7 header {* A Chinese theory *}
     8 
     9 theory Chinese imports Main begin
    10 
    11 text{* 数学家能把咖啡变成理论,如今中国的数学家也可
    12        以在伊莎贝拉的帮助下把茶变成理论.  
    13 
    14        伊莎贝拉-世界数学家的新宠,现今能识别中文,成为
    15        中国数学家理论推导的得力助手.
    16 
    17     *}
    18 
    19 datatype shuzi =
    20     One   ("一")
    21   | Two   ("二")
    22   | Three ("三") 
    23   | Four  ("四")
    24   | Five  ("五")
    25   | Six   ("六")
    26   | Seven ("七")
    27   | Eight ("八")
    28   | Nine  ("九")
    29   | Ten   ("十")
    30 
    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"
    42 
    43 thm translate.simps
    44 
    45 lemma "|四| + |六| = |十|"
    46   by simp 
    47 
    48 end