Theory Slicing

(*<*)
theory Slicing
  imports Abstract_Monitor MFOTL
begin
(*>*)

section ‹Slicing framework›

text ‹This section formalizes the abstract slicing framework and the joint data slicer
  presented in the article~\<^cite>‹‹Sections 4.2 and~4.3› in "SchneiderBBKT-STTT20"›.›

subsection ‹Abstract slicing›

subsubsection ‹Definition 1›

text ‹Corresponds to locale @{locale monitor} defined in theory
  @{theory MFOTL_Monitor.Abstract_Monitor}.›

subsubsection ‹Definition 2›

locale slicer = monitor +
  fixes submonitor :: "'k :: finite ⇒ 'a prefix ⇒ (nat × 'b option list) set"
  and   splitter :: "'a prefix ⇒ 'k ⇒ 'a prefix"
  and   joiner :: "('k ⇒ (nat × 'b option list) set) ⇒ (nat × 'b option list) set"
assumes mono_splitter: "π ≤ π' ⟹ splitter π k ≤ splitter π' k"
  and   correct_slicer: "joiner (λk. submonitor k (splitter π k)) = M π"
begin

lemmas sound_slicer = equalityD1[OF correct_slicer]
lemmas complete_slicer = equalityD2[OF correct_slicer]

end

locale self_slicer = slicer nfv fv sat M "λ_. M" splitter joiner for nfv fv sat M splitter joiner

subsubsection ‹Definition 3›

locale event_separable_splitter =
  fixes event_splitter :: "'a ⇒ 'k :: finite set"
begin

lift_definition splitter :: "'a prefix ⇒ 'k ⇒ 'a prefix" is
  "λπ k. map (λ(D, t). ({e ∈ D. k ∈ event_splitter e}, t)) π"
  by (auto simp: o_def split_beta)

subsubsection ‹Lemma 1›

lemma mono_splitter: "π ≤ π' ⟹ splitter π k ≤ splitter π' k"
  by transfer auto

end


subsection ‹Joint data slicer›

abbreviation (input) "ok φ v ≡ wf_tuple (MFOTL.nfv φ) (MFOTL.fv φ) v"

locale splitting_strategy =
  fixes φ :: "'a MFOTL.formula"
  and strategy :: "'a option list ⇒ 'k :: finite set"
  assumes strategy_nonempty: "ok φ v ⟹ strategy v ≠ {}"
begin

abbreviation slice_set where
  "slice_set k ≡ {v. ∃v'. map the v' = v ∧ ok φ v' ∧ k ∈ strategy v'}"

end

subsubsection ‹Definition 4›

locale MFOTL_monitor =
  monitor "MFOTL.nfv φ" "MFOTL.fv φ" "λσ v i. MFOTL.sat σ v i φ" M for φ M

locale joint_data_slicer = MFOTL_monitor φ M + splitting_strategy φ strategy
  for φ M strategy
begin

definition event_splitter where
  "event_splitter e = (⋃(strategy ` {v. ok φ v ∧ MFOTL.matches (map the v) φ e}))"

sublocale event_separable_splitter where event_splitter = event_splitter .

definition joiner where
  "joiner = (λs. ⋃k. s k ∩ (UNIV :: nat set) × {v. k ∈ strategy v})"

lemma splitter_pslice: "splitter π k = MFOTL_slicer.pslice φ (slice_set k) π"
  by transfer (auto simp: event_splitter_def)

subsubsection ‹Lemma 2›

text ‹Corresponds to the following theorem @{thm[source] sat_slice_strong} proved in theory
   @{theory MFOTL_Monitor.Abstract_Monitor}:

   @{thm sat_slice_strong[no_vars]}›

subsubsection ‹Theorem 1›

