theory Xmlt2
imports
"HOL-Library.Extended_Nat"
XML.Xml
Certification_Monads.Strict_Sum
Show.Show_Instances
Shows_Literal
begin
text ‹String literals in parser, for nicer generated code›
type_synonym ltag = String.literal
datatype 'a xml_error = TagMismatch "ltag list" | Fatal 'a
text ‹
@{term "TagMismatch tags"} represents tag mismatch, expecting one of @{term tags} but
something else is encountered.
›
lemma xml_error_mono [partial_function_mono]:
assumes p1: "⋀tags. mono_option (p1 tags)"
and p2: "⋀x. mono_option (p2 x)"
and f: "mono_option f"
shows "mono_option (λg. case s of TagMismatch tags ⇒ p1 tags g | Fatal x ⇒ p2 x g)"
using assms by (cases s, auto intro!:partial_function_mono)
text ‹A state is a tuple of
the XML or list of XMLs to be parsed,
the attributes,
a flag indicating if mismatch is allowed,
a list of tags that have been mismatched,
the current position.
›
type_synonym 'a xmlt2 = "xml × (string × string) list × bool × ltag list × ltag list ⇒ String.literal xml_error +⇩⊥ 'a"
type_synonym 'a xmlst = "xml list × (string × string) list × bool × ltag list × ltag list ⇒ String.literal xml_error +⇩⊥ 'a"
lemma xml_state_cases:
assumes "⋀p nam atts xmls. x = (XML nam atts xmls, p) ⟹ thesis"
and "⋀p txt. x = (XML_text txt, p) ⟹ thesis"
shows thesis
using assms by (cases x; cases "fst x", auto)
lemma xmls_state_cases:
assumes "⋀p. x = ([],p) ⟹ thesis"
and "⋀xml xmls p. x = (xml # xmls, p) ⟹ thesis"
shows thesis
using assms by (cases x; cases "fst x", auto)
lemma xmls_state_induct:
fixes x :: "xml list × _"
assumes "⋀a b c d. P ([],a,b,c,d)"
and "⋀xml xmls a b c d. (⋀a b c d. P (xmls,a,b,c,d)) ⟹ P (xml # xmls, a, b, c, d)"
shows "P x"
proof (induct x)
case (fields xmls a b c d)
with assms show ?case by (induct xmls arbitrary:a b c d, auto)
qed
definition xml_error
where "xml_error str x ≡ case x of (xmls,_,_,_,pos) ⇒
let next = case xmls of
XML tag _ _ # _ ⇒ STR ''<'' + String.implode tag + STR ''>''
| XML_text str # _ ⇒ STR ''text element \"'' + String.implode str + STR ''\"''
| [] ⇒ STR ''tag close''
in
Left (Fatal (STR ''parse error on '' + next + STR '' at '' + default_showsl_list showsl_lit pos (STR '''') + STR '':⏎'' + str))"
definition xml_return :: "'a ⇒ 'a xmlst"
where "xml_return v x ≡ case x
of ([],_) ⇒ Right v
| _ ⇒ xml_error (STR ''expecting tag close'') x"
definition "mismatch tag x ≡ case x of
(xmls,atts,flag,cands,_) ⇒
if flag then Left (TagMismatch (tag#cands))
else xml_error (STR ''expecting '' + default_showsl_list showsl_lit (tag#cands) (STR '''')) x"
abbreviation xml_any :: "xml xmlt2"
where
"xml_any x ≡ Right (fst x)"
text ‹Conditional parsing depending on tag match.›
definition bind2 :: "'a +⇩⊥'b ⇒ ('a ⇒ 'c +⇩⊥ 'd) ⇒ ('b ⇒ 'c +⇩⊥ 'd) ⇒ 'c +⇩⊥ 'd" where
"bind2 x f g = (case x of
Bottom ⇒ Bottom
| Left a ⇒ f a
| Right b ⇒ g b)"
lemma bind2_cong[fundef_cong]: "x = y ⟹ (⋀ a. y = Left a ⟹ f1 a = f2 a) ⟹
(⋀ b. y = Right b ⟹ g1 b = g2 b) ⟹ bind2 x f1 g1 = bind2 y f2 g2"
by (cases x, auto simp: bind2_def)
lemma bind2_code[code]:
"bind2 (sumbot a) f g = (case a of Inl a ⇒ f a | Inr b ⇒ g b)"
by (cases a) (auto simp: bind2_def)
definition xml_or (infixr "XMLor" 51)
where
"xml_or p1 p2 x ≡ case x of (x1,atts,flag,cands,rest) ⇒ (
bind2 (p1 (x1,atts,True,cands,rest))
(λ err1. case err1
of TagMismatch cands1 ⇒ p2 (x1,atts,flag,cands1,rest)
| err1 ⇒ Left err1)
Right)"
definition xml_do :: "ltag ⇒ 'a xmlst ⇒ 'a xmlt2" where
"xml_do tag p x ≡
case x of (XML nam atts xmls, _, flag, cands, pos) ⇒
if nam = String.explode tag then p (xmls,atts,False,[],tag#pos) ― ‹inner tag mismatch is not allowed›
else mismatch tag ([fst x], snd x)
| _ ⇒ mismatch tag ([fst x], snd x)"
text ‹parses the first child›
definition xml_take :: "'a xmlt2 ⇒ ('a ⇒ 'b xmlst) ⇒ 'b xmlst"
where "xml_take p1 p2 x ≡
case x of ([],rest) ⇒ (
― ‹Only for accumulating expected tags.›
bind2 (p1 (XML [] [] [], rest)) Left (λ a. Left (Fatal (STR ''unexpected'')))
)
| (x#xs,atts,flag,cands,rest) ⇒ (
bind2 (p1 (x,atts,flag,cands,rest)) Left
(λ a. p2 a (xs,atts,False,[],rest))) ― ‹If one child is parsed, then later mismatch is not allowed›"
definition xml_take_text :: "(string ⇒ 'a xmlst) ⇒ 'a xmlst" where
"xml_take_text p xs ≡
case xs of (XML_text text # xmls, s) ⇒ p text (xmls,s)
| _ ⇒ xml_error (STR ''expecting a text'') xs"
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) = (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]) =
do { l ← nat_of_string_aux n s; m ← nat_of_digit c; Some (10 * l + m) }"
by (induct s arbitrary:n, auto)
private lemma nat_of_string_aux_digit:
assumes m10: "m < 10"
shows "nat_of_string_aux n (s @ string_of_digit m) =
do { l ← nat_of_string_aux n s; Some (10 * l + m) }"
proof-
{ note numeral_eq_Suc[simp]
note m10[simplified]
}
from this[unfolded less_Suc_eq, folded numeral_1_eq_Suc_0, unfolded Suc_numeral, simplified]
show ?thesis by (auto simp add: nat_of_digit_def nat_of_string_aux_snoc)
qed
declare string_of_digit.simps[simp del]
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 "[]"]
apply (auto simp add:shows_string_def nat_of_string_def string_of_digit.simps)
done
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 (auto simp: shows_prec_nat_def[symmetric] shows_string_def)
apply (subst shows_move)
using nat_of_string_aux_digit[OF pos_mod_bound,simplified]
using m IH by (auto simp: nat_of_string_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.simps)
done
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
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 do { n ← nat_of_string (tl s); Inr (- int n) }
else do { n ← nat_of_string s; Inr (int n) }"
definition xml_take_int :: "(int ⇒ 'a xmlst) ⇒ 'a xmlst" where
"xml_take_int p xs ≡
case xs of (XML_text text # xmls, s) ⇒
(case int_of_string text of Inl x ⇒ xml_error x xs | Inr n ⇒ p n (xmls,s))
| _ ⇒ xml_error (STR ''expecting an integer'') xs"
definition xml_take_nat :: "(nat ⇒ 'a xmlst) ⇒ 'a xmlst" where
"xml_take_nat p xs ≡
case xs of (XML_text text # xmls, s) ⇒
(case nat_of_string text of Inl x ⇒ xml_error x xs | Inr n ⇒ p n (xmls,s))
| _ ⇒ xml_error (STR ''expecting a number'') xs"
definition xml_leaf where
"xml_leaf tag ret ≡ xml_do tag (xml_return ret)"
definition xml_text :: "ltag ⇒ string xmlt2" where
"xml_text tag ≡ xml_do tag (xml_take_text xml_return)"
definition xml_int :: "ltag ⇒ int xmlt2" where
"xml_int tag ≡ xml_do tag (xml_take_int xml_return)"
definition xml_nat :: "ltag ⇒ nat xmlt2" where
"xml_nat tag ≡ xml_do tag (xml_take_nat xml_return)"
definition bool_of_string :: "string ⇒ String.literal + bool"
where
"bool_of_string s ≡
if s = ''true'' then Inr True
else if s = ''false'' then Inr False
else Inl (STR ''cannot convert \"'' + String.implode s + STR ''\" into Boolean'')"
definition xml_bool :: "ltag ⇒ bool xmlt2"
where
"xml_bool tag x ≡
bind2 (xml_text tag x) Left
(λ str. ( case bool_of_string str of Inr b ⇒ Right b
| Inl err ⇒ xml_error err ([fst x], snd x)
))"
definition xml_change :: "'a xmlt2 ⇒ ('a ⇒ 'b xmlst) ⇒ 'b xmlt2" where
"xml_change p f x ≡
bind2 (p x) Left (λ a. case x of (_,rest) ⇒ f a ([],rest))"
text ‹
Parses the first child, if tag matches.
›
definition xml_take_optional :: "'a xmlt2 ⇒ ('a option ⇒ 'b xmlst) ⇒ 'b xmlst"
where "xml_take_optional p1 p2 xs ≡
case xs of ([],_) ⇒ p2 None xs
| (xml # xmls, atts, allow, cands, rest) ⇒
bind2 (p1 (xml, atts, True, cands, rest))
(λ e. case e of
TagMismatch cands1 ⇒ p2 None (xml#xmls, atts, allow, cands1, rest) ― ‹TagMismatch is allowed›
| _ ⇒ Left e)
(λ a. p2 (Some a) (xmls, atts, False, [], rest))"
definition xml_take_default :: "'a ⇒ 'a xmlt2 ⇒ ('a ⇒ 'b xmlst) ⇒ 'b xmlst"
where "xml_take_default a p1 p2 xs ≡
case xs of ([],_) ⇒ p2 a xs
| (xml # xmls, atts, allow, cands, rest) ⇒ (
bind2 (p1 (xml, atts, True, cands, rest))
(λ e. case e of
TagMismatch cands1 ⇒ p2 a (xml#xmls, atts, allow, cands1, rest) ― ‹TagMismatch is allowed›
| _ ⇒ Left e)
(λa. p2 a (xmls, atts, False, [], rest)))"
text ‹Take first children, as many as tag matches.›
fun xml_take_many_sub :: "'a list ⇒ nat ⇒ enat ⇒ 'a xmlt2 ⇒ ('a list ⇒ 'b xmlst) ⇒ 'b xmlst" where
"xml_take_many_sub acc minOccurs maxOccurs p1 p2 ([], atts, allow, rest) = (
if minOccurs = 0 then p2 (rev acc) ([], atts, allow, rest)
else ― ‹only for nice error log›
bind2 (p1 (XML [] [] [], atts, False, rest)) Left (λ _. Left (Fatal (STR ''unexpected'')))
)"
| "xml_take_many_sub acc minOccurs maxOccurs p1 p2 (xml # xmls, atts, allow, cands, rest) = (
if maxOccurs = 0 then p2 (rev acc) (xml # xmls, atts, allow, cands, rest)
else
bind2 (p1 (xml, atts, minOccurs = 0, cands, rest))
(λ e. case e of
TagMismatch tags ⇒ p2 (rev acc) (xml # xmls, atts, allow, cands, rest)
| _ ⇒ Left e)
(λ a. xml_take_many_sub (a # acc) (minOccurs-1) (maxOccurs-1) p1 p2 (xmls, atts, False, [], rest))
)"
abbreviation xml_take_many where "xml_take_many ≡ xml_take_many_sub []"
fun pick_up where
"pick_up rest key [] = None"
| "pick_up rest key ((l,r)#s) = (if key = l then Some (r,rest@s) else pick_up ((l,r)#rest) key s)"
definition xml_take_attribute :: "ltag ⇒ (string ⇒ 'a xmlst) ⇒ 'a xmlst"
where "xml_take_attribute att p xs ≡
case xs of (xmls,atts,allow,cands,pos) ⇒ (
case pick_up [] (String.explode att) atts of
None ⇒ xml_error (STR ''attribute \"'' + att + STR ''\" not found'') xs
| Some(v,rest) ⇒ p v (xmls,rest,allow,cands,pos)
)"
definition xml_take_attribute_optional :: "ltag ⇒ (string option ⇒ 'a xmlst) ⇒ 'a xmlst"
where "xml_take_attribute_optional att p xs ≡
case xs of (xmls,atts,info) ⇒ (
case pick_up [] (String.explode att) atts of
None ⇒ p None xs
| Some(v,rest) ⇒ p (Some v) (xmls,rest,info)
)"
definition xml_take_attribute_default :: "string ⇒ ltag ⇒ (string ⇒ 'a xmlst) ⇒ 'a xmlst"
where "xml_take_attribute_default def att p xs ≡
case xs of (xmls,atts,info) ⇒ (
case pick_up [] (String.explode att) atts of
None ⇒ p def xs
| Some(v,rest) ⇒ p v (xmls,rest,info)
)"
nonterminal xml_binds and xml_bind
syntax
"_xml_block" :: "xml_binds ⇒ 'a" ("XMLdo {//(2 _)//}" [12] 1000)
"_xml_take" :: "pttrn ⇒ 'a ⇒ xml_bind" ("(2_ ←/ _)" 13)
"_xml_take_text" :: "pttrn ⇒ xml_bind" ("(2_ ←text)" 13)
"_xml_take_int" :: "pttrn ⇒ xml_bind" ("(2_ ←int)" 13)
"_xml_take_nat" :: "pttrn ⇒ xml_bind" ("(2_ ←nat)" 13)
"_xml_take_att" :: "pttrn ⇒ ltag ⇒ xml_bind" ("(2_ ←att/ _)" 13)
"_xml_take_att_optional" :: "pttrn ⇒ ltag ⇒ xml_bind" ("(2_ ←att?/ _)" 13)
"_xml_take_att_default" :: "pttrn ⇒ ltag ⇒ string ⇒ xml_bind" ("(2_ ←att[(_)]/ _)" 13)
"_xml_take_optional" :: "pttrn ⇒ 'a ⇒ xml_bind" ("(2_ ←?/ _)" 13)
"_xml_take_default" :: "pttrn ⇒ 'b ⇒ 'a ⇒ xml_bind" ("(2_ ←[(_)]/ _)" 13)
"_xml_take_all" :: "pttrn ⇒ 'a ⇒ xml_bind" ("(2_ ←*/ _)" 13)
"_xml_take_many" :: "pttrn ⇒ nat ⇒ enat ⇒ 'a ⇒ xml_bind" ("(2_ ←^{(_)..(_)}/ _)" 13)
"_xml_let" :: "pttrn ⇒ 'a ⇒ xml_bind" ("(2let _ =/ _)" [1000, 13] 13)
"_xml_final" :: "'a xmlst ⇒ xml_binds" ("_")
"_xml_cons" :: "xml_bind ⇒ xml_binds ⇒ xml_binds" ("_;//_" [13, 12] 12)
"_xml_do" :: "ltag ⇒ xml_binds ⇒ 'a" ("XMLdo (_) {//(2 _)//}" [1000,12] 1000)
syntax (ASCII)
"_xml_take" :: "pttrn ⇒ 'a ⇒ xml_bind" ("(2_ <-/ _)" 13)
translations
"_xml_block (_xml_cons (_xml_take p x) (_xml_final e))"
⇌ "_xml_block (_xml_final (CONST xml_take x (λp. e)))"
"_xml_block (_xml_cons (_xml_take_text p) (_xml_final e))"
⇌ "_xml_block (_xml_final (CONST xml_take_text (λp. e)))"
"_xml_block (_xml_cons (_xml_take_int p) (_xml_final e))"
⇌ "_xml_block (_xml_final (CONST xml_take_int (λp. e)))"
"_xml_block (_xml_cons (_xml_take_nat p) (_xml_final e))"
⇌ "_xml_block (_xml_final (CONST xml_take_nat (λp. e)))"
"_xml_block (_xml_cons (_xml_take_att p x) (_xml_final e))"
⇌ "_xml_block (_xml_final (CONST xml_take_attribute x (λp. e)))"
"_xml_block (_xml_cons (_xml_take_att_optional p x) (_xml_final e))"
⇌ "_xml_block (_xml_final (CONST xml_take_attribute_optional x (λp. e)))"
"_xml_block (_xml_cons (_xml_take_att_default p d x) (_xml_final e))"
⇌ "_xml_block (_xml_final (CONST xml_take_attribute_default d x (λp. e)))"
"_xml_block (_xml_cons (_xml_take_optional p x) (_xml_final e))"
⇌ "_xml_block (_xml_final (CONST xml_take_optional x (λp. e)))"
"_xml_block (_xml_cons (_xml_take_default p d x) (_xml_final e))"
⇌ "_xml_block (_xml_final (CONST xml_take_default d x (λp. e)))"
"_xml_block (_xml_cons (_xml_take_all p x) (_xml_final e))"
⇌ "_xml_block (_xml_final (CONST xml_take_many 0 ∞ x (λp. e)))"
"_xml_block (_xml_cons (_xml_take_many p minOccurs maxOccurs x) (_xml_final e))"
⇌ "_xml_block (_xml_final (CONST xml_take_many minOccurs maxOccurs x (λp. e)))"
"_xml_block (_xml_cons (_xml_let p t) bs)"
⇌ "let p = t in _xml_block bs"
"_xml_block (_xml_cons b (_xml_cons c cs))"
⇌ "_xml_block (_xml_cons b (_xml_final (_xml_block (_xml_cons c cs))))"
"_xml_cons (_xml_let p t) (_xml_final s)"
⇌ "_xml_final (let p = t in s)"
"_xml_block (_xml_final e)" ⇀ "e"
"_xml_do t e" ⇌ "CONST xml_do t (_xml_block e)"
fun xml_error_to_string where
"xml_error_to_string (Fatal e) = String.explode (STR ''Fatal: '' + e)"
| "xml_error_to_string (TagMismatch e) = String.explode (STR ''tag mismatch: '' + default_showsl_list showsl_lit e (STR ''''))"
definition string2xml :: "string ⇒ string + xml" where
"string2xml str ≡
case (do {
update_tokens remove_comments;
xml ← parse_node;
eoi;
Parser_Monad.return xml
}) str
of Inl err ⇒ Inl err | Inr (xml,_) ⇒ Inr xml"
definition parse_xml :: "'a xmlt2 ⇒ xml ⇒ string +⇩⊥ 'a"
where "parse_xml p xml ≡
bind2 (xml_take p xml_return ([xml],[],False,[],[]))
(Left o xml_error_to_string) Right"
subsection ‹Handling of special characters in text›
definition "special_map = map_of [
(''quot'', ''\"''), (''#34'', ''\"''), ― ‹double quotation mark›
(''amp'', ''&''), (''#38'', ''&''), ― ‹ampersand›
(''apos'', [CHR 0x27]), (''#39'', [CHR 0x27]), ― ‹single quotes›
(''lt'', ''<''), (''#60'', ''<''), ― ‹less-than sign›
(''gt'', ''>''), (''#62'', ''>'') ― ‹greater-than sign›
]"
fun extract_special
where
"extract_special acc [] = None"
| "extract_special acc (x # xs) =
(if x = CHR '';'' then map_option (λs. (s, xs)) (special_map (rev acc))
else extract_special (x#acc) xs)"
lemma extract_special_length [termination_simp]:
assumes "extract_special acc xs = Some (y, ys)"
shows "length ys < length xs"
using assms by (induct acc xs rule: extract_special.induct) (auto split: if_splits)
fun normalize_special
where
"normalize_special [] = []"
| "normalize_special (x # xs) =
(if x = CHR ''&'' then
(case extract_special [] xs of
None ⇒ ''&'' @ normalize_special xs
| Some (spec, ys) ⇒ spec @ normalize_special ys)
else x # normalize_special xs)"
fun map_xml_text :: "(string ⇒ string) ⇒ xml ⇒ xml"
where
"map_xml_text f (XML t as cs) = XML t as (map (map_xml_text f) cs)"
| "map_xml_text f (XML_text txt) = XML_text (f txt)"
definition parse_xmlfile :: "'a xmlt2 ⇒ string ⇒ string +⇩⊥ 'a"
where
"parse_xmlfile p str ≡ case Xml.doc_of_string str of
Inl err ⇒ Left err
| Inr (XMLDOC header xml) ⇒ parse_xml p (map_xml_text normalize_special xml)"
definition parse_xml_string :: "'a xmlt2 ⇒ string ⇒ string +⇩⊥ 'a"
where "parse_xml_string p str ≡ case string2xml str of
Inl err ⇒ Left err
| Inr xml ⇒ parse_xml p xml"
subsection ‹For Terminating Parsers›
primrec size_xml
where "size_xml (XML_text str) = size str"
| "size_xml (XML tag atts xmls) = 1 + size tag + (∑xml ← xmls. size_xml xml)"
abbreviation "size_xml_state ≡ size_xml ∘ fst"
abbreviation "size_xmls_state x ≡ (∑xml ← fst x. size_xml xml)"
lemma size_xml_nth [dest]: "i < length xmls ⟹ size_xml (xmls!i) ≤ sum_list (map size_xml xmls)"
using elem_le_sum_list[of _ "map Xmlt2.size_xml _", unfolded length_map] by auto
lemma xml_or_cong[fundef_cong]:
assumes "⋀info. p (fst x, info) = p' (fst x, info)"
and "⋀info. q (fst x, info) = q' (fst x, info)"
and "x = x'"
shows "(p XMLor q) x = (p' XMLor q') x'"
using assms
by (cases x, auto simp: xml_or_def intro!: Option.bind_cong split:sum.split xml_error.split)
lemma xml_do_cong[fundef_cong]:
fixes p :: "'a xmlst"
assumes "⋀tag' atts xmls info. fst x = XML tag' atts xmls ⟹ String.explode tag = tag' ⟹ p (xmls,atts,info) = p' (xmls,atts,info)"
and "x = x'"
shows "xml_do tag p x = xml_do tag p' x'"
using assms by (cases x, auto simp: xml_do_def split: xml.split)
lemma xml_take_cong[fundef_cong]:
fixes p :: "'a xmlt2" and q :: "'a ⇒ 'b xmlst"
assumes "⋀a as info. fst x = a#as ⟹ p (a, info) = p' (a, info)"
and "⋀a as ret info info'. x' = (a#as,info) ⟹ q ret (as, info') = q' ret (as, info')"
and "⋀info. p (XML [] [] [], info) = p' (XML [] [] [], info)"
and "x = x'"
shows "xml_take p q x = xml_take p' q' x'"
using assms by (cases x, auto simp: xml_take_def intro!: Option.bind_cong split: list.split sum.split)
lemma xml_take_many_cong[fundef_cong]:
fixes p :: "'a xmlt2" and q :: "'a list ⇒ 'b xmlst"
assumes p: "⋀n info. n < length (fst x) ⟹ p (fst x' ! n, info) = p' (fst x' ! n, info)"
and err: "⋀info. p (XML [] [] [], info) = p' (XML [] [] [], info)"
and q: "⋀ret n info. q ret (drop n (fst x'), info) = q' ret (drop n (fst x'), info)"
and xx': "x = x'"
shows "xml_take_many_sub ret minOccurs maxOccurs p q x = xml_take_many_sub ret minOccurs maxOccurs p' q' x'"
proof-
obtain as b where x: "x = (as,b)" by (cases x, auto)
show ?thesis
proof (insert p q, fold xx', unfold x, induct as arbitrary: b minOccurs maxOccurs ret)
case Nil
with err show ?case by (cases b, auto intro!: Option.bind_cong)
next
case (Cons a as)
from Cons(2,3)[where n=0] Cons(2,3)[where n="Suc n" for n]
show ?case by (cases b, auto intro!: bind2_cong Cons(1) split: sum.split xml_error.split)
qed
qed
lemma xml_take_optional_cong[fundef_cong]:
fixes p :: "'a xmlt2" and q :: "'a option ⇒ 'b xmlst"
assumes "⋀a as info. fst x = a # as ⟹ p (a, info) = p' (a, info)"
and "⋀a as ret info. fst x = a # as ⟹ q (Some ret) (as, info) = q' (Some ret) (as, info)"
and "⋀info. q None (fst x', info) = q' None (fst x', info)"
and xx': "x = x'"
shows "xml_take_optional p q x = xml_take_optional p' q' x'"
using assms by (cases x', auto simp: xml_take_optional_def split: list.split sum.split xml_error.split intro!: bind2_cong)
lemma xml_take_default_cong[fundef_cong]:
fixes p :: "'a xmlt2" and q :: "'a ⇒ 'b xmlst"
assumes "⋀a as info. fst x = a # as ⟹ p (a, info) = p' (a, info)"
and "⋀a as ret info. fst x = a # as ⟹ q ret (as, info) = q' ret (as, info)"
and "⋀info. q d (fst x', info) = q' d (fst x', info)"
and xx': "x = x'"
shows "xml_take_default d p q x = xml_take_default d p' q' x'"
using assms by (cases x', auto simp: xml_take_default_def split: list.split sum.split xml_error.split intro!: bind2_cong)
lemma xml_change_cong[fundef_cong]:
assumes "x = x'"
and "p x' = p' x'"
and "⋀ret y. p x = Right ret ⟹ q ret y = q' ret y"
shows "xml_change p q x = xml_change p' q' x'"
using assms by (cases x', auto simp: xml_change_def split: option.split sum.split intro!: bind2_cong)
text ‹Some fundef_cong lemmas, can't they be automatic?›
lemma if_cong_applied[fundef_cong]:
"b = c ⟹
(c ⟹ x z = u w) ⟹
(¬ c ⟹ y z = v w) ⟹
z = w ⟹
(if b then x else y) z =
(if c then u else v) w"
by auto
lemma option_case_cong[fundef_cong]:
"option = option' ⟹
(option' = None ⟹ f1 z = g1 w) ⟹
(⋀x2. option' = Some x2 ⟹ f2 x2 z = g2 x2 w) ⟹
z = w ⟹
(case option of None ⇒ f1 | Some x2 ⇒ f2 x2) z = (case option' of None ⇒ g1 | Some x2 ⇒ g2 x2) w"
by (cases option, auto)
lemma sum_case_cong[fundef_cong]:
"s = ss ⟹
(⋀x1. ss = Inl x1 ⟹ f1 x1 z = g1 x1 w) ⟹
(⋀x2. ss = Inr x2 ⟹ f2 x2 z = g2 x2 w) ⟹
z = w ⟹
(case s of Inl x1 ⇒ f1 x1 | Inr x2 ⇒ f2 x2) z = (case ss of Inl x1 ⇒ g1 x1 | Inr x2 ⇒ g2 x2) w"
by (cases s, auto)
lemma prod_case_cong[fundef_cong]: "p = pp ⟹
(⋀x1 x2. pp = (x1, x2) ⟹ f x1 x2 z = g x1 x2 w) ⟹
(case p of (x1, x2) ⇒ f x1 x2) z = (case pp of (x1, x2) ⇒ g x1 x2) w"
by (auto split: prod.split)
text ‹Mononicity rules of combinators for partial-function command.›
lemma bind2_mono [partial_function_mono]:
assumes p0: "mono_sum_bot p0"
assumes p1: "⋀y. mono_sum_bot (p1 y)"
assumes p2: "⋀y. mono_sum_bot (p2 y)"
shows "mono_sum_bot (λg. bind2 (p0 g) (λy. p1 y g) (λy. p2 y g))"
proof (rule monotoneI)
fix f g :: "'a ⇒ 'b +⇩⊥ 'c"
assume fg: "fun_ord sum_bot_ord f g"
with p0 have "sum_bot_ord (p0 f) (p0 g)" by (rule monotoneD[of _ _ _ f g])
then have "sum_bot_ord
(bind2 (p0 f) (λ y. p1 y f) (λ y. p2 y f))
(bind2 (p0 g) (λ y. p1 y f) (λ y. p2 y f))"
unfolding flat_ord_def bind2_def by auto
also from p1 have "⋀ y'. sum_bot_ord (p1 y' f) (p1 y' g)"
by (rule monotoneD) (rule fg)
then have "sum_bot_ord
(bind2 (p0 g) (λ y. p1 y f) (λ y. p2 y f))
(bind2 (p0 g) (λ y. p1 y g) (λ y. p2 y f))"
unfolding flat_ord_def by (cases "p0 g") (auto simp: bind2_def)
also (sum_bot.leq_trans)
from p2 have "⋀ y'. sum_bot_ord (p2 y' f) (p2 y' g)"
by (rule monotoneD) (rule fg)
then have "sum_bot_ord
(bind2 (p0 g) (λ y. p1 y g) (λ y. p2 y f))
(bind2 (p0 g) (λ y. p1 y g) (λ y. p2 y g))"
unfolding flat_ord_def by (cases "p0 g") (auto simp: bind2_def)
finally (sum_bot.leq_trans)
show "sum_bot_ord (bind2 (p0 f) (λy. p1 y f) (λy. p2 y f))
(bind2 (p0 g) (λya. p1 ya g) (λya. p2 ya g))" .
qed
lemma xml_or_mono [partial_function_mono]:
assumes p1: "⋀y. mono_sum_bot (p1 y)"
assumes p2: "⋀y. mono_sum_bot (p2 y)"
shows "mono_sum_bot (λg. xml_or (λy. p1 y g) (λy. p2 y g) x)"
using p1 unfolding xml_or_def
by (cases x, auto simp: xml_or_def intro!: partial_function_mono,
intro monotoneI, auto split: xml_error.splits simp: sum_bot.leq_refl dest: monotoneD[OF p2])
lemma xml_do_mono [partial_function_mono]:
assumes p1: "⋀y. mono_sum_bot (p1 y)"
shows "mono_sum_bot (λg. xml_do t (λy. p1 y g) x)"
by (cases x, cases "fst x") (auto simp: xml_do_def intro!: partial_function_mono p1)
lemma xml_take_mono [partial_function_mono]:
assumes p1: "⋀y. mono_sum_bot (p1 y)"
assumes p2: "⋀x z. mono_sum_bot (λ y. p2 z x y)"
shows "mono_sum_bot (λg. xml_take (λy. p1 y g) (λ x y. p2 x y g) x)"
proof (cases x)
case (fields a b c d e)
show ?thesis unfolding xml_take_def fields split
by (cases a, auto intro!: partial_function_mono p2 p1)
qed
lemma xml_take_default_mono [partial_function_mono]:
assumes p1: "⋀y. mono_sum_bot (p1 y)"
assumes p2: "⋀x z. mono_sum_bot (λ y. p2 z x y)"
shows "mono_sum_bot (λg. xml_take_default a (λy. p1 y g) (λ x y. p2 x y g) x)"
proof (cases x)
case (fields a b c d e)
show ?thesis unfolding xml_take_default_def fields split
by (cases a, auto intro!: partial_function_mono p2 p1, intro monotoneI,
auto split: xml_error.splits simp: sum_bot.leq_refl dest: monotoneD[OF p2])
qed
lemma xml_take_optional_mono [partial_function_mono]:
assumes p1: "⋀y. mono_sum_bot (p1 y)"
assumes p2: "⋀x z. mono_sum_bot (λ y. p2 z x y)"
shows "mono_sum_bot (λg. xml_take_optional (λy. p1 y g) (λ x y. p2 x y g) x)"
proof (cases x)
case (fields a b c d e)
show ?thesis unfolding xml_take_optional_def fields split
by (cases a, auto intro!: partial_function_mono p2 p1, intro monotoneI,
auto split: xml_error.splits simp: sum_bot.leq_refl dest: monotoneD[OF p2])
qed
lemma xml_change_mono [partial_function_mono]:
assumes p1: "⋀y. mono_sum_bot (p1 y)"
assumes p2: "⋀x z. mono_sum_bot (λ y. p2 z x y)"
shows "mono_sum_bot (λg. xml_change (λy. p1 y g) (λ x y. p2 x y g) x)"
unfolding xml_change_def by (intro partial_function_mono p1, cases x, auto intro: p2)
lemma xml_take_many_sub_mono [partial_function_mono]:
assumes p1: "⋀y. mono_sum_bot (p1 y)"
assumes p2: "⋀x z. mono_sum_bot (λ y. p2 z x y)"
shows "mono_sum_bot (λg. xml_take_many_sub a b c (λy. p1 y g) (λ x y. p2 x y g) x)"
proof -
obtain xs atts allow cands rest where x: "x = (xs, atts, allow, cands, rest)" by (cases x)
show ?thesis unfolding x
proof (induct xs arbitrary: a b c atts allow rest cands)
case Nil
show ?case by (auto intro!: partial_function_mono p1 p2)
next
case (Cons x xs)
show ?case unfolding xml_take_many_sub.simps
by (auto intro!: partial_function_mono p2 p1 Cons, intro monotoneI,
auto split: xml_error.splits simp: sum_bot.leq_refl dest: monotoneD[OF p2])
qed
qed
end