Session MFODL_Monitor_Optimized

Theory Code_Double

(*<*)
theory Code_Double
  imports IEEE_Floating_Point.IEEE_Properties
    "HOL-Library.Code_Target_Int"
    Containers.Collection_Eq
    Containers.Collection_Order
begin
(*>*)

section ‹Code adaptation for IEEE double-precision floats›

subsection ‹copysign›

lift_definition copysign :: "('e, 'f) float  ('e, 'f) float  ('e, 'f) float" is
  "λ(_, e::'e word, f::'f word) (s::1 word, _, _). (s, e, f)" .

lemma is_nan_copysign[simp]: "is_nan (copysign x y)  is_nan x"
  unfolding is_nan_def by transfer auto


subsection ‹Additional lemmas about generic floats›

lemma is_nan_some_nan[simp]: "is_nan (some_nan :: ('e, 'f) float)"
  unfolding some_nan_def
  by (rule someI[where x="Abs_float (0, max_word :: 'e word, 1)"])
    (auto simp add: is_nan_def exponent_def fraction_def emax_def Abs_float_inverse[simplified])

lemma not_is_nan_0[simp]: "¬ is_nan 0"
  unfolding is_nan_def by (simp add: zero_simps)

lemma not_is_nan_1[simp]: "¬ is_nan 1"
  unfolding is_nan_def by transfer simp

lemma is_nan_plus: "is_nan x  is_nan y  is_nan (x + y)"
  unfolding plus_float_def fadd_def by auto

lemma is_nan_minus: "is_nan x  is_nan y  is_nan (x - y)"
  unfolding minus_float_def fsub_def by auto

lemma is_nan_times: "is_nan x  is_nan y  is_nan (x * y)"
  unfolding times_float_def fmul_def by auto

lemma is_nan_divide: "is_nan x  is_nan y  is_nan (x / y)"
  unfolding divide_float_def fdiv_def by auto

lemma is_nan_float_sqrt: "is_nan x  is_nan (float_sqrt x)"
  unfolding float_sqrt_def fsqrt_def by simp

lemma nan_fcompare: "is_nan x  is_nan y  fcompare x y = Und"
  unfolding fcompare_def by simp

lemma nan_not_le: "is_nan x  is_nan y  ¬ x  y"
  unfolding less_eq_float_def fle_def fcompare_def by simp

lemma nan_not_less: "is_nan x  is_nan y  ¬ x < y"
  unfolding less_float_def flt_def fcompare_def by simp

lemma nan_not_zero: "is_nan x  ¬ is_zero x"
  unfolding is_nan_def is_zero_def by simp

lemma nan_not_infinity: "is_nan x  ¬ is_infinity x"
  unfolding is_nan_def is_infinity_def by simp

lemma zero_not_infinity: "is_zero x  ¬ is_infinity x"
  unfolding is_zero_def is_infinity_def by simp

lemma zero_not_nan: "is_zero x  ¬ is_nan x"
  unfolding is_zero_def is_nan_def by simp


lemma minus_one_power_one_word: "(-1 :: real) ^ unat (x :: 1 word) = (if unat x = 0 then 1 else -1)"
proof -
  have "unat x = 0  unat x = 1"
    using le_SucE[OF unat_one_word_le] by auto
  then show ?thesis by auto
qed

definition valofn :: "('e, 'f) float  real" where
  "valofn x = (2^exponent x / 2^bias TYPE(('e, 'f) float)) *
      (1 + real (fraction x) / 2^LENGTH('f))"

definition valofd :: "('e, 'f) float  real" where
  "valofd x = (2 / 2^bias TYPE(('e, 'f) float)) * (real (fraction x) / 2^LENGTH('f))"

lemma valof_alt: "valof x = (if exponent x = 0 then
    if sign x = 0 then valofd x else - valofd x
  else if sign x = 0 then valofn x else - valofn x)"
  unfolding valofn_def valofd_def
  by transfer (auto simp: minus_one_power_one_word unat_eq_0 field_simps)

lemma fraction_less_2p: "fraction (x :: ('e, 'f) float) < 2^LENGTH('f)"
  by transfer auto

lemma valofn_ge_0: "0  valofn x"
  unfolding valofn_def by simp

lemma valofn_ge_2p: "2^exponent (x :: ('e, 'f) float) / 2^bias TYPE(('e, 'f) float)  valofn x"
  unfolding valofn_def by (simp add: field_simps)

lemma valofn_less_2p:
  fixes x :: "('e, 'f) float"
  assumes "exponent x < e"
  shows "valofn x < 2^e / 2^bias TYPE(('e, 'f) float)"
proof -
  have "1 + real (fraction x) / 2^LENGTH('f) < 2"
    by (simp add: fraction_less_2p)
  then have "valofn x < (2^exponent x / 2^bias TYPE(('e, 'f) float)) * 2"
    unfolding valofn_def by (simp add: field_simps)
  also have "...  2^e / 2^bias TYPE(('e, 'f) float)"
    using assms by (auto simp: less_eq_Suc_le field_simps elim: order_trans[rotated, OF exp_less])
  finally show ?thesis .
qed

lemma valofd_ge_0: "0  valofd x"
  unfolding valofd_def by simp

lemma valofd_less_2p: "valofd (x :: ('e, 'f) float) < 2 / 2^bias TYPE(('e, 'f) float)"
  unfolding valofd_def
  by (simp add: fraction_less_2p field_simps)

lemma valofn_le_imp_exponent_le:
  fixes x y :: "('e, 'f) float"
  assumes "valofn x  valofn y"
  shows "exponent x  exponent y"
proof (rule ccontr)
  assume "¬ exponent x  exponent y"
  then have "valofn y < 2^exponent x / 2^bias TYPE(('e, 'f) float)"
    using valofn_less_2p[of y] by auto
  also have "...  valofn x" by (rule valofn_ge_2p)
  finally show False using assms by simp
qed

lemma valofn_eq:
  fixes x y :: "('e, 'f) float"
  assumes "valofn x = valofn y"
  shows "exponent x = exponent y" "fraction x = fraction y"
proof -
  from assms show "exponent x = exponent y"
    by (auto intro!: antisym valofn_le_imp_exponent_le)
  with assms show "fraction x = fraction y"
    unfolding valofn_def by (simp add: field_simps)
qed

lemma valofd_eq:
  fixes x y :: "('e, 'f) float"
  assumes "valofd x = valofd y"
  shows "fraction x = fraction y"
  using assms unfolding valofd_def by (simp add: field_simps)

lemma is_zero_valof_conv: "is_zero x  valof x = 0"
  unfolding is_zero_def valof_alt
  using valofn_ge_2p[of x] by (auto simp: valofd_def field_simps dest: order.antisym)

lemma valofd_neq_valofn:
  fixes x y :: "('e, 'f) float"
  assumes "exponent y  0"
  shows "valofd x  valofn y" "valofn y  valofd x"
proof -
  have "valofd x < 2 / 2^bias TYPE(('e, 'f) float)" by (rule valofd_less_2p)
  also have "...  2 ^ IEEE.exponent y / 2 ^ bias TYPE(('e, 'f) IEEE.float)"
    using assms by (simp add: self_le_power field_simps)
  also have "...  valofn y" by (rule valofn_ge_2p)
  finally show "valofd x  valofn y" "valofn y  valofd x" by simp_all
qed

lemma sign_gt_0_conv: "0 < sign x  sign x = 1"
  by (cases x rule: sign_cases) simp_all

lemma valof_eq:
  assumes "¬ is_zero x  ¬ is_zero y"
  shows "valof x = valof y  x = y"
proof
  assume *: "valof x = valof y"
  with assms have "valof y  0" by (simp add: is_zero_valof_conv)
  with * show "x = y"
    unfolding valof_alt
    using valofd_ge_0[of x] valofd_ge_0[of y] valofn_ge_0[of x] valofn_ge_0[of y]
    by (auto simp: valofd_neq_valofn sign_gt_0_conv split: if_splits
        intro!: float_eqI elim: valofn_eq valofd_eq)
qed simp

lemma zero_fcompare: "is_zero x  is_zero y  fcompare x y = ccode.Eq"
  unfolding fcompare_def by (simp add: zero_not_infinity zero_not_nan is_zero_valof_conv)


subsection ‹Doubles with a unified NaN value›

quotient_type double = "(11, 52) float" / "λx y. is_nan x  is_nan y  x = y"
  by (auto intro!: equivpI reflpI sympI transpI)

instantiation double :: "{zero, one, plus, minus, uminus, times, ord}"
begin

lift_definition zero_double :: "double" is "0" .
lift_definition one_double :: "double" is "1" .

lift_definition plus_double :: "double  double  double" is plus
  by (auto simp: is_nan_plus)

lift_definition minus_double :: "double  double  double" is minus
  by (auto simp: is_nan_minus)

lift_definition uminus_double :: "double  double" is uminus
  by auto

lift_definition times_double :: "double  double  double" is times
  by (auto simp: is_nan_times)

lift_definition less_eq_double :: "double  double  bool" is "(≤)"
  by (auto simp: nan_not_le)

lift_definition less_double :: "double  double  bool" is "(<)"
  by (auto simp: nan_not_less)

instance ..

end

instantiation double :: inverse
begin

lift_definition divide_double :: "double  double  double" is divide
  by (auto simp: is_nan_divide)

definition inverse_double :: "double  double" where
  "inverse_double x = 1 div x"

instance ..

end

lift_definition sqrt_double :: "double  double" is float_sqrt
  by (auto simp: is_nan_float_sqrt)

no_notation plus_infinity ("")

lift_definition infinity :: "double" is plus_infinity .

lift_definition nan :: "double" is some_nan .

lift_definition is_zero :: "double  bool" is IEEE.is_zero
  by (auto simp: nan_not_zero)

lift_definition is_infinite :: "double  bool" is IEEE.is_infinity
  by (auto simp: nan_not_infinity)

lift_definition is_nan :: "double  bool" is IEEE.is_nan
  by auto

lemma is_nan_conv: "is_nan x  x = nan"
  by transfer auto

lift_definition copysign_double :: "double  double  double" is
  "λx y. if IEEE.is_nan y then some_nan else copysign x y"
  by auto

text ‹Note: @{const copysign_double} deviates from the IEEE standard in cases where
  the second argument is a NaN.›

lift_definition fcompare_double :: "double  double  ccode" is fcompare
  by (auto simp: nan_fcompare)

lemma nan_fcompare_double: "is_nan x  is_nan y  fcompare_double x y = Und"
  by transfer (rule nan_fcompare)

consts compare_double :: "double  double  integer"

specification (compare_double)
  compare_double_less: "compare_double x y < 0  is_nan x  ¬ is_nan y  fcompare_double x y = ccode.Lt"
  compare_double_eq: "compare_double x y = 0  is_nan x  is_nan y  fcompare_double x y = ccode.Eq"
  compare_double_greater: "compare_double x y > 0  ¬ is_nan x  is_nan y  fcompare_double x y = ccode.Gt"
  by (rule exI[where x="λx y. if is_nan x then if is_nan y then 0 else -1
    else if is_nan y then 1 else (case fcompare_double x y of ccode.Eq  0 | ccode.Lt  -1 | ccode.Gt  1)"],
        transfer, auto simp: fcompare_def)

lemmas compare_double_simps = compare_double_less compare_double_eq compare_double_greater

lemma compare_double_le_0: "compare_double x y  0 
  is_nan x  fcompare_double x y  {ccode.Eq, ccode.Lt}"
  by (rule linorder_cases[of "compare_double x y" 0]; simp)
    (auto simp: compare_double_simps nan_fcompare_double)

lift_definition double_of_integer :: "integer  double" is
  "λx. zerosign 0 (intround To_nearest (int_of_integer x))" .

definition double_of_int where [code del]: "double_of_int x = double_of_integer (integer_of_int x)"

lemma [code]: "double_of_int (int_of_integer x) = double_of_integer x"
  unfolding double_of_int_def by simp

lift_definition integer_of_double :: "double  integer" is
  "λx. if IEEE.is_nan x  IEEE.is_infinity x then undefined
     else integer_of_int valof (intround float_To_zero (valof x) :: (11, 52) float)"
  by auto

definition int_of_double: "int_of_double x = int_of_integer (integer_of_double x)"


subsection ‹Linear ordering›

definition lcompare_double :: "double  double  integer" where
  "lcompare_double x y = (if is_zero x  is_zero y then
      compare_double (copysign_double 1 x) (copysign_double 1 y)
    else compare_double x y)"

lemma fcompare_double_swap: "fcompare_double x y = ccode.Gt  fcompare_double y x = ccode.Lt"
  by transfer (auto simp: fcompare_def)

lemma fcompare_double_refl: "¬ is_nan x  fcompare_double x x = ccode.Eq"
  by transfer (auto simp: fcompare_def)

lemma fcompare_double_Eq1: "fcompare_double x y = ccode.Eq  fcompare_double y z = c  fcompare_double x z = c"
  by transfer (auto simp: fcompare_def split: if_splits)

lemma fcompare_double_Eq2: "fcompare_double y z = ccode.Eq  fcompare_double x y = c  fcompare_double x z = c"
  by transfer (auto simp: fcompare_def split: if_splits)

lemma fcompare_double_Lt_trans: "fcompare_double x y = ccode.Lt  fcompare_double y z = ccode.Lt  fcompare_double x z = ccode.Lt"
  by transfer (auto simp: fcompare_def split: if_splits)

lemma fcompare_double_eq: "¬ is_zero x  ¬ is_zero y  fcompare_double x y = ccode.Eq  x = y"
  by transfer (auto simp: fcompare_def valof_eq IEEE.is_infinity_def split: if_splits intro!: float_eqI)

lemma fcompare_double_Lt_asym: "fcompare_double x y = ccode.Lt  fcompare_double y x = ccode.Lt  False"
  by transfer (auto simp: fcompare_def split: if_splits)

lemma compare_double_swap: "0 < compare_double x y  compare_double y x < 0"
  by (auto simp: compare_double_simps fcompare_double_swap)

lemma compare_double_refl: "compare_double x x = 0"
  by (auto simp: compare_double_eq intro!: fcompare_double_refl)

lemma compare_double_trans: "compare_double x y  0  compare_double y z  0  compare_double x z  0"
  by (fastforce simp: compare_double_le_0 nan_fcompare_double
      dest: fcompare_double_Eq1 fcompare_double_Eq2 fcompare_double_Lt_trans)

lemma compare_double_antisym: "compare_double x y  0  compare_double y x  0 
  ¬ is_zero x  ¬ is_zero y  x = y"
  unfolding compare_double_le_0
  by (auto simp: nan_fcompare_double is_nan_conv
      intro: fcompare_double_eq fcompare_double_eq[symmetric]
      dest: fcompare_double_Lt_asym)

lemma zero_compare_double_copysign: "compare_double (copysign_double 1 x) (copysign_double 1 y)  0 
  is_zero x  is_zero y  compare_double x y  0"
  unfolding compare_double_le_0
  by transfer (auto simp: nan_not_zero zero_fcompare split: if_splits)

lemma is_zero_double_cases: "is_zero x  (x = 0  P)  (x = -0  P)  P"
  by transfer (auto elim!: is_zero_cases)

lemma copysign_1_0[simp]: "copysign_double 1 0 = 1" "copysign_double 1 (-0) = -1"
  by (transfer, simp, transfer, auto)+

lemma is_zero_uminus_double[simp]: "is_zero (- x)  is_zero x"
  by transfer simp

lemma not_is_zero_one_double[simp]: "¬ is_zero 1"
  by (transfer, unfold IEEE.is_zero_def, transfer, simp)

lemma uminus_one_neq_one_double[simp]: "- 1  (1 :: double)"
  by (transfer, transfer, simp)

definition lle_double :: "double  double  bool" where
  "lle_double x y  lcompare_double x y  0"

definition lless_double :: "double  double  bool" where
  "lless_double x y  lcompare_double x y < 0"

lemma lcompare_double_ge_0: "lcompare_double x y  0  lle_double y x"
  unfolding lle_double_def lcompare_double_def
  using compare_double_swap not_less by auto

lemma lcompare_double_gt_0: "lcompare_double x y > 0  lless_double y x"
  unfolding lless_double_def lcompare_double_def
  using compare_double_swap by auto

lemma lcompare_double_eq_0: "lcompare_double x y = 0  x = y"
proof
  assume *: "lcompare_double x y = 0"
  show "x = y" proof (cases "is_zero x  is_zero y")
    case True
    with * show ?thesis
      by (fastforce simp: lcompare_double_def compare_double_simps is_nan_conv
          elim: is_zero_double_cases dest!: fcompare_double_eq[rotated])
  next
    case False
    with * show ?thesis
      by (auto simp: lcompare_double_def linorder_not_less[symmetric] compare_double_swap
          intro!: compare_double_antisym)
  qed
next
  assume "x = y"
  then show "lcompare_double x y = 0"
    by (simp add: lcompare_double_def compare_double_refl)
qed

lemmas lcompare_double_0_folds = lle_double_def[symmetric] lless_double_def[symmetric]
  lcompare_double_ge_0 lcompare_double_gt_0 lcompare_double_eq_0

interpretation double_linorder: linorder lle_double lless_double
proof
  fix x y z :: double
  show "lless_double x y  lle_double x y  ¬ lle_double y x"
    unfolding lless_double_def lle_double_def lcompare_double_def
    by (auto simp: compare_double_swap not_le)
  show "lle_double x x"
    unfolding lle_double_def lcompare_double_def
    by (auto simp: compare_double_refl)
  show "lle_double x z" if "lle_double x y" and "lle_double y z"
    using that
    by (auto 0 3 simp: lle_double_def lcompare_double_def not_le compare_double_swap
        split: if_splits dest: compare_double_trans zero_compare_double_copysign
        zero_compare_double_copysign[OF less_imp_le] compare_double_antisym)
  show "x = y" if "lle_double x y" and "lle_double y x"
  proof (cases "is_zero x  is_zero y")
    case True
    with that show ?thesis
      by (auto 0 3 simp: lle_double_def lcompare_double_def elim: is_zero_double_cases
          dest!: compare_double_antisym)
  next
    case False
    with that show ?thesis
      by (auto simp: lle_double_def lcompare_double_def elim!: compare_double_antisym)
  qed
  show "lle_double x y  lle_double y x"
    unfolding lle_double_def lcompare_double_def
    by (auto simp: compare_double_swap not_le)
qed

instantiation double :: equal
begin

definition equal_double :: "double  double  bool" where
  "equal_double x y  lcompare_double x y = 0"

instance by intro_classes (simp add: equal_double_def lcompare_double_eq_0)

end

derive (eq) ceq double

definition comparator_double :: "double comparator" where
  "comparator_double x y = (let c = lcompare_double x y in
    if c = 0 then order.Eq else if c < 0 then order.Lt else order.Gt)"

lemma comparator_double: "comparator comparator_double"
  unfolding comparator_double_def
  by (auto simp: lcompare_double_0_folds split: if_splits intro!: comparator.intro)

local_setup Comparator_Generator.register_foreign_comparator @{typ double}
    @{term comparator_double}
    @{thm comparator_double}

derive ccompare double


subsubsection ‹Code setup›