sublocale joint_monitor: MFOTL_monitor φ "λπ. joiner (λk. M (splitter π k))"
proof (unfold_locales, goal_cases mono wf sound complete)
  case (mono π π')
  show ?case
    using mono_monitor[OF mono_splitter, OF mono]
    by (auto simp: joiner_def)
next
  case (wf i v π)
  then obtain k where in_M: "(i, v) ∈ M (splitter π k)"  and k: "k ∈ strategy v"
    unfolding joiner_def by (auto split: if_splits)
  then show ?case
    using wf_monitor[OF in_M] by auto
next
  case (sound i v π σ)
  then obtain k where in_M: "(i, v) ∈ M (splitter π k)"  and k: "k ∈ strategy v"
    unfolding joiner_def by (auto split: if_splits)
  have wf: "ok φ v" and sat: "⋀σ. prefix_of (splitter π k) σ ⟹ MFOTL.sat σ (map the v) i φ"
    using sound_monitor[OF in_M] wf_monitor[OF in_M] by auto
  then have "MFOTL.sat σ (map the v) i φ" if "prefix_of π σ" for σ
    using that k
    by (intro iffD2[OF sat_slice_iff[of "map the v" "slice_set k" σ i φ]])
      (auto simp: wf_tuple_def fvi_less_nfv splitter_pslice intro!: exI[of _ v] prefix_of_pmap_Γ)
  then show ?case using sound(2) by blast
next
  case (complete π σ v i)
  with strategy_nonempty obtain k where k: "k ∈ strategy v" by blast
  have "MFOTL.sat σ' (map the v) i φ" if "prefix_of (MFOTL_slicer.pslice φ (slice_set k) π) σ'" for σ'
  proof -
    have "MFOTL.sat σ' (map the v) i φ = MFOTL.sat (MFOTL_slicer.slice φ (slice_set k) σ') (map the v) i φ"
      using complete(2) k by (auto intro!: sat_slice_iff)
    also have "… = MFOTL.sat (MFOTL_slicer.slice φ (slice_set k) (replace_prefix π σ')) (map the v) i φ"
      using that complete k by (subst slice_replace_prefix[symmetric]; simp)
    also have "… = MFOTL.sat (replace_prefix π σ') (map the v) i φ"
      using complete(2) k by (auto intro!: sat_slice_iff[symmetric])
    also have "…"
      by (rule complete(3)[rule_format], rule prefix_of_replace_prefix[OF that])
    finally show ?thesis .
  qed
  with complete(1-3) obtain π' where π':
    "prefix_of π' (MFOTL_slicer.slice φ (slice_set k) σ)" "(i, v) ∈ M π'"
    by (atomize_elim, intro complete_monitor[where π="MFOTL_slicer.pslice φ (slice_set k) π"])
      (auto simp: splitter_pslice intro!: prefix_of_pmap_Γ)
  from π'(1) obtain π'' where "π' = MFOTL_slicer.pslice φ (slice_set k) π''" "prefix_of π'' σ"
    by (atomize_elim, rule prefix_of_map_Γ_D)
  with π' k show ?case
    by (intro exI[of _ π'']) (auto simp: joiner_def splitter_pslice intro!: exI[of _ k])
qed

subsubsection ‹Corollary 1›

sublocale joint_slicer: slicer "MFOTL.nfv φ" "MFOTL.fv φ" "λσ v i. MFOTL.sat σ v i φ"
  "λπ. joiner (λk. M (splitter π k))" "λ_. M" splitter joiner
  by standard (auto simp: mono_splitter)

end

subsubsection ‹Definition 5›

text ‹Corresponds to locale @{locale sliceable_monitor} defined in theory
  @{theory MFOTL_Monitor.Abstract_Monitor}.›

locale slicable_joint_data_slicer =
  sliceable_monitor "MFOTL.nfv φ" "MFOTL.fv φ" "relevant_events φ" "λσ v i. MFOTL.sat σ v i φ" M +
  joint_data_slicer φ M strategy for φ M strategy
begin

lemma monitor_split: "ok φ v ⟹ k ∈ strategy v ⟹ (i, v) ∈ M (splitter π k) ⟷ (i, v) ∈ M π"
  unfolding splitter_pslice
  by (rule sliceable_M)
    (auto simp: wf_tuple_def fvi_less_nfv intro!: mem_restrI[rotated 2, where y="map the v"])

subsubsection ‹Theorem 2›

sublocale self_slicer "MFOTL.nfv φ" "MFOTL.fv φ" "λσ v i. MFOTL.sat σ v i φ" M splitter joiner
proof (standard, erule mono_splitter, safe, goal_cases sound complete)
  case (sound π i v)
  have "ok φ v" using joint_monitor.wf_monitor[OF sound] by auto
  from sound obtain k where "(i, v) ∈ M (splitter π k)" "k ∈ strategy v"
    unfolding joiner_def by blast
  with ‹ok φ v› show ?case by (simp add: monitor_split)
next
  case (complete π i v)
  have "ok φ v" using wf_monitor[OF complete] by auto
  with complete strategy_nonempty obtain k where k: "k ∈ strategy v" by blast
  then have "(i, v) ∈ M (splitter π k)" using complete ‹ok φ v› by (simp add: monitor_split)
  with k show ?case unfolding joiner_def by blast
qed

end

subsubsection ‹Towards Theorem 3›

fun names :: "'a MFOTL.formula ⇒ MFOTL.name set" where
  "names (MFOTL.Pred e _) = {e}"
| "names (MFOTL.Eq _ _) = {}"
| "names (MFOTL.Neg ψ) = names ψ"
| "names (MFOTL.Or α β) = names α ∪ names β"
| "names (MFOTL.Exists ψ) = names ψ"
| "names (MFOTL.Prev I ψ) = names ψ"
| "names (MFOTL.Next I ψ) = names ψ"
| "names (MFOTL.Since α I β) = names α ∪ names β"
| "names (MFOTL.Until α I β) = names α ∪ names β"

fun gen_unique :: "'a MFOTL.formula ⇒ bool" where
  "gen_unique (MFOTL.Pred _ _) = True"
| "gen_unique (MFOTL.Eq (MFOTL.Var _) (MFOTL.Const _)) = False"
| "gen_unique (MFOTL.Eq (MFOTL.Const _) (MFOTL.Var _)) = False"
| "gen_unique (MFOTL.Eq _ _) = True"
| "gen_unique (MFOTL.Neg ψ) = gen_unique ψ"
| "gen_unique (MFOTL.Or α β) = (gen_unique α ∧ gen_unique β ∧ names α ∩ names β = {})"
| "gen_unique (MFOTL.Exists ψ) = gen_unique ψ"
| "gen_unique (MFOTL.Prev I ψ) = gen_unique ψ"
| "gen_unique (MFOTL.Next I ψ) = gen_unique ψ"
| "gen_unique (MFOTL.Since α I β) = (gen_unique α ∧ gen_unique β ∧ names α ∩ names β = {})"
| "gen_unique (MFOTL.Until α I β) = (gen_unique α ∧ gen_unique β ∧ names α ∩ names β = {})"

lemma sat_inter_names_cong: "(⋀e. e ∈ names φ ⟹ {xs. (e, xs) ∈ E} = {xs. (e, xs) ∈ F}) ⟹
  MFOTL.sat (map_Γ (λD. D ∩ E) σ) v i φ ⟷ MFOTL.sat (map_Γ (λD. D ∩ F) σ) v i φ"
  by (induction φ arbitrary: v i) (auto split: nat.splits)

lemma matches_in_names: "MFOTL.matches v φ x ⟹ fst x ∈ names φ"
  by (induction φ arbitrary: v) (auto)

lemma unique_names_matches_absorb: "fst x ∈ names α ⟹ names α ∩ names β = {} ⟹
    MFOTL.matches v α x ∨ MFOTL.matches v β x ⟷ MFOTL.matches v α x"
  "fst x ∈ names β ⟹ names α ∩ names β = {} ⟹
    MFOTL.matches v α x ∨ MFOTL.matches v β x ⟷ MFOTL.matches v β x"
  by (auto dest: matches_in_names)

definition mergeable_envs where
  "mergeable_envs n S ⟷ (∀v1∈S. ∀v2∈S. (∀A B f.
    (∀x∈A. x < n ∧ v1 ! x = f x) ∧ (∀x∈B. x < n ∧ v2 ! x = f x) ⟶
    (∃v∈S. ∀x∈A ∪ B. v ! x = f x)))"

