Theory QueryGraph

(* Author: Bernhard Stöckl *)

theory QueryGraph
  imports Complex_Main "Graph_Additions" "Selectivities" "JoinTree"
begin

section ‹Query Graphs›

locale query_graph = graph +
  fixes sel :: "'b weight_fun"
  fixes cf :: "'a ⇒ real"
  assumes sel_sym: "⟦tail G e⇩1 = head G e⇩2; head G e⇩1 = tail G e⇩2⟧ ⟹ sel e⇩1 = sel e⇩2"
      and not_arc_sel_1: "e ∉ arcs G ⟹ sel e = 1"
      and sel_pos: "sel e > 0"
      and sel_leq_1: "sel e ≤ 1"
      and pos_cards: "x ∈ verts G ⟹ cf x > 0"

begin

subsection ‹Function for Join Trees and Selectivities›

definition matching_sel :: "'a selectivity ⇒ bool" where
  "matching_sel f = (∀x y.
      (∃e. (tail G e) = x ∧ (head G e) = y ∧ f x y = sel e)
    ∨ ((∄e. (tail G e) = x ∧ (head G e) = y) ∧ f x y = 1))"

definition match_sel :: "'a selectivity" where
  "match_sel x y =
    (if ∃e ∈ arcs G. (tail G e) = x ∧ (head G e) = y
    then sel (THE e. e ∈ arcs G ∧ (tail G e) = x ∧ (head G e) = y) else 1)"

definition matching_rels :: "'a joinTree ⇒ bool" where
  "matching_rels t = (relations t ⊆ verts G)"

definition remove_sel :: "'a ⇒ 'b weight_fun" where
  "remove_sel x = (λb. if b∈{a ∈ arcs G. tail G a = x ∨ head G a = x} then 1 else sel b)"

definition valid_tree :: "'a joinTree ⇒ bool" where
  "valid_tree t = (relations t = verts G ∧ distinct_relations t)"

fun no_cross_products :: "'a joinTree ⇒ bool" where
  "no_cross_products (Relation rel) = True"
| "no_cross_products (Join l r) = ((∃x∈relations l. ∃y∈relations r. x →⇘G⇙ y)
    ∧ no_cross_products l ∧ no_cross_products r)"

subsection "Proofs"

text ‹
  Proofs that a query graph satisifies basic properties of join trees and selectivities.
›

lemma sel_less_arc: "sel x < 1 ⟹ x ∈ arcs G"
  using not_arc_sel_1 by force

lemma joinTree_card_pos: "matching_rels t ⟹ pos_rel_cards cf t"
  by(induction t) (auto simp: pos_cards pos_rel_cards_def matching_rels_def)

lemma symmetric_arcs: "x∈arcs G ⟹ ∃y. head G x = tail G y ∧ tail G x = head G y"
  using sym_arcs symmetric_conv by fast

lemma arc_ends_eq_impl_sel_eq: "head G x = head G y ⟹ tail G x = tail G y ⟹ sel x = sel y"
  using sel_sym symmetric_arcs not_arc_sel_1 by metis

lemma arc_ends_eq_impl_arc_eq:
  "⟦e1 ∈ arcs G; e2 ∈ arcs G; head G e1 = head G e2; tail G e1 = tail G e2⟧ ⟹ e1 = e2"
  using no_multi_alt by blast

lemma matching_sel_simp_if_not1:
  "⟦matching_sel sf; sf x y ≠ 1⟧ ⟹ ∃e ∈ arcs G. tail G e = x ∧ head G e = y ∧ sf x y = sel e"
  using not_arc_sel_1 unfolding matching_sel_def by fastforce

lemma matching_sel_simp_if_arc:
  "⟦matching_sel sf; e ∈ arcs G⟧ ⟹ sf (tail G e) (head G e) = sel e"
  unfolding matching_sel_def by (metis arc_ends_eq_impl_sel_eq)

