src/HOL/ex/Chinese.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17553 d7b304d05956
child 24312 bb5ec06f7c7a
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
wenzelm@17505
     1
(* -*- coding: utf-8 -*-
wenzelm@17505
     2
    ID:         $Id$
wenzelm@17505
     3
    Author:     Ning Zhang and Christian Urban
wenzelm@17505
     4
wenzelm@17505
     5
Example theory involving Unicode characters (UTF-8 encoding) -- both
wenzelm@17505
     6
formal and informal ones.
wenzelm@17505
     7
*)
wenzelm@17505
     8
wenzelm@17505
     9
header {* A Chinese theory *}
wenzelm@17505
    10
wenzelm@17553
    11
theory Chinese imports Main begin
wenzelm@17505
    12
wenzelm@17505
    13
text{* 数学家能把咖啡变成理论,如今中国的数学家也可
wenzelm@17505
    14
       以在伊莎贝拉的帮助下把茶变成理论.  
wenzelm@17505
    15
wenzelm@17505
    16
       伊莎贝拉-世界数学家的新宠,现今能识别中文,成为
wenzelm@17505
    17
       中国数学家理论推导的得力助手.
wenzelm@17505
    18
wenzelm@17505
    19
    *}
wenzelm@17505
    20
wenzelm@17505
    21
datatype shuzi =
wenzelm@17505
    22
    One   ("一")
wenzelm@17505
    23
  | Two   ("二")
wenzelm@17505
    24
  | Three ("三") 
wenzelm@17505
    25
  | Four  ("四")
wenzelm@17505
    26
  | Five  ("五")
wenzelm@17505
    27
  | Six   ("六")
wenzelm@17505
    28
  | Seven ("七")
wenzelm@17505
    29
  | Eight ("八")
wenzelm@17505
    30
  | Nine  ("九")
wenzelm@17505
    31
  | Ten   ("十")
wenzelm@17505
    32
wenzelm@17505
    33
consts
wenzelm@17505
    34
  translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100)
wenzelm@17505
    35
wenzelm@17505
    36
primrec
wenzelm@17505
    37
 "|一| = 1"
wenzelm@17505
    38
 "|二| = 2"
wenzelm@17505
    39
 "|三| = 3"
wenzelm@17505
    40
 "|四| = 4"
wenzelm@17505
    41
 "|五| = 5"
wenzelm@17505
    42
 "|六| = 6"
wenzelm@17505
    43
 "|七| = 7"
wenzelm@17505
    44
 "|八| = 8"
wenzelm@17505
    45
 "|九| = 9"
wenzelm@17505
    46
 "|十| = 10"
wenzelm@17505
    47
wenzelm@17505
    48
thm translate.simps
wenzelm@17505
    49
wenzelm@17505
    50
lemma "|四| + |六| = |十|"
wenzelm@17505
    51
  by simp 
wenzelm@17505
    52
wenzelm@17505
    53
end