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., @{typenat}, @{typeint}, and @{typebool} in (out) of the 
  domains of strings. We provide variants for the two string representations of Isabelle/HOL, namely
  @{typestring} and @{typeString.literal}. 
›


subsubsection‹Bool›
definition 
 Readbool s = (if s = ''True'' then True else False)
definition
 Showbool b = (if b then ''True'' else ''False'')
definition 
 STR_is_bool s = (Showbool (Readbool s) = s)

declare Readbool_def [solidity_symbex]
        Showbool_def [solidity_symbex]

lemma Show_Read_bool_id: STR_is_bool s  (Showbool (Readbool 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 Readbool_def Showbool_def)

lemma Read_Show_bool_id: Readbool (Showbool b) = b
  by(auto simp: Readbool_def Showbool_def)

definition ReadLbool::String.literal  bool (_) where 
 ReadLbool s = (if s = STR ''True'' then True else False)
definition ShowLbool:: bool  String.literal (_) where
 ShowLbool b = (if b then STR ''True'' else STR ''False'')
definition 
 strL_is_bool' s = (ShowLbool (ReadLbool s) = s)

declare ReadLbool_def [solidity_symbex]
        ShowLbool_def [solidity_symbex]


lemma Show_Read_bool'_id: strL_is_bool' s  (ShowLbool (ReadLbool 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 ReadLbool_def ShowLbool_def)

lemma Read_Show_bool'_id: ReadLbool (ShowLbool b) = b
  by(auto simp: ReadLbool_def ShowLbool_def)


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  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 (smt (z3) list.simps(3) nat_explode'.simps) 

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 (z3) 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 
  Readnat :: string  nat where 
 Readnat s = nat_implode (map nat_of_digit s)

definition 
  Shownat::"nat  string" where
 Shownat n = map digit_of_nat (nat_explode n)

declare Readnat_def [solidity_symbex]
        Shownat_def [solidity_symbex]

definition 
  STR_is_nat s = (Shownat (Readnat s) = s)

value Readnat ''10''
value Shownat 10
value Readnat (Shownat (10)) = 10
value Shownat (Readnat (''10'')) = ''10''

lemma Show_nat_not_neg: 
  set (Shownat n) {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'',
                     CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}
  unfolding Shownat_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: (Shownat n)  []
  by (simp add: Shownat_def nat_explode_not_empty)

lemma not_hd: L  []  e  set(L)  hd L  e
  by auto

lemma Show_nat_not_neg'': hd (Shownat n)  (CHR ''-'')
  using Show_nat_not_neg[of n]
  Show_nat_not_empty[of n] not_hd[of Shownat n]
  by auto

lemma Show_Read_nat_id: STR_is_nat s  (Shownat (Readnat 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: Readnat(Shownat n) = n
  apply(unfold Readnat_def Shownat_def)
  using bar' nat_of_digit_digit_of_nat_id nat_explode_digits
  using nat_implode_explode_id 
  by presburger

definition 
  ReadLnat :: String.literal  nat (_) where 
 ReadLnat = Readnat  String.explode

definition 
  ShowLnat::nat  String.literal (_)where
 ShowLnat = String.implode  Shownat

declare ReadLnat_def [solidity_symbex]
        ShowLnat_def [solidity_symbex]


definition 
  strL_is_nat' s = (ShowLnat (ReadLnat s) = s)

value STR ''10''::nat
value ReadLnat (STR ''10'')
value 10::nat
value ShowLnat 10
value ReadLnat (ShowLnat (10)) = 10
value ShowLnat (ReadLnat (STR ''10'')) = STR ''10''

lemma Show_Read_nat'_id: strL_is_nat' s  (ShowLnat (ReadLnat 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 Shownat_ascii: map String.ascii_of (Shownat n) = Shownat n
  using Show_nat_not_neg digits_are_ascii
  by (meson map_idI subsetD)


lemma Read_Show_nat'_id: ReadLnat(ShowLnat n) = n
  apply(unfold ReadLnat_def ShowLnat_def, simp)
  by (simp add: Shownat_ascii  Read_Show_nat_id)


subsubsection‹Integer›
definition 
  Readint :: string  int where 
 Readint x = (if hd x = (CHR ''-'') then  -(int (Readnat (tl x))) else int (Readnat x))

definition 
  Showint::int  string where
 Showint i = (if i < 0 then (CHR ''-'')#(Shownat (nat (-i))) 
                        else Shownat (nat i))

definition 
 STR_is_int s = (Showint (Readint s) = s)


declare Readint_def [solidity_symbex]
        Showint_def [solidity_symbex]

value Readint (Showint   10)  =  10
value Readint (Showint (-10)) = -10

value Showint (Readint (''10''))  =  ''10''
value Showint (Readint (''-10'')) = ''-10''

lemma Show_Read_id: STR_is_int s  (Showint (Readint s) = s)
  by(simp add:STR_is_int_def)

lemma Read_Show_id: Readint(Showint(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 (Showint n)
  by(simp add:STR_is_int_def Read_Show_id)

definition 
  ReadLint :: String.literal  int (_) where 
 ReadLint  = Readint  String.explode 

definition 
  ShowLint::int  String.literal (_) where
 ShowLint =String.implode  Showint

definition 
 strL_is_int' s = (ShowLint (ReadLint s) = s)

declare ReadLint_def [solidity_symbex]
        ShowLint_def [solidity_symbex]

value ReadLint (ShowLint   10)  =  10
value ReadLint (ShowLint (-10)) = -10

value ShowLint (ReadLint (STR ''10''))  =  STR ''10''
value ShowLint (ReadLint (STR ''-10'')) = STR ''-10''

lemma Show_ReadL_id: strL_is_int' s  (ShowLint (ReadLint s) = s)
  by(simp add:strL_is_int'_def)

lemma Read_ShowL_id: ReadLint (ShowLint x) = x
proof(cases x < 0)
  case True
  then show ?thesis using ShowLint_def ReadLint_def Showint_def Shownat_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 ShowLint_def ReadLint_def Showint_def Shownat_ascii 
    by (metis Read_Show_id String.explode_implode_eq comp_apply)
qed 

lemma STR_is_int_ShowL: strL_is_int' (ShowLint 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