Theory Number_Parser
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