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