Theory Basics

section ‹Preliminaries›

text ‹\label{sec:preliminaries}›

text ‹Before we define the \td in Isabelle/HOL and start with its partial correctness proof, we define
all required data structures, formalize definitions and prove auxiliary lemmas.›

theory Basics
  imports Main "HOL-Library.Finite_Map"
begin

unbundle lattice_syntax

subsection ‹Strategy Trees›

text ‹The constraint system is a function mapping each unknown to a right-hand side to compute its
  value. We require the right-hand sides to be pure functionals
  \<^cite>‹hofmannWhatPureFunctional2010›. This means that they may query the values of other unknowns
  and perform additional computations based on those, but they may, e.g., not spy on the solver's
  data structures. Such pure functions can be expressed as strategy trees.›

datatype ('a, 'b) strategy_tree = Answer 'b |
  Query 'a "'b ⇒ ('a , 'b) strategy_tree"


text ‹The solver is defined based on a black-box function T describing the constraint system and
  under the assumption that the special element @{term ⊥} exists among the values.›

locale Solver =
  fixes D :: "'d :: bot"
    and T :: "'x ⇒ ('x , 'd) strategy_tree"
begin

subsection ‹Auxiliary Lemmas for Default Maps›

text‹The solver maintains a solver state to implement optimizations based on self-observation.
  Among the data structures for the solver state are maps that return a default value for
  non-existing keys. In the following, we define some helper functions and lemmas for these.›

definition fmlookup_default where
  "fmlookup_default m d x = (case fmlookup m x of Some v ⇒ v | None ⇒ d)"

abbreviation slookup where
  "slookup infl x ≡ set (fmlookup_default infl [] x)"

definition mlup where
  "mlup σ x ≡ case σ x of Some v ⇒ v | None ⇒ ⊥"

definition fminsert where
  "fminsert infl x y = fmupd x (y # (fmlookup_default infl [] x)) infl"

lemma set_fmlookup_default_cases:
  assumes "y ∈ slookup infl x"
  obtains (1) xs where "fmlookup infl x = Some xs" and "y ∈ set xs"
  using assms that unfolding fmlookup_default_def
  by (cases "fmlookup infl x"; auto)

lemma notin_fmlookup_default_cases:
  assumes "y ∉ slookup infl x"
  obtains (1) xs where "fmlookup infl x = Some xs" and "y ∉ set xs"
  | (2) "fmlookup infl x = None"
  using assms that unfolding fmlookup_default_def
  by (cases "fmlookup infl x"; auto)

lemma slookup_helper[simp]:
  assumes "fmlookup m x = Some ys"
    and "y ∈ set ys"
  shows "y ∈ slookup m x"
  using assms(1,2) notin_fmlookup_default_cases by force

lemma lookup_implies_mlup:
  assumes "σ x = σ' x'"
  shows "mlup σ x = mlup σ' x'"
  using assms
  unfolding mlup_def fmlookup_default_def
  by auto

lemma fmlookup_fminsert:
  assumes "fmlookup_default infl [] x = xs"
  shows "fmlookup (fminsert infl x y) x = Some (y # xs)"
proof(cases "fmlookup infl x")
  case None
  then show ?thesis using assms unfolding fmlookup_default_def fminsert_def by auto
next
  case (Some a)
  then show ?thesis using assms unfolding fmlookup_default_def fminsert_def by auto
qed

lemma fmlookup_fminsert':
  obtains xs ys
  where "fmlookup (fminsert infl x y) x = Some xs"
    and "fmlookup_default infl [] x = ys" and "xs = y # ys"
  using that fmlookup_fminsert
  by fastforce

lemma fmlookup_default_drop_set:
  "fmlookup_default (fmdrop_set A m) [] x = (if x ∉ A then fmlookup_default m [] x else [])"
  by (simp add: fmlookup_default_def)

lemma mlup_eq_mupd_set:
  assumes "x ∉ s"
    and "∀y∈s. mlup σ y = mlup σ' y"
  shows "∀y∈s. mlup σ y = mlup (σ'(x ↦ xd)) y"
  using assms
  by (simp add: mlup_def)

subsection ‹Functions on the Constraint System›

text ‹The function @{term rhs_length} computes the length of a specific path in the strategy tree
  defined by a value assignment for unknowns @{term σ}.›