declare [[code drop:
      "0 :: double"
      "1 :: double"
      "plus :: double  _"
      "minus :: double  _"
      "uminus :: double  _"
      "times :: double  _"
      "less_eq :: double  _"
      "less :: double  _"
      "divide :: double  _"
      sqrt_double infinity nan is_zero is_infinite is_nan copysign_double fcompare_double
      double_of_integer integer_of_double
      ]]

code_printing
  code_module FloatUtil  (OCaml)
‹module FloatUtil : sig
  val iszero : float -> bool
  val isinfinite : float -> bool
  val isnan : float -> bool
  val copysign : float -> float -> float
  val compare : float -> float -> Z.t
end = struct
  let iszero x = (Pervasives.classify_float x = Pervasives.FP_zero);;
  let isinfinite x = (Pervasives.classify_float x = Pervasives.FP_infinite);;
  let isnan x = (Pervasives.classify_float x = Pervasives.FP_nan);;
  let copysign x y = if isnan y then Pervasives.nan else Pervasives.copysign x y;;
  let compare x y = Z.of_int (Pervasives.compare x y);;
end;;›

code_reserved OCaml Pervasives FloatUtil

code_printing
  type_constructor double  (OCaml) "float"
  | constant "uminus :: double  double"  (OCaml) "Pervasives.(~-.)"
  | constant "(+) :: double  double  double"  (OCaml) "Pervasives.(+.)"
  | constant "(*) :: double  double  double"  (OCaml) "Pervasives.( *. )"
  | constant "(/) :: double  double  double"  (OCaml) "Pervasives.('/.)"
  | constant "(-) :: double  double  double"  (OCaml) "Pervasives.(-.)"
  | constant "0 :: double"  (OCaml) "0.0"
  | constant "1 :: double"  (OCaml) "1.0"
  | constant "(≤) :: double  double  bool"  (OCaml) "Pervasives.(<=)"
  | constant "(<) :: double  double  bool"  (OCaml) "Pervasives.(<)"
  | constant "sqrt_double :: double  double"  (OCaml) "Pervasives.sqrt"
  | constant "infinity :: double"  (OCaml) "Pervasives.infinity"
  | constant "nan :: double"  (OCaml) "Pervasives.nan"
  | constant "is_zero :: double  bool"  (OCaml) "FloatUtil.iszero"
  | constant "is_infinite :: double  bool"  (OCaml) "FloatUtil.isinfinite"
  | constant "is_nan :: double  bool"  (OCaml) "FloatUtil.isnan"
  | constant "copysign_double :: double  double  double"  (OCaml) "FloatUtil.copysign"
  | constant "compare_double :: double  double  integer"  (OCaml) "FloatUtil.compare"
  | constant "double_of_integer :: integer  double"  (OCaml) "Z.to'_float"
  | constant "integer_of_double :: double  integer"  (OCaml) "Z.of'_float"

hide_const (open) fcompare_double

(*<*)
end
(*>*)

Theory Event_Data

(*<*)
theory Event_Data
  imports
    "HOL-Library.Char_ord"
    Code_Double
    Deriving.Derive
begin
(*>*)

section ‹Event parameters›

definition div_to_zero :: "integer  integer  integer" where
  "div_to_zero x y = (let z = fst (Code_Numeral.divmod_abs x y) in
    if (x < 0)  (y < 0) then - z else z)"

definition mod_to_zero :: "integer  integer  integer" where
  "mod_to_zero x y = (let z = snd (Code_Numeral.divmod_abs x y) in
    if x < 0 then - z else z)"

lemma "b  0  div_to_zero a b * b + mod_to_zero a b = a"
  unfolding div_to_zero_def mod_to_zero_def Let_def
  by (auto simp: minus_mod_eq_mult_div[symmetric] div_minus_right mod_minus_right ac_simps)


datatype event_data = EInt integer | EFloat double | EString String.literal

derive (eq) ceq event_data
derive ccompare event_data

instantiation event_data :: "{ord, plus, minus, uminus, times, divide, modulo}"
begin

fun less_eq_event_data where
  "EInt x  EInt y  x  y"
| "EInt x  EFloat y  double_of_integer x  y"
| "EInt _  EString _  False"
| "EFloat x  EInt y  x  double_of_integer y"
| "EFloat x  EFloat y  x  y"
| "EFloat _  EString _  False"
| "EString x  EString y  lexordp_eq (String.explode x) (String.explode y)"
| "EString _  _  False"

definition less_event_data :: "event_data  event_data  bool"  where
  "less_event_data x y  x  y  ¬ y  x"

fun plus_event_data where
  "EInt x + EInt y = EInt (x + y)"
| "EInt x + EFloat y = EFloat (double_of_integer x + y)"
| "EFloat x + EInt y = EFloat (x + double_of_integer y)"
| "EFloat x + EFloat y = EFloat (x + y)"
| "(_::event_data) + _ = EFloat nan"

fun minus_event_data where
  "EInt x - EInt y = EInt (x - y)"
| "EInt x - EFloat y = EFloat (double_of_integer x - y)"
| "EFloat x - EInt y = EFloat (x - double_of_integer y)"
| "EFloat x - EFloat y = EFloat (x - y)"
| "(_::event_data) - _ = EFloat nan"

fun uminus_event_data where
  "- EInt x = EInt (- x)"
| "- EFloat x = EFloat (- x)"
| "- (_::event_data) = EFloat nan"

fun times_event_data where
  "EInt x * EInt y = EInt (x * y)"
| "EInt x * EFloat y = EFloat (double_of_integer x * y)"
| "EFloat x * EInt y = EFloat (x * double_of_integer y)"
| "EFloat x * EFloat y = EFloat (x * y)"
| "(_::event_data) * _ = EFloat nan"

fun divide_event_data where
  "EInt x div EInt y = EInt (div_to_zero x y)"
| "EInt x div EFloat y = EFloat (double_of_integer x div y)"
| "EFloat x div EInt y = EFloat (x div double_of_integer y)"
| "EFloat x div EFloat y = EFloat (x div y)"
| "(_::event_data) div _ = EFloat nan"

fun modulo_event_data where
  "EInt x mod EInt y = EInt (mod_to_zero x y)"
| "(_::event_data) mod _ = EFloat nan"

instance ..

end

primrec integer_of_event_data :: "event_data  integer" where
  "integer_of_event_data (EInt x) = x"
| "integer_of_event_data (EFloat x) = integer_of_double x"
| "integer_of_event_data (EString _) = 0"

primrec double_of_event_data :: "event_data  double" where
  "double_of_event_data (EInt x) = double_of_integer x"
| "double_of_event_data (EFloat x) = x"
| "double_of_event_data (EString _) = nan"

(*<*)
end
(*>*)

Theory Regex

(*<*)
theory Regex
  imports
    "MFOTL_Monitor.Trace"
    "HOL-Library.Lattice_Syntax"
    "HOL-Library.Extended_Nat"
begin
(*>*)

section ‹Regular expressions›

context begin

