Structure ASCIInumbersTheory


Source File Identifier index Theory binding index

signature ASCIInumbersTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val HEX_def_primitive : thm
    val UNHEX_def_primitive : 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 EVERY_isDigit_num_to_dec_string : thm
    val EVERY_isHexDigit_num_to_hex_string : thm
    val HEX_UNHEX : thm
    val HEX_def : thm
    val HEX_ind : thm
    val LENGTH_num_to_bin_string : thm
    val LENGTH_num_to_dec_string : thm
    val LENGTH_num_to_hex_string : thm
    val LENGTH_num_to_oct_string : 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 isDigit_HEX : thm
    val isHexDigit_HEX : thm
    val n2s_compute : thm
    val n2s_s2n : thm
    val num_bin_string : thm
    val num_dec_string : thm
    val num_from_X_string_leading_zeroes : thm
    val num_hex_string : thm
    val num_oct_string : thm
    val num_to_bin_string_nil : thm
    val num_to_dec_string_compute : thm
    val num_to_dec_string_nil : thm
    val num_to_hex_string_nil : thm
    val num_to_oct_string_nil : thm
    val s2n_compute : thm
    val s2n_leading_zeroes : 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_def_primitive]  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_def_primitive]  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 ∘ 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
   
   [EVERY_isDigit_num_to_dec_string]  Theorem
      
      ⊢ ∀n. EVERY isDigit (toString n)
   
   [EVERY_isHexDigit_num_to_hex_string]  Theorem
      
      ⊢ ∀n. EVERY (λc. isHexDigit c ∧ (isAlpha c ⇒ isUpper c))
              (num_to_hex_string n)
   
   [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
   
   [LENGTH_num_to_bin_string]  Theorem
      
      ⊢ STRLEN (num_to_bin_string n) = if n = 0 then 1 else LOG 2 n + 1
   
   [LENGTH_num_to_dec_string]  Theorem
      
      ⊢ STRLEN (toString n) = if n = 0 then 1 else LOG 10 n + 1
   
   [LENGTH_num_to_hex_string]  Theorem
      
      ⊢ STRLEN (num_to_hex_string n) = if n = 0 then 1 else LOG 16 n + 1
   
   [LENGTH_num_to_oct_string]  Theorem
      
      ⊢ STRLEN (num_to_oct_string n) = if n = 0 then 1 else LOG 8 n + 1
   
   [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
   
   [isDigit_HEX]  Theorem
      
      ⊢ ∀n. n < 10 ⇒ isDigit (HEX n)
   
   [isHexDigit_HEX]  Theorem
      
      ⊢ ∀n. n < 16 ⇒
            isHexDigit (HEX n) ∧ (isAlpha (HEX n) ⇒ isUpper (HEX n))
   
   [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 ∘ c2n) s ⇒
          n2s b n2c (s2n b c2n s) =
          if s2n b c2n s = 0 then STRING (n2c 0) ""
          else MAP (n2c ∘ c2n) (LASTN (SUC (LOG b (s2n b c2n s))) s)
   
   [num_bin_string]  Theorem
      
      ⊢ num_from_bin_string ∘ num_to_bin_string = I
   
   [num_dec_string]  Theorem
      
      ⊢ toNum ∘ toString = I
   
   [num_from_X_string_leading_zeroes]  Theorem
      
      ⊢ num_from_bin_string (STRING #"0" t) = num_from_bin_string t ∧
        num_from_oct_string (STRING #"0" t) = num_from_oct_string t ∧
        toNum (STRING #"0" t) = toNum t ∧
        num_from_hex_string (STRING #"0" t) = num_from_hex_string t
   
   [num_hex_string]  Theorem
      
      ⊢ num_from_hex_string ∘ num_to_hex_string = I
   
   [num_oct_string]  Theorem
      
      ⊢ num_from_oct_string ∘ num_to_oct_string = I
   
   [num_to_bin_string_nil]  Theorem
      
      ⊢ num_to_bin_string n ≠ ""
   
   [num_to_dec_string_compute]  Theorem
      
      ⊢ toString = n2lA "" HEX 10
   
   [num_to_dec_string_nil]  Theorem
      
      ⊢ toString n ≠ ""
   
   [num_to_hex_string_nil]  Theorem
      
      ⊢ num_to_hex_string n ≠ ""
   
   [num_to_oct_string_nil]  Theorem
      
      ⊢ num_to_oct_string n ≠ ""
   
   [s2n_compute]  Theorem
      
      ⊢ s2n b f s = l2n b (MAP f (REVERSE (EXPLODE s)))
   
   [s2n_leading_zeroes]  Theorem
      
      ⊢ 0 < b ⇒ s2n b UNHEX (STRING #"0" t) = s2n b UNHEX t
   
   [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, Trindemossen-1