Quelle  ReadShow.thy

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_bool s = (if s = ''True'' then True else False)›
definition
 ‹Show_bool b = (if b then ''True'' else ''False'')›
definition 
 ‹STR_is_bool s = (Show_bool (Read_bool s) = s)›

declare Read_{bool_def} [solidity_symbex]
        Show_{bool_def} [solidity_symbex]

lemma Show_Read_bool_id: ‹STR_is_bool s ==> (Show_bool (Read_bool 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_{bool_def} Show_{bool_def})

lemma Read_Show_bool_id: ‹Read_bool (Show_bool b) = b›
  by(auto simp: Read_{bool_def} Show_{bool_def})

definition ReadL_bool::‹String.literal ==> bool› (‹⌊_⌋›) where 
 ‹ReadL_bool s = (if s = STR ''True'' then True else False)›
definition ShowL_bool:: ‹bool ==> String.literal› (‹⌈_⌉›) where
 ‹ShowL_bool b = (if b then STR ''True'' else STR ''False'')›
definition 
 ‹strL_is_bool' s = (ShowL_bool (ReadL_bool s) = s)›

declare ReadL_{bool_def} [solidity_symbex]
        ShowL_{bool_def} [solidity_symbex]


lemma Show_Read_bool'_id: ‹strL_is_bool' s ==> (ShowL_bool (ReadL_bool 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_{bool_def} ShowL_{bool_def})

lemma Read_Show_bool'_id[simp]: ‹ReadL_bool (ShowL_bool b) = b›
  by(auto simp: ReadL_{bool_def} ShowL_{bool_def})

lemma true_neq_false[simp]: "ShowL_bool True ≠ ShowL_bool 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_nat :: ‹string ==> nat› where 
 ‹Read_nat s = nat_implode (map nat_of_digit s)›

definition 
  Show_nat::"nat ==> string" where
 ‹Show_nat n = map digit_of_nat (nat_explode n)›

declare Read_{nat_def} [solidity_symbex]
        Show_{nat_def} [solidity_symbex]

definition 
  ‹STR_is_nat s = (Show_nat (Read_nat s) = s)›

value ‹Read_nat ''10''›
value ‹Show_nat 10›
value ‹Read_nat (Show_nat (10)) = 10›
value ‹Show_nat (Read_nat (''10'')) = ''10''›

lemma Show_nat_not_neg: 
  ‹set (Show_nat n) ⊆{CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'',
 CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}›
  unfolding Show_{nat_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_nat n) ≠ []›
  by (simp add: Show_{nat_def} nat_explode_not_empty)

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

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

lemma Show_Read_nat_id: ‹STR_is_nat s ==> (Show_nat (Read_nat 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_nat(Show_nat n) = n›
  apply(unfold Read_{nat_def} Show_{nat_def})
  using bar' nat_of_digit_digit_of_nat_id nat_explode_digits
  using nat_implode_explode_id 
  by presburger

definition 
  ReadL_nat :: ‹String.literal ==> nat› (‹⌈_⌉›) where 
 ‹ReadL_nat = Read_nat ∘ String.explode›

definition 
  ShowL_nat::‹nat ==> String.literal› (‹⌊_⌋›)where
 ‹ShowL_nat = String.implode ∘ Show_nat›

declare ReadL_{nat_def} [solidity_symbex]
        ShowL_{nat_def} [solidity_symbex]


definition 
  ‹strL_is_nat' s = (ShowL_nat (ReadL_nat s) = s)›

value ‹⌈STR ''10''⌉::nat›
value ‹ReadL_nat (STR ''10'')›
value ‹⌊10::nat⌋›
value ‹ShowL_nat 10›
value ‹ReadL_nat (ShowL_nat (10)) = 10›
value ‹ShowL_nat (ReadL_nat (STR ''10'')) = STR ''10''›

lemma Show_Read_nat'_id: ‹strL_is_nat' s ==> (ShowL_nat (ReadL_nat 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_{nat_ascii}: ‹map String.ascii_of (Show_nat n) = Show_nat n›
  using Show_nat_not_neg digits_are_ascii
  by (meson map_idI subsetD)


lemma Read_Show_nat'_id: ‹ReadL_nat(ShowL_nat n) = n›
  apply(unfold ReadL_{nat_def} ShowL_{nat_def}, simp)
  by (simp add: Show_{nat_ascii}  Read_Show_nat_id)


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

definition 
  Show_int::‹int ==> string› where
 ‹Show_int i = (if i < 0 then (CHR ''-'')#(Show_nat (nat (-i)))
 else Show_nat (nat i))›

definition 
 ‹STR_is_int s = (Show_int (Read_int s) = s)›


declare Read_{int_def} [solidity_symbex]
        Show_{int_def} [solidity_symbex]

value ‹Read_int (Show_int 10) = 10›
value ‹Read_int (Show_int (-10)) = -10›

value ‹Show_int (Read_int (''10'')) = ''10''›
value ‹Show_int (Read_int (''-10'')) = ''-10''›

lemma Show_Read_id: ‹STR_is_int s ==> (Show_int (Read_int s) = s)›
  by(simp add:STR_is_int_def)
                          
lemma Read_Show_id: ‹Read_int(Show_int(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_int n)›
  by(simp add:STR_is_int_def Read_Show_id)

definition 
  ReadL_int :: ‹String.literal ==> int› (‹⌈_⌉›) where 
 ‹ReadL_int = Read_int ∘ String.explode›

definition 
  ShowL_int::‹int ==> String.literal› (‹⌊_⌋›) where
 ‹ShowL_int =String.implode ∘ Show_int›

definition 
 ‹strL_is_int' s = (ShowL_int (ReadL_int s) = s)›

declare ReadL_{int_def} [solidity_symbex]
        ShowL_{int_def} [solidity_symbex]

value ‹ReadL_int (ShowL_int 10) = 10›
value ‹ReadL_int (ShowL_int (-10)) = -10›

value ‹ShowL_int (ReadL_int (STR ''10'')) = STR ''10''›
value ‹ShowL_int (ReadL_int (STR ''-10'')) = STR ''-10''›

lemma Show_ReadL_id: ‹strL_is_int' s ==> (ShowL_int (ReadL_int s) = s)›
  by(simp add:strL_is_int'_def)

lemma Read_ShowL_id: ‹ReadL_int (ShowL_int x) = x›
proof(cases ‹x < 0›)
  case True
  then show ?thesis using ShowL_{int_def} ReadL_{int_def} Show_{int_def} Show_{nat_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_{int_def} ReadL_{int_def} Show_{int_def} Show_{nat_ascii} 
    by (metis Read_Show_id String.explode_implode_eq comp_apply)
qed 

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