Theory FixedPoint

section ‹(Co)Inductive Predicates›

text ‹This subsection corresponds to Section 4 of the paper~\<^cite>‹"UnboundedSL"›.›

theory FixedPoint
  imports Distributivity Combinability
begin

type_synonym ('d, 'c, 'a) chain = "nat ⇒ ('d, 'c, 'a) interp"

context logic
begin

subsection Definitions

definition smaller_interp :: "('d, 'c, 'a) interp ⇒ ('d, 'c, 'a) interp ⇒ bool" where
  "smaller_interp Δ Δ' ⟷ (∀s. Δ s ⊆ Δ' s)"

lemma smaller_interpI:
  assumes "⋀s x. x ∈ Δ s ⟹ x ∈ Δ' s"
  shows "smaller_interp Δ Δ'"
  by (simp add: assms smaller_interp_def subsetI)

definition indep_interp where
  "indep_interp A ⟷ (∀x s Δ Δ'. x, s, Δ ⊨ A ⟷ x, s, Δ' ⊨ A)"

fun applies_eq :: "('a, 'b, 'c, 'd) assertion ⇒ ('d, 'c, 'a) interp ⇒ ('d, 'c, 'a) interp" where
  "applies_eq A Δ s = { a |a. a, s, Δ ⊨ A }"

definition monotonic :: "(('d, 'c, 'a) interp ⇒ ('d, 'c, 'a) interp) ⇒ bool" where
  "monotonic f ⟷ (∀Δ Δ'. smaller_interp Δ Δ' ⟶ smaller_interp (f Δ) (f Δ'))"

lemma monotonicI:
  assumes "⋀Δ Δ'. smaller_interp Δ Δ' ⟹ smaller_interp (f Δ) (f Δ')"
  shows "monotonic f"
  by (simp add: assms monotonic_def)

definition non_increasing :: "(('d, 'c, 'a) interp ⇒ ('d, 'c, 'a) interp) ⇒ bool" where
  "non_increasing f ⟷ (∀Δ Δ'. smaller_interp Δ Δ' ⟶ smaller_interp (f Δ') (f Δ))"

lemma non_increasingI:
  assumes "⋀Δ Δ'. smaller_interp Δ Δ' ⟹ smaller_interp (f Δ') (f Δ)"
  shows "non_increasing f"
  by (simp add: assms non_increasing_def)


lemma smaller_interp_refl:
  "smaller_interp Δ Δ"
  by (simp add: smaller_interp_def)


lemma smaller_interp_applies_cons:
  assumes "smaller_interp (applies_eq A Δ) (applies_eq A Δ')"
      and "a, s, Δ ⊨ A"
    shows "a, s, Δ' ⊨ A"
proof -
  have "a ∈ applies_eq A Δ s"
    using assms(2) by force
  then have "a ∈ applies_eq A Δ' s"
    by (metis assms(1) in_mono smaller_interp_def)
  then show ?thesis by auto
qed

definition empty_interp where
  "empty_interp s = {}"

definition full_interp :: "('d, 'c, 'a) interp" where
  "full_interp s = UNIV"

lemma smaller_interp_trans:
  assumes "smaller_interp a b"
      and "smaller_interp b c"
    shows "smaller_interp a c"
  by (metis assms(1) assms(2) dual_order.trans smaller_interp_def)

lemma smaller_empty:
  "smaller_interp empty_interp x"
  by (simp add: empty_interp_def smaller_interp_def)

text ‹The definition of set-closure properties corresponds to Definition 8 of the paper~\<^cite>‹"UnboundedSL"›.›

definition set_closure_property :: "('a ⇒ 'a ⇒ 'a set) ⇒ ('d, 'c, 'a) interp ⇒ bool" where
  "set_closure_property S Δ ⟷ (∀a b s. a ∈ Δ s ∧ b ∈ Δ s ⟶ S a b ⊆ Δ s)"

lemma set_closure_propertyI:
  assumes "⋀a b s. a ∈ Δ s ∧ b ∈ Δ s ⟹ S a b ⊆ Δ s"
  shows "set_closure_property S Δ"
  by (simp add: assms set_closure_property_def)

lemma set_closure_property_instantiate:
  assumes "set_closure_property S Δ"
      and "a ∈ Δ s"
      and "b ∈ Δ s"
      and "x ∈ S a b"
    shows "x ∈ Δ s"
  using assms subsetD set_closure_property_def by metis





























subsection ‹Everything preserves monotonicity›


lemma indep_implies_non_increasing:
  assumes "indep_interp A"
  shows "non_increasing (applies_eq A)"
  by (metis (no_types, lifting) applies_eq.simps assms indep_interp_def smaller_interp_def mem_Collect_eq non_increasingI subsetI)

subsubsection Monotonicity

lemma mono_instantiate:
  assumes "monotonic (applies_eq A)"
      and "x ∈ applies_eq A Δ s"
      and "smaller_interp Δ Δ'"
    shows "x ∈ applies_eq A Δ' s"
  using assms(1) assms(2) assms(3) monotonic_def smaller_interp_applies_cons by fastforce

lemma mono_star:
  assumes "monotonic (applies_eq A)"
      and "monotonic (applies_eq B)"
    shows "monotonic (applies_eq (Star A B))"
