Theory Xmlt
section ‹XML Transformers for Extracting Data from XML Nodes›
theory Xmlt
imports
Xml
Certification_Monads.Strict_Sum
HOL.Rat
begin
type_synonym
tag = string
text ‹The type of transformers on xml nodes.›
type_synonym
'a xmlt = "xml ⇒ string +⇩⊥ 'a"
definition map :: "(xml ⇒ ('e +⇩⊥ 'a)) ⇒ xml list ⇒ 'e +⇩⊥ 'a list"
where
[code_unfold]: "map = map_sum_bot"
lemma map_mono [partial_function_mono]:
fixes C :: "xml ⇒ ('b ⇒ ('e +⇩⊥ 'c)) ⇒ 'e +⇩⊥ 'd"
assumes C: "⋀y. y ∈ set B ⟹ mono_sum_bot (C y)"
shows "mono_sum_bot (λf. map (λy. C y f) B)"
unfolding map_def by (auto intro: partial_function_mono C)
hide_const (open) map
fun "text" :: "tag ⇒ string xmlt"
where
"text tag (XML n atts [XML_text t]) =
(if n = tag ∧ atts = [] then return t
else error (concat
[''could not extract text for '', tag,'' from '', ''⏎'', show (XML n atts [XML_text t])]))"
| "text tag xml = error (concat [''could not extract text for '', tag,'' from '', ''⏎'', show xml])"
hide_const (open) "text"
definition bool_of_string :: "string ⇒ string +⇩⊥ bool"
where
"bool_of_string s =
(if s = ''true'' then return True
else if s = ''false'' then return False
else error (''cannot convert '' @ s @ '' into Boolean''))"
fun bool :: "tag ⇒ bool xmlt"
where
"bool tag node = Xmlt.text tag node ⤜ bool_of_string"
hide_const (open) bool
definition fail :: "tag ⇒ 'a xmlt"
where
"fail tag xml =
error (concat
[''could not transform the following xml element (expected '', tag, '')'', ''⏎'', show xml])"
hide_const (open) fail
definition guard :: "(xml ⇒ bool) ⇒ 'a xmlt ⇒ 'a xmlt ⇒ 'a xmlt"
where
"guard p p1 p2 x = (if p x then p1 x else p2 x)"
hide_const (open) guard
lemma guard_mono [partial_function_mono]:
assumes p1: "⋀y. mono_sum_bot (p1 y)"
and p2: "⋀y. mono_sum_bot (p2 y)"
shows "mono_sum_bot (λg. Xmlt.guard p (λy. p1 y g) (λy. p2 y g) x)"
by (cases x) (auto intro!: partial_function_mono p1 p2 simp: Xmlt.guard_def)
fun leaf :: "tag ⇒ 'a ⇒ 'a xmlt"
where
"leaf tag x (XML name atts cs) =
(if name = tag ∧ atts = [] ∧ cs = [] then return x
else Xmlt.fail tag (XML name atts cs))" |
"leaf tag x xml = Xmlt.fail tag xml"
hide_const (open) leaf
fun list1element :: "'a list ⇒ 'a option"
where
"list1element [x] = Some x" |
"list1element _ = None"
fun singleton :: "tag ⇒ 'a xmlt ⇒ ('a ⇒ 'b) ⇒ 'b xmlt"
where
"singleton tag p1 f xml =
(case xml of
XML name atts cs ⇒
(if name = tag ∧ atts = [] then
(case list1element cs of
Some (cs1) ⇒ p1 cs1 ⤜ return ∘ f
| None ⇒ Xmlt.fail tag xml)
else Xmlt.fail tag xml)
| _ ⇒ Xmlt.fail tag xml)"
hide_const (open) singleton
lemma singleton_mono [partial_function_mono]:
assumes p: "⋀y. mono_sum_bot (p1 y)"
shows "mono_sum_bot (λg. Xmlt.singleton t (λy. p1 y g) f x)"
by (cases x, cases "list1element (Xml.children x)") (auto intro!: partial_function_mono p)
fun list2elements :: "'a list ⇒ ('a × 'a) option"
where
"list2elements [x, y] = Some (x, y)" |
"list2elements _ = None"
fun pair :: "tag ⇒ 'a xmlt ⇒ 'b xmlt ⇒ ('a ⇒ 'b ⇒ 'c) ⇒ 'c xmlt"
where
"pair tag p1 p2 f xml =
(case xml of
XML name atts cs ⇒
(if name = tag ∧ atts = [] then
(case list2elements cs of
Some (cs1, cs2) ⇒
do {
a ← p1 cs1;
b ← p2 cs2;
return (f a b)
}
| None ⇒ Xmlt.fail tag xml)
else Xmlt.fail tag xml)
| _ ⇒ Xmlt.fail tag xml)"
hide_const (open) pair
lemma pair_mono [partial_function_mono]:
assumes "⋀y. mono_sum_bot (p1 y)"
and "⋀y. mono_sum_bot (p2 y)"
shows "mono_sum_bot (λg. Xmlt.pair t (λy. p1 y g) (λ y. p2 y g) f x)"
using assms
by (cases x, cases "list2elements (Xml.children x)") (auto intro!: partial_function_mono)
fun list3elements :: "'a list ⇒ ('a × 'a × 'a) option"
where
"list3elements [x, y, z] = Some (x, y, z)" |
"list3elements _ = None"
fun triple :: "string ⇒ 'a xmlt ⇒ 'b xmlt ⇒ 'c xmlt ⇒ ('a ⇒ 'b ⇒ 'c ⇒ 'd) ⇒ 'd xmlt"
where
"triple tag p1 p2 p3 f xml = (case xml of XML name atts cs ⇒
(if name = tag ∧ atts = [] then
(case list3elements cs of
Some (cs1, cs2, cs3) ⇒
do {
a ← p1 cs1;
b ← p2 cs2;
c ← p3 cs3;
return (f a b c)
}
| None ⇒ Xmlt.fail tag xml)
else Xmlt.fail tag xml)
| _ ⇒ Xmlt.fail tag xml)"
lemma triple_mono [partial_function_mono]:
assumes "⋀y. mono_sum_bot (p1 y)"
and "⋀y. mono_sum_bot (p2 y)"
and "⋀y. mono_sum_bot (p3 y)"
shows "mono_sum_bot (λg. Xmlt.triple t (λy. p1 y g) (λ y. p2 y g) (λ y. p3 y g) f x)"
using assms
by (cases x, cases "list3elements (Xml.children x)", auto intro!: partial_function_mono)
fun list4elements :: "'a list ⇒ ('a × 'a × 'a × 'a) option"
where
"list4elements [x, y, z, u] = Some (x, y, z, u)" |
"list4elements _ = None"
fun
tuple4 ::
"string ⇒ 'a xmlt ⇒ 'b xmlt ⇒ 'c xmlt ⇒ 'd xmlt ⇒ ('a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e) ⇒ 'e xmlt"
where
"tuple4 tag p1 p2 p3 p4 f xml =
(case xml of
XML name atts cs ⇒
(if name = tag ∧ atts = [] then
(case list4elements cs of
Some (cs1, cs2, cs3, cs4) ⇒
do {
a ← p1 cs1;
b ← p2 cs2;
c ← p3 cs3;
d ← p4 cs4;
return (f a b c d)
}
| None ⇒ Xmlt.fail tag xml)
else Xmlt.fail tag xml)
| _ ⇒ Xmlt.fail tag xml)"
lemma tuple4_mono [partial_function_mono]:
assumes "⋀y. mono_sum_bot (p1 y)"
and "⋀y. mono_sum_bot (p2 y)"
and "⋀y. mono_sum_bot (p3 y)"
and"⋀y. mono_sum_bot (p4 y)"
shows "mono_sum_bot (λg. Xmlt.tuple4 t (λy. p1 y g) (λ y. p2 y g) (λ y. p3 y g) (λ y. p4 y g) f x)"
using assms
by (cases x, cases "list4elements (Xml.children x)") (auto intro!: partial_function_mono)
fun list5elements :: "'a list ⇒ ('a × 'a × 'a × 'a × 'a) option"
where
"list5elements [x, y, z, u, v] = Some (x, y, z, u, v)" |
"list5elements _ = None"
fun
tuple5 ::
"string ⇒ 'a xmlt ⇒ 'b xmlt ⇒ 'c xmlt ⇒ 'd xmlt ⇒ 'e xmlt ⇒
('a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'f) ⇒ 'f xmlt"
where
"tuple5 tag p1 p2 p3 p4 p5 f xml =
(case xml of
XML name atts cs ⇒
(if name = tag ∧ atts = [] then
(case list5elements cs of
Some (cs1,cs2,cs3,cs4,cs5) ⇒
do {
a ← p1 cs1;
b ← p2 cs2;
c ← p3 cs3;
d ← p4 cs4;
e ← p5 cs5;
return (f a b c d e)
}
| None ⇒ Xmlt.fail tag xml)
else Xmlt.fail tag xml)
| _ ⇒ Xmlt.fail tag xml)"
lemma tuple5_mono [partial_function_mono]:
assumes "⋀y. mono_sum_bot (p1 y)"
and "⋀y. mono_sum_bot (p2 y)"
and "⋀y. mono_sum_bot (p3 y)"
and "⋀y. mono_sum_bot (p4 y)"
and "⋀y. mono_sum_bot (p5 y)"
shows "mono_sum_bot (λg. Xmlt.tuple5 t (λy. p1 y g) (λ y. p2 y g) (λ y. p3 y g) (λ y. p4 y g) (λ y. p5 y g) f x)"
using assms
by (cases x, cases "list5elements (Xml.children x)") (auto intro!: partial_function_mono)
fun list6elements :: "'a list ⇒ ('a × 'a × 'a × 'a × 'a × 'a) option"
where
"list6elements [x, y, z, u, v, w] = Some (x, y, z, u, v, w)" |
"list6elements _ = None"
fun
tuple6 ::
"string ⇒ 'a xmlt ⇒ 'b xmlt ⇒ 'c xmlt ⇒ 'd xmlt ⇒ 'e xmlt ⇒ 'f xmlt ⇒
('a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'f ⇒ 'g) ⇒ 'g xmlt"
where
"tuple6 tag p1 p2 p3 p4 p5 p6 f xml =
(case xml of
XML name atts cs ⇒
(if name = tag ∧ atts = [] then
(case list6elements cs of
Some (cs1,cs2,cs3,cs4,cs5,cs6) ⇒
do {
a ← p1 cs1;
b ← p2 cs2;
c ← p3 cs3;
d ← p4 cs4;
e ← p5 cs5;
ff ← p6 cs6;
return (f a b c d e ff)
}
| None ⇒ Xmlt.fail tag xml)
else Xmlt.fail tag xml)
| _ ⇒ Xmlt.fail tag xml)"
lemma tuple6_mono [partial_function_mono]:
assumes "⋀y. mono_sum_bot (p1 y)"
and "⋀y. mono_sum_bot (p2 y)"
and "⋀y. mono_sum_bot (p3 y)"
and "⋀y. mono_sum_bot (p4 y)"
and "⋀y. mono_sum_bot (p5 y)"
and "⋀y. mono_sum_bot (p6 y)"
shows "mono_sum_bot (λg. Xmlt.tuple6 t (λy. p1 y g) (λ y. p2 y g) (λ y. p3 y g) (λ y. p4 y g) (λ y. p5 y g) (λ y. p6 y g) f x)"
using assms
by (cases x, cases "list6elements (Xml.children x)") (auto intro!: partial_function_mono)
fun optional :: "tag ⇒ 'a xmlt ⇒ ('a option ⇒ 'b) ⇒ 'b xmlt"
where
"optional tag p1 f (XML name atts cs) =
(let l = length cs in
(if name = tag ∧ atts = [] ∧ l ≥ 0 ∧ l ≤ 1 then do {
if l = 1 then do {
x1 ← p1 (cs ! 0);
return (f (Some x1))
} else return (f None)
} else Xmlt.fail tag (XML name atts cs)))" |
"optional tag p1 f xml = Xmlt.fail tag xml"
lemma optional_mono [partial_function_mono]:
assumes "⋀y. mono_sum_bot (p1 y)"
shows "mono_sum_bot (λg. Xmlt.optional t (λy. p1 y g) f x)"
using assms by (cases x) (auto intro!: partial_function_mono)
fun xml1to2elements :: "string ⇒ 'a xmlt ⇒ 'b xmlt ⇒ ('a ⇒ 'b option ⇒ 'c) ⇒ 'c xmlt"
where
"xml1to2elements tag p1 p2 f (XML name atts cs) = (
let l = length cs in
(if name = tag ∧ atts = [] ∧ l ≥ 1 ∧ l ≤ 2
then do {
x1 ← p1 (cs ! 0);
(if l = 2
then do {
x2 ← p2 (cs ! 1);
return (f x1 (Some x2))
} else return (f x1 None))
} else Xmlt.fail tag (XML name atts cs)))" |
"xml1to2elements tag p1 p2 f xml = Xmlt.fail tag xml"
lemma xml1to2elements_mono[partial_function_mono]:
assumes p1: "⋀y. mono_sum_bot (p1 y)"
"⋀y. mono_sum_bot (p2 y)"
shows "mono_sum_bot (λg. xml1to2elements t (λy. p1 y g) (λy. p2 y g) f x)"
by (cases x, auto intro!: partial_function_mono p1)
text ‹
Apply the first transformer to the first child-node, then check the second child-node,
which is must be a Boolean. If the Boolean is true, then apply the second transformer
to the last child-node.
›
fun xml2nd_choice :: "tag ⇒ 'a xmlt ⇒ tag ⇒ 'b xmlt ⇒ ('a ⇒ 'b option ⇒ 'c) ⇒ 'c xmlt"
where
"xml2nd_choice tag p1 cn p2 f (XML name atts cs) = (
let l = length cs in
(if name = tag ∧ atts = [] ∧ l ≥ 2 then do {
x1 ← p1 (cs ! 0);
b ← Xmlt.bool cn (cs ! 1);
(if b then do {
x2 ← p2 (cs ! (l - 1));
return (f x1 (Some x2))
} else return (f x1 None))
} else Xmlt.fail tag (XML name atts cs)))" |
"xml2nd_choice tag p1 cn p2 f xml = Xmlt.fail tag xml"
lemma xml2nd_choice_mono [partial_function_mono]:
assumes p1: "⋀y. mono_sum_bot (p1 y)"
"⋀y. mono_sum_bot (p2 y)"
shows "mono_sum_bot (λg. xml2nd_choice t (λy. p1 y g) h (λy. p2 y g) f x)"
by (cases x, auto intro!: partial_function_mono p1)
fun
xml2to3elements ::
"string ⇒ 'a xmlt ⇒ 'b xmlt ⇒ 'c xmlt ⇒ ('a ⇒ 'b ⇒ 'c option ⇒ 'd) ⇒ 'd xmlt"
where
"xml2to3elements tag p1 p2 p3 f (XML name atts cs) = (
let l = length cs in
(if name = tag ∧ atts = [] ∧ l ≥ 2 ∧ l ≤ 3 then do {
x1 ← p1 (cs ! 0);
x2 ← p2 (cs ! 1);
(if l = 3 then do {
x3 ← p3 (cs ! 2);
return (f x1 x2 (Some x3))
} else return (f x1 x2 None))
} else Xmlt.fail tag (XML name atts cs)))" |
"xml2to3elements tag p1 p2 p3 f xml = Xmlt.fail tag xml"
lemma xml2to3elements_mono [partial_function_mono]:
assumes p1: "⋀y. mono_sum_bot (p1 y)"
"⋀y. mono_sum_bot (p2 y)"
"⋀y. mono_sum_bot (p3 y)"
shows "mono_sum_bot (λg. xml2to3elements t (λy. p1 y g) (λy. p2 y g) (λy. p3 y g) f x)"
by (cases x, auto intro!: partial_function_mono p1)
fun
xml3to4elements ::
"string ⇒ 'a xmlt ⇒ 'b xmlt ⇒ 'c xmlt ⇒ 'd xmlt ⇒ ('a ⇒ 'b ⇒ 'c option ⇒ 'd ⇒ 'e) ⇒
'e xmlt"
where
"xml3to4elements tag p1 p2 p3 p4 f (XML name atts cs) = (
let l = length cs in
(if name = tag ∧ atts = [] ∧ l ≥ 3 ∧ l ≤ 4 then do {
x1 ← p1 (cs ! 0);
x2 ← p2 (cs ! 1);
(if l = 4 then do {
x3 ← p3 (cs ! 2);
x4 ← p4 (cs ! 3);
return (f x1 x2 (Some x3) x4)
} else do {
x4 ← p4 (cs ! 2);
return (f x1 x2 None x4)
} )
} else Xmlt.fail tag (XML name atts cs)))" |
"xml3to4elements tag p1 p2 p3 p4 f xml = Xmlt.fail tag xml"
lemma xml3to4elements_mono [partial_function_mono]:
assumes p1: "⋀y. mono_sum_bot (p1 y)"
"⋀y. mono_sum_bot (p2 y)"
"⋀y. mono_sum_bot (p3 y)"
"⋀y. mono_sum_bot (p4 y)"
shows "mono_sum_bot (λg. xml3to4elements t (λy. p1 y g) (λy. p2 y g) (λy. p3 y g) (λy. p4 y g) f x)"
by (cases x, auto intro!: partial_function_mono p1)
fun many :: "tag ⇒ 'a xmlt ⇒ ('a list ⇒ 'b) ⇒ 'b xmlt"
where
"many tag p f (XML name atts cs) =
(if name = tag ∧ atts = [] then (Xmlt.map p cs ⤜ (return ∘ f))
else Xmlt.fail tag (XML name atts cs))" |
"many tag p f xml = Xmlt.fail tag xml"
hide_const (open) many
lemma many_mono [partial_function_mono]:
fixes p1 :: "xml ⇒ ('b ⇒ (string +⇩⊥ 'c)) ⇒ string +⇩⊥ 'd"
assumes "⋀y. y ∈ set (Xml.children x) ⟹ mono_sum_bot (p1 y)"
shows "mono_sum_bot (λg. Xmlt.many t (λy. p1 y g) f x)"
using assms by (cases x) (auto intro!: partial_function_mono)
fun many1_gen :: "tag ⇒ 'a xmlt ⇒ ('a ⇒ 'b xmlt) ⇒ ('a ⇒ 'b list ⇒ 'c) ⇒ 'c xmlt"
where
"many1_gen tag p1 p2 f (XML name atts cs) =
(if name = tag ∧ atts = [] ∧ cs ≠ [] then
(case cs of h # t ⇒ do {
x ← p1 h;
xs ← Xmlt.map (p2 x) t;
return (f x xs)
})
else Xmlt.fail tag (XML name atts cs))" |
"many1_gen tag p1 p2 f xml = Xmlt.fail tag xml"
definition many1 :: "string ⇒ 'a xmlt ⇒ 'b xmlt ⇒ ('a ⇒ 'b list ⇒ 'c) ⇒ 'c xmlt"
where
"many1 tag p1 p2 = Xmlt.many1_gen tag p1 (λ_. p2)"
hide_const (open) many1
lemma many1_mono [partial_function_mono]:
fixes p1 :: "xml ⇒ ('b ⇒ (string +⇩⊥ 'c)) ⇒ string +⇩⊥ 'd"
assumes "⋀y. mono_sum_bot (p1 y)"
and "⋀y. y ∈ set (tl (Xml.children x)) ⟹ mono_sum_bot (p2 y)"
shows "mono_sum_bot (λg. Xmlt.many1 t (λy. p1 y g) (λy. p2 y g) f x)"
unfolding Xmlt.many1_def using assms
by (cases x, cases "Xml.children x") (auto intro!: partial_function_mono)
fun length_ge_2 :: "'a list ⇒ bool"
where
"length_ge_2 (_ # _ # _) = True" |
"length_ge_2 _ = False"
fun many2 :: "tag ⇒ 'a xmlt ⇒ 'b xmlt ⇒ 'c xmlt ⇒ ('a ⇒ 'b ⇒ 'c list ⇒ 'd) ⇒ 'd xmlt"
where
"many2 tag p1 p2 p3 f (XML name atts cs) =
(if name = tag ∧ atts = [] ∧ length_ge_2 cs then
(case cs of cs0 # cs1 # t ⇒ do {
x ← p1 cs0;
y ← p2 cs1;
xs ← Xmlt.map p3 t;
return (f x y xs)
})
else Xmlt.fail tag (XML name atts cs))" |
"many2 tag p1 p2 p3 f xml = Xmlt.fail tag xml"
lemma many2_mono [partial_function_mono]:
fixes p1 :: "xml ⇒ ('b ⇒ (string +⇩⊥ 'c)) ⇒ string +⇩⊥ 'd"
assumes "⋀y. mono_sum_bot (p1 y)"
and "⋀y. mono_sum_bot (p2 y)"
and "⋀y. mono_sum_bot (p3 y)"
shows "mono_sum_bot (λg. Xmlt.many2 t (λy. p1 y g) (λy. p2 y g) (λy. p3 y g) f x)"
using assms
by (cases x, cases "Xml.children x", (auto intro!: partial_function_mono)[1], cases "tl (Xml.children x)", auto intro!: partial_function_mono)
fun
xml1or2many_elements ::
"string ⇒ 'a xmlt ⇒ 'b xmlt ⇒ 'c xmlt ⇒ ('a ⇒ 'b option ⇒ 'c list ⇒ 'd) ⇒ 'd xmlt"
where
"xml1or2many_elements tag p1 p2 p3 f (XML name atts cs) =
(if name = tag ∧ atts = [] ∧ cs ≠ [] then
(case cs of
cs0 # tt ⇒
do {
x ← p1 cs0;
(case tt of
cs1 # t ⇒
do {
try do {
y ← p2 cs1;
xs ← Xmlt.map p3 t;
return (f x (Some y) xs)
} catch (λ _. do {
xs ← Xmlt.map p3 tt;
return (f x None xs)
})
}
| [] ⇒ return (f x None []))})
else Xmlt.fail tag (XML name atts cs))" |
"xml1or2many_elements tag p1 p2 p3 f xml = Xmlt.fail tag xml"
fun
xml1many2elements_gen ::
"string ⇒ 'a xmlt ⇒ ('a ⇒ 'b xmlt) ⇒ 'c xmlt ⇒ 'd xmlt ⇒
('a ⇒ 'b list ⇒ 'c ⇒ 'd ⇒ 'e) ⇒ 'e xmlt"
where
"xml1many2elements_gen tag p1 p2 p3 p4 f (XML name atts cs) = (
let ds = List.rev cs; l = length cs in
(if name = tag ∧ atts = [] ∧ l ≥ 3 then do {
x ← p1 (cs ! 0);
xs ← Xmlt.map (p2 x) (tl (take (l - 2) cs));
y ← p3 (ds ! 1);
z ← p4 (ds ! 0);
return (f x xs y z)
} else Xmlt.fail tag (XML name atts cs)))" |
"xml1many2elements_gen tag p1 p2 p3 p4 f xml = Xmlt.fail tag xml"
lemma xml1many2elements_gen_mono [partial_function_mono]:
fixes p1 :: "xml ⇒ ('b ⇒ (string +⇩⊥ 'c)) ⇒ string +⇩⊥ 'd"
assumes p1: "⋀y. mono_sum_bot (p1 y)"
"⋀y. mono_sum_bot (p3 y)"
"⋀y. mono_sum_bot (p4 y)"
shows "mono_sum_bot (λg. xml1many2elements_gen t (λy. p1 y g) p2 (λy. p3 y g) (λy. p4 y g) f x)"
by (cases x, auto intro!: partial_function_mono p1)
fun
xml1many2elements ::
"string ⇒ 'a xmlt ⇒ 'b xmlt ⇒ 'c xmlt ⇒ 'd xmlt ⇒ ('a ⇒ 'b list ⇒ 'c ⇒ 'd ⇒ 'e) ⇒
'e xmlt"
where
"xml1many2elements tag p1 p2 = xml1many2elements_gen tag p1 (λ_. p2)"
fun
xml_many2elements ::
"string ⇒ 'a xmlt ⇒ 'b xmlt ⇒ 'c xmlt ⇒ ('a list ⇒ 'b ⇒ 'c ⇒ 'd) ⇒ 'd xmlt"
where
"xml_many2elements tag p1 p2 p3 f (XML name atts cs) = (
let ds = List.rev cs in
(if name = tag ∧ atts = [] ∧ length_ge_2 cs then do {
xs ← Xmlt.map p1 (List.rev (tl (tl ds)));
y ← p2 (ds ! 1);
z ← p3 (ds ! 0);
return (f xs y z)
} else Xmlt.fail tag (XML name atts cs)))" |
"xml_many2elements tag p1 p2 p3 f xml = Xmlt.fail tag xml"
definition options :: "(string × 'a xmlt) list ⇒ 'a xmlt"
where
"options ps x =
(case map_of ps (Xml.tag x) of
None ⇒ error (concat
[''expected one of: '', concat (map (λp. fst p @ '' '') ps), ''⏎'', ''but found'', ''⏎'', show x])
| Some p ⇒ p x)"
hide_const (open) options
lemma options_mono_gen [partial_function_mono]:
assumes p: "⋀ k p. (k, p) ∈ set ps ⟹ mono_sum_bot (p x)"
shows "mono_sum_bot (λ g. Xmlt.options (map (λ (k, p). (k, (λ y. p y g))) ps) x)"
proof -
{
fix g
have "(map (λp. fst p @ '' '') (map (λ(k, p). (k, λy. p y g)) ps)) =
map (λp. fst p @ '' '') ps"
by (induct ps) (auto)
} note id = this
{
fix z
have "mono_sum_bot
(λg. case map_of (map (λ(k, p). (k, λy. p y g)) ps) (Xml.tag x) of
None ⇒ z
| Some p ⇒ p x)"
using p
proof (induct ps)
case Nil
show ?case by (auto intro: partial_function_mono)
next
case (Cons kp ps)
obtain k p where kp: "kp = (k,p)" by force
note Cons = Cons[unfolded kp]
from Cons(2) have monop: "mono_sum_bot (p x)" and mono: "⋀ k p. (k,p) ∈ set ps ⟹ mono_sum_bot (p x)" by auto
show ?case
proof (cases "Xml.tag x = k")
case True
thus ?thesis unfolding kp using monop by auto
next
case False
thus ?thesis using Cons(1) mono unfolding kp by auto
qed
qed
} note main = this
show ?thesis unfolding Xmlt.options_def
unfolding id
by (rule main)
qed
local_setup ‹fn lthy =>
let
val N = 30
val thy = Proof_Context.theory_of lthy
val options = @{term "Xmlt.options :: (string × (xml ⇒ (string +⇩⊥ 'd))) list ⇒ xml ⇒ string +⇩⊥ 'd"}
val mono_sum_bot = @{term "mono_sum_bot :: (('a ⇒ ('b +⇩⊥ 'c)) ⇒ string +⇩⊥ 'd) ⇒ bool"}
val ktyp = @{typ string}
val x = @{term "x :: xml"}
val y = @{term "y :: xml"}
val g = @{term "g :: 'a ⇒ 'b +⇩⊥ 'c"}
val ptyp = @{typ "xml ⇒ ('a ⇒ ('b +⇩⊥ 'c)) ⇒ string +⇩⊥ 'd"}
fun k i = Free ("k" ^ string_of_int i,ktyp)
fun p i = Free ("p" ^ string_of_int i,ptyp)
fun prem i = HOLogic.mk_Trueprop (mono_sum_bot $ (p i $ x))
fun prems n = 1 upto n |> map prem
fun pair i = HOLogic.mk_prod (k i, lambda y (p i $ y $ g))
fun pair2 i = HOLogic.mk_prod (k i, p i)
fun list n = 1 upto n |> map pair |> HOLogic.mk_list @{typ "(string × (xml ⇒ string +⇩⊥ 'd))"}
fun list2 n = 1 upto n |> map pair2 |> HOLogic.mk_list (HOLogic.mk_prodT (ktyp,ptyp))
fun concl n = HOLogic.mk_Trueprop (mono_sum_bot $ lambda g (options $ (list n) $ x))
fun xs n = x :: (1 upto n |> map (fn i => [p i, k i]) |> List.concat)
|> map (fst o dest_Free)
fun tac n pc =
let
val {prems = prems, context = ctxt} = pc
val mono_thm = Thm.instantiate'
(map (SOME o Thm.ctyp_of ctxt) [@{typ 'a},@{typ 'b},@{typ 'c},@{typ 'd}])
(map (SOME o Thm.cterm_of ctxt) [list2 n,x]) @{thm Xmlt.options_mono_gen}
in
Method.insert_tac ctxt (mono_thm :: prems) 1 THEN force_tac ctxt 1
end
fun thm n = Goal.prove lthy (xs n) (prems n) (concl n) (tac n)
val thms = map thm (0 upto N)
in Local_Theory.note ((@{binding "options_mono_thms"}, []), thms) lthy |> snd end
›
declare Xmlt.options_mono_thms [partial_function_mono]
fun choice :: "string ⇒ 'a xmlt list ⇒ 'a xmlt"
where
"choice e [] x = error (concat [''error in parsing choice for '', e, ''⏎'', show x])" |
"choice e (p # ps) x = (try p x catch (λ_. choice e ps x))"
hide_const (open) choice
lemma choice_mono_2 [partial_function_mono]:
assumes p: "mono_sum_bot (p1 x)"
"mono_sum_bot (p2 x)"
shows "mono_sum_bot (λ g. Xmlt.choice e [(λ y. p1 y g), (λ y. p2 y g)] x)"
using p by (auto intro!: partial_function_mono)
lemma choice_mono_3 [partial_function_mono]:
assumes p: "mono_sum_bot (p1 x)"
"mono_sum_bot (p2 x)"
"mono_sum_bot (p3 x)"
shows "mono_sum_bot (λ g. Xmlt.choice e [(λ y. p1 y g), (λ y. p2 y g), (λ y. p3 y g)] x)"
using p by (auto intro!: partial_function_mono)
fun change :: "'a xmlt ⇒ ('a ⇒ 'b) ⇒ 'b xmlt"
where
"change p f x = p x ⤜ return ∘ f"
hide_const (open) change
lemma change_mono [partial_function_mono]:
assumes p: "⋀y. mono_sum_bot (p1 y)"
shows "mono_sum_bot (λg. Xmlt.change (λy. p1 y g) f x)"
by (cases x, insert p, auto intro!: partial_function_mono)
fun int_of_digit :: "char ⇒ string +⇩⊥ int"
where
"int_of_digit x =
(if x = CHR ''0'' then return 0
else if x = CHR ''1'' then return 1
else if x = CHR ''2'' then return 2
else if x = CHR ''3'' then return 3
else if x = CHR ''4'' then return 4
else if x = CHR ''5'' then return 5
else if x = CHR ''6'' then return 6
else if x = CHR ''7'' then return 7
else if x = CHR ''8'' then return 8
else if x = CHR ''9'' then return 9
else error (x # '' is not a digit''))"
fun int_of_string_aux :: "int ⇒ string ⇒ string +⇩⊥ int"
where
"int_of_string_aux n [] = return n" |
"int_of_string_aux n (d # s) = (int_of_digit d ⤜ (λm. int_of_string_aux (10 * n + m) s))"
definition int_of_string :: "string ⇒ string +⇩⊥ int"
where
"int_of_string s =
(if s = [] then error ''cannot convert empty string into number''
else if take 1 s = ''-'' then int_of_string_aux 0 (tl s) ⤜ (λ i. return (0 - i))
else int_of_string_aux 0 s)"
hide_const int_of_string_aux
fun int :: "tag ⇒ int xmlt"
where
"int tag x = (Xmlt.text tag x ⤜ int_of_string)"
hide_const (open) int
fun nat :: "tag ⇒ nat xmlt"
where
"nat tag x = do {
txt ← Xmlt.text tag x;
i ← int_of_string txt;
return (Int.nat i)
}"
hide_const (open) nat
definition rat :: "rat xmlt"
where
"rat = Xmlt.options [
(''integer'', Xmlt.change (Xmlt.int ''integer'') of_int),
(''rational'',
Xmlt.pair ''rational'' (Xmlt.int ''numerator'') (Xmlt.int ''denominator'')
(λ x y. of_int x / of_int y))]"
hide_const (open) rat
end