Theory LTL.Equivalence_Relations

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

section ‹Equivalence Relations for LTL formulas›

theory Equivalence_Relations
imports
  LTL
begin

subsection ‹Language Equivalence›

definition ltl_lang_equiv :: "'a ltln  'a ltln  bool" (infix "L" 75)
where
  "φ L ψ  w. w n φ  w n ψ"

lemma ltl_lang_equiv_equivp:
  "equivp (∼L)"
  unfolding ltl_lang_equiv_def
  by (simp add: equivpI reflp_def symp_def transp_def)

lemma ltl_lang_equiv_and_true[simp]:
  "φ1 andn φ2 L truen  φ1 L truen  φ2 L truen"
  unfolding ltl_lang_equiv_def by auto

lemma ltl_lang_equiv_and_false[intro, simp]:
  "φ1 L falsen  φ1 andn φ2 L falsen"
  "φ2 L falsen  φ1 andn φ2 L falsen"
  unfolding ltl_lang_equiv_def by auto

lemma ltl_lang_equiv_or_false[simp]:
  "φ1 orn φ2 L falsen  φ1 L falsen  φ2 L falsen"
  unfolding ltl_lang_equiv_def by auto

lemma ltl_lang_equiv_or_const[intro, simp]:
  "φ1 L truen  φ1 orn φ2 L truen"
  "φ2 L truen  φ1 orn φ2 L truen"
  unfolding ltl_lang_equiv_def by auto


subsection ‹Propositional Equivalence›

fun ltl_prop_entailment :: "'a ltln set  'a ltln  bool" (infix "P" 80)
where
  "𝒜 P truen = True"
| "𝒜 P falsen = False"
| "𝒜 P φ andn ψ = (𝒜 P φ  𝒜 P ψ)"
| "𝒜 P φ orn ψ = (𝒜 P φ  𝒜 P ψ)"
| "𝒜 P φ = (φ  𝒜)"

lemma ltl_prop_entailment_monotonI[intro]:
  "S P φ  S  S'  S' P φ"
  by (induction φ) auto

lemma ltl_models_equiv_prop_entailment:
  "w n φ  {ψ. w n ψ} P φ"
  by (induction φ) auto

definition ltl_prop_equiv :: "'a ltln  'a ltln  bool" (infix "P" 75)
where
  "φ P ψ  𝒜. 𝒜 P φ  𝒜 P ψ"

definition ltl_prop_implies :: "'a ltln  'a ltln  bool" (infix "P" 75)
where
  "φ P ψ  𝒜. 𝒜 P φ  𝒜 P ψ"

lemma ltl_prop_implies_equiv:
  "φ P ψ  (φ P ψ  ψ P φ)"
  unfolding ltl_prop_equiv_def ltl_prop_implies_def by meson

lemma ltl_prop_equiv_equivp:
  "equivp (∼P)"
  by (simp add: ltl_prop_equiv_def equivpI reflp_def symp_def transp_def)

lemma ltl_prop_equiv_trans[trans]:
  "φ P ψ  ψ P χ  φ P χ"
  by (simp add: ltl_prop_equiv_def)

lemma ltl_prop_equiv_true:
  "φ P truen  {} P φ"
  using bot.extremum ltl_prop_entailment.simps(1) ltl_prop_equiv_def by blast

lemma ltl_prop_equiv_false:
  "φ P falsen  ¬ UNIV P φ"
  by (meson ltl_prop_entailment.simps(2) ltl_prop_entailment_monotonI ltl_prop_equiv_def top_greatest)

lemma ltl_prop_equiv_true_implies_true:
  "x P truen  x P y  y P truen"
  by (simp add: ltl_prop_equiv_def ltl_prop_implies_def)

lemma ltl_prop_equiv_false_implied_by_false:
  "y P falsen  x P y  x P falsen"
  by (simp add: ltl_prop_equiv_def ltl_prop_implies_def)

