Theory Ample_Correctness

section ‹Correctness Theorem of Partial Order Reduction›

theory Ample_Correctness
imports
  Ample_Abstract
  Formula
begin

  locale ample_correctness =
    S: transition_system_complete ex en init int +
    R: transition_system_complete ex ren init int +
    F: formula_next_free φ +
    ample_abstract ex en init int ind src ren
    for ex :: "'action ⇒ 'state ⇒ 'state"
    and en :: "'action ⇒ 'state ⇒ bool"
    and init :: "'state ⇒ bool"
    and int :: "'state ⇒ 'interpretation"
    and ind :: "'action ⇒ 'action ⇒ bool"
    and src :: "'state ⇒ 'state ⇒ bool"
    and ren :: "'action ⇒ 'state ⇒ bool"
    and φ :: "'interpretation pltl"
  begin

    lemma reduction_language_indistinguishable:
      assumes "R.language ⊆ F.language"
      shows "S.language ⊆ F.language"
    proof
      fix u
      assume 1: "u ∈ S.language"
      obtain v where 2: "v ∈ R.language" "snth u ≈ snth v" using reduction_language_stuttering 1 by this
      have 3: "v ∈ F.language" using assms 2(1) by rule
      show "u ∈ F.language" using 2(2) 3 by auto
    qed

    theorem reduction_correct: "S.language ⊆ F.language ⟷ R.language ⊆ F.language"
      using reduction_language_subset reduction_language_indistinguishable by blast

  end

end