Theory Calculus_Variations

(*  Title:       Variations on a Theme
 *  Author:      Sophie Tourret <stourret at mpi-inf.mpg.de>, 2018-2020 *)

section ‹Variations on a Theme›

text ‹In this section, section 2.4 of the report is covered, demonstrating
  that various notions of redundancy are equivalent.›

theory Calculus_Variations
  imports Calculus
begin

locale reduced_calculus = calculus Bot Inf entails Red_I Red_F
  for
    Bot :: "'f set" and
    Inf :: ‹'f inference set› and
    entails :: "'f set ⇒ 'f set ⇒ bool" (infix "⊨" 50) and
    Red_I :: "'f set ⇒ 'f inference set" and
    Red_F :: "'f set ⇒ 'f set"
 + assumes
   inf_in_red_inf: "Inf_between UNIV (Red_F N) ⊆ Red_I N"
begin

(* lem:reduced-rc-implies-sat-equiv-reduced-sat *)
lemma sat_eq_reduc_sat: "saturated N ⟷ reduc_saturated N"
proof
  fix N
  assume "saturated N"
  then show "reduc_saturated N"
    using Red_I_without_red_F saturated_without_red_F
    unfolding saturated_def reduc_saturated_def
    by blast
next
  fix N
  assume red_sat_n: "reduc_saturated N"
  show "saturated N" unfolding saturated_def
    using red_sat_n inf_in_red_inf unfolding reduc_saturated_def Inf_from_def Inf_between_def
    by blast
qed

end

locale reducedly_statically_complete_calculus = calculus +
  assumes reducedly_statically_complete:
    "B ∈ Bot ⟹ reduc_saturated N ⟹ N ⊨ {B} ⟹ ∃B'∈Bot. B' ∈ N"

locale reducedly_statically_complete_reduced_calculus = reduced_calculus +
  assumes reducedly_statically_complete:
    "B ∈ Bot ⟹ reduc_saturated N ⟹ N ⊨ {B} ⟹ ∃B'∈Bot. B' ∈ N"
begin

sublocale reducedly_statically_complete_calculus
  by (simp add: calculus_axioms reducedly_statically_complete
    reducedly_statically_complete_calculus_axioms.intro
    reducedly_statically_complete_calculus_def)

(* cor:reduced-rc-implies-st-ref-comp-equiv-reduced-st-ref-comp 1/2 *)
sublocale statically_complete_calculus
proof
  fix B N
  assume
    bot_elem: ‹B ∈ Bot› and
    saturated_N: "saturated N" and
    refut_N: "N ⊨ {B}"
  have reduc_saturated_N: "reduc_saturated N" using saturated_N sat_eq_reduc_sat by blast
  show "∃B'∈Bot. B' ∈ N" using reducedly_statically_complete[OF bot_elem reduc_saturated_N refut_N] .
qed

end

context reduced_calculus
begin

(* cor:reduced-rc-implies-st-ref-comp-equiv-reduced-st-ref-comp 2/2 *)
lemma stat_ref_comp_imp_red_stat_ref_comp:
  "statically_complete_calculus Bot Inf entails Red_I Red_F ⟹
   reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F"
proof
  fix B N
  assume
    stat_ref_comp: "statically_complete_calculus Bot Inf (⊨) Red_I Red_F" and
    bot_elem: ‹B ∈ Bot› and
    saturated_N: "reduc_saturated N" and
    refut_N: "N ⊨ {B}"
  have reduc_saturated_N: "saturated N" using saturated_N sat_eq_reduc_sat by blast
  show "∃B'∈Bot. B' ∈ N"
    using statically_complete_calculus.statically_complete[OF stat_ref_comp
      bot_elem reduc_saturated_N refut_N] .
qed

end

context calculus
begin

definition Red_Red_I :: "'f set ⇒ 'f inference set" where
  "Red_Red_I N = Red_I N ∪ Inf_between UNIV (Red_F N)"

lemma reduced_calc_is_calc: "calculus Bot Inf entails Red_Red_I Red_F"
proof
  fix N
  show "Red_Red_I N ⊆ Inf"
    unfolding Red_Red_I_def Inf_between_def Inf_from_def using Red_I_to_Inf by auto
next
  fix B N
  assume
    b_in: "B ∈ Bot" and
    n_entails: "N ⊨ {B}"
  show "N - Red_F N ⊨ {B}"
    by (simp add: Red_F_Bot b_in n_entails)