lemma matching_sel1_if_no_arc: "matching_sel sf ⟹ ¬(x →⇘G⇙ y ∨ y →⇘G⇙ x) ⟹ sf x y = 1"
  using not_arc_sel_1 unfolding arcs_ends_def arc_to_ends_def matching_sel_def image_iff by metis

lemma matching_sel_alt_aux1:
  "matching_sel f
    ⟹ (∀x y. (∃e ∈ arcs G. (tail G e) = x ∧ (head G e) = y ∧ f x y = sel e)
            ∨ ((∄e. e ∈ arcs G ∧ (tail G e) = x ∧ (head G e) = y) ∧ f x y = 1))"
  by (metis matching_sel_def arc_ends_eq_impl_sel_eq not_arc_sel_1)

lemma matching_sel_alt_aux2:
  "(∀x y.(∃e ∈ arcs G. (tail G e) = x ∧ (head G e) = y ∧ f x y = sel e)
      ∨ ((∄e. e ∈ arcs G ∧ (tail G e) = x ∧ (head G e) = y) ∧ f x y = 1))
    ⟹ matching_sel f"
  by (fastforce simp: not_arc_sel_1 matching_sel_def)

lemma matching_sel_alt:
  "matching_sel f
    = (∀x y. (∃e ∈ arcs G. (tail G e) = x ∧ (head G e) = y ∧ f x y = sel e)
          ∨ ((∄e. e ∈ arcs G ∧ (tail G e) = x ∧ (head G e) = y) ∧ f x y = 1))"
  using matching_sel_alt_aux1 matching_sel_alt_aux2 by blast

lemma matching_sel_symm:
  assumes "matching_sel f"
  shows "sel_symm f"
  unfolding sel_symm_def
proof (standard, standard)
  fix x y
  show "f x y = f y x"
  proof(cases "∃e∈arcs G. (head G e) = x ∧ (tail G e) = y")
    case True
    then show ?thesis using assms symmetric_arcs sel_sym unfolding matching_sel_def by metis
  next
    case False
    then show ?thesis by (metis assms symmetric_arcs matching_sel_def not_arc_sel_1 sel_sym)
  qed
qed

lemma matching_sel_reasonable: "matching_sel f ⟹ sel_reasonable f"
  using sel_reasonable_def matching_sel_def sel_pos sel_leq_1
  by (metis le_numeral_extra(4) less_numeral_extra(1))

lemma matching_reasonable_cards:
  "⟦matching_sel f; matching_rels t⟧ ⟹ reasonable_cards cf f t"
  by (simp add: joinTree_card_pos matching_sel_reasonable pos_sel_reason_impl_reason)

lemma matching_sel_unique_aux:
  assumes "matching_sel f" "matching_sel g"
  shows "f x y = g x y"
proof(cases "∃e. tail G e = x ∧ head G e = y")
  case True
  then show ?thesis
    using assms arc_ends_eq_impl_sel_eq unfolding matching_sel_def by metis
next
  case False
  then show ?thesis using assms unfolding matching_sel_def by fastforce
qed

lemma matching_sel_unique: "⟦matching_sel f; matching_sel g⟧ ⟹ f = g"
  using matching_sel_unique_aux by blast

lemma match_sel_matching[intro]: "matching_sel match_sel"
  unfolding matching_sel_alt
proof(standard,standard)
  fix x y
  show "(∃e∈arcs G. tail G e = x ∧ head G e = y ∧ match_sel x y = sel e) ∨
          ((∄e. e ∈ arcs G ∧ tail G e = x ∧ head G e = y) ∧ match_sel x y = 1)"
  proof(cases "∃e ∈ arcs G. tail G e = x ∧ head G e = y")
    case True
    then obtain e where e_def: "e ∈ arcs G" "tail G e = x" "head G e = y" by blast
    then have "match_sel x y = sel (THE e. e ∈ arcs G ∧ tail G e = x ∧ head G e = y)"
      unfolding match_sel_def by auto
    moreover have "(THE e. e ∈ arcs G ∧ tail G e = x ∧ head G e = y) = e"
      using e_def arc_ends_eq_impl_arc_eq by blast
    ultimately show ?thesis using e_def by blast
  next
    case False
    then show ?thesis unfolding match_sel_def by auto
  qed