function (domintros) rhs_length where
  "rhs_length (Answer d) _ = 0" |
  "rhs_length (Query x f) σ = 1 + rhs_length (f (mlup σ x)) σ"
  by pat_completeness auto

termination rhs_length
proof (rule allI, safe)
  fix t :: "('a, 'b) strategy_tree" and σ :: "('a, 'b) map"
  show "rhs_length_dom (t, σ)"
    by (induction t, auto simp add: rhs_length.domintros)
qed

text ‹The function @{term traverse_rhs} traverses a strategy tree and determines the answer when
  choosing the path through the strategy tree based on a given unknown-value mapping @{term σ}›
function (domintros) traverse_rhs where
  "traverse_rhs (Answer d) _ = d" |
  "traverse_rhs (Query x f) σ = traverse_rhs (f (mlup σ x)) σ"
  by pat_completeness auto

termination traverse_rhs
  by (relation "measure (λ(t,σ). rhs_length t σ)") auto

text ‹The function @{term eq} evaluates the right-hand side of an unknown x with an unknown-value
  mapping @{term σ}.›
definition eq :: "'x ⇒ ('x, 'd) map ⇒ 'd" where
  "eq x σ = traverse_rhs (T x) σ"
declare eq_def[simp]


subsection ‹Subtrees of Strategy Trees›

text‹We define the set of subtrees of a strategy tree for a specific path (defined through
  @{term σ}).›
inductive_set subt_aux ::
    "('x, 'd) map ⇒ ('x, 'd) strategy_tree ⇒ ('x, 'd) strategy_tree set" for σ t where
  base: "t ∈ subt_aux σ t"
| step: "t' ∈ subt_aux σ t ⟹ t' = Query y g ⟹ (g (mlup σ y)) ∈ subt_aux σ t"

definition subt where
  "subt σ x = subt_aux σ (T x)"

lemma subt_of_answer_singleton:
  shows "subt_aux σ (Answer d) = {Answer d}"
proof (intro set_eqI iffI, goal_cases)
  case (1 x)
  then show ?case by (induction rule: subt_aux.induct; simp)
next
  case (2 x)
  then show ?case by (simp add: subt_aux.base)
qed

lemma subt_transitive:
  assumes "t' ∈ subt_aux σ t"
  shows "subt_aux σ t' ⊆ subt_aux σ t"
proof
  fix τ
  assume "τ ∈ subt_aux σ t'"
  then show "τ ∈ subt_aux σ t"
    using assms
    by (induction rule: subt_aux.induct; simp add: subt_aux.step)
qed

lemma subt_unfold:
  shows "subt_aux σ (Query x f) = insert (Query x f) (subt_aux σ (f (mlup σ x)))"
proof(intro set_eqI iffI, goal_cases)
  case (1 τ)
  then show ?case
    using subt_aux.simps
    by (induction rule: subt_aux.induct; blast)
next
  case (2 τ)
  then show ?case
  proof (elim insertE, goal_cases)
    case 1
    then show ?case
      using subt_aux.base
      by simp
  next
    case 2
    then show ?case
      using subt_transitive[of "f (mlup σ x)" σ "Query x f"] subt_aux.base subt_aux.step
      by auto
  qed
qed

subsection ‹Dependencies between Unknowns›

text‹The set @{term "dep σ x"} collects all unknowns occuring in the right-hand side of @{term x}
  when traversing it with @{term σ}.›
function dep_aux where
  "dep_aux σ (Answer d) = {}"
| "dep_aux σ (Query y g) = insert y (dep_aux σ (g (mlup σ y)))"
  by pat_completeness auto

termination dep_aux
  by (relation "measure (λ(σ, t). rhs_length t σ)") auto

definition dep where
  "dep σ x = dep_aux σ (T x)"

lemma dep_aux_eq:
  assumes "∀y ∈ dep_aux σ t. mlup σ y = mlup σ' y"
  shows "dep_aux σ t = dep_aux σ' t"
  using assms
  by (induction t rule: strategy_tree.induct) auto

lemmas dep_eq = dep_aux_eq[of σ "T x" σ' for σ x σ', folded dep_def]

