Quelle  Xmlt.thy

(*
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 +_\<bottom> 'a"
type_synonym 'a xmlst = "xml list × (string × string) list × bool × ltag list × ltag list ==> String.literal xml_error +_\<bottom> '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 +_\<bottom>'b ==> ('a ==> 'c +_\<bottom> 'd) ==> ('b ==> 'c +_\<bottom> 'd) ==> 'c +_\<bottom> '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.
\<close>
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))"

  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)))"

  ‹Take first children, as many as tag matches.›

  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))
 )"

  xml_take_many where "xml_take_many ≡ xml_take_many_sub []"

  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)"

  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)
 )"

  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)
 )"

  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)
 )"

  xml_binds and xml_bind
 
 "_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)

  (ASCII)
 "_xml_take" :: "pttrn ==> 'a ==> xml_bind" (‹(2_ <-/ _)› 13)

 
 "_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)"

  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 ''''))"

  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 +_\<bottom> '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 +_\<bottom> '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