Quelle  Number_Parser.thy

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
*)

text ‹We provide two parsers for natural numbers and integers, which are
 verified in the sense that they are the inverse of the show-function for
 these types. We therefore also prove that the show-functions are injective.›
theory Number_Parser
  imports 
    Show_Instances
begin

text ‹We define here the bind-operations for option and sum-type. We do not
 import these operations from Certification-Monads.Strict-Sum and Parser-Monad,
 since these imports would yield a cyclic dependency of
 the two AFP entries Show and Certification-Monads.›

definition obind where "obind opt f = (case opt of None ==> None | Some x ==> f x)" 
definition sbind where "sbind su f = (case su of Inl e ==> Inl e | Inr r ==> f r)" 

context begin

text ‹A natural number parser which is proven correct:›

definition nat_of_digit :: "char ==> nat option" where
  "nat_of_digit x ≡
    if x = CHR ''0'' then Some 0
    else if x = CHR ''1'' then Some 1
    else if x = CHR ''2'' then Some 2
    else if x = CHR ''3'' then Some 3
    else if x = CHR ''4'' then Some 4
    else if x = CHR ''5'' then Some 5
    else if x = CHR ''6'' then Some 6
    else if x = CHR ''7'' then Some 7
    else if x = CHR ''8'' then Some 8
    else if x = CHR ''9'' then Some 9
    else None" 

private fun nat_of_string_aux :: "nat ==> string ==> nat option"
  where
    "nat_of_string_aux n [] = Some n" |
    "nat_of_string_aux n (d # s) = (obind (nat_of_digit d) (λm. nat_of_string_aux (10 * n + m) s))"

definition "nat_of_string s ≡
  case if s = [] then None else nat_of_string_aux 0 s of
    None ==> Inl (STR ''cannot convert \"'' + String.implode s + STR ''\" to a number'')
  | Some n ==> Inr n"

private lemma nat_of_string_aux_snoc:
  "nat_of_string_aux n (s @ [c]) =
     obind (nat_of_string_aux n s) (λ l. obind (nat_of_digit c) (λ m. Some (10 * l + m)))"
  by (induct s arbitrary:n, auto simp: obind_def split: option.splits)

private lemma nat_of_string_aux_digit:
  assumes m10: "m < 10"
  shows "nat_of_string_aux n (s @ string_of_digit m) =
    obind (nat_of_string_aux n s) (λ l. Some (10 * l + m))"
proof -
  from m10 have "m = 0 ∨ m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 ∨ m = 5 ∨ m = 6 ∨ m = 7 ∨ m = 8 ∨ m = 9" 
    by presburger
  thus ?thesis by (auto simp add: nat_of_digit_def nat_of_string_aux_snoc string_of_digit_def
        obind_def split: option.splits)
qed


private lemmas shows_move = showsp_nat_append[of 0 _ "[]",simplified, folded shows_prec_nat_def]

private lemma nat_of_string_aux_show: "nat_of_string_aux 0 (show m) = Some m"
proof (induct m rule:less_induct)
  case IH: (less m)
  show ?case proof (cases "m < 10")
    case m10: True
    show ?thesis
      apply (unfold shows_prec_nat_def)
      apply (subst showsp_nat.simps)
      using m10 nat_of_string_aux_digit[OF m10, of 0 "[]"]
      by (auto simp add:shows_string_def nat_of_string_def string_of_digit_def obind_def)
  next
    case m: False
    then have "m div 10 < m" by auto
    note IH = IH[OF this]
    show ?thesis apply (unfold shows_prec_nat_def, subst showsp_nat.simps)
      using m apply (simp add: shows_prec_nat_def[symmetric] shows_string_def)
      apply (subst shows_move)
      using nat_of_string_aux_digit m IH 
      by (auto simp: nat_of_string_def obind_def)
  qed
qed

lemma fixes m :: nat shows show_nonemp: "show m ≠ []"
  apply (unfold shows_prec_nat_def)
  apply (subst showsp_nat.simps)
  apply (fold shows_prec_nat_def)
  apply (unfold o_def)
  apply (subst shows_move)
  apply (auto simp: shows_string_def string_of_digit_def)
  done

text ‹The parser ‹nat_of_string› is the inverse of ‹show›.›
lemma nat_of_string_show[simp]: "nat_of_string (show m) = Inr m"
  using nat_of_string_aux_show by (auto simp: nat_of_string_def show_nonemp)

end


text ‹We also provide a verified parser for integers.›

fun safe_head where "safe_head [] = None" | "safe_head (x#xs) = Some x"

definition int_of_string :: "string ==> String.literal + int"
  where "int_of_string s ≡
    if safe_head s = Some (CHR ''-'') then sbind (nat_of_string (tl s)) (λ n. Inr (- int n))
    else sbind (nat_of_string s) (λ n. Inr (int n))"

definition digits :: "char set" where
  "digits = set (''0123456789'')" 

lemma set_string_of_digit: "set (string_of_digit x) ⊆ digits" 
  unfolding digits_def string_of_digit_def by auto

lemma range_showsp_nat: "set (showsp_nat p n s) ⊆ digits ∪ set s" 
proof (induct p n arbitrary: s rule: showsp_nat.induct)
  case (1 p n s)
  then show ?case using set_string_of_digit[of n] set_string_of_digit[of "n mod 10"]
    by (auto simp: showsp_nat.simps[of p n] shows_string_def) fastforce
qed

lemma set_show_nat: "set (show (n :: nat)) ⊆ digits" 
  using range_showsp_nat[of 0 n Nil] unfolding shows_prec_nat_def by auto

lemma int_of_string_show[simp]: "int_of_string (show x) = Inr x" 
proof -
  have "show x = showsp_int 0 x []" 
    by (simp add: shows_prec_int_def)
  also have "… = (if x < 0 then ''-'' @ show (nat (-x)) else show (nat x))" 
    unfolding showsp_int_def if_distrib shows_prec_nat_def
    by (simp add: shows_string_def)
  also have "int_of_string … = Inr x" 
  proof (cases "x < 0")
    case True
    thus ?thesis unfolding int_of_string_def sbind_def by simp
  next
    case False
    from set_show_nat have "set (show (nat x)) ⊆ digits" .
    hence "CHR ''-'' ∉ set (show (nat x))" unfolding digits_def by auto
    hence "safe_head (show (nat x)) ≠ Some CHR ''-''" 
      by (cases "show (nat x)", auto) 
    thus ?thesis using False
      by (simp add: int_of_string_def sbind_def)
  qed
  finally show ?thesis .
qed

hide_const (open) obind sbind

text ‹Eventually, we derive injectivity of the show-functions for nat and int.›

lemma inj_show_nat: "inj (show :: nat ==> string)" 
  by (rule inj_on_inverseI[of _ "λ s. case nat_of_string s of Inr x ==> x"], auto)

lemma inj_show_int: "inj (show :: int ==> string)" 
  by (rule inj_on_inverseI[of _ "λ s. case int_of_string s of Inr x ==> x"], auto)


end