lemma subt_implies_dep:
  assumes "Query y g ∈ subt_aux σ t"
  shows "y ∈ dep_aux σ t"
  using assms subt_of_answer_singleton subt_unfold
  by (induction t) auto

lemma solution_sufficient:
  assumes "∀y ∈ dep σ x. mlup σ y = mlup σ' y"
  shows "eq x σ = eq x σ'"
proof -
  obtain xd where xd_def: "eq x σ = xd" by simp
  have "traverse_rhs t σ' = xd"
    if "t ∈ subt σ x"
      and "traverse_rhs t σ = xd"
    for t
    using that
  proof(induction t rule: strategy_tree.induct)
    case (Query y g)
    define t where [simp]: "t = g (mlup σ y)"
    have "traverse_rhs t σ' = xd"
      using subt_aux.step Query.prems Query.IH
      by (simp add: subt_def)
    then show ?case
      using subt_implies_dep[where ?t="T x", folded subt_def dep_def] Query.prems(1) assms(1)
      by simp
  qed simp
  then show ?thesis
    using assms subt_aux.base xd_def
    unfolding eq_def subt_def
    by simp
qed

corollary eq_mupd_no_dep:
  assumes "x ∉ dep σ y"
  shows "eq y σ = eq y (σ (x ↦ xd))"
  using assms solution_sufficient fmupd_lookup
  unfolding fmlookup_default_def mlup_def
  by simp

subsection ‹Set ‹Reach››

text‹Let @{term reach} be the set of all unknowns contributing to @{term x} (for a given @{term σ}).
  This corresponds to the set of all unknowns on which @{term x} transitively depends on when
  evaluating the necessary right-hand sides with @{term σ}.›

inductive_set reach for σ x where
  base: "x ∈ reach σ x"
| step: "y ∈ reach σ x ⟹ z ∈ dep σ y ⟹ z ∈ reach σ x"

text‹The solver stops descending when it encounters an unknown whose evaluation it has already
  started (i.e. an unknown in @{term c}). Therefore, @{term reach} might collect contributing
  unknowns which the solver did not descend into. For a predicate, that relates more closely to the
  solver's history, we define the set @{term [source = true] reach_cap}. Similarly to
  @{term reach} it collects the unknowns on which an unknown transitively depends, but only until an
  unknown in @{term c} is reached.›

inductive_set reach_cap_tree for σ c t where
  base: "x ∈ dep_aux σ t ⟹ x ∈ reach_cap_tree σ c t"
| step: "y ∈ reach_cap_tree σ c t ⟹ y ∉ c ⟹ z ∈ dep σ y ⟹ z ∈ reach_cap_tree σ c t"

abbreviation "reach_cap σ c x
  ≡ insert x (if x ∈ c then {} else reach_cap_tree σ (insert x c) (T x))"

lemma reach_cap_tree_answer_empty[simp]:
  "reach_cap_tree σ c (Answer d) = {}"
proof (intro equals0I, goal_cases)
  case (1 y)
  then show ?case by (induction rule: reach_cap_tree.induct; simp)
qed

lemma dep_subset_reach_cap_tree:
  "dep_aux σ' t ⊆ reach_cap_tree σ' c t"
proof(intro subsetI, goal_cases)
  case (1 x)
  then show ?case using reach_cap_tree.base
    by (induction rule: dep_aux.induct; auto)
qed

lemma reach_cap_tree_subset:
  shows "reach_cap_tree σ c t ⊆ reach_cap_tree σ (c - {x}) t"