qed

corollary match_sel_unique: "matching_sel f ⟹ f = match_sel"
  using matching_sel_unique by blast

corollary match_sel1_if_no_arc: "¬(x →⇘G⇙ y ∨ y →⇘G⇙ x) ⟹ match_sel x y = 1"
  using matching_sel1_if_no_arc by blast

corollary match_sel_symm[intro]: "sel_symm match_sel"
  using matching_sel_symm by blast

corollary match_sel_reasonable[intro]: "sel_reasonable match_sel"
  using matching_sel_reasonable by blast

corollary match_reasonable_cards: "matching_rels t ⟹ reasonable_cards cf match_sel t"
  using matching_reasonable_cards by blast

lemma matching_rels_trans: "matching_rels (Join l r) = (matching_rels l ∧ matching_rels r)"
  using matching_rels_def by simp

lemma first_node_in_verts_if_rels_eq_verts: "relations t = verts G ⟹ first_node t ∈ verts G"
  unfolding first_node_eq_hd using inorder_eq_set hd_in_set[OF inorder_nempty] by fast

lemma first_node_in_verts_if_valid: "valid_tree t ⟹ first_node t ∈ verts G"
  using first_node_in_verts_if_rels_eq_verts valid_tree_def by simp

lemma dominates_sym: "(x →⇘G⇙ y) ⟷ (y →⇘G⇙ x)"
  using graph_symmetric by blast

lemma no_cross_mirror_eq: "no_cross_products (mirror t) = no_cross_products t"
  using graph_symmetric by(induction t) auto

lemma no_cross_create_ldeep_rev_app:
  "⟦ys≠[]; no_cross_products (create_ldeep_rev (xs@ys))⟧ ⟹ no_cross_products (create_ldeep_rev ys)"
proof(induction "xs@ys" arbitrary: xs rule: create_ldeep_rev.induct)
  case (2 x)
  then show ?case by (metis append_eq_Cons_conv append_is_Nil_conv)
next
  case (3 x y zs)
  then show ?case
  proof(cases xs)
    case Nil
    then show ?thesis using "3.prems"(2) by simp
  next
    case (Cons x' xs')
    have "no_cross_products (Join (create_ldeep_rev (y#zs)) (Relation x))"
      using "3.hyps"(2) "3.prems"(2) create_ldeep_rev.simps(3)[of x y zs] by simp
    then have "no_cross_products (create_ldeep_rev (y#zs))" by simp
    then show ?thesis using "3.hyps" "3.prems"(1) Cons by simp
  qed
qed(simp)

lemma no_cross_create_ldeep_app:
  "⟦xs≠[]; no_cross_products (create_ldeep (xs@ys))⟧ ⟹ no_cross_products (create_ldeep xs)"
  by (simp add: create_ldeep_def no_cross_create_ldeep_rev_app)

lemma matching_rels_if_no_cross: "⟦∀r. t ≠ Relation r; no_cross_products t⟧ ⟹ matching_rels t"
  unfolding matching_rels_def by(induction t) fastforce+

lemma no_cross_awalk:
  "⟦matching_rels t; no_cross_products t; x ∈ relations t; y ∈ relations t⟧
    ⟹ ∃p. awalk x p y ∧ set (awalk_verts x p) ⊆ relations t"
proof(induction t arbitrary: x y)
  case (Relation rel)
  then have "x ∈ verts G" using matching_rels_def by blast
  then have "awalk x [] x" by (simp add: awalk_Nil_iff)
  then show ?case using Relation(3,4) by force
