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 some types, 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 as defined by Hofmann et.al (2010).
  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"

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)

lemma slookup_fminsert_other: "z ≠ x ⟹ slookup (fminsert infl1 x y) z = slookup infl1 z"
  unfolding fminsert_def fmlookup_default_def by auto

lemma slookup_fminsert_same: "slookup (fminsert infl1 x y) x = slookup infl1 x ∪ {y}"
  unfolding fminsert_def fmlookup_default_def by auto

lemma slookup_fminsert: "slookup (fminsert infl x y) z =
  (if x = z then slookup infl x ∪ {y} else slookup infl z)"
  unfolding fminsert_def fmlookup_default_def by auto


subsection ‹Functions on the Constraint System›

type_synonym ('x,'d) eqsT = "'x ⇒ ('x , 'd) strategy_tree"

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,'d::bot) eqsT ⇒ 'x ⇒ ('x, 'd) map ⇒ 'd" where
  "eq T 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::bot) 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 T σ 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 fast
  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 T σ 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

lemma dep_eq:
  assumes "∀y ∈ dep T σ x. mlup σ y = mlup σ' y"
  shows "dep T σ x = dep T σ' x"
  using dep_aux_eq assms unfolding dep_def by auto

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) fastforce+

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

lemma solution_sufficient:
  assumes "∀y ∈ dep T σ x. mlup σ y = mlup σ' y"
  shows "eq T x σ = eq T x σ'"
  using assms solution_sufficient_t
  unfolding eq_def dep_def
  by auto

corollary eq_mupd_no_dep:
  assumes "x ∉ dep T σ y"
  shows "eq T y σ = eq T y (σ (x ↦ xd))"
  using assms solution_sufficient[of T] 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 T σ x where
  base: "x ∈ reach T σ x"
| step: "y ∈ reach T σ x ⟹ z ∈ dep T σ y ⟹ z ∈ reach T σ 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 T σ c t where
  base: "x ∈ dep_aux σ t ⟹ x ∈ reach_cap_tree T σ c t"
| step: "y ∈ reach_cap_tree T σ c t ⟹ y ∉ c ⟹ z ∈ dep T σ y ⟹ z ∈ reach_cap_tree T σ c t"

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

lemma reach_cap_tree_answer_empty[simp]:
  "reach_cap_tree T σ 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 T σ' c t"
proof(intro subsetI, goal_cases)
  case (1 x)
  then show ?case using reach_cap_tree.base[where ?T=T]
    by (induction rule: dep_aux.induct; auto)
qed

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

