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