Quelle ReadShow.thy

Sprache: Isabelle

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

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.17 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.