lemma ltl_prop_implication_implies_ltl_implication:
  "w n φ  φ P ψ  w n ψ"
  using ltl_models_equiv_prop_entailment ltl_prop_implies_def by blast

lemma ltl_prop_equiv_implies_ltl_lang_equiv:
  "φ P ψ  φ L ψ"
  using ltl_lang_equiv_def ltl_prop_implication_implies_ltl_implication ltl_prop_implies_equiv by blast

lemma ltl_prop_equiv_lt_ltl_lang_equiv[simp]:
  "(∼P)  (∼L)"
  using ltl_prop_equiv_implies_ltl_lang_equiv by blast


subsection ‹Constants Equivalence›

datatype tvl = Yes | No | Maybe

definition eval_and :: "tvl  tvl  tvl"
where
  "eval_and φ ψ =
    (case (φ, ψ) of
      (Yes, Yes)  Yes
    | (No, _)  No
    | (_, No)  No
    | _  Maybe)"

definition eval_or :: "tvl  tvl  tvl"
where
  "eval_or φ ψ =
    (case (φ, ψ) of
      (No, No)  No
    | (Yes, _)  Yes
    | (_, Yes)  Yes
    | _  Maybe)"

fun eval :: "'a ltln  tvl"
where
  "eval truen = Yes"
| "eval falsen = No"
| "eval (φ andn ψ) = eval_and (eval φ) (eval ψ)"
| "eval (φ orn ψ) = eval_or (eval φ) (eval ψ)"
| "eval φ = Maybe"

lemma eval_and_const[simp]:
  "eval_and φ ψ = No  φ = No  ψ = No"
  "eval_and φ ψ = Yes  φ = Yes  ψ = Yes"
  unfolding eval_and_def
  by (cases φ; cases ψ, auto)+

lemma eval_or_const[simp]:
  "eval_or φ ψ = Yes  φ = Yes  ψ = Yes"
  "eval_or φ ψ = No  φ = No  ψ = No"
  unfolding eval_or_def
  by (cases φ; cases ψ, auto)+

lemma eval_prop_entailment:
  "eval φ = Yes  {} P φ"
  "eval φ = No  ¬ UNIV P φ"
  by (induction φ) auto

definition ltl_const_equiv :: "'a ltln  'a ltln  bool" (infix "C" 75)
where
  "φ C ψ  φ = ψ  (eval φ = eval ψ  eval ψ  Maybe)"

lemma ltl_const_equiv_equivp:
  "equivp (∼C)"
  unfolding ltl_const_equiv_def
  by (intro equivpI reflpI sympI transpI) auto

lemma ltl_const_equiv_const:
  "φ C truen  eval φ = Yes"
  "φ C falsen  eval φ = No"
  unfolding ltl_const_equiv_def by force+

lemma ltl_const_equiv_and_const[simp]:
  "φ1 andn φ2 C truen  φ1 C truen  φ2 C truen"
  "φ1 andn φ2 C falsen  φ1 C falsen  φ2 C falsen"
  unfolding ltl_const_equiv_const by force+

lemma ltl_const_equiv_or_const[simp]:
  "φ1 orn φ2 C truen  φ1 C truen  φ2 C truen"
  "φ1 orn φ2 C falsen  φ1 C falsen  φ2 C falsen"
  unfolding ltl_const_equiv_const by force+

lemma ltl_const_equiv_other[simp]:
  "φ C propn(a)  φ = propn(a)"
  "φ C npropn(a)  φ = npropn(a)"
  "φ C Xn ψ  φ = Xn ψ"
  "φ C ψ1 Un ψ2  φ = ψ1 Un ψ2"
  "φ C ψ1 Rn ψ2  φ = ψ1 Rn ψ2"
  "φ C ψ1 Wn ψ2  φ = ψ1 Wn ψ2"
  "φ C ψ1 Mn ψ2  φ = ψ1 Mn ψ2"
  using ltl_const_equiv_def by fastforce+