proof
  fix xa
  show "xa ∈ reach_cap_tree σ c t ⟹ xa ∈ reach_cap_tree σ (c - {x}) t"
  proof(induction rule: reach_cap_tree.induct)
    case base
    then show ?case
      using reach_cap_tree.base
      by simp
  next
    case (step y' z)
    then show ?case
      using reach_cap_tree.step
      by simp
  qed
qed

lemma reach_empty_capped:
  shows "reach σ x = insert x (reach_cap_tree σ {x} (T x))"
proof(intro equalityI subsetI, goal_cases)
  case (1 y)
  then show ?case
  proof(induction rule: reach.induct)
    case (step y z)
    then show ?case using reach_cap_tree.base[of z σ "T x"] reach_cap_tree.step[of y σ "{x}"]
      unfolding dep_def by blast
  qed simp
next
  case (2 y)
  then show ?case
    using reach.base
  proof(cases "y = x")
    case False
    then have "y ∈ reach_cap_tree σ {x} (T x)"
      using 2
      by simp
    then show ?thesis
    proof(induction rule: reach_cap_tree.induct)
      case (base y)
      then show ?case
        using reach.base reach.step[of x]
        unfolding dep_def
        by auto
    next
      case (step y z)
      then show ?case
        using reach.step
        by blast
    qed
  qed simp
qed

lemma dep_aux_implies_reach_cap_tree:
  assumes "y ∉ c"
    and "y ∈ dep_aux σ t"
  shows "reach_cap_tree σ c (T y) ⊆ reach_cap_tree σ c t"
proof
  fix xa
  assume "xa ∈ reach_cap_tree σ c (T y)"
  then show "xa ∈ reach_cap_tree σ c t"
  proof(induction rule: reach_cap_tree.induct)
    case (base x)
    then show ?case
      using assms reach_cap_tree.base reach_cap_tree.step[unfolded dep_def, of y]
      by simp
  next
    case (step y z)
    then show ?case
      using reach_cap_tree.step
      by simp
  qed
qed

lemma reach_cap_tree_simp:
  shows "reach_cap_tree σ c t
    = dep_aux σ t ∪ (⋃ξ∈dep_aux σ t - c. reach_cap_tree σ (insert ξ c) (T ξ))"
proof (intro set_eqI iffI, goal_cases)
  case (1 x)
  then show ?case
  proof (induction rule: reach_cap_tree.induct)
    case (base x)
    then show ?case using reach_cap_tree.step by auto
  next
    case (step y z)
    then show ?case using reach_cap_tree.step[of y σ] reach_cap_tree.base[of z σ "T y"]
      unfolding dep_def
      by blast
  qed
next
  case (2 x)
  then show ?case
  proof (elim UnE, goal_cases)
    case 1
    then show ?case using reach_cap_tree.base by simp
  next
    case 2
    then obtain y where "x ∈ reach_cap_tree σ (insert y c) (T y)" and "y ∈ dep_aux σ t - c" by auto
    then show ?case
    using dep_aux_implies_reach_cap_tree[of y c] reach_cap_tree_subset[of σ "insert y c" "T y" y]
    by auto
  qed
qed

lemma reach_cap_tree_step:
  assumes "mlup σ y = yd"
  shows "reach_cap_tree σ c (Query y g) = insert y (if y ∈ c then {}
    else reach_cap_tree σ (insert y c) (T y)) ∪ reach_cap_tree σ c (g yd)"
  using assms reach_cap_tree_simp[of σ c]
  by auto

lemma reach_cap_tree_eq:
  assumes "∀x∈reach_cap_tree σ c t. mlup σ x = mlup σ' x"
  shows "reach_cap_tree σ c t = reach_cap_tree σ' c t"