next
  case (Join l r)
  then consider "x ∈ relations l" "y ∈ relations l" | "x ∈ relations r" "y ∈ relations l"
    | "x ∈ relations l" "y ∈ relations r" | "x ∈ relations r" "y ∈ relations r"
    by force
  then show ?case
  proof(cases)
    case 1
    then show ?thesis using Join.IH(1)[of x y] Join.prems(1,2) matching_rels_trans by auto
  next
    case 2
    then obtain x' y' e where e_def:
        "x' ∈ relations r" "y' ∈ relations l" "tail G e = y'" "head G e = x'" "e ∈ arcs G"
      using Join.prems(2) by auto
    then obtain e2 where e2_def: "tail G e2 = x'" "head G e2 = y'" "e2 ∈ arcs G"
      using symmetric_conv by force
    obtain p1 where p1_def: "awalk y' p1 y ∧ set (awalk_verts y' p1) ⊆ relations l"
      using Join.IH(1) Join.prems(1,2) 2(2) matching_rels_trans e_def(2) by fastforce
    obtain p2 where p2_def: "awalk x p2 x' ∧ set (awalk_verts x p2) ⊆ relations r"
      using Join.IH(2) Join.prems(1,2) 2(1) matching_rels_trans e_def(1) by fastforce
    have "awalk x (p2@[e2]@p1) y"
      using e2_def p1_def p2_def awalk_appendI arc_implies_awalk by blast
    moreover from this have "set (awalk_verts x (p2@[e2]@p1)) ⊆ relations (Join l r)"
      using p1_def p2_def awalk_verts_append3 by auto
    ultimately show ?thesis by blast
  next
    case 3
    then obtain x' y' e where e_def:
        "x' ∈ relations l" "y' ∈ relations r" "tail G e = x'" "head G e = y'" "e ∈ arcs G"
      using Join.prems(2) by auto
    obtain p1 where p1_def: "awalk y' p1 y ∧ set (awalk_verts y' p1) ⊆ relations r"
      using Join.IH(2) Join.prems(1,2) 3(2) matching_rels_trans e_def(2) by fastforce
    obtain p2 where p2_def: "awalk x p2 x' ∧ set (awalk_verts x p2) ⊆ relations l"
      using Join.IH(1) Join.prems(1,2) 3(1) matching_rels_trans e_def(1) by fastforce
    have "awalk x (p2@[e]@p1) y"
      using e_def(3-5) p1_def p2_def awalk_appendI arc_implies_awalk by blast
    moreover from this have "set (awalk_verts x (p2@[e]@p1)) ⊆ relations (Join l r)"
      using p1_def p2_def awalk_verts_append3 by auto
    ultimately show ?thesis by blast
  next
    case 4
    then show ?thesis using Join.IH(2)[of x y] Join.prems(1,2) matching_rels_trans by auto
  qed
qed

lemma no_cross_apath:
  "⟦matching_rels t; no_cross_products t; x ∈ relations t; y ∈ relations t⟧
    ⟹ ∃p. apath x p y ∧ set (awalk_verts x p) ⊆ relations t"
  using no_cross_awalk apath_awalk_to_apath awalk_to_apath_verts_subset by blast

lemma no_cross_reachable:
  "⟦matching_rels t; no_cross_products t; x ∈ relations t; y ∈ relations t⟧ ⟹ x →⇧* y"
  using no_cross_awalk reachable_awalk by blast

corollary reachable_if_no_cross:
  "⟦∃t. relations t = verts G ∧ no_cross_products t; x ∈ verts G; y ∈ verts G⟧ ⟹ x →⇧* y"
  using no_cross_reachable matching_rels_def by blast

lemma remove_sel_sym:
  "⟦tail G e⇩1 = head G e⇩2; head G e⇩1 = tail G e⇩2⟧ ⟹ (remove_sel x) e⇩1 = (remove_sel x) e⇩2"
  by(metis (no_types, lifting) mem_Collect_eq not_arc_sel_1 remove_sel_def sel_sym)+

lemma remove_sel_1: "e ∉ arcs G ⟹ (remove_sel x) e = 1"
  apply(cases "e∈{a ∈ arcs G. tail G a = x ∨ head G a = x}")
  by(auto simp: not_arc_sel_1 sel_sym remove_sel_def)

