Theory Generic_Join

section ‹The algorithm›

theory Generic_Join
  imports MFOTL_Monitor.Table
begin

type_synonym 'a atable = "nat set × 'a table"
type_synonym 'a query = "'a atable set"
type_synonym vertices = "nat set"

subsection ‹Generic algorithm›

locale getIJ =
  fixes getIJ :: "'a query  'a query  vertices  vertices × vertices"
  assumes coreProperties: "card V  2  getIJ Q_pos Q_neg V = (I, J) 
    card I  1  card J  1  V = I  J  I  J = {}"
begin

lemma getIJProperties:
  assumes "card V  2"
  assumes "(I, J) = getIJ Q_pos Q_neg V"
  shows "card I  1" and "card J  1" and "card I < card V" and "card J < card V"
    and "V = I  J" and "I  J = {}"
proof -
  show "1  card I" using coreProperties[of V Q_pos Q_neg I J] assms by auto
  show "1  card J" using coreProperties[of V Q_pos Q_neg I J] assms by auto
  show "card I < card V" by (metis (no_types, lifting) Int_ac(3) One_nat_def Suc_le_lessD assms(1)
        assms(2) card_gt_0_iff card_seteq dual_order.trans getIJ.coreProperties getIJ_axioms leI
        le_iff_inf one_le_numeral sup_ge1 sup_ge2)
  show "card J < card V" by (metis One_nat_def Suc_1 assms(1) assms(2) card_gt_0_iff card_seteq
        getIJ.coreProperties getIJ_axioms leI le_0_eq le_iff_inf nat.simps(3) sup_ge1 sup_ge2)
  show "V = I  J" by (metis assms(1) assms(2) getIJ.coreProperties getIJ_axioms)
  show "I  J = {}" by (metis assms(1) assms(2) getIJ_axioms getIJ_def)
qed

fun projectTable :: "vertices  'a atable  'a atable" where
  "projectTable V (s, t) = (s  V, Set.image (restrict V) t)"

fun filterQuery :: "vertices  'a query  'a query" where
  "filterQuery V Q = Set.filter (λ(s, _). ¬ Set.is_empty (s  V)) Q"

fun filterQueryNeg :: "vertices  'a query  'a query" where
  "filterQueryNeg V Q = Set.filter (λ(A, _). A  V) Q"

fun projectQuery :: "vertices  'a query  'a query" where
  "projectQuery V s = Set.image (projectTable V) s"

fun isSameIntersection :: "'a tuple  nat set  'a tuple  bool" where
  "isSameIntersection t1 s t2 = (is. t1!i = t2!i)"

fun semiJoin :: "'a atable  (nat set × 'a tuple)  'a atable" where
  "semiJoin (s, tab) (st, tup) = (s, Set.filter (isSameIntersection tup (s  st)) tab)"

fun newQuery :: "vertices  'a query  (nat set × 'a tuple)  'a query" where
  "newQuery V Q (st, t) = Set.image (λtab. projectTable V (semiJoin tab (st, t))) Q"

fun merge_option :: "'a option × 'a option  'a option" where
  "merge_option (None, None) = None"
