Theory Priced_Spectrum

section ‹Priced Spectrum›

theory Priced_Spectrum
imports
  Priced_HML
  HML_Spectrum
  (* "HOL-ex.Sketch_and_Explore" *)
begin

(* declare [[atp_proof_cartouches]] *)

context lts
begin

interpretation hml: lts_semantics where satisfies = satisfies
  by unfold_locales
interpretation hml_conj: lts_semantics where satisfies = satisfies_conj
  by unfold_locales

abbreviation ‹price_preordered pr ≡ hml.preordered (Collect (formula_of_price pr))›

subsection ‹Enabledness›

text ‹A minimal and a way bigger coordinate to characterize enabledness preorder.
   (One could still increase either one of the last two dimensions, but would arrive at the same language.)›
lemma enabledness_conjunctions_are_neutral: 
  ‹hml.eq_distinctive
    (Collect (formula_of_price (Price 1 0 0 0 0 0)))
    (Collect (formula_of_price (Price 1 ∞ ∞ ∞ 0 0)))›
  unfolding hml.leq_distinctive_def
proof safe
  fix p q φ
  assume case_assms:
    ‹formula_of_price (Price 1 0 0 0 0 0) φ›
    ‹p ⊨ φ› ‹¬ q ⊨ φ›
  hence ‹φ ∈ Collect (formula_of_price (Price 1 ∞ ∞ ∞ 0 0))›
    using price_closure
    by (metis (no_types, opaque_lifting) enat_ord_simps(3) less_eq_distinction_price.simps mem_Collect_eq order_refl)
  thus ‹∃φ' ∈Collect (formula_of_price (Price 1 ∞ ∞ ∞ 0 0)). hml.distinguishes φ' p q›
    using case_assms by blast
next
  fix p q φ
  assume case_assms:
    ‹formula_of_price (Price 1 ∞ ∞ ∞ 0 0) φ›
    ‹p ⊨ φ› ‹¬ q ⊨ φ›
  show ‹∃φ'∈Collect (formula_of_price (Price 1 0 0 0 0 0)). hml.distinguishes φ' p q›
  proof (cases φ)
    case HML_true
    then show ?thesis using case_assms by auto
  next
    case (HML_conj I Ψ)
    hence ‹∀i ∈ I. ∃ α. Ψ i = +⟨α⟩HML_true›
      using case_assms(1)
      by (simp, metis deeper_conjuncts_require_observations neg_conjuncts_require_negations
          distinction_price.sel(1) distinction_price.sel(6) member_remove remove_def)
    hence ‹∀i ∈ I. ∃ α. (Ψ i) = (+⟨α⟩HML_true) ∧
        formula_of_price (Price 1 0 0 0 0 0) (⟨α⟩HML_true)›
      by auto
    then show ?thesis using case_assms HML_conj
      by (metis mem_Collect_eq satisfies.simps(2) satisfies_conj.simps(1))
  next
    case (HML_obs α φ')
    hence ‹formula_of_price (Price 0 ∞ ∞ ∞ 0 0) φ'› using case_assms(1) by simp
    hence ‹φ' = HML_true› using only_true_for_free
      using distinction_price.sel(1) by blast
    hence ‹formula_of_price (Price 0 0 0 0 0 0) φ'› by simp
    hence ‹formula_of_price (Price 1 0 0 0 0 0) (⟨α⟩φ')› by simp
    then show ?thesis using case_assms(2,3) HML_obs by blast
  qed
qed

subsection ‹Traces›

lemma trace_observations_respect_prices:
  assumes
    ‹observations_traces φ›
  shows
    ‹formula_of_price (Price ∞ 0 0 0 0 0) φ›
  using assms by (induct, auto)

lemma trace_prices_imply_observations:
  assumes
    ‹formula_of_price (Price ∞ 0 0 0 0 0) φ›
  shows
    ‹observations_traces φ›
  using assms by (induct φ, auto simp add: observations_traces.intros)

theorem traces_priced_characterization:
    ‹(≲T) = price_preordered (Price ∞ 0 0 0 0 0)›
  using trace_observations_respect_prices trace_prices_imply_observations
  unfolding observations_traces_characterizes_trace_preorder by blast

subsection ‹Simulation›

lemma simulation_prices_imply_observations:
fixes
  φ :: ‹('a, 's) hml_formula› and
  ψ :: ‹('a, 's) hml_conjunct›
shows
  ‹formula_of_price (Price ∞ ∞ ∞ ∞ 0 0) φ ⟹ observations_simulation φ›
  ‹conjunct_of_price (Price ∞ ∞ ∞ ∞ 0 0) ψ ⟹ observations_simulation_conj ψ›
proof (induct φ and ψ)
  case HML_true
  then show ?case using observations_simulation_observations_simulation_conj.intros by simp
next
  case (HML_conj I Ψ)
  hence ‹I ≠ {}›
    using observations_simulation.cases by auto
  then show ?case using HML_conj
    apply (auto)
    by (metis Diff_iff ‹I ≠ {}› observations_simulation.simps range_eqI singletonD)
next
  case (HML_obs α φ)
  then show ?case
    using observations_simulation_observations_simulation_conj.intros by auto
next
  case (HML_pos φ)
  show ?case
  proof (cases φ)
    case HML_true
    then show ?thesis using HML_pos
      by simp
  next
    case (HML_conj I' Ψ')
    then show ?thesis using HML_pos
      by simp
  next
    case (HML_obs α φ')
    then show ?thesis using HML_pos observations_simulation_conj.simps
      by (metis conjunct_of_price.simps(1) distinction_price.sel(3) hml_formula.distinct(3,5)
        hml_formula.simps(11) observations_simulation.simps min_enat_simps(5)
        price_cap_obs.simps)
  qed
next
  case (HML_neg φ)
  from this(2) have False by (cases φ, auto)
  thus ?case ..
qed

lemma simulation_observations_respect_prices:
fixes
  φ :: ‹('a, 's) hml_formula› and
  ψ :: ‹('a, 's) hml_conjunct›
shows
  ‹observations_simulation φ ⟹ formula_of_price (Price ∞ ∞ ∞ ∞ 0 0) φ›
  ‹observations_simulation_conj ψ ⟹ conjunct_of_price (Price ∞ ∞ ∞ ∞ 0 0) ψ›
proof (induct φ and ψ)
  case HML_true
  then show ?case by simp
next
  case (HML_conj I Ψ)
  hence ‹I ≠ {}›
    using observations_simulation.cases by auto
  then show ?case using HML_conj
    apply (auto)
    by (metis DiffD1 hml_formula.distinct(1,5) hml_formula.inject(1) observations_simulation.simps range_eqI)
next
  case (HML_obs α φ)
  then show ?case
    using lts.observations_simulation.cases by auto
next
  case (HML_pos φ)
  then obtain α φ' where α_φ': ‹φ = (⟨α⟩φ') ∧ observations_simulation φ'›
    using lts.observations_simulation_conj.simps
    by (metis hml_conjunct.inject(1))
  hence ‹conjunct_of_price (Price ∞ ∞ ∞ ∞ 0 0) (+(⟨α⟩φ'))›
    using HML_pos.hyps lts.observations_simulation.simps by auto
  thus ?case using α_φ' by blast
next
  case (HML_neg φ)
  from this(2) have False
    using observations_simulation_conj.simps by blast
  thus ?case ..
qed

theorem simulation_priced_characterization:
    ‹(≲S) = price_preordered (Price ∞ ∞ ∞ ∞ 0 0)›
  using simulation_observations_respect_prices simulation_prices_imply_observations
  unfolding observations_simulation_characterize_simulation_preorder by blast

end

end