section ‹Examples›

(*<*)
theory Examples
imports Restrict_Frees_Impl
begin
(*>*)

global_interpretation extra_cp: simplification cp cpropagated
  defines RB = "simplification.rb_impl_det cp"
      and assemble = "simplification.assemble cp"
      and SPLIT = "simplification.split_impl_det cp"
  by standard (auto simp only: sat_cp fv_cp rrb_cp gen_Gen_cp cpropagated_cp cpropagated_cp_triv
    cpropagated_sub Let_def is_Bool_def fv.simps cp.simps cpropagated_simps nocp.simps cpropagated_nocp split: if_splits)

subsection ‹Restricting Bounds in the "Suspicious Users" Query›

context
  fixes b s p u :: nat and B P S
  defines "b ≡ 0"
    and "s ≡ Suc 0"
    and "p ≡ Suc (Suc 0)"
    and "u ≡ Suc (Suc (Suc 0))"
    and "B ≡ λb. Pred ''B'' [Var b] :: (string, string) fmla"
    and "P ≡ λb p. Pred ''P'' [Var b, Var p] :: (string, string) fmla"
    and "S ≡ λp u s. Pred ''S'' [Var p, Var u, Var s] :: (string, string) fmla"
  notes cp.simps[simp del]
begin

definition Q_susp_user where
  "Q_susp_user = Conj (B b) (Exists s (Forall p (Impl (P b p) (S p u s))))"
definition Q_susp_user_rb :: "(string, string) fmla" where
  "Q_susp_user_rb = Conj (B b) (Disj (Exists s (Conj (Forall p (Impl (P b p) (S p u s))) (Exists p (S p u s)))) (Forall p (Neg (P b p))))"

lemma ex_rb_Q_susp_user: "the_res (RB Q_susp_user) = Q_susp_user_rb"
  by code_simp

end

subsection ‹Splitting a Disjunction of Predicates›

context
  fixes x y :: nat and B P
  defines "x ≡ 0"
    and "y ≡ 1"
    and "B ≡ λb. Pred ''B'' [Var b] :: (string, string) fmla"
    and "P ≡ λb p. Pred ''P'' [Var b, Var p] :: (string, string) fmla"
  notes cp.simps[simp del]
begin

definition Q_disj where
  "Q_disj = Disj (B x) (P x y)"
definition Q_disj_split_fin :: "(string, string) fmla" where
  "Q_disj_split_fin = Conj (Disj (B x) (P x y)) (P x y)"
definition Q_disj_split_inf :: "(string, string) fmla" where
  "Q_disj_split_inf = Exists x (B x)"

lemma ex_split_Q_disj: "the_res (SPLIT Q_disj) = (Q_disj_split_fin, Q_disj_split_inf)"
  by code_simp

end

subsection ‹Splitting a Conjunction with an Equality›

context
  fixes x u v :: nat and B
  defines "x ≡ 0"
    and "u ≡ 1"
    and "v ≡ 2"
    and "B ≡ λb. Pred ''B'' [Var b] :: (string, string) fmla"
  notes cp.simps[simp del]
begin

definition Q_eq where
  "Q_eq = Conj (B x) (u ≈ v)"
definition Q_eq_split_fin :: "(string, string) fmla" where
  "Q_eq_split_fin = Bool False"
definition Q_eq_split_inf :: "(string, string) fmla" where
  "Q_eq_split_inf = Exists x (B x)"

lemma ex_split_Q_eq: "the_res (SPLIT Q_eq) = (Q_eq_split_fin, Q_eq_split_inf)"
  by code_simp

end

subsection ‹Splitting the "Suspicious Users" Query›

context
  fixes b s p u :: nat and B P S
  defines "b ≡ 0"
    and "s ≡ Suc 0"
    and "p ≡ Suc (Suc 0)"
    and "u ≡ Suc (Suc (Suc 0))"
    and "B ≡ λb. Pred ''B'' [Var b] :: (string, string) fmla"
    and "P ≡ λb p. Pred ''P'' [Var b, Var p] :: (string, string) fmla"
    and "S ≡ λp u s. Pred ''S'' [Var p, Var u, Var s] :: (string, string) fmla"
  notes cp.simps[simp del]
begin

definition "Q_susp_user_split_fin = Conj Q_susp_user_rb (Exists s (Exists p (S p u s)))"
definition "Q_susp_user_split_inf = Exists b (Conj (B b) (Forall p (Neg (P b p))))"

lemma ex_split_Q_susp_user: "the_res (SPLIT Q_susp_user) = (Q_susp_user_split_fin, Q_susp_user_split_inf)"
  by code_simp

end

(*<*)
end
(*>*)