(*  Title:       Deriving class instances for datatypes
    Author:      Christian Sternagel and René Thiemann  <christian.sternagel|rene.thiemann@uibk.ac.at>
    Maintainer:  Christian Sternagel and René Thiemann 
    License:     LGPL
*)
section ‹Derive Manager›

theory Derive_Manager
imports Main
keywords "print_derives" :: diag and "derive" :: thy_decl
begin

text ‹
  The derive manager allows the user to register various derive-hooks, e.g., for orders,
  pretty-printers, hash-functions, etc. All registered hooks are accessible via the derive command.

  @{rail ‹
    @'derive' ('(' param ')')? sort (datatype+)
  ›}

  \begin{description}
  \item ‹❙d❙e❙r❙i❙v❙e (param) sort datatype› calls the hook for deriving ‹sort› (that
  may depend on the optional ‹param›) on ‹datatype› (if such a hook is registered).

  E.g., ‹❙d❙e❙r❙i❙v❙e compare_order list› will derive a comparator for datatype @{type list}
  which is also used to define a linear order on @{type list}s.
  \end{description}

  There is also the diagnostic command ‹❙p❙r❙i❙n❙t❙_❙d❙e❙r❙i❙v❙e❙s› that shows the list of currently
  registered hooks.
›

ML_file ‹derive_manager.ML›

end

signature DERIVE_MANAGER =
sig
  (* identifier, description, (fn dtyp_name => param => derive-method) *)
  val register_derive : string -> string -> (string -> string -> theory -> theory) -> theory -> theory
  (* identifier, description, (fn dtyp_name => param => derive-method) *)
  val derive : string -> string -> string -> theory -> theory
  val derive_cmd : string -> string -> string -> theory -> theory
  (* print all registered deriving-methods  *)
  val print_info : theory -> unit
end

structure Derive_Manager : DERIVE_MANAGER =
struct

structure Derive_Data = Theory_Data
  (
    type T =
      (string * (string -> string -> theory -> theory)) Symtab.table  (* descr * derive-fun *)

    val empty = Symtab.empty
    val extend = I
    val merge = Symtab.merge (K true)
  )

val derive_options =
  Derive_Data.get #> Symtab.dest #> map (fn (id, (descr, _)) => (id, descr))

(* FIXME: possibly use Pretty function for presentation. *)
fun print_info thy =
  let
    val _ = writeln "The following sorts can be derived"
    val _ = derive_options thy |> sort_by fst |> map (fn (id,descr) => writeln (id ^ ": " ^ descr))
  in () end

fun register_derive id descr f thy =
  if Symtab.defined (Derive_Data.get thy) id then
    error ("Identifier " ^ quote id ^ " already in use for " ^ quote "deriving")
  else
    Derive_Data.map (Symtab.update_new (id, (descr, f))) thy

fun gen_derive prep id dtname param thy =
  (case Symtab.lookup (Derive_Data.get thy) id of
    NONE => error ("No handler to derive sort " ^ quote id ^
      " is registered. Try " ^ quote "print_derives" ^ " to see available sorts.")
  | SOME (_, f) => f (prep thy dtname) param thy)

val derive = gen_derive (K I)

fun derive_cmd id param dtname = gen_derive
  (fn thy => fst o dest_Type o Syntax.parse_typ (Proof_Context.init_global thy)) id dtname param
  
(* TODO: also check for alternative of  *)
(* NB: Proof_Context.read_type_name_proper ctxt false could be an alternative. *)

val _ =
  Outer_Syntax.command @{command_keyword print_derives} "lists all registered sorts which can be derived"
    (Scan.succeed (Toplevel.theory (tap print_info)))

val _ =
  Outer_Syntax.command @{command_keyword derive} "derives some sort"
    (Parse.parname -- Parse.name -- Scan.repeat1 Parse.type_const >> (fn ((param, s), tycons) =>
      Toplevel.theory (fold (derive_cmd s param) tycons)))

end

section ‹Shared Utilities for all Generator›

text ‹In this theory we mainly provide some Isabelle/ML infrastructure
  that is used by several generators. It consists of a uniform interface
  to access all the theorems, terms, etc.\ from the BNF package, and 
  some auxiliary functions which provide recursors on datatypes, common tactics, etc.›

theory Generator_Aux
imports 
  Main
begin

ML_file ‹bnf_access.ML›
ML_file ‹generator_aux.ML›

lemma in_set_simps: 
  "x ∈ set (y # z # ys) = (x = y ∨ x ∈ set (z # ys))"
  "x ∈ set ([y]) = (x = y)"
  "x ∈ set [] = False" 
  "Ball (set []) P = True" 
  "Ball (set [x]) P = P x" 
  "Ball (set (x # y # zs)) P = (P x ∧ Ball (set (y # zs)) P)" 
  by auto
  
lemma conj_weak_cong: "a = b ⟹ c = d ⟹ (a ∧ c) = (b ∧ d)" by auto

lemma refl_True: "(x = x) = True" by simp

end

(*  Title:       Deriving class instances for datatypes
    Author:      Christian Sternagel and René Thiemann  <christian.sternagel|rene.thiemann@uibk.ac.at>
    Maintainer:  Christian Sternagel and René Thiemann 
    License:     LGPL
*)
signature BNF_ACCESS =
sig
(* thms *)
val induct_thms : Proof.context -> string list -> thm list
val case_thms : Proof.context -> string list -> thm list
val distinct_thms : Proof.context -> string list -> thm list list
val inject_thms : Proof.context -> string list -> thm list list
val set_simps : Proof.context -> string list -> thm list list
val case_simps : Proof.context -> string list -> thm list list
val map_simps : Proof.context -> string list -> thm list list
val map_comps : Proof.context -> string list -> thm list

(* terms *)
val map_terms : Proof.context -> string list -> term list
val set_terms : Proof.context -> string list -> term list list
val case_consts : Proof.context -> string list -> term list
val constr_terms : Proof.context -> string -> term list

(* types *)
val constr_argument_types : Proof.context -> string list -> typ list list list
val bnf_types : Proof.context -> string list -> typ list

end

structure Bnf_Access : BNF_ACCESS =
struct

fun constr_terms lthy = BNF_FP_Def_Sugar.fp_sugar_of lthy
  #> the #> #fp_ctr_sugar #> #ctr_sugar #> #ctrs

