Theory Datalog

theory Datalog imports Main begin


section ‹Datalog programs and their solutions›

datatype (vars_id: 'x,'c) id = 
  is_Var: Var 'x 
  | is_Cst: Cst (the_Cst: 'c)

datatype (preds_rh: 'p,'x,'c) rh = 
  Eql "('x,'c) id" "('x,'c) id" ("_ = _" [61, 61] 61)
  | Neql "('x,'c) id" "('x,'c) id" ("_ ≠ _" [61, 61] 61)
  | PosLit 'p "('x,'c) id list" ("+ _ _" [61, 61] 61)
  | NegLit 'p "('x,'c) id list" ("¬ _ _" [61, 61] 61)

type_synonym ('p,'x,'c) lh = "'p × ('x,'c) id list"

fun preds_lh :: "('p,'x,'c) lh ⇒ 'p set" where 
  "preds_lh (p,ids) = {p}"

datatype (preds_cls: 'p, 'x,'c) clause = Cls 'p "('x,'c) id list" (the_rhs: "('p,'x,'c) rh list")

fun the_lh where
  "the_lh (Cls p ids rhs) = (p,ids)"

type_synonym ('p,'x,'c) dl_program = "('p,'x,'c) clause set"

definition "preds_dl dl = ⋃{preds_cls c| c. c ∈ dl}"

lemma preds_dl_union[simp]: "preds_dl (dl1 ∪ dl2) = preds_dl dl1 ∪ preds_dl dl2"
  unfolding preds_dl_def by auto

type_synonym ('x,'c) var_val = "'x ⇒ 'c"

type_synonym ('p,'c) pred_val = "'p ⇒ 'c list set"


fun eval_id :: "('x,'c) id ⇒ ('x,'c) var_val ⇒ 'c" ("⟦_⟧id") where
  "⟦Var x⟧id σ = σ x"
| "⟦Cst c⟧id σ = c"

fun eval_ids :: "('x,'c) id list ⇒ ('x,'c) var_val ⇒ 'c list" ("⟦_⟧ids") where
  "⟦ids⟧ids σ = map (λa. ⟦a⟧id σ) ids"

fun meaning_rh :: "('p,'x,'c) rh ⇒ ('p,'c) pred_val ⇒ ('x,'c) var_val ⇒ bool" ("⟦_⟧rh") where
  "⟦a = a'⟧rh ρ σ ⟷ ⟦a⟧id σ = ⟦a'⟧id σ"
| "⟦a ≠ a'⟧rh ρ σ ⟷ ⟦a⟧id σ  ≠ ⟦a'⟧id σ"
| "⟦+ p ids⟧rh ρ σ ⟷ ⟦ids⟧ids σ ∈ ρ p"
| "⟦¬ p ids⟧rh ρ σ ⟷ ¬ ⟦ids⟧ids σ ∈ ρ p"

fun meaning_rhs :: "('p,'x,'c) rh list ⇒ ('p,'c) pred_val ⇒ ('x,'c) var_val ⇒ bool" ("⟦_⟧rhs") where
  "⟦rhs⟧rhs ρ σ ⟷ (∀rh ∈ set rhs. ⟦rh⟧rh ρ σ)"

fun meaning_lh :: "('p,'x,'c) lh ⇒ ('p,'c) pred_val ⇒ ('x,'c) var_val ⇒ bool" ("⟦_⟧lh") where
  "⟦(p,ids)⟧lh ρ σ ⟷ ⟦ids⟧ids σ ∈ ρ p"

fun meaning_cls :: "('p,'x,'c) clause ⇒ ('p,'c) pred_val ⇒ ('x,'c) var_val ⇒ bool" ("⟦_⟧cls") where
  "⟦Cls p ids rhs⟧cls ρ σ ⟷ (⟦rhs⟧rhs ρ σ ⟶ ⟦(p,ids)⟧lh ρ σ)" 

fun solves_lh :: "('p,'c) pred_val ⇒ ('p,'x,'c) lh ⇒ bool" (infix "⊨lh" 91) where
  "ρ ⊨lh (p,ids) ⟷ (∀σ. ⟦(p,ids)⟧lh ρ σ)"

fun solves_rh :: "('p,'c) pred_val ⇒ ('p,'x,'c) rh ⇒ bool" (infix "⊨rh" 91) where 
  "ρ ⊨rh rh ⟷ (∀σ. ⟦rh⟧rh ρ σ)"

definition solves_cls :: "('p,'c) pred_val ⇒ ('p,'x,'c) clause ⇒ bool" (infix "⊨cls" 91) where
  "ρ ⊨cls c ⟷ (∀σ. ⟦c⟧cls ρ σ)"

definition solves_program :: "('p,'c) pred_val ⇒ ('p,'x,'c) dl_program ⇒ bool" (infix "⊨dl" 91) where
  "ρ ⊨dl dl ⟷ (∀c ∈ dl. ρ ⊨cls c)"


section ‹Substitutions›

type_synonym ('x,'c) subst = "'x ⇒ ('x,'c) id"

fun subst_id :: "('x,'c) id ⇒ ('x,'c) subst ⇒ ('x,'c) id" (infix "⋅id" 70) where
  "(Var x) ⋅id η  = η x"
| "(Cst e) ⋅id η = (Cst e)"

fun subst_ids :: "('x,'c) id list ⇒ ('x,'c) subst ⇒ ('x,'c) id list" (infix "⋅ids" 50) where
  "ids ⋅ids η = map (λa. a ⋅id η) ids"

fun subst_rh :: "('p,'x,'c) rh ⇒ ('x,'c) subst ⇒ ('p,'x,'c) rh" (infix "⋅rh" 50) where
  "(a = a') ⋅rh η = (a ⋅id η = a' ⋅id η)"
| "(a ≠ a') ⋅rh η = (a ⋅id η ≠ a' ⋅id η)"
| "(+ p ids) ⋅rh η = (+ p (ids ⋅ids η))"
| "(¬ p ids) ⋅rh η = (¬ p ( ids ⋅ids η))"

fun subst_rhs :: "('p,'x,'c) rh list ⇒ ('x,'c) subst ⇒ ('p,'x,'c) rh list" (infix "⋅rhs" 50) where
  "rhs ⋅rhs η = map (λa. a ⋅rh η) rhs"

fun subst_lh :: "('p,'x,'c) lh ⇒ ('x,'c) subst ⇒ ('p,'x,'c) lh" (infix "⋅lh" 50) where
  "(p,ids) ⋅lh η = (p, ids ⋅ids η)"

fun subst_cls :: "('p,'x,'c) clause ⇒ ('x,'c) subst ⇒ ('p,'x,'c) clause" (infix "⋅cls" 50) where
  "(Cls p ids rhs) ⋅cls η  = Cls p (ids ⋅ids η) (rhs ⋅rhs η)"

definition compose :: "('x,'c) subst ⇒ ('x,'c) var_val ⇒ ('x,'c) var_val" (infix "∘sv" 50) where
  "(η ∘sv σ) x = ⟦(η x)⟧id σ"


section ‹Substituting variable valuations›

fun substv_id :: "('x,'c) id ⇒ ('x,'c) var_val ⇒ ('x,'c) id" (infix "⋅vid" 70) where
  "(Var x) ⋅vid σ = Cst (σ x)"
| "(Cst e) ⋅vid σ = (Cst e)"

fun substv_ids :: "('x,'c) id list ⇒ ('x,'c) var_val ⇒ ('x,'c) id list" (infix "⋅vids" 50) where
  "ids ⋅vids σ = map (λa. a ⋅vid σ) ids"

fun substv_rh :: "('p,'x,'c) rh ⇒ ('x,'c) var_val ⇒ ('p,'x,'c) rh" (infix "⋅vrh" 50) where
  "(a = a') ⋅vrh σ = (a ⋅vid σ = a' ⋅vid σ)"
| "(a ≠ a') ⋅vrh σ = (a ⋅vid σ ≠ a' ⋅vid σ)"
| "(+ p ids) ⋅vrh σ = (+ p (ids ⋅vids σ))"
| "(¬ p ids) ⋅vrh σ = (¬ p (ids ⋅vids σ))"

definition substv_rhs :: "('p,'x,'c) rh list ⇒ ('x,'c) var_val ⇒ ('p,'x,'c) rh list" (infix "⋅vrhs" 50) where
  "rhs ⋅vrhs σ = map (λa. a ⋅vrh σ) rhs"

fun substv_lh :: "('p,'x,'c) lh ⇒ ('x,'c) var_val ⇒ ('p,'x,'c) lh" (infix "⋅vlh" 50) where
  "(p,ids) ⋅vlh σ = (p, ids ⋅vids σ)"

fun substv_cls :: "('p,'x,'c) clause ⇒ ('x,'c) var_val ⇒ ('p,'x,'c) clause" (infix "⋅vcls" 50) where
  "(Cls p ids rhs) ⋅vcls σ  = Cls p (ids ⋅vids σ) (rhs ⋅vrhs σ)"


section ‹Datalog lemmas›

subsection ‹Variable valuations›

lemma substv_id_is_Cst_eval_id:
  "a' ⋅vid σ' = Cst (⟦a'⟧id σ')"
  by (cases a') auto

lemma eval_id_is_substv_id:
  "⟦a'⟧id σ' = ⟦a⟧id σ ⟷ (a' ⋅vid σ') = (a ⋅vid σ)"
  by (cases a'; cases a) auto

lemma eval_ids_is_substv_ids:
  "⟦ids'⟧ids σ' = ⟦ids⟧ids σ ⟷ (ids' ⋅vids σ') = (ids ⋅vids σ)"
proof (induction ids' arbitrary: ids)
  case Nil
  then show ?case 
    by auto
next
  case (Cons a ids')
  note Cons_outer = Cons
  show ?case
  proof (cases ids)
    case Nil
    then show ?thesis
      using Cons_outer by auto
  next
    case (Cons a list)
    then show ?thesis
      using eval_id_is_substv_id Cons_outer by force
  qed
qed

lemma solves_rh_substv_rh_if_meaning_rh:
  assumes "⟦a⟧rh ρ σ"
  shows "ρ ⊨rh (a ⋅vrh σ)"
using assms proof (induction a)
  case (Eql a a')
  then show ?case 
    by (auto simp add: eval_id_is_substv_id)
next
  case (Neql a a')
  then show ?case
    using eval_id_is_substv_id by (auto simp add: substv_id_is_Cst_eval_id) 
next
  case (PosLit p ids)
  then show ?case 
    by (auto simp add: substv_id_is_Cst_eval_id comp_def eval_id_is_substv_id) 
next
  case (NegLit p ids)
  then show ?case 
    by (auto simp add: substv_id_is_Cst_eval_id comp_def eval_id_is_substv_id) 
qed

lemma solves_lh_substv_lh_if_meaning_lh:
  assumes "⟦a⟧lh ρ σ"
  shows "ρ ⊨lh (a ⋅vlh σ)"
proof -
  obtain p ids where a_split: "a = (p, ids)"
    by (cases a)
  show ?thesis
    using assms unfolding a_split
    by (auto simp add: substv_id_is_Cst_eval_id comp_def eval_id_is_substv_id) 
qed


subsection ‹Solve lhs›

lemma solves_lh_iff_solves_lh: "ρ ⊨cls Cls p ids [] ⟷ ρ ⊨rh (+ p ids)"
  using solves_cls_def by force

lemma solves_lh_lh:
  assumes "ρ ⊨cls Cls p args []"
  shows "ρ ⊨lh (p, args)"
  using assms unfolding solves_cls_def by auto

lemmas solve_lhs = solves_lh_iff_solves_lh solves_lh_lh


subsection ‹Propositional inferences›


subsubsection ‹Of last right hand›

lemma prop_inf_last_from_cls_rh_to_cls:
  assumes "ρ ⊨cls Cls p ids (rhs @ [rh])"
  assumes "ρ ⊨rh rh"
  shows "ρ ⊨cls Cls p ids rhs"
  using assms unfolding solves_cls_def by auto

lemma prop_inf_last_from_cls_lh_to_cls:
  assumes "ρ ⊨cls Cls p ids (rhs @ [+ p ids])"
  assumes "ρ ⊨lh (p, ids)"
  shows "ρ ⊨cls Cls p ids rhs"
  using assms by (force simp add: solves_cls_def)

lemmas prop_inf_last = prop_inf_last_from_cls_rh_to_cls prop_inf_last_from_cls_lh_to_cls


subsubsection ‹Of only right hand›

lemma modus_ponens_rh:
  assumes "ρ ⊨cls Cls p ids [+ p' ids']"
  assumes "ρ ⊨lh (p', ids')"
  shows "ρ ⊨lh (p, ids)"
  using assms
proof -
  from assms(2) have "∀σ. ⟦+ p' ids'⟧rh ρ σ"
    by fastforce
  then have "ρ ⊨cls Cls p ids []"
    using assms(1) self_append_conv2 solves_rh.elims(3) prop_inf_last_from_cls_rh_to_cls by metis 
  then show "ρ ⊨lh (p, ids)"
    by (meson solves_lh_lh)
qed

lemma prop_inf_only_from_cls_cls_to_cls:
  assumes "ρ ⊨cls Cls p ids [+ p' ids']"
  assumes "ρ ⊨cls Cls p' ids' []"
  shows "ρ ⊨cls Cls p ids []"
  by (metis append_self_conv2 assms prop_inf_last_from_cls_rh_to_cls solves_lh_iff_solves_lh)

lemmas prop_inf_only = modus_ponens_rh prop_inf_only_from_cls_cls_to_cls


subsubsection ‹Of all right hands›

lemma modus_ponens:
  assumes "ρ ⊨cls Cls p ids rhs"
  assumes "∀rh∈set rhs. ρ ⊨rh rh"
  shows "ρ ⊨lh (p, ids)"
  using assms unfolding solves_cls_def meaning_lh.simps by force

lemmas prop_inf_all = modus_ponens

lemmas prop_inf = prop_inf_last prop_inf_only prop_inf_all

subsection ‹Substitution›

lemma substitution_lemma_id: "⟦a⟧id (η ∘sv σ) = ⟦a ⋅id η⟧id σ"
  by (cases a) (auto simp add: compose_def)

lemma substitution_lemma_ids: "⟦ids⟧ids (η ∘sv σ) = ⟦ids ⋅ids η⟧ids σ"
  using substitution_lemma_id by auto

lemma substitution_lemma_lh: "⟦(p, ids)⟧lh ρ (η ∘sv σ) ⟷ ⟦(p, ids ⋅ids η )⟧lh ρ σ"
  by (metis meaning_lh.simps substitution_lemma_ids)

lemma substitution_lemma_rh:"⟦rh⟧rh ρ (η ∘sv σ) ⟷ ⟦rh ⋅rh η⟧rh ρ σ"
proof (induction rh)
  case (Eql a a')
  then show ?case
    by (simp add: substitution_lemma_id)
next
  case (Neql a a')
  then show ?case
    by (simp add: substitution_lemma_id)
next
  case (PosLit p ids)
  then show ?case
    using substitution_lemma_lh by fastforce
next
  case (NegLit p ids)
  then show ?case
    using substitution_lemma_lh by fastforce
qed

lemma substitution_lemma_rhs: "⟦rhs⟧rhs ρ (η ∘sv σ) ⟷ ⟦rhs ⋅rhs η⟧rhs ρ σ"
  by (simp add: substitution_lemma_rh) 

lemma substitution_lemma_cls:
  "⟦c⟧cls ρ (η ∘sv σ) = ⟦c ⋅cls η⟧cls ρ σ"
proof (induction c)
  case (Cls p ids rhs)
  have "⟦rhs⟧rhs ρ (η ∘sv σ) = ⟦rhs ⋅rhs η⟧rhs ρ σ"
    using substitution_lemma_rhs by blast
  moreover
  have  "⟦(p, ids)⟧lh ρ (η ∘sv σ) = ⟦(p, ids ⋅ids η)⟧lh ρ σ"
    using substitution_lemma_lh by metis
  ultimately
  show ?case
    unfolding meaning_cls.simps by auto
qed

lemma substitution_lemma:
  assumes "ρ ⊨cls c"
  shows "ρ ⊨cls (c ⋅cls (η::('x,'c) subst))"
proof -
  show ?thesis
    unfolding solves_cls_def
  proof
    fix σ :: "'x ⇒ 'c"
    from assms have "⟦c⟧cls ρ (η ∘sv σ)"
      using solves_cls_def by auto
    then show "⟦c ⋅cls η ⟧cls ρ σ"
      using substitution_lemma_cls by blast
  qed
qed


section ‹Stratification and solutions to stratified datalog programs›

type_synonym 'p strat = "'p ⇒ nat"

fun rnk :: "'p strat ⇒ ('p,'x,'c) rh ⇒ nat" where
  "rnk s (a = a') = 0"
| "rnk s (a ≠ a') = 0"
| "rnk s (+ p ids) = s p"
| "rnk s (¬ p ids) = 1 + s p"

fun strat_wf_cls :: "'p strat ⇒ ('p,'x,'c) clause ⇒ bool" where
  "strat_wf_cls s (Cls p ids rhs) ⟷ (∀rh ∈ set rhs. s p ≥ rnk s rh)"

definition strat_wf :: "'p strat ⇒ ('p,'x,'c) dl_program ⇒ bool" where
  "strat_wf s dl ⟷ (∀c ∈ dl. strat_wf_cls s c)"

definition max_stratum :: "'p strat ⇒ ('p,'x,'c) dl_program ⇒ nat" where
  "max_stratum s dl = Max {s p | p ids rhs. Cls p ids rhs ∈ dl}"

fun pred_val_lte_stratum :: "('p,'c) pred_val ⇒ 'p strat ⇒ nat ⇒ ('p,'c) pred_val" 
  ("_ ≤≤≤_≤≤≤ _" 0) where 
  "(ρ ≤≤≤s≤≤≤ n) p = (if s p ≤ n then ρ p else {})"

fun dl_program_lte_stratum :: "('p,'x,'c) dl_program ⇒ 'p strat ⇒ nat ⇒ ('p,'x,'c) dl_program" 
  ("_ ≤≤_≤≤ _" 0) where 
  "(dl ≤≤s≤≤ n) = {(Cls p ids rhs)| p ids rhs . (Cls p ids rhs) ∈ dl ∧ s p ≤ n}"

fun dl_program_on_stratum :: "('p,'x,'c) dl_program ⇒ 'p strat ⇒ nat ⇒ ('p,'x,'c) dl_program" 
  ("_ ==_== _" 0) where 
  "(dl ==s== n) = {(Cls p ids rhs)| p ids rhs . (Cls p ids rhs) ∈ dl ∧ s p = n}"

― ‹The ordering on predicate valuations from
     Flemming Nielson and Hanne Riis Nielson. 
     Program analysis (an appetizer). 
     CoRR,abs/2012.10086, 2020.›
definition lt :: "('p,'c) pred_val ⇒ 'p strat ⇒ ('p,'c) pred_val ⇒ bool" ("_ ⊏_⊏ _") where
  "(ρ ⊏s⊏ ρ') ⟷ (∃p. ρ p ⊂ ρ' p ∧
                       (∀p'. s p' = s p ⟶ ρ p' ⊆ ρ' p') ∧
                       (∀p'. s p' < s p ⟶ ρ p' = ρ' p'))"

― ‹The ordering on predicate valuations from
     Teodor C. Przymusinski.
     On the declarative semantics of deductive databases and logic programs.
     In Jack Minker, editor, Foundations of Deductive Databases and Logic Programming,
       pages 193–216. Morgan Kaufmann, 1988.›
definition lt_prz :: "('p,'c) pred_val ⇒ 'p strat ⇒ ('p,'c) pred_val ⇒ bool" ("_ ⊏_⊏prz _") where
  "(ρM ⊏s⊏prz ρN) ⟷ ρN ≠ ρM ∧ 
                     (∀pA cA. cA ∈ ρN pA - ρM pA ⟶ (∃pB cB. cB ∈ ρM pB - ρN pB ∧ s pA > s pB))"

definition lte :: "('p,'c) pred_val ⇒ 'p strat ⇒ ('p,'c) pred_val ⇒ bool" ("_ ⊑_⊑ _") where
  "(ρ ⊑s⊑ ρ') ⟷ ρ = ρ' ∨ (ρ ⊏s⊏ ρ')"

definition least_solution :: "('p,'c) pred_val ⇒ ('p,'x,'c) dl_program ⇒ 'p strat ⇒ bool" 
  ("_ ⊨lst") where
  "ρ ⊨lst dl s ⟷ ρ ⊨dl dl ∧ (∀ρ'. ρ' ⊨dl dl ⟶ ρ ⊑s⊑ ρ')"

definition minimal_solution :: "('p,'c) pred_val ⇒ ('p,'x,'c) dl_program ⇒ 'p strat ⇒ bool"
  ("_ ⊨min") where
  "ρ ⊨min dl s ⟷ ρ ⊨dl dl ∧ (∄ρ'. ρ' ⊨dl dl ∧ ρ' ⊏s⊏ ρ)"

lemma lte_def2:
  "(ρ ⊑s⊑ ρ') ⟷ ρ ≠ ρ' ⟶ (ρ ⊏s⊏ ρ')"
  unfolding lte_def by auto


subsection ‹Solving lower strata›

lemma strat_wf_lte_if_strat_wf_lte:
  assumes "n > m"
  assumes "strat_wf s (dl ≤≤s≤≤ n)"
  shows "strat_wf s (dl ≤≤s≤≤ m)"
  using assms unfolding strat_wf_def by fastforce

lemma strat_wf_lte_if_strat_wf:
  assumes "strat_wf s dl"
  shows "strat_wf s (dl ≤≤s≤≤ n)"
  using assms unfolding strat_wf_def by auto

lemma meaning_lte_m_iff_meaning_rh:
  assumes "rnk s rh ≤ n"
  shows "⟦rh⟧rh (ρ ≤≤≤s≤≤≤ n) σ ⟷ ⟦rh⟧rh ρ σ"
  using assms equals0D meaning_rh.elims(3) pred_val_lte_stratum.simps by fastforce

lemma meaning_lte_m_iff_meaning_lh:
  assumes "s p ≤ m"
  shows "⟦(p, ids)⟧lh (ρ ≤≤≤s≤≤≤ m) σ ⟷ ⟦(p, ids)⟧lh ρ σ"
  using assms by auto

lemma meaning_lte_m_iff_meaning_cls:
  assumes "strat_wf_cls s (Cls p ids rhs)"
  assumes "s p ≤ m"
  shows "⟦Cls p ids rhs⟧cls (ρ ≤≤≤s≤≤≤ m) σ ⟷ ⟦Cls p ids rhs⟧cls ρ σ"
proof -
  have p_leq_m: "s p ≤ m"
    using assms by fastforce
  have rh_leq_m: "∀rh ∈ set rhs. rnk s rh ≤ m"
    using assms assms(2) dual_order.trans by (metis (no_types, lifting) p_leq_m strat_wf_cls.simps)

  show "⟦Cls p ids rhs⟧cls (ρ ≤≤≤s≤≤≤ m) σ ⟷ ⟦Cls p ids rhs⟧cls ρ σ"
    using meaning_lte_m_iff_meaning_rh[of s _ m ρ σ] p_leq_m rh_leq_m assms(2) by force
qed

lemma solves_lte_m_iff_solves_cls:
  assumes "strat_wf_cls s (Cls p ids rhs)"
  assumes "s p ≤ m"
  shows "(ρ ≤≤≤s≤≤≤ m) ⊨cls Cls p ids rhs ⟷ ρ ⊨cls Cls p ids rhs"
  by (meson assms meaning_lte_m_iff_meaning_cls solves_cls_def)
                                          
lemma downward_lte_solves:
  assumes "n > m"
  assumes "ρ ⊨dl (dl ≤≤s≤≤ n)"
  assumes "strat_wf s dl"
  shows "(ρ ≤≤≤s≤≤≤ m) ⊨dl (dl ≤≤s≤≤ m)"
  unfolding solves_program_def
proof
  fix c
  assume a: "c ∈ (dl ≤≤s≤≤ m)"
  obtain p ids rhs where c_split: "c = Cls p ids rhs"
    by (cases c) auto

  have "m < n"
    using assms(1) by blast
  moreover
  have "strat_wf_cls s (Cls p ids rhs)"
    using a assms(3) c_split strat_wf_lte_if_strat_wf strat_wf_def by blast
  moreover
  have "s p ≤ m"
    using a c_split by force
  moreover
  have "ρ ⊨cls Cls p ids rhs"
    using c_split assms a unfolding solves_program_def by force  
  ultimately
  show "(ρ ≤≤≤s≤≤≤ m) ⊨cls c"
    using c_split by (simp add: solves_lte_m_iff_solves_cls)
qed

lemma downward_solves:
  assumes "ρ ⊨dl dl"
  assumes "strat_wf s dl"
  shows "(ρ ≤≤≤s≤≤≤ m) ⊨dl (dl ≤≤s≤≤ m)"
  unfolding solves_program_def
proof
  fix c
  assume a: "c ∈ (dl ≤≤s≤≤ m)"
  then obtain p ids rhs where c_def: "c = Cls p ids rhs"
    by (cases c) auto

  have "ρ ⊨cls c"
    using ‹c ∈ (dl ≤≤s≤≤ m)› assms(1) solves_program_def by auto

  have "(ρ ≤≤≤s≤≤≤ m) ⊨cls Cls p ids rhs"
    using ‹ρ ⊨cls c› a assms(2) c_def solves_lte_m_iff_solves_cls strat_wf_def by fastforce
  then show "(ρ ≤≤≤s≤≤≤ m) ⊨cls c"
    using c_def by auto
qed


subsection ‹Least solutions›


subsubsection ‹Existence of least solutions›

definition Inter' :: "('a ⇒ 'b set) set ⇒ 'a ⇒ 'b set" ("⋂") where 
  "(⋂ ρs) = (λp. ⋂{ρ p | ρ. ρ ∈ ρs})"

lemma Inter'_def2: "(⋂ ρs) = (λp. ⋂{m. ∃ρ ∈ ρs. m = ρ p})"
  unfolding Inter'_def by auto

lemma member_Inter':
  assumes "∀p ∈ ps. y ∈ p x"
  shows "y ∈ (⋂ ps) x"
  using assms unfolding Inter'_def by auto

lemma member_if_member_Inter':
  assumes "y ∈ (⋂ ps) x"
  assumes "p ∈ ps"
  shows "y ∈ p x"
  using assms unfolding Inter'_def by auto

lemma member_Inter'_iff:
  "(∀p ∈ ps. y ∈ p x) ⟷ y ∈ (⋂ ps) x"
  unfolding Inter'_def by auto

lemma intersection_valuation_subset_valuation:
  assumes "P ρ"
  shows "⋂ {ρ'. P  ρ'} p ⊆ ρ p"
  using assms unfolding Inter'_def by auto

fun solve_pg where
  "solve_pg s dl 0 = (⋂ {ρ. ρ ⊨dl (dl ==s== 0)})"
| "solve_pg s dl (Suc n) = (⋂ {ρ. ρ ⊨dl (dl ==s== Suc n) ∧ (ρ ≤≤≤s≤≤≤ n) = solve_pg s dl n})"

definition least_rank_p_st :: "('p ⇒ bool) ⇒ 'p ⇒ ('p ⇒ nat) ⇒ bool" where 
  "least_rank_p_st P p s ⟷ P p ∧ (∀p'. P p' ⟶ s p ≤ s p')"

lemma least_rank_p_st_exists:
  assumes "P p"
  shows "∃p''. least_rank_p_st P p'' s"
  using assms
proof (induction "s p" arbitrary: p rule: less_induct)
  case less
  then show ?case
  proof (cases "∃p''. s p'' < s p ∧ P p''")
    case True
    then show ?thesis
      using less by auto
  next
    case False
    then show ?thesis
      by (metis least_rank_p_st_def less.prems linorder_not_le)
  qed
qed

lemma below_least_rank_p_st:
  assumes "least_rank_p_st P p'' s"
  assumes "s p < s p''"
  shows "¬P p"
  using assms 
proof (induction "s p''")
  case 0
  then show ?case by auto
next
  case (Suc n)
  then show ?case
    by (metis least_rank_p_st_def linorder_not_le)
qed

lemma lt_if_lt_prz:
  assumes "ρM ⊏s⊏prz ρN"
  shows "ρN ⊏s⊏ ρM"
proof -
  from assms have unf: 
    "ρN ≠ ρM"
    "∀pA cA. cA ∈ ρN pA - ρM pA ⟶ (∃pB cB. cB ∈ ρM pB - ρN pB ∧ s pB < s pA)"
    unfolding lt_prz_def by auto
  then have "∃p. ρN p ≠ ρM p"
    by auto
  then have "∃p. least_rank_p_st (λp. ρN p ≠ ρM p) p s"
    using least_rank_p_st_exists by smt
  then obtain p where "least_rank_p_st (λp. ρN p ≠ ρM p) p s"
    by auto
  have "ρN p ≠ ρM p"
    by (metis (mono_tags, lifting) ‹least_rank_p_st (λp. ρN p ≠ ρM p) p s› least_rank_p_st_def)
  then have "(∃c. c ∈ ρM p ∧ c ∉ ρN p) ∨ (∃c. c ∈ ρN p ∧ c ∉ ρM p)"
    by auto
  then show "ρN ⊏s⊏ ρM"
  proof 
    assume "∃c. c ∈ ρM p ∧ c ∉ ρN p"
    then obtain c where "c ∈ ρM p" "c ∉ ρN p"
      by auto
    have "(∀p'. s p' < s p ⟶ ρN p' = ρM p')"
      using ‹least_rank_p_st (λp. ρN p ≠ ρM p) p s› below_least_rank_p_st by fastforce
    have "(∀p'. s p' = s p ⟶ ρN p' ⊆ ρM p')"
      using ‹∀p'. s p' < s p ⟶ ρN p' = ρM p'› unf by auto
    then show ?thesis
      unfolding lt_def using ‹∀p'. s p' < s p ⟶ ρN p' = ρM p'› ‹ρN p ≠ ρM p› by blast
  next 
    assume "∃c. c ∈ ρN p ∧ c ∉ ρM p"
    then obtain c where "c ∈ ρN p ∧ c ∉ ρM p"
      by auto
    then have "∃pB cB. cB ∈ ρM pB - ρN pB ∧ s pB < s p"
      using unf by auto
    then obtain pB cB where "cB ∈ ρM pB - ρN pB" "s pB < s p"
      by auto
    then have "False"
      using ‹least_rank_p_st (λp. ρN p ≠ ρM p) p s› below_least_rank_p_st by fastforce
    then show ?thesis
      by auto
  qed
qed

lemma lt_prz_if_lt_if:
  assumes "ρM ⊏s⊏ ρN"
  shows "ρN ⊏s⊏prz ρM"
proof -
  have "ρM ≠ ρN"
    using assms lt_def by fastforce
  moreover
  have "(∀pA cA. cA ∈ ρM pA - ρN pA ⟶ (∃pB cB. cB ∈ ρN pB - ρM pB ∧ s pB < s pA))"
  proof (rule, rule, rule)
    fix pA cA
    assume "cA ∈ ρM pA - ρN pA"
    then show "∃pB cB. cB ∈ ρN pB - ρM pB ∧ s pB < s pA"
      by (smt (verit) DiffD1 DiffD2 antisym_conv3 assms lt_def psubset_imp_ex_mem subsetD)
  qed
  ultimately
  show "ρN ⊏s⊏prz ρM"
    unfolding lt_prz_def by auto
qed

lemma lt_prz_iff_lt:
  "ρM ⊏s⊏ ρN ⟷ ρN ⊏s⊏prz ρM"
  using lt_if_lt_prz lt_prz_if_lt_if by blast

lemma solves_leq:
  assumes "ρ ⊨dl (dl ≤≤s≤≤ m)"
  assumes "n ≤ m"
  shows "ρ ⊨dl (dl ≤≤s≤≤ n)"
  using assms unfolding solves_program_def by auto

lemma solves_Suc:
  assumes "ρ ⊨dl (dl ≤≤s≤≤ Suc n)"
  shows "ρ ⊨dl (dl ≤≤s≤≤ n)"
  by (meson assms lessI less_imp_le_nat solves_leq)

lemma solve_pg_0_subset:
  assumes "ρ ⊨dl (dl ≤≤s≤≤ 0)"
  shows "(solve_pg s dl 0) p ⊆ ρ p"
  using assms by (auto simp add: Inter'_def)

lemma solve_pg_Suc_subset:
  assumes "ρ ⊨dl (dl ==s== Suc n)"
  assumes "(ρ ≤≤≤s≤≤≤ n) = solve_pg s dl n"
  shows "(solve_pg s dl (Suc n)) p ⊆ ρ p"
  using assms by (force simp add: Inter'_def2)

lemma solve_pg_0_empty:
  assumes "s p > 0"
  shows "(solve_pg s dl 0) p = {}"
proof -
  define ρ'' :: "'a ⇒ 'b list set" where "ρ'' = (solve_pg s dl 0)"
  define ρ' :: "'a ⇒ 'b list set" where "ρ' = (λp. if s p = 0 then UNIV else {})"
  have "ρ' ⊨dl (dl ==s== 0)"
    unfolding solves_program_def solves_cls_def 
  proof (rule, rule)
    fix c σ
    assume c_dl0: "c ∈ (dl ==s== 0)"
    obtain p' ids rhs where c_split: "c = Cls p' ids rhs"
      by (cases c) auto
    then have sp'0: "s p' = 0" 
      using c_dl0 by auto
    have "⟦Cls p' ids rhs⟧cls ρ' σ"
      unfolding meaning_cls.simps
    proof (rule) 
      assume "⟦rhs⟧rhs ρ' σ"
      show "⟦(p', ids)⟧lh ρ' σ"
        using ρ'_def sp'0 by force
    qed
    then show "⟦c⟧cls ρ' σ"
      unfolding c_split by auto
  qed
  have "ρ'' p ⊆ ρ' p"
    using ‹ρ' ⊨dl (dl ==s== 0)› ρ''_def solve_pg_0_subset by fastforce
  then have "ρ'' p = {}"
    unfolding ρ'_def using assms(1) by simp
  then show ?thesis 
    unfolding ρ''_def by auto
qed

lemma solve_pg_above_empty:
  assumes "s p > n"
  shows "(solve_pg s dl n) p = {}"
  using assms proof (induction n arbitrary: p)
  case 0
  then show ?case
    using solve_pg_0_empty by metis
next
  case (Suc n)
  define ρ'' :: "'a ⇒ 'b list set" where 
    "ρ'' = (solve_pg s dl (Suc n))"
  define ρ' :: "'a ⇒ 'b list set" where 
    "ρ' = (λp. if s p < Suc n then (solve_pg s dl n) p else if s p = Suc n then UNIV else {})"

  have ρ'_solves: "ρ' ⊨dl (dl ==s== Suc n)"
    unfolding solves_program_def solves_cls_def 
  proof (rule, rule)
    fix c σ
    assume c_dlSucn: "c ∈ (dl ==s== Suc n)"
    obtain p' ids rhs where c_split: "c = Cls p' ids rhs"
      by (cases c) auto
    then have sp'Sucn: "s p' = Suc n" 
      using c_dlSucn by auto
    have "⟦Cls p' ids rhs⟧cls ρ' σ"
      unfolding meaning_cls.simps
    proof (rule)
      assume "⟦rhs⟧rhs ρ' σ"
      show "⟦(p', ids)⟧lh ρ' σ"
        using ρ'_def sp'Sucn by auto[]
    qed
    then show "⟦c⟧cls ρ' σ"
      unfolding c_split by auto
  qed
  have "∀p. (ρ' ≤≤≤s≤≤≤ n) p = (solve_pg s dl n) p"
    using Suc by (auto simp add: ρ'_def)
  then have "ρ'' p ⊆ ρ' p"
    using solve_pg_Suc_subset[of ρ' dl s n  p] ρ'_solves ρ''_def by force
  then have "ρ'' p = {}"
    unfolding ρ'_def using assms(1) Suc by simp
  then show ?case
    unfolding ρ''_def by auto
qed

lemma exi_sol_n: 
  "∃ρ'. ρ' ⊨dl (dl ==s== Suc m) ∧ (ρ' ≤≤≤s≤≤≤ m) = solve_pg s dl m"
proof -
  define ρ' where 
    "ρ' = (λp. (if s p < Suc m then (solve_pg s dl m) p else if s p = Suc m then UNIV else {}))"

  have "ρ' ⊨dl (dl ==s== Suc m)"
    unfolding ρ'_def solves_cls_def solves_program_def by fastforce
  moreover
  have "∀p. (ρ' ≤≤≤s≤≤≤ m) p = solve_pg s dl m p"
    unfolding ρ'_def using solve_pg_above_empty[of m s _ dl] by auto
  ultimately
  show ?thesis 
    by force
qed

lemma solve_pg_agree_above:
  assumes "s p ≤ m"
  shows "(solve_pg s dl m) p = (solve_pg s dl (s p)) p"
  using assms 
proof (induction m)
  case 0
  then show ?case
    by force
next
  case (Suc m)
  show ?case
  proof (cases "s p = Suc m")
    case True
    then show ?thesis by auto
  next
    case False
    then have s_p: "s p ≤ m"
      using Suc by auto
    then have solve_pg_sp_m: "(solve_pg s dl (s p)) p = (solve_pg s dl m) p"
      using Suc by auto
    have ρ'_solve_pg: "∀ρ'. ρ' ⊨dl (dl ==s== Suc m) ⟶
                           (ρ' ≤≤≤s≤≤≤ m) = solve_pg s dl m ⟶
                           ρ' p = solve_pg s dl m p"
      by (metis pred_val_lte_stratum.simps s_p)
    have "⋂ {ρ'. ρ' ⊨dl (dl ==s== Suc m) ∧ (ρ' ≤≤≤s≤≤≤ m) = solve_pg s dl m} p =
          solve_pg s dl (s p) p"
    proof (rule; rule)
      fix x 
      assume "x ∈ ⋂ {ρ'. ρ' ⊨dl (dl ==s== Suc m) ∧ (ρ' ≤≤≤s≤≤≤ m) = solve_pg s dl m} p"
      then show "x ∈ solve_pg s dl (s p) p"
        by (metis (mono_tags) CollectI ρ'_solve_pg exi_sol_n member_if_member_Inter' solve_pg_sp_m)
    next
      fix x
      assume "x ∈ solve_pg s dl (s p) p"
      then show "x ∈ ⋂ {ρ'. ρ' ⊨dl (dl ==s== Suc m) ∧ (ρ' ≤≤≤s≤≤≤ m) = solve_pg s dl m} p"
        by (simp add: ρ'_solve_pg member_Inter' solve_pg_sp_m)
    qed
    then show ?thesis
      by simp
  qed
qed

lemma solve_pg_two_agree_above:
  assumes "s p ≤ n"
  assumes "s p ≤ m"
  shows "(solve_pg s dl m) p = (solve_pg s dl n) p"
  using assms solve_pg_agree_above by metis

lemma pos_rhs_stratum_leq_clause_stratum:
  assumes "strat_wf s dl"
  assumes "Cls p ids rhs ∈ dl"
  assumes "+ p' ids' ∈ set rhs"
  shows "s p' ≤ s p"
  using assms unfolding strat_wf_def by fastforce

lemma neg_rhs_stratum_less_clause_stratum:
  assumes "strat_wf s dl"
  assumes "Cls p ids rhs ∈ dl"
  assumes "¬ p' ids' ∈ set rhs"
  shows "s p' < s p"
  using assms unfolding strat_wf_def by fastforce

lemma solve_pg_two_agree_above_on_rh:
  assumes "strat_wf s dl"
  assumes "Cls p ids rhs ∈ dl"
  assumes "s p ≤ n"
  assumes "s p ≤ m"
  assumes "rh ∈ set rhs"
  shows "⟦rh⟧rh (solve_pg s dl m) σ ⟷ ⟦rh⟧rh (solve_pg s dl n) σ"
proof (cases rh)
  case (Eql a a')
  then show ?thesis
    using assms by auto
next
  case (Neql a a')
  then show ?thesis 
    using assms by auto
next
  case (PosLit p' ids')
  then have "s p' ≤ m"
    using assms pos_rhs_stratum_leq_clause_stratum by fastforce
  moreover
  from PosLit have "s p' ≤ n"
    using assms pos_rhs_stratum_leq_clause_stratum by fastforce
  ultimately
  have "solve_pg s dl m p' = solve_pg s dl n p'"
    using solve_pg_two_agree_above[of s p' n m dl] by force
  then show ?thesis
    by (simp add: PosLit)
next
  case (NegLit p' ids)
  then have "s p' < m"
    using assms neg_rhs_stratum_less_clause_stratum by fastforce
  moreover
  from NegLit have "s p' < n"
    using assms neg_rhs_stratum_less_clause_stratum by fastforce
  ultimately
  have "solve_pg s dl m p' = solve_pg s dl n p'"
    using solve_pg_two_agree_above[of s p' n m dl] by force
  then show ?thesis
    by (simp add: NegLit)
qed

lemma solve_pg_two_agree_above_on_lh:
  assumes "s p ≤ n"
  assumes "s p ≤ m"
  shows "⟦(p,ids)⟧lh (solve_pg s dl m) σ ⟷ ⟦(p,ids)⟧lh (solve_pg s dl n) σ"
  by (metis assms meaning_lh.simps solve_pg_two_agree_above)

lemma solve_pg_two_agree_above_on_cls:
  assumes "strat_wf s dl"
  assumes "Cls p ids rhs ∈ dl"
  assumes "s p ≤ n"
  assumes "s p ≤ m"
  shows "⟦Cls p ids rhs⟧cls (solve_pg s dl n) σ ⟷ ⟦Cls p ids rhs⟧cls (solve_pg s dl m) σ"
  using assms solve_pg_two_agree_above_on_rh solve_pg_two_agree_above_on_lh
  by (meson meaning_rhs.simps meaning_cls.simps)

lemma solve_pg_two_agree_above_on_cls_Suc:
  assumes "strat_wf s dl"
  assumes "Cls p ids rhs ∈ dl"
  assumes "s p ≤ n"
  shows "⟦Cls p ids rhs⟧cls (solve_pg s dl (Suc n)) σ ⟷ ⟦Cls p ids rhs⟧cls (solve_pg s dl n) σ"
  using solve_pg_two_agree_above_on_cls[OF assms(1,2,3), of "Suc n" σ] assms(3) by auto

lemma stratum0_no_neg':
  assumes "strat_wf s dl"
  assumes "Cls p ids rhs ∈ dl"
  assumes "s p = 0"
  assumes "rh ∈ set rhs"
  shows "∄p' ids. rh = ¬ p' ids"
  by (metis One_nat_def add_eq_0_iff_both_eq_0 assms bot_nat_0.extremum_uniqueI 
      bot_nat_0.not_eq_extremum rnk.simps(4) strat_wf_cls.simps strat_wf_def zero_less_Suc)

lemma stratumSuc_less_neg':
  assumes "strat_wf s dl"
  assumes "Cls p ids rhs ∈ dl"
  assumes "s p = Suc n"
  assumes "¬ p' ids' ∈ set rhs"
  shows "s p' ≤ n"
  using assms unfolding strat_wf_def by force

lemma stratum0_no_neg:
  assumes "strat_wf s dl"
  assumes "Cls p ids rhs ∈ (dl ≤≤s≤≤ 0)"
  assumes "rh ∈ set rhs"
  shows "∄p' ids. rh = ¬ p ids"
  using assms stratum0_no_neg' by fastforce 

lemma stratumSuc_less_neg:
  assumes "strat_wf s dl"
  assumes "Cls p ids rhs ∈ (dl ≤≤s≤≤ Suc n)"
  assumes "¬ p' ids' ∈ set rhs"
  shows "s p' ≤ n"
  using assms neg_rhs_stratum_less_clause_stratum by fastforce

lemma all_meaning_rh_if_solve_pg_0:
  assumes "strat_wf s dl"
  assumes "⟦rh⟧rh (solve_pg s dl 0) σ"
  assumes "ρ ⊨dl (dl ≤≤s≤≤ 0)"
  assumes "rh ∈ set rhs"
  assumes "Cls p ids rhs ∈ (dl ≤≤s≤≤ 0)"
  shows "⟦rh⟧rh ρ σ"
proof (cases rh)
  case (Eql a1 a2)
  then show ?thesis
    using assms by auto
next
  case (Neql a1 a2)
  then show ?thesis
    using assms by auto
next
  case (PosLit p ids)
  then show ?thesis
    using assms meaning_rh.simps(3) solve_pg_0_subset by fastforce
next
  case (NegLit p ids)
  then show ?thesis
    using assms stratum0_no_neg' by fastforce
qed

lemma all_meaning_rh_if_solve_pg_Suc:
  assumes "strat_wf s dl"
  assumes "⟦rh⟧rh (solve_pg s dl (Suc n)) σ"
  assumes "ρ ⊨dl (dl ==s== Suc n)"
  assumes "(ρ ≤≤≤s≤≤≤ n) = solve_pg s dl n"
  assumes "rh ∈ set rhs"
  assumes "Cls p ids rhs ∈ (dl ≤≤s≤≤ Suc n)"
  shows "⟦rh⟧rh ρ σ"
proof (cases rh)
  case (Eql a a')
  then show ?thesis
    using assms(2) by auto
next
  case (Neql a a')
  then show ?thesis
    using assms(2) by force
next
  case (PosLit p' ids')
  then show ?thesis
    using assms solve_pg_Suc_subset by fastforce
next
  case (NegLit p' ids')
  then have "s p' ≤ n"
    using stratumSuc_less_neg[OF assms(1) assms(6), of p'] assms(5) by auto
  then have "⟦rh⟧rh (solve_pg s dl n) σ"
    by (metis NegLit assms(2) le_imp_less_Suc less_imp_le_nat meaning_rh.simps(4) 
        solve_pg_two_agree_above)
  then have "⟦rh⟧rh (ρ ≤≤≤s≤≤≤ n) σ"
    using assms(4) by presburger
  then show ?thesis
    by (simp add: NegLit ‹s p' ≤ n›)
qed

lemma solve_pg_0_if_all_meaning_lh:
  assumes "∀ρ'. ρ' ⊨dl (dl ≤≤s≤≤ 0) ⟶ ⟦(p, ids)⟧lh ρ' σ"
  shows "⟦(p, ids)⟧lh (solve_pg s dl 0) σ"
  using assms by (auto simp add: Inter'_def)

lemma all_meaning_lh_if_solve_pg_0:
  assumes "⟦(p, ids)⟧lh (solve_pg s dl 0) σ"
  shows "∀ρ'. ρ' ⊨dl (dl ≤≤s≤≤ 0) ⟶ ⟦(p, ids)⟧lh ρ' σ"
  using assms by (auto simp add: Inter'_def)

lemma solve_pg_0_iff_all_meaning_lh:
  "⟦(p, ids)⟧lh (solve_pg s dl 0) σ ⟷ (∀ρ'. ρ' ⊨dl (dl ≤≤s≤≤ 0) ⟶ ⟦(p, ids)⟧lh ρ' σ)"
  using solve_pg_0_if_all_meaning_lh all_meaning_lh_if_solve_pg_0 by metis

lemma solve_pg_Suc_if_all_meaning_lh:
  assumes "∀ρ'. ρ' ⊨dl (dl ==s== Suc n) ⟶ (ρ' ≤≤≤s≤≤≤ n) = solve_pg s dl n ⟶ ⟦(p, ids)⟧lh ρ' σ"
  shows "⟦(p, ids)⟧lh (solve_pg s dl (Suc n)) σ"
  using assms by (auto simp add: Inter'_def)

lemma all_meaning_if_solve_pg_Suc_lh:
  assumes "⟦(p, ids)⟧lh (solve_pg s dl (Suc n)) σ"
  shows "∀ρ'. ρ' ⊨dl (dl ==s== Suc n) ⟶ (ρ' ≤≤≤s≤≤≤ n) = solve_pg s dl n ⟶ ⟦(p, ids)⟧lh ρ' σ"
  using assms by (auto simp add: Inter'_def)

lemma solve_pg_Suc_iff_all_meaning_lh:
  "(⟦(p, ids)⟧lh (solve_pg s dl (Suc n)) σ) ⟷
   (∀ρ'. ρ' ⊨dl (dl ==s== Suc n) ⟶ (ρ' ≤≤≤s≤≤≤ n) = solve_pg s dl n ⟶ ⟦(p, ids)⟧lh ρ' σ)"
  by (auto simp add: Inter'_def)

lemma solve_pg_0_meaning_cls':
  assumes "strat_wf s dl"
  assumes "Cls p ids rhs ∈ (dl ≤≤s≤≤ 0)"
  shows "⟦Cls p ids rhs⟧cls (solve_pg s dl 0) σ"
  unfolding meaning_cls.simps
proof
  define ρ'' :: "'a ⇒ 'c list set" where "ρ'' = (solve_pg s dl 0)"
  assume "⟦rhs⟧rhs (solve_pg s dl 0) σ"
  then have "∀ρ'. ρ' ⊨dl (dl ≤≤s≤≤ 0) ⟶ (∀rh∈set rhs. ⟦rh⟧rh ρ' σ)"
    using all_meaning_rh_if_solve_pg_0[OF assms(1), of _ σ _ rhs p ids, OF _ _ _ assms(2)] 
    by auto
  then have "∀ρ'. ρ' ⊨dl (dl ≤≤s≤≤ 0) ⟶ ⟦(p, ids)⟧lh  ρ' σ"
    by (metis assms(2) meaning_cls.simps solves_cls_def solves_program_def meaning_rhs.simps)
  then show "⟦(p, ids)⟧lh (solve_pg s dl 0) σ"
    using solve_pg_0_if_all_meaning_lh by auto
qed

lemma solve_pg_meaning_cls':
  assumes "strat_wf s dl"
  assumes "Cls p ids rhs ∈ (dl ≤≤s≤≤ n)"
  shows "⟦Cls p ids rhs⟧cls (solve_pg s dl n) σ"
  unfolding meaning_cls.simps
  using assms
proof (induction n)
  case 0
  then show ?case
    using solve_pg_0_meaning_cls' unfolding meaning_cls.simps by metis 
next
  case (Suc n)
  have leq_n: "s p ≤ Suc n"
    using Suc.prems(2) by auto

  have cls_in: "Cls p ids rhs ∈ dl"
    using assms(2) by force

  show ?case
  proof (cases "s p = Suc n")
    case True
    have cls_in_Suc: "Cls p ids rhs ∈ (dl ==s== Suc n)"
      by (simp add: True cls_in)
    show ?thesis
    proof
      define ρ'' :: "'a ⇒ 'c list set" where "ρ'' = (solve_pg s dl (Suc n))"
      assume "⟦rhs⟧rhs (solve_pg s dl (Suc n)) σ"
      then have 
        "∀ρ'. ρ' ⊨dl (dl ==s== Suc n) ⟶ 
              (ρ' ≤≤≤s≤≤≤ n) = solve_pg s dl n ⟶ 
              (∀rh∈set rhs. ⟦rh⟧rh ρ' σ)"
        using all_meaning_rh_if_solve_pg_Suc[OF assms(1) _ _ _ _ Suc(3), of _ σ] 
        by auto
      then have "∀ρ'. ρ' ⊨dl (dl ==s== Suc n) ⟶
                 (ρ' ≤≤≤s≤≤≤ n) = solve_pg s dl n ⟶ 
                 ⟦(p, ids)⟧lh ρ' σ"
        using meaning_cls.simps solves_cls_def solves_program_def cls_in_Suc meaning_rhs.simps by metis
      then show "⟦(p, ids)⟧lh (solve_pg s dl (Suc n)) σ"
        using solve_pg_Suc_if_all_meaning_lh[of dl s n p ids σ] by auto
    qed
  next
    case False
    then have False': "s p < Suc n"
      using leq_n by auto
    then have s_p_n: "s p ≤ n"
      by auto
    then have "Cls p ids rhs ∈ (dl ≤≤s≤≤ n)"
      by (simp add: cls_in)
    then have "(∀rh∈set rhs. ⟦rh⟧rh (solve_pg s dl n) σ) ⟶ ⟦(p, ids)⟧lh (solve_pg s dl n) σ"
      using Suc by auto
    then show ?thesis
      using False' meaning_cls.simps solve_pg_two_agree_above_on_cls_Suc assms cls_in s_p_n 
        meaning_rhs.simps by metis
  qed
qed

lemma solve_pg_meaning_cls:
  assumes "strat_wf s dl"
  assumes "c ∈ (dl ≤≤s≤≤ n)"
  shows "⟦c⟧cls (solve_pg s dl n) σ"
  using assms solve_pg_meaning_cls'[of s dl] by (cases c) metis

lemma solve_pg_solves_cls:
  assumes "strat_wf s dl"
  assumes "c ∈ (dl ≤≤s≤≤ n)"
  shows "solve_pg s dl n ⊨cls c"
  unfolding solves_cls_def using solve_pg_meaning_cls assms by blast

lemma solve_pg_solves_dl:
  assumes "strat_wf s dl"
  shows "solve_pg s dl n ⊨dl (dl ≤≤s≤≤ n)"
proof -
  have "∀c ∈ (dl ≤≤s≤≤ n). (solve_pg s dl n) ⊨cls c"
    using assms solve_pg_solves_cls[of s dl] by auto
  then show "solve_pg s dl n ⊨dl (dl ≤≤s≤≤ n)"
    using solves_program_def by blast
qed

lemma disjE3:
  assumes major: "P ∨ Q ∨ Z"
    and minorP: "P ⟹ R"
    and minorQ: "Q ⟹ R"
    and minorZ: "Z ⟹ R"
  shows R
  using assms by auto

lemma solve_pg_0_below_solution:
  assumes "ρ ⊨dl (dl ≤≤s≤≤ 0)"
  shows "(solve_pg s dl 0) ⊑s⊑ ρ"
proof -
  define ρ'' :: "'a ⇒ 'b list set" where "ρ'' = solve_pg s dl 0"

  have "ρ'' ≠ ρ ⟶ ρ'' ⊏s⊏ ρ"
  proof 
    assume "ρ'' ≠ ρ"
    have ρ''_subs_ρ: "∀p. ρ'' p ⊆ ρ p"
      using solve_pg_0_subset unfolding ρ''_def using assms(1) by force
    have "∃p. least_rank_p_st (λp. ρ'' p ≠ ρ p) p s"
      by (meson ‹ρ'' ≠ ρ› ext least_rank_p_st_exists)
    then obtain p where p_p: "least_rank_p_st (λp. ρ'' p ≠ ρ p) p s"
      by auto
    then have "ρ'' p ⊂ ρ p"
      by (metis (mono_tags, lifting) ρ''_subs_ρ least_rank_p_st_def psubsetI)
    moreover
    have "∀p'. s p' = s p ⟶ ρ'' p' ⊆ ρ p'"
      using ρ''_subs_ρ by auto
    moreover
    have "∀p'. s p' < s p ⟶ ρ'' p' = ρ p'"
      using below_least_rank_p_st[OF p_p] by auto
    ultimately
    show "ρ'' ⊏s⊏ ρ"
      unfolding lt_def by auto
  qed
  then show ?thesis
    using ρ''_def lte_def by auto
qed

lemma least_disagreement_proper_subset:
  assumes "ρ''n ⊏s⊏ ρ"
  assumes "least_rank_p_st (λp. ρ''n p ≠ ρ p) p s"
  shows "ρ''n p ⊂ ρ p"
proof -
  from assms obtain p'' where p''_p:
    "ρ''n p'' ⊂ ρ p''"
    "(∀p'. s p' = s p'' ⟶ ρ''n p' ⊆ ρ p')"
    "(∀p'. s p' < s p'' ⟶ ρ''n p' = ρ p')"
    unfolding lt_def by auto
  moreover
  from p''_p have "s p'' = s p"
    by (metis (mono_tags, lifting) antisym_conv2 assms(2) least_rank_p_st_def)
  ultimately
  show ?thesis
    by (metis (mono_tags, lifting) assms(2) least_rank_p_st_def psubsetI)
qed

lemma subset_on_least_disagreement:
  assumes "ρ''n ⊏s⊏ ρ"
  assumes "least_rank_p_st (λp. ρ''n p ≠ ρ p) p s"
  assumes "s p' = s p"
  shows "ρ''n p' ⊆ ρ p'"
proof -
  from assms obtain p'' where p''_p:
    "ρ''n p'' ⊂ ρ p''"
    "(∀p'. s p' = s p'' ⟶ ρ''n p' ⊆ ρ p')"
    "(∀p'. s p' < s p'' ⟶ ρ''n p' = ρ p')"
    unfolding lt_def by auto
  moreover
  from p''_p have "s p'' = s p"
    by (metis (mono_tags, lifting) antisym_conv2 assms(2) least_rank_p_st_def)
  ultimately
  show ?thesis
    using assms by metis
qed

lemma equal_below_least_disagreement:
  assumes "ρ''n ⊏s⊏ ρ"
  assumes "least_rank_p_st (λp. ρ''n p ≠ ρ p) p s"
  assumes "s p' < s p"
  shows "ρ''n p' = ρ p'"
proof -
  from assms obtain p'' where p''_p:
    "ρ''n p'' ⊂ ρ p''"
    "(∀p'. s p' = s p'' ⟶ ρ''n p' ⊆ ρ p')"
    "(∀p'. s p' < s p'' ⟶ ρ''n p' = ρ p')"
    unfolding lt_def by auto
  moreover
  from p''_p have "s p'' = s p"
    by (metis (mono_tags, lifting) antisym_conv2 assms(2) least_rank_p_st_def)
  ultimately
  show ?thesis
    using assms by metis
qed

lemma solution_on_subset_solution_below:
  "(dl ==s== n) ⊆ (dl ≤≤s≤≤ n)"
  by fastforce

lemma solves_program_mono:
  assumes "dl ⊆ dl'"
  assumes "ρ ⊨dl dl'"
  shows "ρ ⊨dl dl"
  by (meson assms in_mono solves_program_def)

lemma solution_on_if_solution_below:
  assumes "ρ ⊨dl (dl ≤≤s≤≤ n)"
  shows  "ρ ⊨dl (dl ==s== n)"
  by (meson assms solves_program_mono solution_on_subset_solution_below)

lemma solve_pg_Suc_subset_solution:
  assumes "ρ ⊨dl (dl ≤≤s≤≤ Suc n)"
  assumes "(ρ ≤≤≤s≤≤≤ n) = solve_pg s dl n"
  shows "solve_pg s dl (Suc n) p ⊆ ρ p"
  by (meson assms solution_on_if_solution_below solve_pg_Suc_subset)

lemma solve_pg_subset_solution:
  assumes "m > n"
  assumes "ρ ⊨dl (dl ≤≤s≤≤ m)"
  assumes "(ρ ≤≤≤s≤≤≤ n) = solve_pg s dl n"
  shows "solve_pg s dl (Suc n) p ⊆ ρ p"
  by (meson Suc_leI assms solve_pg_Suc_subset_solution solves_leq)

lemma below_least_disagreement:
  assumes "least_rank_p_st (λp. ρ' p ≠ ρ p) p s"
  assumes "s p' < s p"
  shows "ρ' p' = ρ p'"
  using assms below_least_rank_p_st by fastforce

definition agree_below_eq :: "('p,'c) pred_val ⇒ ('p,'c) pred_val ⇒ nat ⇒ 'p strat ⇒ bool"  where
  "agree_below_eq ρ ρ' n s ⟷ (∀p. s p ≤ n ⟶ ρ p = ρ' p)"

definition agree_below :: "('p,'c) pred_val ⇒ ('p,'c) pred_val ⇒ nat ⇒ 'p strat ⇒ bool"  where
  "agree_below ρ ρ' n s ⟷ (∀p. s p < n ⟶ ρ p = ρ' p)"

definition agree_above :: "('p,'c) pred_val ⇒ ('p,'c) pred_val ⇒ nat ⇒ 'p strat ⇒ bool"  where
  "agree_above ρ ρ' n s ⟷ (∀p. s p > n ⟶ ρ p = ρ' p)"

definition agree_above_eq :: "('p,'c) pred_val ⇒ ('p,'c) pred_val ⇒ nat ⇒ 'p strat ⇒ bool" where
  "agree_above_eq ρ ρ' n s ⟷ (∀p. s p ≥ n ⟶ ρ p = ρ' p)"

lemma agree_below_trans:
  assumes "agree_below_eq ρ ρ' n s"
  assumes "agree_below_eq ρ' ρ'' n s"
  shows "agree_below_eq ρ ρ'' n s"
  using assms unfolding agree_below_eq_def by auto

lemma agree_below_eq_less_eq:
  assumes "l ≤ n"
  assumes "agree_below_eq ρ ρ' n s"
  shows "agree_below_eq ρ ρ' l s"
  using assms unfolding agree_below_eq_def by auto

lemma agree_below_trans':
  assumes "agree_below_eq ρ ρ' n s"
  assumes "agree_below_eq ρ' ρ'' m s"
  assumes "l ≤ n"
  assumes "l ≤ m"
  shows "agree_below_eq ρ ρ'' l s"
  using assms unfolding agree_below_eq_def by auto

lemma agree_below_eq_least_disagreement:
  assumes "least_rank_p_st (λp. ρ' p ≠ ρ p) p s"
  assumes "n < s p"
  shows "agree_below_eq ρ' ρ n s"
  using agree_below_eq_def assms(1) assms(2) below_least_rank_p_st by fastforce

lemma agree_below_least_disagreement:
  assumes "least_rank_p_st (λp. ρ' p ≠ ρ p) p s"
  shows "agree_below ρ' ρ (s p) s"
  using agree_below_def assms below_least_rank_p_st by fastforce

lemma eq_if_agree_below_eq_agree_above:
  assumes "agree_below_eq ρ ρ' n s"
  assumes "agree_above ρ ρ' n s"
  shows "ρ = ρ'"
  by (metis agree_above_def agree_below_eq_def assms ext le_eq_less_or_eq nat_le_linear)

lemma eq_if_agree_below_agree_above_eq:
  assumes "agree_below ρ ρ' n s"
  assumes "agree_above_eq ρ ρ' n s"
  shows "ρ = ρ'"
  by (metis agree_above_eq_def agree_below_def assms ext le_eq_less_or_eq nat_le_linear)
  

lemma eq_if_agree_below_eq_agree_above_eq:
  assumes "agree_below_eq ρ ρ' n s"
  assumes "agree_above_eq ρ ρ' n s"
  shows "ρ = ρ'"
  by (meson agree_above_def agree_above_eq_def eq_if_agree_below_eq_agree_above assms 
      less_imp_le_nat)

lemma agree_below_eq_pred_val_lte_stratum:
  "agree_below_eq ρ (ρ ≤≤≤s≤≤≤ n) n s"
  by (simp add: agree_below_eq_def)

lemma agree_below_eq_pred_val_lte_stratum_less_eq:
  assumes "m ≤ n"
  shows "agree_below_eq ρ (ρ ≤≤≤s≤≤≤ n) m s"
  using agree_below_eq_less_eq agree_below_eq_pred_val_lte_stratum assms by blast

lemma agree_below_eq_solve_pg:
  assumes "l ≤ m"
  assumes "l ≤ n"
  shows "agree_below_eq (solve_pg s dl n) (solve_pg s dl m) l s"
  unfolding agree_below_eq_def by (meson assms dual_order.trans solve_pg_two_agree_above)    

lemma solve_pg_below_solution:
  assumes "ρ ⊨dl (dl ≤≤s≤≤ n)"
  shows "solve_pg s dl n ⊑s⊑ ρ"
  using assms
proof (induction n arbitrary: ρ)
  case 0
  then show ?case
    using solve_pg_0_below_solution by blast
next
  case (Suc n)
  define ρ''n :: "'a ⇒ 'b list set" where "ρ''n = solve_pg s dl n"
  define ρ''n1 :: "'a ⇒ 'b list set" where "ρ''n1 = solve_pg s dl (Suc n)"

  have ρ''n_below_ρ: "ρ''n ⊑s⊑ ρ"
    using Suc.IH Suc.prems ρ''n_def solves_Suc by blast

  have agree_ρ''n1_ρ''n: "agree_below_eq ρ''n1 ρ''n n s"
    unfolding ρ''n_def ρ''n1_def using agree_below_eq_solve_pg using le_Suc_eq by blast

  have "ρ''n1 ⊑s⊑ ρ"
    unfolding lte_def2
  proof
    assume "ρ''n1 ≠ ρ"
    then have "∃p. least_rank_p_st (λp. ρ''n1 p ≠ ρ p) p s"
      using least_rank_p_st_exists[of "(λp. ρ''n1 p ≠ ρ p)"] by force
    then obtain p where p_p: "least_rank_p_st (λp. ρ''n1 p ≠ ρ p) p s"
      by blast
    then have dis: "ρ''n1 p ≠ ρ p"
      unfolding least_rank_p_st_def by auto
    from p_p have agg: "agree_below ρ''n1 ρ (s p) s"
      by (simp add: agree_below_least_disagreement)

    define i where "i = s p"
    have "i < Suc n ∨ Suc n ≤ i"
      by auto
    then show "ρ''n1 ⊏s⊏ ρ"
    proof (rule disjE)
      assume "i < Suc n"
      then have "s p ≤ n"
        unfolding i_def by auto
      then have "ρ''n p ≠ ρ p"
        by (metis agree_ρ''n1_ρ''n agree_below_eq_def dis)

      have "ρ''n ⊏s⊏ ρ"
        by (metis ρ''n_below_ρ ‹ρ''n p ≠ ρ p› lte_def)
      moreover
      have "∀p'. ρ''n p' ≠ ρ p' ⟶ s p ≤ s p'"
        by (metis agree_ρ''n1_ρ''n ‹s p ≤ n› agg agree_below_def agree_below_eq_def le_trans 
            linorder_le_cases linorder_le_less_linear)
      then have "least_rank_p_st (λp. ρ''n p ≠ ρ p) p s"
          using ‹ρ''n p ≠ ρ p› unfolding least_rank_p_st_def by auto
      ultimately
      have "ρ''n p ⊂ ρ p ∧
           (∀p'. s p' = s p ⟶ ρ''n p' ⊆ ρ p') ∧
           (∀p'. s p' < s p ⟶ ρ''n p' = ρ p')"
        using least_disagreement_proper_subset[of ρ''n s ρ p]
          subset_on_least_disagreement[of ρ''n s ρ p] equal_below_least_disagreement[of ρ''n s ρ p] 
        by metis
      then have "ρ''n1 p ⊂ ρ p ∧
           (∀p'. s p' = s p ⟶ ρ''n1 p' ⊆ ρ p') ∧
           (∀p'. s p' < s p ⟶ ρ''n1 p' = ρ p')"
        using agree_ρ''n1_ρ''n ‹s p ≤ n› by (simp add: agree_below_eq_def)
      then show "ρ''n1 ⊏s⊏ ρ"
        unfolding lt_def by auto
    next
      assume "Suc n ≤ i"
      have "ρ ⊨dl (dl ≤≤s≤≤ Suc n)"
        using Suc.prems by auto
      moreover
      have "(ρ ≤≤≤s≤≤≤ n) = (solve_pg s dl n)"
      proof -
        have "agree_below_eq ρ''n ρ''n1 n s"
          by (metis agree_ρ''n1_ρ''n agree_below_eq_def)
        moreover
        have "agree_below_eq ρ''n1 ρ n s"
          using ‹Suc n ≤ i› agree_below_eq_least_disagreement i_def p_p by fastforce
        moreover
        have "agree_below_eq ρ (ρ ≤≤≤s≤≤≤ n) n s"
          by (simp add: agree_below_eq_pred_val_lte_stratum)
        ultimately
        have "agree_below_eq ρ''n (ρ ≤≤≤s≤≤≤ n) n s"
          using agree_below_trans by metis
        moreover
        have "agree_above ρ''n (ρ ≤≤≤s≤≤≤ n) n s"
          using ρ''n_def by (simp add: agree_above_def solve_pg_above_empty)
        ultimately
        have "(ρ ≤≤≤s≤≤≤ n) = ρ''n"
           using eq_if_agree_below_eq_agree_above by blast
        then show "(ρ ≤≤≤s≤≤≤ n) = (solve_pg s dl n)"
          using ρ''n_def by metis
      qed
      ultimately
      have "ρ ⊨dl (dl ≤≤s≤≤ Suc n) ∧ (ρ ≤≤≤s≤≤≤ n) = solve_pg s dl n"
        by auto
      then have "ρ''n1 p ⊆ ρ p"
        using solve_pg_subset_solution[of n "Suc n" ρ dl s p]
        using ρ''n1_def by fastforce 
      then have "ρ''n1 p ⊂ ρ p"
        using dis by auto
      moreover
      have "∀p'. s p' = s p ⟶ ρ''n1 p' ⊆ ρ p'"
        using ‹ρ ⊨dl (dl ≤≤s≤≤ Suc n) ∧ (ρ ≤≤≤s≤≤≤ n) = solve_pg s dl n› ρ''n1_def 
          solve_pg_subset_solution by fastforce
      moreover
      have "∀p'. s p' < s p ⟶ ρ''n1 p' = ρ p'"
        using below_least_rank_p_st p_p by fastforce
      ultimately
      show "ρ''n1 ⊏s⊏ ρ"
        unfolding lt_def by auto
    qed
  qed
  then show ?case
    unfolding ρ''n1_def by auto
qed

lemma solve_pg_least_solution':
  assumes "strat_wf s dl"
  shows "solve_pg s dl n ⊨lst (dl ≤≤s≤≤ n) s"
  using assms least_solution_def solve_pg_below_solution solve_pg_solves_dl by blast 

lemma stratum_less_eq_max_stratum:
  assumes "finite dl"
  assumes "Cls p ids rhs ∈ dl"
  shows "s p ≤ max_stratum s dl"
proof -
  have "s p ∈ {s p | p ids rhs. Cls p ids rhs ∈ dl}"
    using assms(2) by auto
  moreover
  have "{s p | p ids rhs. Cls p ids rhs ∈ dl} = (λc. (case c of Cls p ids rhs ⇒ s p)) ` dl"
    unfolding image_def by (metis (mono_tags, lifting) clause.case the_lh.cases)
  then have "finite {s p | p ids rhs. Cls p ids rhs ∈ dl}"
    by (simp add: assms(1))
  ultimately
  show ?thesis
    unfolding max_stratum_def using Max.coboundedI by auto
qed

lemma finite_above_max_stratum:
  assumes "finite dl"
  assumes "max_stratum s dl ≤ n"
  shows "(dl ≤≤s≤≤ n) = dl"
proof (rule; rule)
  fix c
  assume "c ∈ (dl ≤≤s≤≤ n)"
  then show "c ∈ dl"
    by auto
next
  fix c
  assume c_in_dl: "c ∈ dl"
  then obtain p ids rhs where c_split: "c = Cls p ids rhs"
    by (cases c) auto
  then have c_in_dl': "Cls p ids rhs ∈ dl"
    using c_in_dl by auto
  then have "s p ≤ max_stratum s dl"
    using stratum_less_eq_max_stratum assms by metis
  then have "Cls p ids rhs ∈ (dl ≤≤s≤≤ n)"
    using c_in_dl' assms(2) by auto 
  then show "c ∈ (dl ≤≤s≤≤ n)"
    unfolding c_split by auto
qed 

lemma finite_max_stratum:
  assumes "finite dl"
  shows "(dl ≤≤s≤≤ max_stratum s dl) = dl"
  using assms finite_above_max_stratum[of dl s "max_stratum s dl"] by auto 

lemma solve_pg_least_solution:
  assumes "finite dl"
  assumes "strat_wf s dl"
  shows "solve_pg s dl (max_stratum s dl) ⊨lst dl s"
proof -
  have "solve_pg s dl (max_stratum s dl) ⊨lst (dl ≤≤s≤≤ (max_stratum s dl)) s"
    using solve_pg_least_solution' assms by auto
  then show ?thesis
    using finite_max_stratum assms by metis
qed

lemma exi_least_solution:
  assumes "finite dl"
  assumes "strat_wf s dl"
  shows "∃ρ. ρ ⊨lst dl s"
  using assms solve_pg_least_solution by metis


subsubsection ‹Equality of least and minimal solution›

lemma least_iff_minimal:
  assumes "finite dl"
  assumes "strat_wf s dl"
  shows "ρ ⊨lst dl s ⟷ ρ ⊨min dl s"
proof
  assume "ρ ⊨lst dl s"
  then have ρ_least: "ρ ⊨dl dl" "(∀σ'. σ' ⊨dl dl ⟶ ρ ⊑s⊑ σ')"
    unfolding least_solution_def by auto
  then have "(∄ρ'. ρ' ⊨dl dl ∧ ρ' ⊏s⊏ ρ)"
    by (metis (full_types) ‹∀ρ'. ρ' ⊨dl dl ⟶ ρ ⊑s⊑ ρ'› lt_def lte_def nat_neq_iff psubsetE)
  then show "ρ ⊨min dl s"
    unfolding minimal_solution_def using ρ_least by metis
next
  assume min: "ρ ⊨min dl s"
  have "∃ρ'. ρ' ⊨lst dl s"
    using solve_pg_least_solution assms by metis
  then show "ρ ⊨lst dl s"
    by (metis min least_solution_def lte_def minimal_solution_def)
qed


subsubsection ‹Least solution on lower strata›

lemma below_subset:
  "(dl ≤≤s≤≤ n) ⊆ dl"
  by auto

lemma finite_below_finite:
  assumes "finite dl"
  shows "finite (dl ≤≤s≤≤ n)"
  using assms finite_subset below_subset by metis

lemma downward_least_solution:
  assumes "finite dl"
  assumes "n > m"
  assumes "strat_wf s dl"
  assumes "ρ ⊨lst (dl ≤≤s≤≤ n) s"
  shows "(ρ ≤≤≤s≤≤≤ m) ⊨lst (dl ≤≤s≤≤ m) s"
proof (rule ccontr)
  assume a: "¬ (ρ ≤≤≤s≤≤≤ m) ⊨lst (dl ≤≤s≤≤ m) s"
  have s_dl_m: "strat_wf s (dl ≤≤s≤≤ m)"
    using assms strat_wf_lte_if_strat_wf by auto
  have strat_wf_n: "strat_wf s (dl ≤≤s≤≤ n)"
    using assms strat_wf_lte_if_strat_wf by auto
  from a have "¬ (ρ ≤≤≤s≤≤≤ m) ⊨min (dl ≤≤s≤≤ m) s"
    using least_iff_minimal s_dl_m assms(1) finite_below_finite by metis
  moreover 
  have "(ρ ≤≤≤s≤≤≤ m) ⊨dl (dl ≤≤s≤≤ m)"
    using assms downward_lte_solves least_solution_def by blast
  ultimately
  have "(∃σ'. σ' ⊨dl (dl ≤≤s≤≤ m) ∧ (σ' ⊏s⊏ (ρ ≤≤≤s≤≤≤ m)))"
    unfolding minimal_solution_def by auto
  then obtain ρ' where ρ'_p1: "ρ' ⊨dl (dl ≤≤s≤≤ m)" and ρ'_p2: "(ρ' ⊏s⊏ (ρ ≤≤≤s≤≤≤ m))"
    by auto
  then have "∃p. ρ' p ⊂ (ρ ≤≤≤s≤≤≤ m) p ∧
                    (∀p'. s p' = s p ⟶ ρ' p' ⊆ (ρ ≤≤≤s≤≤≤ m) p') ∧
                    (∀p'. s p' < s p ⟶ ρ' p' = (ρ ≤≤≤s≤≤≤ m) p')"
    unfolding lt_def by auto
  then obtain p where p_p1: "ρ' p ⊂ (ρ ≤≤≤s≤≤≤ m) p" and
    p_p2: "∀p'. s p' = s p ⟶ ρ' p' ⊆ (ρ ≤≤≤s≤≤≤ m) p'" and
    p_p3: "∀p'. s p' < s p ⟶ ρ' p' = (ρ ≤≤≤s≤≤≤ m) p'"
    by auto
  define ρ'' where "ρ'' == λp. if s p ≤ m then ρ' p else UNIV"

  have "s p ≤ m"
    using p_p1 by auto
  then have "ρ'' p ⊂ ρ p"
    unfolding ρ''_def using p_p1 by auto
  moreover
  have "∀p'. s p' = s p ⟶ ρ'' p' ⊆ ρ p'"
    using p_p2
    by (metis ρ''_def calculation pred_val_lte_stratum.simps top.extremum_strict)
  moreover
  have "∀p'. s p' < s p ⟶ ρ'' p' = ρ p'"
    using ρ''_def p_p3 calculation(1) by force
  ultimately
  have "(ρ'' ⊏s⊏ ρ)"
    by (metis lt_def)
  moreover
  have "ρ'' ⊨dl (dl ≤≤s≤≤ n)"
    unfolding solves_program_def
  proof
    fix c
    assume c_in_dl_n: "c ∈ (dl ≤≤s≤≤ n)"
    then obtain p ids rhs where c_def: "c = Cls p ids rhs"
      by (cases c) auto

    have "ρ'' ⊨cls Cls p ids rhs"
      unfolding solves_cls_def
    proof
      fix σ
      show "⟦Cls p ids rhs⟧cls ρ'' σ"
      proof (cases "s p ≤ m")
        case True
        then have "c ∈ (dl ≤≤s≤≤ m)"
          using c_in_dl_n c_def by auto
        then have "⟦Cls p ids rhs⟧cls ρ' σ"
          using ρ'_p1 c_def solves_cls_def solves_program_def by blast
        
        show ?thesis
          unfolding meaning_cls.simps
        proof
          assume "⟦rhs⟧rhs ρ'' σ"
          have "⟦rhs⟧rhs ρ' σ"
            unfolding meaning_rhs.simps
          proof
            fix rh
            assume "rh ∈ set rhs"
            then have "⟦rh⟧rh ρ'' σ"
              using ‹⟦rhs⟧rhs ρ'' σ› by force
            then show "⟦rh⟧rh ρ' σ"
            proof (cases rh)
              case (Eql a a')
              then show ?thesis
                using ‹⟦rh⟧rh ρ'' σ› by auto
            next
              case (Neql a a')
              then show ?thesis
                using ‹⟦rh⟧rh ρ'' σ› by auto
            next
              case (PosLit p ids)
              then show ?thesis
                using ‹⟦rh⟧rh ρ'' σ› ‹c ∈ (dl ≤≤s≤≤ m)› ‹rh ∈ set rhs› ρ''_def assms(3) c_def 
                  pos_rhs_stratum_leq_clause_stratum by fastforce
            next
              case (NegLit p ids)
              then show ?thesis
                using ‹⟦rh⟧rh ρ'' σ› ‹c ∈ (dl ≤≤s≤≤ m)› ‹rh ∈ set rhs› ρ''_def c_def 
                  neg_rhs_stratum_less_clause_stratum s_dl_m by fastforce
            qed
          qed
          then have "⟦(p, ids)⟧lh ρ' σ"
            using ‹⟦Cls p ids rhs⟧cls ρ' σ› by force
          then show  "⟦(p, ids)⟧lh ρ'' σ"
            using ρ''_def by force
        qed
      next
        case False
        then show ?thesis
          by (simp add: ρ''_def)
      qed
    qed
    then show "ρ'' ⊨cls c"
      using c_def by blast
  qed
  ultimately
  have "¬ρ ⊨min (dl ≤≤s≤≤ n) s"
    unfolding minimal_solution_def by auto
  then have "¬ρ ⊨lst (dl ≤≤s≤≤ n) s" 
    using least_iff_minimal strat_wf_n finite_below_finite assms by metis
  then show "False"
    using assms by auto
qed

lemma downward_least_solution_same_stratum:
  assumes "finite dl"
  assumes "strat_wf s dl"
  assumes "ρ ⊨lst dl s"
  shows "(ρ ≤≤≤s≤≤≤ m) ⊨lst (dl ≤≤s≤≤ m) s"
proof (cases "m < max_stratum s dl")
  case True
  have "(dl ≤≤s≤≤ max_stratum s dl) = dl"
    using assms(1) finite_max_stratum by blast
  with True show ?thesis
    using downward_least_solution[of dl m "max_stratum s dl" s ρ]
      assms by auto
next
  case False
  then have "max_stratum s dl ≤ m"
    by auto
  moreover
  have "(dl ≤≤s≤≤ m) = dl"
    using assms(1) calculation finite_above_max_stratum by blast
  then
  show ?thesis
    using assms below_subset downward_least_solution least_solution_def lessI less_imp_le_nat 
      solves_leq[of _ dl s _ m] solves_program_mono[of _ dl ρ ] by metis
qed


subsection ‹Negation›

definition agree_var_val :: "'x set ⇒ ('x, 'c) var_val ⇒ ('x, 'c) var_val ⇒ bool " where
  "agree_var_val xs σ σ' ⟷ (∀x ∈ xs. σ x = σ' x)"

fun vars_ids :: "('a, 'b) id list ⇒ 'a set" where
  "vars_ids ids = ⋃(vars_id ` set ids)"

fun vars_lh :: "('p,'x,'c) lh ⇒ 'x set" where
  "vars_lh (p,ids) = vars_ids ids"

definition lh_consequence :: "('p, 'c) pred_val ⇒ ('p, 'x, 'c) clause ⇒ ('p, 'x, 'c) lh ⇒ bool" 
  where
  "lh_consequence ρ c lh ⟷ (∃σ'. ((the_lh c) ⋅vlh σ') = lh ∧ ⟦the_rhs c⟧rhs ρ σ')"

lemma meaning_rh_iff_meaning_rh_pred_val_lte_stratum:
  assumes "c ∈ (dl ≤≤s≤≤ s p)"
  assumes "strat_wf s dl"
  assumes "rh ∈ set (the_rhs c)"
  shows "⟦rh⟧rh ρ σ' ⟷ ⟦rh⟧rh (ρ ≤≤≤s≤≤≤ s p) σ'"
proof (cases rh)
  case (Eql a a')
  then show ?thesis 
    by auto
next
  case (Neql a a')
  then show ?thesis 
    by auto
next
  case (PosLit p' ids)
  show ?thesis
  proof
    assume "⟦rh⟧rh ρ σ'"
    then show "⟦rh⟧rh (ρ ≤≤≤s≤≤≤ s p) σ'"
      using PosLit assms pos_rhs_stratum_leq_clause_stratum by fastforce
  next
    assume "⟦rh⟧rh (ρ ≤≤≤s≤≤≤ s p) σ'"
    then show "⟦rh⟧rh ρ σ'"
      by (metis PosLit equals0D meaning_rh.simps(3) pred_val_lte_stratum.simps)
  qed
next
  case (NegLit p' ids)
  show ?thesis
  proof
    assume "⟦rh⟧rh ρ σ'"
    then show "⟦rh⟧rh (ρ ≤≤≤s≤≤≤ s p) σ'"
      using NegLit assms by fastforce
  next
    assume "⟦rh⟧rh (ρ ≤≤≤s≤≤≤ s p) σ'"
    then show "⟦rh⟧rh ρ σ'"
      using NegLit assms(1) assms(2) assms(3) neg_rhs_stratum_less_clause_stratum by fastforce
  qed
qed

lemma meaning_rhs_iff_meaning_rhs_pred_val_lte_stratum:
  assumes "c ∈ (dl ≤≤s≤≤ s p)"
  assumes "strat_wf s dl"
  shows "⟦the_rhs c⟧rhs ρ σ' ⟷ ⟦the_rhs c⟧rhs (ρ ≤≤≤s≤≤≤ s p) σ'"
  by (meson assms(1) assms(2) meaning_rh_iff_meaning_rh_pred_val_lte_stratum meaning_rhs.simps)

lemma meaning_rhs_if_meaning_rhs_with_removed_top_strata:
  assumes "⟦rhs⟧rhs (ρ'(p := ρ' p - {⟦ids⟧ids σ})) σ'"
  assumes "strat_wf s dl"
  assumes c_dl': "Cls p' ids' rhs ∈ (dl ≤≤s≤≤ s p)"
  shows "⟦rhs⟧rhs ρ' σ'"
proof -
  have "∀rh' ∈ set rhs. rnk s rh' ≤ s p'"
    using assms c_dl' in_mono strat_wf_cls.simps strat_wf_def by fastforce

  show ?thesis
    unfolding meaning_rhs.simps
  proof
    fix rh
    assume "rh ∈ set rhs"
    show "⟦rh⟧rh ρ' σ'"
    proof (cases rh)
      case (Eql a a')
      then show ?thesis
        using ‹rh ∈ set rhs› assms by auto
    next
      case (Neql a a')
      then show ?thesis
        using ‹rh ∈ set rhs› assms by auto
    next
      case (PosLit p'' ids'')
      then show ?thesis
        by (metis Diff_empty Diff_insert0 ‹rh ∈ set rhs› assms fun_upd_other fun_upd_same insertCI 
            insert_Diff meaning_rh.simps(3) meaning_rhs.elims(2))
    next
      case (NegLit p'' ids'')
      have "p'' ≠ p"
        using NegLit One_nat_def ‹∀rh'∈set rhs. rnk s rh' ≤ s p'› ‹rh ∈ set rhs› c_dl' by fastforce
      then show ?thesis
        using NegLit  ‹rh ∈ set rhs› assms by auto
    qed
  qed
qed

lemma meaning_PosLit_least':
  assumes "finite dl"
  assumes "ρ ⊨lst dl s"
  assumes "strat_wf s dl"
  assumes "⟦+ p ids⟧rh ρ σ"
  shows "∃c ∈ dl. lh_consequence ρ c ((p,ids) ⋅vlh σ)"
proof (rule ccontr)
  assume "¬(∃c ∈ dl. lh_consequence ρ c ((p,ids) ⋅vlh σ))"
  then have "¬(∃c ∈ dl. ∃σ'. ((the_lh c) ⋅vlh σ') = ((p,ids) ⋅vlh σ) ∧ (⟦the_rhs c⟧rhs ρ σ'))"
    unfolding lh_consequence_def by auto
  then have a: "∀c ∈ dl. ∀σ'. ((the_lh c) ⋅vlh σ') = ((p,ids) ⋅vlh σ) ⟶ ¬(⟦the_rhs c⟧rhs ρ σ')"
    by metis

  define ρ' where "ρ' = (ρ ≤≤≤s≤≤≤ s p)"
  define dl' where "dl' = (dl ≤≤s≤≤ s p)"

  have ρ'_least: "ρ' ⊨lst dl' s"
    using downward_solves[of ρ dl s] assms downward_least_solution_same_stratum 
    unfolding ρ'_def dl'_def by blast
  moreover
  have no_match: "∀c ∈ dl'. ∀σ'. ((the_lh c) ⋅vlh σ') = ((p,ids) ⋅vlh σ) ⟶ ¬(⟦the_rhs c⟧rhs ρ' σ')"
    using a
    unfolding dl'_def ρ'_def
    by (meson assms(3) below_subset meaning_rhs_iff_meaning_rhs_pred_val_lte_stratum in_mono)

  define ρ'' where "ρ'' = ρ'(p := ρ' p - {⟦ids⟧ids σ})"
    

  have "ρ'' ⊨dl dl'"
    unfolding solves_program_def
  proof
    fix c
    assume c_dl': "c ∈ dl'"
    obtain p' ids' rhs' where c_split: "c = Cls p' ids' rhs'"
      by (cases c)
    show "ρ'' ⊨cls c"
      unfolding solves_cls_def
    proof
      fix σ'
      have "⟦Cls p' ids' rhs'⟧cls ρ'' σ'"
        unfolding meaning_cls.simps
      proof
        assume "⟦rhs'⟧rhs ρ'' σ'"
        then have rhs'_true: "⟦rhs'⟧rhs ρ' σ'" 
          using meaning_rhs_if_meaning_rhs_with_removed_top_strata[of rhs' ρ' p ids σ σ']
            ρ''_def assms(3) c_dl' c_split dl'_def using ρ''_def by force 
        have "⟦(p',ids')⟧lh ρ' σ'"
          by (metis rhs'_true c_split c_dl' ρ'_least clause.inject least_solution_def 
              meaning_cls.elims(2) solves_cls_def solves_program_def)
        moreover
        have "((p', ids') ⋅vlh σ') ≠ ((p, ids) ⋅vlh σ)"
          using no_match rhs'_true c_split c_dl' by fastforce
        ultimately
        show "⟦(p', ids')⟧lh ρ'' σ'"
          using  ρ''_def eval_ids_is_substv_ids by auto
      qed
      then show "⟦c⟧cls ρ'' σ'"
        unfolding c_split by auto
    qed
  qed
  moreover
  have "ρ'' ⊏s⊏ ρ'"
  proof -
    have "ρ'' p ⊂ ρ' p"
      unfolding ρ'_def
      using DiffD2 ‹⟦+ p ids⟧rh ρ σ› ρ''_def ρ'_def by auto
    moreover
    have "∀p'. s p' = s p ⟶ ρ'' p' ⊆ ρ' p'"
      unfolding ρ'_def
      by (simp add: ρ''_def ρ'_def)
    moreover
    have "∀p'. s p' < s p ⟶ ρ'' p' = ρ' p'"
      using ρ''_def by force
    ultimately
    show "ρ'' ⊏s⊏ ρ'"
      unfolding lt_def by auto
  qed
  ultimately
  show "False"
    by (metis assms(1,3) dl'_def finite_below_finite least_iff_minimal minimal_solution_def 
        strat_wf_lte_if_strat_wf)
qed

lemma meaning_lh_least':
  assumes "finite dl"
  assumes "ρ ⊨lst dl s"
  assumes "strat_wf s dl"
  assumes "⟦(p, ids)⟧lh ρ σ"
  shows "∃c ∈ dl. lh_consequence ρ c ((p,ids) ⋅vlh σ)"
  using assms meaning_PosLit_least' by fastforce

lemma meaning_lh_least:
  assumes "finite dl"
  assumes "ρ ⊨lst dl s"
  assumes "strat_wf s dl"
  shows "⟦(p, ids)⟧lh ρ σ ⟷ (∃c ∈ dl. lh_consequence ρ c ((p,ids) ⋅vlh σ))"
proof
  assume "⟦(p, ids)⟧lh ρ σ"
  then show "∃c ∈ dl. lh_consequence ρ c ((p,ids) ⋅vlh σ)"
    by (meson assms meaning_lh_least')
next
  assume "∃c ∈ dl. lh_consequence ρ c ((p,ids) ⋅vlh σ)"
  then show "⟦(p, ids)⟧lh ρ σ"
    unfolding lh_consequence_def
    using assms(2) eval_ids_is_substv_ids least_solution_def meaning_cls.simps meaning_lh.simps 
      solves_cls_def solves_program_def clause.exhaust clause.sel(3) prod.inject substv_lh.simps 
      the_lh.simps by metis
qed

lemma meaning_PosLit_least:
  assumes "finite dl"
  assumes "ρ ⊨lst dl s"
  assumes "strat_wf s dl"
  shows "⟦+ p ids⟧rh ρ σ ⟷ (∃c ∈ dl. lh_consequence ρ c ((p,ids) ⋅vlh σ))"
proof
  assume "⟦+ p ids⟧rh ρ σ"
  then show "∃c ∈ dl. lh_consequence ρ c ((p,ids) ⋅vlh σ)"
    by (meson assms(1,2,3) meaning_PosLit_least')
next
  assume "∃c ∈ dl. lh_consequence ρ c ((p,ids) ⋅vlh σ)"
  then show "⟦+ p ids⟧rh ρ σ"
    unfolding lh_consequence_def
    using assms(2) eval_ids_is_substv_ids least_solution_def meaning_cls.simps meaning_lh.simps 
      solves_cls_def solves_program_def clause.exhaust clause.sel(3) meaning_rh.simps(3) prod.inject 
      substv_lh.simps the_lh.simps by metis
qed

lemma meaning_NegLit_least:
  assumes "finite dl"
  assumes "ρ ⊨lst dl s"
  assumes "strat_wf s dl"
  shows "⟦¬ p ids⟧rh ρ σ ⟷ (¬(∃c ∈ dl. lh_consequence ρ c ((p,ids) ⋅vlh σ)))"
  by (metis assms(1,2,3) meaning_PosLit_least meaning_rh.simps(3) meaning_rh.simps(4))

lemma solves_PosLit_least:
  assumes "finite dl"
  assumes "ρ ⊨lst dl s"
  assumes "strat_wf s dl"
  assumes "∀a ∈ set ids. is_Cst a"
  shows "ρ ⊨rh (+ p ids) ⟷ (∃c ∈ dl. lh_consequence ρ c (p,ids))"
proof -
  have "∀σ. ((p, ids) ⋅vlh σ) = (p, ids)"
    using assms(4) by (induction ids) (auto simp add: is_Cst_def)
  then show ?thesis
    by (metis assms(1,2,3) meaning_PosLit_least solves_rh.simps)
qed

lemma solves_lh_least:
  assumes "finite dl"
  assumes "ρ ⊨lst dl s"
  assumes "strat_wf s dl"
  assumes "∀a ∈ set ids. is_Cst a"
  shows "ρ ⊨lh (p, ids) ⟷ (∃c ∈ dl. lh_consequence ρ c (p,ids))"
proof -
  have "∀σ. ((p, ids) ⋅vlh σ) = (p, ids)"
    using assms(4) by (induction ids) (auto simp add: is_Cst_def)
  then show ?thesis
    by (metis assms(1,2,3) meaning_lh_least solves_lh.simps)
qed

lemma solves_NegLit_least:
  assumes "finite dl"
  assumes "ρ ⊨lst dl s"
  assumes "strat_wf s dl"
  assumes "∀a ∈ set ids. is_Cst a"
  shows "ρ ⊨rh (¬ p ids) ⟷ ¬(∃c ∈ dl. lh_consequence ρ c (p,ids))"
proof -
  have "∀σ. ((p, ids) ⋅vlh σ) = (p, ids)"
    using assms(4) by (induction ids) (auto simp add: is_Cst_def)
  then show ?thesis
    by (metis assms(1,2,3) meaning_NegLit_least solves_rh.simps)
qed

end