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