# Theory M2L_Equivalence_Checking

```(* Author: Dmitriy Traytel *)

section ‹Deciding Equivalence of M2L Formulas›

(*<*)
theory M2L_Equivalence_Checking
imports
Pi_Equivalence_Checking
PNormalization
Init_Normalization
M2L_Normalization
Pi_Regular_Exp_Dual
begin
(*>*)

global_interpretation embed "set o σ Σ" "wf_atom Σ" π lookup "ε Σ"
for Σ :: "'a :: linorder list"
defines
𝔇 = "embed.lderiv lookup (ε Σ)"
and Co𝔇 = "embed.lderiv_dual lookup (ε Σ)"
by unfold_locales (auto simp: σ_def π_def ε_def set_n_lists)

lemma enum_not_empty[simp]: "Enum.enum ≠ []" (is "?enum ≠ []")
proof (rule notI)
assume "?enum = []"
hence "set ?enum = {}" by simp
thus False unfolding UNIV_enum[symmetric] by simp
qed

global_interpretation Φ: formula "Enum.enum :: 'a :: {enum, linorder} list"
defines
pre_wf_formula = Φ.pre_wf_formula
and wf_formula = Φ.wf_formula
and rexp_of = Φ.rexp_of
and rexp_of_alt = Φ.rexp_of_alt
and rexp_of_alt' = Φ.rexp_of_alt'
and rexp_of' = Φ.rexp_of'
and rexp_of'' = Φ.rexp_of''
and valid_ENC = Φ.valid_ENC
and ENC = Φ.ENC
and dec_interp = Φ.dec_interp
by unfold_locales (auto simp: σ_def π_def set_n_lists)

lemma lang_Plus_Zero: "lang Σ n (Plus r One) = lang Σ n (Plus s One) ⟷ lang Σ n r - {[]} = lang Σ n s - {[]}"
by auto

lemmas lang⇩M⇩2⇩L_rexp_of_norm = trans[OF sym[OF Φ.lang⇩M⇩2⇩L_norm] Φ.lang⇩M⇩2⇩L_rexp_of]
lemmas lang⇩M⇩2⇩L_rexp_of'_norm = trans[OF sym[OF Φ.lang⇩M⇩2⇩L_norm] Φ.lang⇩M⇩2⇩L_rexp_of']
lemmas lang⇩M⇩2⇩L_rexp_of''_norm = trans[OF sym[OF Φ.lang⇩M⇩2⇩L_norm] Φ.lang⇩M⇩2⇩L_rexp_of'']

setup ‹Sign.map_naming (Name_Space.mandatory_path "slow")›

global_interpretation D: rexp_DFA "σ Σ" "wf_atom Σ" π lookup "λx. «pnorm (inorm x)»"
"λa r. «𝔇 Σ a r»" final "alphabet.wf (wf_atom Σ) n" pnorm "lang Σ n" n
for Σ :: "'a :: linorder list" and n :: nat
defines
test = "rexp_DA.test (final :: 'a atom rexp ⇒ bool)"
and step = "rexp_DA.step (σ Σ) (λa r. «𝔇 Σ a r») pnorm n"
and closure = "rexp_DA.closure (σ Σ) (λa r. «𝔇 Σ a r») final pnorm n"
and check_eqvRE = "rexp_DA.check_eqv (σ Σ) (λx. «pnorm (inorm x)») (λa r. «𝔇 Σ a r») final pnorm n"
and test_invariant = "rexp_DA.test_invariant (final :: 'a atom rexp ⇒ bool) ::
(('a × bool list) list × _) list × _ ⇒ bool"
and step_invariant = "rexp_DA.step_invariant (σ Σ) (λa r. «𝔇 Σ a r») pnorm n"
and closure_invariant = "rexp_DA.closure_invariant (σ Σ) (λa r. «𝔇 Σ a r») final pnorm n"
and counterexampleRE = "rexp_DA.counterexample (σ Σ) (λx. «pnorm (inorm x)») (λa r. «𝔇 Σ a r») final pnorm n"
and reachable = "rexp_DA.reachable (σ Σ) (λx. «pnorm (inorm x)») (λa r. «𝔇 Σ a r») pnorm n"
and automaton = "rexp_DA.automaton (σ Σ) (λx. «pnorm (inorm x)») (λa r. «𝔇 Σ a r») pnorm n"
by unfold_locales (auto simp only: comp_apply
ACI_norm_wf ACI_norm_lang wf_inorm lang_inorm wf_pnorm lang_pnorm wf_lderiv lang_lderiv
lang_final finite_fold_lderiv dest!: lang_subset_lists)

definition check_eqv where
"check_eqv n φ ψ ⟷ wf_formula n (FOr φ ψ) ∧
slow.check_eqvRE Enum.enum n (Plus (rexp_of'' n (norm φ)) One) (Plus (rexp_of'' n (norm ψ)) One)"

definition counterexample where
"counterexample n φ ψ =
map_option (λw. dec_interp n (FOV (FOr φ ψ)) w)
(slow.counterexampleRE Enum.enum n (Plus (rexp_of'' n (norm φ)) One) (Plus (rexp_of'' n (norm ψ)) One))"

lemma soundness: "slow.check_eqv n φ ψ ⟹ Φ.lang⇩M⇩2⇩L n φ = Φ.lang⇩M⇩2⇩L n ψ"
by (rule box_equals[OF iffD1[OF lang_Plus_Zero, OF slow.D.check_eqv_sound]
sym[OF trans[OF lang⇩M⇩2⇩L_rexp_of''_norm]] sym[OF trans[OF lang⇩M⇩2⇩L_rexp_of''_norm]]])
(auto simp: slow.check_eqv_def intro!: Φ.wf_rexp_of'')

lemma completeness:
assumes "Φ.lang⇩M⇩2⇩L n φ = Φ.lang⇩M⇩2⇩L n ψ" "wf_formula n (FOr φ ψ)"
shows "slow.check_eqv n φ ψ"
using assms(2) unfolding slow.check_eqv_def
by (intro conjI[OF assms(2) slow.D.check_eqv_complete[OF iffD2[OF lang_Plus_Zero]],
OF box_equals[OF assms(1) lang⇩M⇩2⇩L_rexp_of''_norm lang⇩M⇩2⇩L_rexp_of''_norm]])
(auto intro!: Φ.wf_rexp_of'')

setup ‹Sign.map_naming Name_Space.parent_path›

setup ‹Sign.map_naming (Name_Space.mandatory_path "fast")›

global_interpretation D: rexp_DA_no_post "σ Σ" "wf_atom Σ" π lookup "λx. pnorm (inorm x)"
"λa r. pnorm (𝔇 Σ a r)" final "alphabet.wf (wf_atom Σ) n" "lang Σ n" n
for Σ :: "'a :: linorder list" and n :: nat
defines
test = "rexp_DA.test (final :: 'a atom rexp ⇒ bool)"
and step = "rexp_DA.step (σ Σ) (λa r. pnorm (𝔇 Σ a r)) id n"
and closure = "rexp_DA.closure (σ Σ) (λa r. pnorm (𝔇 Σ a r)) final id n"
and check_eqvRE = "rexp_DA.check_eqv (σ Σ) (λx. pnorm (inorm x)) (λa r. pnorm (𝔇 Σ a r)) final id n"
and test_invariant = "rexp_DA.test_invariant (final :: 'a atom rexp ⇒ bool) ::
(('a × bool list) list × _) list × _ ⇒ bool"
and step_invariant = "rexp_DA.step_invariant (σ Σ) (λa r. pnorm (𝔇 Σ a r)) id n"
and closure_invariant = "rexp_DA.closure_invariant (σ Σ) (λa r. pnorm (𝔇 Σ a r)) final id n"
and counterexampleRE = "rexp_DA.counterexample (σ Σ) (λx. pnorm (inorm x)) (λa r. pnorm (𝔇 Σ a r)) final id n"
and reachable = "rexp_DA.reachable (σ Σ) (λx. pnorm (inorm x)) (λa r. pnorm (𝔇 Σ a r)) id n"
and automaton = "rexp_DA.automaton (σ Σ) (λx. pnorm (inorm x)) (λa r. pnorm (𝔇 Σ a r)) id n"
by unfold_locales (auto simp only: comp_apply
ACI_norm_wf ACI_norm_lang wf_inorm lang_inorm wf_pnorm lang_pnorm wf_lderiv lang_lderiv id_apply
lang_final dest!: lang_subset_lists)

definition check_eqv where
"check_eqv n φ ψ ⟷ wf_formula n (FOr φ ψ) ∧
fast.check_eqvRE Enum.enum n (Plus (rexp_of'' n (norm φ)) One) (Plus (rexp_of'' n (norm ψ)) One)"

definition counterexample where
"counterexample n φ ψ =
map_option (λw. dec_interp n (FOV (FOr φ ψ)) w)
(fast.counterexampleRE Enum.enum n (Plus (rexp_of'' n (norm φ)) One) (Plus (rexp_of'' n (norm ψ)) One))"

lemma soundness: "fast.check_eqv n φ ψ ⟹ Φ.lang⇩M⇩2⇩L n φ = Φ.lang⇩M⇩2⇩L n ψ"
by (rule box_equals[OF iffD1[OF lang_Plus_Zero, OF fast.D.check_eqv_sound]
sym[OF trans[OF lang⇩M⇩2⇩L_rexp_of''_norm]] sym[OF trans[OF lang⇩M⇩2⇩L_rexp_of''_norm]]])
(auto simp: fast.check_eqv_def intro!: Φ.wf_rexp_of'')

setup ‹Sign.map_naming Name_Space.parent_path›

setup ‹Sign.map_naming (Name_Space.mandatory_path "dual")›

global_interpretation D: rexp_DA_no_post "σ Σ" "wf_atom Σ" π lookup
"λx. pnorm_dual (rexp_dual_of (inorm x))" "λa r. pnorm_dual (Co𝔇 Σ a r)" final_dual
"alphabet.wf_dual (wf_atom Σ) n" "lang_dual Σ n" n
for Σ :: "'a :: linorder list" and n :: nat
defines
test = "rexp_DA.test (final_dual :: 'a atom rexp_dual ⇒ bool)"
and step = "rexp_DA.step (σ Σ) (λa r. pnorm_dual (Co𝔇 Σ a r)) id n"
and closure = "rexp_DA.closure (σ Σ) (λa r. pnorm_dual (Co𝔇 Σ a r)) final_dual id n"
and check_eqvRE = "rexp_DA.check_eqv (σ Σ) (λx. pnorm_dual (rexp_dual_of (inorm x))) (λa r. pnorm_dual (Co𝔇 Σ a r)) final_dual id n"
and test_invariant = "rexp_DA.test_invariant (final_dual :: 'a atom rexp_dual ⇒ bool) ::
(('a × bool list) list × _) list × _ ⇒ bool"
and step_invariant = "rexp_DA.step_invariant (σ Σ) (λa r. pnorm_dual (Co𝔇 Σ a r)) id n"
and closure_invariant = "rexp_DA.closure_invariant (σ Σ) (λa r. pnorm_dual (Co𝔇 Σ a r)) final_dual id n"
and counterexampleRE = "rexp_DA.counterexample (σ Σ) (λx. pnorm_dual (rexp_dual_of (inorm x))) (λa r. pnorm_dual (Co𝔇 Σ a r)) final_dual id n"
and reachable = "rexp_DA.reachable (σ Σ) (λx. pnorm_dual (rexp_dual_of (inorm x))) (λa r. pnorm_dual (Co𝔇 Σ a r)) id n"
and automaton = "rexp_DA.automaton (σ Σ) (λx. pnorm_dual (rexp_dual_of (inorm x))) (λa r. pnorm_dual (Co𝔇 Σ a r)) id n"
by unfold_locales (auto simp only: comp_apply id_apply
wf_inorm lang_inorm
wf_dual_pnorm_dual lang_dual_pnorm_dual
wf_dual_rexp_dual_of lang_dual_rexp_dual_of
wf_dual_lderiv_dual lang_dual_lderiv_dual
lang_dual_final_dual dest!: lang_dual_subset_lists)

definition check_eqv where
"check_eqv n φ ψ ⟷ wf_formula n (FOr φ ψ) ∧
dual.check_eqvRE Enum.enum n (Plus (rexp_of'' n (norm φ)) One) (Plus (rexp_of'' n (norm ψ)) One)"

definition counterexample where
"counterexample n φ ψ =
map_option (λw. dec_interp n (FOV (FOr φ ψ)) w)
(dual.counterexampleRE Enum.enum n (Plus (rexp_of'' n (norm φ)) One) (Plus (rexp_of'' n (norm ψ)) One))"

lemma soundness: "dual.check_eqv n φ ψ ⟹ Φ.lang⇩M⇩2⇩L n φ = Φ.lang⇩M⇩2⇩L n ψ"
by (rule box_equals[OF iffD1[OF lang_Plus_Zero, OF dual.D.check_eqv_sound]
sym[OF trans[OF lang⇩M⇩2⇩L_rexp_of''_norm]] sym[OF trans[OF lang⇩M⇩2⇩L_rexp_of''_norm]]])
(auto simp: dual.check_eqv_def intro!: Φ.wf_rexp_of'')

setup ‹Sign.map_naming Name_Space.parent_path›

(*<*)
end
(*>*)
```