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

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 "∃s∈lpd 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 "∃s∈rpd 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: "∀x∈fv_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) = (⋃t∈set 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 ⋃x∈set 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 "∀i∈fvi (b + c) φ. i < n"
shows "∀i∈fvi 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 "∀i∈fvi (Suc b) φ. i < n"
shows "∀i∈fvi 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: "∀i∈fv φ. i < nfv φ"
unfolding nfv_def
by (auto simp add: Max_gr_iff intro: max.strict_coboundedI2)

lemma fvi_less_nfv_regex: "∀i∈fv_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 ψ) = (∃j≤i. mem (τ σ i - τ σ j) I ∧ sat σ V v j ψ ∧ (∀k ∈ {j <.. i}. sat σ V v k φ))"
| "sat σ V v i (Until φ I ψ) = (∃j≥i. mem (τ σ j - τ σ i) I ∧ sat σ V v j ψ ∧ (∀k ∈ {i ..< j}. sat σ V v k φ))"
| "sat σ V v i (MatchP I r) = (∃j≤i. mem (τ σ i - τ σ j) I ∧ Regex.match (sat σ V v) r j i)"
| "sat σ V v i (MatchF I r) = (∃j≥i. 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: "∀x∈fv φ. 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 "∀x∈fv φ. 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:
"∀x∈fv_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:
"∀x∈fv_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. x∈set 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) = (∀t∈set 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. ∀t∈set 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:
"∀x∈fv φ. 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 "∀x∈fv φ. 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: "(⋃x∈set neg. fv x) ⊆ (⋃x∈set pos. fv x)" using "1.prems" posneg by simp
then have "fv (Ands l) ⊆ (⋃x∈set pos. fv x)"
proof -
have "fv (Ands l) = (⋃x∈set pos. fv x) ∪ (⋃x∈set 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 "(⋃x∈set neg. fv x) ⊆ (⋃x∈set 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 "(⋃x∈set 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 "(⋃x∈set 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"
shows "wf_tuple n Y as"

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

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 (⋃A∈set 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 "(⋃A∈set 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›)+

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 (⋃A∈set 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 φ<