Theory Calculus_Variations
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
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)
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
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
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)
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
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
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)
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
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)
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)"
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)
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
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)
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