```section‹Converting Types to Strings and Back Again›
imports
Solidity_Symbex
begin

text‹
In the following, we formalize a family of projection (and injection) functions for injecting
(projecting) basic types (i.e., @{type ‹nat›}, @{type ‹int›}, and @{type ‹bool›} in (out) of the
domains of strings. We provide variants for the two string representations of Isabelle/HOL, namely
@{type ‹string›} and @{type ‹String.literal›}.
›

subsubsection‹Bool›
definition
‹Read⇩b⇩o⇩o⇩l s = (if s = ''True'' then True else False)›
definition
‹Show⇩b⇩o⇩o⇩l b = (if b then ''True'' else ''False'')›
definition
‹STR_is_bool s = (Show⇩b⇩o⇩o⇩l (Read⇩b⇩o⇩o⇩l s) = s)›

Show⇩b⇩o⇩o⇩l_def [solidity_symbex]

using STR_is_bool_def by fastforce

lemma STR_is_bool_split: ‹STR_is_bool s ⟹ s = ''False'' ∨ s = ''True''›

definition ReadL⇩b⇩o⇩o⇩l::‹String.literal ⇒ bool› (‹⌊_⌋›) where
‹ReadL⇩b⇩o⇩o⇩l s = (if s = STR ''True'' then True else False)›
definition ShowL⇩b⇩o⇩o⇩l:: ‹bool ⇒ String.literal› (‹⌈_⌉›) where
‹ShowL⇩b⇩o⇩o⇩l b = (if b then STR ''True'' else STR ''False'')›
definition
‹strL_is_bool' s = (ShowL⇩b⇩o⇩o⇩l (ReadL⇩b⇩o⇩o⇩l s) = s)›

ShowL⇩b⇩o⇩o⇩l_def [solidity_symbex]

using strL_is_bool'_def by fastforce

lemma strL_is_bool'_split:  ‹strL_is_bool' s ⟹ s = STR ''False'' ∨ s = STR ''True''›

lemma true_neq_false[simp]: "ShowL⇩b⇩o⇩o⇩l True ≠ ShowL⇩b⇩o⇩o⇩l False"

subsubsection‹Natural Numbers›

definition  nat_of_digit ::  ‹char ⇒ nat› where
‹nat_of_digit c =
(if c = CHR ''0'' then 0
else if c = CHR ''1'' then 1
else if c = CHR ''2'' then 2
else if c = CHR ''3'' then 3
else if c = CHR ''4'' then 4
else if c = CHR ''5'' then 5
else if c = CHR ''6'' then 6
else if c = CHR ''7'' then 7
else if c = CHR ''8'' then 8
else if c = CHR ''9'' then 9
else undefined)›

declare nat_of_digit_def [solidity_symbex]

definition  is_digit ::  ‹char ⇒ bool› where
‹is_digit c =
(if c = CHR ''0'' then True
else if c = CHR ''1'' then True
else if c = CHR ''2'' then True
else if c = CHR ''3'' then True
else if c = CHR ''4'' then True
else if c = CHR ''5'' then True
else if c = CHR ''6'' then True
else if c = CHR ''7'' then True
else if c = CHR ''8'' then True
else if c = CHR ''9'' then True
else if c = CHR ''-'' then True
else False)›

definition  digit_of_nat ::  ‹nat ⇒ char› where
‹digit_of_nat x =
(if x = 0 then CHR ''0''
else if x = 1 then CHR ''1''
else if x = 2 then CHR ''2''
else if x = 3 then CHR ''3''
else if x = 4 then CHR ''4''
else if x = 5 then CHR ''5''
else if x = 6 then CHR ''6''
else if x = 7 then CHR ''7''
else if x = 8 then CHR ''8''
else if x = 9 then CHR ''9''
else undefined)›

declare digit_of_nat_def [solidity_symbex]

lemma nat_of_digit_digit_of_nat_id:
‹x < 10 ⟹ nat_of_digit (digit_of_nat x) = x›

lemma img_digit_of_nat:
‹n < 10 ⟹ digit_of_nat n ∈ {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'',
CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}›

lemma digit_of_nat_nat_of_digit_id:
‹c ∈ {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'',
CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}
⟹ digit_of_nat (nat_of_digit c) = c›
by(code_simp, auto)

definition
nat_implode :: ‹'a::{numeral,power,zero} list ⇒ 'a› where
‹nat_implode n = foldr (+) (map (λ (p,d) ⇒ 10 ^ p * d) (enumerate 0 (rev n))) 0›

declare nat_implode_def [solidity_symbex]

fun nat_explode' :: ‹nat ⇒ nat list› where
‹nat_explode' x = (case  x < 10 of True ⇒ [x mod 10]
| _ ⇒ (x mod 10 )#(nat_explode' (x div 10)))›

definition
nat_explode :: ‹nat ⇒ nat list› where
‹nat_explode x = (rev (nat_explode' x))›

declare nat_explode_def [solidity_symbex]

lemma nat_explode'_not_empty: ‹nat_explode' n ≠ []›
by (smt (verit, ccfv_threshold) nat_explode'.elims ord.lexordp_eq_simps(1) ord.lexordp_eq_simps(3))

lemma nat_explode_not_empty: ‹nat_explode n ≠ []›
using nat_explode'_not_empty nat_explode_def by auto

lemma nat_explode'_ne_suc: ‹∃ n. nat_explode' (Suc n) ≠ nat_explode' n›
by(rule exI [of _ ‹0::nat›], simp)

lemma nat_explode'_digit: ‹hd (nat_explode' n ) < 10›
proof(induct  ‹n›)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case proof (cases ‹n < 9›)
case True
then show ?thesis by simp
next
case False
then show ?thesis
by simp
qed
qed

lemma div_ten_less: ‹n ≠ 0 ⟹ ((n::nat) div 10) < n›
by simp

lemma unroll_nat_explode':
‹¬ n < 10 ⟹ (case n < 10 of True ⇒ [n mod 10] | False ⇒ n mod 10 # nat_explode' (n div 10)) =
(n mod 10 # nat_explode' (n div 10))›
by simp

lemma nat_explode_mod_10_ident: ‹map (λ x. x mod 10) (nat_explode' n) = nat_explode' n›
proof (cases ‹n < 10›)
case True
then show ?thesis by simp
next
case False
then show ?thesis
proof (induct ‹n› rule: nat_less_induct)
case (1 n) note * = this
then show ?case
using div_ten_less apply(simp (no_asm))
using unroll_nat_explode'[of n] *
by (smt (verit) list.simps(8) list.simps(9) mod_div_trivial mod_eq_self_iff_div_eq_0
nat_explode'.simps zero_less_numeral)
qed
qed

lemma nat_explode'_digits:
‹∀d ∈ set (nat_explode' n). d < 10›
proof
fix d
assume ‹d ∈ set (nat_explode' n)›
then have ‹d ∈ set (map (λm. m mod 10) (nat_explode' n))›
by (simp only: nat_explode_mod_10_ident)
then show ‹d < 10›
by auto
qed

lemma nat_explode_digits:
‹∀d ∈ set (nat_explode n). d < 10›
using nat_explode'_digits [of n] by (simp only: nat_explode_def set_rev)

value ‹nat_implode(nat_explode 42) = 42›
value ‹nat_explode (Suc 21)›

lemma nat_implode_append:
‹nat_implode (a@[b]) = (1*b + foldr (+) (map (λ(p, y). 10 ^ p * y) (enumerate (Suc 0) (rev a))) 0 )›

lemma enumerate_suc: ‹enumerate (Suc n) l = map (λ (a,b). (a+1::nat,b)) (enumerate n l)›
proof (induction ‹l›)
case Nil
then show ?case by simp
next
case (Cons a x) note * = this
then show ?case apply(simp only:enumerate_simps)

apply(simp only:‹enumerate (Suc n) x = map (λa. case a of (a, b) ⇒ (a + 1, b)) (enumerate n x)›[symmetric])
apply(simp)
using *
by (metis apfst_conv cond_case_prod_eta enumerate_Suc_eq)
qed

lemma mult_assoc_aux1:
‹(λ(p, y). 10 ^ p * y) ∘ (λ(a, y). (Suc a, y)) = (λ(p, y). (10::nat) * (10 ^ p) * y)›
by(auto simp:o_def)

lemma fold_map_transfer:
‹(foldr (+) (map (λ(x,y). 10 * (f (x,y))) l) (0::nat)) = 10 * (foldr (+) (map (λx. (f x)) l) (0::nat))›
proof(induct ‹l›)
case Nil
then show ?case by(simp)
next
case (Cons a l)
then show ?case  by(simp)
qed

lemma mult_assoc_aux2: ‹(λ(p, y). 10 * 10 ^ p * (y::nat)) = (λ(p, y). 10 * (10 ^ p * y))›
by(auto)

lemma nat_implode_explode_id: ‹nat_implode (nat_explode n) = n›
proof (cases ‹n=0›)
case True note * = this
then show ?thesis
next
case False
then show ?thesis
proof (induct ‹n› rule: nat_less_induct)
case (1 n) note * = this
then  have
**: ‹nat_implode (nat_explode (n div 10)) = n div 10›
proof (cases ‹n div 10 = 0›)
case True
then show ?thesis by(simp add: nat_explode_def nat_implode_def)
next
case False
then show ?thesis
using div_ten_less[of ‹n›] *
by(simp)
qed
then show ?case
proof (cases ‹n < 10›)
case True
then show ?thesis  by(simp add: nat_explode_def nat_implode_def)
next
case False note *** = this
then show ?thesis
apply(simp only: bool.case(2))
apply(simp del:nat_explode'.simps rev_rev_ident)
apply(fold nat_explode_def)
apply(simp only:nat_implode_append)
apply(simp only:mult_assoc_aux1)
using mult_assoc_aux2 apply(simp)
using fold_map_transfer[of ‹λ(p, y). 10 ^ p * y›
‹(enumerate 0 (rev (nat_explode (n div 10))))›, simplified]
apply(simp) apply(fold nat_implode_def) using **
by simp
qed
qed
qed

definition
Read⇩n⇩a⇩t :: ‹string ⇒ nat› where
‹Read⇩n⇩a⇩t s = nat_implode (map nat_of_digit s)›

definition
Show⇩n⇩a⇩t::"nat ⇒ string" where
‹Show⇩n⇩a⇩t n = map digit_of_nat (nat_explode n)›

Show⇩n⇩a⇩t_def [solidity_symbex]

definition
‹STR_is_nat s = (Show⇩n⇩a⇩t (Read⇩n⇩a⇩t s) = s)›

value ‹Show⇩n⇩a⇩t 10›
value ‹Read⇩n⇩a⇩t (Show⇩n⇩a⇩t (10)) = 10›
value ‹Show⇩n⇩a⇩t (Read⇩n⇩a⇩t (''10'')) = ''10''›

lemma Show_nat_not_neg:
‹set (Show⇩n⇩a⇩t n) ⊆{CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'',
CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}›
unfolding Show⇩n⇩a⇩t_def
using  nat_explode_digits[of n]  img_digit_of_nat imageE image_set subsetI
by (smt (verit) imageE image_set subsetI)

lemma Show_nat_not_empty: ‹(Show⇩n⇩a⇩t n) ≠ []›

lemma not_hd: ‹L ≠ [] ⟹ e ∉ set(L) ⟹ hd L ≠ e›
by auto

lemma Show_nat_not_neg'': ‹hd (Show⇩n⇩a⇩t n) ≠ (CHR ''-'')›
using Show_nat_not_neg[of ‹n›]
Show_nat_not_empty[of ‹n›] not_hd[of ‹Show⇩n⇩a⇩t n›]
by auto

lemma bar': ‹∀ d ∈ set l . d < 10 ⟹ map nat_of_digit (map digit_of_nat l) = l›
using  nat_of_digit_digit_of_nat_id

using bar' nat_of_digit_digit_of_nat_id nat_explode_digits
using nat_implode_explode_id
by presburger

definition
ReadL⇩n⇩a⇩t :: ‹String.literal ⇒ nat› (‹⌈_⌉›) where

definition
ShowL⇩n⇩a⇩t::‹nat ⇒ String.literal› (‹⌊_⌋›)where
‹ShowL⇩n⇩a⇩t = String.implode ∘ Show⇩n⇩a⇩t›

ShowL⇩n⇩a⇩t_def [solidity_symbex]

definition
‹strL_is_nat' s = (ShowL⇩n⇩a⇩t (ReadL⇩n⇩a⇩t s) = s)›

value ‹⌈STR ''10''⌉::nat›
value ‹⌊10::nat⌋›
value ‹ShowL⇩n⇩a⇩t 10›
value ‹ReadL⇩n⇩a⇩t (ShowL⇩n⇩a⇩t (10)) = 10›
value ‹ShowL⇩n⇩a⇩t (ReadL⇩n⇩a⇩t (STR ''10'')) = STR ''10''›

lemma digits_are_ascii:
‹c ∈ {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'',
CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}
⟹ String.ascii_of c = c›
by auto

lemma Show⇩n⇩a⇩t_ascii: ‹map String.ascii_of (Show⇩n⇩a⇩t n) = Show⇩n⇩a⇩t n›
using Show_nat_not_neg digits_are_ascii
by (meson map_idI subsetD)

subsubsection‹Integer›
definition
Read⇩i⇩n⇩t :: ‹string ⇒ int› where
‹Read⇩i⇩n⇩t x = (if hd x = (CHR ''-'') then  -(int (Read⇩n⇩a⇩t (tl x))) else int (Read⇩n⇩a⇩t x))›

definition
Show⇩i⇩n⇩t::‹int ⇒ string› where
‹Show⇩i⇩n⇩t i = (if i < 0 then (CHR ''-'')#(Show⇩n⇩a⇩t (nat (-i)))
else Show⇩n⇩a⇩t (nat i))›

definition
‹STR_is_int s = (Show⇩i⇩n⇩t (Read⇩i⇩n⇩t s) = s)›

Show⇩i⇩n⇩t_def [solidity_symbex]

value ‹Read⇩i⇩n⇩t (Show⇩i⇩n⇩t   10)  =  10›
value ‹Read⇩i⇩n⇩t (Show⇩i⇩n⇩t (-10)) = -10›

value ‹Show⇩i⇩n⇩t (Read⇩i⇩n⇩t (''10''))  =  ''10''›
value ‹Show⇩i⇩n⇩t (Read⇩i⇩n⇩t (''-10'')) = ''-10''›

apply(code_simp)
apply(thin_tac ‹¬ x < 0 ›)
using Show_nat_not_neg''
by blast

lemma STR_is_int_Show: ‹STR_is_int (Show⇩i⇩n⇩t n)›

definition
ReadL⇩i⇩n⇩t :: ‹String.literal ⇒ int› (‹⌈_⌉›) where

definition
ShowL⇩i⇩n⇩t::‹int ⇒ String.literal› (‹⌊_⌋›) where
‹ShowL⇩i⇩n⇩t =String.implode ∘ Show⇩i⇩n⇩t›

definition
‹strL_is_int' s = (ShowL⇩i⇩n⇩t (ReadL⇩i⇩n⇩t s) = s)›

ShowL⇩i⇩n⇩t_def [solidity_symbex]

value ‹ReadL⇩i⇩n⇩t (ShowL⇩i⇩n⇩t   10)  =  10›
value ‹ReadL⇩i⇩n⇩t (ShowL⇩i⇩n⇩t (-10)) = -10›

value ‹ShowL⇩i⇩n⇩t (ReadL⇩i⇩n⇩t (STR ''10''))  =  STR ''10''›
value ‹ShowL⇩i⇩n⇩t (ReadL⇩i⇩n⇩t (STR ''-10'')) = STR ''-10''›

proof(cases ‹x < 0›)
case True
then show ?thesis using ShowL⇩i⇩n⇩t_def ReadL⇩i⇩n⇩t_def Show⇩i⇩n⇩t_def Show⇩n⇩a⇩t_ascii
by (metis (no_types, lifting) Read_Show_id String.ascii_of_Char comp_def implode.rep_eq list.simps(9))
next
case False
then show ?thesis using ShowL⇩i⇩n⇩t_def ReadL⇩i⇩n⇩t_def Show⇩i⇩n⇩t_def Show⇩n⇩a⇩t_ascii