lemma ltl_const_equiv_no_const_singleton:
  "eval ψ = Maybe  φ C ψ  φ = ψ"
  unfolding ltl_const_equiv_def by fastforce

lemma ltl_const_equiv_implies_prop_equiv:
  "φ C truen  φ P truen"
  "φ C falsen  φ P falsen"
  unfolding ltl_const_equiv_const eval_prop_entailment ltl_prop_equiv_def
  by auto

lemma ltl_const_equiv_no_const_prop_equiv:
  "eval ψ = Maybe  φ C ψ  φ P ψ"
  using ltl_const_equiv_no_const_singleton equivp_reflp[OF ltl_prop_equiv_equivp]
  by blast

lemma ltl_const_equiv_implies_ltl_prop_equiv:
  "φ C ψ  φ P ψ"
proof (induction ψ)
  case (And_ltln ψ1 ψ2)

  show ?case
  proof (cases "eval (ψ1 andn ψ2)")
    case Yes

    then have "φ C truen"
      by (meson And_ltln.prems equivp_transp ltl_const_equiv_const(1) ltl_const_equiv_equivp)
    then show ?thesis
      by (metis (full_types) Yes ltl_const_equiv_const(1) ltl_const_equiv_implies_prop_equiv(1) ltl_prop_equiv_trans ltl_prop_implies_equiv)
  next
    case No

    then have "φ C falsen"
      by (meson And_ltln.prems equivp_transp ltl_const_equiv_const(2) ltl_const_equiv_equivp)
    then show ?thesis
      by (metis (full_types) No ltl_const_equiv_const(2) ltl_const_equiv_implies_prop_equiv(2) ltl_prop_equiv_trans ltl_prop_implies_equiv)
  next
    case Maybe

    then show ?thesis
      using And_ltln.prems ltl_const_equiv_no_const_prop_equiv by force
  qed
next
  case (Or_ltln ψ1 ψ2)

  then show ?case
  proof (cases "eval (ψ1 orn ψ2)")
    case Yes

    then have "φ C truen"
      by (meson Or_ltln.prems equivp_transp ltl_const_equiv_const(1) ltl_const_equiv_equivp)
    then show ?thesis
      by (metis (full_types) Yes ltl_const_equiv_const(1) ltl_const_equiv_implies_prop_equiv(1) ltl_prop_equiv_trans ltl_prop_implies_equiv)
  next
    case No

    then have "φ C falsen"
      by (meson Or_ltln.prems equivp_transp ltl_const_equiv_const(2) ltl_const_equiv_equivp)
    then show ?thesis
      by (metis (full_types) No ltl_const_equiv_const(2) ltl_const_equiv_implies_prop_equiv(2) ltl_prop_equiv_trans ltl_prop_implies_equiv)
  next
    case Maybe

    then show ?thesis
      using Or_ltln.prems ltl_const_equiv_no_const_prop_equiv by force
  qed
qed (simp_all add: ltl_const_equiv_implies_prop_equiv equivp_reflp[OF ltl_prop_equiv_equivp])

lemma ltl_const_equiv_lt_ltl_prop_equiv[simp]:
  "(∼C)  (∼P)"
  using ltl_const_equiv_implies_ltl_prop_equiv by blast


subsection ‹Quotient types›

quotient_type 'a ltlnL = "'a ltln" / "(∼L)"
  by (rule ltl_lang_equiv_equivp)

instantiation ltlnL :: (type) equal
begin

lift_definition ltlnL_eq_test :: "'a ltlnL  'a ltlnL  bool" is "λx y. x L y"
  by (metis ltlnL.abs_eq_iff)

definition
  eqL: "equal_class.equal  ltlnL_eq_test"

instance
  by (standard; simp add: eqL ltlnL_eq_test.rep_eq, metis Quotient_ltlnL Quotient_rel_rep)

end


quotient_type 'a ltlnP = "'a ltln" / "(∼P)"
  by (rule ltl_prop_equiv_equivp)

