diff --git a/metadata/entries/Berlekamp_Zassenhaus.toml b/metadata/entries/Berlekamp_Zassenhaus.toml
--- a/metadata/entries/Berlekamp_Zassenhaus.toml
+++ b/metadata/entries/Berlekamp_Zassenhaus.toml
@@ -1,56 +1,57 @@
title = "The Factorization Algorithm of Berlekamp and Zassenhaus"
date = 2016-10-14
topics = [
"Mathematics/Algebra",
]
abstract = """
We formalize the Berlekamp-Zassenhaus algorithm for factoring
square-free integer polynomials in Isabelle/HOL. We further adapt an
existing formalization of Yun’s square-free factorization algorithm to
integer polynomials, and thus provide an efficient and certified
factorization algorithm for arbitrary univariate polynomials.
The algorithm first performs a factorization in the prime field GF(p) and
then performs computations in the integer ring modulo p^k, where both
p and k are determined at runtime. Since a natural modeling of these
structures via dependent types is not possible in Isabelle/HOL, we
formalize the whole algorithm using Isabelle’s recent addition of
local type definitions.
Through experiments we verify that our algorithm factors polynomials of degree
100 within seconds.
"""
license = "bsd"
note = ""
[authors]
[authors.divason]
homepage = "divason_homepage"
[authors.joosten]
email = "joosten_email"
[authors.thiemann]
email = "thiemann_email"
[authors.yamada]
email = "yamada_email"
[contributors]
[notify]
thiemann = "thiemann_email"
[history]
+2024-04-12 = "Added interface to simplify usage of generated code. "
[extra]
[related]
dois = [
"10.1007/s10817-019-09526-y",
"10.1017/CBO9781139856065"
]
pubs = [
"Wikipedia"
]
diff --git a/metadata/entries/Polynomial_Factorization.toml b/metadata/entries/Polynomial_Factorization.toml
--- a/metadata/entries/Polynomial_Factorization.toml
+++ b/metadata/entries/Polynomial_Factorization.toml
@@ -1,42 +1,43 @@
title = "Polynomial Factorization"
date = 2016-01-29
topics = [
"Mathematics/Algebra",
]
abstract = """
Based on existing libraries for polynomial interpolation and matrices,
we formalized several factorization algorithms for polynomials, including
Kronecker's algorithm for integer polynomials,
Yun's square-free factorization algorithm for field polynomials, and
Berlekamp's algorithm for polynomials over finite fields.
By combining the last one with Hensel's lifting,
we derive an efficient factorization algorithm for the integer polynomials,
which is then lifted for rational polynomials by mechanizing Gauss' lemma.
Finally, we assembled a combined factorization algorithm for rational polynomials,
which combines all the mentioned algorithms and additionally uses the explicit formula for roots
of quadratic polynomials and a rational root test.
As side products, we developed division algorithms for polynomials over integral domains,
as well as primality-testing and prime-factorization algorithms for integers."""
license = "bsd"
note = ""
[authors]
[authors.thiemann]
email = "thiemann_email"
[authors.yamada]
email = "yamada_email"
[contributors]
[notify]
thiemann = "thiemann_email"
yamada = "yamada_email1"
[history]
+2024-04-12 = "changed definition of square-free-factorization. "
[extra]
[related]
diff --git a/metadata/entries/Show.toml b/metadata/entries/Show.toml
--- a/metadata/entries/Show.toml
+++ b/metadata/entries/Show.toml
@@ -1,37 +1,38 @@
title = "Haskell's Show Class in Isabelle/HOL"
date = 2014-07-29
topics = [
"Computer science/Functional programming",
]
abstract = """
We implemented a type class for \"to-string\" functions, similar to
Haskell's Show class. Moreover, we provide instantiations for Isabelle/HOL's
standard types like bool, prod, sum, nats, ints, and rats. It is further
possible, to automatically derive show functions for arbitrary user defined
datatypes similar to Haskell's \"deriving Show\"."""
license = "lgpl"
note = ""
[authors]
[authors.sternagel]
email = "sternagel_email"
[authors.thiemann]
email = "thiemann_email"
[contributors]
[notify]
sternagel = "sternagel_email1"
thiemann = "thiemann_email"
[history]
2015-03-11 = "Adapted development to new-style (BNF-based) datatypes. "
2015-04-10 = """
Moved development for old-style datatypes into subdirectory
\"Old_Datatype\". """
+2024-04-12 = "Added show-class based on string literals, added parsers for nat and int, added injectivity proofs. "
[extra]
[related]
diff --git a/metadata/entries/XML.toml b/metadata/entries/XML.toml
--- a/metadata/entries/XML.toml
+++ b/metadata/entries/XML.toml
@@ -1,36 +1,41 @@
title = "XML"
date = 2014-10-03
topics = [
"Computer science/Functional programming",
"Computer science/Data structures",
]
abstract = """
This entry provides an XML library for Isabelle/HOL. This includes parsing
and pretty printing of XML trees as well as combinators for transforming XML
trees into arbitrary user-defined data. The main contribution of this entry is
an interface (fit for code generation) that allows for communication between
verified programs formalized in Isabelle/HOL and the outside world via XML.
This library was developed as part of the IsaFoR/CeTA project
to which we refer for examples of its usage."""
license = "bsd"
note = ""
[authors]
[authors.sternagel]
email = "sternagel_email"
[authors.thiemann]
email = "thiemann_email"
+[authors.yamada]
+email = "yamada_email"
+
[contributors]
[notify]
sternagel = "sternagel_email"
thiemann = "thiemann_email"
+yamada = "yamada_email"
[history]
+2024-04-12 = "Switched to new XML-transformers, developed by Akihisa Yamada. "
[extra]
[related]
diff --git a/thys/Show/Number_Parser.thy b/thys/Show/Number_Parser.thy
new file mode 100644
--- /dev/null
+++ b/thys/Show/Number_Parser.thy
@@ -0,0 +1,166 @@
+(*
+Author: Christian Sternagel
+Author: René Thiemann
+*)
+
+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
\ No newline at end of file
diff --git a/thys/Show/ROOT b/thys/Show/ROOT
--- a/thys/Show/ROOT
+++ b/thys/Show/ROOT
@@ -1,21 +1,22 @@
chapter AFP
session Show = Deriving +
options [timeout = 600]
sessions
"HOL-Computational_Algebra"
theories
Show_Instances
Show_Poly
Show_Complex
Show_Real_Impl
Shows_Literal
+ Number_Parser
document_files
"root.bib"
"root.tex"
session Old_Datatype_Show in "Old_Datatype" = Datatype_Order_Generator +
options [timeout = 600]
theories
Old_Show_Instances
Old_Show_Examples
diff --git a/thys/Show/Show_Instances.thy b/thys/Show/Show_Instances.thy
--- a/thys/Show/Show_Instances.thy
+++ b/thys/Show/Show_Instances.thy
@@ -1,335 +1,163 @@
(* Title: Show
Author: Christian Sternagel
Author: René Thiemann
Maintainer: Christian Sternagel
Maintainer: René Thiemann
*)
section \Instances of the Show Class for Standard Types\
theory Show_Instances
imports
Show
HOL.Rat
begin
definition showsp_unit :: "unit showsp"
where
"showsp_unit p x = shows_string ''()''"
lemma show_law_unit [show_law_intros]:
"show_law showsp_unit x"
by (rule show_lawI) (simp add: showsp_unit_def show_law_simps)
abbreviation showsp_char :: "char showsp"
where
"showsp_char \ shows_prec"
lemma show_law_char [show_law_intros]:
"show_law showsp_char x"
by (rule show_lawI) (simp add: show_law_simps)
primrec showsp_bool :: "bool showsp"
where
"showsp_bool p True = shows_string ''True''" |
"showsp_bool p False = shows_string ''False''"
lemma show_law_bool [show_law_intros]:
"show_law showsp_bool x"
by (rule show_lawI, cases x) (simp_all add: show_law_simps)
primrec pshowsp_prod :: "(shows \ shows) showsp"
where
"pshowsp_prod p (x, y) = shows_string ''('' o x o shows_string '', '' o y o shows_string '')''"
(*NOTE: in order to be compatible with automatically generated show funtions,
show-arguments of "map"-functions need to get precedence 1 (which may lead to
redundant parentheses in the output, but seems unavoidable in the current setup,
i.e., pshowsp via primrec followed by defining showsp via pshowsp composed with map).*)
definition showsp_prod :: "'a showsp \ 'b showsp \ ('a \ 'b) showsp"
where
[code del]: "showsp_prod s1 s2 p = pshowsp_prod p o map_prod (s1 1) (s2 1)"
lemma showsp_prod_simps [simp, code]:
"showsp_prod s1 s2 p (x, y) =
shows_string ''('' o s1 1 x o shows_string '', '' o s2 1 y o shows_string '')''"
by (simp add: showsp_prod_def)
lemma show_law_prod [show_law_intros]:
"(\x. x \ Basic_BNFs.fsts y \ show_law s1 x) \
(\x. x \ Basic_BNFs.snds y \ show_law s2 x) \
show_law (showsp_prod s1 s2) y"
proof (induct y)
case (Pair x y)
note * = Pair [unfolded prod_set_simps]
show ?case
by (rule show_lawI)
(auto simp del: o_apply intro!: o_append intro: show_lawD * simp: show_law_simps)
qed
-fun string_of_digit :: "nat \ string"
+definition string_of_digit :: "nat \ string"
where
"string_of_digit n =
(if n = 0 then ''0''
else if n = 1 then ''1''
else if n = 2 then ''2''
else if n = 3 then ''3''
else if n = 4 then ''4''
else if n = 5 then ''5''
else if n = 6 then ''6''
else if n = 7 then ''7''
else if n = 8 then ''8''
else ''9'')"
fun showsp_nat :: "nat showsp"
where
"showsp_nat p n =
(if n < 10 then shows_string (string_of_digit n)
else showsp_nat p (n div 10) o shows_string (string_of_digit (n mod 10)))"
declare showsp_nat.simps [simp del]
lemma show_law_nat [show_law_intros]:
"show_law showsp_nat n"
by (rule show_lawI, induct n rule: nat_less_induct) (simp add: show_law_simps showsp_nat.simps)
lemma showsp_nat_append [show_law_simps]:
"showsp_nat p n (x @ y) = showsp_nat p n x @ y"
by (intro show_lawD show_law_intros)
definition showsp_int :: "int showsp"
where
"showsp_int p i =
(if i < 0 then shows_string ''-'' o showsp_nat p (nat (- i)) else showsp_nat p (nat i))"
lemma show_law_int [show_law_intros]:
"show_law showsp_int i"
by (rule show_lawI, cases "i < 0") (simp_all add: showsp_int_def show_law_simps)
lemma showsp_int_append [show_law_simps]:
"showsp_int p i (x @ y) = showsp_int p i x @ y"
by (intro show_lawD show_law_intros)
definition showsp_rat :: "rat showsp"
where
"showsp_rat p x =
(case quotient_of x of (d, n) \
if n = 1 then showsp_int p d else showsp_int p d o shows_string ''/'' o showsp_int p n)"
lemma show_law_rat [show_law_intros]:
"show_law showsp_rat r"
by (rule show_lawI, cases "quotient_of r") (simp add: showsp_rat_def show_law_simps)
lemma showsp_rat_append [show_law_simps]:
"showsp_rat p r (x @ y) = showsp_rat p r x @ y"
by (intro show_lawD show_law_intros)
text \
Automatic show functions are not used for @{type unit}, @{type prod}, and numbers:
for @{type unit} and @{type prod}, we do not want to display @{term "''Unity''"} and
@{term "''Pair''"}; for @{type nat}, we do not want to display
@{term "''Suc (Suc (... (Suc 0) ...))''"}; and neither @{type int}
nor @{type rat} are datatypes.
\
local_setup \
Show_Generator.register_foreign_partial_and_full_showsp @{type_name prod} 0
@{term "pshowsp_prod"}
@{term "showsp_prod"} (SOME @{thm showsp_prod_def})
@{term "map_prod"} (SOME @{thm prod.map_comp}) [true, true]
@{thm show_law_prod}
#> Show_Generator.register_foreign_showsp @{typ unit} @{term "showsp_unit"} @{thm show_law_unit}
#> Show_Generator.register_foreign_showsp @{typ bool} @{term "showsp_bool"} @{thm show_law_bool}
#> Show_Generator.register_foreign_showsp @{typ char} @{term "showsp_char"} @{thm show_law_char}
#> Show_Generator.register_foreign_showsp @{typ nat} @{term "showsp_nat"} @{thm show_law_nat}
#> Show_Generator.register_foreign_showsp @{typ int} @{term "showsp_int"} @{thm show_law_int}
#> Show_Generator.register_foreign_showsp @{typ rat} @{term "showsp_rat"} @{thm show_law_rat}
\
derive "show" option sum prod unit bool nat int rat
export_code
"shows_prec :: 'a::show option showsp"
"shows_prec :: ('a::show, 'b::show) sum showsp"
"shows_prec :: ('a::show \ 'b::show) showsp"
"shows_prec :: unit showsp"
"shows_prec :: char showsp"
"shows_prec :: bool showsp"
"shows_prec :: nat showsp"
"shows_prec :: int showsp"
"shows_prec :: rat showsp"
checking
-text \In the sequel we prove injectivity of @{term "show :: nat \ string"}.\
-
-lemma string_of_digit_inj:
- assumes "x < y \ y < 10"
- shows "string_of_digit x \ string_of_digit y"
- using assms
- apply (cases "y=1", simp)
- apply (cases "y=2", simp)
- apply (cases "y=3", simp)
- apply (cases "y=4", simp)
- apply (cases "y=5", simp)
- apply (cases "y=6", simp)
- apply (cases "y=7", simp)
- apply (cases "y=8", simp)
- apply (cases "y=9", simp)
- by arith
-
-
-lemma string_of_digit_inj_2:
- assumes "x < 10"
- shows "length (string_of_digit x) = 1"
- using assms
- apply (cases "x=0", simp)
- apply (cases "x=1", simp)
- apply (cases "x=2", simp)
- apply (cases "x=3", simp)
- apply (cases "x=4", simp)
- apply (cases "x=5", simp)
- apply (cases "x=6", simp)
- apply (cases "x=7", simp)
- apply (cases "x=8", simp)
- apply (cases "x=9", simp)
- by arith
-
-declare string_of_digit.simps[simp del]
-
-lemma string_of_digit_inj_1:
- assumes "x < 10" and "y < 10" and "x \ y"
- shows "string_of_digit x \ string_of_digit y"
-proof
- assume ass: "string_of_digit x = string_of_digit y"
- with assms have "\ xx yy :: nat. xx < 10 \ yy < 10 \ xx < yy \ string_of_digit xx = string_of_digit yy"
- proof (cases "x < y", blast)
- case False
- with \x \ y\ have "y < x" by arith
- with assms ass have "y < 10 \ x < 10 \ y < x \ string_of_digit y = string_of_digit x" by auto
- then show ?thesis by blast
- qed
- from this obtain xx yy :: nat where cond: "xx < 10 \ yy < 10 \ xx < yy \ string_of_digit xx = string_of_digit yy" by blast
- then show False using string_of_digit_inj by auto
-qed
-
-lemma shows_prec_nat_simp1:
- fixes n::nat assumes "\ n < 10" shows "shows_prec d n xs = ((shows_prec d (n div 10) \ shows_string (string_of_digit (n mod 10)))) xs"
- using showsp_nat.simps[of d n]
- unfolding if_not_P[OF assms] shows_string_def o_def
- unfolding shows_prec_nat_def by simp
-
-lemma show_nat_simp1: "\ (n::nat) < 10 \ show n = show (n div 10) @ string_of_digit (n mod 10)"
- using shows_prec_nat_simp1[of n "0::nat" "[]"] unfolding shows_string_def o_def
- unfolding shows_prec_append[symmetric] by simp
-
-lemma show_nat_len_1: fixes x :: nat
- shows "length (show x) > 0"
-proof (cases "x < 10")
- assume ass: "\ x < 10"
- then have "show x = show (x div 10) @ string_of_digit (x mod 10)" by (rule show_nat_simp1)
- then have "length (show x) = length (show (x div 10)) + length (string_of_digit (x mod 10))"
- unfolding length_append[symmetric] by simp
- with ass show ?thesis by (simp add: string_of_digit_inj_2)
-next
- assume "x < 10" then show ?thesis
- unfolding shows_prec_nat_def
- unfolding showsp_nat.simps[of 0 x]
- unfolding shows_string_def by (simp add: string_of_digit_inj_2)
-qed
-
-lemma shows_prec_nat_simp2:
- fixes n::nat assumes "n < 10" shows "shows_prec d n xs = string_of_digit n @ xs"
- using showsp_nat.simps[of d n]
- unfolding shows_prec_nat_def if_P[OF assms] shows_string_def by simp
-
-lemma show_nat_simp2:
- fixes n::nat assumes "n < 10" shows "show n = string_of_digit n"
- using shows_prec_nat_simp2[OF assms, of "0::nat" "[]"] by simp
-
-lemma show_nat_len_2:
- fixes x :: nat
- assumes one: "length (show x) = 1"
- shows "x < 10"
-proof (rule ccontr)
- assume ass: "\ x < 10"
- then have "show x = show (x div 10) @ string_of_digit (x mod 10)" by (rule show_nat_simp1)
- then have "length (show x) = length (show (x div 10)) + length (string_of_digit (x mod 10))"
- unfolding length_append[symmetric] by simp
- with one have "length (show (x div 10)) = 0" by (simp add: string_of_digit_inj_2)
- with show_nat_len_1 show False by best
-qed
-
-lemma show_nat_len_3:
- fixes x :: nat
- assumes one: "length (show x) > 1"
- shows "\ x < 10"
-proof
- assume ass: "x < 10"
- then have "show x = string_of_digit x" by (rule show_nat_simp2)
- with string_of_digit_inj_2 ass have "length (show x) = 1" by simp
- with one show False by arith
-qed
-
-lemma inj_show_nat: "inj (show::nat \ string)"
- unfolding inj_on_def
-proof (clarify)
- fix x y :: nat assume "show x = show y"
- then obtain n where "length (show x) = n \ show x = show y" by blast
- then show "x = y"
- proof (induct n arbitrary: x y)
- case 0
- fix x y :: nat
- assume ass: "length (show x) = 0 \ show x = show y"
- then show ?case using show_nat_len_1 by best
- next
- case (Suc n)
- then have eq: "show x = show y" by blast
- from Suc have len: "length (show x) = Suc n" by blast
- show ?case
- proof (cases n)
- case 0
- with Suc have one: "length(show x) = 1 \ length (show y) = 1" by (auto)
- with show_nat_len_2 have ten: "x < 10 \ y < 10" by simp
- show ?thesis
- proof (cases "x = y", simp)
- case False
- with ten string_of_digit_inj_1 have "string_of_digit x \ string_of_digit y" by auto
- with ten eq show ?thesis using show_nat_simp2[of x] show_nat_simp2[of y] by simp
- qed
- next
- case (Suc m)
- with len eq have "length (show x) = Suc (Suc m) \ length (show y) = Suc (Suc m)" by auto
- then have "length (show x) > 1 \ length (show y) > 1" by simp
- then have large: "\ x < 10 \ \ y < 10" using show_nat_len_3 by simp
- let ?e = "\x::nat. show (x div 10) @ string_of_digit (x mod 10)"
- from large have id: "show x = ?e x \ show y = ?e y"
- using show_nat_simp1[of x] show_nat_simp1[of y] by auto
- from string_of_digit_inj_2 have one: "length (string_of_digit(x mod 10)) = 1
- \ length(string_of_digit(y mod 10)) = 1" by auto
- from one have "\xx. string_of_digit(x mod 10) = [xx]"
- by (cases "string_of_digit (x mod 10)",simp,cases "tl (string_of_digit (x mod 10))",simp,simp)
- from this obtain xx where xx: "string_of_digit(x mod 10) = [xx]" ..
- from one have "\xx. string_of_digit(y mod 10) = [xx]"
- by (cases "string_of_digit (y mod 10)",simp,cases "tl (string_of_digit (y mod 10))",simp,simp)
- from this obtain yy where yy: "string_of_digit(y mod 10) = [yy]" ..
- from id have "length (show x) = length (show (x div 10)) + length (string_of_digit (x mod 10))" unfolding length_append[symmetric] by simp
- with one len have shorter: "length (show (x div 10)) = n" by simp
- from eq id xx yy
- have "(show (x div 10) @ [xx]) = (show (y div 10) @ [yy])" by simp
- then have "(show (x div 10) = show(y div 10)) \ xx = yy" by clarify
- then have nearly: "show (x div 10) = show (y div 10)
- \ string_of_digit(x mod 10) = string_of_digit(y mod 10)" using xx yy by simp
- with shorter and
- \length (show (x div 10)) = n \ show (x div 10) = show (y div 10) \ x div 10 = y div 10\
- have div: "x div 10 = y div 10" by blast
- from nearly string_of_digit_inj_1 have mod: "x mod 10 = y mod 10"
- by (cases "x mod 10 = y mod 10", simp, simp)
- have "x = 10 * (x div 10) + (x mod 10)" by auto
- also have "\ = 10 * (y div 10) + (y mod 10)" using div mod by auto
- also have "\ = y" by auto
- finally show ?thesis .
- qed
- qed
-qed
-
end
diff --git a/thys/Show/Shows_Literal.thy b/thys/Show/Shows_Literal.thy
--- a/thys/Show/Shows_Literal.thy
+++ b/thys/Show/Shows_Literal.thy
@@ -1,177 +1,177 @@
(* Title: Shows_Literal
Author: René Thiemann
Maintainer: René Thiemann
*)
section \Show Based on String Literals\
theory Shows_Literal
imports
Main
- Show.Show_Real
+ Show_Real
begin
text \In this theory we provide an alternative to the @{class show}-class, where
@{typ String.literal} instead of @{typ string} is used, with the aim that target-language
readable strings are used in generated code. In particular when writing Isabelle functions that
produce strings such as @{term "STR ''this is info for the user: ...''"},
this class might be useful.
To keep it simple, in contrast to @{class show}, here we do not enforce the show law.\
type_synonym showsl = "String.literal \ String.literal"
definition showsl_of_shows :: "shows \ showsl" where
"showsl_of_shows shws s = String.implode (shws []) + s"
definition showsl_lit :: "String.literal \ showsl" where
"showsl_lit = (+)"
definition "showsl_paren s = showsl_lit (STR ''('') o s o showsl_lit (STR '')'')"
fun showsl_sep :: "('a \ showsl) \ showsl \ 'a list \ showsl"
where
"showsl_sep s sep [] = showsl_lit (STR '''')" |
"showsl_sep s sep [x] = s x" |
"showsl_sep s sep (x#xs) = s x o sep o showsl_sep s sep xs"
definition
showsl_list_gen :: "('a \ showsl) \ String.literal \ String.literal
\ String.literal \ String.literal \ 'a list \ showsl"
where
"showsl_list_gen showslx e l s r xs =
(if xs = [] then showsl_lit e
else showsl_lit l o showsl_sep showslx (showsl_lit s) xs o showsl_lit r)"
definition default_showsl_list :: "('a \ showsl) \ 'a list \ showsl" where
"default_showsl_list sl = showsl_list_gen sl (STR ''[]'') (STR ''['') (STR '', '') (STR '']'')"
definition [code_unfold]: "char_zero = (48 :: integer)"
lemma char_zero: "char_zero = integer_of_char (CHR ''0'')" by code_simp
fun lit_of_digit :: "nat \ String.literal" where
"lit_of_digit n =
String.implode [char_of_integer (char_zero + integer_of_nat n)]"
class showl =
fixes showsl :: "'a \ showsl"
and showsl_list :: "'a list \ showsl"
definition "showsl_lines desc_empty = showsl_list_gen showsl desc_empty (STR '''') (STR ''\'') (STR '''')"
abbreviation showl where "showl x \ showsl x (STR '''')"
instantiation char :: showl
begin
definition "showsl_char c = showsl_lit (String.implode [c])" \ \Shouldn't there be a faster conversion than via strings?\
definition "showsl_list_char cs s = showsl_lit (String.implode cs) s"
instance ..
end
instantiation String.literal :: showl
begin
definition "showsl (s :: String.literal) = showsl_lit s"
definition "showsl_list (xs :: String.literal list) = default_showsl_list showsl xs"
instance ..
end
instantiation bool :: showl
begin
definition "showsl (b :: bool) = showsl_lit (if b then STR ''True'' else STR ''False'')"
definition "showsl_list (xs :: bool list) = default_showsl_list showsl xs"
instance ..
end
instantiation nat :: showl
begin
fun showsl_nat :: "nat \ showsl" where
"showsl_nat n =
(if n < 10 then showsl_lit (lit_of_digit n)
else showsl_nat (n div 10) o showsl_lit (lit_of_digit (n mod 10)))"
definition "showsl_list (xs :: nat list) = default_showsl_list showsl xs"
instance ..
end
instantiation int :: showl
begin
definition "showsl_int i =
(if i < 0 then showsl_lit (STR ''-'') o showsl (nat (- i)) else showsl (nat i))"
definition "showsl_list (xs :: int list) = default_showsl_list showsl xs"
instance ..
end
instantiation integer :: showl
begin
definition showsl_integer :: "integer \ showsl" where "showsl_integer i = showsl (int_of_integer i)"
definition showsl_list_integer :: "integer list \ showsl" where "showsl_list_integer xs = default_showsl_list showsl xs"
instance ..
end
instantiation rat :: showl
begin
definition "showsl_rat x =
(case quotient_of x of (d, n) \
if n = 1 then showsl d else showsl d o showsl_lit (STR ''/'') o showsl n)"
definition "showsl_list (xs :: rat list) = default_showsl_list showsl xs"
instance ..
end
instantiation real :: showl
begin
definition "showsl (x :: real) = showsl_lit (String.implode (show_real x))"
definition "showsl_list (xs :: real list) = default_showsl_list showsl xs"
instance ..
end
instantiation unit :: showl
begin
definition "showsl (x :: unit) = showsl_lit (STR ''()'')"
definition "showsl_list (xs :: unit list) = default_showsl_list showsl xs"
instance ..
end
instantiation option :: (showl) showl
begin
fun showsl_option where
"showsl_option None = showsl_lit (STR ''None'')"
| "showsl_option (Some x) = showsl_lit (STR ''Some ('') o showsl x o showsl_lit (STR '')'')"
definition "showsl_list (xs :: 'a option list) = default_showsl_list showsl xs"
instance ..
end
instantiation sum :: (showl,showl) showl
begin
fun showsl_sum where
"showsl_sum (Inl x) = showsl_lit (STR ''Inl ('') o showsl x o showsl_lit (STR '')'')"
| "showsl_sum (Inr x) = showsl_lit (STR ''Inr ('') o showsl x o showsl_lit (STR '')'')"
definition "showsl_list (xs :: ('a + 'b) list) = default_showsl_list showsl xs"
instance ..
end
instantiation prod :: (showl,showl) showl
begin
fun showsl_prod where
"showsl_prod (Pair x y) = showsl_lit (STR ''('') o showsl x
o showsl_lit (STR '', '') o showsl y o showsl_lit (STR '')'')"
definition "showsl_list (xs :: ('a * 'b) list) = default_showsl_list showsl xs"
instance ..
end
definition [code_unfold]: "showsl_nl = showsl (STR ''\'')"
definition add_index :: "showsl \ nat \ showsl" where
"add_index s i = s o showsl_lit (STR ''.'') o showsl i"
instantiation list :: (showl) showl
begin
definition showsl_list :: "'a list \ showsl" where
"showsl_list (xs :: 'a list) = showl_class.showsl_list xs"
definition "showsl_list_list (xs :: 'a list list) = default_showsl_list showsl xs"
instance ..
end
end
diff --git a/thys/XML/Example_Application.thy b/thys/XML/Example_Application.thy
new file mode 100644
--- /dev/null
+++ b/thys/XML/Example_Application.thy
@@ -0,0 +1,51 @@
+(*
+Author: René Thiemann
+*)
+theory Example_Application
+ imports
+ Xmlt
+begin
+
+text \Let us consider inputs that consist of an optional number and a list of first order terms,
+ where these terms use strings as function names and numbers for variables.
+ We assume that we have a XML-document that describes these kinds of inputs and now want to parse them.\
+
+definition exampleInput where "exampleInput = STR
+ ''
+ 42
+
+ fo<>bar
+ 1
+ 3
+
+ 15
+ ''"
+
+datatype fo_term = Fun string "fo_term list" | Var int
+
+definition var :: "fo_term xmlt" where "var = xml_change (xml_int (STR ''var'')) (xml_return \ Var)"
+
+text \a recursive parser is best defined via partial-function. Note that the xml-argument
+ should be provided, otherwise strict evalution languages will not terminate.\
+partial_function (sum_bot) parse_term :: "fo_term xmlt"
+where
+ [code]: "parse_term xml = (
+ XMLdo (STR ''funapp'') {
+ name \ xml_text (STR ''symbol'');
+ args \* parse_term;
+ xml_return (Fun name args)
+ } XMLor var) xml"
+
+text \for non-recursive parsers, we can eta-contract\
+definition parse_input :: "(int option \ fo_term list) xmlt" where
+ "parse_input = XMLdo (STR ''input'') {
+ onum \? xml_int (STR ''magicNumber'');
+ terms \* parse_term;
+ xml_return (onum,terms)
+ }"
+
+definition test where "test = parse_xml_string parse_input (String.explode exampleInput)"
+
+value test (* successfully parses the example input *)
+export_code test checking SML
+end
\ No newline at end of file
diff --git a/thys/XML/ROOT b/thys/XML/ROOT
--- a/thys/XML/ROOT
+++ b/thys/XML/ROOT
@@ -1,11 +1,12 @@
chapter AFP
session XML = "HOL-Library" +
options [timeout = 600]
sessions
Certification_Monads
Show
theories
Xmlt
+ Example_Application
document_files
"root.tex"
diff --git a/thys/XML/Xml.thy b/thys/XML/Xml.thy
--- a/thys/XML/Xml.thy
+++ b/thys/XML/Xml.thy
@@ -1,880 +1,880 @@
(* Title: Xml
Author: Christian Sternagel
Author: René Thiemann
*)
section \Parsing and Printing XML Documents\
theory Xml
imports
Certification_Monads.Parser_Monad
"HOL-Library.Char_ord"
"HOL-Library.Code_Abstract_Char"
begin
datatype xml =
\ \node-name, attributes, child-nodes\
XML string "(string \ string) list" "xml list" |
XML_text string
datatype xmldoc =
\ \header, body\
XMLDOC "string list" (root_node: xml)
fun tag :: "xml \ string" where
"tag (XML name _ _ ) = name" |
"tag (XML_text _) = []"
hide_const (open) tag
fun children :: "xml \ xml list" where
"children (XML _ _ cs) = cs" |
"children (XML_text _) = []"
hide_const (open) children
fun num_children :: "xml \ nat" where
"num_children (XML _ _ cs) = length cs" |
"num_children (XML_text _) = 0"
hide_const (open) num_children
subsection \Printing of XML Nodes and Documents\
instantiation xml :: "show"
begin
definition shows_attr :: "string \ string \ shows"
where
"shows_attr av = shows (fst av) o shows_string (''=\"'' @ snd av @ ''\"'')"
definition shows_attrs :: "(string \ string) list \ shows"
where
"shows_attrs as = foldr (\a. '' '' +#+ shows_attr a) as"
fun shows_XML_indent :: "string \ nat \ xml \ shows"
where
"shows_XML_indent ind i (XML n a c) =
(''\'' +#+ ind +#+ ''<'' +#+ shows n +@+ shows_attrs a +@+
(if c = [] then shows_string ''/>''
else (
''>'' +#+
foldr (shows_XML_indent (replicate i (CHR '' '') @ ind) i) c +@+ ''\'' +#+ ind +#+
'''')))" |
"shows_XML_indent ind i (XML_text t) = shows_string t"
definition "shows_prec (d::nat) xml = shows_XML_indent '''' 2 xml"
definition "shows_list (xs :: xml list) = showsp_list shows_prec 0 xs"
lemma shows_attr_append:
"(s +#+ shows_attr av) (r @ t) = (s +#+ shows_attr av) r @ t"
unfolding shows_attr_def by (cases av) (auto simp: show_law_simps)
lemma shows_attrs_append [show_law_simps]:
"shows_attrs as (r @ s) = shows_attrs as r @ s"
using shows_attr_append by (induct as) (simp_all add: shows_attrs_def)
lemma append_xml':
"shows_XML_indent ind i xml (r @ s) = shows_XML_indent ind i xml r @ s"
by (induct xml arbitrary: ind r s) (auto simp: show_law_simps)
lemma shows_prec_xml_append [show_law_simps]:
"shows_prec d (xml::xml) (r @ s) = shows_prec d xml r @ s"
unfolding shows_prec_xml_def by (rule append_xml')
instance
by standard (simp_all add: show_law_simps shows_list_xml_def)
end
instantiation xmldoc :: "show"
begin
fun shows_xmldoc
where
"shows_xmldoc (XMLDOC h x) = shows_lines h o shows_nl o shows x"
definition "shows_prec (d::nat) doc = shows_xmldoc doc"
definition "shows_list (xs :: xmldoc list) = showsp_list shows_prec 0 xs"
lemma shows_prec_xmldoc_append [show_law_simps]:
"shows_prec d (x::xmldoc) (r @ s) = shows_prec d x r @ s"
by (cases x) (auto simp: shows_prec_xmldoc_def show_law_simps)
instance
by standard (simp_all add: show_law_simps shows_list_xmldoc_def)
end
subsection \XML-Parsing\
definition parse_text :: "string option parser"
where
"parse_text = do {
ts \ many ((\) CHR ''<'');
let text = trim ts;
if text = [] then return None
else return (Some (List.rev (trim (List.rev text))))
}"
lemma is_parser_parse_text [intro]:
"is_parser parse_text"
by (auto simp: parse_text_def)
lemma parse_text_consumes:
assumes *: "ts \ []" "hd ts \ CHR ''<''"
and parse: "parse_text ts = Inr (t, ts')"
shows "length ts' < length ts"
proof -
from * obtain a tss where ts: "ts = a # tss" and not: "a \ CHR ''<''"
by (cases ts, auto)
note parse = parse [unfolded parse_text_def Let_def ts]
from parse obtain x1 x2 where many: "many ((\) CHR ''<'') tss = Inr (x1, x2)"
using not by (cases "many ((\) CHR ''<'') tss",
auto simp: bind_def)
from is_parser_many many have len: "length x2 \ length tss" by blast
from parse many have "length ts' \ length x2"
using not by (simp add: bind_def return_def split: if_splits)
with len show ?thesis unfolding ts by auto
qed
definition parse_attribute_value :: "string parser"
where
"parse_attribute_value = do {
exactly [CHR ''\"''];
v \ many ((\) CHR ''\"'');
exactly [CHR ''\"''];
return v
}"
lemma is_parser_parse_attribute_value [intro]:
"is_parser parse_attribute_value"
by (auto simp: parse_attribute_value_def)
text \A list of characters that are considered to be "letters" for tag-names.\
definition letters :: "char list"
where
"letters = ''abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ_0123456789&;:-''"
definition is_letter :: "char \ bool"
where
"is_letter c \ c \ set letters"
lemma is_letter_pre_code:
"is_letter c \
CHR ''a'' \ c \ c \ CHR ''z'' \
CHR ''A'' \ c \ c \ CHR ''Z'' \
CHR ''0'' \ c \ c \ CHR ''9'' \
c \ set ''_&;:-''"
by (cases c) (simp add: less_eq_char_def is_letter_def letters_def)
definition many_letters :: "string parser"
where
[simp]: "many_letters = manyof letters"
lemma many_letters [code, code_unfold]:
"many_letters = many is_letter"
by (simp add: is_letter_def [abs_def] manyof_def)
definition parse_name :: "string parser"
where
"parse_name s = (do {
n \ many_letters;
spaces;
if n = [] then
error (''expected letter '' @ letters @ '' but first symbol is \"'' @ take 1 s @ ''\"'')
else return n
}) s"
lemma is_parser_parse_name [intro]:
"is_parser parse_name"
proof
fix s r x
assume res: "parse_name s = Inr (x, r)"
let ?exp = "do {
n \ many_letters;
spaces;
if n = [] then
error (''expected letter '' @ letters @ '' but first symbol is \"'' @ take 1 s @ ''\"'')
else return n
}"
have isp: "is_parser ?exp" by auto
have id: "parse_name s = ?exp s" by (simp add: parse_name_def)
from isp [unfolded is_parser_def, rule_format, OF res [unfolded id]]
show "length r \ length s" .
qed
function (sequential) parse_attributes :: "(string \ string) list parser"
where
"parse_attributes [] = Error_Monad.return ([], [])" |
"parse_attributes (c # s) =
(if c \ set ''/>'' then Error_Monad.return ([], c # s)
else (do {
k \