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 langM2L_rexp_of_norm = trans[OF sym[OF Φ.langM2L_norm] Φ.langM2L_rexp_of]
lemmas langM2L_rexp_of'_norm = trans[OF sym[OF Φ.langM2L_norm] Φ.langM2L_rexp_of']
lemmas langM2L_rexp_of''_norm = trans[OF sym[OF Φ.langM2L_norm] Φ.langM2L_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 φ ψ ⟹ Φ.langM2L n φ = Φ.langM2L n ψ"
  by (rule box_equals[OF iffD1[OF lang_Plus_Zero, OF slow.D.check_eqv_sound]
  sym[OF trans[OF langM2L_rexp_of''_norm]] sym[OF trans[OF langM2L_rexp_of''_norm]]])
   (auto simp: slow.check_eqv_def intro!: Φ.wf_rexp_of'')

lemma completeness:
  assumes "Φ.langM2L n φ = Φ.langM2L 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) langM2L_rexp_of''_norm langM2L_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 φ ψ ⟹ Φ.langM2L n φ = Φ.langM2L n ψ"
  by (rule box_equals[OF iffD1[OF lang_Plus_Zero, OF fast.D.check_eqv_sound]
  sym[OF trans[OF langM2L_rexp_of''_norm]] sym[OF trans[OF langM2L_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 φ ψ ⟹ Φ.langM2L n φ = Φ.langM2L n ψ"
  by (rule box_equals[OF iffD1[OF lang_Plus_Zero, OF dual.D.check_eqv_sound]
  sym[OF trans[OF langM2L_rexp_of''_norm]] sym[OF trans[OF langM2L_rexp_of''_norm]]])
   (auto simp: dual.check_eqv_def intro!: Φ.wf_rexp_of'')

setup ‹Sign.map_naming Name_Space.parent_path›

(*<*)
end
(*>*)