next
  fix N N' :: "'f set"
  assume "N ⊆ N'"
  then show "Red_F N ⊆ Red_F N'" by (simp add: Red_F_of_subset)
next
  fix N N' :: "'f set"
  assume n_in: "N ⊆ N'"
  then have "Inf_from (UNIV - (Red_F N')) ⊆ Inf_from (UNIV - (Red_F N))"
    using Red_F_of_subset[OF n_in] unfolding Inf_from_def by auto
  then have "Inf_between UNIV (Red_F N) ⊆ Inf_between UNIV (Red_F N')"
    unfolding Inf_between_def by auto
  then show "Red_Red_I N ⊆ Red_Red_I N'"
    unfolding Red_Red_I_def using Red_I_of_subset[OF n_in] by blast
next
  fix N N' :: "'f set"
  assume "N' ⊆ Red_F N"
  then show "Red_F N ⊆ Red_F (N - N')" by (simp add: Red_F_of_Red_F_subset)
next
  fix N N' :: "'f set"
  assume np_subs: "N' ⊆ Red_F N"
  have "Red_F N ⊆ Red_F (N - N')" by (simp add: Red_F_of_Red_F_subset np_subs)
  then have "Inf_from (UNIV - (Red_F (N - N'))) ⊆ Inf_from (UNIV - (Red_F N))"
    by (metis Diff_subset Red_F_of_subset eq_iff)
  then have "Inf_between UNIV (Red_F N) ⊆ Inf_between UNIV (Red_F (N - N'))"
    unfolding Inf_between_def by auto
  then show "Red_Red_I N ⊆ Red_Red_I (N - N')"
    unfolding Red_Red_I_def using Red_I_of_Red_F_subset[OF np_subs] by blast
next
  fix ι N
  assume "ι ∈ Inf"
    "concl_of ι ∈ N"
  then show "ι ∈ Red_Red_I N"
    by (simp add: Red_I_of_Inf_to_N Red_Red_I_def)
qed

lemma inf_subs_reduced_red_inf: "Inf_between UNIV (Red_F N) ⊆ Red_Red_I N"
  unfolding Red_Red_I_def by simp

