Theory Lem_string_extra

chapter ‹Generated by Lem from ‹string_extra.lem›.›

theory "Lem_string_extra" 

imports
  Main
  "Lem_num"
  "Lem_list"
  "Lem_basic_classes"
  "Lem_string"
  "Lem_list_extra"

begin 

― ‹‹****************************************************************************››
― ‹‹ String functions                                                           ››
― ‹‹****************************************************************************››

― ‹‹open import Basic_classes››
― ‹‹open import Num››
― ‹‹open import List››
― ‹‹open import String››
― ‹‹open import List_extra››
― ‹‹open import {hol} `stringLib`››
― ‹‹open import {hol} `ASCIInumbersTheory`››


― ‹‹****************************************************************************››
― ‹‹ Character's to numbers                                                     ››
― ‹‹****************************************************************************››

― ‹‹val ord : char -> nat››

― ‹‹val chr : nat -> char››

― ‹‹****************************************************************************››
― ‹‹ Converting to strings                                                      ››
― ‹‹****************************************************************************››

― ‹‹val stringFromNatHelper : nat -> list char -> list char››
fun  stringFromNatHelper  :: " nat ⇒(char)list ⇒(char)list "  where 
     " stringFromNatHelper n acc1 = (
  if n =( 0 :: nat) then
    acc1
  else
    stringFromNatHelper (n div( 10 :: nat)) ((%n. char_of (n::nat)) ((n mod( 10 :: nat)) +( 48 :: nat)) # acc1))"


― ‹‹val stringFromNat : nat -> string››
definition stringFromNat  :: " nat ⇒ string "  where 
     " stringFromNat n = ( 
  if n =( 0 :: nat) then (''0'') else  (stringFromNatHelper n []))"


― ‹‹val stringFromNaturalHelper : natural -> list char -> list char››
fun  stringFromNaturalHelper  :: " nat ⇒(char)list ⇒(char)list "  where 
     " stringFromNaturalHelper n acc1 = (
  if n =( 0 :: nat) then
    acc1
  else
    stringFromNaturalHelper (n div( 10 :: nat)) ((%n. char_of (n::nat)) ( ((n mod( 10 :: nat)) +( 48 :: nat))) # acc1))"


― ‹‹val stringFromNatural : natural -> string››
definition stringFromNatural  :: " nat ⇒ string "  where 
     " stringFromNatural n = ( 
  if n =( 0 :: nat) then (''0'') else  (stringFromNaturalHelper n []))"


― ‹‹val stringFromInt : int -> string››
definition stringFromInt  :: " int ⇒ string "  where 
     " stringFromInt i = ( 
  if i <( 0 :: int) then 
    (''-'') @ stringFromNat (nat (abs i))
  else
    stringFromNat (nat (abs i)))"


― ‹‹val stringFromInteger : integer -> string››
definition stringFromInteger  :: " int ⇒ string "  where 
     " stringFromInteger i = ( 
  if i <( 0 :: int) then 
    (''-'') @ stringFromNatural (nat (abs i))
  else
    stringFromNatural (nat (abs i)))"



― ‹‹****************************************************************************››
― ‹‹ List-like operations                                                       ››
― ‹‹****************************************************************************››

― ‹‹val nth : string -> nat -> char››
definition nth  :: " string ⇒ nat ⇒ char "  where 
     " nth s n = ( List.nth ( s) n )"


― ‹‹val stringConcat : list string -> string››
definition stringConcat  :: "(string)list ⇒ string "  where 
     " stringConcat s = (
  List.foldr (@) s (''''))"


― ‹‹****************************************************************************››
― ‹‹ String comparison                                                          ››
― ‹‹****************************************************************************››

― ‹‹val stringCompare : string -> string -> ordering››

definition stringLess  :: " string ⇒ string ⇒ bool "  where 
     " stringLess x y = ( orderingIsLess (EQ))"

definition stringLessEq  :: " string ⇒ string ⇒ bool "  where 
     " stringLessEq x y = ( ¬ (orderingIsGreater (EQ)))"

definition stringGreater  :: " string ⇒ string ⇒ bool "  where 
     " stringGreater x y = ( stringLess y x )"

definition stringGreaterEq  :: " string ⇒ string ⇒ bool "  where 
     " stringGreaterEq x y = ( stringLessEq y x )"


definition instance_Basic_classes_Ord_string_dict  :: "(string)Ord_class "  where 
     " instance_Basic_classes_Ord_string_dict = ((|

  compare_method = (λ x y. EQ),

  isLess_method = stringLess,

  isLessEqual_method = stringLessEq,

  isGreater_method = stringGreater,

  isGreaterEqual_method = stringGreaterEq |) )"

 
end