# Theory Hebrew

Up to index of Isabelle/HOL/ex

theory Hebrew
imports Main
begin

    (* -*- coding: utf-8 -*-
        ID:         $Id: Hebrew.thy,v 1.2 2005/09/20 11:57:08 wenzelm Exp $
        Author:     Makarius

    Example theory involving Unicode characters (UTF-8 encoding) -- both
    formal and informal ones.
    *)

    header {* A Hebrew theory *}

    theory Hebrew
    imports Main
    begin

    text {* The Hebrew Alef-Bet (א-ב). *}

    datatype alef_bet =
        Alef    ("א")
      | Bet     ("ב")
      | Gimel   ("ג")
      | Dalet   ("ד")
      | He      ("ה")
      | Vav     ("ו")
      | Zayin   ("ז")
      | Het     ("ח")
      | Tet     ("ט")
      | Yod     ("י")
      | Kaf     ("כ")
      | Lamed   ("ל")
      | Mem     ("מ")
      | Nun     ("נ")
      | Samekh  ("ס")
      | Ayin    ("ע")
      | Pe      ("פ")
      | Tsadi   ("צ")
      | Qof     ("ק")
      | Resh    ("ר")
      | Shin    ("ש")
      | Tav     ("ת")

    thm alef_bet.induct

    text {* Interpreting Hebrew letters as numbers. *}

    consts
      mispar :: "alef_bet => nat"
    primrec
      "mispar א = 1"
      "mispar ב = 2"
      "mispar ג = 3"
      "mispar ד = 4"
      "mispar ה = 5"
      "mispar ו = 6"
      "mispar ז = 7"
      "mispar ח = 8"
      "mispar ט = 9"
      "mispar י = 10"
      "mispar כ = 20"
      "mispar ל = 30"
      "mispar מ = 40"
      "mispar נ = 50"
      "mispar ס = 60"
      "mispar ע = 70"
      "mispar פ = 80"
      "mispar צ = 90"
      "mispar ק = 100"
      "mispar ר = 200"
      "mispar ש = 300"
      "mispar ת = 400"

    thm mispar.simps

    lemma "mispar ק + mispar ל + mispar ה = 135"
      by simp

    end

lemma

      mispar ק + mispar ל + mispar ה = 135