lemma reach_empty_capped:
  shows "reach T σ x = insert x (reach_cap_tree T σ {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 T σ "{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 T σ {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 fast
    next
      case (step y z)
      then show ?case
        using reach.step[of _ T]
        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 T σ c (T y) ⊆ reach_cap_tree T σ c t"
proof
  fix xa
  assume "xa ∈ reach_cap_tree T σ c (T y)"
  then show "xa ∈ reach_cap_tree T σ c t"
  proof(induction rule: reach_cap_tree.induct)
    case (base x)
    then show ?case
      using assms reach_cap_tree.base[where ?T=T] reach_cap_tree.step[unfolded dep_def, of y T]
      by simp
  next
    case (step y z)
    then show ?case
      using reach_cap_tree.step[of _ T]
      by simp
  qed
qed

lemma reach_cap_tree_simp:
  shows "reach_cap_tree T σ c t
    = dep_aux σ t ∪ (⋃ξ∈dep_aux σ t - c. reach_cap_tree T σ (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 T σ] 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[where ?T=T] by simp
  next
    case 2
    then obtain y where "x ∈ reach_cap_tree T σ (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 _ _ T]
        reach_cap_tree_subset[of T σ "insert y c" "T y" y]
      by auto
  qed
qed

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

lemma reach_cap_tree_eq:
  assumes "∀x∈reach_cap_tree T σ c t. mlup σ x = mlup σ' x"
  shows "reach_cap_tree T σ c t = reach_cap_tree T σ' 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 T c] dep_aux_eq reach_cap_tree.base[of x σ' t T c]
      by metis
  next
    case (step y z)
    then show ?case
      using assms reach_cap_tree.step[of y T σ c t] reach_cap_tree.step[of y T σ' c t z] dep_eq
      by metis
  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 T c] dep_aux_eq reach_cap_tree.base[of x σ' t T c]
      by metis
  next
    case (step y z)
    then show ?case
      using assms reach_cap_tree.step[of y T σ c t] dep_eq reach_cap_tree.step[of y T σ' c t z]
      by metis
  qed
qed

lemma reach_cap_tree_simp2:
  shows "insert x (if x ∈ c then {} else reach_cap_tree T σ c (T x)) =
         reach_cap T σ c x"
proof(cases "x ∈ c" rule: case_split[case_names called not_called])
  case not_called
  moreover have "insert x (reach_cap_tree T σ (insert x c) (T x))
    = insert x (reach_cap_tree T σ 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 T σ x" rule: case_split[case_names xdep no_xdep])
        case xdep
        then show ?thesis using 2 reach_cap_tree.base[of y σ "T x" T "insert x c", folded dep_def]
          by auto
      next
        case no_xdep
        have "y ∈ reach_cap_tree T σ 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[where ?T=T] reach_cap_tree.base[where ?T=T]
            unfolding 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 T σ' ξ ⊆ s"
  shows "reach_cap T σ' (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 T σ' (c - {x}) (T x)"
      using 1 reach_cap_tree_simp2[of x "c - {x}" T σ'] by auto
    then show ?thesis using assms
    proof(induction)
      case (base y)
      then show ?case using base.hyps unfolding 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 T σ c (g yd) ⊆ reach_cap_tree T σ 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 T σ c t' ⊆ reach_cap_tree T σ c t"
  using assms
proof(induction rule: subt_aux.induct)
  case (step t' y g)
  then show ?case using reach_cap_tree_step[where ?T=T] by simp
qed simp

lemma reach_cap_tree_singleton:
  assumes "reach_cap_tree T σ (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 T σ (insert x c) t"
    using reach_cap_tree.base[where ?T=T] 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 T x σ vars ≡ x ∈ vars ∧ (∀u ∈ vars. eq T u σ = mlup σ u ∧ dep T σ u ⊆ vars)"

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

subsection ‹Partial post-solution›

text‹An unknown-to-value mapping @{term σ} is a partial post-solution for a set of
  unknowns @{term vars} if for any unknown @{term x} in @{term vars}, the value of @{term x} in
  @{term σ} over-approximates the value obtained from an evaluation of its right-hand side function
  with @{term σ}. Additionally, the set of unknowns should be closed under their dependencies.›

abbreviation part_post_solution ::
  "('x,'d::order_bot) eqsT ⇒ 'x ⇒ ('x, 'd) map ⇒ 'x set ⇒ bool" where
  "part_post_solution T x σ vars ≡
    x ∈ vars ∧ (∀u ∈ vars. eq T u σ ≤ mlup σ u ∧ dep T σ u ⊆ vars)"


subsection ‹Monotonic Right-hand Sides›

abbreviation option_def_bot :: "'b :: order_bot option ⇒ 'b" where
  "option_def_bot op ≡ (case op of Some d ⇒ d | None ⇒ ⊥)"

abbreviation option_leq ::
      "'b :: order_bot option ⇒ 'b :: order_bot option ⇒ bool" (infix "⊑⇩o" 900) where
  "o1 ⊑⇩o o2 ≡ option_def_bot o1 ≤ option_def_bot o2"

abbreviation map_leq ::
    "('a, 'b :: order_bot) map ⇒ ('a, 'b :: order_bot) map ⇒ bool"  (infix "⊑⇩m" 50) where
  "m⇩1 ⊑⇩m m⇩2 ≡ (∀a. mlup m⇩1 a ≤ mlup m⇩2 a)"

abbreviation map_le :: "('x, 'd::order_bot) map ⇒ ('x, 'd) map ⇒ bool" (infix "⊏⇩m" 50) where
  "map_le σ σ' ≡ (σ ⊑⇩m σ' ∧ (∃x. mlup σ x < mlup σ' x))"

abbreviation map_eq :: "('x, 'd::bot) map ⇒ ('x, 'd) map ⇒ bool" (infix "=⇩m" 50) where
  "map_eq σ σ' ≡ (∀a. mlup σ a = mlup σ' a)"

definition is_mono_eq where
  "is_mono_eq (T :: 'a ⇒ ('a, 'b :: order_bot) strategy_tree)
    ≡ (∀x σ⇩1 σ⇩2. σ⇩1 ⊑⇩m σ⇩2 ⟶ eq T x σ⇩1 ≤ eq T x σ⇩2)"

lemma mlup_is_option_def_bot: "option_def_bot (m a) = mlup m a"
  by (simp add: mlup_def)

subsection ‹Monotonicity of Dependencies of Right-hand Sides›

definition mono_deps where
  "mono_deps (T :: 'a ⇒ ('a, 'b :: order_bot) strategy_tree)
    ≡ (∀x σ⇩1 σ⇩2. σ⇩1 ⊑⇩m σ⇩2 ⟶ dep T σ⇩1 x ⊆ dep T σ⇩2 x)"

subsection ‹Subtrees for Specific Prefixes›

fun subt_for_prefix ::
  "('x,'d::bot) strategy_tree ⇒ 'x list ⇒ ('x,'d) map ⇒ ('x,'d) strategy_tree option" where
  "subt_for_prefix t [] _ = Some t"
| "subt_for_prefix (Answer _) (p#pre) _ = None"
| "subt_for_prefix (Query y g) (p#pre) σ = (
    if y = p then subt_for_prefix (g (mlup σ y)) pre σ else None)"

lemma subt_for_prefix_same:
  assumes "∀u ∈ set pre. mlup σ u = mlup σ' u"
  shows "subt_for_prefix t pre σ = subt_for_prefix t pre σ'"
  using assms by (induction t pre σ rule: subt_for_prefix.induct) auto

lemma subt_for_prefix_implies_subt: "subt_for_prefix t pre σ = Some st ⟹ st ∈ subt_aux σ t"
proof (induction t pre σ rule: subt_for_prefix.induct)
  case (1 t σ)
  then have "t = st" by auto
  then show ?case using subt_aux.base by simp
next
  case (2 d p pre σ)
  then show ?case by simp
next
  case (3 y g p pre σ)
  then have "y = p" "subt_for_prefix (g (mlup σ y)) pre σ = Some st" by (auto split: if_splits)
  then have "st ∈ subt_aux σ (g (mlup σ y))" using 3(1) by simp
  then show ?case by (simp add: subt_unfold)
qed

lemma subt_for_prefix_transitive:
  assumes "subt_for_prefix t1 pre1 σ = Some t2"
    and "subt_for_prefix t2 pre2 σ = Some t3"
  shows "subt_for_prefix t1 (pre1 @ pre2) σ = Some t3"
  using assms
proof (induction pre1 arbitrary: t1)
  case Nil
  then have "t1 = t2" by simp
  then show ?case using Nil(2) by simp
next
  case (Cons p pre1)
  obtain g where "t1 = Query p g" "subt_for_prefix (g (mlup σ p)) pre1 σ = Some t2"
    using Cons(2) by (smt (verit) list.discI list.inject option.discI subt_for_prefix.elims)
  then have "subt_for_prefix (g (mlup σ p)) (pre1 @ pre2) σ = Some t3" using Cons(1,3) by auto
  then show ?case using ‹t1 = Query p g› by auto
qed


subsection ‹Measure Relations for the Termination Proofs›

subsubsection‹Called Relation›

definition c_relation :: "('x set × 'x set) set" where
  "c_relation = measure (λc. card (UNIV - c))"

subsubsection‹Right-hand Side Relation›

text‹First, we build a wellfounded relation for direct subtrees.›

inductive direct_subt ::
    "('x, 'd) strategy_tree ⇒ ('x, 'd) strategy_tree ⇒ bool" (infix "⊏⇩t⇧1" 50) where
  "g d ⊏⇩t⇧1 Query y g"

abbreviation strict_subt ::
    "('x, 'd) strategy_tree ⇒ ('x, 'd) strategy_tree ⇒ bool" (infix "⊏⇩t⇧+" 50) where
  "strict_subt ≡ direct_subt⇧+⇧+"

abbreviation strict_subt_relation ::
    "(('x, 'd) strategy_tree × ('x, 'd) strategy_tree) set" where
  "strict_subt_relation ≡ {(t',t). t' ⊏⇩t⇧1 t}"

lemma wf_direct_subt: "wf {(t'::('x,'d) strategy_tree,t). t' ⊏⇩t⇧1 t}"
proof -
  have "{t ∈ Q. ∀st' ∈ Q. ¬ st' ⊏⇩t⇧1 t} ≠ {}" if "Q ≠ {}" for Q :: "(('x, 'd) strategy_tree) set"
  proof -
    obtain t where "t ∈ Q" using ‹Q ≠ {}› by auto
    define is_minimal where "is_minimal ≡ λstm. (∀st' ∈ Q. ¬ st' ⊏⇩t⇧1 stm)"
    then have "is_minimal t ∨ (∃stm ∈ Q. stm ⊏⇩t⇧+ t ∧ is_minimal stm)"
    proof (induction t)
      case (Answer d)
      then show ?case using direct_subt.cases by blast
    next
      case (Query y g)
      consider (smaller_exists) d where "∃stm∈Q. stm ⊏⇩t⇧+ (g d) ∧ is_minimal stm"
        | (reached_min) "⋀d. is_minimal (g d)" using Query.hyps by blast
      then show ?case
      proof cases
        case smaller_exists
        have "g d ⊏⇩t⇧+ Query y g" for d by (simp add: direct_subt.intros tranclp.r_into_trancl)
        then have "st ⊏⇩t⇧+ Query y g" if "st ⊏⇩t⇧+ g d" for st d by (meson that tranclp_trans)
        then have "∃stm∈Q. stm ⊏⇩t⇧+ Query y g ∧ is_minimal stm" using smaller_exists by blast
        then show ?thesis by simp
      next
        case reached_min
        consider (subt_in_Q) d where "g d ∈ Q"
          | (no_subt_inQ) "⋀d. g d ∉ Q" by blast
        then show ?thesis
        proof cases
          case subt_in_Q
          have "g d ⊏⇩t⇧+ Query y g" for d by (simp add: direct_subt.intros tranclp.r_into_trancl)
          then show ?thesis using reached_min subt_in_Q by blast
        next
          case no_subt_inQ
          have "is_minimal (Query y g)"
            using no_subt_inQ by (auto simp add: is_minimal_def direct_subt.simps)
          then show ?thesis by simp
        qed
      qed
    qed
    then show ?thesis using ‹t ∈ Q› is_minimal_def by blast
  qed
  then have "(∃t∈Q. ∀st' ∈ Q. (st',t) ∉ {(t',t). t' ⊏⇩t⇧1 t})"
      if "(Q :: (('x, 'd) strategy_tree) set) ≠ {}" for Q
    using that by auto
  then show ?thesis using wf_eq_minimal[of "{(t',t). t' ⊏⇩t⇧1 t}"] by (metis empty_iff)
qed

lemma wf_rhs_relation: "wf strict_subt_relation"
  using wf_direct_subt by auto

subsubsection‹Sigma Relation›

definition sigma_increasing :: "(('x, 'd::order_bot) map × ('x, 'd) map) set" where
  "sigma_increasing = {(σ', σ). σ ⊏⇩m σ'}"


text ‹For the termination proof, we assume the lattice to fulfill the ascending chain
  condition (acc) and the set of all unknowns to be finite. A partially ordered set fulfills the
  ascending chain condition states, if no infinite ascending chain $d_0 < d_1 < \dots$ exists. This
  means, that every weakly ascending chain $d_0 \leq d_1 \leq \dots$ eventually stabilizes, i.e.
  there exists an $n \in N$ such that $d_n = d_{n+1} = \dots$.
  A lattice fullfills the acc if the strict (reverse) order, i.e. >, corresponding to its partial
  order (po) {$\leq$} is is a well-founded relation (compare @{thm wf_def} and
  @{thm wf_eq_minimal}).
›

lemma wf_sigma_increasing:
  assumes acc: "wf {(y,x::'d::order_bot). less x y}"
  and finite_vars: "finite (UNIV :: 'x set)"
  shows "wf (sigma_increasing :: (('x,'d) map × ('x,'d) map) set)"
proof -
  have "{σ ∈ Q. ∀σ' ∈ Q. ¬ (∀x ∈ U. mlup σ x ≤ mlup σ' x) ∨
      ¬ (∃x ∈ U. mlup σ x < mlup σ' x)} ≠ {}" if "Q ≠ {}" "finite U"
      for Q :: "('x ⇒ 'd::order_bot option) set" and U :: "'x set"
    using that(2) that(1)
  proof (induction U arbitrary: Q rule: finite_induct)
    case empty
    then show ?case by blast
  next
    case (insert x U')
    define Vd where "Vd ≡ {d. ∃σ ∈ Q. d = mlup σ x}"
    have "Vd ≠ {}" using Vd_def insert.prems by blast
    then obtain dm where "dm ∈ Vd" and B:"∀y ∈ Vd. (y, dm) ∈ {(y, x). ¬ x < y}"
      using wfE_min'[OF acc]
      by (metis case_prodI mem_Collect_eq)
    define V where "V ≡ {σ ∈ Q. mlup σ x = dm}"
    then have "V ≠ {}" using Vd_def ‹dm ∈ Vd› by blast

    define S where "S ≡ {σ ∈ V. ∀σ' ∈ V. ¬ (∀x ∈ U'. mlup σ x ≤ mlup σ' x)
        ∨ ¬ (∃x ∈ U'. mlup σ x < mlup σ' x)}"
    then have "S ≠ {}" using ‹V ≠ {}› insert by auto

    then obtain σ where "σ ∈ S" and "σ ∈ Q" using S_def V_def by auto
    moreover have "S ⊆ Q" using S_def V_def by blast
    moreover have "¬ (∀x ∈ insert x U'. mlup σ x ≤ mlup σ' x)
        ∨ ¬ (∃x ∈ insert x U'. mlup σ x < mlup σ' x)" if "σ' ∈ V" for σ'
      using S_def V_def ‹σ ∈ S› that by auto
    moreover have "¬ (∀x ∈ insert x U'. mlup σ x ≤ mlup σ' x)
        ∨ ¬ (∃x ∈ insert x U'. mlup σ x < mlup σ' x)" if "σ' ∈ Q - V" for σ'
    proof -
      have "σ' ∉ V" using that by auto
      then have "¬ mlup σ x < mlup σ' x" using B S_def V_def Vd_def calculation(1) that by blast
      then show ?thesis using S_def V_def calculation(1) that by auto
    qed
    ultimately show ?case by blast
  qed
  note I = this
  have "(∃σ∈Q. ∀σ' ∈ Q. (σ', σ) ∉ sigma_increasing)" if "Q ≠ {}"
      for Q :: "('x ⇒ 'd option) set"
    using I[OF that finite_vars] unfolding sigma_increasing_def by auto
  then show ?thesis using wf_eq_minimal by (metis empty_iff)
qed

end