Theory ReadShow

section‹Converting Types to Strings and Back Again›
theory ReadShow
  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)›

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

lemma Show_Read_bool_id: ‹STR_is_bool s ⟹ (Show⇩b⇩o⇩o⇩l (Read⇩b⇩o⇩o⇩l s) = s)›
  using STR_is_bool_def by fastforce

lemma STR_is_bool_split: ‹STR_is_bool s ⟹ s = ''False'' ∨ s = ''True''›
  by(auto simp: STR_is_bool_def Read⇩b⇩o⇩o⇩l_def Show⇩b⇩o⇩o⇩l_def)

lemma Read_Show_bool_id: ‹Read⇩b⇩o⇩o⇩l (Show⇩b⇩o⇩o⇩l b) = b›
  by(auto simp: Read⇩b⇩o⇩o⇩l_def Show⇩b⇩o⇩o⇩l_def)

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)›

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


lemma Show_Read_bool'_id: ‹strL_is_bool' s ⟹ (ShowL⇩b⇩o⇩o⇩l (ReadL⇩b⇩o⇩o⇩l s) = s)›
  using strL_is_bool'_def by fastforce

lemma strL_is_bool'_split:  ‹strL_is_bool' s ⟹ s = STR ''False'' ∨ s = STR ''True''›
  by(auto simp: strL_is_bool'_def ReadL⇩b⇩o⇩o⇩l_def ShowL⇩b⇩o⇩o⇩l_def)

lemma Read_Show_bool'_id[simp]: ‹ReadL⇩b⇩o⇩o⇩l (ShowL⇩b⇩o⇩o⇩l b) = b›
  by(auto simp: ReadL⇩b⇩o⇩o⇩l_def ShowL⇩b⇩o⇩o⇩l_def)

lemma true_neq_false[simp]: "ShowL⇩b⇩o⇩o⇩l True ≠ ShowL⇩b⇩o⇩o⇩l False"
  by (metis Read_Show_bool'_id)

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›
  by(simp add:nat_of_digit_def digit_of_nat_def)

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''}›
  by(simp add:nat_of_digit_def digit_of_nat_def)

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 (induction n rule: nat_explode'.induct) (simp_all split: bool.split)

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 )›
  by(simp add:nat_implode_def)

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 
    by (simp add: nat_explode_def nat_implode_def) 
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 (no_asm)  add:nat_explode_def del:rev_rev_ident)
        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 add:enumerate_suc)
        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)›

declare Read⇩n⇩a⇩t_def [solidity_symbex]
        Show⇩n⇩a⇩t_def [solidity_symbex]

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

value ‹Read⇩n⇩a⇩t ''10''›
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) ≠ []›
  by (simp add: Show⇩n⇩a⇩t_def nat_explode_not_empty)

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 Show_Read_nat_id: ‹STR_is_nat s ⟹ (Show⇩n⇩a⇩t (Read⇩n⇩a⇩t s) = s)›
  by(simp add:STR_is_nat_def)

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 
  by (simp add: map_idI)

lemma Read_Show_nat_id: ‹Read⇩n⇩a⇩t(Show⇩n⇩a⇩t n) = n›
  apply(unfold Read⇩n⇩a⇩t_def Show⇩n⇩a⇩t_def)
  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 
 ‹ReadL⇩n⇩a⇩t = Read⇩n⇩a⇩t ∘ String.explode›

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

declare ReadL⇩n⇩a⇩t_def [solidity_symbex]
        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 ‹ReadL⇩n⇩a⇩t (STR ''10'')›
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 Show_Read_nat'_id: ‹strL_is_nat' s ⟹ (ShowL⇩n⇩a⇩t (ReadL⇩n⇩a⇩t s) = s)›
  by(simp add:strL_is_nat'_def)

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)


lemma Read_Show_nat'_id: ‹ReadL⇩n⇩a⇩t(ShowL⇩n⇩a⇩t n) = n›
  apply(unfold ReadL⇩n⇩a⇩t_def ShowL⇩n⇩a⇩t_def, simp)
  by (simp add: Show⇩n⇩a⇩t_ascii  Read_Show_nat_id)


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)›


declare Read⇩i⇩n⇩t_def [solidity_symbex]
        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''›

lemma Show_Read_id: ‹STR_is_int s ⟹ (Show⇩i⇩n⇩t (Read⇩i⇩n⇩t s) = s)›
  by(simp add:STR_is_int_def)
                          
lemma Read_Show_id: ‹Read⇩i⇩n⇩t(Show⇩i⇩n⇩t(x)) = x›
  apply(code_simp)
  apply(auto simp:Show_nat_not_neg Read_Show_nat_id)[1]
  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)›
  by(simp add:STR_is_int_def Read_Show_id)

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

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)›

declare ReadL⇩i⇩n⇩t_def [solidity_symbex]
        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''›

lemma Show_ReadL_id: ‹strL_is_int' s ⟹ (ShowL⇩i⇩n⇩t (ReadL⇩i⇩n⇩t s) = s)›
  by(simp add:strL_is_int'_def)

lemma Read_ShowL_id: ‹ReadL⇩i⇩n⇩t (ShowL⇩i⇩n⇩t x) = x›
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 
    by (metis Read_Show_id String.explode_implode_eq comp_apply)
qed 

lemma STR_is_int_ShowL: ‹strL_is_int' (ShowL⇩i⇩n⇩t n)›
  by(simp add:strL_is_int'_def Read_ShowL_id)

lemma String_Cancel: "a + (c::String.literal) = b + c ⟹ a = b"
using String.plus_literal.rep_eq
by (metis append_same_eq literal.explode_inject)

end