Theory Compatibility_Containers_Regular_Sets

(*  Title:      Containers/Compatibility_Containers_Regular_Sets.thy
    Author:     Andreas Lochbihler, ETH Zurich *)

section ‹Compatibility with Regular-Sets›

theory Compatibility_Containers_Regular_Sets imports
  Containers
  "Regular-Sets.Regexp_Method"
begin

text ‹
  Adaptation theory to make ‹regexp› work when @{theory Containers.Containers} are loaded.

  Warning: Each invocation of ‹regexp› takes longer than without @{theory Containers.Containers}
  because the code generator takes longer to generate the evaluation code for ‹regexp›.
›

datatype_compat rexp
derive ceq rexp
derive ccompare rexp
derive (choose) set_impl rexp

notepad begin
fix r s :: "('a × 'a) set"
have "(r ∪ s^+)^* = (r ∪ s)^*" by regexp
end

end