Structure ASCIInumbersTheory


Source File Identifier index Theory binding index

signature ASCIInumbersTheory =
sig
  type thm = Thm.thm

  (*  Definitions  *)
    val HEX_primitive_def : thm
    val UNHEX_primitive_def : thm
    val fromBinString_def : thm
    val fromDecString_def : thm
    val fromHexString_def : thm
    val n2s_def : thm
    val num_from_bin_string_def : thm
    val num_from_dec_string_def : thm
    val num_from_hex_string_def : thm
    val num_from_oct_string_def : thm
    val num_to_bin_string_def : thm
    val num_to_dec_string_def : thm
    val num_to_hex_string_def : thm
    val num_to_oct_string_def : thm
    val s2n_def : thm

  (*  Theorems  *)
    val BIT_num_from_bin_string : thm
    val DEC_UNDEC : thm
    val HEX_UNHEX : thm
    val HEX_def : thm
    val HEX_ind : thm
    val STRCAT_toString_inj : thm
    val SUB_num_to_bin_string : thm
    val UNHEX_HEX : thm
    val UNHEX_def : thm
    val UNHEX_ind : thm
    val n2s_compute : thm
    val n2s_s2n : thm
    val num_bin_string : thm
    val num_dec_string : thm
    val num_hex_string : thm
    val num_oct_string : thm
    val s2n_compute : thm
    val s2n_n2s : thm
    val toNum_toString : thm
    val toString_11 : thm
    val toString_inj : thm
    val toString_toNum_cancel : thm

  val ASCIInumbers_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [numposrep] Parent theory of "ASCIInumbers"

   [string] Parent theory of "ASCIInumbers"

   [HEX_primitive_def]  Definition

      |- HEX =
         WFREC (@R. WF R)
           (λHEX a.
              case a of
                0 => I #"0"
              | 1 => I #"1"
              | 2 => I #"2"
              | 3 => I #"3"
              | 4 => I #"4"
              | 5 => I #"5"
              | 6 => I #"6"
              | 7 => I #"7"
              | 8 => I #"8"
              | 9 => I #"9"
              | 10 => I #"A"
              | 11 => I #"B"
              | 12 => I #"C"
              | 13 => I #"D"
              | 14 => I #"E"
              | 15 => I #"F"
              | v => ARB)

   [UNHEX_primitive_def]  Definition

      |- UNHEX =
         WFREC (@R. WF R)
           (λUNHEX a.
              case a of
                #"0" => I 0
              | #"1" => I 1
              | #"2" => I 2
              | #"3" => I 3
              | #"4" => I 4
              | #"5" => I 5
              | #"6" => I 6
              | #"7" => I 7
              | #"8" => I 8
              | #"9" => I 9
              | #"a" => I 10
              | #"b" => I 11
              | #"c" => I 12
              | #"d" => I 13
              | #"e" => I 14
              | #"f" => I 15
              | #"A" => I 10
              | #"B" => I 11
              | #"C" => I 12
              | #"D" => I 13
              | #"E" => I 14
              | #"F" => I 15
              | v => ARB)

   [fromBinString_def]  Definition

      |- ∀s.
           fromBinString s =
           if s ≠ "" ∧ EVERY (λc. (c = #"0") ∨ (c = #"1")) s then
             SOME (num_from_bin_string s)
           else NONE

   [fromDecString_def]  Definition

      |- ∀s.
           fromDecString s =
           if s ≠ "" ∧ EVERY isDigit s then SOME (toNum s) else NONE

   [fromHexString_def]  Definition

      |- ∀s.
           fromHexString s =
           if s ≠ "" ∧ EVERY isHexDigit s then SOME (num_from_hex_string s)
           else NONE

   [n2s_def]  Definition

      |- ∀b f n. n2s b f n = REVERSE (MAP f (n2l b n))

   [num_from_bin_string_def]  Definition

      |- num_from_bin_string = s2n 2 UNHEX

   [num_from_dec_string_def]  Definition

      |- toNum = s2n 10 UNHEX

   [num_from_hex_string_def]  Definition

      |- num_from_hex_string = s2n 16 UNHEX

   [num_from_oct_string_def]  Definition

      |- num_from_oct_string = s2n 8 UNHEX

   [num_to_bin_string_def]  Definition

      |- num_to_bin_string = n2s 2 HEX

   [num_to_dec_string_def]  Definition

      |- toString = n2s 10 HEX

   [num_to_hex_string_def]  Definition

      |- num_to_hex_string = n2s 16 HEX

   [num_to_oct_string_def]  Definition

      |- num_to_oct_string = n2s 8 HEX

   [s2n_def]  Definition

      |- ∀b f s. s2n b f s = l2n b (MAP f (REVERSE s))

   [BIT_num_from_bin_string]  Theorem

      |- ∀x s.
           EVERY ($> 2 o UNHEX) s ∧ x < STRLEN s ⇒
           (BIT x (num_from_bin_string s) ⇔
            (UNHEX (SUB (s,PRE (STRLEN s − x))) = 1))

   [DEC_UNDEC]  Theorem

      |- ∀c. isDigit c ⇒ (HEX (UNHEX c) = c)

   [HEX_UNHEX]  Theorem

      |- ∀c. isHexDigit c ⇒ (HEX (UNHEX c) = toUpper c)

   [HEX_def]  Theorem

      |- (HEX 0 = #"0") ∧ (HEX 1 = #"1") ∧ (HEX 2 = #"2") ∧
         (HEX 3 = #"3") ∧ (HEX 4 = #"4") ∧ (HEX 5 = #"5") ∧
         (HEX 6 = #"6") ∧ (HEX 7 = #"7") ∧ (HEX 8 = #"8") ∧
         (HEX 9 = #"9") ∧ (HEX 10 = #"A") ∧ (HEX 11 = #"B") ∧
         (HEX 12 = #"C") ∧ (HEX 13 = #"D") ∧ (HEX 14 = #"E") ∧
         (HEX 15 = #"F")

   [HEX_ind]  Theorem

      |- ∀P.
           P 0 ∧ P 1 ∧ P 2 ∧ P 3 ∧ P 4 ∧ P 5 ∧ P 6 ∧ P 7 ∧ P 8 ∧ P 9 ∧
           P 10 ∧ P 11 ∧ P 12 ∧ P 13 ∧ P 14 ∧ P 15 ∧ (∀v18. P v18) ⇒
           ∀v. P v

   [STRCAT_toString_inj]  Theorem

      |- ∀n m s. (STRCAT s (toString n) = STRCAT s (toString m)) ⇔ (n = m)

   [SUB_num_to_bin_string]  Theorem

      |- ∀x n.
           x < STRLEN (num_to_bin_string n) ⇒
           (SUB (num_to_bin_string n,x) =
            HEX (BITV n (PRE (STRLEN (num_to_bin_string n) − x))))

   [UNHEX_HEX]  Theorem

      |- ∀n. n < 16 ⇒ (UNHEX (HEX n) = n)

   [UNHEX_def]  Theorem

      |- (UNHEX #"0" = 0) ∧ (UNHEX #"1" = 1) ∧ (UNHEX #"2" = 2) ∧
         (UNHEX #"3" = 3) ∧ (UNHEX #"4" = 4) ∧ (UNHEX #"5" = 5) ∧
         (UNHEX #"6" = 6) ∧ (UNHEX #"7" = 7) ∧ (UNHEX #"8" = 8) ∧
         (UNHEX #"9" = 9) ∧ (UNHEX #"a" = 10) ∧ (UNHEX #"b" = 11) ∧
         (UNHEX #"c" = 12) ∧ (UNHEX #"d" = 13) ∧ (UNHEX #"e" = 14) ∧
         (UNHEX #"f" = 15) ∧ (UNHEX #"A" = 10) ∧ (UNHEX #"B" = 11) ∧
         (UNHEX #"C" = 12) ∧ (UNHEX #"D" = 13) ∧ (UNHEX #"E" = 14) ∧
         (UNHEX #"F" = 15)

   [UNHEX_ind]  Theorem

      |- ∀P.
           P #"0" ∧ P #"1" ∧ P #"2" ∧ P #"3" ∧ P #"4" ∧ P #"5" ∧ P #"6" ∧
           P #"7" ∧ P #"8" ∧ P #"9" ∧ P #"a" ∧ P #"b" ∧ P #"c" ∧ P #"d" ∧
           P #"e" ∧ P #"f" ∧ P #"A" ∧ P #"B" ∧ P #"C" ∧ P #"D" ∧ P #"E" ∧
           P #"F" ∧ (∀v24. P v24) ⇒
           ∀v. P v

   [n2s_compute]  Theorem

      |- n2s b f n = IMPLODE (REVERSE (MAP f (n2l b n)))

   [n2s_s2n]  Theorem

      |- ∀c2n n2c b s.
           1 < b ∧ EVERY ($> b o c2n) s ⇒
           (n2s b n2c (s2n b c2n s) =
            if s2n b c2n s = 0 then STRING (n2c 0) ""
            else MAP (n2c o c2n) (LASTN (SUC (LOG b (s2n b c2n s))) s))

   [num_bin_string]  Theorem

      |- num_from_bin_string o num_to_bin_string = I

   [num_dec_string]  Theorem

      |- toNum o toString = I

   [num_hex_string]  Theorem

      |- num_from_hex_string o num_to_hex_string = I

   [num_oct_string]  Theorem

      |- num_from_oct_string o num_to_oct_string = I

   [s2n_compute]  Theorem

      |- s2n b f s = l2n b (MAP f (REVERSE (EXPLODE s)))

   [s2n_n2s]  Theorem

      |- ∀c2n n2c b n.
           1 < b ∧ (∀x. x < b ⇒ (c2n (n2c x) = x)) ⇒
           (s2n b c2n (n2s b n2c n) = n)

   [toNum_toString]  Theorem

      |- ∀n. toNum (toString n) = n

   [toString_11]  Theorem

      |- ∀n m. (toString n = toString m) ⇔ (n = m)

   [toString_inj]  Theorem

      |- ∀n m. (toString n = toString m) ⇔ (n = m)

   [toString_toNum_cancel]  Theorem

      |- ∀n. toNum (toString n) = n


*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-10