Theory Xmlt

(*
Author:  Akihisa Yamada <ayamada@trs.cm.is.nagoya-u.ac.jp> 
Author:  Christian Sternagel <c.sternagel@gmail.com> (
Author:  René Thiemann <rene.thiemann@uibk.ac.at> 
*)
theory Xmlt
  imports
    "HOL-Library.Extended_Nat"
    Show.Number_Parser
    Certification_Monads.Strict_Sum
    Show.Shows_Literal
    Xml
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 xmlt = "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 xmlt"
  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 xmlt" 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 xmlt ⇒ ('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"

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 xmlt" where
  "xml_text tag ≡ xml_do tag (xml_take_text xml_return)"

definition xml_int :: "ltag ⇒ int xmlt" where
  "xml_int tag ≡ xml_do tag (xml_take_int xml_return)"

definition xml_nat :: "ltag ⇒ nat xmlt" 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 xmlt"
  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 xmlt ⇒ ('a ⇒ 'b xmlst) ⇒ 'b xmlt" 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 xmlt ⇒ ('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 xmlt ⇒ ('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 xmlt ⇒ ('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 parse_xml :: "'a xmlt ⇒ xml ⇒ string +⇩⊥ 'a"
  where "parse_xml p xml ≡
    bind2 (xml_take p xml_return ([xml],[],False,[],[])) 
      (Left o xml_error_to_string) Right"

(*BEGIN: special chars*)
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)"
    (*END: special chars*)

definition parse_xml_string :: "'a xmlt ⇒ string ⇒ string +⇩⊥ 'a"
  where
    "parse_xml_string p str ≡ case doc_of_string str of
    Inl err ⇒ Left err
  | Inr (XMLDOC header xml) ⇒ parse_xml p (map_xml_text normalize_special xml)"


subsection ‹For Terminating Parsers›

(*TODO: replace the default size of xml *)
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 Xmlt.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 xmlt" 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 xmlt" 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 xmlt" 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 xmlt" 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)


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

partial_function (sum_bot) xml_foldl :: "('a ⇒ 'b xmlt) ⇒ ('a ⇒ 'b ⇒ 'a) ⇒ 'a ⇒ 'a xmlst" where
  [code]: "xml_foldl p f a xs = (case xs of ([],_) ⇒ Right a
     | _ ⇒ xml_take (p a) (λ b. xml_foldl p f (f a b)) xs)" 

end