proof(intro equalityI subsetI, goal_cases)
  case (1 x)
  then show ?case
  proof(induction rule: reach_cap_tree.induct)
    case (base x)
    then show ?case
      using assms reach_cap_tree.base[of _ σ t c] dep_aux_eq reach_cap_tree.base[of x σ' t c]
      by metis
  next
    case (step y z)
    then show ?case
      using assms reach_cap_tree.step[of y σ c t] dep_eq reach_cap_tree.step[of y σ' c t z]
      by blast
  qed
next
  case (2 x)
  then show ?case
  proof(induction rule: reach_cap_tree.induct)
    case (base x)
    then show ?case
      using assms reach_cap_tree.base[of _ σ t c] dep_aux_eq reach_cap_tree.base[of x σ' t c]
      by metis
  next
    case (step y z)
    then show ?case
      using assms reach_cap_tree.step[of y σ c t] dep_eq reach_cap_tree.step[of y σ' c t z]
      by blast
  qed
qed

lemma reach_cap_tree_simp2:
  shows "insert x (if x ∈ c then {} else reach_cap_tree σ c (T x)) =
         insert x (if x ∈ c then {} else reach_cap_tree σ (insert x c) (T x))"
proof(cases "x ∈ c" rule: case_split[case_names called not_called])
  case not_called
  moreover have "insert x (reach_cap_tree σ (insert x c) (T x))
    = insert x (reach_cap_tree σ c (T x))"
  proof(intro equalityI subsetI, goal_cases)
    case (1 y)
    then show ?case
    proof(cases "x = y")
      case False
      then show ?thesis
        by (metis "1" Diff_insert_absorb in_mono insert_mono not_called reach_cap_tree_subset)
    qed auto
  next
    case (2 y)
    then show ?case
    proof(cases "x = y")
      case False
      then show ?thesis
      proof(cases "y ∈ dep σ x" rule: case_split[case_names xdep no_xdep])
        case xdep
        then show ?thesis using 2 reach_cap_tree.base[of y σ "T x" "insert x c", folded dep_def]
          by auto
      next
        case no_xdep
        have "y ∈ reach_cap_tree σ c (T x)" using 2 False by auto
        then show ?thesis
        proof (induction rule: reach_cap_tree.induct)
          case (base x)
          then show ?case by (simp add: reach_cap_tree.base)
        next
          case (step y z)
          then show ?case using reach_cap_tree.step reach_cap_tree.base dep_def by blast
        qed
      qed
    qed auto
  qed
  then show ?thesis by auto
qed auto

lemma dep_closed_implies_reach_cap_tree_closed:
  assumes "x ∈ s"
    and "∀ξ∈s - (c - {x}). dep σ' ξ ⊆ s"
  shows "reach_cap σ' (c - {x}) x ⊆ s"
proof (intro subsetI, goal_cases)
  case (1 y)
  then show ?case using assms
  proof(cases "x = y")
    case False
    then have "y ∈ reach_cap_tree σ' (c - {x}) (T x)"
      using 1 reach_cap_tree_simp2[of x "c - {x}" σ'] by auto
    then show ?thesis using assms
    proof(induction)
      case (base y)
      then show ?case using base.hyps dep_def by auto
    next
      case (step y z)
      then show ?case by (metis (no_types, lifting) Diff_iff insert_subset mk_disjoint_insert)
    qed
  qed simp
qed

lemma reach_cap_tree_subset2:
  assumes "mlup σ y = yd"
  shows "reach_cap_tree σ c (g yd) ⊆ reach_cap_tree σ c (Query y g)"
  using reach_cap_tree_step[OF assms] by blast

lemma reach_cap_tree_subset_subt:
  assumes "t' ∈ subt_aux σ t"
  shows "reach_cap_tree σ c t' ⊆ reach_cap_tree σ c t"
  using assms
proof(induction rule: subt_aux.induct)
  case (step t' y g)
  then show ?case using reach_cap_tree_step by simp
qed simp

lemma reach_cap_tree_singleton:
  assumes "reach_cap_tree σ (insert x c) t ⊆ {x}"
  obtains (Answer) d where "t = Answer d"
  | (Query) f where "t = Query x f"
    and "dep_aux σ t = {x}"
  using assms that(1)
proof(cases t)
  case (Query x' f)
  then have "x' ∈ reach_cap_tree σ (insert x c) t"
    using reach_cap_tree.base dep_aux.simps(2) by simp
  then have [simp]: "x' = x" using assms by auto
  then show ?thesis
    using assms that(2) reach_cap_tree.base Query dep_subset_reach_cap_tree subset_antisym
    by fastforce
qed simp

subsection ‹Partial solution›

text‹Finally, we define an unknown-to-value mapping @{term σ} to be a partial solution over a set of
  unknowns @{term vars} if for every unknown in @{term vars}, the value obtained from an evaluation
  of its right-hand side function @{term "eq x"} with @{term σ} matches the value stored in
  @{term σ}.›
abbreviation part_solution where
  "part_solution σ vars ≡ (∀x ∈ vars. eq x σ = mlup σ x)"

lemma part_solution_coinciding_sigma_called:
  assumes "part_solution σ (s - c)"
    and "∀x ∈ s. mlup σ x = mlup σ' x"
    and "∀x ∈ s - c. dep σ x ⊆ s"
  shows "part_solution σ' (s - c)"
  using assms
proof(intro ballI, goal_cases)
  case (1 x)
  then have "∀y∈dep σ x. mlup σ y = mlup σ' y" by blast
  then show ?case using 1 solution_sufficient[of σ x σ'] by simp
qed

end

end