instantiation ltlnP :: (type) equal
begin

lift_definition ltlnP_eq_test :: "'a ltlnP  'a ltlnP  bool" is "λx y. x P y"
  by (metis ltlnP.abs_eq_iff)

definition
  eqP: "equal_class.equal  ltlnP_eq_test"

instance
  by (standard; simp add: eqP ltlnP_eq_test.rep_eq, metis Quotient_ltlnP Quotient_rel_rep)

end


quotient_type 'a ltlnC = "'a ltln" / "(∼C)"
  by (rule ltl_const_equiv_equivp)

instantiation ltlnC :: (type) equal
begin

lift_definition ltlnC_eq_test :: "'a ltlnC  'a ltlnC  bool" is "λx y. x C y"
  by (metis ltlnC.abs_eq_iff)

definition
  eqC: "equal_class.equal  ltlnC_eq_test"

instance
  by (standard; simp add: eqC ltlnC_eq_test.rep_eq, metis Quotient_ltlnC Quotient_rel_rep)

end



subsection ‹Cardinality of propositional quotient sets›

definition sat_models :: "'a ltlnP  'a ltln set set"
where
  "sat_models φ = {𝒜. 𝒜 P rep_ltlnP φ}"

lemma Rep_Abs_prop_entailment[simp]:
  "𝒜 P rep_ltlnP (abs_ltlnP φ) = 𝒜 P φ"
  by (metis Quotient3_ltlnP Quotient3_rep_abs ltl_prop_equiv_def)

lemma sat_models_Abs:
  "𝒜  sat_models (abs_ltlnP φ) = 𝒜 P φ"
  by (simp add: sat_models_def)

lemma sat_models_inj:
  "inj sat_models"
proof (rule injI)
  fix φ ψ :: "'a ltlnP"
  assume "sat_models φ = sat_models ψ"

  then have "rep_ltlnP φ P rep_ltlnP ψ"
    unfolding sat_models_def ltl_prop_equiv_def by force

  then show "φ = ψ"
    by (meson Quotient3_ltlnP Quotient3_rel_rep)
qed


fun prop_atoms :: "'a ltln  'a ltln set"
where
  "prop_atoms truen = {}"
| "prop_atoms falsen = {}"
| "prop_atoms (φ andn ψ) = prop_atoms φ  prop_atoms ψ"
| "prop_atoms (φ orn ψ) = prop_atoms φ  prop_atoms ψ"
| "prop_atoms φ = {φ}"

fun nested_prop_atoms :: "'a ltln  'a ltln set"
where
  "nested_prop_atoms truen = {}"
| "nested_prop_atoms falsen = {}"
| "nested_prop_atoms (φ andn ψ) = nested_prop_atoms φ  nested_prop_atoms ψ"
| "nested_prop_atoms (φ orn ψ) = nested_prop_atoms φ  nested_prop_atoms ψ"
| "nested_prop_atoms (Xn φ) = {Xn φ}  nested_prop_atoms φ"
| "nested_prop_atoms (φ Un ψ) = {φ Un ψ}  nested_prop_atoms φ  nested_prop_atoms ψ"
| "nested_prop_atoms (φ Rn ψ) = {φ Rn ψ}  nested_prop_atoms φ  nested_prop_atoms ψ"
| "nested_prop_atoms (φ Wn ψ) = {φ Wn ψ}  nested_prop_atoms φ  nested_prop_atoms ψ"
| "nested_prop_atoms (φ Mn ψ) = {φ Mn ψ}  nested_prop_atoms φ  nested_prop_atoms ψ"
| "nested_prop_atoms φ = {φ}"

lemma prop_atoms_nested_prop_atoms:
  "prop_atoms φ  nested_prop_atoms φ"
  by (induction φ) auto

lemma prop_atoms_subfrmlsn:
  "prop_atoms φ  subfrmlsn φ"
  by (induction φ) auto