lemma mergeable_envsI:
  assumes "⋀v1 v2 v. v1 ∈ S ⟹ v2 ∈ S ⟹ length v = n ⟹ ∀x < n. v ! x = v1 ! x ∨ v ! x = v2 ! x ⟹ v ∈ S"
  shows "mergeable_envs n S"
  unfolding mergeable_envs_def
proof (safe, goal_cases mergeable)
  case [simp]: (mergeable v1 v2 A B f)
  let ?v = "tabulate (λx. if x ∈ A ∪ B then f x else v1 ! x) 0 n"
  from assms[of v1 v2 ?v, simplified] show ?case
    by (auto intro!: bexI[of _ ?v])
qed

lemma in_listset_nth: "x ∈ listset As ⟹ i < length As ⟹ x ! i ∈ As ! i"
  by (induction As arbitrary: x i) (auto simp: set_Cons_def nth_Cons split: nat.split)

lemma all_nth_in_listset: "length x = length As ⟹ (⋀i. i < length As ⟹ x ! i ∈ As ! i) ⟹ x ∈ listset As"
  by (induction x As rule: list_induct2) (fastforce simp: set_Cons_def nth_Cons)+

lemma mergeable_envs_listset: "mergeable_envs (length As) (listset As)"
  by (rule mergeable_envsI) (auto intro!: all_nth_in_listset elim!: in_listset_nth)