| "merge_option (Some x, None) = Some x"
| "merge_option (None, Some x) = Some x"
| "merge_option (Some a, Some b) = Some a"
(* Last case shouldn't happen but useful for proof *)

fun merge :: "'a tuple  'a tuple  'a tuple" where
  "merge t1 t2 = map merge_option (zip t1 t2)"

function (sequential) genericJoin :: "vertices  'a query  'a query  'a table" where
  "genericJoin V Q_pos Q_neg =
    (if card V  1 then
      ((_, x)  Q_pos. x) - ((_, x)  Q_neg. x)
    else
      let (I, J) = getIJ Q_pos Q_neg V in
      let Q_I_pos = projectQuery I (filterQuery I Q_pos) in
      let Q_I_neg = filterQueryNeg I Q_neg in
      let R_I = genericJoin I Q_I_pos Q_I_neg in
      let Q_J_neg = Q_neg - Q_I_neg in
      let Q_J_pos = filterQuery J Q_pos in
      let X = {(t, genericJoin J (newQuery J Q_J_pos (I, t)) (newQuery J Q_J_neg (I, t))) | t . t  R_I} in
      ((t, x)  X. {merge xx t | xx . xx  x}))"
by pat_completeness auto
termination
  by (relation "measure (λ(V, Q_pos, Q_neg). card V)") (auto simp add: getIJProperties)

fun wrapperGenericJoin :: "'a query  'a query  'a table" where
  "wrapperGenericJoin Q_pos Q_neg =
    (if (((A, X)Q_pos. Set.is_empty X)  ((A, X)Q_neg. Set.is_empty A  ¬ Set.is_empty X)) then
      {}
    else
      let Q = Set.filter (λ(A, _). ¬ Set.is_empty A) Q_pos in
      if Set.is_empty Q then
        ((A, X)Q_pos. X) -  ((A, X)Q_neg. X)
      else
        let V = ((A, X)Q. A) in
        let Qn = Set.filter (λ(A, _). A  V  card A  1) Q_neg in
        genericJoin V Q Qn)"

end

subsection ‹An instantation›

fun score :: "'a query  nat  nat" where
  "score Q i = (let relevant = Set.image (λ(_, x). card x) (Set.filter (λ(sign, _). i  sign) Q) in
    let l = sorted_list_of_set relevant in
    foldl (+) 0 l
)"

fun arg_max_list :: "('a  nat)  'a list  'a" where
  "arg_max_list f l = (let m = Max (set (map f l)) in arg_min_list (λx. m - f x) l)"

lemma arg_max_list_element:
  assumes "length l  1" shows "arg_max_list f l  set l"
  by (metis One_nat_def arg_max_list.simps arg_min_list_in assms le_imp_less_Suc less_irrefl list.size(3))

fun max_getIJ :: "'a query  'a query  vertices  vertices × vertices" where
  "max_getIJ Q_pos Q_neg V = (
  let l = sorted_list_of_set V in
  if Set.is_empty Q_neg then
    let x = arg_max_list (score Q_pos) l in
    ({x}, V - {x})
  else
    let x = arg_max_list (score Q_neg) l in
    (V - {x}, {x}))"

lemma max_getIJ_coreProperties:
  assumes "card V  2"
  assumes "(I, J) = max_getIJ Q_pos Q_neg V"
  shows "card I  1  card J  1  V = I  J  I  J = {}"
proof -
  have "finite V" using assms(1) card.infinite by force
  define l where "l = sorted_list_of_set V"
  then have "length l  1" by (metis Suc_1 Suc_le_lessD finite V assms(1) distinct_card
        distinct_sorted_list_of_set less_imp_le set_sorted_list_of_set)
  show ?thesis
  proof (cases "Set.is_empty Q_neg")
    case True
    define x where "x = arg_max_list (score Q_pos) l"
    then have "x  (set l)" using 1  length l arg_max_list_element by blast
    then have "x  V" by (simp add: finite V l_def)
    moreover have "(I, J) = ({x}, V - {x})" 
    proof -
      have "(I, J) =  (let l = sorted_list_of_set V in
    let x = arg_max_list (score Q_pos) l in
    ({x}, V - {x}))" by (simp add: True assms(2))
      then show ?thesis by (metis l_def x_def)
    qed
    then show ?thesis using Pair_inject finite V assms(1) calculation by auto
  next
    case False
    define x where "x = arg_max_list (score Q_neg) l"
    then have "x  (set l)" using 1  length l arg_max_list_element by blast
    then have "x  V" by (simp add: finite V l_def)
    moreover have "(I, J) = (V - {x}, {x})"
    proof -
      have "(I, J) = (let l = sorted_list_of_set V in
  let x = arg_max_list (score Q_neg) l in (V - {x}, {x}))" by (simp add: False assms(2))
      then show ?thesis by (metis l_def x_def)
    qed
    then show ?thesis using Pair_inject finite V assms(1) calculation by auto
  qed
qed

global_interpretation New_max: getIJ max_getIJ
  defines New_max_getIJ_genericJoin = "New_max.genericJoin"
  and New_max_getIJ_wrapperGenericJoin = "New_max.wrapperGenericJoin"
  by standard (metis max_getIJ_coreProperties)

end