lemma del_vert_remove_sel_1:
  assumes "e ∉ arcs ((del_vert x))"
  shows "(remove_sel x) e = 1"
proof(cases "e∈{a ∈ arcs G. tail G a = x ∨ head G a = x}")
  case True
  then show ?thesis by (simp add: remove_sel_def)
next
  case False
  then have "e ∉ arcs G" using assms arcs_del_vert by simp
  then show ?thesis using remove_sel_def not_arc_sel_1 by simp
qed

lemma remove_sel_pos: "remove_sel x e > 0"
  by(cases "e∈{a ∈ arcs G. tail G a = x ∨ head G a = x}") (auto simp: remove_sel_def sel_pos)

lemma remove_sel_leq_1: "remove_sel x e ≤ 1"
  by(cases "e∈{a ∈ arcs G. tail G a = x ∨ head G a = x}") (auto simp: remove_sel_def sel_leq_1)

lemma del_vert_pos_cards: "x ∈ verts (del_vert y) ⟹ cf x > 0"
  by(cases "x=y") (auto simp: remove_sel_def del_vert_def pos_cards)

lemma del_vert_remove_sel_query_graph:
  "query_graph G sel cf ⟹ query_graph (del_vert x) (remove_sel x) cf"
  by (simp add: del_vert_pos_cards del_vert_remove_sel_1 graph_del_vert remove_sel_sym
      remove_sel_leq_1 remove_sel_pos query_graph.intro graph_axioms head_del_vert
      query_graph_axioms_def tail_del_vert)

lemma finite_nempty_set_min:
  assumes "xs ≠ {}" and "finite xs"
  shows "∃x. min_degree xs x"
proof -
  have "finite xs" using assms(2) by simp
  then show ?thesis
  using assms proof (induction "xs" rule: finite_induct)
    case empty
    then show ?case by simp
  next
    case ind: (insert x xs)
    then show ?case
    proof(cases xs)
      case emptyI
      then show ?thesis by (metis order_refl singletonD singletonI)
    next
      case (insertI xs' x')
      then have "∃a. min_degree xs a" using ind by simp
      then show ?thesis
        using ind by (metis order_trans insert_iff le_cases)
    qed
  qed
qed

lemma no_cross_reachable_graph':
  "⟦∃t. relations t = verts G ∧ no_cross_products t; x∈verts G; y∈verts G⟧
    ⟹ x →⇧*⇘mk_symmetric G⇙ y"
  by (simp add: reachable_mk_symmetricI reachable_if_no_cross)

lemma verts_nempty_if_tree: "∃t. relations t ⊆ verts G ⟹ verts G ≠ {}"
  using relations_nempty by fast

lemma connected_if_tree: "∃t. relations t = verts G ∧ no_cross_products t ⟹ connected G"
  using no_cross_reachable_graph' connected_def strongly_connected_def verts_nempty_if_tree
  by fastforce

end

locale nempty_query_graph = query_graph +
  assumes non_empty: "verts G ≠ {}"

subsection ‹Pair Query Graph›

text ‹Alternative definition based on pair graphs›

locale pair_query_graph = pair_graph +
  fixes sel :: "('a × 'a) weight_fun"
  fixes cf :: "'a ⇒ real"
  assumes sel_sym: "⟦tail G e⇩1 = head G e⇩2; head G e⇩1 = tail G e⇩2⟧ ⟹ sel e⇩1 = sel e⇩2"
      and not_arc_sel_1: "e ∉ parcs G ⟹ sel e = 1"
      and sel_pos: "sel e > 0"
      and sel_leq_1: "sel e ≤ 1"
      and pos_cards: "x ∈ pverts G ⟹ cf x > 0"

sublocale pair_query_graph ⊆ query_graph
  by(unfold_locales) (auto simp: sel_sym not_arc_sel_1 sel_pos sel_leq_1 pos_cards)

context pair_query_graph
begin

lemma "matching_sel f ⟷ (∀x y. sel (x,y) = f x y)"
  using matching_sel_def sel_sym by fastforce

end

end