lemma nested_prop_atoms_subfrmlsn:
  "nested_prop_atoms φ  subfrmlsn φ"
  by (induction φ) auto

lemma prop_atoms_notin[simp]:
  "truen  prop_atoms φ"
  "falsen  prop_atoms φ"
  "φ1 andn φ2  prop_atoms φ"
  "φ1 orn φ2  prop_atoms φ"
  by (induction φ) auto

lemma nested_prop_atoms_notin[simp]:
  "truen  nested_prop_atoms φ"
  "falsen  nested_prop_atoms φ"
  "φ1 andn φ2  nested_prop_atoms φ"
  "φ1 orn φ2  nested_prop_atoms φ"
  by (induction φ) auto

lemma prop_atoms_finite:
  "finite (prop_atoms φ)"
  by (induction φ) auto

lemma nested_prop_atoms_finite:
  "finite (nested_prop_atoms φ)"
  by (induction φ) auto

lemma prop_atoms_entailment_iff:
  "φ  prop_atoms ψ  𝒜 P φ  φ  𝒜"
  by (induction φ) auto

lemma prop_atoms_entailment_inter:
  "prop_atoms φ  P  (𝒜  P) P φ = 𝒜 P φ"
  by (induction φ) auto

lemma nested_prop_atoms_entailment_inter:
  "nested_prop_atoms φ  P  (𝒜  P) P φ = 𝒜 P φ"
  by (induction φ) auto

lemma sat_models_inter_inj_helper:
  assumes
    "prop_atoms φ  P"
  and
    "prop_atoms ψ  P"
  and
    "sat_models (abs_ltlnP φ)  Pow P = sat_models (abs_ltlnP ψ)  Pow P"
  shows
    "φ P ψ"
proof -
  from assms have "𝒜. (𝒜  P) P φ  (𝒜  P) P ψ"
    by (auto simp: sat_models_Abs)

  with assms show "φ P ψ"
    by (simp add: prop_atoms_entailment_inter ltl_prop_equiv_def)
qed

lemma sat_models_inter_inj:
  "inj_on (λφ. sat_models φ  Pow P) {abs_ltlnP φ |φ. prop_atoms φ  P}"
  by (auto simp: inj_on_def sat_models_inter_inj_helper ltlnP.abs_eq_iff)

lemma sat_models_pow_pow:
  "{sat_models (abs_ltlnP φ)  Pow P | φ. prop_atoms φ  P}  Pow (Pow P)"
  by (auto simp: sat_models_def)

lemma sat_models_finite:
  "finite P  finite {sat_models (abs_ltlnP φ)  Pow P | φ. prop_atoms φ  P}"
  using sat_models_pow_pow finite_subset by fastforce

lemma sat_models_card:
  "finite P  card ({sat_models (abs_ltlnP φ)  Pow P | φ. prop_atoms φ  P})  2 ^ 2 ^ card P"
  by (metis (mono_tags, lifting) sat_models_pow_pow Pow_def card_Pow card_mono finite_Collect_subsets)


lemma image_filter:
  "f ` {g a | a. P a} = {f (g a) | a. P a}"
  by blast

lemma prop_equiv_finite:
  "finite P  finite {abs_ltlnP ψ | ψ. prop_atoms ψ  P}"
  by (auto simp: image_filter sat_models_finite finite_imageD[OF _ sat_models_inter_inj])

lemma prop_equiv_card:
  "finite P  card {abs_ltlnP ψ | ψ. prop_atoms ψ  P}  2 ^ 2 ^ card P"
  by (auto simp: image_filter sat_models_card card_image[OF sat_models_inter_inj, symmetric])


lemma prop_equiv_subset:
  "{abs_ltlnP ψ |ψ. nested_prop_atoms ψ  P}  {abs_ltlnP ψ |ψ. prop_atoms ψ  P}"
  using prop_atoms_nested_prop_atoms by blast

lemma prop_equiv_finite':
  "finite P  finite {abs_ltlnP ψ | ψ. nested_prop_atoms ψ  P}"
  using prop_equiv_finite prop_equiv_subset finite_subset by fast