fun induct_thms lthy =
  map (hd o #co_inducts o the o #fp_co_induct_sugar o the o BNF_FP_Def_Sugar.fp_sugar_of lthy)

fun case_thms lthy =
  map (#exhaust o #ctr_sugar o #fp_ctr_sugar o the o BNF_FP_Def_Sugar.fp_sugar_of lthy)

fun set_simps lthy = 
  map (#set_thms o #fp_bnf_sugar o the o BNF_FP_Def_Sugar.fp_sugar_of lthy)

fun distinct_thms lthy =
  map (#distincts o #ctr_sugar o #fp_ctr_sugar o the o BNF_FP_Def_Sugar.fp_sugar_of lthy)

fun inject_thms lthy =
  map (#injects o #ctr_sugar o #fp_ctr_sugar o the o BNF_FP_Def_Sugar.fp_sugar_of lthy)

fun case_simps lthy = 
  map (#case_thms o #ctr_sugar o #fp_ctr_sugar o the o BNF_FP_Def_Sugar.fp_sugar_of lthy)

fun map_simps lthy = 
  map (#map_thms o #fp_bnf_sugar o the o BNF_FP_Def_Sugar.fp_sugar_of lthy)

fun map_comps lthy tycos = hd tycos
  |> (#bnfs o #fp_res o the o BNF_FP_Def_Sugar.fp_sugar_of lthy)
  |> map (BNF_Def.map_comp_of_bnf)

fun constr_argument_types lthy = 
  map (#ctrXs_Tss o #fp_ctr_sugar o the o BNF_FP_Def_Sugar.fp_sugar_of lthy)

fun bnf_types lthy = 
  map (#X o the o BNF_FP_Def_Sugar.fp_sugar_of lthy)

fun map_terms lthy tycos = hd tycos
  |> (#bnfs o #fp_res o the o BNF_FP_Def_Sugar.fp_sugar_of lthy)
  |> map (BNF_Def.map_of_bnf)

fun set_terms lthy tycos = hd tycos
  |> (#bnfs o #fp_res o the o BNF_FP_Def_Sugar.fp_sugar_of lthy)
  |> map (BNF_Def.sets_of_bnf)

fun case_consts lthy = map (BNF_FP_Def_Sugar.fp_sugar_of lthy
  #> the #> #fp_ctr_sugar #> #ctr_sugar #> #casex)

end

(*  Title:       Deriving class instances for datatypes
    Author:      Christian Sternagel and René Thiemann  <christian.sternagel|rene.thiemann@uibk.ac.at>
    Maintainer:  Christian Sternagel and René Thiemann
    License:     LGPL
*)
signature GENERATOR_AUX =
sig
  val alist_to_string : (string * 'a)list -> string

  (* put a string in sub-script *)
  val sub : string -> string

  (* put a type-name in sub-script *)
  val subT : string -> typ -> string

  (* [a,..,n] -> _{a_.._n} *)
  val ints_to_subscript : int list -> string

  (* drop last element of a non-empty list *)
  val drop_last : 'a list -> 'a list

  (* rename old types to new types in term, typ-lists (fst and snd components) are assumed to be distinct *)
  val rename_types : (typ * typ) list -> term -> term

  (* λ x1 ... xn.t *)
  val lambdas : term list -> term -> term

  (* thm[OF _(NONE) foo (SOME foo) ...] *)
  val OF_option : thm -> thm option list -> thm

  (* aim: treat a possible empty conjunction and handle each subcase
     by a specific tactic (indexed from 0 onwards) *)
  val conjI_tac : thm list ->
    Proof.context -> 'a list -> (Proof.context -> int -> tactic) -> tactic

  (* check whether a given type is of a given sort *)
  val is_class_instance : theory -> string -> sort -> bool

  val mk_case_tac :
    Proof.context ->
    term option list list ->
    thm ->
    (int -> Proof.context * thm list * (string * cterm) list -> tactic) ->
    tactic

  (*type-inference after replacing all schematic type-variables by dummyT*)
  val infer_type : Proof.context -> term -> term

  (* like old prove_multi, but in non-blocking future-verion *)
  val prove_multi_future : Proof.context -> string list -> term list -> term list ->
    ({prems: thm list, context: Proof.context} -> tactic) -> thm list

  (* determines all mutual recursive types of a given BNF-least-fixpoint-type *)
  val mutual_recursive_types : string -> Proof.context -> string list * typ list

  (* a fold over types, differentiating mutual recursive types and other type-constructors *)
  val recursor :
    (string -> 'info) * (* accessing the information of a datatype *)
    ('info -> bool list) * (* which arguments are used of a datatype *)
    string list -> (* information on used arguments and recursive types *)
    bool -> (*recursion over all types (or only used types)*)
    (typ -> 'a) -> (* how to treat TFrees *)
    (typ -> 'a) -> (* how to treat TVars *)
    (typ -> 'a) -> (* how to treat recursive case *)
    ((typ * 'a option) list * 'info -> 'a) -> (* how to treat non-rec.-case; NONE result for unused types, if all = false *)
    typ -> 'a

  (* split global list of induction hypotheses according to list of argument types *)
  val split_IHs : (string -> 'info) * ('info -> bool list) * string list -> typ list -> thm list -> thm list list

  (* a standard tactic to solve proof obligation with recursion on types:
     variables and rec.-cases are handled via IHs and preconditions,
     for non-rec.-type constructors  a partial soundness thm has to be generated from the info *)
  val std_recursor_tac : (string -> 'info) * ('info -> bool list) * string list ->
    typ list ->
    ('info -> thm) ->
    thm list -> typ -> thm list -> Proof.context -> tactic

  (* delivers a full type from a type name by instantiating the type-variables of that
   type with different variables of a given sort, also returns the chosen variables
   as second component *)
  val typ_and_vs_of_typname : theory -> string -> sort -> typ * (string * sort) list

  (* similar to typ_and_vs_of_typname, but only for used types the sort contraint will be enforced *)
  val typ_and_vs_of_used_typname : string -> bool list -> string list -> typ * (string * string list) list

  val freeify_tvars : typ -> typ

  val add_used_tycos : Proof.context -> string -> string list -> string list

  val type_parameters : typ -> Proof.context -> (string * sort) list * typ list

  val define_overloaded : (string * term) -> local_theory -> thm * local_theory

  val define_overloaded_generic : (Attrib.binding * term) -> local_theory -> thm * local_theory

  val mk_id : typ -> term

  val mk_def : typ -> string -> term -> term

  val mk_infer_const : string -> Proof.context -> term -> term

  val ind_case_to_idxs : 'a list list -> int -> int * int

  val create_partial :
    'a ->
    (typ -> bool) ->
    (local_theory -> string -> bool list) ->
    (local_theory -> string -> term) ->
    (local_theory -> string -> 'a -> term) ->
    string list ->
    (local_theory -> string -> 'a) ->
    typ ->
    local_theory -> term

  val create_map :
    (typ -> term) -> (*default operation*)
    (string * typ -> 'a -> term) -> (*recursive occurrences of operation*)
    'a -> (*initial state*)
    (typ -> bool) -> (*early abort*)
    (local_theory -> string -> bool list) -> (*used positions*)
    (local_theory -> string -> term) -> (*map function*)
    (local_theory -> string -> 'a -> term) -> (*partial operation*)
    string list -> (*mutually recursive types*)
    (local_theory -> string -> 'a) -> (*next state function*)
    typ -> (*type for which map should be created*)
    local_theory -> term

end

structure Generator_Aux : GENERATOR_AUX =
struct

fun alist_to_string al = map fst al |> commas |> enclose "(" ")"

fun typ_and_vs_of_used_typname typ_name used_pos sort =
  let
    val sorts = map (fn b => if b then sort else @{sort type}) used_pos
    val ty_vars = Name.invent_names (Name.make_context [typ_name]) "a" sorts
    val ty = Type (typ_name,map TFree ty_vars)
  in
    (ty,ty_vars)
  end

fun is_class_instance thy tname class =
  Sorts.has_instance (Sign.classes_of thy) tname class

fun conjI_tac conj_thms ctxt xs tac =
  if null xs then all_tac
  else
    (K (Method.try_intros_tac ctxt conj_thms [])
    THEN_ALL_NEW (fn k' =>
      Subgoal.SUBPROOF (fn {context = ctxt', ...} => tac ctxt' (k' - 1)) ctxt k'))
    1

fun mk_id T =
  let val x = Free ("x", T)
  in lambda x x end

local
  fun create_gen mk_comp dfun mk_p x early_abort up mfun pfun tycos read T lthy =
    let
      fun create x (T as (Type (tyco, Ts))) =
            if early_abort T then mk_id dummyT
            else if member (op =) tycos tyco then mk_p (tyco, T) x
            else
              let
                val x' = read lthy tyco
                val ts = (up lthy tyco ~~ Ts) |> map (fn (used, T) =>
                  if used then create x' T else dfun dummyT)
              in mk_comp (pfun lthy tyco x, list_comb (mfun lthy tyco, ts)) end
        | create _ _ = mk_id dummyT
    in create x T end
in
  fun create_partial x = create_gen HOLogic.mk_comp mk_id ((K o K) (mk_id dummyT)) x
  fun create_map dfun mk_p x = create_gen snd dfun mk_p x
end

fun drop_last [] = raise Empty
  | drop_last (x::xs) =
      let
        fun init _ [] = []
          | init x (y::ys) = x :: init y ys
      in init x xs end

fun rename_types [] t = t
  | rename_types ((t1, t2) :: ts) t =
      if t1 = t2 then rename_types ts t
      else
        let val swap = [(t1, t2), (t2, t1)]
        in
          rename_types
            (map (apfst (typ_subst_atomic swap)) ts)
            (subst_atomic_types swap t)
        end

fun sub s = Symbol.explode s |> map (fn c => "⇩" ^ c) |> implode

fun subT name T = name ^ sub
      (case T of
        TVar (xi, _) => Term.string_of_vname xi
      | TFree (x, _) => x
      | Type (tyco, _) => tyco)

val ints_to_subscript = sub o foldr1 (fn (x, y) => x ^ "_" ^ y) o map string_of_int

fun ind_case_to_idxs cTys=
  let
    fun number n (i, j) ((_ :: xs) :: ys) = (n, (i, j)) :: number (n+1) (i, j+1) (xs :: ys)
      | number n (i, _) ([] :: ys) = number n (i+1, 0) ys
      | number _ _ [] = []
  in AList.lookup (op =) (number 0 (0, 0) cTys) #> the end

(*recursively compute free type variables that are actually used by a given ((co)data)type, i.e.,
are not (indirect) phantom types.*)
fun add_used_tfrees ctxt =
      let
        val thy = Proof_Context.theory_of ctxt

        fun err_schematic T =
              error ("illegal schematic type variable " ^ quote (Syntax.string_of_typ ctxt T))

        fun add _ (T as TVar _) = err_schematic T
          | add _ (TFree (x, _)) = insert (op =) x
          | add skip (Type (tyco, Ts)) =
              if member (op =) skip tyco then I
              else
                (case BNF_FP_Def_Sugar.fp_sugar_of ctxt tyco of
                  NONE => fold (add skip) Ts
                | SOME _ => (*(co)datatype*)
                  BNF_LFP_Compat.the_spec thy tyco
                  |>> map TFree |>> (fn x => x ~~ Ts) ||> map snd ||> flat
                  |> uncurry (map o typ_subst_atomic)
                  |> fold (add (insert (op =) tyco skip)))
      in add [] end

(*collect all Type(constructor) names occurring in a given type*)
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
  | add_tycos _ = I

(*starting from a (co)datatype "tyco", collect all Type(constructor) names that are
involved in its construction*)
fun add_used_tycos ctxt tyco =
      (case BNF_FP_Def_Sugar.fp_sugar_of ctxt tyco of
        NONE => I
      | SOME sugar => #fp_ctr_sugar sugar |> #ctrXs_Tss |> flat |> fold add_tycos)

fun infer_type ctxt =
      map_types (map_type_tvar (K dummyT))
      #> singleton (Type_Infer_Context.infer_types ctxt)

val lambdas = fold_rev lambda

fun mk_def T c rhs = Logic.mk_equals (Const (c, T), rhs)

fun OF_option thm thms = thm OF map (the_default @{lemma "P ⟹ P" by simp}) thms

fun typ_and_vs_of_typname thy typ_name sort =
  let
    val ar = Sign.arity_number thy typ_name
    val sorts = map (K sort) (1 upto ar)
    val ty_vars = Name.invent_names (Name.make_context [typ_name]) "a" sorts
    val ty = Type (typ_name,map TFree ty_vars)
  in (ty,ty_vars) end


(* code copied from HOL/SPARK/TOOLS *)
fun define_overloaded_generic (binding,eq) lthy =
  let
    val ((c, _), rhs) = eq |> Syntax.check_term lthy |>
      Logic.dest_equals |>> dest_Free;
    val ((_, (_, thm)), lthy') = Local_Theory.define
      ((Binding.name c, NoSyn), (binding, rhs)) lthy
    val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
    val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm
  in (thm', lthy')
end

fun define_overloaded (name,eq) = define_overloaded_generic ((Binding.name name, @{attributes [code]}),eq)


fun mk_case_tac ctxt insts thm sub_case_tac =
  (DETERM o Induct.cases_tac ctxt false insts (SOME thm) []
  THEN_ALL_NEW (fn i =>
    Subgoal.SUBPROOF (fn {context = ctxt, prems = hyps, params = params, ...} =>
      sub_case_tac (i-1) (ctxt, hyps, params)) ctxt i))
  1

val freeify_tvars = map_type_tvar (TFree o apfst fst)

fun mutual_recursive_types tyco lthy =
      (case BNF_FP_Def_Sugar.fp_sugar_of lthy tyco of
        SOME sugar =>
          if Sign.arity_number (Proof_Context.theory_of lthy) tyco -
            BNF_Def.live_of_bnf (#fp_bnf sugar) > 0
          then error "only datatypes without dead type parameters are supported"
          else if #fp sugar = BNF_Util.Least_FP then
            sugar |> #fp_res |> #Ts |> `(map (fst o dest_Type))
            ||> map freeify_tvars
          else error "only least fixpoints are supported"
      | NONE => error ("type " ^ quote tyco ^ " does not appear to be a new style datatype"))

fun type_parameters T lthy =
      let
        val tfrees = T |> dest_Type |> snd |> map dest_TFree
        val used_tfrees = (*type parameters of type tyco that are used (maintain original order)*)
          inter (op =) (add_used_tfrees lthy T []) (map fst tfrees)
          |> map (fn a => TFree (a, AList.lookup (op =) tfrees a |> the))
      in (tfrees, used_tfrees) end

fun sum_list xs = fold (curry (op +)) xs 0

fun mk_infer_const name ctxt c = infer_type ctxt (Const (name, dummyT) $ c)

fun prove_multi_future ctxt = Goal.prove_common ctxt (SOME ~1)

fun recursor rec_info all free tvar r typ (T as Type (tyco,Ts)) =
      if member (op =) (#3 rec_info) tyco then r T
      else
        let
          val (get_info,get_used,_) = rec_info
          val info = get_info tyco
          val up = get_used info
          val recs = (if all then map (pair true) Ts else up ~~ Ts) |> map (fn (b, T) =>
            if b then (T, SOME (recursor rec_info all free tvar r typ T)) else (T, NONE))
        in typ (recs, info) end
  | recursor _ _ free _ _ _ (T as TFree _) = free T
  | recursor _ _ _ tvar _ _ (T as TVar _) = tvar T

(* use the recursor to compute the number of IHs, in order to split them *)
fun num_IHs rec_info = recursor rec_info true (K 0) (K 0) (K 1)
      (fn (xs, _) => sum_list (map (the o snd) xs))

fun split_IHs rec_info (ty :: tys : typ list) (IHs : thm list) : thm list list =
      let
        val n = num_IHs rec_info ty
        val _ = if n > length IHs then error "split IH error: too few" else ()
      in
        take n IHs :: split_IHs rec_info tys (drop n IHs)
      end
  | split_IHs _ [] [] = []
  | split_IHs _ [] (_ :: _) = error "split IH error: too many"

fun std_recursor_tac rec_info used_tfrees info_to_pthm assms = recursor rec_info false
      (* TFrees via pre_condition and blast *)
      (fn T => fn IH => fn ctxt =>
          if null IH then
            (resolve_tac ctxt [nth assms (find_index (equal T) used_tfrees)] THEN_ALL_NEW blast_tac ctxt) 1
          else error "error 1 in distributing IHs in recursor_tac")
      (* TVars may not occur *)
      (fn ty => error ("error in recursor_tac for " ^ @{make_string} ty))
      (* recursive case via IH and blast *)
      (K (fn IHs => fn ctxt =>
        if length IHs = 1 then
          (resolve_tac ctxt [hd IHs] THEN_ALL_NEW blast_tac ctxt) 1
        else error "error 2 in distributing IHs in recursor_tac"))
      (* non-rec.-case distributed IHs and invokes partial soundness thm *)
      (fn (tys_tactics, info) => fn IH => fn ctxt =>
        let
          val IHs = split_IHs rec_info (map fst tys_tactics) IH
          val tactics = tys_tactics ~~ IHs |> map_filter (fn ((_, tac_opt), IH) =>
            Option.map (fn f => f IH) tac_opt)
          val pthm = info_to_pthm info
        in
          HEADGOAL (
            resolve_tac ctxt [pthm]
            THEN_ALL_NEW (fn k => Subgoal.SUBPROOF (fn {prems, context = ctxt', ...} =>
              Method.insert_tac ctxt' prems 1
              THEN (nth tactics (k - 1) ctxt')) ctxt k))
        end)

end

(*  Title:       Deriving class instances for datatypes
    Author:      Christian Sternagel and René Thiemann  <christian.sternagel|rene.thiemann@uibk.ac.at>
    Maintainer:  Christian Sternagel and René Thiemann 
    License:     LGPL
*)
section ‹Comparisons›

subsection ‹Comparators and Linear Orders›

theory Comparator
imports Main
begin

text ‹Instead of having to define a strict and a weak linear order, @{term "((<), (≤))"},
 one can alternative use a comparator to define the linear order, which may deliver 
 three possible outcomes when comparing two values.›

datatype order = Eq | Lt | Gt

type_synonym 'a comparator = "'a ⇒ 'a ⇒ order"

text ‹In the following, we provide the obvious definitions how to switch between 
  linear orders and comparators.›

definition lt_of_comp :: "'a comparator ⇒ 'a ⇒ 'a ⇒ bool" where
  "lt_of_comp acomp x y = (case acomp x y of Lt ⇒ True | _ ⇒ False)"

definition le_of_comp :: "'a comparator ⇒ 'a ⇒ 'a ⇒ bool" where
  "le_of_comp acomp x y = (case acomp x y of Gt ⇒ False | _ ⇒ True)"
  
definition comp_of_ords :: "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a comparator" where
  "comp_of_ords le lt x y = (if lt x y then Lt else if le x y then Eq else Gt)"

lemma comp_of_ords_of_le_lt[simp]: "comp_of_ords (le_of_comp c) (lt_of_comp c) = c"
  by (intro ext, auto simp: comp_of_ords_def le_of_comp_def lt_of_comp_def split: order.split)

lemma lt_of_comp_of_ords: "lt_of_comp (comp_of_ords le lt) = lt"
  by (intro ext, auto simp: comp_of_ords_def le_of_comp_def lt_of_comp_def split: order.split)

lemma le_of_comp_of_ords_gen: "(⋀ x y. lt x y ⟹ le x y) ⟹ le_of_comp (comp_of_ords le lt) = le"
  by (intro ext, auto simp: comp_of_ords_def le_of_comp_def lt_of_comp_def split: order.split)

lemma le_of_comp_of_ords_linorder: assumes "class.linorder le lt"
  shows "le_of_comp (comp_of_ords le lt) = le"
proof -
  interpret linorder le lt by fact
  show ?thesis by (rule le_of_comp_of_ords_gen) simp
qed

fun invert_order:: "order ⇒ order" where
  "invert_order Lt = Gt" |
  "invert_order Gt = Lt" |
  "invert_order Eq = Eq"

locale comparator =
  fixes comp :: "'a comparator"
  assumes sym: "invert_order (comp x y) = comp y x"
    and weak_eq: "comp x y = Eq ⟹ x = y"
    and comp_trans: "comp x y = Lt ⟹ comp y z = Lt ⟹ comp x z = Lt"
begin 

lemma eq: "(comp x y = Eq) = (x = y)"
proof
  assume "x = y"
  with sym [of y y] show "comp x y = Eq" by (cases "comp x y") auto
qed (rule weak_eq)

lemma comp_same [simp]:
  "comp x x = Eq"
  by (simp add: eq)

abbreviation "lt ≡ lt_of_comp comp"
abbreviation "le ≡ le_of_comp comp"

sublocale ordering le lt
proof
  note [simp] = lt_of_comp_def le_of_comp_def
  fix x y z :: 'a
  show "le x x" using eq [of x x] by (simp)
  show "le x y ⟹ le y z ⟹ le x z"
    by (cases "comp x y" "comp y z" rule: order.exhaust [case_product order.exhaust])
       (auto dest: comp_trans simp: eq)
  show "le x y ⟹ le y x ⟹ x = y"
    using sym [of x y] by (cases "comp x y") (simp_all add: eq)
  show "lt x y ⟷ le x y ∧ x ≠ y"
    using eq [of x y] by (cases "comp x y") (simp_all)
qed

lemma linorder: "class.linorder le lt"
proof (rule class.linorder.intro)
  interpret order le lt
    using ordering_axioms by (rule ordering_orderI)
  show ‹class.order le lt›
    by (fact order_axioms)
  show ‹class.linorder_axioms le›
  proof
    note [simp] = lt_of_comp_def le_of_comp_def
    fix x y :: 'a
    show "le x y ∨ le y x"
      using sym [of x y] by (cases "comp x y") (simp_all)
  qed
qed

sublocale linorder le lt
  by (rule linorder)

lemma Gt_lt_conv: "comp x y = Gt ⟷ lt y x" 
  unfolding lt_of_comp_def sym[of x y, symmetric] 
  by (cases "comp x y", auto)
lemma Lt_lt_conv: "comp x y = Lt ⟷ lt x y" 
  unfolding lt_of_comp_def by (cases "comp x y", auto)
lemma eq_Eq_conv: "comp x y = Eq ⟷ x = y" 
  by (rule eq)
lemma nGt_le_conv: "comp x y ≠ Gt ⟷ le x y" 
  unfolding le_of_comp_def by (cases "comp x y", auto)
lemma nLt_le_conv: "comp x y ≠ Lt ⟷ le y x" 
  unfolding le_of_comp_def sym[of x y, symmetric] by (cases "comp x y", auto)
lemma nEq_neq_conv: "comp x y ≠ Eq ⟷ x ≠ y" 
  using eq_Eq_conv[of x y] by simp

lemmas le_lt_convs =  nLt_le_conv nGt_le_conv Gt_lt_conv Lt_lt_conv eq_Eq_conv nEq_neq_conv

lemma two_comparisons_into_case_order: 
  "(if le x y then (if x = y then P else Q) else R) = (case_order P Q R (comp x y))" 
  "(if le x y then (if y = x then P else Q) else R) = (case_order P Q R (comp x y))" 
  "(if le x y then (if le y x then P else Q) else R) = (case_order P Q R (comp x y))" 
  "(if le x y then (if lt x y then Q else P) else R) = (case_order P Q R (comp x y))" 
  "(if lt x y then Q else (if le x y then P else R)) = (case_order P Q R (comp x y))" 
  "(if lt x y then Q else (if lt y x then R else P)) = (case_order P Q R (comp x y))" 
  "(if lt x y then Q else (if x = y then P else R)) = (case_order P Q R (comp x y))" 
  "(if lt x y then Q else (if y = x then P else R)) = (case_order P Q R (comp x y))" 
  "(if x = y then P else (if lt y x then R else Q)) = (case_order P Q R (comp x y))" 
  "(if x = y then P else (if lt x y then Q else R)) = (case_order P Q R (comp x y))" 
  "(if x = y then P else (if le y x then R else Q)) = (case_order P Q R (comp x y))" 
  "(if x = y then P else (if le x y then Q else R)) = (case_order P Q R (comp x y))"
  by (auto simp: le_lt_convs split: order.splits)

end

lemma comp_of_ords: assumes "class.linorder le lt"
  shows "comparator (comp_of_ords le lt)"
proof -
  interpret linorder le lt by fact
  show ?thesis
    by (unfold_locales, auto simp: comp_of_ords_def split: if_splits)
qed

definition (in linorder) comparator_of :: "'a comparator" where
  "comparator_of x y = (if x < y then Lt else if x = y then Eq else Gt)"

lemma comparator_of: "comparator comparator_of"
  by unfold_locales (auto split: if_splits simp: comparator_of_def)

end

(*  Title:       Deriving class instances for datatypes
    Author:      Christian Sternagel and René Thiemann  <christian.sternagel|rene.thiemann@uibk.ac.at>
    Maintainer:  Christian Sternagel and René Thiemann 
    License:     LGPL
*)
subsection ‹Compare›

theory Compare
imports Comparator
keywords "compare_code" :: thy_decl
begin

text ‹This introduces a type class for having a proper comparator, similar to @{class linorder}.
  Since most of the Isabelle/HOL algorithms work on the latter, we also provide a method which 
  turns linear-order based algorithms into comparator-based algorithms, where two consecutive 
  invocations of linear orders and equality are merged into one comparator invocation.
  We further define a class which both define a linear order and a comparator, and where the
  induces orders coincide.›

class compare =
  fixes compare :: "'a comparator"
  assumes comparator_compare: "comparator compare"
begin

lemma compare_Eq_is_eq [simp]:
  "compare x y = Eq ⟷ x = y"
  by (rule comparator.eq [OF comparator_compare])
  
lemma compare_refl [simp]:
  "compare x x = Eq"
  by simp

end

lemma (in linorder) le_lt_comparator_of:
  "le_of_comp comparator_of = (≤)" "lt_of_comp comparator_of = (<)"
  by (intro ext, auto simp: comparator_of_def le_of_comp_def lt_of_comp_def)+

class compare_order = ord + compare +
  assumes ord_defs: "le_of_comp compare = (≤) " "lt_of_comp compare = (<)"

text ‹ @{class compare_order} is @{class compare} and @{class linorder}, where comparator and orders 
  define the same ordering.›

subclass (in compare_order) linorder
  by (unfold ord_defs[symmetric], rule comparator.linorder, rule comparator_compare)

context compare_order
begin

lemma compare_is_comparator_of: 
  "compare = comparator_of" 
proof (intro ext)
  fix x y :: 'a
  show "compare x y = comparator_of x y"
    by  (unfold comparator_of_def, unfold ord_defs[symmetric] lt_of_comp_def, 
      cases "compare x y", auto)
qed

lemmas two_comparisons_into_compare = 
  comparator.two_comparisons_into_case_order[OF comparator_compare, unfolded ord_defs]
  
thm two_comparisons_into_compare
end

ML_file ‹compare_code.ML›

text ‹‹Compare_Code.change_compare_code const ty-vars› changes the code equations of some constant such that
  two consecutive comparisons via @{term "(<=)"}, @{term "(<)"}", or @{term "(=)"} are turned into one
  invocation of @{const compare}. 
  The difference to a standard ‹code_unfold› is that here we change the code-equations
  where an additional sort-constraint on @{class compare_order} can be added. Otherwise, there would
  be no @{const compare}-function.›

end

signature COMPARE_CODE =
sig
  
  (* changes the code equations of some constant such that
     two consecutive comparisons via <=, <, or = are turned into one
     invocation of the comparator. 
     The difference to a standard code_unfold is that here we change the code-equations
     where an additional sort-constraint on compare_order can be added. Otherwise, there would
     be no compare-function. *)
  val change_compare_code : 
    term                      (* the constant *) 
    -> string list     (* the list of type parameters which should be constraint to @{sort compare_order} *) 
    -> local_theory -> local_theory

end

structure Compare_Code : COMPARE_CODE =
struct

fun drop_leading_qmark s = 
  if String.isPrefix "?" s then String.substring (s,1,String.size s - 1) else s

fun change_compare_code const inst_names lthy = 
  let
    val inst_names = map drop_leading_qmark inst_names
    val const_string = quote (Pretty.string_of (Syntax.pretty_term lthy const))
    val cname = (case const of Const (cname,_) => cname | _ => 
      error ("expected constant as input, but got " ^ const_string))
    val cert = Code.get_cert lthy [] cname
    val code_eqs = cert |> Code.equations_of_cert (Proof_Context.theory_of lthy)
    |> snd |> these |> map (fst o snd) |> map_filter I
    val _ = if null code_eqs then error "could not find code equations" else ()

    (* adding sort-constraint compare_order within code equations*)
    val const' = hd code_eqs |> Thm.concl_of |> Logic.dest_equals |> fst |> strip_comb |> fst
    val types = Term.add_tvars const' []
    val ctyp_of = TVar #> Thm.ctyp_of lthy
    fun filt s = not (member (op =) (@{sort ord} @ @{sort linorder} @ @{sort order}) s)
    val map_types = maps (fn ty => if List.exists (fn tn => tn = (fst o fst) ty) inst_names then 
      [(ty, ctyp_of (apsnd (fn ss => filter filt ss @ @{sort compare_order}) ty))] else 
      []) types
    val code_eqs = map (Thm.instantiate (map_types, [])) code_eqs 

    (* replace comparisons and register code eqns *)
    val new_code_eqs = map (Local_Defs.unfold lthy @{thms two_comparisons_into_compare}) code_eqs
    val _ = if map Thm.prop_of new_code_eqs = map Thm.prop_of code_eqs then
      warning ("Code equations for " ^ const_string ^ " did not change\n" ^
      "Perhaps you have to provide some type variables which should be restricted to compare_order\n" ^
      (@{make_string} (map TVar types ~~ map snd types, const', code_eqs))) 
      else ()
    val lthy = Local_Theory.note (
      (Binding.name (Long_Name.base_name cname ^ "_compare_code"), @{attributes [code]}), new_code_eqs) lthy 
      |> snd    
  in
    lthy
  end
  
fun change_compare_code_cmd const tnames_option lthy = 
  change_compare_code (Syntax.read_term lthy const) tnames_option lthy

val _ =
  Outer_Syntax.local_theory @{command_keyword compare_code} 
    "turn comparisons via <= and < into compare within code-equations"
    (Scan.optional (@{keyword "("} |-- (Parse.list Parse.string) --| @{keyword ")"}) [] --
      Parse.term >> (fn (inst, c) => change_compare_code_cmd c inst))

end

subsection ‹Example: Modifying the Code-Equations of Red-Black-Trees›

theory RBT_Compare_Order_Impl
imports
  Compare
  "HOL-Library.RBT_Impl"
begin

text ‹In the following, we modify all code-equations of the red-black-tree 
  implementation that perform comparisons. As a positive result, they now all require
  one invocation of comparator, where before two comparisons have been performed.
  The disadvantage of this simple solution is the additional class constraint on
  @{class compare_order}.›

compare_code ("'a") rbt_ins
compare_code ("'a") rbt_lookup
compare_code ("'a") rbt_del
compare_code ("'a") rbt_map_entry
compare_code ("'a") sunion_with
compare_code ("'a") sinter_with
compare_code ("'a") rbt_split

export_code rbt_ins rbt_lookup rbt_del rbt_map_entry rbt_union_with_key rbt_inter_with_key rbt_minus in Haskell

end

subsection ‹A Comparator-Interface to Red-Black-Trees›

theory RBT_Comparator_Impl
imports 
  "HOL-Library.RBT_Impl"
  Comparator
begin

text ‹For all of the main algorithms of red-black trees, we
  provide alternatives which are completely based on comparators,
  and which are provable equivalent. At the time of writing,
  this interface is used in the Container AFP-entry.
  
  It does not rely on the modifications of code-equations as in 
  the previous subsection.›

context 
  fixes c :: "'a comparator"
begin

primrec rbt_comp_lookup :: "('a, 'b) rbt ⇒ 'a ⇀ 'b"
where
  "rbt_comp_lookup RBT_Impl.Empty k = None"
| "rbt_comp_lookup (Branch _ l x y r) k = 
   (case c k x of Lt ⇒ rbt_comp_lookup l k 
     | Gt ⇒ rbt_comp_lookup r k 
     | Eq ⇒ Some y)"

fun
  rbt_comp_ins :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ 'a ⇒ 'b ⇒ ('a,'b) rbt ⇒ ('a,'b) rbt"
where
  "rbt_comp_ins f k v RBT_Impl.Empty = Branch RBT_Impl.R RBT_Impl.Empty k v  RBT_Impl.Empty" |
  "rbt_comp_ins f k v (Branch RBT_Impl.B l x y r) = (case c k x of 
      Lt ⇒ balance (rbt_comp_ins f k v l) x y r
    | Gt ⇒ balance l x y (rbt_comp_ins f k v r)
    | Eq ⇒ Branch RBT_Impl.B l x (f k y v) r)" |
  "rbt_comp_ins f k v (Branch RBT_Impl.R l x y r) = (case c k x of 
      Lt ⇒ Branch RBT_Impl.R (rbt_comp_ins f k v l) x y r
    | Gt ⇒ Branch RBT_Impl.R l x y (rbt_comp_ins f k v r)
    | Eq ⇒ Branch RBT_Impl.R l x (f k y v) r)"

definition rbt_comp_insert_with_key :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ 'a ⇒ 'b ⇒ ('a,'b) rbt ⇒ ('a,'b) rbt"
where "rbt_comp_insert_with_key f k v t = paint RBT_Impl.B (rbt_comp_ins f k v t)"

definition rbt_comp_insert :: "'a ⇒ 'b ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt" where
  "rbt_comp_insert = rbt_comp_insert_with_key (λ_ _ nv. nv)"

fun
  rbt_comp_del_from_left :: "'a ⇒ ('a,'b) rbt ⇒ 'a ⇒ 'b ⇒ ('a,'b) rbt ⇒ ('a,'b) rbt" and
  rbt_comp_del_from_right :: "'a ⇒ ('a,'b) rbt ⇒ 'a ⇒ 'b ⇒ ('a,'b) rbt ⇒ ('a,'b) rbt" and
  rbt_comp_del :: "'a⇒ ('a,'b) rbt ⇒ ('a,'b) rbt"
where
  "rbt_comp_del x RBT_Impl.Empty = RBT_Impl.Empty" |
  "rbt_comp_del x (Branch _ a y s b) = 
   (case c x y of 
        Lt ⇒ rbt_comp_del_from_left x a y s b 
      | Gt ⇒ rbt_comp_del_from_right x a y s b
      | Eq ⇒ combine a b)" |
  "rbt_comp_del_from_left x (Branch RBT_Impl.B lt z v rt) y s b = balance_left (rbt_comp_del x (Branch RBT_Impl.B lt z v rt)) y s b" |
  "rbt_comp_del_from_left x a y s b = Branch RBT_Impl.R (rbt_comp_del x a) y s b" |
  "rbt_comp_del_from_right x a y s (Branch RBT_Impl.B lt z v rt) = balance_right a y s (rbt_comp_del x (Branch RBT_Impl.B lt z v rt))" | 
  "rbt_comp_del_from_right x a y s b = Branch RBT_Impl.R a y s (rbt_comp_del x b)"

definition "rbt_comp_delete k t = paint RBT_Impl.B (rbt_comp_del k t)"

definition "rbt_comp_bulkload xs = foldr (λ(k, v). rbt_comp_insert k v) xs RBT_Impl.Empty"

primrec
  rbt_comp_map_entry :: "'a ⇒ ('b ⇒ 'b) ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt"
where
  "rbt_comp_map_entry k f RBT_Impl.Empty = RBT_Impl.Empty"
| "rbt_comp_map_entry k f (Branch cc lt x v rt) =
    (case c k x of 
        Lt ⇒ Branch cc (rbt_comp_map_entry k f lt) x v rt
      | Gt ⇒ Branch cc lt x v (rbt_comp_map_entry k f rt)
      | Eq ⇒ Branch cc lt x (f v) rt)"

function comp_sunion_with :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ ('a × 'b) list ⇒ ('a × 'b) list ⇒ ('a × 'b) list" 
where
  "comp_sunion_with f ((k, v) # as) ((k', v') # bs) =
   (case c k' k of 
        Lt ⇒ (k', v') # comp_sunion_with f ((k, v) # as) bs
      | Gt ⇒ (k, v) # comp_sunion_with f as ((k', v') # bs)
      | Eq ⇒ (k, f k v v') # comp_sunion_with f as bs)"
| "comp_sunion_with f [] bs = bs"
| "comp_sunion_with f as [] = as"
by pat_completeness auto
termination by lexicographic_order

function comp_sinter_with :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ ('a × 'b) list ⇒ ('a × 'b) list ⇒ ('a × 'b) list"
where
  "comp_sinter_with f ((k, v) # as) ((k', v') # bs) =
  (case c k' k of 
      Lt ⇒ comp_sinter_with f ((k, v) # as) bs
    | Gt ⇒ comp_sinter_with f as ((k', v') # bs)
    | Eq ⇒ (k, f k v v') # comp_sinter_with f as bs)"
| "comp_sinter_with f [] _ = []"
| "comp_sinter_with f _ [] = []"
by pat_completeness auto
termination by lexicographic_order

fun rbt_split_comp :: "('a, 'b) rbt ⇒ 'a ⇒ ('a, 'b) rbt × 'b option × ('a, 'b) rbt" where
  "rbt_split_comp RBT_Impl.Empty k = (RBT_Impl.Empty, None, RBT_Impl.Empty)"
| "rbt_split_comp (RBT_Impl.Branch _ l a b r) x = (case c x a of
    Lt ⇒ (case rbt_split_comp l x of (l1, β, l2) ⇒ (l1, β, rbt_join l2 a b r))
  | Gt ⇒ (case rbt_split_comp r x of (r1, β, r2) ⇒ (rbt_join l a b r1, β, r2))
  | Eq ⇒ (l, Some b, r))"

lemma rbt_split_comp_size: "(l2, b, r2) = rbt_split_comp t2 a ⟹ size l2 + size r2 ≤ size t2"
  by (induction t2 a arbitrary: l2 b r2 rule: rbt_split_comp.induct)
     (auto split: order.splits if_splits prod.splits)

function rbt_comp_union_rec :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt" where
  "rbt_comp_union_rec f t1 t2 = (let (f, t2, t1) =
    if flip_rbt t2 t1 then (λk v v'. f k v' v, t1, t2) else (f, t2, t1) in
    if small_rbt t2 then RBT_Impl.fold (rbt_comp_insert_with_key f) t2 t1
    else (case t1 of RBT_Impl.Empty ⇒ t2
      | RBT_Impl.Branch _ l1 a b r1 ⇒
        case rbt_split_comp t2 a of (l2, β, r2) ⇒
          rbt_join (rbt_comp_union_rec f l1 l2) a (case β of None ⇒ b | Some b' ⇒ f a b b') (rbt_comp_union_rec f r1 r2)))"
  by pat_completeness auto
termination
  using rbt_split_comp_size
  by (relation "measure (λ(f,t1,t2). size t1 + size t2)") (fastforce split: if_splits)+

declare rbt_comp_union_rec.simps[simp del]

function rbt_comp_union_swap_rec :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ bool ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt" where
  "rbt_comp_union_swap_rec f γ t1 t2 = (let (γ, t2, t1) =
    if flip_rbt t2 t1 then (¬γ, t1, t2) else (γ, t2, t1);
    f' = (if γ then (λk v v'. f k v' v) else f) in
    if small_rbt t2 then RBT_Impl.fold (rbt_comp_insert_with_key f') t2 t1
    else case t1 of rbt.Empty ⇒ t2
      | Branch x l1 a b r1 ⇒
        case rbt_split_comp t2 a of (l2, β, r2) ⇒
          rbt_join (rbt_comp_union_swap_rec f γ l1 l2) a (case β of None ⇒ b | Some x ⇒ f' a b x) (rbt_comp_union_swap_rec f γ r1 r2))"
  by pat_completeness auto
termination
  using rbt_split_comp_size
  by (relation "measure (λ(f,γ,t1, t2). size t1 + size t2)") (fastforce split: if_splits)+

declare rbt_comp_union_swap_rec.simps[simp del]

lemma rbt_comp_union_swap_rec: "rbt_comp_union_swap_rec f γ t1 t2 =
  rbt_comp_union_rec (if γ then (λk v v'. f k v' v) else f) t1 t2"
proof (induction f γ t1 t2 rule: rbt_comp_union_swap_rec.induct)
  case (1 f γ t1 t2)
  show ?case
    using 1[OF refl _ refl refl _ refl _ refl]
    unfolding rbt_comp_union_swap_rec.simps[of _ _ t1] rbt_comp_union_rec.simps[of _ t1]
    by (auto simp: Let_def split: rbt.splits prod.splits option.splits) (* slow *)
qed

lemma rbt_comp_union_swap_rec_code[code]: "rbt_comp_union_swap_rec f γ t1 t2 = (
    let bh1 = bheight t1; bh2 = bheight t2; (γ, t2, bh2, t1, bh1) =
    if bh1 < bh2 then (¬γ, t1, bh1, t2, bh2) else (γ, t2, bh2, t1, bh1);
    f' = (if γ then (λk v v'. f k v' v) else f) in
    if bh2 < 4 then RBT_Impl.fold (rbt_comp_insert_with_key f') t2 t1
    else case t1 of rbt.Empty ⇒ t2
      | Branch x l1 a b r1 ⇒
        case rbt_split_comp t2 a of (l2, β, r2) ⇒
          rbt_join (rbt_comp_union_swap_rec f γ l1 l2) a (case β of None ⇒ b | Some x ⇒ f' a b x) (rbt_comp_union_swap_rec f γ r1 r2))"
  by (auto simp: rbt_comp_union_swap_rec.simps flip_rbt_def small_rbt_def)

definition "rbt_comp_union_with_key f t1 t2 = paint RBT_Impl.B (rbt_comp_union_swap_rec f False t1 t2)"

definition "map_filter_comp_inter f t1 t2 = List.map_filter (λ(k, v).
  case rbt_comp_lookup t1 k of None ⇒ None
  | Some v' ⇒ Some (k, f k v' v)) (RBT_Impl.entries t2)"

function rbt_comp_inter_rec :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt" where
  "rbt_comp_inter_rec f t1 t2 = (let (f, t2, t1) =
    if flip_rbt t2 t1 then (λk v v'. f k v' v, t1, t2) else (f, t2, t1) in
    if small_rbt t2 then rbtreeify (map_filter_comp_inter f t1 t2)
    else case t1 of RBT_Impl.Empty ⇒ RBT_Impl.Empty
    | RBT_Impl.Branch _ l1 a b r1 ⇒
      case rbt_split_comp t2 a of (l2, β, r2) ⇒ let l' = rbt_comp_inter_rec f l1 l2; r' = rbt_comp_inter_rec f r1 r2 in
      (case β of None ⇒ rbt_join2 l' r' | Some b' ⇒ rbt_join l' a (f a b b') r'))"
  by pat_completeness auto
termination
  using rbt_split_comp_size
  by (relation "measure (λ(f,t1,t2). size t1 + size t2)") (fastforce split: if_splits)+

declare rbt_comp_inter_rec.simps[simp del]

function rbt_comp_inter_swap_rec :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ bool ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt" where
  "rbt_comp_inter_swap_rec f γ t1 t2 = (let (γ, t2, t1) =
    if flip_rbt t2 t1 then (¬γ, t1, t2) else (γ, t2, t1);
    f' = if γ then (λk v v'. f k v' v) else f in
    if small_rbt t2 then rbtreeify (map_filter_comp_inter f' t1 t2)
    else case t1 of rbt.Empty ⇒ rbt.Empty
    | Branch x l1 a b r1 ⇒
      (case rbt_split_comp t2 a of (l2, β, r2) ⇒ let l' = rbt_comp_inter_swap_rec f γ l1 l2; r' = rbt_comp_inter_swap_rec f γ r1 r2 in
      (case β of None ⇒ rbt_join2 l' r' | Some b' ⇒ rbt_join l' a (f' a b b') r')))"
  by pat_completeness auto
termination
  using rbt_split_comp_size
  by (relation "measure (λ(f,γ,t1,t2). size t1 + size t2)") (fastforce split: if_splits)+

declare rbt_comp_inter_swap_rec.simps[simp del]

lemma rbt_comp_inter_swap_rec: "rbt_comp_inter_swap_rec f γ t1 t2 =
  rbt_comp_inter_rec (if γ then (λk v v'. f k v' v) else f) t1 t2"
proof (induction f γ t1 t2 rule: rbt_comp_inter_swap_rec.induct)
  case (1 f γ t1 t2)
  show ?case
    using 1[OF refl _ refl refl _ refl _ refl]
    unfolding rbt_comp_inter_swap_rec.simps[of _ _ t1] rbt_comp_inter_rec.simps[of _ t1]
    by (auto simp: Let_def split: rbt.splits prod.splits option.splits)
qed

lemma comp_inter_with_key_code[code]: "rbt_comp_inter_swap_rec f γ t1 t2 = (
  let bh1 = bheight t1; bh2 = bheight t2; (γ, t2, bh2, t1, bh1) =
  if bh1 < bh2 then (¬γ, t1, bh1, t2, bh2) else (γ, t2, bh2, t1, bh1);
  f' = (if γ then (λk v v'. f k v' v) else f) in
  if bh2 < 4 then rbtreeify (map_filter_comp_inter f' t1 t2)
  else case t1 of rbt.Empty ⇒ rbt.Empty
    | Branch x l1 a b r1 ⇒
      (case rbt_split_comp t2 a of (l2, β, r2) ⇒ let l' = rbt_comp_inter_swap_rec f γ l1 l2; r' = rbt_comp_inter_swap_rec f γ r1 r2 in
      (case β of None ⇒ rbt_join2 l' r' | Some b' ⇒ rbt_join l' a (f' a b b') r')))"
  by (auto simp: rbt_comp_inter_swap_rec.simps flip_rbt_def small_rbt_def)

definition "rbt_comp_inter_with_key f t1 t2 = paint RBT_Impl.B (rbt_comp_inter_swap_rec f False t1 t2)"

definition "filter_comp_minus t1 t2 =
  filter (λ(k, _). rbt_comp_lookup t2 k = None) (RBT_Impl.entries t1)"

fun comp_minus :: "('a, 'b) rbt ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt" where
  "comp_minus t1 t2 = (if small_rbt t2 then RBT_Impl.fold (λk _ t. rbt_comp_delete k t) t2 t1
    else if small_rbt t1 then rbtreeify (filter_comp_minus t1 t2)
    else case t2 of RBT_Impl.Empty ⇒ t1
      | RBT_Impl.Branch _ l2 a b r2 ⇒
        case rbt_split_comp t1 a of (l1, _, r1) ⇒ rbt_join2 (comp_minus l1 l2) (comp_minus r1 r2))"

declare comp_minus.simps[simp del]

definition "rbt_comp_minus t1 t2 = paint RBT_Impl.B (comp_minus t1 t2)"

context
  assumes c: "comparator c"
begin

lemma rbt_comp_lookup: "rbt_comp_lookup = ord.rbt_lookup (lt_of_comp c)" 
proof (intro ext)
  fix k and t :: "('a,'b)rbt"
  show "rbt_comp_lookup t k = ord.rbt_lookup (lt_of_comp c) t k"
    by (induct t, unfold rbt_comp_lookup.simps ord.rbt_lookup.simps
      comparator.two_comparisons_into_case_order[OF c]) 
      (auto split: order.splits)
qed  

lemma rbt_comp_ins: "rbt_comp_ins = ord.rbt_ins (lt_of_comp c)" 
proof (intro ext)
  fix f k v and t :: "('a,'b)rbt"
  show "rbt_comp_ins f k v t = ord.rbt_ins (lt_of_comp c) f k v t"
    by (induct f k v t rule: rbt_comp_ins.induct, unfold rbt_comp_ins.simps ord.rbt_ins.simps
      comparator.two_comparisons_into_case_order[OF c]) 
      (auto split: order.splits)
qed  

lemma rbt_comp_insert_with_key: "rbt_comp_insert_with_key = ord.rbt_insert_with_key (lt_of_comp c)"
  unfolding rbt_comp_insert_with_key_def[abs_def] ord.rbt_insert_with_key_def[abs_def]
  unfolding rbt_comp_ins ..

lemma rbt_comp_insert: "rbt_comp_insert = ord.rbt_insert (lt_of_comp c)"
  unfolding rbt_comp_insert_def[abs_def] ord.rbt_insert_def[abs_def]
  unfolding rbt_comp_insert_with_key ..

lemma rbt_comp_del: "rbt_comp_del = ord.rbt_del (lt_of_comp c)" 
proof - {
  fix k a b and s t :: "('a,'b)rbt"
  have 
    "rbt_comp_del_from_left k t a b s = ord.rbt_del_from_left (lt_of_comp c) k t a b s"
    "rbt_comp_del_from_right k t a b s = ord.rbt_del_from_right (lt_of_comp c) k t a b s"
    "rbt_comp_del k t = ord.rbt_del (lt_of_comp c) k t"
  by (induct k t a b s and k t a b s and k t rule: rbt_comp_del_from_left_rbt_comp_del_from_right_rbt_comp_del.induct,
    unfold 
      rbt_comp_del.simps ord.rbt_del.simps
      rbt_comp_del_from_left.simps ord.rbt_del_from_left.simps
      rbt_comp_del_from_right.simps ord.rbt_del_from_right.simps
      comparator.two_comparisons_into_case_order[OF c],
    auto split: order.split) 
  }
  thus ?thesis by (intro ext)
qed  

lemma rbt_comp_delete: "rbt_comp_delete = ord.rbt_delete (lt_of_comp c)"
  unfolding rbt_comp_delete_def[abs_def] ord.rbt_delete_def[abs_def]
  unfolding rbt_comp_del ..

lemma rbt_comp_bulkload: "rbt_comp_bulkload = ord.rbt_bulkload (lt_of_comp c)"
  unfolding rbt_comp_bulkload_def[abs_def] ord.rbt_bulkload_def[abs_def]
  unfolding rbt_comp_insert ..

lemma rbt_comp_map_entry: "rbt_comp_map_entry = ord.rbt_map_entry (lt_of_comp c)" 
proof (intro ext)
  fix f k and t :: "('a,'b)rbt"
  show "rbt_comp_map_entry f k t = ord.rbt_map_entry (lt_of_comp c) f k t"
    by (induct t, unfold rbt_comp_map_entry.simps ord.rbt_map_entry.simps
      comparator.two_comparisons_into_case_order[OF c]) 
      (auto split: order.splits)
qed  

lemma comp_sunion_with: "comp_sunion_with = ord.sunion_with (lt_of_comp c)"
proof (intro ext)
  fix f and as bs :: "('a × 'b)list"
  show "comp_sunion_with f as bs = ord.sunion_with (lt_of_comp c) f as bs"
    by (induct f as bs rule: comp_sunion_with.induct,
      unfold comp_sunion_with.simps ord.sunion_with.simps
      comparator.two_comparisons_into_case_order[OF c]) 
      (auto split: order.splits)
qed

lemma anti_sym: "lt_of_comp c a x ⟹ lt_of_comp c x a ⟹ False"
  by (metis c comparator.Gt_lt_conv comparator.Lt_lt_conv order.distinct(5))

lemma rbt_split_comp: "rbt_split_comp t x = ord.rbt_split (lt_of_comp c) t x"
  by (induction t x rule: rbt_split_comp.induct)
     (auto simp: ord.rbt_split.simps comparator.le_lt_convs[OF c]
      split: order.splits prod.splits dest: anti_sym)

lemma comp_union_with_key: "rbt_comp_union_rec f t1 t2 = ord.rbt_union_rec (lt_of_comp c) f t1 t2"
proof (induction f t1 t2 rule: rbt_comp_union_rec.induct)
  case (1 f t1 t2)
  obtain f' t1' t2' where flip: "(f', t2', t1') =
    (if flip_rbt t2 t1 then (λk v v'. f k v' v, t1, t2) else (f, t2, t1))"
    by fastforce
  show ?case
  proof (cases t1')
    case (Branch _ l1 a b r1)
    have t1_not_Empty: "t1' ≠ RBT_Impl.Empty"
      by (auto simp: Branch)
    obtain l2 β r2 where split: "rbt_split_comp t2' a = (l2, β, r2)"
      by (cases "rbt_split_comp t2' a") auto
    show ?thesis
      using 1[OF flip refl _ _ Branch]
      unfolding rbt_comp_union_rec.simps[of _ t1] ord.rbt_union_rec.simps[of _ _ t1] flip[symmetric]
      by (auto simp: Branch split rbt_split_comp[symmetric] rbt_comp_insert_with_key
          split: prod.splits)
  qed (auto simp: rbt_comp_union_rec.simps[of _ t1] ord.rbt_union_rec.simps[of _ _ t1] flip[symmetric]
       rbt_comp_insert_with_key rbt_split_comp[symmetric])
qed

lemma comp_sinter_with: "comp_sinter_with = ord.sinter_with (lt_of_comp c)"
proof (intro ext)
  fix f and as bs :: "('a × 'b)list"
  show "comp_sinter_with f as bs = ord.sinter_with (lt_of_comp c) f as bs"
    by (induct f as bs rule: comp_sinter_with.induct,
      unfold comp_sinter_with.simps ord.sinter_with.simps
      comparator.two_comparisons_into_case_order[OF c]) 
      (auto split: order.splits)
qed

lemma rbt_comp_union_with_key: "rbt_comp_union_with_key = ord.rbt_union_with_key (lt_of_comp c)"
  by (rule ext)+
     (auto simp: rbt_comp_union_with_key_def rbt_comp_union_swap_rec ord.rbt_union_with_key_def
      ord.rbt_union_swap_rec comp_union_with_key)

lemma comp_inter_with_key: "rbt_comp_inter_rec f t1 t2 = ord.rbt_inter_rec (lt_of_comp c) f t1 t2"
proof (induction f t1 t2 rule: rbt_comp_inter_rec.induct)
  case (1 f t1 t2)
  obtain f' t1' t2' where flip: "(f', t2', t1') =
    (if flip_rbt t2 t1 then (λk v v'. f k v' v, t1, t2) else (f, t2, t1))"
    by fastforce
  show ?case
  proof (cases t1')
    case (Branch _ l1 a b r1)
    have t1_not_Empty: "t1' ≠ RBT_Impl.Empty"
      by (auto simp: Branch)
    obtain l2 β r2 where split: "rbt_split_comp t2' a = (l2, β, r2)"
      by (cases "rbt_split_comp t2' a") auto
    show ?thesis
      using 1[OF flip refl _ _ Branch]
      unfolding rbt_comp_inter_rec.simps[of _ t1] ord.rbt_inter_rec.simps[of _ _ t1] flip[symmetric]
      by (auto simp: Branch split rbt_split_comp[symmetric] rbt_comp_lookup
          ord.map_filter_inter_def map_filter_comp_inter_def split: prod.splits)
  qed (auto simp: rbt_comp_inter_rec.simps[of _ t1] ord.rbt_inter_rec.simps[of _ _ t1] flip[symmetric]
       ord.map_filter_inter_def map_filter_comp_inter_def rbt_comp_lookup rbt_split_comp[symmetric])
qed

lemma rbt_comp_inter_with_key: "rbt_comp_inter_with_key = ord.rbt_inter_with_key (lt_of_comp c)"
  by (rule ext)+
     (auto simp: rbt_comp_inter_with_key_def rbt_comp_inter_swap_rec
      ord.rbt_inter_with_key_def ord.rbt_inter_swap_rec comp_inter_with_key)

lemma comp_minus: "comp_minus t1 t2 = ord.rbt_minus_rec (lt_of_comp c) t1 t2"
proof (induction t1 t2 rule: comp_minus.induct)
  case (1 t1 t2)
  show ?case
  proof (cases t2)
    case (Branch _ l2 a u r2)
    have t2_not_Empty: "t2 ≠ RBT_Impl.Empty"
      by (auto simp: Branch)
    obtain l1 β r1 where split: "rbt_split_comp t1 a = (l1, β, r1)"
      by (cases "rbt_split_comp t1 a") auto
    show ?thesis
      using 1[OF _ _ Branch]
      unfolding comp_minus.simps[of t1 t2] ord.rbt_minus_rec.simps[of _ t1 t2]
      by (auto simp: Branch split rbt_split_comp[symmetric] rbt_comp_delete rbt_comp_lookup
          filter_comp_minus_def ord.filter_minus_def split: prod.splits)
  qed (auto simp: comp_minus.simps[of t1] ord.rbt_minus_rec.simps[of _ t1]
       filter_comp_minus_def ord.filter_minus_def
       rbt_comp_delete rbt_comp_lookup rbt_split_comp[symmetric])
qed

lemma rbt_comp_minus: "rbt_comp_minus = ord.rbt_minus (lt_of_comp c)"
  by (rule ext)+ (auto simp: rbt_comp_minus_def ord.rbt_minus_def comp_minus)

lemmas rbt_comp_simps = 
  rbt_comp_insert
  rbt_comp_lookup
  rbt_comp_delete
  rbt_comp_bulkload
  rbt_comp_map_entry
  rbt_comp_union_with_key
  rbt_comp_inter_with_key
  rbt_comp_minus
end
end

end