qualified datatype (atms: 'a) regex = Skip nat | Test 'a
  | Plus "'a regex" "'a regex" | Times "'a regex" "'a regex"  | Star "'a regex"

lemma finite_atms[simp]: "finite (atms r)"
  by (induct r) auto

definition "Wild = Skip 1"

lemma size_regex_estimation[termination_simp]: "x  atms r  y < f x  y < size_regex f r"
  by (induct r) auto

lemma size_regex_estimation'[termination_simp]: "x  atms r  y  f x  y  size_regex f r"
  by (induct r) auto

qualified definition "TimesL r S = Times r ` S"
qualified definition "TimesR R s = (λr. Times r s) ` R"

qualified primrec fv_regex where
  "fv_regex fv (Skip n) = {}"
| "fv_regex fv (Test φ) = fv φ"
| "fv_regex fv (Plus r s) = fv_regex fv r  fv_regex fv s"
| "fv_regex fv (Times r s) = fv_regex fv r  fv_regex fv s"
| "fv_regex fv (Star r) = fv_regex fv r"

lemma fv_regex_cong[fundef_cong]:
  "r = r'  (z. z  atms r  fv z = fv' z)  fv_regex fv r = fv_regex fv' r'"
  by (induct r arbitrary: r') auto

lemma finite_fv_regex[simp]: "(z. z  atms r  finite (fv z))  finite (fv_regex fv r)"
  by (induct r) auto

lemma fv_regex_commute:
  "(z. z  atms r  x  fv z  g x  fv' z)  x  fv_regex fv r  g x  fv_regex fv' r"
  by (induct r) auto

lemma fv_regex_alt: "fv_regex fv r = (z  atms r. fv z)"
  by (induct r) auto

qualified definition nfv_regex where
  "nfv_regex fv r = Max (insert 0 (Suc ` fv_regex fv r))"

lemma insert_Un: "insert x (A  B) = insert x A  insert x B"
  by auto

lemma nfv_regex_simps[simp]:
  assumes [simp]: "(z. z  atms r  finite (fv z))" "(z. z  atms s  finite (fv z))"
  shows
  "nfv_regex fv (Skip n) = 0"
  "nfv_regex fv (Test φ) = Max (insert 0 (Suc ` fv φ))"
  "nfv_regex fv (Plus r s) = max (nfv_regex fv r) (nfv_regex fv s)"
  "nfv_regex fv (Times r s) = max (nfv_regex fv r) (nfv_regex fv s)"
  "nfv_regex fv (Star r) = nfv_regex fv r"
  unfolding nfv_regex_def
  by (auto simp add: image_Un Max_Un insert_Un simp del: Un_insert_right Un_insert_left)

abbreviation "min_regex_default f r j  (if atms r = {} then j else Min ((λz. f z j) ` atms r))"

qualified primrec match :: "(nat  'a  bool)  'a regex  nat  nat  bool" where
  "match test (Skip n) = (λi j. j = i + n)"
| "match test (Test φ) = (λi j. i = j  test i φ)"
| "match test (Plus r s) = match test r  match test s"
| "match test (Times r s) = match test r OO match test s"
| "match test (Star r) = (match test r)**"

lemma match_cong[fundef_cong]:
  "r = r'  (i z. z  atms r  t i z = t' i z)  match t r = match t' r'"
  by (induct r arbitrary: r') auto

qualified primrec eps where
  "eps test i (Skip n) = (n = 0)"
| "eps test i (Test φ) = test i φ"
| "eps test i (Plus r s) = (eps test i r  eps test i s)"
| "eps test i (Times r s) = (eps test i r  eps test i s)"
| "eps test i (Star r) = True"

qualified primrec lpd where
  "lpd test i (Skip n) = (case n of 0  {} | Suc m  {Skip m})"
| "lpd test i (Test φ) = {}"
| "lpd test i (Plus r s) = (lpd test i r  lpd test i s)"
| "lpd test i (Times r s) = TimesR (lpd test i r) s  (if eps test i r then lpd test i s else {})"
| "lpd test i (Star r) = TimesR (lpd test i r) (Star r)"

qualified primrec lpdκ where
  "lpdκ κ test i (Skip n) = (case n of 0  {} | Suc m  {κ (Skip m)})"
| "lpdκ κ test i (Test φ) = {}"
| "lpdκ κ test i (Plus r s) = lpdκ κ test i r  lpdκ κ test i s"
| "lpdκ κ test i (Times r s) = lpdκ (λt. κ (Times t s)) test i r  (if eps test i r then lpdκ κ test i s else {})"
| "lpdκ κ test i (Star r) = lpdκ (λt. κ (Times t (Star r))) test i r"

qualified primrec rpd where
  "rpd test i (Skip n) = (case n of 0  {} | Suc m  {Skip m})"
| "rpd test i (Test φ) = {}"
| "rpd test i (Plus r s) = (rpd test i r  rpd test i s)"
| "rpd test i (Times r s) = TimesL r (rpd test i s)  (if eps test i s then rpd test i r else {})"
| "rpd test i (Star r) = TimesL (Star r) (rpd test i r)"

qualified primrec rpdκ where
  "rpdκ κ test i (Skip n) = (case n of 0  {} | Suc m  {κ (Skip m)})"
| "rpdκ κ test i (Test φ) = {}"
| "rpdκ κ test i (Plus r s) = rpdκ κ test i r  rpdκ κ test i s"
| "rpdκ κ test i (Times r s) = rpdκ (λt. κ (Times r t)) test i s  (if eps test i s then rpdκ κ test i r else {})"
| "rpdκ κ test i (Star r) = rpdκ (λt. κ (Times (Star r) t)) test i r"

lemma lpdκ_lpd: "lpdκ κ test i r = κ ` lpd test i r"
  by (induct r arbitrary: κ) (auto simp: TimesR_def split: nat.splits)

lemma rpdκ_rpd: "rpdκ κ test i r = κ ` rpd test i r"
  by (induct r arbitrary: κ) (auto simp: TimesL_def split: nat.splits)

lemma match_le: "match test r i j  i  j"
proof (induction r arbitrary: i j)
  case (Times r s)
  then show ?case using order.trans by fastforce
next
  case (Star r)
  from Star.prems show ?case
    unfolding match.simps by (induct i j rule: rtranclp.induct) (force dest: Star.IH)+
qed auto

lemma match_rtranclp_le: "(match test r)** i j  i  j"
  by (metis match.simps(5) match_le)

lemma eps_match: "eps test i r  match test r i i"
  by (induction r) (auto dest: antisym[OF match_le match_le])

lemma lpd_match: "i < j  match test r i j  (s  lpd test i r. match test s) (i + 1) j"
proof (induction r arbitrary: i j)
  case (Times r s)
  have "match test (Times r s) i j  (k. match test r i k  match test s k j)"
    by auto
  also have "  match test r i i  match test s i j 
    (k>i. match test r i k  match test s k j)"
    using match_le[of test r i] nat_less_le by auto
  also have "  match test r i i  (t  lpd test i s. match test t) (i + 1) j 
    (k>i. (t  lpd test i r. match test t) (i + 1) k  match test s k j)"
    using Times.IH(1) Times.IH(2)[OF Times.prems] by metis
  also have "  match test r i i  (t  lpd test i s. match test t) (i + 1) j 
    (k. (t  lpd test i r. match test t) (i + 1) k  match test s k j)"
    using Times.prems by (intro disj_cong[OF refl] iff_exI) (auto dest: match_le)
  also have "  ( (match test ` lpd test i (Times r s))) (i + 1) j"
    by (force simp: TimesL_def TimesR_def eps_match)
  finally show ?case .
next
  case (Star r)
  have "slpd test i r. (match test s OO (match test r)**) (i + 1) j" if "(match test r)** i j"
    using that Star.prems match_le[of test _ "i + 1"]
  proof (induct rule: converse_rtranclp_induct)
    case (step i k)
    then show ?case
      by (cases "i < k") (auto simp: not_less Star.IH dest: match_le)
  qed simp
  with Star.prems show ?case using match_le[of test _  "i + 1"]
    by (auto simp: TimesL_def TimesR_def Suc_le_eq Star.IH[of i]
      elim!: converse_rtranclp_into_rtranclp[rotated])
qed (auto split: nat.splits)

lemma rpd_match: "i < j  match test r i j  (s  rpd test j r. match test s) i (j - 1)"
proof (induction r arbitrary: i j)
  case (Times r s)
  have "match test (Times r s) i j  (k. match test r i k  match test s k j)"
    by auto
  also have "  match test r i j  match test s j j 
    (k<j. match test r i k  match test s k j)"
    using match_le[of test s _ j] nat_less_le by auto
  also have "  (t  rpd test j r. match test t) i (j - 1)  match test s j j  
    (k<j. match test r i k  (t  rpd test j s. match test t) k (j - 1))"
    using Times.IH(1)[OF Times.prems] Times.IH(2) by metis
  also have "  (t  rpd test j r. match test t) i (j - 1)  match test s j j  
    (k. match test r i k  (t  rpd test j s. match test t) k (j - 1))"
    using Times.prems by (intro disj_cong[OF refl] iff_exI) (auto dest: match_le)
  also have "  ( (match test ` rpd test j (Times r s))) i (j - 1)"
    by (force simp: TimesL_def TimesR_def eps_match)
  finally show ?case .
next
  case (Star r)
  have "srpd test j r. ((match test r)** OO match test s) i (j - 1)" if "(match test r)** i j"
    using that Star.prems match_le[of test _ _ "j - 1"]
  proof (induct rule: rtranclp_induct)
    case (step k j)
    then show ?case
      by (cases "k < j") (auto simp: not_less Star.IH dest: match_le)
  qed simp
  with Star.prems show ?case
    by (auto 0 3 simp: TimesL_def TimesR_def intro: Star.IH[of _ j, THEN iffD2]
      elim!: rtranclp.rtrancl_into_rtrancl dest: match_le[of test _ _ "j - 1", unfolded One_nat_def])
qed (auto split: nat.splits)

lemma lpd_fv_regex: "s  lpd test i r  fv_regex fv s  fv_regex fv r"
  by (induct r arbitrary: s) (auto simp: TimesR_def TimesL_def split: if_splits nat.splits)+

lemma rpd_fv_regex: "s  rpd test i r  fv_regex fv s  fv_regex fv r"
  by (induct r arbitrary: s) (auto simp: TimesR_def TimesL_def split: if_splits nat.splits)+

lemma match_fv_cong:
  "(i x. x  atms r  test i x = test' i x)  match test r = match test' r"
  by (induct r) auto

lemma eps_fv_cong:
  "(i x. x  atms r  test i x = test' i x)  eps test i r = eps test' i r"
  by (induct r) auto

datatype modality = Past | Futu
datatype safety = Strict | Lax

context
  fixes fv :: "'a  'b set"
  and safe :: "safety  'a  bool"
begin

qualified fun safe_regex :: "modality  safety  'a regex  bool" where
  "safe_regex m _ (Skip n) = True"
| "safe_regex m g (Test φ) = safe g φ"
| "safe_regex m g (Plus r s) = ((g = Lax  fv_regex fv r = fv_regex fv s)  safe_regex m g r  safe_regex m g s)"
| "safe_regex Futu g (Times r s) =
    ((g = Lax  fv_regex fv r  fv_regex fv s)  safe_regex Futu g s  safe_regex Futu Lax r)"
| "safe_regex Past g (Times r s) =
    ((g = Lax  fv_regex fv s  fv_regex fv r)  safe_regex Past g r  safe_regex Past Lax s)"
| "safe_regex m g (Star r) = ((g = Lax  fv_regex fv r = {})  safe_regex m g r)"

lemmas safe_regex_induct = safe_regex.induct[case_names Skip Test Plus TimesF TimesP Star]

lemma safe_cosafe:
  "(x. x  atms r  safe Strict x  safe Lax x)  safe_regex m Strict r  safe_regex m Lax r"
  by (induct r; cases m) auto

lemma safe_lpd_fv_regex_le: "safe_regex Futu Strict r  s  lpd test i r  fv_regex fv r  fv_regex fv s"
  by (induct r) (auto simp: TimesR_def split: if_splits)

lemma safe_lpd_fv_regex: "safe_regex Futu Strict r  s  lpd test i r  fv_regex fv s = fv_regex fv r"
  by (simp add: eq_iff lpd_fv_regex safe_lpd_fv_regex_le)

lemma cosafe_lpd: "safe_regex Futu Lax r  s  lpd test i r  safe_regex Futu Lax s"
proof (induct r arbitrary: s)
  case (Plus r1 r2)
  from Plus(3,4) show ?case
    by (auto elim: Plus(1,2))
next
  case (Times r1 r2)
  from Times(3,4) show ?case
    by (auto simp: TimesR_def elim: Times(1,2) split: if_splits)
qed (auto simp: TimesR_def split: nat.splits)

lemma safe_lpd: "(x  atms r. safe Strict x  safe Lax x) 
  safe_regex Futu Strict r  s  lpd test i r  safe_regex Futu Strict s"
proof (induct r arbitrary: s)
  case (Plus r1 r2)
  from Plus(3,4,5) show ?case
    by (auto elim: Plus(1,2) simp: ball_Un)
next
  case (Times r1 r2)
  from Times(3,4,5) show ?case
    by (force simp: TimesR_def ball_Un elim: Times(1,2) cosafe_lpd dest: lpd_fv_regex split: if_splits)
next
  case (Star r)
  from Star(2,3,4) show ?case
    by (force simp: TimesR_def elim: Star(1) cosafe_lpd
      dest: safe_cosafe[rotated] lpd_fv_regex[where fv=fv] split: if_splits)
qed (auto split: nat.splits)

lemma safe_rpd_fv_regex_le: "safe_regex Past Strict r  s  rpd test i r  fv_regex fv r  fv_regex fv s"
  by (induct r) (auto simp: TimesL_def split: if_splits)

lemma safe_rpd_fv_regex: "safe_regex Past Strict r  s  rpd test i r  fv_regex fv s = fv_regex fv r"
  by (simp add: eq_iff rpd_fv_regex safe_rpd_fv_regex_le)

lemma cosafe_rpd: "safe_regex Past Lax r  s  rpd test i r  safe_regex Past Lax s"
proof (induct r arbitrary: s)
  case (Plus r1 r2)
  from Plus(3,4) show ?case
    by (auto elim: Plus(1,2))
next
  case (Times r1 r2)
  from Times(3,4) show ?case
    by (auto simp: TimesL_def elim: Times(1,2) split: if_splits)
qed (auto simp: TimesL_def split: nat.splits)

lemma safe_rpd: "(x  atms r. safe Strict x  safe Lax x) 
  safe_regex Past Strict r  s  rpd test i r  safe_regex Past Strict s"
proof (induct r arbitrary: s)
  case (Plus r1 r2)
  from Plus(3,4,5) show ?case
    by (auto elim: Plus(1,2) simp: ball_Un)
next
  case (Times r1 r2)
  from Times(3,4,5) show ?case
    by (force simp: TimesL_def ball_Un elim: Times(1,2) cosafe_rpd dest: rpd_fv_regex split: if_splits)
next
  case (Star r)
  from Star(2,3,4) show ?case
    by (force simp: TimesL_def elim: Star(1) cosafe_rpd
      dest: safe_cosafe[rotated] rpd_fv_regex[where fv=fv] split: if_splits)
qed (auto split: nat.splits)

lemma safe_regex_safe: "(g r. safe g r  safe Lax r) 
  safe_regex m g r  x  atms r  safe Lax x"
  by (induct m g r rule: safe_regex.induct) auto

lemma safe_regex_map_regex:
  "(g x. x  atms r  safe g x   safe g (f x))  (x. x  atms r  fv (f x) = fv x) 
   safe_regex m g r  safe_regex m g (map_regex f r)"
  by (induct m g r rule: safe_regex.induct) (auto simp: fv_regex_alt regex.set_map)

end

lemma safe_regex_cong[fundef_cong]:
  "(g x. x  atms r  safe g x = safe' g x) 
  Regex.safe_regex fv safe m g r = Regex.safe_regex fv safe' m g r"
  by (induct m g r rule: safe_regex.induct) auto

lemma safe_regex_mono:
  "(g x. x  atms r  safe g x  safe' g x) 
  Regex.safe_regex fv safe m g r  Regex.safe_regex fv safe' m g r"
  by (induct m g r rule: safe_regex.induct) auto

lemma match_map_regex: "match t (map_regex f r) = match (λk z. t k (f z)) r"
  by (induct r) auto

lemma match_cong_strong:
  "(k z. k  {i ..< j + 1}  z  atms r  t k z = t' k z)  match t r i j = match t' r i j"
proof (induction r arbitrary: i j)
  case (Times r s)
  from Times.prems show ?case
    by (auto 0 4 simp: relcompp_apply intro: le_less_trans match_le less_Suc_eq_le
      dest: Times.IH[THEN iffD1, rotated -1] Times.IH[THEN iffD2, rotated -1] match_le)
next
  case (Star r)
  show ?case unfolding match.simps
  proof (rule iffI)
    assume *: "(match t r)** i j"
    then have "i  j" unfolding match.simps(5)[symmetric]
      by (rule match_le)
    with * show "(match t' r)** i j" using Star.prems
    proof (induction i j rule: rtranclp.induct)
      case (rtrancl_into_rtrancl a b c)
      from rtrancl_into_rtrancl(1,2,4,5) show ?case
        by (intro rtranclp.rtrancl_into_rtrancl[OF rtrancl_into_rtrancl.IH])
          (auto dest!: Star.IH[THEN iffD1, rotated -1]
            dest: match_le match_rtranclp_le simp: less_Suc_eq_le)
    qed simp
  next
    assume *: "(match t' r)** i j"
    then have "i  j" unfolding match.simps(5)[symmetric]
      by (rule match_le)
    with * show "(match t r)** i j" using Star.prems
    proof (induction i j rule: rtranclp.induct)
      case (rtrancl_into_rtrancl a b c)
      from rtrancl_into_rtrancl(1,2,4,5) show ?case
        by (intro rtranclp.rtrancl_into_rtrancl[OF rtrancl_into_rtrancl.IH])
          (auto dest!: Star.IH[THEN iffD2, rotated -1]
            dest: match_le match_rtranclp_le simp: less_Suc_eq_le)
    qed simp
  qed
qed auto

end

(*<*)
end
(*>*)

Theory Formula

(*<*)
theory Formula
  imports
    Event_Data
    Regex
    "MFOTL_Monitor.Interval"
    "MFOTL_Monitor.Trace"
    "MFOTL_Monitor.Abstract_Monitor"
    "HOL-Library.Mapping"
    Containers.Set_Impl
begin
(*>*)

section ‹Metric first-order dynamic logic›

derive (eq) ceq enat

instantiation enat :: ccompare begin
definition ccompare_enat :: "enat comparator option" where
  "ccompare_enat = Some (λx y. if x = y then order.Eq else if x < y then order.Lt else order.Gt)"

instance by intro_classes
    (auto simp: ccompare_enat_def split: if_splits intro!: comparator.intro)
end

context begin

subsection ‹Formulas and satisfiability›

qualified type_synonym name = String.literal
qualified type_synonym event = "(name × event_data list)"
qualified type_synonym database = "(name, event_data list set list) mapping"
qualified type_synonym prefix = "(name × event_data list) prefix"
qualified type_synonym trace = "(name × event_data list) trace"

qualified type_synonym env = "event_data list"

subsubsection ‹Syntax›

qualified datatype trm = is_Var: Var nat | is_Const: Const event_data
  | Plus trm trm | Minus trm trm | UMinus trm | Mult trm trm | Div trm trm | Mod trm trm
  | F2i trm | I2f trm

qualified primrec fvi_trm :: "nat  trm  nat set" where
  "fvi_trm b (Var x) = (if b  x then {x - b} else {})"
| "fvi_trm b (Const _) = {}"
| "fvi_trm b (Plus x y) = fvi_trm b x  fvi_trm b y"
| "fvi_trm b (Minus x y) = fvi_trm b x  fvi_trm b y"
| "fvi_trm b (UMinus x) = fvi_trm b x"
| "fvi_trm b (Mult x y) = fvi_trm b x  fvi_trm b y"
| "fvi_trm b (Div x y) = fvi_trm b x  fvi_trm b y"
| "fvi_trm b (Mod x y) = fvi_trm b x  fvi_trm b y"
| "fvi_trm b (F2i x) = fvi_trm b x"
| "fvi_trm b (I2f x) = fvi_trm b x"

abbreviation "fv_trm  fvi_trm 0"

qualified primrec eval_trm :: "env  trm  event_data" where
  "eval_trm v (Var x) = v ! x"
| "eval_trm v (Const x) = x"
| "eval_trm v (Plus x y) = eval_trm v x + eval_trm v y"
| "eval_trm v (Minus x y) = eval_trm v x - eval_trm v y"
| "eval_trm v (UMinus x) = - eval_trm v x"
| "eval_trm v (Mult x y) = eval_trm v x * eval_trm v y"
| "eval_trm v (Div x y) = eval_trm v x div eval_trm v y"
| "eval_trm v (Mod x y) = eval_trm v x mod eval_trm v y"
| "eval_trm v (F2i x) = EInt (integer_of_event_data (eval_trm v x))"
| "eval_trm v (I2f x) = EFloat (double_of_event_data (eval_trm v x))"

lemma eval_trm_fv_cong: "xfv_trm t. v ! x = v' ! x  eval_trm v t = eval_trm v' t"
  by (induction t) simp_all


qualified datatype agg_type = Agg_Cnt | Agg_Min | Agg_Max | Agg_Sum | Agg_Avg | Agg_Med
qualified type_synonym agg_op = "agg_type × event_data"

definition flatten_multiset :: "(event_data × enat) set  event_data list" where
  "flatten_multiset M = concat (map (λ(x, c). replicate (the_enat c) x) (csorted_list_of_set M))"

fun eval_agg_op :: "agg_op  (event_data × enat) set  event_data" where
  "eval_agg_op (Agg_Cnt, y0) M = EInt (integer_of_int (length (flatten_multiset M)))"
| "eval_agg_op (Agg_Min, y0) M = (case flatten_multiset M of
      []  y0
    | x # xs  foldl min x xs)"
| "eval_agg_op (Agg_Max, y0) M = (case flatten_multiset M of
      []  y0
    | x # xs  foldl max x xs)"
| "eval_agg_op (Agg_Sum, y0) M = foldl plus y0 (flatten_multiset M)"
| "eval_agg_op (Agg_Avg, y0) M = EFloat (let xs = flatten_multiset M in case xs of
      []  0
    | _  double_of_event_data (foldl plus (EInt 0) xs) / double_of_int (length xs))"
| "eval_agg_op (Agg_Med, y0) M = EFloat (let xs = flatten_multiset M; u = length xs in
    if u = 0 then 0 else
      let u' = u div 2 in
      if even u then
        (double_of_event_data (xs ! (u'-1)) + double_of_event_data (xs ! u') / double_of_int 2)
      else double_of_event_data (xs ! u'))"

qualified datatype (discs_sels) formula = Pred name "trm list"
  | Let name formula formula
  | Eq trm trm | Less trm trm | LessEq trm trm
  | Neg formula | Or formula formula | And formula formula | Ands "formula list" | Exists formula
  | Agg nat agg_op nat trm formula
  | Prev  formula | Next  formula
  | Since formula  formula | Until formula  formula
  | MatchF  "formula Regex.regex" | MatchP  "formula Regex.regex"

qualified definition "FF = Exists (Neg (Eq (Var 0) (Var 0)))"
qualified definition "TT  Neg FF"

qualified fun fvi :: "nat  formula  nat set" where
  "fvi b (Pred r ts) = (tset ts. fvi_trm b t)"
| "fvi b (Let p φ ψ) = fvi b ψ"
| "fvi b (Eq t1 t2) = fvi_trm b t1  fvi_trm b t2"
| "fvi b (Less t1 t2) = fvi_trm b t1  fvi_trm b t2"
| "fvi b (LessEq t1 t2) = fvi_trm b t1  fvi_trm b t2"
| "fvi b (Neg φ) = fvi b φ"
| "fvi b (Or φ ψ) = fvi b φ  fvi b ψ"
| "fvi b (And φ ψ) = fvi b φ  fvi b ψ"
| "fvi b (Ands φs) = (let xs = map (fvi b) φs in xset xs. x)"
| "fvi b (Exists φ) = fvi (Suc b) φ"
| "fvi b (Agg y ω b' f φ) = fvi (b + b') φ  fvi_trm (b + b') f  (if b  y then {y - b} else {})"
| "fvi b (Prev I φ) = fvi b φ"
| "fvi b (Next I φ) = fvi b φ"
| "fvi b (Since φ I ψ) = fvi b φ  fvi b ψ"
| "fvi b (Until φ I ψ) = fvi b φ  fvi b ψ"
| "fvi b (MatchF I r) = Regex.fv_regex (fvi b) r"
| "fvi b (MatchP I r) = Regex.fv_regex (fvi b) r"

abbreviation "fv  fvi 0"
abbreviation "fv_regex  Regex.fv_regex fv"

lemma fv_abbrevs[simp]: "fv TT = {}" "fv FF = {}"
  unfolding TT_def FF_def by auto

lemma fv_subset_Ands: "φ  set φs  fv φ  fv (Ands φs)"
  by auto

lemma finite_fvi_trm[simp]: "finite (fvi_trm b t)"
  by (induction t) simp_all

lemma finite_fvi[simp]: "finite (fvi b φ)"
  by (induction φ arbitrary: b) simp_all

lemma fvi_trm_plus: "x  fvi_trm (b + c) t  x + c  fvi_trm b t"
  by (induction t) auto

lemma fvi_trm_iff_fv_trm: "x  fvi_trm b t  x + b  fv_trm t"
  using fvi_trm_plus[where b=0 and c=b] by simp_all

lemma fvi_plus: "x  fvi (b + c) φ  x + c  fvi b φ"
proof (induction φ arbitrary: b rule: formula.induct)
  case (Exists φ)
  then show ?case by force
next
  case (Agg y ω b' f φ)
  have *: "b + c + b' = b + b' + c" by simp
  from Agg show ?case by (force simp: * fvi_trm_plus)
qed (auto simp add: fvi_trm_plus fv_regex_commute[where g = "λx. x + c"])

lemma fvi_Suc: "x  fvi (Suc b) φ  Suc x  fvi b φ"
  using fvi_plus[where c=1] by simp

lemma fvi_plus_bound:
  assumes "ifvi (b + c) φ. i < n"
  shows "ifvi b φ. i < c + n"
proof
  fix i
  assume "i  fvi b φ"
  show "i < c + n"
  proof (cases "i < c")
    case True
    then show ?thesis by simp
  next
    case False
    then obtain i' where "i = i' + c"
      using nat_le_iff_add by (auto simp: not_less)
    with assms i  fvi b φ show ?thesis by (simp add: fvi_plus)
  qed
qed

lemma fvi_Suc_bound:
  assumes "ifvi (Suc b) φ. i < n"
  shows "ifvi b φ. i < Suc n"
  using assms fvi_plus_bound[where c=1] by simp

lemma fvi_iff_fv: "x  fvi b φ  x + b  fv φ"
  using fvi_plus[where b=0 and c=b] by simp_all

qualified definition nfv :: "formula  nat" where
  "nfv φ = Max (insert 0 (Suc ` fv φ))"

qualified abbreviation nfv_regex where
  "nfv_regex  Regex.nfv_regex fv"

qualified definition envs :: "formula  env set" where
  "envs φ = {v. length v = nfv φ}"

lemma nfv_simps[simp]:
  "nfv (Let p φ ψ) = nfv ψ"
  "nfv (Neg φ) = nfv φ"
  "nfv (Or φ ψ) = max (nfv φ) (nfv ψ)"
  "nfv (And φ ψ) = max (nfv φ) (nfv ψ)"
  "nfv (Prev I φ) = nfv φ"
  "nfv (Next I φ) = nfv φ"
  "nfv (Since φ I ψ) = max (nfv φ) (nfv ψ)"
  "nfv (Until φ I ψ) = max (nfv φ) (nfv ψ)"
  "nfv (MatchP I r) = Regex.nfv_regex fv r"
  "nfv (MatchF I r) = Regex.nfv_regex fv r"
  "nfv_regex (Regex.Skip n) = 0"
  "nfv_regex (Regex.Test φ) = Max (insert 0 (Suc ` fv φ))"
  "nfv_regex (Regex.Plus r s) = max (nfv_regex r) (nfv_regex s)"
  "nfv_regex (Regex.Times r s) = max (nfv_regex r) (nfv_regex s)"
  "nfv_regex (Regex.Star r) = nfv_regex r"
  unfolding nfv_def Regex.nfv_regex_def by (simp_all add: image_Un Max_Un[symmetric])

lemma nfv_Ands[simp]: "nfv (Ands l) = Max (insert 0 (nfv ` set l))"
proof (induction l)
  case Nil
  then show ?case unfolding nfv_def by simp
next
  case (Cons a l)
  have "fv (Ands (a # l)) = fv a  fv (Ands l)" by simp
  then have "nfv (Ands (a # l)) = max (nfv a) (nfv (Ands l))"
    unfolding nfv_def
    by (auto simp: image_Un Max.union[symmetric])
  with Cons.IH show ?case
    by (cases l) auto
qed

lemma fvi_less_nfv: "ifv φ. i < nfv φ"
  unfolding nfv_def
  by (auto simp add: Max_gr_iff intro: max.strict_coboundedI2)

lemma fvi_less_nfv_regex: "ifv_regex φ. i < nfv_regex φ"
  unfolding Regex.nfv_regex_def
  by (auto simp add: Max_gr_iff intro: max.strict_coboundedI2)

subsubsection ‹Future reach›

qualified fun future_bounded :: "formula  bool" where
  "future_bounded (Pred _ _) = True"
| "future_bounded (Let p φ ψ) = (future_bounded φ  future_bounded ψ)"
| "future_bounded (Eq _ _) = True"
| "future_bounded (Less _ _) = True"
| "future_bounded (LessEq _ _) = True"
| "future_bounded (Neg φ) = future_bounded φ"
| "future_bounded (Or φ ψ) = (future_bounded φ  future_bounded ψ)"
| "future_bounded (And φ ψ) = (future_bounded φ  future_bounded ψ)"
| "future_bounded (Ands l) = list_all future_bounded l"
| "future_bounded (Exists φ) = future_bounded φ"
| "future_bounded (Agg y ω b f φ) = future_bounded φ"
| "future_bounded (Prev I φ) = future_bounded φ"
| "future_bounded (Next I φ) = future_bounded φ"
| "future_bounded (Since φ I ψ) = (future_bounded φ  future_bounded ψ)"
| "future_bounded (Until φ I ψ) = (future_bounded φ  future_bounded ψ  right I  )"
| "future_bounded (MatchP I r) = Regex.pred_regex future_bounded r"
| "future_bounded (MatchF I r) = (Regex.pred_regex future_bounded r  right I  )"


subsubsection ‹Semantics›

definition "ecard A = (if finite A then card A else )"

qualified fun sat :: "trace  (name  nat  event_data list set)  env  nat  formula  bool" where
  "sat σ V v i (Pred r ts) = (case V r of
       None  (r, map (eval_trm v) ts)  Γ σ i
     | Some X  map (eval_trm v) ts  X i)"
| "sat σ V v i (Let p φ ψ) =
    sat σ (V(p  λi. {v. length v = nfv φ  sat σ V v i φ})) v i ψ"
| "sat σ V v i (Eq t1 t2) = (eval_trm v t1 = eval_trm v t2)"
| "sat σ V v i (Less t1 t2) = (eval_trm v t1 < eval_trm v t2)"
| "sat σ V v i (LessEq t1 t2) = (eval_trm v t1  eval_trm v t2)"
| "sat σ V v i (Neg φ) = (¬ sat σ V v i φ)"
| "sat σ V v i (Or φ ψ) = (sat σ V v i φ  sat σ V v i ψ)"
| "sat σ V v i (And φ ψ) = (sat σ V v i φ  sat σ V v i ψ)"
| "sat σ V v i (Ands l) = (φ  set l. sat σ V v i φ)"
| "sat σ V v i (Exists φ) = (z. sat σ V (z # v) i φ)"
| "sat σ V v i (Agg y ω b f φ) =
    (let M = {(x, ecard Zs) | x Zs. Zs = {zs. length zs = b  sat σ V (zs @ v) i φ  eval_trm (zs @ v) f = x}  Zs  {}}
    in (M = {}  fv φ  {0..<b})  v ! y = eval_agg_op ω M)"
| "sat σ V v i (Prev I φ) = (case i of 0  False | Suc j  mem (τ σ i - τ σ j) I  sat σ V v j φ)"
| "sat σ V v i (Next I φ) = (mem (τ σ (Suc i) - τ σ i) I  sat σ V v (Suc i) φ)"
| "sat σ V v i (Since φ I ψ) = (ji. mem (τ σ i - τ σ j) I  sat σ V v j ψ  (k  {j <.. i}. sat σ V v k φ))"
| "sat σ V v i (Until φ I ψ) = (ji. mem (τ σ j - τ σ i) I  sat σ V v j ψ  (k  {i ..< j}. sat σ V v k φ))"
| "sat σ V v i (MatchP I r) = (ji. mem (τ σ i - τ σ j) I  Regex.match (sat σ V v) r j i)"
| "sat σ V v i (MatchF I r) = (ji. mem (τ σ j - τ σ i) I  Regex.match (sat σ V v) r i j)"

lemma sat_abbrevs[simp]:
  "sat σ V v i TT" "¬ sat σ V v i FF"
  unfolding TT_def FF_def by auto

lemma sat_Ands: "sat σ V v i (Ands l)  (φset l. sat σ V v i φ)"
  by (simp add: list_all_iff)

lemma sat_Until_rec: "sat σ V v i (Until φ I ψ) 
  mem 0 I  sat σ V v i ψ 
  (Δ σ (i + 1)  right I  sat σ V v i φ  sat σ V v (i + 1) (Until φ (subtract (Δ σ (i + 1)) I) ψ))"
  (is "?L  ?R")
proof (rule iffI; (elim disjE conjE)?)
  assume ?L
  then obtain j where j: "i  j" "mem (τ σ j - τ σ i) I" "sat σ V v j ψ" "k  {i ..< j}. sat σ V v k φ"
    by auto
  then show ?R
  proof (cases "i = j")
    case False
    with j(1,2) have σ (i + 1)  right I"
      by (auto elim: order_trans[rotated] simp: diff_le_mono)
    moreover from False j(1,4) have "sat σ V v i φ" by auto
    moreover from False j have "sat σ V v (i + 1) (Until φ (subtract (Δ σ (i + 1)) I) ψ)"
      by (cases "right I") (auto simp: le_diff_conv le_diff_conv2 intro!: exI[of _ j])
    ultimately show ?thesis by blast
  qed simp
next
  assume Δ: σ (i + 1)  right I" and now: "sat σ V v i φ" and
   "next": "sat σ V v (i + 1) (Until φ (subtract (Δ σ (i + 1)) I) ψ)"
  from "next" obtain j where j: "i + 1  j" "mem (τ σ j - τ σ (i + 1)) ((subtract (Δ σ (i + 1)) I))"
      "sat σ V v j ψ" "k  {i + 1 ..< j}. sat σ V v k φ"
    by auto
  from Δ j(1,2) have "mem (τ σ j - τ σ i) I"
    by (cases "right I") (auto simp: le_diff_conv2)
  with now j(1,3,4) show ?L by (auto simp: le_eq_less_or_eq[of i] intro!: exI[of _ j])
qed auto

lemma sat_Since_rec: "sat σ V v i (Since φ I ψ) 
  mem 0 I  sat σ V v i ψ 
  (i > 0  Δ σ i  right I  sat σ V v i φ  sat σ V v (i - 1) (Since φ (subtract (Δ σ i) I) ψ))"
  (is "?L  ?R")
proof (rule iffI; (elim disjE conjE)?)
  assume ?L
  then obtain j where j: "j  i" "mem (τ σ i - τ σ j) I" "sat σ V v j ψ" "k  {j <.. i}. sat σ V v k φ"
    by auto
  then show ?R
  proof (cases "i = j")
    case False
    with j(1) obtain k where [simp]: "i = k + 1"
      by (cases i) auto
    with j(1,2) False have σ i  right I"
      by (auto elim: order_trans[rotated] simp: diff_le_mono2 le_Suc_eq)
    moreover from False j(1,4) have "sat σ V v i φ" by auto
    moreover from False j have "sat σ V v (i - 1) (Since φ (subtract (Δ σ i) I) ψ)"
      by (cases "right I") (auto simp: le_diff_conv le_diff_conv2 intro!: exI[of _ j])
    ultimately show ?thesis by auto
  qed simp
next
  assume i: "0 < i" and Δ: σ i  right I" and now: "sat σ V v i φ" and
   "prev": "sat σ V v (i - 1) (Since φ (subtract (Δ σ i) I) ψ)"
  from "prev" obtain j where j: "j  i - 1" "mem (τ σ (i - 1) - τ σ j) ((subtract (Δ σ i) I))"
      "sat σ V v j ψ" "k  {j <.. i - 1}. sat σ V v k φ"
    by auto
  from Δ i j(1,2) have "mem (τ σ i - τ σ j) I"
    by (cases "right I") (auto simp: le_diff_conv2)
  with now i j(1,3,4) show ?L by (auto simp: le_Suc_eq gr0_conv_Suc intro!: exI[of _ j])
qed auto

lemma sat_MatchF_rec: "sat σ V v i (MatchF I r)  mem 0 I  Regex.eps (sat σ V v) i r 
  Δ σ (i + 1)  right I  (s  Regex.lpd (sat σ V v) i r. sat σ V v (i + 1) (MatchF (subtract (Δ σ (i + 1)) I) s))"
  (is "?L  ?R1  ?R2")
proof (rule iffI; (elim disjE conjE bexE)?)
  assume ?L
  then obtain j where j: "j  i" "mem (τ σ j - τ σ i) I" and "Regex.match (sat σ V v) r i j" by auto
  then show "?R1  ?R2"
  proof (cases "i < j")
    case True
    with ‹Regex.match (sat σ V v) r i j lpd_match[of i j "sat σ V v" r]
    obtain s where "s  Regex.lpd (sat σ V v) i r" "Regex.match (sat σ V v) s (i + 1) j" by auto
    with True j have ?R2
      by (cases "right I")
        (auto simp: le_diff_conv le_diff_conv2 intro!: exI[of _ j] elim: le_trans[rotated])
    then show ?thesis by blast
  qed (auto simp: eps_match)
next
  assume "enat (Δ σ (i + 1))  right I"
  moreover
  fix s
  assume [simp]: "s  Regex.lpd (sat σ V v) i r" and "sat σ V v (i + 1) (MatchF (subtract (Δ σ (i + 1)) I) s)"
  then obtain j where "j > i" "Regex.match (sat σ V v) s (i + 1) j"
    "mem (τ σ j - τ σ (Suc i)) (subtract (Δ σ (i + 1)) I)" by (auto simp: Suc_le_eq)
  ultimately show ?L
    by (cases "right I")
      (auto simp: le_diff_conv lpd_match intro!: exI[of _ j] bexI[of _ s])
qed (auto simp: eps_match intro!: exI[of _ i])

lemma sat_MatchP_rec: "sat σ V v i (MatchP I r)  mem 0 I  Regex.eps (sat σ V v) i r 
  i > 0  Δ σ i  right I  (s  Regex.rpd (sat σ V v) i r. sat σ V v (i - 1) (MatchP (subtract (Δ σ i) I) s))"
  (is "?L  ?R1  ?R2")
proof (rule iffI; (elim disjE conjE bexE)?)
  assume ?L
  then obtain j where j: "j  i" "mem (τ σ i - τ σ j) I" and "Regex.match (sat σ V v) r j i" by auto
  then show "?R1  ?R2"
  proof (cases "j < i")
    case True
    with ‹Regex.match (sat σ V v) r j i rpd_match[of j i "sat σ V v" r]
    obtain s where "s  Regex.rpd (sat σ V v) i r" "Regex.match (sat σ V v) s j (i - 1)" by auto
    with True j have ?R2
      by (cases "right I")
        (auto simp: le_diff_conv le_diff_conv2 intro!: exI[of _ j] elim: le_trans)
    then show ?thesis by blast
  qed (auto simp: eps_match)
next
  assume "enat (Δ σ i)  right I"
  moreover
  fix s
  assume [simp]: "s  Regex.rpd (sat σ V v) i r" and "sat σ V v (i - 1) (MatchP (subtract (Δ σ i) I) s)" "i > 0"
  then obtain j where "j < i" "Regex.match (sat σ V v) s j (i - 1)"
    "mem (τ σ (i - 1) - τ σ j) (subtract (Δ σ i) I)" by (auto simp: gr0_conv_Suc less_Suc_eq_le)
  ultimately show ?L
    by (cases "right I")
      (auto simp: le_diff_conv rpd_match intro!: exI[of _ j] bexI[of _ s])
qed (auto simp: eps_match intro!: exI[of _ i])

lemma sat_Since_0: "sat σ V v 0 (Since φ I ψ)  mem 0 I  sat σ V v 0 ψ"
  by auto

lemma sat_MatchP_0: "sat σ V v 0 (MatchP I r)  mem 0 I  Regex.eps (sat σ V v) 0 r"
  by (auto simp: eps_match)

lemma sat_Since_point: "sat σ V v i (Since φ I ψ) 
    (j. j  i  mem (τ σ i - τ σ j) I  sat σ V v i (Since φ (point (τ σ i - τ σ j)) ψ)  P)  P"
  by (auto intro: diff_le_self)

lemma sat_MatchP_point: "sat σ V v i (MatchP I r) 
    (j. j  i  mem (τ σ i - τ σ j) I  sat σ V v i (MatchP (point (τ σ i - τ σ j)) r)  P)  P"
  by (auto intro: diff_le_self)

lemma sat_Since_pointD: "sat σ V v i (Since φ (point t) ψ)  mem t I  sat σ V v i (Since φ I ψ)"
  by auto

lemma sat_MatchP_pointD: "sat σ V v i (MatchP (point t) r)  mem t I  sat σ V v i (MatchP I r)"
  by auto

lemma sat_fv_cong: "xfv φ. v!x = v'!x  sat σ V v i φ = sat σ V v' i φ"
proof (induct φ arbitrary: V v v' i rule: formula.induct)
  case (Pred n ts)
  show ?case by (simp cong: map_cong eval_trm_fv_cong[OF Pred[simplified, THEN bspec]] split: option.splits)
next
  case (Let p b φ ψ)
  then show ?case
    by auto
next
  case (Eq x1 x2)
  then show ?case unfolding fvi.simps sat.simps by (metis UnCI eval_trm_fv_cong)
next
  case (Less x1 x2)
  then show ?case unfolding fvi.simps sat.simps by (metis UnCI eval_trm_fv_cong)
next
  case (LessEq x1 x2)
  then show ?case unfolding fvi.simps sat.simps by (metis UnCI eval_trm_fv_cong)
next
  case (Ands l)
  have "φ. φ  set l  sat σ V v i φ = sat σ V v' i φ"
  proof -
    fix φ assume "φ  set l"
    then have "fv φ  fv (Ands l)" using fv_subset_Ands by blast
    then have "xfv φ. v!x = v'!x" using Ands.prems by blast
    then show "sat σ V v i φ = sat σ V v' i φ" using Ands.hyps φ  set l by blast
  qed
  then show ?case using sat_Ands by blast
next
  case (Exists φ)
  then show ?case unfolding sat.simps by (intro iff_exI) (simp add: fvi_Suc nth_Cons')
next
  case (Agg y ω b f φ)
  have "v ! y = v' ! y"
    using Agg.prems by simp
  moreover have "sat σ V (zs @ v) i φ = sat σ V (zs @ v') i φ" if "length zs = b" for zs
    using that Agg.prems by (simp add: Agg.hyps[where v="zs @ v" and v'="zs @ v'"]
        nth_append fvi_iff_fv(1)[where b=b])
  moreover have "eval_trm (zs @ v) f = eval_trm (zs @ v') f" if "length zs = b" for zs
    using that Agg.prems by (auto intro!: eval_trm_fv_cong[where v="zs @ v" and v'="zs @ v'"]
        simp: nth_append fvi_iff_fv(1)[where b=b] fvi_trm_iff_fv_trm[where b="length zs"])
  ultimately show ?case
    by (simp cong: conj_cong)
next
  case (MatchF I r)
  then have "Regex.match (sat σ V v) r = Regex.match (sat σ V v') r"
    by (intro match_fv_cong) (auto simp: fv_regex_alt)
  then show ?case
    by auto
next
  case (MatchP I r)
  then have "Regex.match (sat σ V v) r = Regex.match (sat σ V v') r"
    by (intro match_fv_cong) (auto simp: fv_regex_alt)
  then show ?case
    by auto
qed (auto 10 0 split: nat.splits intro!: iff_exI)

lemma match_fv_cong:
  "xfv_regex r. v!x = v'!x  Regex.match (sat σ V v) r = Regex.match (sat σ V v') r"
  by (rule match_fv_cong, rule sat_fv_cong) (auto simp: fv_regex_alt)

lemma eps_fv_cong:
  "xfv_regex r. v!x = v'!x  Regex.eps (sat σ V v) i r = Regex.eps (sat σ V v') i r"
  unfolding eps_match by (erule match_fv_cong[THEN fun_cong, THEN fun_cong])


subsection ‹Past-only formulas›

fun past_only :: "formula  bool" where
  "past_only (Pred _ _) = True"
| "past_only (Eq _ _) = True"
| "past_only (Less _ _) = True"
| "past_only (LessEq _ _) = True"
| "past_only (Let _ α β) = (past_only α  past_only β)"
| "past_only (Neg ψ) = past_only ψ"
| "past_only (Or α β) = (past_only α  past_only β)"
| "past_only (And α β) = (past_only α  past_only β)"
| "past_only (Ands l) = (αset l. past_only α)"
| "past_only (Exists ψ) = past_only ψ"
| "past_only (Agg _ _ _ _ ψ) = past_only ψ"
| "past_only (Prev _ ψ) = past_only ψ"
| "past_only (Next _ _) = False"
| "past_only (Since α _ β) = (past_only α  past_only β)"
| "past_only (Until α _ β) = False"
| "past_only (MatchP _ r) = Regex.pred_regex past_only r"
| "past_only (MatchF _ _) = False"

lemma past_only_sat:
  assumes "prefix_of π σ" "prefix_of π σ'"
  shows "i < plen π  dom V = dom V' 
     (p i. p  dom V  i < plen π  the (V p) i = the (V' p) i) 
     past_only φ  sat σ V v i φ = sat σ' V' v i φ"
proof (induction φ arbitrary: V V' v i)
  case (Pred e ts)
  show ?case proof (cases "V e")
    case None
    then have "V' e = None" using ‹dom V = dom V' by auto
    with None Γ_prefix_conv[OF assms(1,2) Pred(1)] show ?thesis by simp
  next
    case (Some a)
    moreover obtain a' where "V' e = Some a'" using Some ‹dom V = dom V' by auto
    moreover have "the (V e) i = the (V' e) i"
      using Some Pred(1,3) by (fastforce intro: domI)
    ultimately show ?thesis by simp
  qed
next
  case (Let p φ ψ)
  let ?V = "λV σ. (V(p  λi. {v. length v = nfv φ  sat σ V v i φ}))"
  show ?case unfolding sat.simps proof (rule Let.IH(2))
    show "i < plen π" by fact
    from Let.prems show "past_only ψ" by simp
    from Let.prems show "dom (?V V σ) = dom (?V V' σ')"
      by (simp del: fun_upd_apply)
  next
    fix p' i
    assume *: "p'  dom (?V V σ)" "i < plen π"
    show "the (?V V σ p') i = the (?V V' σ' p') i" proof (cases "p' = p")
      case True
      with Let i < plen π show ?thesis by auto
    next
      case False
      with * show ?thesis by (auto intro!: Let.prems(3))
    qed
  qed
next
  case (Ands l)
  with Γ_prefix_conv[OF assms] show ?case by simp
next
  case (Prev I φ)
  with τ_prefix_conv[OF assms] show ?case by (simp split: nat.split)
next
  case (Since φ1 I φ2)
  with τ_prefix_conv[OF assms] show ?case by auto
next
  case (MatchP I r)
  then have "Regex.match (sat σ V v) r a b = Regex.match (sat σ' V' v) r a b" if "b < plen π" for a b
    using that by (intro Regex.match_cong_strong) (auto simp: regex.pred_set)
  with τ_prefix_conv[OF assms] MatchP(2) show ?case by auto
qed auto


subsection ‹Safe formulas›

fun remove_neg :: "formula  formula" where
  "remove_neg (Neg φ) = φ"
| "remove_neg φ = φ"

lemma fvi_remove_neg[simp]: "fvi b (remove_neg φ) = fvi b φ"
  by (cases φ) simp_all

lemma partition_cong[fundef_cong]:
  "xs = ys  (x. xset xs  f x = g x)  partition f xs = partition g ys"
  by (induction xs arbitrary: ys) auto

lemma size_remove_neg[termination_simp]: "size (remove_neg φ)  size φ"
  by (cases φ) simp_all

fun is_constraint :: "formula  bool" where
  "is_constraint (Eq t1 t2) = True"
| "is_constraint (Less t1 t2) = True"
| "is_constraint (LessEq t1 t2) = True"
| "is_constraint (Neg (Eq t1 t2)) = True"
| "is_constraint (Neg (Less t1 t2)) = True"
| "is_constraint (Neg (LessEq t1 t2)) = True"
| "is_constraint _ = False"

definition safe_assignment :: "nat set  formula  bool" where
  "safe_assignment X φ = (case φ of
       Eq (Var x) (Var y)  (x  X  y  X)
     | Eq (Var x) t  (x  X  fv_trm t  X)
     | Eq t (Var x)  (x  X  fv_trm t  X)
     | _  False)"

fun safe_formula :: "formula  bool" where
  "safe_formula (Eq t1 t2) = (is_Const t1  (is_Const t2  is_Var t2)  is_Var t1  is_Const t2)"
| "safe_formula (Neg (Eq (Var x) (Var y))) = (x = y)"
| "safe_formula (Less t1 t2) = False"
| "safe_formula (LessEq t1 t2) = False"
| "safe_formula (Pred e ts) = (tset ts. is_Var t  is_Const t)"
| "safe_formula (Let p φ ψ) = ({0..<nfv φ}  fv φ  safe_formula φ  safe_formula ψ)"
| "safe_formula (Neg φ) = (fv φ = {}  safe_formula φ)"
| "safe_formula (Or φ ψ) = (fv ψ = fv φ  safe_formula φ  safe_formula ψ)"
| "safe_formula (And φ ψ) = (safe_formula φ 
    (safe_assignment (fv φ) ψ  safe_formula ψ 
      fv ψ  fv φ  (is_constraint ψ  (case ψ of Neg ψ'  safe_formula ψ' | _  False))))"
| "safe_formula (Ands l) = (let (pos, neg) = partition safe_formula l in pos  [] 
    list_all safe_formula (map remove_neg neg)  (set (map fv neg))  (set (map fv pos)))"
| "safe_formula (Exists φ) = (safe_formula φ)"
| "safe_formula (Agg y ω b f φ) = (safe_formula φ  y + b  fv φ  {0..<b}  fv φ  fv_trm f  fv φ)"
| "safe_formula (Prev I φ) = (safe_formula φ)"
| "safe_formula (Next I φ) = (safe_formula φ)"
| "safe_formula (Since φ I ψ) = (fv φ  fv ψ 
    (safe_formula φ  (case φ of Neg φ'  safe_formula φ' | _  False))  safe_formula ψ)"
| "safe_formula (Until φ I ψ) = (fv φ  fv ψ 
    (safe_formula φ  (case φ of Neg φ'  safe_formula φ' | _  False))  safe_formula ψ)"
| "safe_formula (MatchP I r) = Regex.safe_regex fv (λg φ. safe_formula φ 
     (g = Lax  (case φ of Neg φ'  safe_formula φ' | _  False))) Past Strict r"
| "safe_formula (MatchF I r) = Regex.safe_regex fv (λg φ. safe_formula φ 
     (g = Lax  (case φ of Neg φ'  safe_formula φ' | _  False))) Futu Strict r"

abbreviation "safe_regex  Regex.safe_regex fv (λg φ. safe_formula φ 
  (g = Lax  (case φ of Neg φ'  safe_formula φ' | _  False)))"

lemma safe_regex_safe_formula:
  "safe_regex m g r  φ  Regex.atms r  safe_formula φ 
  (ψ. φ = Neg ψ  safe_formula ψ)"
  by (cases g) (auto dest!: safe_regex_safe[rotated] split: formula.splits[where formula=φ])

lemma safe_abbrevs[simp]: "safe_formula TT" "safe_formula FF"
  unfolding TT_def FF_def by auto

definition safe_neg :: "formula  bool" where
  "safe_neg φ  (¬ safe_formula φ  safe_formula (remove_neg φ))"

definition atms :: "formula Regex.regex  formula set" where
  "atms r = (φ  Regex.atms r.
     if safe_formula φ then {φ} else case φ of Neg φ'  {φ'} | _  {})"

lemma atms_simps[simp]:
  "atms (Regex.Skip n) = {}"
  "atms (Regex.Test φ) = (if safe_formula φ then {φ} else case φ of Neg φ'  {φ'} | _  {})"
  "atms (Regex.Plus r s) = atms r  atms s"
  "atms (Regex.Times r s) = atms r  atms s"
  "atms (Regex.Star r) = atms r"
  unfolding atms_def by auto

lemma finite_atms[simp]: "finite (atms r)"
  by (induct r) (auto split: formula.splits)

lemma disjE_Not2: "P  Q  (P  R)  (¬P  Q  R)  R"
  by blast

lemma safe_formula_induct[consumes 1, case_names Eq_Const Eq_Var1 Eq_Var2 neq_Var Pred Let
    And_assign And_safe And_constraint And_Not Ands Neg Or Exists Agg
    Prev Next Since Not_Since Until Not_Until MatchP MatchF]:
  assumes "safe_formula φ"
    and Eq_Const: "c d. P (Eq (Const c) (Const d))"
    and Eq_Var1: "c x. P (Eq (Const c) (Var x))"
    and Eq_Var2: "c x. P (Eq (Var x) (Const c))"
    and neq_Var: "x. P (Neg (Eq (Var x) (Var x)))"
    and Pred: "e ts. tset ts. is_Var t  is_Const t  P (Pred e ts)"
    and Let: "p φ ψ. {0..<nfv φ}  fv φ  safe_formula φ  safe_formula ψ  P φ  P ψ  P (Let p φ ψ)"
    and And_assign: "φ ψ. safe_formula φ  safe_assignment (fv φ) ψ  P φ  P (And φ ψ)"
    and And_safe: "φ ψ. safe_formula φ  ¬ safe_assignment (fv φ) ψ  safe_formula ψ 
      P φ  P ψ  P (And φ ψ)"
    and And_constraint: "φ ψ. safe_formula φ  ¬ safe_assignment (fv φ) ψ  ¬ safe_formula ψ 
      fv ψ  fv φ  is_constraint ψ  P φ  P (And φ ψ)"
    and And_Not: "φ ψ. safe_formula φ  ¬ safe_assignment (fv φ) (Neg ψ)  ¬ safe_formula (Neg ψ) 
      fv (Neg ψ)  fv φ  ¬ is_constraint (Neg ψ)  safe_formula ψ  P φ  P ψ  P (And φ (Neg ψ))"
    and Ands: "l pos neg. (pos, neg) = partition safe_formula l  pos  [] 
      list_all safe_formula pos  list_all safe_formula (map remove_neg neg) 
      (φset neg. fv φ)  (φset pos. fv φ) 
      list_all P pos  list_all P (map remove_neg neg)  P (Ands l)"
    and Neg: "φ. fv φ = {}  safe_formula φ  P φ  P (Neg φ)"
    and Or: "φ ψ. fv ψ = fv φ  safe_formula φ  safe_formula ψ  P φ  P ψ  P (Or φ ψ)"
    and Exists: "φ. safe_formula φ  P φ  P (Exists φ)"
    and Agg: "y ω b f φ. y + b  fv φ  {0..<b}  fv φ  fv_trm f  fv φ 
      safe_formula φ  P φ  P (Agg y ω b f φ)"
    and Prev: "I φ. safe_formula φ  P φ  P (Prev I φ)"
    and Next: "I φ. safe_formula φ  P φ  P (Next I φ)"
    and Since: "φ I ψ. fv φ  fv ψ  safe_formula φ  safe_formula ψ  P φ  P ψ  P (Since φ I ψ)"
    and Not_Since: "φ I ψ. fv (Neg φ)  fv ψ  safe_formula φ 
      ¬ safe_formula (Neg φ)  safe_formula ψ  P φ  P ψ  P (Since (Neg φ) I ψ )"
    and Until: "φ I ψ. fv φ  fv ψ  safe_formula φ  safe_formula ψ  P φ  P ψ  P (Until φ I ψ)"
    and Not_Until: "φ I ψ. fv (Neg φ)  fv ψ  safe_formula φ 
      ¬ safe_formula (Neg φ)  safe_formula ψ  P φ  P ψ  P (Until (Neg φ) I ψ)"
    and MatchP: "I r. safe_regex Past Strict r  φ  atms r. P φ  P (MatchP I r)"
    and MatchF: "I r. safe_regex Futu Strict r  φ  atms r. P φ  P (MatchF I r)"
  shows "P φ"
using assms(1) proof (induction φ rule: safe_formula.induct)
  case (1 t1 t2)
  then show ?case using Eq_Const Eq_Var1 Eq_Var2 by (auto simp: trm.is_Const_def trm.is_Var_def)
next
  case (9 φ ψ)
  from ‹safe_formula (And φ ψ) have "safe_formula φ" by simp
  from ‹safe_formula (And φ ψ) consider
    (a) "safe_assignment (fv φ) ψ"
    | (b) "¬ safe_assignment (fv φ) ψ" "safe_formula ψ"
    | (c) "fv ψ  fv φ" "¬ safe_assignment (fv φ) ψ" "¬ safe_formula ψ" "is_constraint ψ"
    | (d) ψ' where "fv ψ  fv φ" "¬ safe_assignment (fv φ) ψ" "¬ safe_formula ψ" "¬ is_constraint ψ"
        "ψ = Neg ψ'" "safe_formula ψ'"
    by (cases ψ) auto
  then show ?case proof cases
    case a
    then show ?thesis using "9.IH" ‹safe_formula φ by (intro And_assign)
  next
    case b
    then show ?thesis using "9.IH" ‹safe_formula φ by (intro And_safe)
  next
    case c
    then show ?thesis using "9.IH" ‹safe_formula φ by (intro And_constraint)
  next
    case d
    then show ?thesis using "9.IH" ‹safe_formula φ by (blast intro!: And_Not)
  qed
next
  case (10 l)
  obtain pos neg where posneg: "(pos, neg) = partition safe_formula l" by simp
  have "pos  []" using "10.prems" posneg by simp
  moreover have "list_all safe_formula pos" using posneg by (simp add: list.pred_set)
  moreover have safe_remove_neg: "list_all safe_formula (map remove_neg neg)" using "10.prems" posneg by auto
  moreover have "list_all P pos"
    using posneg "10.IH"(1) by (simp add: list_all_iff)
  moreover have "list_all P (map remove_neg neg)"
    using "10.IH"(2)[OF posneg] safe_remove_neg by (simp add: list_all_iff)
  ultimately show ?case using "10.IH"(1) "10.prems" Ands posneg by simp
next
  case (15 φ I ψ)
  then show ?case
  proof (cases φ)
    case (Ands l)
    then show ?thesis using "15.IH"(1) "15.IH"(3) "15.prems" Since by auto
  qed (auto 0 3 elim!: disjE_Not2 intro: Since Not_Since) (*SLOW*)
next
  case (16 φ I ψ)
  then show ?case
  proof (cases φ)
    case (Ands l)
    then show ?thesis using "16.IH"(1) "16.IH"(3) "16.prems" Until by auto
  qed (auto 0 3 elim!: disjE_Not2 intro: Until Not_Until) (*SLOW*)
next
  case (17 I r)
  then show ?case
    by (intro MatchP) (auto simp: atms_def dest: safe_regex_safe_formula split: if_splits)
next
  case (18 I r)
  then show ?case
    by (intro MatchF) (auto simp: atms_def dest: safe_regex_safe_formula split: if_splits)
qed (auto simp: assms)

lemma safe_formula_NegD:
  "safe_formula (Formula.Neg φ)  fv φ = {}  (x. φ = Formula.Eq (Formula.Var x) (Formula.Var x))"
  by (induct "Formula.Neg φ" rule: safe_formula_induct) auto


subsection ‹Slicing traces›

qualified fun matches ::
  "env  formula  name × event_data list  bool" where
  "matches v (Pred r ts) e = (fst e = r  map (eval_trm v) ts = snd e)"
| "matches v (Let p φ ψ) e =
    ((v'. matches v' φ e  matches v ψ (p, v')) 
    fst e  p  matches v ψ e)"
| "matches v (Eq _ _) e = False"
| "matches v (Less _ _) e = False"
| "matches v (LessEq _ _) e = False"
| "matches v (Neg φ) e = matches v φ e"
| "matches v (Or φ ψ) e = (matches v φ e  matches v ψ e)"
| "matches v (And φ ψ) e = (matches v φ e  matches v ψ e)"
| "matches v (Ands l) e = (φset l. matches v φ e)"
| "matches v (Exists φ) e = (z. matches (z # v) φ e)"
| "matches v (Agg y ω b f φ) e = (zs. length zs = b  matches (zs @ v) φ e)"
| "matches v (Prev I φ) e = matches v φ e"
| "matches v (Next I φ) e = matches v φ e"
| "matches v (Since φ I ψ) e = (matches v φ e  matches v ψ e)"
| "matches v (Until φ I ψ) e = (matches v φ e  matches v ψ e)"
| "matches v (MatchP I r) e = (φ  Regex.atms r. matches v φ e)"
| "matches v (MatchF I r) e = (φ  Regex.atms r. matches v φ e)"

lemma matches_cong:
  "xfv φ. v!x = v'!x  matches v φ e = matches v' φ e"
proof (induct φ arbitrary: v v' e)
  case (Pred n ts)
  show ?case
    by (simp cong: map_cong eval_trm_fv_cong[OF Pred(1)[simplified, THEN bspec]])
next
  case (Let p b φ ψ)
  then show ?case
    by (cases e) (auto 11 0)
next
  case (Ands l)
  have "φ. φ  (set l)  matches v φ e = matches v' φ e"
  proof -
    fix φ assume "φ  (set l)"
    then have "fv φ  fv (Ands l)" using fv_subset_Ands by blast
    then have "xfv φ. v!x = v'!x" using Ands.prems by blast
    then show "matches v φ e = matches v' φ e" using Ands.hyps φ  set l by blast
  qed
  then show ?case by simp
next
  case (Exists φ)
  then show ?case unfolding matches.simps by (intro iff_exI) (simp add: fvi_Suc nth_Cons')
next
  case (Agg y ω b f φ)
  have "matches (zs @ v) φ e = matches (zs @ v') φ e" if "length zs = b" for zs
    using that Agg.prems by (simp add: Agg.hyps[where v="zs @ v" and v'="zs @ v'"]
        nth_append fvi_iff_fv(1)[where b=b])
  then show ?case by auto
qed (auto 9 0 simp add: nth_Cons' fv_regex_alt)

abbreviation relevant_events where "relevant_events φ S  {e. S  {v. matches v φ e}  {}}"

lemma sat_slice_strong:
  assumes "v  S" "dom V = dom V'"
    "p v i. p  dom V  (p, v)  relevant_events φ S  v  the (V p) i  v  the (V' p) i"
  shows "relevant_events φ S - {e. fst e  dom V}  E 
    sat σ V v i φ  sat (map_Γ (λD. D  E) σ) V' v i φ"
  using assms
proof (induction φ arbitrary: V V' v S i)
  case (Pred r ts)
  show ?case proof (cases "V r")
    case None
    then have "V' r = None" using ‹dom V = dom V' by auto
    with None Pred(1,2) show ?thesis by (auto simp: domIff dest!: subsetD)
  next
    case (Some a)
    moreover obtain a' where "V' r = Some a'" using Some ‹dom V = dom V' by auto
    moreover have "(map (eval_trm v) ts  the (V r) i) = (map (eval_trm v) ts  the (V' r) i)"
      using Some Pred(2,4) by (fastforce intro: domI)
    ultimately show ?thesis by simp
  qed
next
  case (Let p φ ψ)
  from Let.prems show ?case unfolding sat.simps
  proof (intro Let(2)[of S], goal_cases relevant v dom V)
    case (V p' v' i)
    then show ?case
    proof (cases "p' = p")
      case [simp]: True
      with V show ?thesis
        unfolding fun_upd_apply eqTrueI[OF True] if_True option.sel mem_Collect_eq
      proof (intro ex_cong conj_cong refl Let(1)[where
        S="{v'. (v  S. matches v ψ (p, v'))}" and V=V],
        goal_cases relevant' v' dom' V')
        case relevant'
        then show ?case
          by (elim subset_trans[rotated]) (auto simp: set_eq_iff)
      next
        case (V' p' v' i)
        then show ?case
          by (intro V(4)) (auto simp: set_eq_iff)
      qed auto
    next
      case False
      with V(2,3,5,6) show ?thesis
        unfolding fun_upd_apply eq_False[THEN iffD2, OF False] if_False
        by (intro V(4)) (auto simp: False)
    qed
  qed (auto simp: dom_def)
next
  case (Or φ ψ)
  show ?case using Or.IH[of S V v V'] Or.prems
    by (auto simp: Collect_disj_eq Int_Un_distrib subset_iff)
next
  case (And φ ψ)
  show ?case using And.IH[of S V v V'] And.prems
    by (auto simp: Collect_disj_eq Int_Un_distrib subset_iff)
next
  case (Ands l)
  obtain "relevant_events (Ands l) S - {e. fst e  dom V}  E" "v  S" using Ands.prems(1) Ands.prems(2) by blast
  then have "{e. S  {v. matches v (Ands l) e}  {}} - {e. fst e  dom V}  E" by simp
  have "φ. φ  set l  sat σ V v i φ  sat (map_Γ (λD. D  E) σ) V' v i φ"
  proof -
    fix φ assume "φ  set l"
    have "relevant_events φ S = {e. S  {v. matches v φ e}  {}}" by simp
    have "{e. S  {v. matches v φ e}  {}}  {e. S  {v. matches v (Ands l) e}  {}}" (is "?A  ?B")
    proof (rule subsetI)
      fix e assume "e  ?A"
      then have "S  {v. matches v φ e}  {}" by blast
      moreover have "S  {v. matches v (Ands l) e}  {}"
      proof -
        obtain v where "v  S" "matches v φ e" using calculation by blast
        then show ?thesis using φ  set l by auto
      qed
      then show "e  ?B" by blast
    qed
    then have "relevant_events φ S - {e. fst e  dom V}  E" using Ands.prems(1) by auto
    then show "sat σ V v i φ  sat (map_Γ (λD. D  E) σ) V' v i φ"
      using Ands.prems(2,3) φ  set l
      by (intro Ands.IH[of φ S V v V' i] Ands.prems(4)) auto
  qed
  show ?case using φ. φ  set l  sat σ V v i φ = sat (map_Γ (λD. D  E) σ) V' v i φ sat_Ands by blast
next
  case (Exists φ)
  have "sat σ V (z # v) i φ = sat (map_Γ (λD. D  E) σ) V' (z # v) i φ" for z
    using Exists.prems(1-3) by (intro Exists.IH[where S="{z # v | v. v  S}"] Exists.prems(4)) auto
  then show ?case by simp
next
  case (Agg y ω b f φ)
  have "sat σ V (zs @ v) i φ = sat (map_Γ (λD. D  E) σ) V' (zs @ v) i φ" if "length zs = b" for zs
    using that Agg.prems(1-3) by (intro Agg.IH[where S="{zs @ v | v. v  S}"] Agg.prems(4)) auto
  then show ?case by (simp cong: conj_cong)
next
  case (Prev I φ)
  then show ?case by (auto cong: nat.case_cong)
next
  case (Next I φ)
  then show ?case by simp
next
  case (Since φ I ψ)
  show ?case using Since.IH[of S V] Since.prems
   by (auto simp: Collect_disj_eq Int_Un_distrib subset_iff)
next
  case (Until φ I ψ)
  show ?case using Until.IH[of S V] Until.prems
    by (auto simp: Collect_disj_eq Int_Un_distrib subset_iff)
next
  case (MatchP I r)
  from MatchP.prems(1-3) have "Regex.match (sat σ V v) r = Regex.match (sat (map_Γ (λD. D  E) σ) V' v) r"
    by (intro Regex.match_fv_cong MatchP(1)[of _ S V v] MatchP.prems(4)) auto
  then show ?case
    by auto
next
  case (MatchF I r)
  from MatchF.prems(1-3) have "Regex.match (sat σ V v) r = Regex.match (sat (map_Γ (λD. D  E) σ) V' v) r"
    by (intro Regex.match_fv_cong MatchF(1)[of _ S V v] MatchF.prems(4)) auto
  then show ?case
    by auto
qed simp_all


subsection ‹Translation to n-ary conjunction›

fun get_and_list :: "formula  formula list" where
  "get_and_list (Ands l) = l"
| "get_and_list φ = [φ]"

lemma fv_get_and: "(x(set (get_and_list φ)). fvi b x) = fvi b φ"
  by (induction φ rule: get_and_list.induct) simp_all

lemma safe_get_and: "safe_formula φ  list_all safe_neg (get_and_list φ)"
  by (induction φ rule: get_and_list.induct) (simp_all add: safe_neg_def list_all_iff)

lemma sat_get_and: "sat σ V v i φ  list_all (sat σ V v i) (get_and_list φ)"
  by (induction φ rule: get_and_list.induct) (simp_all add: list_all_iff)

fun convert_multiway :: "formula  formula" where
  "convert_multiway (Neg φ) = Neg (convert_multiway φ)"
| "convert_multiway (Or φ ψ) = Or (convert_multiway φ) (convert_multiway ψ)"
| "convert_multiway (And φ ψ) = (if safe_assignment (fv φ) ψ then
      And (convert_multiway φ) ψ
    else if safe_formula ψ then
      Ands (get_and_list (convert_multiway φ) @ get_and_list (convert_multiway ψ))
    else if is_constraint ψ then
      And (convert_multiway φ) ψ
    else Ands (convert_multiway ψ # get_and_list (convert_multiway φ)))"
| "convert_multiway (Exists φ) = Exists (convert_multiway φ)"
| "convert_multiway (Agg y ω b f φ) = Agg y ω b f (convert_multiway φ)"
| "convert_multiway (Prev I φ) = Prev I (convert_multiway φ)"
| "convert_multiway (Next I φ) = Next I (convert_multiway φ)"
| "convert_multiway (Since φ I ψ) = Since (convert_multiway φ) I (convert_multiway ψ)"
| "convert_multiway (Until φ I ψ) = Until (convert_multiway φ) I (convert_multiway ψ)"
| "convert_multiway (MatchP I r) = MatchP I (Regex.map_regex convert_multiway r)"
| "convert_multiway (MatchF I r) = MatchF I (Regex.map_regex convert_multiway r)"
| "convert_multiway φ = φ"

abbreviation "convert_multiway_regex  Regex.map_regex convert_multiway"

lemma fv_safe_get_and:
  "safe_formula φ  fv φ  (x(set (filter safe_formula (get_and_list φ))). fv x)"
proof (induction φ rule: get_and_list.induct)
  case (1 l)
  obtain pos neg where posneg: "(pos, neg) = partition safe_formula l" by simp
  have "get_and_list (Ands l) = l" by simp
  have sub: "(xset neg. fv x)  (xset pos. fv x)" using "1.prems" posneg by simp
  then have "fv (Ands l)  (xset pos. fv x)"
  proof -
    have "fv (Ands l) = (xset pos. fv x)  (xset neg. fv x)" using posneg by auto
    then show ?thesis using sub by simp
  qed
  then show ?case using posneg by auto
qed auto

lemma ex_safe_get_and:
  "safe_formula φ  list_ex safe_formula (get_and_list φ)"
proof (induction φ rule: get_and_list.induct)
  case (1 l)
  have "get_and_list (Ands l) = l" by simp
  obtain pos neg where posneg: "(pos, neg) = partition safe_formula l" by simp
  then have "pos  []" using "1.prems" by simp
  then obtain x where "x  set pos" by fastforce
  then show ?case using posneg using Bex_set_list_ex by fastforce
qed simp_all

lemma case_NegE: "(case φ of Neg φ'  P φ' | _  False)  (φ'. φ = Neg φ'  P φ'  Q)  Q"
  by (cases φ) simp_all

lemma convert_multiway_remove_neg: "safe_formula (remove_neg φ)  convert_multiway (remove_neg φ) = remove_neg (convert_multiway φ)"
  by (cases φ) (auto elim: case_NegE)

lemma fv_convert_multiway: "safe_formula φ  fvi b (convert_multiway φ) = fvi b φ"
proof (induction φ arbitrary: b rule: safe_formula.induct)
  case (9 φ ψ)
  then show ?case by (cases ψ) (auto simp: fv_get_and Un_commute)
next
  case (15 φ I ψ)
  show ?case proof (cases "safe_formula φ")
    case True
    with 15 show ?thesis by simp
  next
    case False
    with "15.prems" obtain φ' where "φ = Neg φ'" by (simp split: formula.splits)
    with False 15 show ?thesis by simp
  qed
next
  case (16 φ I ψ)
  show ?case proof (cases "safe_formula φ")
    case True
    with 16 show ?thesis by simp
  next
    case False
    with "16.prems" obtain φ' where "φ = Neg φ'" by (simp split: formula.splits)
    with False 16 show ?thesis by simp
  qed
next
  case (17 I r)
  then show ?case
    unfolding convert_multiway.simps fvi.simps fv_regex_alt regex.set_map image_image
    by (intro arg_cong[where f=Union, OF image_cong[OF refl]])
      (auto dest!: safe_regex_safe_formula)
next
  case (18 I r)
  then show ?case
    unfolding convert_multiway.simps fvi.simps fv_regex_alt regex.set_map image_image
    by (intro arg_cong[where f=Union, OF image_cong[OF refl]])
      (auto dest!: safe_regex_safe_formula)
qed (auto simp del: convert_multiway.simps(3))

lemma get_and_nonempty:
  assumes "safe_formula φ"
  shows "get_and_list φ  []"
  using assms by (induction φ) auto

lemma future_bounded_get_and:
  "list_all future_bounded (get_and_list φ) = future_bounded φ"
  by (induction φ) simp_all

lemma safe_convert_multiway: "safe_formula φ  safe_formula (convert_multiway φ)"
proof (induction φ rule: safe_formula_induct)
  case (And_safe φ ψ)
  let ?a = "And φ ψ"
  let ?b = "convert_multiway ?a"
  let ?cφ = "convert_multiway φ"
  let ?cψ = "convert_multiway ψ"
  have b_def: "?b = Ands (get_and_list ?cφ @ get_and_list ?cψ)"
    using And_safe by simp
  show ?case proof -
    let ?l = "get_and_list ?cφ @ get_and_list ?cψ"
    obtain pos neg where posneg: "(pos, neg) = partition safe_formula ?l" by simp
    then have "list_all safe_formula pos" by (auto simp: list_all_iff)
    have lsafe_neg: "list_all safe_neg ?l"
      using And_safe ‹safe_formula φ ‹safe_formula ψ
      by (simp add: safe_get_and)
    then have "list_all safe_formula (map remove_neg neg)"
    proof -
      have "x. x  set neg  safe_formula (remove_neg x)"
      proof -
        fix x assume "x  set neg"
        then have "¬ safe_formula x" using posneg by auto
        moreover have "safe_neg x" using lsafe_neg x  set neg
          unfolding safe_neg_def list_all_iff partition_set[OF posneg[symmetric], symmetric]
          by simp
        ultimately show "safe_formula (remove_neg x)" using safe_neg_def by blast
      qed
      then show ?thesis by (auto simp: list_all_iff)
    qed

    have pos_filter: "pos = filter safe_formula (get_and_list ?cφ @ get_and_list ?cψ)"
      using posneg by simp
    have "(xset neg. fv x)  (xset pos. fv x)"
    proof -
      have 1: "fv ?cφ  (x(set (filter safe_formula (get_and_list ?cφ))). fv x)" (is "_  ?fvφ")
        using And_safe ‹safe_formula φ by (blast intro!: fv_safe_get_and)
      have 2: "fv ?cψ  (x(set (filter safe_formula (get_and_list ?cψ))). fv x)" (is "_  ?fvψ")
        using And_safe ‹safe_formula ψ by (blast intro!: fv_safe_get_and)
      have "(xset neg. fv x)  fv ?cφ  fv ?cψ" proof -
        have " (fv ` set neg)   (fv ` (set pos  set neg))"
          by simp
        also have "...  fv (convert_multiway φ)  fv (convert_multiway ψ)"
          unfolding partition_set[OF posneg[symmetric], simplified]
          by (simp add: fv_get_and)
        finally show ?thesis .
      qed
      then have "(xset neg. fv x)  ?fvφ  ?fvψ" using 1 2 by blast
      then show ?thesis unfolding pos_filter by simp
    qed
    have "pos  []"
    proof -
      obtain x where "x  set (get_and_list ?cφ)" "safe_formula x"
        using And_safe ‹safe_formula φ ex_safe_get_and by (auto simp: list_ex_iff)
      then show ?thesis
        unfolding pos_filter by (auto simp: filter_empty_conv)
    qed
    then show ?thesis unfolding b_def
      using  (fv ` set neg)   (fv ` set pos) ‹list_all safe_formula (map remove_neg neg)
        ‹list_all safe_formula pos posneg
      by simp
  qed
next
  case (And_Not φ ψ)
  let ?a = "And φ (Neg ψ)"
  let ?b = "convert_multiway ?a"
  let ?cφ = "convert_multiway φ"
  let ?cψ = "convert_multiway ψ"
  have b_def: "?b = Ands (Neg ?cψ # get_and_list ?cφ)"
    using And_Not by simp
  show ?case proof -
    let ?l = "Neg ?cψ # get_and_list ?cφ"
    note ‹safe_formula ?cφ
    then have "list_all safe_neg (get_and_list ?cφ)" by (simp add: safe_get_and)
    moreover have "safe_neg (Neg ?cψ)"
      using ‹safe_formula ?cψ by (simp add: safe_neg_def)
    then have lsafe_neg: "list_all safe_neg ?l" using calculation by simp
    obtain pos neg where posneg: "(pos, neg) = partition safe_formula ?l" by simp
    then have "list_all safe_formula pos" by (auto simp: list_all_iff)
    then have "list_all safe_formula (map remove_neg neg)"
    proof -
      have "x. x  (set neg)  safe_formula (remove_neg x)"
      proof -
        fix x assume "x  set neg"
        then have "¬ safe_formula x" using posneg by (auto simp del: filter.simps)
        moreover have "safe_neg x" using lsafe_neg x  set neg
          unfolding safe_neg_def list_all_iff partition_set[OF posneg[symmetric], symmetric]
          by simp
        ultimately show "safe_formula (remove_neg x)" using safe_neg_def by blast
      qed
      then show ?thesis using Ball_set_list_all by force
    qed

    have pos_filter: "pos = filter safe_formula ?l"
      using posneg by simp
    have neg_filter: "neg = filter (Not  safe_formula) ?l"
      using posneg by simp
    have "(x(set neg). fv x)  (x(set pos). fv x)"
    proof -
      have fv_neg: "(x(set neg). fv x)  (x(set ?l). fv x)" using posneg by auto
      have "(x(set ?l). fv x)  fv ?cφ  fv ?cψ"
        using ‹safe_formula φ ‹safe_formula ψ
        by (simp add: fv_get_and fv_convert_multiway)
      also have "fv ?cφ  fv ?cψ  fv ?cφ"
        using ‹safe_formula φ ‹safe_formula ψ ‹fv (Neg ψ)  fv φ
        by (simp add: fv_convert_multiway[symmetric])
      finally have "(x(set neg). fv x)  fv ?cφ"
        using fv_neg unfolding neg_filter by blast
      then show ?thesis
        unfolding pos_filter
        using fv_safe_get_and[OF And_Not.IH(1)]
        by auto
    qed
    have "pos  []"
    proof -
      obtain x where "x  set (get_and_list ?cφ)" "safe_formula x"
        using And_Not.IH ‹safe_formula φ ex_safe_get_and by (auto simp: list_ex_iff)
      then show ?thesis
        unfolding pos_filter by (auto simp: filter_empty_conv)
    qed
    then show ?thesis unfolding b_def
      using  (fv ` set neg)   (fv ` set pos) ‹list_all safe_formula (map remove_neg neg)
        ‹list_all safe_formula pos posneg
      by simp
  qed
next
  case (Neg φ)
  have "safe_formula (Neg φ')  safe_formula φ'" if "fv φ' = {}" for φ'
    using that by (cases "Neg φ'" rule: safe_formula.cases) simp_all
  with Neg show ?case by (simp add: fv_convert_multiway)
next
  case (MatchP I r)
  then show ?case
    by (auto 0 3 simp: atms_def fv_convert_multiway intro!: safe_regex_map_regex
      elim!: disjE_Not2 case_NegE
      dest: safe_regex_safe_formula split: if_splits)
next
  case (MatchF I r)
  then show ?case
    by (auto 0 3 simp: atms_def fv_convert_multiway intro!: safe_regex_map_regex
      elim!: disjE_Not2 case_NegE
      dest: safe_regex_safe_formula split: if_splits)
qed (auto simp: fv_convert_multiway)

lemma future_bounded_convert_multiway: "safe_formula φ  future_bounded (convert_multiway φ) = future_bounded φ"
proof (induction φ rule: safe_formula_induct)
  case (And_safe φ ψ)
  let ?a = "And φ ψ"
  let ?b = "convert_multiway ?a"
  let ?cφ = "convert_multiway φ"
  let ?cψ = "convert_multiway ψ"
  have b_def: "?b = Ands (get_and_list ?cφ @ get_and_list ?cψ)"
    using And_safe by simp
  have "future_bounded ?a = (future_bounded ?cφ  future_bounded ?cψ)"
    using And_safe by simp
  moreover have "future_bounded ?cφ = list_all future_bounded (get_and_list ?cφ)"
    using ‹safe_formula φ by (simp add: future_bounded_get_and safe_convert_multiway)
  moreover have "future_bounded ?cψ = list_all future_bounded (get_and_list ?cψ)"
    using ‹safe_formula ψ by (simp add: future_bounded_get_and safe_convert_multiway)
  moreover have "future_bounded ?b = list_all future_bounded (get_and_list ?cφ @ get_and_list ?cψ)"
    unfolding b_def by simp
  ultimately show ?case by simp
next
  case (And_Not φ ψ)
  let ?a = "And φ (Neg ψ)"
  let ?b = "convert_multiway ?a"
  let ?cφ = "convert_multiway φ"
  let ?cψ = "convert_multiway ψ"
  have b_def: "?b = Ands (Neg ?cψ # get_and_list ?cφ)"
    using And_Not by simp
  have "future_bounded ?a = (future_bounded ?cφ  future_bounded ?cψ)"
    using And_Not by simp
  moreover have "future_bounded ?cφ = list_all future_bounded (get_and_list ?cφ)"
    using ‹safe_formula φ by (simp add: future_bounded_get_and safe_convert_multiway)
  moreover have "future_bounded ?b = list_all future_bounded (Neg ?cψ # get_and_list ?cφ)"
    unfolding b_def by (simp add: list.pred_map o_def)
  ultimately show ?case by auto
next
  case (MatchP I r)
  then show ?case
    by (fastforce simp: atms_def regex.pred_set regex.set_map ball_Un
        elim: safe_regex_safe_formula[THEN disjE_Not2])
next
  case (MatchF I r)
  then show ?case
    by (fastforce simp: atms_def regex.pred_set regex.set_map ball_Un
        elim: safe_regex_safe_formula[THEN disjE_Not2])
qed auto

lemma sat_convert_multiway: "safe_formula φ  sat σ V v i (convert_multiway φ)  sat σ V v i φ"
proof (induction φ arbitrary: v i rule: safe_formula_induct)
  case (And_safe φ ψ)
  let ?a = "And φ ψ"
  let ?b = "convert_multiway ?a"
  let ?la = "get_and_list (convert_multiway φ)"
  let ?lb = "get_and_list (convert_multiway ψ)"
  let ?sat = "sat σ V v i"
  have b_def: "?b = Ands (?la @ ?lb)" using And_safe by simp
  have "list_all ?sat ?la  ?sat φ" using And_safe sat_get_and by blast
  moreover have "list_all ?sat ?lb  ?sat ψ" using And_safe sat_get_and by blast
  ultimately show ?case using And_safe by (auto simp: list.pred_set)
next
  case (And_Not φ ψ)
  let ?a = "And φ (Neg ψ)"
  let ?b = "convert_multiway ?a"
  let ?la = "get_and_list (convert_multiway φ)"
  let ?lb = "convert_multiway ψ"
  let ?sat = "sat σ V v i"
  have b_def: "?b = Ands (Neg ?lb # ?la)" using And_Not by simp
  have "list_all ?sat ?la  ?sat φ" using And_Not sat_get_and by blast
  then show ?case using And_Not by (auto simp: list.pred_set)
next
  case (Agg y ω b f φ)
  then show ?case
    by (simp add: nfv_def fv_convert_multiway cong: conj_cong)
next
  case (MatchP I r)
  then have "Regex.match (sat σ V v) (convert_multiway_regex r) = Regex.match (sat σ V v) r"
    unfolding match_map_regex
    by (intro Regex.match_fv_cong)
      (auto 0 4 simp: atms_def elim!: disjE_Not2 dest!: safe_regex_safe_formula)
  then show ?case
    by auto
next
  case (MatchF I r)
  then have "Regex.match (sat σ V v) (convert_multiway_regex r) = Regex.match (sat σ V v) r"
    unfolding match_map_regex
    by (intro Regex.match_fv_cong)
      (auto 0 4 simp: atms_def elim!: disjE_Not2 dest!: safe_regex_safe_formula)
  then show ?case
    by auto
qed (auto cong: nat.case_cong)

end (*context*)

interpretation Formula_slicer: abstract_slicer "relevant_events φ" for φ .

lemma sat_slice_iff:
  assumes "v  S"
  shows "Formula.sat σ V v i φ  Formula.sat (Formula_slicer.slice φ S σ) V v i φ"
  by (rule sat_slice_strong[OF assms]) auto

lemma Neg_splits:
  "P (case φ of formula.Neg ψ  f ψ | φ  g φ) =
   ((ψ. φ = formula.Neg ψ  P (f ψ))  ((¬ Formula.is_Neg φ)  P (g φ)))"
  "P (case φ of formula.Neg ψ  f ψ | _  g φ) =
   (¬ ((ψ. φ = formula.Neg ψ  ¬ P (f ψ))  ((¬ Formula.is_Neg φ)  ¬ P (g φ))))"
  by (cases φ; auto simp: Formula.is_Neg_def)+

(*<*)
end
(*>*)

Theory Optimized_Join

(*<*)
theory Optimized_Join
  imports "Generic_Join.Generic_Join_Correctness"
begin
(*>*)

section ‹Optimized relational join›

subsection ‹Binary join›

definition join_mask :: "nat  nat set  bool list" where
  "join_mask n X = map (λi. i  X) [0..<n]"

fun proj_tuple :: "bool list  'a tuple  'a tuple" where
  "proj_tuple [] [] = []"
| "proj_tuple (True # bs) (a # as) = a # proj_tuple bs as"
| "proj_tuple (False # bs) (a # as) = None # proj_tuple bs as"
| "proj_tuple (b # bs) [] = []"
| "proj_tuple [] (a # as) = []"

lemma proj_tuple_replicate: "(i. i  set bs  ¬i)  length bs = length as 
  proj_tuple bs as = replicate (length bs) None"
  by (induction bs as rule: proj_tuple.induct) fastforce+

lemma proj_tuple_join_mask_empty: "length as = n 
  proj_tuple (join_mask n {}) as = replicate n None"
  using proj_tuple_replicate[of "join_mask n {}"] by (auto simp add: join_mask_def)

lemma proj_tuple_alt: "proj_tuple bs as = map2 (λb a. if b then a else None) bs as"
  by (induction bs as rule: proj_tuple.induct) auto

lemma map2_map: "map2 f (map g [0..<length as]) as = map (λi. f (g i) (as ! i)) [0..<length as]"
  by (rule nth_equalityI) auto

lemma proj_tuple_join_mask_restrict: "length as = n 
  proj_tuple (join_mask n X) as = restrict X as"
  by (auto simp add: restrict_def proj_tuple_alt join_mask_def map2_map)

lemma wf_tuple_proj_idle:
  assumes wf: "wf_tuple n X as"
  shows "proj_tuple (join_mask n X) as = as"
  using proj_tuple_join_mask_restrict[of as n X, unfolded restrict_idle[OF wf]] wf
  by (auto simp add: wf_tuple_def)

lemma wf_tuple_change_base:
  assumes wf: "wf_tuple n X as"
  and mask: "join_mask n X = join_mask n Y"
  shows "wf_tuple n Y as"
  using wf mask by (auto simp add: wf_tuple_def join_mask_def)

definition proj_tuple_in_join :: "bool  bool list  'a tuple  'a table  bool" where
  "proj_tuple_in_join pos bs as t = (if pos then proj_tuple bs as  t else proj_tuple bs as  t)"

abbreviation "join_cond pos t  (λas. if pos then as  t else as  t)"

abbreviation "join_filter_cond pos t  (λas _. join_cond pos t as)"

lemma proj_tuple_in_join_mask_idle:
  assumes wf: "wf_tuple n X as"
  shows "proj_tuple_in_join pos (join_mask n X) as t  join_cond pos t as"
  using wf_tuple_proj_idle[OF wf] by (auto simp add: proj_tuple_in_join_def)

lemma join_sub:
  assumes "L  R" "table n L t1" "table n R t2"
  shows "join t2 pos t1 = {as  t2. proj_tuple_in_join pos (join_mask n L) as t1}"
  using assms proj_tuple_join_mask_restrict[of _ n L] join_restrict[of t2 n R t1 L pos]
    wf_tuple_length restrict_idle
  by (auto simp add: table_def proj_tuple_in_join_def sup.absorb1) fastforce+

lemma join_sub':
  assumes "R  L" "table n L t1" "table n R t2"
  shows "join t2 True t1 = {as  t1. proj_tuple_in_join True (join_mask n R) as t2}"
  using assms proj_tuple_join_mask_restrict[of _ n R] join_restrict[of t2 n R t1 L True]
    wf_tuple_length restrict_idle
  by (auto simp add: table_def proj_tuple_in_join_def sup.absorb1 Un_absorb1) fastforce+

lemma join_eq:
  assumes tab: "table n R t1" "table n R t2"
  shows "join t2 pos t1 = (if pos then t2  t1 else t2 - t1)"
  using join_sub[OF _ tab, of pos] tab(2) proj_tuple_in_join_mask_idle[of n R _ pos t1]
  by (auto simp add: table_def)

lemma join_no_cols:
  assumes tab: "table n {} t1" "table n R t2"
  shows "join t2 pos t1 = (if (pos  replicate n None  t1) then t2 else {})"
  using join_sub[OF _ tab, of pos] tab(2)
  by (auto simp add: table_def proj_tuple_in_join_def wf_tuple_length proj_tuple_join_mask_empty)

lemma join_empty_left: "join {} pos t = {}"
  by (auto simp add: join_def)

lemma join_empty_right: "join t pos {} = (if pos then {} else t)"
  by (auto simp add: join_def)

fun bin_join :: "nat  nat set  'a table  bool  nat set  'a table  'a table" where
  "bin_join n A t pos A' t' =
    (if t = {} then {}
    else if t' = {} then (if pos then {} else t)
    else if A' = {} then (if (pos  replicate n None  t') then t else {})
    else if A' = A then (if pos then t  t' else t - t')
    else if A'  A then {as  t. proj_tuple_in_join pos (join_mask n A') as t'}
    else if A  A'  pos then {as  t'. proj_tuple_in_join pos (join_mask n A) as t}
    else join t pos t')"

lemma bin_join_table:
  assumes tab: "table n A t" "table n A' t'"
  shows "bin_join n A t pos A' t' = join t pos t'"
  using assms join_empty_left[of pos t'] join_empty_right[of t pos]
    join_no_cols[OF _ assms(1), of t' pos] join_eq[of n A t' t pos] join_sub[OF _ assms(2,1)]
    join_sub'[OF _ assms(2,1)]
  by auto+

subsection ‹Multi-way join›

fun mmulti_join' :: "(nat set list  nat set list  'a table list  'a table)" where
  "mmulti_join' A_pos A_neg L = (
    let Q = set (zip A_pos L) in
    let Q_neg = set (zip A_neg (drop (length A_pos) L)) in
    New_max_getIJ_wrapperGenericJoin Q Q_neg)"

lemma mmulti_join'_correct:
  assumes "A_pos  []"
      and "list_all2 (λA X. table n A X  wf_set n A) (A_pos @ A_neg) L"
  shows "z  mmulti_join' A_pos A_neg L  wf_tuple n (Aset A_pos. A) z 
    list_all2 (λA X. restrict A z  X) A_pos (take (length A_pos) L) 
    list_all2 (λA X. restrict A z  X) A_neg (drop (length A_pos) L)"
proof -
  define Q where "Q = set (zip A_pos L)"
  have Q_alt: "Q = set (zip A_pos (take (length A_pos) L))"
    unfolding Q_def by (fastforce simp: in_set_zip)
  define Q_neg where "Q_neg = set (zip A_neg (drop (length A_pos) L))"
  let ?r = "mmulti_join' A_pos A_neg L"
  have "?r = New_max_getIJ_wrapperGenericJoin Q Q_neg"
    unfolding Q_def Q_neg_def by (simp del: New_max.wrapperGenericJoin.simps)
  moreover have "card Q  1"
    unfolding Q_def using assms(1,2)
    by (auto simp: Suc_le_eq card_gt_0_iff zip_eq_Nil_iff)
  moreover have "(A, X)(Q  Q_neg). table n A X  wf_set n A"
    unfolding Q_alt Q_neg_def using assms(2) by (simp add: zip_append1 list_all2_iff)
  ultimately have "z  ?r  wf_tuple n ((A, X)Q. A) z 
      ((A, X)Q. restrict A z  X)  ((A, X)Q_neg. restrict A z  X)"
    using New_max.wrapper_correctness case_prod_beta' by blast
  moreover have "(Aset A_pos. A) = ((A, X)Q. A)" proof -
    from assms(2) have "length A_pos  length L" by (auto dest!: list_all2_lengthD)
    then show ?thesis
      unfolding Q_alt
      by (auto elim: in_set_impl_in_set_zip1[rotated, where ys="take (length A_pos) L"]
          dest: set_zip_leftD)
  qed
  moreover have "z. ((A, X)Q. restrict A z  X) 
    list_all2 (λA X. restrict A z  X) A_pos (take (length A_pos) L)"
    unfolding Q_alt using assms(2) by (auto simp add: list_all2_iff)
  moreover have "z. ((A, X)Q_neg. restrict A z  X) 
    list_all2 (λA X. restrict A z  X) A_neg (drop (length A_pos) L)"
    unfolding Q_neg_def using assms(2) by (auto simp add: list_all2_iff)
  ultimately show ?thesis
    unfolding Q_def Q_neg_def using assms(2) by simp
qed

lemmas restrict_nested = New_max.restrict_nested

lemma list_all2_opt_True:
  assumes "list_all2 (λA X. table n A X  wf_set n A) ((A_zs @ A_x # A_xs @ A_y # A_ys) @ A_neg)
    ((zs @ x # xs @ y # ys) @ L_neg)"
    "length A_xs = length xs" "length A_ys = length ys" "length A_zs = length zs"
  shows "list_all2 (λA X. table n A X  wf_set n A)
    ((A_zs @ (A_x  A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)"
proof -
  have assms_dest: "table n A_x x" "table n A_y y" "wf_set n A_x" "wf_set n A_y"
    using assms
    by (auto simp del: mmulti_join'.simps simp add: list_all2_append1 dest: list_all2_lengthD)
  then have tabs: "table n (A_x  A_y) (join x True y)" "wf_set n (A_x  A_y)"
    using join_table[of n A_x x A_y y True "A_x  A_y", OF assms_dest(1,2)] assms_dest(3,4)
    by (auto simp add: wf_set_def)
  then show "list_all2 (λA X. table n A X  wf_set n A)
    ((A_zs @ (A_x  A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)"
    using assms
    by (auto simp del: mmulti_join'.simps simp add: list_all2_append1 list_all2_append2
        list_all2_Cons1 list_all2_Cons2 dest: list_all2_lengthD) fastforce
qed

lemma mmulti_join'_opt_True:
  assumes "list_all2 (λA X. table n A X  wf_set n A) ((A_zs @ A_x # A_xs @ A_y # A_ys) @ A_neg)
    ((zs @ x # xs @ y # ys) @ L_neg)"
    "length A_xs = length xs" "length A_ys = length ys" "length A_zs = length zs"
  shows "mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg) =
    mmulti_join' (A_zs @ (A_x  A_y) # A_xs @ A_ys) A_neg
    ((zs @ join x True y # xs @ ys) @ L_neg)"
proof -
  have assms_dest: "table n A_x x" "table n A_y y" "wf_set n A_x" "wf_set n A_y"
    using assms
    by (auto simp del: mmulti_join'.simps simp add: list_all2_append1 dest: list_all2_lengthD)
  then have tabs: "table n (A_x  A_y) (join x True y)" "wf_set n (A_x  A_y)"
    using join_table[of n A_x x A_y y True "A_x  A_y", OF assms_dest(1,2)] assms_dest(3,4)
    by (auto simp add: wf_set_def)
  then have list_all2': "list_all2 (λA X. table n A X  wf_set n A)
    ((A_zs @ (A_x  A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)"
    using assms
    by (auto simp del: mmulti_join'.simps simp add: list_all2_append1 list_all2_append2
        list_all2_Cons1 list_all2_Cons2 dest: list_all2_lengthD) fastforce
  have res: "z Z. wf_tuple n Z z  A_x  A_y  Z 
    restrict (A_x  A_y) z  join x True y  restrict A_x z  x  restrict A_y z  y"
    using join_restrict[of x n A_x y A_y True] wf_tuple_restrict_simple[of n _ _ "A_x  A_y"]
      assms_dest(1,2)
    by (auto simp add: table_def restrict_nested Int_absorb2)
  show ?thesis
  proof (rule set_eqI, rule iffI)
    fix z
    assume "z  mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg
      ((zs @ x # xs @ y # ys) @ L_neg)"
    then have z_in_dest: "wf_tuple n ((set (A_zs @ A_x # A_xs @ A_y # A_ys))) z"
      "list_all2 (λA. (∈) (restrict A z)) A_zs zs"
      "restrict A_x z  x"
      "list_all2 (λA. (∈) (restrict A z)) A_ys ys"
      "restrict A_y z  y"
      "list_all2 (λA. (∈) (restrict A z)) A_xs xs"
      "list_all2 (λA. (∉) (restrict A z)) A_neg L_neg"
      using mmulti_join'_correct[OF _ assms(1), of z]
      by (auto simp del: mmulti_join'.simps simp add: assms list_all2_append1
          dest: list_all2_lengthD)
    then show "z  mmulti_join' (A_zs @ (A_x  A_y) # A_xs @ A_ys) A_neg
      ((zs @ join x True y # xs @ ys) @ L_neg)"
      using mmulti_join'_correct[OF _ list_all2', of z] res[OF z_in_dest(1)]
      by (auto simp add: assms list_all2_appendI le_supI2 Un_assoc simp del: mmulti_join'.simps
          dest: list_all2_lengthD)
  next
    fix z
    assume "z  mmulti_join' (A_zs @ (A_x  A_y) # A_xs @ A_ys) A_neg
      ((zs @ join x True y # xs @ ys) @ L_neg)"
    then have z_in_dest: "wf_tuple n ((set (A_zs @ A_x # A_xs @ A_y # A_ys))) z"
      "list_all2 (λA. (∈) (restrict A z)) A_zs zs"
      "restrict (A_x  A_y) z  join x True y"
      "list_all2 (λA. (∈) (restrict A z)) A_ys ys"
      "list_all2 (λA. (∈) (restrict A z)) A_xs xs"
      "list_all2 (λA. (∉) (restrict A z)) A_neg L_neg"
      using mmulti_join'_correct[OF _ list_all2', of z]
      by (auto simp del: mmulti_join'.simps simp add: assms list_all2_append Un_assoc
          dest: list_all2_lengthD)
    then show "z  mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg
      ((zs @ x # xs @ y # ys) @ L_neg)"
      using mmulti_join'_correct[OF _ assms(1), of z] res[OF z_in_dest(1)]
      by (auto simp add: assms list_all2_appendI le_supI2 Un_assoc simp del: mmulti_join'.simps
          dest: list_all2_lengthD)
  qed
qed

lemma list_all2_opt_False:
  assumes "list_all2 (λA X. table n A X  wf_set n A)
    ((A_zs @ A_x # A_xs) @ (A_ws @ A_y # A_ys)) ((zs @ x # xs) @ (ws @ y # ys))"
    "length A_ws = length ws" "length A_xs = length xs"
    "length A_ys = length ys" "length A_zs = length zs"
    "A_y  A_x"
  shows "list_all2 (λA X. table n A X  wf_set n A)
    ((A_zs @ A_x # A_xs) @ (A_ws @ A_ys)) ((zs @ join x False y # xs) @ (ws @ ys))"
proof -
  have assms_dest: "table n A_x x" "table n A_y y" "wf_set n A_x" "wf_set n A_y"
    using assms
    by (auto simp del: mmulti_join'.simps simp add: list_all2_append dest: list_all2_lengthD)
  have tabs: "table n A_x (join x False y)"
    using join_table[of n A_x x A_y y False A_x, OF assms_dest(1,2) assms(6)] assms(6) by auto
  then show "list_all2 (λA X. table n A X  wf_set n A)
    ((A_zs @ A_x # A_xs) @ (A_ws @ A_ys)) ((zs @ join x False y # xs) @ (ws @ ys))"
    using assms assms_dest(3)
    by (auto simp del: mmulti_join'.simps simp add: list_all2_append1 list_all2_append2
        list_all2_Cons1 list_all2_Cons2 dest: list_all2_lengthD) fastforce
qed

lemma mmulti_join'_opt_False:
  assumes "list_all2 (λA X. table n A X  wf_set n A)
    ((A_zs @ A_x # A_xs) @ (A_ws @ A_y # A_ys)) ((zs @ x # xs) @ (ws @ y # ys))"
    "length A_ws = length ws" "length A_xs = length xs"
    "length A_ys = length ys" "length A_zs = length zs"
    "A_y  A_x"
  shows "mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ (ws @ y # ys)) =
    mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ join x False y # xs) @ (ws @ ys))"
proof -
  have assms_dest: "table n A_x x" "table n A_y y" "wf_set n A_x" "wf_set n A_y"
    using assms
    by (auto simp del: mmulti_join'.simps simp add: list_all2_append dest: list_all2_lengthD)
  have tabs: "table n A_x (join x False y)"
    using join_table[of n A_x x A_y y False A_x, OF assms_dest(1,2) assms(6)] assms(6) by auto
  then have list_all2': "list_all2 (λA X. table n A X  wf_set n A)
    ((A_zs @ A_x # A_xs) @ (A_ws @ A_ys)) ((zs @ join x False y # xs) @ (ws @ ys))"
    using assms assms_dest(3)
    by (auto simp del: mmulti_join'.simps simp add: list_all2_append1 list_all2_append2
        list_all2_Cons1 list_all2_Cons2 dest: list_all2_lengthD) fastforce
  have res: "z. restrict A_x z  join x False y  restrict A_x z  x  restrict A_y z  y"
    using join_restrict[of x n A_x y A_y False, OF _ _ assms(6)] assms_dest(1,2) assms(6)
    by (auto simp add: table_def restrict_nested Int_absorb2 Un_absorb2)
  show ?thesis
  proof (rule set_eqI, rule iffI)
    fix z
    assume "z  mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys)
      ((zs @ x # xs) @ ws @ y # ys)"
    then have z_in_dest: "wf_tuple n ((set (A_zs @ A_x # A_xs))) z"
      "list_all2 (λA. (∈) (restrict A z)) A_zs zs"
      "restrict A_x z  x"
      "list_all2 (λA. (∈) (restrict A z)) A_xs xs"
      "list_all2 (λA. (∉) (restrict A z)) A_ws ws"
      "restrict A_y z  y"
      "list_all2 (λA. (∉) (restrict A z)) A_ys ys"
      using mmulti_join'_correct[OF _ assms(1), of z]
      by (auto simp del: mmulti_join'.simps simp add: assms list_all2_append1
          dest: list_all2_lengthD)
    then show "z  mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys)
      ((zs @ join x False y # xs) @ ws @ ys)"
      using mmulti_join'_correct[OF _ list_all2', of z] res
      by (auto simp add: assms list_all2_appendI Un_assoc simp del: mmulti_join'.simps
          dest: list_all2_lengthD)
  next
    fix z
    assume "z  mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_ys)
      ((zs @ join x False y # xs) @ ws @ ys)"
    then have z_in_dest: "wf_tuple n ((set (A_zs @ A_x # A_xs))) z"
      "list_all2 (λA. (∈) (restrict A z)) A_zs zs"
      "restrict A_x z  join x False y"
      "list_all2 (λA. (∈) (restrict A z)) A_xs xs"
      "list_all2 (λA. (∉) (restrict A z)) A_ws ws"
      "list_all2 (λA. (∉) (restrict A z)) A_ys ys"
      using mmulti_join'_correct[OF _ list_all2', of z]
      by (auto simp del: mmulti_join'.simps simp add: assms list_all2_append1
          dest: list_all2_lengthD)
    then show "z  mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys)
      ((zs @ x # xs) @ ws @ y # ys)"
      using mmulti_join'_correct[OF _ assms(1), of z] res
      by (auto simp add: assms list_all2_appendI Un_assoc simp del: mmulti_join'.simps
          dest: list_all2_lengthD)
  qed
qed

fun find_sub_in :: "'a set  'a set list  bool 
  ('a set list × 'a set × 'a set list) option" where
  "find_sub_in X [] b = None"
| "find_sub_in X (x # xs) b = (if (x  X  (b  X  x)) then Some ([], x, xs)
    else (case find_sub_in X xs b of None  None | Some (ys, z, zs)  Some (x # ys, z, zs)))"

lemma find_sub_in_sound: "find_sub_in X xs b = Some (ys, z, zs) 
  xs = ys @ z # zs  (z  X  (b  X  z))"
  by (induction X xs b arbitrary: ys z zs rule: find_sub_in.induct)
     (fastforce split: if_splits option.splits)+

fun find_sub_True :: "'a set list 
  ('a set list × 'a set × 'a set list × 'a set × 'a set list) option" where
  "find_sub_True [] = None"
| "find_sub_True (x # xs) = (case find_sub_in x xs True of None 
    (case find_sub_True xs of None  None
    | Some (ys, w, ws, z, zs)  Some (x # ys, w, ws, z, zs))
  | Some (ys, z, zs)  Some ([], x, ys, z, zs))"

lemma find_sub_True_sound: "find_sub_True xs = Some (ys, w, ws, z, zs) 
  xs = ys @ w # ws @ z # zs  (z  w  w  z)"
  using find_sub_in_sound
  by (induction xs arbitrary: ys w ws z zs rule: find_sub_True.induct)
     (fastforce split: option.splits)+

fun find_sub_False :: "'a set list  'a set list 
  (('a set list × 'a set × 'a set list) × ('a set list × 'a set × 'a set list)) option" where
  "find_sub_False [] ns = None"
| "find_sub_False (x # xs) ns = (case find_sub_in x ns False of None 
    (case find_sub_False xs ns of None  None
    | Some ((rs, w, ws), (ys, z, zs))  Some ((x # rs, w, ws), (ys, z, zs)))
  | Some (ys, z, zs)  Some (([], x, xs), (ys, z, zs)))"

lemma find_sub_False_sound: "find_sub_False xs ns = Some ((rs, w, ws), (ys, z, zs)) 
  xs = rs @ w # ws  ns = ys @ z # zs  (z  w)"
  using find_sub_in_sound
  by (induction xs ns arbitrary: rs w ws ys z zs rule: find_sub_False.induct)
     (fastforce split: option.splits)+

fun proj_list_3 :: "'a list  ('b list × 'b × 'b list)  ('a list × 'a × 'a list)" where
  "proj_list_3 xs (ys, z, zs) = (take (length ys) xs, xs ! (length ys),
    take (length zs) (drop (length ys + 1) xs))"

lemma proj_list_3_same:
  assumes "proj_list_3 xs (ys, z, zs) = (ys', z', zs')"
    "length xs = length ys + 1 + length zs"
  shows "xs = ys' @ z' # zs'"
  using assms by (auto simp add: id_take_nth_drop)

lemma proj_list_3_length:
  assumes "proj_list_3 xs (ys, z, zs) = (ys', z', zs')"
    "length xs = length ys + 1 + length zs"
  shows "length ys = length ys'" "length zs = length zs'"
  using assms by auto

fun proj_list_5 :: "'a list 
  ('b list × 'b × 'b list × 'b × 'b list) 
  ('a list × 'a × 'a list × 'a × 'a list)" where
  "proj_list_5 xs (ys, w, ws, z, zs) = (take (length ys) xs, xs ! (length ys),
    take (length ws) (drop (length ys + 1) xs), xs ! (length ys + 1 + length ws),
    drop (length ys + 1 + length ws + 1) xs)"

lemma proj_list_5_same:
  assumes "proj_list_5 xs (ys, w, ws, z, zs) = (ys', w', ws', z', zs')"
    "length xs = length ys + 1 + length ws + 1 + length zs"
  shows "xs = ys' @ w' # ws' @ z' # zs'"
proof -
  have "xs ! length ys # take (length ws) (drop (Suc (length ys)) xs) = take (Suc (length ws)) (drop (length ys) xs)"
    using assms(2) by (simp add: list_eq_iff_nth_eq nth_Cons split: nat.split)
  moreover have "take (Suc (length ws)) (drop (length ys) xs) @ drop (Suc (length ys + length ws)) xs =
      drop (length ys) xs"
    unfolding Suc_eq_plus1 add.assoc[of _ _ 1] add.commute[of _ "length ws + 1"]
      drop_drop[symmetric, of "length ws + 1"] append_take_drop_id ..
  ultimately show ?thesis
    using assms by (auto simp: Cons_nth_drop_Suc append_Cons[symmetric])
qed

lemma proj_list_5_length:
  assumes "proj_list_5 xs (ys, w, ws, z, zs) = (ys', w', ws', z', zs')"
    "length xs = length ys + 1 + length ws + 1 + length zs"
  shows "length ys = length ys'" "length ws = length ws'"
    "length zs = length zs'"
  using assms by auto

fun dominate_True :: "nat set list  'a table list 
  ((nat set list × nat set × nat set list × nat set × nat set list) ×
  ('a table list × 'a table × 'a table list × 'a table × 'a table list)) option" where
  "dominate_True A_pos L_pos = (case find_sub_True A_pos of None  None
  | Some split  Some (split, proj_list_5 L_pos split))"

lemma find_sub_True_proj_list_5_same:
  assumes "find_sub_True xs = Some (ys, w, ws, z, zs)" "length xs = length xs'"
    "proj_list_5 xs' (ys, w, ws, z, zs) = (ys', w', ws', z', zs')"
  shows "xs' = ys' @ w' # ws' @ z' # zs'"
proof -
  have len: "length xs' = length ys + 1 + length ws + 1 + length zs"
    using find_sub_True_sound[OF assms(1)] by (auto simp add: assms(2)[symmetric])
  show ?thesis
    using proj_list_5_same[OF assms(3) len] .
qed

lemma find_sub_True_proj_list_5_length:
  assumes "find_sub_True xs = Some (ys, w, ws, z, zs)" "length xs = length xs'"
    "proj_list_5 xs' (ys, w, ws, z, zs) = (ys', w', ws', z', zs')"
  shows "length ys = length ys'" "length ws = length ws'"
    "length zs = length zs'"
  using find_sub_True_sound[OF assms(1)] proj_list_5_length[OF assms(3)] assms(2) by auto

lemma dominate_True_sound:
  assumes "dominate_True A_pos L_pos = Some ((A_zs, A_x, A_xs, A_y, A_ys), (zs, x, xs, y, ys))"
    "length A_pos = length L_pos"
  shows "A_pos = A_zs @ A_x # A_xs @ A_y # A_ys" "L_pos = zs @ x # xs @ y # ys"
    "length A_xs = length xs" "length A_ys = length ys" "length A_zs = length zs"
  using assms find_sub_True_sound find_sub_True_proj_list_5_same find_sub_True_proj_list_5_length
  by (auto simp del: proj_list_5.simps split: option.splits) fast+

fun dominate_False :: "nat set list  'a table list  nat set list  'a table list 
  (((nat set list × nat set × nat set list) × nat set list × nat set × nat set list) ×
  (('a table list × 'a table × 'a table list) ×
  'a table list × 'a table × 'a table list)) option" where
  "dominate_False A_pos L_pos A_neg L_neg = (case find_sub_False A_pos A_neg of None  None
  | Some (pos_split, neg_split) 
    Some ((pos_split, neg_split), (proj_list_3 L_pos pos_split, proj_list_3 L_neg neg_split)))"

lemma find_sub_False_proj_list_3_same_left:
  assumes "find_sub_False xs ns = Some ((rs, w, ws), (ys, z, zs))"
    "length xs = length xs'" "proj_list_3 xs' (rs, w, ws) = (rs', w', ws')"
  shows "xs' = rs' @ w' # ws'"
proof -
  have len: "length xs' = length rs + 1 + length ws"
    using find_sub_False_sound[OF assms(1)] by (auto simp add: assms(2)[symmetric])
  show ?thesis
    using proj_list_3_same[OF assms(3) len] .
qed

lemma find_sub_False_proj_list_3_length_left:
  assumes "find_sub_False xs ns = Some ((rs, w, ws), (ys, z, zs))"
    "length xs = length xs'" "proj_list_3 xs' (rs, w, ws) = (rs', w', ws')"
  shows "length rs = length rs'" "length ws = length ws'"
  using find_sub_False_sound[OF assms(1)] proj_list_3_length[OF assms(3)] assms(2) by auto

lemma find_sub_False_proj_list_3_same_right:
  assumes "find_sub_False xs ns = Some ((rs, w, ws), (ys, z, zs))"
    "length ns = length ns'" "proj_list_3 ns' (ys, z, zs) = (ys', z', zs')"
  shows "ns' = ys' @ z' # zs'"
proof -
  have len: "length ns' = length ys + 1 + length zs"
    using find_sub_False_sound[OF assms(1)] by (auto simp add: assms(2)[symmetric])
  show ?thesis
    using proj_list_3_same[OF assms(3) len] .
qed

lemma find_sub_False_proj_list_3_length_right:
  assumes "find_sub_False xs ns = Some ((rs, w, ws), (ys, z, zs))"
    "length ns = length ns'" "proj_list_3 ns' (ys, z, zs) = (ys', z', zs')"
  shows "length ys = length ys'" "length zs = length zs'"
  using find_sub_False_sound[OF assms(1)] proj_list_3_length[OF assms(3)] assms(2) by auto

lemma dominate_False_sound:
  assumes "dominate_False A_pos L_pos A_neg L_neg =
    Some (((A_zs, A_x, A_xs), A_ws, A_y, A_ys), ((zs, x, xs), ws, y, ys))"
    "length A_pos = length L_pos" "length A_neg = length L_neg"
  shows "A_pos = (A_zs @ A_x # A_xs)" "A_neg = A_ws @ A_y # A_ys"
    "L_pos = (zs @ x # xs)" "L_neg = ws @ y # ys"
    "length A_ws = length ws" "length A_xs = length xs"
    "length A_ys = length ys" "length A_zs = length zs"
    "A_y  A_x"
  using assms find_sub_False_proj_list_3_same_left find_sub_False_proj_list_3_same_right
    find_sub_False_proj_list_3_length_left find_sub_False_proj_list_3_length_right
    find_sub_False_sound
  by (auto simp del: proj_list_3.simps split: option.splits) fast+

function mmulti_join :: "(nat  nat set list  nat set list  'a table list  'a table)" where
  "mmulti_join n A_pos A_neg L = (if length A_pos + length A_neg  length L then {} else
    let L_pos = take (length A_pos) L; L_neg = drop (length A_pos) L in
    (case dominate_True A_pos L_pos of None 
      (case dominate_False A_pos L_pos A_neg L_neg of None  mmulti_join' A_pos A_neg L
      | Some (((A_zs, A_x, A_xs), A_ws, A_y, A_ys), ((zs, x, xs), ws, y, ys)) 
        mmulti_join n (A_zs @ A_x # A_xs) (A_ws @ A_ys)
        ((zs @ bin_join n A_x x False A_y y # xs) @ (ws @ ys)))
    | Some ((A_zs, A_x, A_xs, A_y, A_ys), (zs, x, xs, y, ys)) 
      mmulti_join n (A_zs @ (A_x  A_y) # A_xs @ A_ys) A_neg
      ((zs @ bin_join n A_x x True A_y y # xs @ ys) @ L_neg)))"
  by pat_completeness auto
termination
  by (relation "measure (λ(n, A_pos, A_neg, L). length A_pos + length A_neg)")
    (use find_sub_True_sound find_sub_False_sound in fastforce split: option.splits›)+

lemma mmulti_join_link:
  assumes "A_pos  []"
      and "list_all2 (λA X. table n A X  wf_set n A) (A_pos @ A_neg) L"
    shows "mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L"
  using assms
proof (induction A_pos A_neg L rule: mmulti_join.induct)
  case (1 n A_pos A_neg L)
  define L_pos where "L_pos = take (length A_pos) L"
  define L_neg where "L_neg = drop (length A_pos) L"
  have L_def: "L = L_pos @ L_neg"
    using L_pos_def L_neg_def by auto
  have lens_match: "length A_pos = length L_pos" "length A_neg = length L_neg"
    using L_pos_def L_neg_def 1(4)[unfolded L_def] by (auto dest: list_all2_lengthD)
  then have lens_sum: "length A_pos + length A_neg = length L"
    by (auto simp add: L_def)
  show ?case
  proof (cases "dominate_True A_pos L_pos")
    case None
    note dom_True = None
    show ?thesis
    proof (cases "dominate_False A_pos L_pos A_neg L_neg")
      case None
      show ?thesis
        by (subst mmulti_join.simps)
           (simp del: dominate_True.simps dominate_False.simps mmulti_join.simps
            mmulti_join'.simps add: Let_def dom_True L_pos_def[symmetric] None
            L_neg_def[symmetric] lens_sum split: option.splits)
    next
      case (Some a)
      then obtain A_zs A_x A_xs A_ws A_y A_ys zs x xs ws y ys where
        dom_False: "dominate_False A_pos L_pos A_neg L_neg =
        Some (((A_zs, A_x, A_xs), A_ws, A_y, A_ys), ((zs, x, xs), ws, y, ys))"
        by (cases a) auto
      note list_all2 = 1(4)[unfolded L_def dominate_False_sound[OF dom_False lens_match]]
      have lens: "length A_ws = length ws" "length A_xs = length xs"
        "length A_ys = length ys" "length A_zs = length zs"
        using dominate_False_sound[OF dom_False lens_match] by auto
      have sub: "A_y  A_x"
        using dominate_False_sound[OF dom_False lens_match] by auto
      have list_all2': "list_all2 (λA X. table n A X  wf_set n A)
        ((A_zs @ A_x # A_xs) @ (A_ws @ A_ys)) ((zs @ join x False y # xs) @ (ws @ ys))"
        using list_all2_opt_False[OF list_all2 lens sub] .
      have tabs: "table n A_x x" "table n A_y y"
        using list_all2 by (auto simp add: lens list_all2_append)
      have bin_join_conv: "join x False y = bin_join n A_x x False A_y y"
        using bin_join_table[OF tabs, symmetric] .
      have mmulti: "mmulti_join n A_pos A_neg L = mmulti_join n (A_zs @ A_x # A_xs) (A_ws @ A_ys)
        ((zs @ bin_join n A_x x False A_y y # xs) @ (ws @ ys))"
        by (subst mmulti_join.simps)
           (simp del: dominate_True.simps dominate_False.simps mmulti_join.simps
            add: Let_def dom_True L_pos_def[symmetric] L_neg_def[symmetric] dom_False lens_sum)
      show ?thesis
        unfolding mmulti
        unfolding L_def dominate_False_sound[OF dom_False lens_match]
        by (rule 1(1)[OF _ L_pos_def L_neg_def dom_True dom_False,
            OF _ _ _ _ _ _ _ _ _ _ _ _ _ list_all2'[unfolded bin_join_conv],
            unfolded mmulti_join'_opt_False[OF list_all2 lens sub, symmetric,
            unfolded bin_join_conv]])
           (auto simp add: lens_sum)
    qed
  next
    case (Some a)
    then obtain A_zs A_x A_xs A_y A_ys zs x xs y ys where dom_True: "dominate_True A_pos L_pos =
      Some ((A_zs, A_x, A_xs, A_y, A_ys), (zs, x, xs, y, ys))"
      by (cases a) auto
    note list_all2 = 1(4)[unfolded L_def dominate_True_sound[OF dom_True lens_match(1)]]
    have lens: "length A_xs = length xs" "length A_ys = length ys" "length A_zs = length zs"
      using dominate_True_sound[OF dom_True lens_match(1)] by auto
    have list_all2': "list_all2 (λA X. table n A X  wf_set n A)
      ((A_zs @ (A_x  A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)"
      using list_all2_opt_True[OF list_all2 lens] .
    have tabs: "table n A_x x" "table n A_y y"
        using list_all2 by (auto simp add: lens list_all2_append)
    have bin_join_conv: "join x True y = bin_join n A_x x True A_y y"
      using bin_join_table[OF tabs, symmetric] .
    have mmulti: "mmulti_join n A_pos A_neg L = mmulti_join n (A_zs @ (A_x  A_y) # A_xs @ A_ys)
      A_neg ((zs @ bin_join n A_x x True A_y y # xs @ ys) @ L_neg)"
      by (subst mmulti_join.simps)
         (simp del: dominate_True.simps dominate_False.simps mmulti_join.simps
          add: Let_def dom_True L_pos_def[symmetric] L_neg_def lens_sum)
    show ?thesis
      unfolding mmulti
      unfolding L_def dominate_True_sound[OF dom_True lens_match(1)]
      by (rule 1(2)[OF _ L_pos_def L_neg_def dom_True,
          OF _ _ _ _ _ _ _ _ _ _ _ list_all2'[unfolded bin_join_conv],
          unfolded mmulti_join'_opt_True[OF list_all2 lens, symmetric,
          unfolded bin_join_conv]])
         (auto simp add: lens_sum)
  qed
qed

lemma mmulti_join_correct:
  assumes "A_pos  []"
      and "list_all2 (λA X. table n A X  wf_set n A) (A_pos @ A_neg) L"
  shows "z  mmulti_join n A_pos A_neg L  wf_tuple n (Aset A_pos. A) z 
    list_all2 (λA X. restrict A z  X) A_pos (take (length A_pos) L) 
    list_all2 (λA X. restrict A z  X) A_neg (drop (length A_pos) L)"
  unfolding mmulti_join_link[OF assms] using mmulti_join'_correct[OF assms] .

(*<*)
end
(*>*)

Theory Monitor

(*<*)
theory Monitor
  imports
    Formula
    Optimized_Join
    "MFOTL_Monitor.Abstract_Monitor"
    "HOL-Library.While_Combinator"
    "HOL-Library.Mapping"
    "Deriving.Derive"
    "Generic_Join.Generic_Join_Correctness"
begin
(*>*)

section ‹Generic monitoring algorithm›

text ‹The algorithm defined here abstracts over the implementation of the temporal operators.›

subsection ‹Monitorable formulas›

definition "mmonitorable φ  safe_formula φ  Formula.future_bounded φ"
definition "mmonitorable_regex b g r  safe_regex b g r  Regex.pred_regex Formula.future_bounded r"

definition is_simple_eq :: "Formula.trm  Formula.trm  bool" where
  "is_simple_eq t1 t2 = (Formula.is_Const t1  (Formula.is_Const t2  Formula.is_Var t2) 
    Formula.is_Var t1  Formula.is_Const t2)"

fun mmonitorable_exec :: "Formula.formula  bool" where
  "mmonitorable_exec (Formula.Eq t1 t2) = is_simple_eq t1 t2"
| "mmonitorable_exec (Formula.Neg (Formula.Eq (Formula.Var x) (Formula.Var y))) = (x = y)"
| "mmonitorable_exec (Formula.Pred e ts) = list_all (λt. Formula.is_Var t  Formula.is_Const t) ts"
| "mmonitorable_exec (Formula.Let p φ ψ) = ({0..<Formula.nfv φ}  Formula.fv φ  mmonitorable_exec φ  mmonitorable_exec ψ)"
| "mmonitorable_exec (Formula.Neg φ) = (fv φ = {}  mmonitorable_exec φ)"
| "mmonitorable_exec (Formula.Or φ ψ) = (fv φ = fv ψ  mmonitorable_exec φ  mmonitorable_exec ψ)"
| "mmonitorable_exec (Formula.And φ ψ) = (mmonitorable_exec φ 
    (safe_assignment (fv φ) ψ  mmonitorable_exec ψ 
      fv ψ  fv φ  (is_constraint ψ  (case ψ of Formula.Neg ψ'  mmonitorable_exec ψ' | _  False))))"
| "mmonitorable_exec (Formula.Ands l) = (let (pos, neg) = partition mmonitorable_exec l in
    pos  []  list_all mmonitorable_exec (map remove_neg neg) 
    (set (map fv neg))  (set (map fv pos)))"
| "mmonitorable_exec (Formula.Exists φ) = (mmonitorable_exec φ)"
| "mmonitorable_exec (Formula.Agg y ω b f φ) = (mmonitorable_exec φ 
    y + b  Formula.fv φ  {0..<b}  Formula.fv φ  Formula.fv_trm f  Formula.fv φ)"
| "mmonitorable_exec (Formula.Prev I φ) = (mmonitorable_exec φ)"
| "mmonitorable_exec (Formula.Next I φ) = (mmonitorable_exec φ)"
| "mmonitorable_exec (Formula.Since φ I ψ) = (Formula.fv φ  Formula.fv ψ 
    (mmonitorable_exec φ  (case φ of Formula.Neg φ'  mmonitorable_exec φ' | _  False))  mmonitorable_exec ψ)"
| "mmonitorable_exec (Formula.Until φ I ψ) = (Formula.fv φ  Formula.fv ψ  right I   
    (mmonitorable_exec φ  (case φ of Formula.Neg φ'  mmonitorable_exec φ' | _  False))  mmonitorable_exec ψ)"
| "mmonitorable_exec (Formula.MatchP I r) = Regex.safe_regex Formula.fv (λg φ<