lemma prop_equiv_card':
  "finite P  card {abs_ltlnP ψ | ψ. nested_prop_atoms ψ  P}  2 ^ 2 ^ card P"
  by (metis (mono_tags, lifting) prop_equiv_card prop_equiv_subset prop_equiv_finite card_mono le_trans)



subsection ‹Substitution›

fun subst :: "'a ltln  ('a ltln  'a ltln)  'a ltln"
where
  "subst truen m = truen"
| "subst falsen m = falsen"
| "subst (φ andn ψ) m = subst φ m andn subst ψ m"
| "subst (φ orn ψ) m = subst φ m orn subst ψ m"
| "subst φ m = (case m φ of Some ψ  ψ | None  φ)"

text ‹Based on Uwe Schoening's Translation Lemma (Logic for CS, p. 54)›

lemma ltl_prop_equiv_subst_S:
  "S P subst φ m = ((S - dom m)  {χ | χ χ'. χ  dom m  m χ = Some χ'  S P χ'}) P φ"
  by (induction φ) (auto split: option.split)

lemma subst_respects_ltl_prop_entailment:
  "φ P ψ  subst φ m P subst ψ m"
  "φ P ψ  subst φ m P subst ψ m"
  unfolding ltl_prop_equiv_def ltl_prop_implies_def ltl_prop_equiv_subst_S by blast+


lemma eval_subst:
  "eval φ = Yes  eval (subst φ m) = Yes"
  "eval φ = No  eval (subst φ m) = No"
  by (meson empty_subsetI eval_prop_entailment ltl_prop_entailment_monotonI ltl_prop_equiv_subst_S subset_UNIV)+

lemma subst_respects_ltl_const_entailment:
  "φ C ψ  subst φ m C subst ψ m"
  unfolding ltl_const_equiv_def
  by (cases "eval ψ") (metis eval_subst(1), metis eval_subst(2), blast)



subsection ‹Order of Equivalence Relations›

locale ltl_equivalence =
  fixes
    eq :: "'a ltln  'a ltln  bool" (infix "" 75)
  assumes
    eq_equivp: "equivp (∼)"
  and
    ge_const_equiv: "(∼C)  (∼)"
  and
    le_lang_equiv: "(∼)  (∼L)"
begin

lemma eq_implies_ltl_equiv:
  "φ  ψ  w n φ = w n ψ"
  using le_lang_equiv ltl_lang_equiv_def by blast

lemma const_implies_eq:
  "φ C ψ  φ  ψ"
  using ge_const_equiv by blast

lemma eq_implies_lang:
  "φ  ψ  φ L ψ"
  using le_lang_equiv by blast

lemma eq_refl[simp]:
  "φ  φ"
  by (meson eq_equivp equivp_reflp)

lemma eq_sym[sym]:
  "φ  ψ  ψ  φ"
  by (meson eq_equivp equivp_symp)

lemma eq_trans[trans]:
  "φ  ψ  ψ  χ  φ  χ"
  by (meson eq_equivp equivp_transp)

end

interpretation ltl_lang_equivalence: ltl_equivalence "(∼L)"
  using ltl_lang_equiv_equivp ltl_const_equiv_lt_ltl_prop_equiv ltl_prop_equiv_lt_ltl_lang_equiv
  by unfold_locales blast+

interpretation ltl_prop_equivalence: ltl_equivalence "(∼P)"
  using ltl_prop_equiv_equivp ltl_const_equiv_lt_ltl_prop_equiv ltl_prop_equiv_lt_ltl_lang_equiv
  by unfold_locales blast+

interpretation ltl_const_equivalence: ltl_equivalence "(∼C)"
  using ltl_const_equiv_equivp ltl_const_equiv_lt_ltl_prop_equiv ltl_prop_equiv_lt_ltl_lang_equiv
  by unfold_locales blast+

end