1 files changed, 124 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lem_string_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_string_extraScript.sml
new file mode 100644
index 00000000..0801601a
--- /dev/null
+++ b/snapshots/hol4/lem/hol-lib/lem_string_extraScript.sml
@@ -0,0 +1,124 @@
+(*Generated by Lem from string_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_numTheory lem_listTheory lem_basic_classesTheory lem_stringTheory lem_list_extraTheory ASCIInumbersTheory stringLib;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_string_extra"
+
+(******************************************************************************)
+(* 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*)
+ val stringFromNatHelper_defn = Hol_defn "stringFromNatHelper" `
+ ((stringFromNatHelper:num ->(char)list ->(char)list) n acc=  
+ (if n =( 0 : num) then
+    acc
+  else
+    stringFromNatHelper (n DIV( 10 : num)) (CHR ((n MOD( 10 : num)) +( 48 : num)) :: acc)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn stringFromNatHelper_defn;
+
+(*val stringFromNat : nat -> string*)
+
+(*val stringFromNaturalHelper : Num.natural -> list char -> list char*)
+ val stringFromNaturalHelper_defn = Hol_defn "stringFromNaturalHelper" `
+ ((stringFromNaturalHelper:num ->(char)list ->(char)list) n acc=  
+ (if n =( 0:num) then
+    acc
+  else
+    stringFromNaturalHelper (n DIV( 10:num)) (CHR ((((n MOD( 10:num)) +( 48:num)):num)) :: acc)))`;
+
+val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn stringFromNaturalHelper_defn;
+
+(*val stringFromNatural : Num.natural -> string*)
+
+(*val stringFromInt : Num.int -> string*)
+val _ = Define `
+ ((stringFromInt:int -> string) i=  
+  (if i <( 0 : int) then 
+     STRCAT"-" (num_to_dec_string (Num (ABS i)))
+  else
+    num_to_dec_string (Num (ABS i))))`;
+
+
+(*val stringFromInteger : Num.integer -> string*)
+val _ = Define `
+ ((stringFromInteger:int -> string) i=  
+  (if i <( 0 : int) then 
+     STRCAT"-" (num_to_dec_string (Num (ABS i)))
+  else
+    num_to_dec_string (Num (ABS i))))`;
+
+
+
+(******************************************************************************)
+(* List-like operations                                                       *)
+(******************************************************************************)
+
+(*val nth : string -> nat -> char*)
+(*let nth s n=  List_extra.nth (toCharList s) n*)
+
+(*val stringConcat : list string -> string*)
+(*let stringConcat s= 
+  List.foldr (^) "" s*)
+
+(******************************************************************************)
+(* String comparison                                                          *)
+(******************************************************************************)
+
+(*val stringCompare : string -> string -> Basic_classes.ordering*)
+
+val _ = Define `
+ ((stringLess:string -> string -> bool) x y=  (orderingIsLess (EQ)))`;
+
+val _ = Define `
+ ((stringLessEq:string -> string -> bool) x y=  (~ (orderingIsGreater (EQ))))`;
+
+val _ = Define `
+ ((stringGreater:string -> string -> bool) x y=  (stringLess y x))`;
+
+val _ = Define `
+ ((stringGreaterEq:string -> string -> bool) x y=  (stringLessEq y x))`;
+
+
+val _ = Define `
+((instance_Basic_classes_Ord_string_dict:(string)lem_basic_classes$Ord_class)= (<|
+
+  compare_method := (\ x y. EQ);
+
+  isLess_method := stringLess;
+
+  isLessEqual_method := stringLessEq;
+
+  isGreater_method := stringGreater;
+
+  isGreaterEqual_method := stringGreaterEq|>))`;
+
+ 
+val _ = export_theory()
+