lemma mergeable_envs_Ex: "mergeable_envs n S ⟹ MFOTL.nfv α ≤ n ⟹ MFOTL.nfv β ≤ n ⟹
  (∃v'∈S. ∀x∈fv α. v' ! x = v ! x) ⟹ (∃v'∈S. ∀x∈fv β. v' ! x = v ! x) ⟹
  (∃v'∈S. ∀x∈fv α ∪ fv β. v' ! x = v ! x)"
proof (clarify, goal_cases mergeable)
  case (mergeable v1 v2)
  then show ?case
    by (auto intro: order.strict_trans2[OF fvi_less_nfv[rule_format]]
      elim!: mergeable_envs_def[THEN iffD1, rule_format, of _ _ v1 v2])
qed

lemma in_set_ConsE: "xs ∈ set_Cons A As ⟹ (⋀y ys. xs = y # ys ⟹ y ∈ A ⟹ ys ∈ As ⟹ P) ⟹ P"
  unfolding set_Cons_def by blast

lemma mergeable_envs_set_Cons: "mergeable_envs n S ⟹ mergeable_envs (Suc n) (set_Cons UNIV S)"
  unfolding mergeable_envs_def
proof (clarify, elim in_set_ConsE, goal_cases mergeable)
  case (mergeable v1 v2 A B f y1 ys1 y2 ys2)
  let ?A = "(λx. x - 1) ` (A - {0})"
  let ?B = "(λx. x - 1) ` (B - {0})"
  from mergeable(4-9) have "∃v ∈ S. ∀x∈?A ∪ ?B. v ! x = f (Suc x)"
    by (auto dest!: mergeable(2,3)[rule_format] intro!: mergeable(1)[rule_format, of ys1 ys2])
  then obtain v where "v ∈ S" "∀x∈?A ∪ ?B. v ! x = f (Suc x)" by blast
  then show ?case
    by (intro bexI[of _ "f 0 # v"]) (auto simp: nth_Cons' set_Cons_def)
qed

lemma slice_Exists: "MFOTL_slicer.slice (MFOTL.Exists φ) S σ = MFOTL_slicer.slice φ (set_Cons UNIV S) σ"
  by (auto simp: set_Cons_def intro: map_Γ_cong)

lemma image_Suc_fvi: "Suc ` MFOTL.fvi (Suc b) φ = MFOTL.fvi b φ - {0}"
  by (auto simp: image_def Bex_def MFOTL.fvi_Suc dest: gr0_implies_Suc)

lemma nfv_Exists: "MFOTL.nfv (MFOTL.Exists φ) = MFOTL.nfv φ - 1"
  unfolding MFOTL.nfv_def
  by (cases "fv φ = {}") (auto simp add: image_Suc_fvi mono_Max_commute[symmetric] mono_def)

lemma set_Cons_empty_iff[simp]: "set_Cons A Xs = {} ⟷ A = {} ∨ Xs = {}"
  unfolding set_Cons_def by auto

lemma unique_sat_slice_mem: "safe_formula φ ⟹ gen_unique φ ⟹ S ≠ {} ⟹
  mergeable_envs n S ⟹ MFOTL.nfv φ ≤ n ⟹
  MFOTL.sat (MFOTL_slicer.slice φ S σ) v i φ ⟹ ∃v'∈S. ∀x∈fv φ. v' ! x = v ! x"
proof (induction arbitrary: v i S n rule: safe_formula_induct)
  case (1 t1 t2)
  then show ?case by (cases "t2") (auto simp: MFOTL.is_Const_def)
next
  case (2 t1 t2)
  then show ?case by (cases "t1") (auto simp: MFOTL.is_Const_def)
next
  case (3 x y)
  then show ?case by auto
next
  case (4 x y)
  then show ?case by simp
next
  case (5 e ts)
  then obtain v' where "v' ∈ S" and eq: "∀t∈set ts. MFOTL.eval_trm v' t = MFOTL.eval_trm v t"
    by auto
  have "∀t∈set ts. ∀x∈fv_trm t. v' ! x = v ! x" proof
    fix t assume "t ∈ set ts"
    with eq have "MFOTL.eval_trm v' t = MFOTL.eval_trm v t" ..
    then show "∀x∈fv_trm t. v' ! x = v ! x" by (cases t) (simp_all)
  qed
  with ‹v' ∈ S› show ?case by auto
next
  case (6 φ ψ)
  from ‹gen_unique (MFOTL.And φ ψ)›
  have
    "MFOTL.sat (MFOTL_slicer.slice (MFOTL.And φ ψ) S σ) v i φ = MFOTL.sat (MFOTL_slicer.slice φ S σ) v i φ"
    "MFOTL.sat (MFOTL_slicer.slice (MFOTL.And φ ψ) S σ) v i ψ = MFOTL.sat (MFOTL_slicer.slice ψ S σ) v i ψ"
    unfolding MFOTL.And_def
    by (fastforce simp: unique_names_matches_absorb intro!: sat_inter_names_cong)+
  with 6(1,4-) 6(2,3)[where S=S] show ?case
    unfolding MFOTL.And_def
    by (auto intro!: mergeable_envs_Ex)
next
  case (7 φ ψ)
  from ‹gen_unique (MFOTL.And_Not φ ψ)›
  have "MFOTL.sat (MFOTL_slicer.slice (MFOTL.And_Not φ ψ) S σ) v i φ = MFOTL.sat (MFOTL_slicer.slice φ S σ) v i φ"
    unfolding MFOTL.And_Not_def
    by (fastforce simp: unique_names_matches_absorb intro!: sat_inter_names_cong)
  with 7(1,2,5-) 7(3)[where S=S] have "∃v'∈S. ∀x∈fv φ. v' ! x = v ! x"
    unfolding MFOTL.And_Not_def by auto
  with ‹fv ψ ⊆ fv φ› show ?case by (auto simp: MFOTL.fvi_And_Not)
next
  case (8 φ ψ)
  from ‹gen_unique (MFOTL.Or φ ψ)›
  have
    "MFOTL.sat (MFOTL_slicer.slice (MFOTL.Or φ ψ) S σ) v i φ = MFOTL.sat (MFOTL_slicer.slice φ S σ) v i φ"
    "MFOTL.sat (MFOTL_slicer.slice (MFOTL.Or φ ψ) S σ) v i ψ = MFOTL.sat (MFOTL_slicer.slice ψ S σ) v i ψ"
    by (fastforce simp: unique_names_matches_absorb intro!: sat_inter_names_cong)+
  with 8(1,4-) 8(2,3)[where S=S] have "∃v'∈S. ∀x∈fv φ. v' ! x = v ! x"
    by (auto simp: ‹fv ψ = fv φ›)
  then show ?case by (auto simp: ‹fv ψ = fv φ›)
next
  case (9 φ)
  then obtain z where sat_φ: "MFOTL.sat (MFOTL_slicer.slice (MFOTL.Exists φ) S σ) (z # v) i φ"
    by auto
  from "9.prems" sat_φ have "∃v'∈set_Cons UNIV S. ∀x∈fv φ. v' ! x = (z # v) ! x"
    unfolding slice_Exists
    by (intro "9.IH") (auto simp: nfv_Exists intro!: mergeable_envs_set_Cons)
  then show ?case
    by (auto simp: set_Cons_def fvi_Suc Ball_def nth_Cons split: nat.splits)
next
  case (10 I φ)
  then obtain j where "MFOTL.sat (MFOTL_slicer.slice φ S σ) v j φ"
    by (auto split: nat.splits)
  with 10 show ?case by simp
next
  case (11 I φ)
  then obtain j where "MFOTL.sat (MFOTL_slicer.slice φ S σ) v j φ"
    by (auto split: nat.splits)
  with 11 show ?case by simp
next
  case (12 φ I ψ)
  from ‹gen_unique (MFOTL.Since φ I ψ)›
  have *:
    "MFOTL.sat (MFOTL_slicer.slice (MFOTL.Since φ I ψ) S σ) v j ψ = MFOTL.sat (MFOTL_slicer.slice ψ S σ) v j ψ" for j
    by (fastforce simp: unique_names_matches_absorb intro!: sat_inter_names_cong)
  from 12 obtain j where "MFOTL.sat (MFOTL_slicer.slice (MFOTL.Since φ I ψ) S σ) v j ψ"
    by auto
  with 12 have "∃v'∈S. ∀x∈fv ψ. v' ! x = v ! x" using * by auto
  with ‹fv φ ⊆ fv ψ› show ?case by auto
next
  case (13 φ I ψ)
  from ‹gen_unique (MFOTL.Since (MFOTL.Neg φ) I ψ)›
  have *:
    "MFOTL.sat (MFOTL_slicer.slice (MFOTL.Since (MFOTL.Neg φ) I ψ) S σ) v j ψ = MFOTL.sat (MFOTL_slicer.slice ψ S σ) v j ψ" for j
    by (fastforce simp: unique_names_matches_absorb intro!: sat_inter_names_cong)
  from 13 obtain j where "MFOTL.sat (MFOTL_slicer.slice (MFOTL.Since (MFOTL.Neg φ) I ψ) S σ) v j ψ"
    by auto
  with 13 have "∃v'∈S. ∀x∈fv ψ. v' ! x = v ! x" using * by auto
  with ‹fv (MFOTL.Neg φ) ⊆ fv ψ› show ?case by auto
next
  case (14 φ I ψ)
  from ‹gen_unique (MFOTL.Until φ I ψ)›
  have *:
    "MFOTL.sat (MFOTL_slicer.slice (MFOTL.Until φ I ψ) S σ) v j ψ = MFOTL.sat (MFOTL_slicer.slice ψ S σ) v j ψ" for j
    by (fastforce simp: unique_names_matches_absorb intro!: sat_inter_names_cong)
  from 14 obtain j where "MFOTL.sat (MFOTL_slicer.slice (MFOTL.Until φ I ψ) S σ) v j ψ"
    by auto
  with 14 have "∃v'∈S. ∀x∈fv ψ. v' ! x = v ! x" using * by auto
  with ‹fv φ ⊆ fv ψ› show ?case by auto
next
  case (15 φ I ψ)
  from ‹gen_unique (MFOTL.Until (MFOTL.Neg φ) I ψ)›
  have *:
    "MFOTL.sat (MFOTL_slicer.slice (MFOTL.Until (MFOTL.Neg φ) I ψ) S σ) v j ψ = MFOTL.sat (MFOTL_slicer.slice ψ S σ) v j ψ" for j
    by (fastforce simp: unique_names_matches_absorb intro!: sat_inter_names_cong)
  from 15 obtain j where "MFOTL.sat (MFOTL_slicer.slice (MFOTL.Until (MFOTL.Neg φ) I ψ) S σ) v j ψ"
    by auto
  with 15 have "∃v'∈S. ∀x∈fv ψ. v' ! x = v ! x" using * by auto
  with ‹fv (MFOTL.Neg φ) ⊆ fv ψ› show ?case by auto
qed

lemma unique_sat_slice:
  assumes formula: "safe_formula φ" "gen_unique φ"
      and restr: "S ≠ {}" "mergeable_envs (MFOTL.nfv φ) S"
      and sat_slice: "MFOTL.sat (MFOTL_slicer.slice φ S σ) v i φ"
    shows "MFOTL.sat σ v i φ"
proof -
  obtain v' where "v' ∈ S" and fv_eq: "∀x∈fv φ. v' ! x = v ! x"
    using unique_sat_slice_mem[OF formula restr order_refl sat_slice] ..
  with sat_slice have "MFOTL.sat (MFOTL_slicer.slice φ S σ) v' i φ"
    by (auto iff: sat_fvi_cong)
  then have "MFOTL.sat σ v' i φ"
    unfolding sat_slice_iff[OF ‹v' ∈ S›, symmetric] .
  with fv_eq show ?thesis by (auto iff: sat_fvi_cong)
qed

subsubsection ‹Lemma 3›

lemma (in splitting_strategy) unique_sat_strategy:
  "safe_formula φ ⟹ gen_unique φ ⟹ slice_set k ≠ {} ⟹
  mergeable_envs (MFOTL.nfv φ) (slice_set k) ⟹
  MFOTL.sat (MFOTL_slicer.slice φ (slice_set k) σ) (map the v) i φ ⟹
  ok φ v ⟹ k ∈ strategy v"
  by (drule (3) unique_sat_slice_mem) (auto dest: wf_tuple_cong)

locale skip_inter = joint_data_slicer +
  assumes nonempty: "slice_set k ≠ {}"
  and mergeable: "mergeable_envs (MFOTL.nfv φ) (slice_set k)"
begin

subsubsection ‹Definition of J'›

definition "skip_joiner = (λs. ⋃k. s k)"

subsubsection ‹Theorem 3›

lemma skip_joiner:
  assumes "safe_formula φ" "gen_unique φ"
  shows "joiner (λk. M (splitter π k)) = skip_joiner (λk. M (splitter π k))"
  (is "?L = ?R")
proof safe
  fix i v
  assume "(i, v) ∈ ?R"
  then obtain k where in_M: "(i, v) ∈ M (splitter π k)"
  unfolding skip_joiner_def by blast
  from ex_prefix_of obtain σ where "prefix_of π σ" by blast
  with wf_monitor[OF in_M] sound_monitor[OF in_M] have
    "MFOTL.sat (MFOTL_slicer.slice φ (slice_set k) σ) (map the v) i φ" "ok φ v"
    by (auto simp: splitter_pslice intro!: prefix_of_pmap_Γ)
  note unique_sat_strategy[OF assms nonempty mergeable this]
  with in_M show "(i, v) ∈ ?L" unfolding joiner_def by blast
qed (auto simp: joiner_def skip_joiner_def)

sublocale skip_joint_monitor: MFOTL_monitor φ
  "λπ. (if safe_formula φ ∧ gen_unique φ then skip_joiner else joiner) (λk. M (splitter π k))"
  using joint_monitor.mono_monitor joint_monitor.wf_monitor joint_monitor.sound_monitor joint_monitor.complete_monitor
  by unfold_locales (auto simp: skip_joiner[symmetric] split: if_splits)

end

(*<*)
end
(*>*)