src/HOL/ex/Chinese.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 24312 bb5ec06f7c7a
child 39246 9e58f0499f57
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     1 (* -*- coding: utf-8 -*- :encoding=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 imports Main begin
    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