(* lem:red'-is-reduced-redcrit *)
text ‹The following is a lemma and not a sublocale as was previously used in similar cases.
  Here, a sublocale cannot be used because it would create an infinitely descending
  chain of sublocales. ›
lemma reduc_calc: "reduced_calculus Bot Inf entails Red_Red_I Red_F"
  using inf_subs_reduced_red_inf reduced_calc_is_calc
  by (simp add: reduced_calculus.intro reduced_calculus_axioms_def)

interpretation reduc_calc: reduced_calculus Bot Inf entails Red_Red_I Red_F
  by (fact reduc_calc)

(* lem:saturation-red-vs-red'-1 *)
lemma sat_imp_red_calc_sat: "saturated N ⟹ reduc_calc.saturated N"
  unfolding saturated_def reduc_calc.saturated_def Red_Red_I_def by blast

(* lem:saturation-red-vs-red'-2 1/2 (i) ⟷ (ii) *)
lemma red_sat_eq_red_calc_sat: "reduc_saturated N ⟷ reduc_calc.saturated N"
proof
  assume red_sat_n: "reduc_saturated N"
  show "reduc_calc.saturated N"
    unfolding reduc_calc.saturated_def
  proof
    fix ι
    assume i_in: "ι ∈ Inf_from N"
    show "ι ∈ Red_Red_I N"
      using i_in red_sat_n
      unfolding reduc_saturated_def Inf_between_def Inf_from_def Red_Red_I_def by blast
  qed
next
  assume red_sat_n: "reduc_calc.saturated N"
  show "reduc_saturated N"
    unfolding reduc_saturated_def
  proof
    fix ι
    assume i_in: "ι ∈ Inf_from (N - Red_F N)"
    show "ι ∈ Red_I N"
      using i_in red_sat_n
      unfolding Inf_from_def reduc_calc.saturated_def Red_Red_I_def Inf_between_def by blast
  qed
qed

(* lem:saturation-red-vs-red'-2 2/2 (i) ⟷ (iii) *)
lemma red_sat_eq_sat: "reduc_saturated N ⟷ saturated (N - Red_F N)"
  unfolding reduc_saturated_def saturated_def by (simp add: Red_I_without_red_F)

(* thm:reduced-stat-ref-compl 1/3 (i) ⟷ (iii) *)
theorem stat_is_stat_red: "statically_complete_calculus Bot Inf entails Red_I Red_F ⟷
  statically_complete_calculus Bot Inf entails Red_Red_I Red_F"
proof
  assume
    stat_ref1: "statically_complete_calculus Bot Inf entails Red_I Red_F"
  show "statically_complete_calculus Bot Inf entails Red_Red_I Red_F"
    using reduc_calc.calculus_axioms
    unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def
  proof
    show "∀B N. B ∈ Bot ⟶ reduc_calc.saturated N ⟶ N ⊨ {B} ⟶ (∃B'∈Bot. B' ∈ N)"
    proof (clarify)
      fix B N
      assume
        b_in: "B ∈ Bot" and
        n_sat: "reduc_calc.saturated N" and
        n_imp_b: "N ⊨ {B}"
      have "saturated (N - Red_F N)" using red_sat_eq_red_calc_sat[of N] red_sat_eq_sat[of N] n_sat by blast
      moreover have "(N - Red_F N) ⊨ {B}" using n_imp_b b_in by (simp add: reduc_calc.Red_F_Bot)
      ultimately show "∃B'∈Bot. B'∈ N"
        using stat_ref1 by (meson DiffD1 b_in statically_complete_calculus.statically_complete)
    qed
  qed
next
  assume
    stat_ref3: "statically_complete_calculus Bot Inf entails Red_Red_I Red_F"
  show "statically_complete_calculus Bot Inf entails Red_I Red_F"
    unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def
    using calculus_axioms
  proof
    show "∀B N. B ∈ Bot ⟶ saturated N ⟶ N ⊨ {B} ⟶ (∃B'∈Bot. B' ∈ N)"
    proof clarify
      fix B N
      assume
        b_in: "B ∈ Bot" and
        n_sat: "saturated N" and
        n_imp_b: "N ⊨ {B}"
      then show "∃B'∈ Bot. B' ∈ N"
        using stat_ref3 sat_imp_red_calc_sat[OF n_sat]
        by (meson statically_complete_calculus.statically_complete)
    qed
  qed
qed

(* thm:reduced-stat-ref-compl 2/3 (iv) ⟷ (iii) *)
theorem red_stat_red_is_stat_red:
  "reducedly_statically_complete_calculus Bot Inf entails Red_Red_I Red_F ⟷
   statically_complete_calculus Bot Inf entails Red_Red_I Red_F"
  using reduc_calc.stat_ref_comp_imp_red_stat_ref_comp
  by (metis reduc_calc.sat_eq_reduc_sat reducedly_statically_complete_calculus.axioms(2)
    reducedly_statically_complete_calculus_axioms_def reduced_calc_is_calc
    statically_complete_calculus.intro statically_complete_calculus_axioms.intro)

(* thm:reduced-stat-ref-compl 3/3 (ii) ⟷ (iii) *)
theorem red_stat_is_stat_red:
  "reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F ⟷
   statically_complete_calculus Bot Inf entails Red_Red_I Red_F"
  using reduc_calc.calculus_axioms calculus_axioms red_sat_eq_red_calc_sat
  unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def
    reducedly_statically_complete_calculus_def reducedly_statically_complete_calculus_axioms_def
  by blast

lemma sup_red_f_in_red_liminf:
  "chain derive Ns ⟹ Sup_llist (lmap Red_F Ns) ⊆ Red_F (Liminf_llist Ns)"
proof
  fix N
  assume
    deriv: "chain derive Ns" and
    n_in_sup: "N ∈ Sup_llist (lmap Red_F Ns)"
  obtain i0 where i_smaller: "enat i0 < llength Ns" and n_in: "N ∈ Red_F (lnth Ns i0)"
    using n_in_sup by (metis Sup_llist_imp_exists_index llength_lmap lnth_lmap)
  have "Red_F (lnth Ns i0) ⊆ Red_F (Liminf_llist Ns)"
    using i_smaller by (simp add: deriv Red_F_subset_Liminf)
  then show "N ∈ Red_F (Liminf_llist Ns)"
    using n_in by fast
qed

lemma sup_red_inf_in_red_liminf:
  "chain derive Ns ⟹ Sup_llist (lmap Red_I Ns) ⊆ Red_I (Liminf_llist Ns)"
proof
  fix ι
  assume
    deriv: "chain derive Ns" and
    i_in_sup: "ι ∈ Sup_llist (lmap Red_I Ns)"
  obtain i0 where i_smaller: "enat i0 < llength Ns" and n_in: "ι ∈ Red_I (lnth Ns i0)"
    using i_in_sup unfolding Sup_llist_def by auto
  have "Red_I (lnth Ns i0) ⊆ Red_I (Liminf_llist Ns)"
    using i_smaller by (simp add: deriv Red_I_subset_Liminf)
  then show "ι ∈ Red_I (Liminf_llist Ns)"
    using n_in by fast
qed

definition reduc_fair :: "'f set llist ⇒ bool" where
  "reduc_fair Ns ⟷
   Inf_from (Liminf_llist Ns - Sup_llist (lmap Red_F Ns)) ⊆ Sup_llist (lmap Red_I Ns)"

(* lem:red-fairness-implies-red-saturation *)
lemma reduc_fair_imp_Liminf_reduc_sat:
  "chain derive Ns ⟹ reduc_fair Ns ⟹ reduc_saturated (Liminf_llist Ns)"
  unfolding reduc_saturated_def
proof -
  fix Ns
  assume
    deriv: "chain derive Ns" and
    red_fair: "reduc_fair Ns"
  have "Inf_from (Liminf_llist Ns - Red_F (Liminf_llist Ns))
    ⊆ Inf_from (Liminf_llist Ns - Sup_llist (lmap Red_F Ns))"
    using sup_red_f_in_red_liminf[OF deriv] unfolding Inf_from_def by blast
  then have "Inf_from (Liminf_llist Ns - Red_F (Liminf_llist Ns)) ⊆ Sup_llist (lmap Red_I Ns)"
    using red_fair unfolding reduc_fair_def by simp
  then show "Inf_from (Liminf_llist Ns - Red_F (Liminf_llist Ns)) ⊆ Red_I (Liminf_llist Ns)"
    using sup_red_inf_in_red_liminf[OF deriv] by fast
qed

end

locale reducedly_dynamically_complete_calculus = calculus +
  assumes
    reducedly_dynamically_complete: "B ∈ Bot ⟹ chain derive Ns ⟹ reduc_fair Ns ⟹
      lhd Ns ⊨ {B} ⟹ ∃i ∈ {i. enat i < llength Ns}. ∃ B'∈Bot. B' ∈ lnth Ns i"
begin

sublocale reducedly_statically_complete_calculus
proof
  fix B N
  assume
    bot_elem: ‹B ∈ Bot› and
    saturated_N: "reduc_saturated N" and
    refut_N: "N ⊨ {B}"
  define Ns where "Ns = LCons N LNil"
  have[simp]: ‹¬ lnull Ns› by (auto simp: Ns_def)
  have deriv_D: ‹chain (⊳) Ns› by (simp add: chain.chain_singleton Ns_def)
  have liminf_is_N: "Liminf_llist Ns = N" by (simp add: Ns_def Liminf_llist_LCons)
  have head_D: "N = lhd Ns" by (simp add: Ns_def)
  have "Sup_llist (lmap Red_F Ns) = Red_F N" by (simp add: Ns_def)
  moreover have "Sup_llist (lmap Red_I Ns) = Red_I N" by (simp add: Ns_def)
  ultimately have fair_D: "reduc_fair Ns"
    using saturated_N liminf_is_N unfolding reduc_fair_def reduc_saturated_def
    by (simp add: reduc_fair_def reduc_saturated_def liminf_is_N)
  obtain i B' where B'_is_bot: ‹B' ∈ Bot› and B'_in: "B' ∈ lnth Ns i" and ‹i < llength Ns›
    using reducedly_dynamically_complete[of B Ns] bot_elem fair_D head_D saturated_N deriv_D refut_N
    by auto
  then have "i = 0"
    by (auto simp: Ns_def enat_0_iff)
  show ‹∃B'∈Bot. B' ∈ N›
    using B'_is_bot B'_in unfolding ‹i = 0› head_D[symmetric] Ns_def by auto
qed

end

sublocale reducedly_statically_complete_calculus ⊆ reducedly_dynamically_complete_calculus
proof
  fix B Ns
  assume
    bot_elem: ‹B ∈ Bot› and
    deriv: ‹chain (⊳) Ns› and
    fair: ‹reduc_fair Ns› and
    unsat: ‹lhd Ns ⊨ {B}›
    have non_empty: ‹¬ lnull Ns› using chain_not_lnull[OF deriv] .
    have subs: ‹lhd Ns ⊆ Sup_llist Ns›
      using lhd_subset_Sup_llist[of Ns] non_empty by (simp add: lhd_conv_lnth)
    have ‹Sup_llist Ns ⊨ {B}›
      using unsat subset_entailed[OF subs] entails_trans[of "Sup_llist Ns" "lhd Ns"] by auto
    then have Sup_no_Red: ‹Sup_llist Ns - Red_F (Sup_llist Ns) ⊨ {B}›
      using bot_elem Red_F_Bot by auto
    have Sup_no_Red_in_Liminf: ‹Sup_llist Ns - Red_F (Sup_llist Ns) ⊆ Liminf_llist Ns›
      using deriv Red_in_Sup by auto
    have Liminf_entails_Bot: ‹Liminf_llist Ns ⊨ {B}›
      using Sup_no_Red subset_entailed[OF Sup_no_Red_in_Liminf] entails_trans by blast
    have ‹reduc_saturated (Liminf_llist Ns)›
    using deriv fair reduc_fair_imp_Liminf_reduc_sat unfolding reduc_saturated_def
      by auto
   then have ‹∃B'∈Bot. B' ∈ Liminf_llist Ns›
     using bot_elem reducedly_statically_complete Liminf_entails_Bot
     by auto
   then show ‹∃i∈{i. enat i < llength Ns}. ∃B'∈Bot. B' ∈ lnth Ns i›
     unfolding Liminf_llist_def by auto
qed

context calculus
begin

lemma dyn_equiv_stat: "dynamically_complete_calculus Bot Inf entails Red_I Red_F =
  statically_complete_calculus Bot Inf entails Red_I Red_F"
proof
  assume "dynamically_complete_calculus Bot Inf entails Red_I Red_F"
  then interpret dynamically_complete_calculus Bot Inf entails Red_I Red_F
    by simp
  show "statically_complete_calculus Bot Inf entails Red_I Red_F"
    by (simp add: statically_complete_calculus_axioms)
next
  assume "statically_complete_calculus Bot Inf entails Red_I Red_F"
  then interpret statically_complete_calculus Bot Inf entails Red_I Red_F
    by simp
  show "dynamically_complete_calculus Bot Inf entails Red_I Red_F"
    by (simp add: dynamically_complete_calculus_axioms)
qed

lemma red_dyn_equiv_red_stat:
  "reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F =
   reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F"
proof
  assume "reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F"
  then interpret reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F
    by simp
  show "reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F"
    by (simp add: reducedly_statically_complete_calculus_axioms)
next
  assume "reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F"
  then interpret reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F
    by simp
  show "reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F"
    by (simp add: reducedly_dynamically_complete_calculus_axioms)
qed

interpretation reduc_calc: reduced_calculus Bot Inf entails Red_Red_I Red_F
  by (fact reduc_calc)

(* thm:reduced-dyn-ref-compl 1/3 (v) ⟷ (vii) *)
theorem dyn_ref_eq_dyn_ref_red:
  "dynamically_complete_calculus Bot Inf entails Red_I Red_F ⟷
   dynamically_complete_calculus Bot Inf entails Red_Red_I Red_F"
  using dyn_equiv_stat stat_is_stat_red reduc_calc.dyn_equiv_stat by meson

(* thm:reduced-dyn-ref-compl 2/3 (viii) ⟷ (vii) *)
theorem red_dyn_ref_red_eq_dyn_ref_red:
  "reducedly_dynamically_complete_calculus Bot Inf entails Red_Red_I Red_F ⟷
   dynamically_complete_calculus Bot Inf entails Red_Red_I Red_F"
  using red_dyn_equiv_red_stat dyn_equiv_stat red_stat_red_is_stat_red
  by (simp add: reduc_calc.dyn_equiv_stat reduc_calc.red_dyn_equiv_red_stat)

(* thm:reduced-dyn-ref-compl 3/3 (vi) ⟷ (vii) *)
theorem red_dyn_ref_eq_dyn_ref_red:
  "reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F ⟷
   dynamically_complete_calculus Bot Inf entails Red_Red_I Red_F"
  using red_dyn_equiv_red_stat dyn_equiv_stat red_stat_is_stat_red
    reduc_calc.dyn_equiv_stat reduc_calc.red_dyn_equiv_red_stat
  by blast

end

end