proof (rule monotonicI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Star A B) Δ) (applies_eq (Star A B) Δ')"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Star A B) Δ s"
    then obtain a b where "Some x = a ⊕ b" "a ∈ applies_eq A Δ s" "b ∈ applies_eq B Δ s"
      by auto
    then have "a ∈ applies_eq A Δ' s ∧ b ∈ applies_eq B Δ' s"
      by (meson asm0 assms(1) assms(2) mono_instantiate)
    then show "x ∈ applies_eq (Star A B) Δ' s"
      using ‹Some x = a ⊕ b› by force
  qed
qed


lemma mono_wand:
  assumes "non_increasing (applies_eq A)"
      and "monotonic (applies_eq B)"
    shows "monotonic (applies_eq (Wand A B))"
proof (rule monotonicI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Wand A B) Δ) (applies_eq (Wand A B) Δ')"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Wand A B) Δ s"
    have "x, s, Δ' ⊨ Wand A B"
    proof (rule sat_wand)
      fix a b
      assume asm2: "a, s, Δ' ⊨ A ∧ Some b = x ⊕ a"
      then have "a, s, Δ ⊨ A"
        by (meson asm0 assms(1) non_increasing_def smaller_interp_applies_cons)
      then have "b, s, Δ ⊨ B"
        using asm1 asm2 by auto
      then show "b, s, Δ' ⊨ B"
        by (meson asm0 assms(2) monotonic_def smaller_interp_applies_cons)
    qed
    then show "x ∈ applies_eq (Wand A B) Δ' s"
      by simp
  qed
qed



lemma mono_and:
  assumes "monotonic (applies_eq A)"
      and "monotonic (applies_eq B)"
    shows "monotonic (applies_eq (And A B))"
proof (rule monotonicI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (And A B) Δ) (applies_eq (And A B) Δ')"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (And A B) Δ s"
    then show "x ∈ applies_eq (And A B) Δ' s"
      using asm0 assms(1) assms(2) monotonic_def logic_axioms mem_Collect_eq sat.simps(8) smaller_interp_applies_cons by fastforce
  qed
qed

lemma mono_or:
  assumes "monotonic (applies_eq A)"
      and "monotonic (applies_eq B)"
    shows "monotonic (applies_eq (Or A B))"
proof (rule monotonicI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Or A B) Δ) (applies_eq (Or A B) Δ')"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Or A B) Δ s"
    then show "x ∈ applies_eq (Or A B) Δ' s"
      using asm0 assms(1) assms(2) monotonic_def logic_axioms mem_Collect_eq sat.simps(8) smaller_interp_applies_cons by fastforce
  qed
qed

lemma mono_sem:
  "monotonic (applies_eq (Sem B))"
  using monotonic_def smaller_interp_def by fastforce

lemma mono_interp:
  "monotonic (applies_eq Pred)"
proof (rule monotonicI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq Pred Δ) (applies_eq Pred Δ')"
  proof (rule smaller_interpI)
    fix s x assume "x ∈ applies_eq Pred Δ s"
    then show "x ∈ applies_eq Pred Δ' s"
      by (metis (mono_tags, lifting) ‹smaller_interp Δ Δ'› applies_eq.simps in_mono mem_Collect_eq sat.simps(10) smaller_interp_def)
  qed
qed


lemma mono_mult:
  assumes "monotonic (applies_eq A)"
  shows "monotonic (applies_eq (Mult π A))"
proof (rule monotonicI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Mult π A) Δ) (applies_eq (Mult π A) Δ')"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Mult π A) Δ s"
    then show "x ∈ applies_eq (Mult π A) Δ' s"
      using asm0 assms monotonic_def smaller_interp_applies_cons by fastforce
  qed
qed

lemma mono_wild:
  assumes "monotonic (applies_eq A)"
  shows "monotonic (applies_eq (Wildcard A))"
proof (rule monotonicI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Wildcard A) Δ) (applies_eq (Wildcard A) Δ')"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Wildcard A) Δ s"
    then show "x ∈ applies_eq (Wildcard A) Δ' s"
      using asm0 assms monotonic_def smaller_interp_applies_cons by fastforce
  qed
qed


lemma mono_imp:
  assumes "non_increasing (applies_eq A)"
      and "monotonic (applies_eq B)"
    shows "monotonic (applies_eq (Imp A B))"
proof (rule monotonicI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Imp A B) Δ) (applies_eq (Imp A B) Δ')"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Imp A B) Δ s"
    have "x, s, Δ' ⊨ Imp A B"
    proof (cases "x, s, Δ' ⊨ A")
      case True
      then have "x, s, Δ ⊨ A"
        by (meson asm0 assms(1) non_increasing_def smaller_interp_applies_cons)
      then have "x, s, Δ ⊨ B"
        using asm1 by auto
      then show ?thesis
        by (metis asm0 assms(2) monotonic_def sat.simps(5) smaller_interp_applies_cons)
    next
      case False
      then show ?thesis by simp
    qed
    then show "x ∈ applies_eq (Imp A B) Δ' s"
      by simp
  qed
qed

lemma mono_bounded:
  assumes "monotonic (applies_eq A)"
  shows "monotonic (applies_eq (Bounded A))"
proof (rule monotonicI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Bounded A) Δ) (applies_eq (Bounded A) Δ')"
  proof (rule smaller_interpI)
    fix s x assume "x ∈ applies_eq (Bounded A) Δ s"
    then show "x ∈ applies_eq (Bounded A) Δ' s"
      using asm assms monotonic_def smaller_interp_applies_cons by fastforce
  qed
qed

lemma mono_exists:
  assumes "monotonic (applies_eq A)"
    shows "monotonic (applies_eq (Exists v A))"
proof (rule monotonicI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Exists v A) Δ) (applies_eq (Exists v A) Δ')"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Exists v A) Δ s"
    then show "x ∈ applies_eq (Exists v A) Δ' s"
      using asm0 assms monotonic_def smaller_interp_applies_cons by fastforce
  qed
qed


lemma mono_forall:
  assumes "monotonic (applies_eq A)"
    shows "monotonic (applies_eq (Forall v A))"
proof (rule monotonicI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Forall v A) Δ) (applies_eq (Forall v A) Δ')"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Forall v A) Δ s"
    then show "x ∈ applies_eq (Forall v A) Δ' s"
      using asm0 assms monotonic_def smaller_interp_applies_cons by fastforce
  qed
qed














subsubsection ‹Non-increasing›

lemma non_increasing_instantiate:
  assumes "non_increasing (applies_eq A)"
      and "x ∈ applies_eq A Δ' s"
      and "smaller_interp Δ Δ'"
    shows "x ∈ applies_eq A Δ s"
  using assms(1) assms(2) assms(3) non_increasing_def smaller_interp_applies_cons by fastforce

lemma non_inc_star:
  assumes "non_increasing (applies_eq A)"
      and "non_increasing (applies_eq B)"
    shows "non_increasing (applies_eq (Star A B))"
proof (rule non_increasingI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Star A B) Δ') (applies_eq (Star A B) Δ)"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Star A B) Δ' s"
    then obtain a b where "Some x = a ⊕ b" "a ∈ applies_eq A Δ' s" "b ∈ applies_eq B Δ' s"
      by auto
    then have "a ∈ applies_eq A Δ s ∧ b ∈ applies_eq B Δ s"
      by (meson asm0 assms(1) assms(2) non_increasing_instantiate)
    then show "x ∈ applies_eq (Star A B) Δ s"
      using ‹Some x = a ⊕ b› by force
  qed
qed


lemma non_increasing_wand:
  assumes "monotonic (applies_eq A)"
      and "non_increasing (applies_eq B)"
    shows "non_increasing (applies_eq (Wand A B))"
proof (rule non_increasingI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Wand A B) Δ') (applies_eq (Wand A B) Δ)"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Wand A B) Δ' s"
    have "x, s, Δ ⊨ Wand A B"
    proof (rule sat_wand)
      fix a b
      assume asm2: "a, s, Δ ⊨ A ∧ Some b = x ⊕ a"
      then have "a, s, Δ' ⊨ A"
        by (meson asm0 assms(1) monotonic_def smaller_interp_applies_cons)
      then have "b, s, Δ' ⊨ B"
        using asm1 asm2 by auto
      then show "b, s, Δ ⊨ B"
        by (meson asm0 assms(2) non_increasing_def smaller_interp_applies_cons)
    qed
    then show "x ∈ applies_eq (Wand A B) Δ s"
      by simp
  qed
qed



lemma non_increasing_and:
  assumes "non_increasing (applies_eq A)"
      and "non_increasing (applies_eq B)"
    shows "non_increasing (applies_eq (And A B))"
proof (rule non_increasingI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ' Δ"
  show "smaller_interp (applies_eq (And A B) Δ) (applies_eq (And A B) Δ')"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (And A B) Δ s"
    then show "x ∈ applies_eq (And A B) Δ' s"
      using asm0 assms(1) assms(2) non_increasing_def logic_axioms mem_Collect_eq sat.simps(8) smaller_interp_applies_cons by fastforce
  qed
qed

lemma non_increasing_or:
  assumes "non_increasing (applies_eq A)"
      and "non_increasing (applies_eq B)"
    shows "non_increasing (applies_eq (Or A B))"
proof (rule non_increasingI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Or A B) Δ') (applies_eq (Or A B) Δ)"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Or A B) Δ' s"
    then show "x ∈ applies_eq (Or A B) Δ s"
      using asm0 assms(1) assms(2) non_increasing_def logic_axioms mem_Collect_eq sat.simps(8) smaller_interp_applies_cons by fastforce
  qed
qed

lemma non_increasing_sem:
  "non_increasing (applies_eq (Sem B))"
  using non_increasing_def smaller_interp_def by fastforce


lemma non_increasing_mult:
  assumes "non_increasing (applies_eq A)"
  shows "non_increasing (applies_eq (Mult π A))"
proof (rule non_increasingI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Mult π A) Δ') (applies_eq (Mult π A) Δ)"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Mult π A) Δ' s"
    then show "x ∈ applies_eq (Mult π A) Δ s"
      using asm0 assms non_increasing_def smaller_interp_applies_cons by fastforce
  qed
qed

lemma non_increasing_wild:
  assumes "non_increasing (applies_eq A)"
  shows "non_increasing (applies_eq (Wildcard A))"
proof (rule non_increasingI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Wildcard A) Δ') (applies_eq (Wildcard A) Δ)"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Wildcard A) Δ' s"
    then show "x ∈ applies_eq (Wildcard A) Δ s"
      using asm0 assms non_increasing_def smaller_interp_applies_cons by fastforce
  qed
qed


lemma non_increasing_imp:
  assumes "monotonic (applies_eq A)"
      and "non_increasing (applies_eq B)"
    shows "non_increasing (applies_eq (Imp A B))"
proof (rule non_increasingI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ Δ'"
  show "smaller_interp (applies_eq (Imp A B) Δ') (applies_eq (Imp A B) Δ)"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Imp A B) Δ' s"
    have "x, s, Δ ⊨ Imp A B"
    proof (cases "x, s, Δ ⊨ A")
      case True
      then have "x, s, Δ' ⊨ A"
        by (meson asm0 assms(1) monotonic_def smaller_interp_applies_cons)
      then have "x, s, Δ' ⊨ B"
        using asm1 by auto
      then show ?thesis
        by (metis asm0 assms(2) non_increasing_def sat.simps(5) smaller_interp_applies_cons)
    next
      case False
      then show ?thesis by simp
    qed
    then show "x ∈ applies_eq (Imp A B) Δ s"
      by simp
  qed
qed


lemma non_increasing_bounded:
  assumes "non_increasing (applies_eq A)"
  shows "non_increasing (applies_eq (Bounded A))"
proof (rule non_increasingI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm: "smaller_interp Δ' Δ"
  show "smaller_interp (applies_eq (Bounded A) Δ) (applies_eq (Bounded A) Δ')"
  proof (rule smaller_interpI)
    fix s x assume "x ∈ applies_eq (Bounded A) Δ s"
    then show "x ∈ applies_eq (Bounded A) Δ' s"
      using asm assms non_increasing_def smaller_interp_applies_cons by fastforce
  qed
qed


lemma non_increasing_exists:
  assumes "non_increasing (applies_eq A)"
    shows "non_increasing (applies_eq (Exists v A))"
proof (rule non_increasingI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ' Δ"
  show "smaller_interp (applies_eq (Exists v A) Δ) (applies_eq (Exists v A) Δ')"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Exists v A) Δ s"
    then show "x ∈ applies_eq (Exists v A) Δ' s"
      using asm0 assms non_increasing_def smaller_interp_applies_cons by fastforce
  qed
qed


lemma non_increasing_forall:
  assumes "non_increasing (applies_eq A)"
    shows "non_increasing (applies_eq (Forall v A))"
proof (rule non_increasingI)
  fix Δ Δ' :: "('c, 'd, 'a) interp"
  assume asm0: "smaller_interp Δ' Δ"
  show "smaller_interp (applies_eq (Forall v A) Δ) (applies_eq (Forall v A) Δ')"
  proof (rule smaller_interpI)
    fix s x assume asm1: "x ∈ applies_eq (Forall v A) Δ s"
    then show "x ∈ applies_eq (Forall v A) Δ' s"
      using asm0 assms non_increasing_def smaller_interp_applies_cons by fastforce
  qed
qed













subsection ‹Tarski's fixed points›

subsubsection ‹Greatest Fixed Point›

definition D :: "(('d, 'c, 'a) interp ⇒ ('d, 'c, 'a) interp) ⇒ ('d, 'c, 'a) interp set" where
  "D f = { Δ |Δ. smaller_interp Δ (f Δ) }"

fun GFP :: "(('d, 'c, 'a) interp ⇒ ('d, 'c, 'a) interp) ⇒ ('d, 'c, 'a) interp" where
  "GFP f s = { σ |σ. ∃Δ ∈ D f. σ ∈ Δ s }"

lemma smaller_interp_D:
  assumes "x ∈ D f"
  shows "smaller_interp x (GFP f)"
  by (metis (mono_tags, lifting) CollectI GFP.elims assms smaller_interpI)

lemma GFP_lub:
  assumes "⋀x. x ∈ D f ⟹ smaller_interp x y"
  shows "smaller_interp (GFP f) y"
proof (rule smaller_interpI)
  fix s x
  assume "x ∈ GFP f s"
  then obtain Δ where "Δ ∈ D f" "x ∈ Δ s"
    by auto
  then show "x ∈ y s"
    by (metis assms in_mono smaller_interp_def)
qed

lemma smaller_interp_antisym:
  assumes "smaller_interp a b"
      and "smaller_interp b a"
    shows "a = b"
proof (rule ext)
  fix x show "a x = b x"
    by (metis assms(1) assms(2) set_eq_subset smaller_interp_def)
qed












subsubsection ‹Least Fixed Point›

definition DD :: "(('d, 'c, 'a) interp ⇒ ('d, 'c, 'a) interp) ⇒ ('d, 'c, 'a) interp set" where
  "DD f = { Δ |Δ. smaller_interp (f Δ) Δ }"

fun LFP :: "(('d, 'c, 'a) interp ⇒ ('d, 'c, 'a) interp) ⇒ ('d, 'c, 'a) interp" where
  "LFP f s = { σ |σ. ∀Δ ∈ DD f. σ ∈ Δ s }"

lemma smaller_interp_DD:
  assumes "x ∈ DD f"
  shows "smaller_interp (LFP f) x"
  using assms smaller_interp_def by fastforce


lemma LFP_glb:
  assumes "⋀x. x ∈ DD f ⟹ smaller_interp y x"
  shows "smaller_interp y (LFP f)"
proof (rule smaller_interpI)
  fix s x
  assume "x ∈ y s"
  then have "⋀Δ. Δ ∈ DD f ⟹ x ∈ Δ s"
    by (metis assms smaller_interp_def subsetD)
  then show "x ∈ LFP f s"
    by simp
qed







subsection ‹Combinability and (an assertion being) intuitionistic are set-closure properties›


subsubsection ‹Intuitionistic assertions›

definition sem_intui :: "('d, 'c, 'a) interp ⇒ bool" where
  "sem_intui Δ ⟷ (∀s σ σ'. σ' ≽ σ ∧ σ ∈ Δ s ⟶ σ' ∈ Δ s)"

lemma sem_intuiI:
  assumes "⋀s σ σ'. σ' ≽ σ ∧ σ ∈ Δ s ⟹ σ' ∈ Δ s"
  shows "sem_intui Δ"
  using assms sem_intui_def by blast

lemma instantiate_intui_applies:
  assumes "intuitionistic s Δ A"
      and "σ' ≽ σ"
      and "σ ∈ applies_eq A Δ s"
    shows "σ' ∈ applies_eq A Δ s"
  using assms(1) assms(2) assms(3) intuitionistic_def by fastforce

lemma sem_intui_intuitionistic:
  "sem_intui (applies_eq A Δ) ⟷ (∀s. intuitionistic s Δ A)" (is "?A ⟷ ?B")
proof
  show "?B ⟹ ?A"
  proof -
    assume ?B
    show ?A
    proof (rule sem_intuiI)
      fix s σ σ'
      assume "σ' ≽ σ ∧ σ ∈ applies_eq A Δ s"
      then show "σ' ∈ applies_eq A Δ s"
        using ‹∀s. intuitionistic s Δ A› instantiate_intui_applies by blast
    qed
  qed
  assume ?A
  show ?B
  proof
    fix s show "intuitionistic s Δ A"
    proof (rule intuitionisticI)
      fix a b
      assume "a ≽ b ∧ b, s, Δ ⊨ A"
      then have "b ∈ applies_eq A Δ s" by simp
      then show "a, s, Δ ⊨ A"
        by (metis CollectD ‹a ≽ b ∧ b, s, Δ ⊨ A› ‹sem_intui (applies_eq A Δ)› applies_eq.simps sem_intui_def)
    qed
  qed
qed



lemma intuitionistic_set_closure:
  "sem_intui = set_closure_property (λa b. { σ |σ. σ ≽ a})"
proof (rule ext)
  fix Δ :: "('c, 'd, 'a) interp"
  show "sem_intui Δ = set_closure_property (λa b. {σ |σ. σ ≽ a}) Δ" (is "?A ⟷ ?B")
  proof
    show "?A ⟹ ?B"
      by (metis (no_types, lifting) CollectD set_closure_propertyI sem_intui_def subsetI)
    assume ?B
    show ?A
    proof (rule sem_intuiI)
      fix s σ σ'
      assume "σ' ≽ σ ∧ σ ∈ Δ s"
      moreover have "(λa b. {σ |σ. σ ≽ a}) σ σ = {σ' |σ'. σ' ≽ σ}" by simp
      ultimately have "{σ' |σ'. σ' ≽ σ} ⊆ Δ s"
        by (metis ‹set_closure_property (λa b. {σ |σ. σ ≽ a}) Δ› set_closure_property_def)
      show "σ' ∈ Δ s"
        using ‹σ' ≽ σ ∧ σ ∈ Δ s› ‹{σ' |σ'. σ' ≽ σ} ⊆ Δ s› by fastforce
    qed
  qed
qed



subsubsection ‹Combinable assertions›

definition sem_combinable :: "('d, 'c, 'a) interp ⇒ bool" where
  "sem_combinable Δ ⟷ (∀s p q a b x. sadd p q = one ∧ a ∈ Δ s ∧ b ∈ Δ s ∧ Some x = p ⊙ a ⊕ q ⊙ b ⟶ x ∈ Δ s)"

lemma sem_combinableI:
  assumes "⋀s p q a b x. sadd p q = one ∧ a ∈ Δ s ∧ b ∈ Δ s ∧ Some x = p ⊙ a ⊕ q ⊙ b ⟹ x ∈ Δ s"
  shows "sem_combinable Δ"
  using assms sem_combinable_def by blast

lemma sem_combinableE:
  assumes "sem_combinable Δ"
      and "a ∈ Δ s"
      and "b ∈ Δ s"
      and "Some x = p ⊙ a ⊕ q ⊙ b"
      and "sadd p q = one"
    shows "x ∈ Δ s"
  using assms(1) assms(2) assms(3) assms(4) assms(5) sem_combinable_def[of Δ]
  by blast

lemma applies_eq_equiv:
  "x ∈ applies_eq A Δ s ⟷ x, s, Δ ⊨ A"
  by simp

lemma sem_combinable_appliesE:
  assumes "sem_combinable (applies_eq A Δ)"
      and "a, s, Δ ⊨ A"
      and "b, s, Δ ⊨ A"
      and "Some x = p ⊙ a ⊕ q ⊙ b"
      and "sadd p q = one"
    shows "x, s, Δ ⊨ A"
    using sem_combinableE[of "applies_eq A Δ" a s b x p q] assms by simp

lemma sem_combinable_equiv:
  "sem_combinable (applies_eq A Δ) ⟷ (combinable Δ A)" (is "?A ⟷ ?B")
proof                                       
  show "?B ⟹ ?A"
  proof -
    assume ?B
    show ?A
    proof (rule sem_combinableI)
      fix s p q a b x
      assume asm: "sadd p q = one ∧ a ∈ applies_eq A Δ s ∧ b ∈ applies_eq A Δ s ∧ Some x = p ⊙ a ⊕ q ⊙ b"
      then show "x ∈ applies_eq A Δ s"
        using ‹combinable Δ A› applies_eq_equiv combinable_instantiate_one by blast
    qed
  qed
  assume ?A
  show ?B
  proof -
    fix s show "combinable Δ A"
    proof (rule combinableI)
      fix a b p q x σ s
      assume "a, s, Δ ⊨ A ∧ b, s, Δ ⊨ A ∧ Some x = p ⊙ a ⊕ q ⊙ b ∧ sadd p q = one"
      then show "x, s, Δ ⊨ A"
        using ‹sem_combinable (applies_eq A Δ)› sem_combinable_appliesE by blast
    qed
  qed
qed


lemma combinable_set_closure:
  "sem_combinable = set_closure_property (λa b. { σ |σ p q. sadd p q = one ∧ Some σ = p ⊙ a ⊕ q ⊙ b})"
proof (rule ext)
  fix Δ :: "('c, 'd, 'a) interp"
  show "sem_combinable Δ = set_closure_property (λa b. { σ |σ p q. sadd p q = one ∧ Some σ = p ⊙ a ⊕ q ⊙ b}) Δ" (is "?A ⟷ ?B")
  proof
    show "?A ⟹ ?B"
    proof -
      assume ?A
      show ?B
      proof (rule set_closure_propertyI)
        fix a b s
        assume "a ∈ Δ s ∧ b ∈ Δ s"
        then show "{x. ∃σ p q. x = σ ∧ sadd p q = one ∧ Some σ = p ⊙ a ⊕ q ⊙ b} ⊆ Δ s"
          using ‹sem_combinable Δ› sem_combinableE by blast
      qed
    qed
    assume ?B
    show ?A
    proof (rule sem_combinableI)
      fix s p q a b x
      assume asm: "sadd p q = one ∧ a ∈ Δ s ∧ b ∈ Δ s ∧ Some x = p ⊙ a ⊕ q ⊙ b"

      then have "x ∈ (λa b. { σ |σ p q. sadd p q = one ∧ Some σ = p ⊙ a ⊕ q ⊙ b}) a b"
        by blast
      moreover have "(λa b. { σ |σ p q. sadd p q = one ∧ Some σ = p ⊙ a ⊕ q ⊙ b}) a b ⊆ Δ s"
        using ‹?B› set_closure_property_def[of "(λa b. { σ |σ p q. sadd p q = one ∧ Some σ = p ⊙ a ⊕ q ⊙ b})" Δ]
        asm by meson
      ultimately show "x ∈ Δ s" by blast
    qed
  qed
qed







subsection ‹Transfinite induction›


definition Inf :: "('d, 'c, 'a) interp set ⇒ ('d, 'c, 'a) interp" where
  "Inf S s = { σ |σ. ∀Δ ∈ S. σ ∈ Δ s}"


definition Sup :: "('d, 'c, 'a) interp set ⇒ ('d, 'c, 'a) interp" where
  "Sup S s = { σ |σ. ∃Δ ∈ S. σ ∈ Δ s}"

definition inf :: "('d, 'c, 'a) interp ⇒ ('d, 'c, 'a) interp ⇒ ('d, 'c, 'a) interp" where
  "inf Δ Δ' s = Δ s ∩ Δ' s"

definition less where
  "less a b ⟷ smaller_interp a b ∧ a ≠ b"

definition sup :: "('d, 'c, 'a) interp ⇒ ('d, 'c, 'a) interp ⇒ ('d, 'c, 'a) interp" where
  "sup Δ Δ' s = Δ s ∪ Δ' s"

lemma smaller_full:
  "smaller_interp x full_interp"
  by (simp add: full_interp_def smaller_interpI)


lemma inf_empty:
  "local.Inf {} = full_interp"
proof (rule ext)
  fix s :: "'c ⇒ 'd" show "local.Inf {} s = full_interp s"
    by (simp add: Inf_def full_interp_def)
qed

lemma sup_empty:
  "local.Sup {} = empty_interp"
proof (rule ext)
  fix s :: "'c ⇒ 'd" show "local.Sup {} s = empty_interp s"
    by (simp add: Sup_def empty_interp_def)
qed

lemma test_axiom_inf:
  assumes "⋀x. x ∈ A ⟹ smaller_interp z x"
  shows "smaller_interp z (local.Inf A)"
proof (rule smaller_interpI)
  fix s x
  assume "x ∈ z s"
  then have "⋀y. y ∈ A ⟹ x ∈ y s"
    by (metis assms in_mono smaller_interp_def)
  then show "x ∈ local.Inf A s"
    by (simp add: Inf_def)
qed


lemma test_axiom_sup:
  assumes "⋀x. x ∈ A ⟹ smaller_interp x z"
  shows "smaller_interp (local.Sup A) z"
proof (rule smaller_interpI)
  fix s x
  assume "x ∈ local.Sup A s"
  then obtain y where "y ∈ A" "x ∈ y s"
    using Sup_def[of A s] mem_Collect_eq[of x]
    by auto
  then show "x ∈ z s"
    by (metis assms smaller_interp_def subsetD)
qed

interpretation complete_lattice Inf Sup inf smaller_interp less sup empty_interp full_interp
  apply standard
  apply (metis less_def smaller_interp_antisym)
  apply (simp add: smaller_interp_refl)
  using smaller_interp_trans apply blast
  using smaller_interp_antisym apply blast
  apply (simp add: inf_def smaller_interp_def)
  apply (simp add: inf_def smaller_interp_def)
  apply (simp add: inf_def smaller_interp_def)
  apply (simp add: smaller_interpI sup_def)
  apply (simp add: smaller_interpI sup_def)
  apply (simp add: smaller_interp_def sup_def)
  apply (metis (mono_tags, lifting) CollectD Inf_def smaller_interpI)
  using test_axiom_inf apply blast
  apply (metis (mono_tags, lifting) CollectI Sup_def smaller_interpI)
  using test_axiom_sup apply auto[1]
  apply (simp add: inf_empty)
  by (simp add: sup_empty)

lemma mono_same:
  "monotonic f ⟷ order_class.mono f"
  by (metis (no_types, opaque_lifting) le_funE le_funI monotonic_def order_class.mono_def smaller_interp_def)

lemma "smaller_interp a b ⟷ a ≤ b"
  by (simp add: le_fun_def smaller_interp_def)



lemma set_closure_property_admissible:
  "ccpo.admissible Sup_class.Sup (≤) (set_closure_property S)"
proof (rule ccpo.admissibleI)
  fix A :: "('c, 'd, 'a) interp set"
  assume asm0: "Complete_Partial_Order.chain (≤) A"
  "A ≠ {}" "∀x∈A. set_closure_property S x"

  show "set_closure_property S (Sup_class.Sup A)"
  proof (rule set_closure_propertyI)
    fix a b s
    assume asm: "a ∈ Sup_class.Sup A s ∧ b ∈ Sup_class.Sup A s"
    then obtain Δa Δb where "Δa ∈ A" "Δb ∈ A" "a ∈ Δa s" "b ∈ Δb s"
      by auto
    then show "S a b ⊆ Sup_class.Sup A s"
    proof (cases "Δa s ⊆ Δb s")
      case True
      then have "S a b ⊆ Δb s"
        by (metis ‹Δb ∈ A› ‹a ∈ Δa s› ‹b ∈ Δb s› asm0(3) set_closure_property_def subsetD)
      then show ?thesis
        using ‹Δb ∈ A› by auto
    next
      case False
      then have "Δb s ⊆ Δa s"
        by (metis ‹Δa ∈ A› ‹Δb ∈ A› asm0(1) chainD le_funD)
      then have "S a b ⊆ Δa s"
        by (metis ‹Δa ∈ A› ‹a ∈ Δa s› ‹b ∈ Δb s› asm0(3) subsetD set_closure_property_def)
      then show ?thesis using ‹Δa ∈ A› by auto
    qed
  qed
qed


definition supp :: "('d, 'c, 'a) interp ⇒ bool" where
  "supp Δ ⟷ (∀a b s. a ∈ Δ s ∧ b ∈ Δ s ⟶ (∃x. a ≽ x ∧ b ≽ x ∧ x ∈ Δ s))"

lemma suppI:
  assumes "⋀a b s. a ∈ Δ s ∧ b ∈ Δ s ⟹ (∃x. a ≽ x ∧ b ≽ x ∧ x ∈ Δ s)"
  shows "supp Δ"
  by (simp add: assms supp_def)

lemma supp_admissible:
  "ccpo.admissible Sup_class.Sup (≤) supp"
proof (rule ccpo.admissibleI)
  fix A :: "('c, 'd, 'a) interp set"
  assume asm0: "Complete_Partial_Order.chain (≤) A"
  "A ≠ {}" "∀x∈A. supp x"
  show "supp (Sup_class.Sup A)"
  proof (rule suppI)
    fix a b s
    assume asm: "a ∈ Sup_class.Sup A s ∧ b ∈ Sup_class.Sup A s"
    then obtain Δa Δb where "Δa ∈ A" "Δb ∈ A" "a ∈ Δa s" "b ∈ Δb s"
      by auto
    then show "∃x. a ≽ x ∧ b ≽ x ∧ x ∈ Sup_class.Sup A s"
    proof (cases "Δa s ⊆ Δb s")
      case True
      then have "a ∈ Δb s"
        using ‹a ∈ Δa s› by blast
      then obtain x where "a ≽ x" "b ≽ x" "x ∈ Δb s"
        by (metis ‹Δb ∈ A› ‹b ∈ Δb s› asm0(3) supp_def)
      then show ?thesis
        using ‹Δb ∈ A› by auto
    next
      case False
      then have "b ∈ Δa s"
        by (metis ‹Δa ∈ A› ‹Δb ∈ A› ‹b ∈ Δb s› asm0(1) chainD le_funD subsetD)
      then obtain x where "a ≽ x" "b ≽ x" "x ∈ Δa s"
        using ‹Δa ∈ A› ‹a ∈ Δa s› asm0(3) supp_def by metis
      then show ?thesis using ‹Δa ∈ A› by auto
    qed
  qed
qed

lemma "Sup_class.Sup {} = empty_interp" using empty_interp_def
  by fastforce

lemma set_closure_prop_empty_all:
  shows "set_closure_property S empty_interp"
  and "set_closure_property S full_interp"
   apply (metis empty_interp_def equals0D set_closure_propertyI)
  by (simp add: full_interp_def set_closure_propertyI)

lemma LFP_preserves_set_closure_property_aux:
  assumes "monotonic f"
      and "set_closure_property S empty_interp"
      and "⋀Δ. set_closure_property S Δ ⟹ set_closure_property S (f Δ)"
    shows "set_closure_property S (ccpo_class.fixp f)"
  using set_closure_property_admissible
proof (rule fixp_induct[of "set_closure_property S"])
  show "set_closure_property S (Sup_class.Sup {})"
    by (simp add: set_closure_property_def)
  show "monotone (≤) (≤) f"
    by (metis (full_types) assms(1) le_fun_def monotoneI monotonic_def smaller_interp_def)
  show "⋀x. set_closure_property S x ⟹ set_closure_property S (f x)"
    by (simp add: assms(3))
qed

lemma GFP_preserves_set_closure_property_aux:
  assumes "order_class.mono f"
      and "set_closure_property S full_interp"
      and "⋀Δ. set_closure_property S Δ ⟹ set_closure_property S (f Δ)"
    shows "set_closure_property S (complete_lattice_class.gfp f)"
  using assms(1)
proof (rule gfp_ordinal_induct[of f "set_closure_property S"])
  show "⋀Sa. set_closure_property S Sa ⟹ complete_lattice_class.gfp f ≤ Sa ⟹ set_closure_property S (f Sa)"
    using assms(3) by blast
  fix M :: "('c, 'd, 'a) interp set"
  assume "∀Sa∈M. set_closure_property S Sa"
  show "set_closure_property S (Inf_class.Inf M)"
  proof (rule set_closure_propertyI)
    fix a b s
    assume "a ∈ Inf_class.Inf M s ∧ b ∈ Inf_class.Inf M s"
    then have "⋀Δ. Δ ∈ M ⟹ a ∈ Δ s ∧ b ∈ Δ s"
      by simp
    then have "⋀Δ. Δ ∈ M ⟹ S a b ⊆ Δ s"
      by (metis ‹∀Sa∈M. set_closure_property S Sa› set_closure_property_def)
    show "S a b ⊆ Inf_class.Inf M s"
      by (simp add: ‹⋀Δ. Δ ∈ M ⟹ S a b ⊆ Δ s› complete_lattice_class.INF_greatest)
  qed
qed








subsection Theorems

subsubsection ‹Greatest Fixed Point›

theorem GFP_is_FP:
  assumes "monotonic f"
  shows "f (GFP f) = GFP f"
proof -
  let ?u = "GFP f"
  have "⋀x. x ∈ D f ⟹ smaller_interp x (f ?u)"
  proof -
    fix x
    assume "x ∈ D f"
    then have "smaller_interp (f x) (f ?u)"
      using assms monotonic_def smaller_interp_D by blast
    moreover have "smaller_interp x (f x)"
      using D_def ‹x ∈ D f› by fastforce
    ultimately show "smaller_interp x (f ?u)"
      using smaller_interp_trans by blast
  qed
  then have "?u ∈ D f"
    using D_def GFP_lub by blast
  then have "f ?u ∈ D f"
    by (metis CollectI D_def ‹⋀x. x ∈ D f ⟹ smaller_interp x (f (GFP f))› assms monotonic_def)
  then show ?thesis
    by (simp add: ‹GFP f ∈ D f› ‹⋀x. x ∈ D f ⟹ smaller_interp x (f (GFP f))› smaller_interp_D smaller_interp_antisym)
qed


theorem GFP_greatest:
  assumes "f u = u"
  shows "smaller_interp u (GFP f)"
  by (simp add: D_def assms smaller_interp_D smaller_interp_refl)


lemma same_GFP:
  assumes "monotonic f"
  shows "complete_lattice_class.gfp f = GFP f"
proof -
  have "f (GFP f) = GFP f"
    using GFP_is_FP assms by blast
  then have "smaller_interp (GFP f) (complete_lattice_class.gfp f)"
    by (metis complete_lattice_class.gfp_upperbound le_funD order_class.order.eq_iff smaller_interp_def)
  moreover have "f (complete_lattice_class.gfp f) = complete_lattice_class.gfp f"
    using assms gfp_fixpoint mono_same by blast
  then have "smaller_interp (complete_lattice_class.gfp f) (GFP f)"
    by (simp add: GFP_greatest)
  ultimately show ?thesis
    by simp
qed

subsubsection ‹Least Fixed Point›

theorem LFP_is_FP:
  assumes "monotonic f"
  shows "f (LFP f) = LFP f"
proof -
  let ?u = "LFP f"
  have "⋀x. x ∈ DD f ⟹ smaller_interp (f ?u) x"
  proof -
    fix x
    assume "x ∈ DD f"
    then have "smaller_interp (f ?u) (f x)"
      using assms monotonic_def smaller_interp_DD by blast
    moreover have "smaller_interp (f x) x"
      using DD_def ‹x ∈ DD f› by fastforce
    ultimately show "smaller_interp (f ?u) x"
      using smaller_interp_trans by blast
  qed
  then have "?u ∈ DD f"
    using DD_def LFP_glb by blast
  then have "f ?u ∈ DD f"
    by (metis (mono_tags, lifting) CollectI DD_def ‹⋀x. x ∈ DD f ⟹ smaller_interp (f (LFP f)) x› assms monotonic_def)
  then show ?thesis
    by (simp add: ‹LFP f ∈ DD f› ‹⋀x. x ∈ DD f ⟹ smaller_interp (f (LFP f)) x› smaller_interp_DD smaller_interp_antisym)
qed

theorem LFP_least:
  assumes "f u = u"
  shows "smaller_interp (LFP f) u"
  by (simp add: DD_def assms smaller_interp_DD smaller_interp_refl)



lemma same_LFP:
  assumes "monotonic f"
  shows "complete_lattice_class.lfp f = LFP f"
proof -
  have "f (LFP f) = LFP f"
    using LFP_is_FP assms by blast
  then have "smaller_interp (complete_lattice_class.lfp f) (LFP f)"
    by (metis complete_lattice_class.lfp_lowerbound le_funE preorder_class.order_refl smaller_interp_def)
  moreover have "f (complete_lattice_class.gfp f) = complete_lattice_class.gfp f"
    using assms gfp_fixpoint mono_same by blast
  then have "smaller_interp (LFP f) (complete_lattice_class.lfp f)"
    by (meson LFP_least assms lfp_fixpoint mono_same)
  ultimately show ?thesis
    by simp
qed


lemma LFP_same:
  assumes "monotonic f"
  shows "ccpo_class.fixp f = LFP f"
proof -
  have "f (ccpo_class.fixp f) = ccpo_class.fixp f"
    by (metis (mono_tags, lifting) assms fixp_unfold mono_same monotoneI order_class.mono_def)
  then have "smaller_interp (LFP f) (ccpo_class.fixp f)"
    by (simp add: LFP_least)
  moreover have "f (LFP f) = LFP f"
    using LFP_is_FP assms by blast
  then have "ccpo_class.fixp f ≤ LFP f"
    by (metis assms fixp_lowerbound mono_same monotoneI order_class.mono_def preorder_class.order_refl)
  ultimately show ?thesis
    by (metis assms lfp_eq_fixp mono_same same_LFP)
qed



text ‹The following theorem corresponds to Theorem 5 of the paper~\<^cite>‹"UnboundedSL"›.›

theorem FP_preserves_set_closure_property:
  assumes "monotonic f"
      and "⋀Δ. set_closure_property S Δ ⟹ set_closure_property S (f Δ)"
    shows "set_closure_property S (GFP f)"
      and "set_closure_property S (LFP f)"
  apply (metis GFP_preserves_set_closure_property_aux assms(1) assms(2) mono_same same_GFP set_closure_prop_empty_all(2))
  by (metis LFP_preserves_set_closure_property_aux LFP_same assms(1) assms(2) set_closure_prop_empty_all(1))

end

end