Theory Priced_HML

theory Priced_HML
imports
  Hennessy_Milner_Logic
  "HOL-Library.Extended_Nat"
begin

datatype distinction_price =
  Price
    (obs_depth: ‹enat›)
    (conj_depth: ‹enat›)
    (pos_cl_height: ‹enat›)
    (pos_cl_height_2: ‹enat›)
    (neg_cl_height: ‹enat›)
    (neg_depth: ‹enat›)

lemma unfold_distinction_price:
 ‹dp = Price (obs_depth dp) (conj_depth dp) (pos_cl_height dp) (pos_cl_height_2 dp) (neg_cl_height dp) (neg_depth dp)›
  using distinction_price.collapse ..

instantiation distinction_price :: order
begin

fun less_eq_distinction_price :: ‹distinction_price ⇒ distinction_price ⇒ bool›
  where ‹less_eq_distinction_price (Price obs conjs posh posh2 negh negs) (Price obs' conjs' posh' posh2' negh' negs') =
    (obs ≤ obs' ∧ conjs ≤ conjs' ∧ posh ≤ posh' ∧ posh2 ≤ posh2' ∧ negh ≤ negh' ∧ negs ≤ negs')›

definition less_distinction_price :: ‹distinction_price ⇒ distinction_price ⇒ bool› where
  ‹less_distinction_price pr pr' ≡
    (pr ≤ pr' ∧ ¬(pr' ≤ pr))›

instance
proof
  fix pr pr':: distinction_price
  show ‹(pr < pr') = (pr ≤ pr' ∧ ¬ pr' ≤ pr)›
    unfolding less_distinction_price_def by blast
next
  fix pr:: distinction_price
  show ‹pr ≤ pr›
    by (induct pr, auto)
next
  fix pr1 pr2 pr3:: distinction_price
  assume ‹pr1 ≤ pr2› ‹pr2 ≤ pr3›
  thus ‹pr1 ≤ pr3›
    using unfold_distinction_price
    by (smt (verit, best) dual_order.trans less_eq_distinction_price.simps)
next
  fix pr1 pr2:: distinction_price
  assume ‹pr1 ≤ pr2› ‹pr2 ≤ pr1›
  thus ‹pr1 = pr2›
    using less_eq_distinction_price.elims(2) by fastforce
qed
end

lemma less_eq_distinction_price_def:
  ‹(p1 ≤ p2) = (obs_depth p1 ≤ obs_depth p2 ∧ conj_depth p1 ≤ conj_depth p2 ∧ pos_cl_height p1 ≤ pos_cl_height p2 ∧ pos_cl_height_2 p1 ≤ pos_cl_height_2 p2 ∧ neg_cl_height p1 ≤ neg_cl_height p2 ∧ neg_depth p1 ≤ neg_depth p2)›
  by (induct p1, induct p2, auto)

primrec price_dec_obs where
  ‹price_dec_obs (Price obs conjs posh posh2 negh negs) = (Price (obs-1) conjs posh posh2 negh negs)›
primrec price_cap_obs where
  ‹price_cap_obs cap (Price obs conjs posh posh2 negh negs) = (Price (min obs cap) conjs posh posh2 negh negs)›
primrec price_cap_posh where
  ‹price_cap_posh cap (Price obs conjs posh posh2 negh negs) = (Price obs conjs (min posh cap) posh2 negh negs)›
primrec price_dec_conjs where
  ‹price_dec_conjs (Price obs conjs posh posh2 negh negs) = (Price obs (conjs-1) posh posh2 negh negs)›
primrec price_dec_negs where
  ‹price_dec_negs (Price obs conjs posh posh2 negh negs) = (Price obs conjs posh posh2 negh (negs - 1))›

primrec formula_of_price :: ‹distinction_price ⇒ ('a,'i) hml_formula ⇒ bool›
  and conjunct_of_price :: ‹distinction_price ⇒ ('a,'i) hml_conjunct ⇒ bool›
  where
  ‹formula_of_price pr HML_true = True›
| ‹formula_of_price pr (⟨α⟩φ)  =
  (if obs_depth pr > 0 then formula_of_price (price_dec_obs pr) φ else False)›
| ‹formula_of_price pr (HML_conj I F) =
  (if conj_depth pr > 0 then
    (∃i∈I.
      conjunct_of_price (price_dec_conjs pr) (F i)
      ∧ (∀j∈(I-{i}). conjunct_of_price (price_cap_posh (pos_cl_height_2 pr) (price_dec_conjs pr)) (F j)))
  else False)›
| ‹conjunct_of_price pr (HML_pos φ) =
  (case φ of (⟨α⟩φ') ⇒ formula_of_price (price_cap_obs (pos_cl_height pr) pr) φ
  | _ ⇒ False)›
| ‹conjunct_of_price pr (HML_neg φ) =
  (case φ of (⟨α⟩φ') ⇒
    if neg_depth pr > 0 then
      formula_of_price (price_dec_negs (price_cap_obs (neg_cl_height pr) pr)) φ else False
  | _ ⇒ False)›

thm hml_formula_hml_conjunct.induct

lemma ediff1_le_mono:
  assumes ‹n ≤ (m::enat)›
  shows ‹n - 1 ≤ m - 1›
  using assms
  by (induct n, induct m, auto simp add: one_enat_def)

lemma emin_le_mono:
  assumes ‹n ≤ (m::enat)›
  shows ‹min a n ≤ min a m›
  using assms
  by (induct n, induct m, auto simp add: min.coboundedI2)

lemma conjuncts_require_observations:
  assumes ‹conjunct_of_price pr ψ› ‹obs_depth pr = 0›
  shows ‹False›
proof (cases ψ)
  case (HML_pos φ)
  then obtain α φ' where ‹φ = ⟨α⟩φ'› using assms(1)
    by (metis conjunct_of_price.simps(1) hml_formula.exhaust hml_formula.simps(10)
        hml_formula.simps(9))
  then show ?thesis using assms HML_pos
    by (metis conjunct_of_price.simps(1) distinction_price.collapse formula_of_price.simps(2)
        hml_formula.simps(11) less_numeral_extra(3) min_enat_simps(3) price_cap_obs.simps)
next
  case (HML_neg φ)
  then obtain α φ' where ‹φ = ⟨α⟩φ'› using assms(1)
    by (metis conjunct_of_price.simps(2) hml_formula.exhaust hml_formula.simps(10)
        hml_formula.simps(9))
  then show ?thesis using assms HML_neg
    by (metis conjunct_of_price.simps(2) distinction_price.collapse distinction_price.sel(1)
        formula_of_price.simps(2) hml_formula.simps(11) le_zero_eq linorder_neq_iff min.cobounded1
        price_cap_obs.simps price_dec_negs.simps)
qed

lemma only_true_for_free:
  assumes ‹formula_of_price pr φ› ‹obs_depth pr = 0›
  shows ‹φ = HML_true›
  using assms
  by (induct pr; induct φ; auto;
      metis conjuncts_require_observations distinction_price.sel(1) price_dec_conjs.simps)

lemma deeper_conjuncts_require_observations:
  assumes ‹conjunct_of_price pr ψ› ‹obs_depth pr = 1›
  shows ‹∃α. ψ = (+⟨α⟩ HML_true) ∨ ψ = (-⟨α⟩ HML_true)›
proof (cases ψ)
  case (HML_pos φ)
  then obtain α φ' where
    ‹φ = ⟨α⟩φ'› ‹formula_of_price (price_dec_obs (price_cap_obs (pos_cl_height pr) pr)) φ'›
    using assms(1)
    by (metis conjunct_of_price.simps(1) formula_of_price.simps(2) hml_formula.exhaust
        hml_formula.simps(10) hml_formula.simps(11) hml_formula.simps(9))
  hence ‹φ' = HML_true›
    using only_true_for_free ‹obs_depth pr = 1›
    by (metis add_diff_cancel_enat distinction_price.exhaust_sel distinction_price.sel(1)
        ediff1_le_mono i1_ne_infinity le_zero_eq min.cobounded1 one_eSuc plus_1_eSuc(1)
        price_cap_obs.simps price_dec_obs.simps)
  then show ?thesis using ‹φ = ⟨α⟩φ'› HML_pos by blast
next
  case (HML_neg φ)
  then obtain α φ' where
    ‹φ = ⟨α⟩φ'› ‹formula_of_price (price_dec_obs (price_dec_negs (price_cap_obs (neg_cl_height pr) pr))) φ'›
    using assms(1)
    by (metis conjunct_of_price.simps(2) formula_of_price.simps(2) hml_formula.exhaust
        hml_formula.simps(10) hml_formula.simps(11) hml_formula.simps(9))
  hence ‹φ' = HML_true›
    using only_true_for_free ‹obs_depth pr = 1›
    by (metis (no_types, lifting) HML_neg assms(1) conjunct_of_price.simps(2)
        distinction_price.exhaust_sel distinction_price.sel(1) eSuc_minus_1 hml_formula.distinct(3)
        hml_formula.simps(11) iless_eSuc0 min.cobounded1 one_eSuc order_le_less price_cap_obs.simps
        price_dec_negs.simps price_dec_obs.simps)
  then show ?thesis using ‹φ = ⟨α⟩φ'› HML_neg by blast
qed

lemma neg_conjuncts_require_negations:
  assumes ‹conjunct_of_price pr (HML_neg φ)› ‹neg_depth pr = 0›
  shows ‹False›
  using assms
  by (auto, metis hml_formula.exhaust hml_formula.simps(10) hml_formula.simps(11) hml_formula.simps(9) less_numeral_extra(3))

lemma price_closure:
  assumes
    ‹p01 ≤ p02›
    ‹formula_of_price p01 φ0›
  shows
    ‹formula_of_price p02 φ0›
proof -
  {
    fix φ :: ‹('a, 'i) hml_formula› and ψ :: ‹('a, 'i) hml_conjunct›
    have
      ‹⋀p1 p2. p1 ≤ p2 ⟹ formula_of_price p1 φ ⟹ formula_of_price p2 φ›
      ‹⋀p1 p2. p1 ≤ p2 ⟹ conjunct_of_price p1 ψ ⟹ conjunct_of_price p2 ψ›
    proof (induct φ and ψ)
      case HML_true
      then show ?case by simp
    next
      case (HML_conj I Ψ)
      from this(3) have ‹∀i∈I. ∃p0 ≤ p1. conjunct_of_price p0 (Ψ i)› apply (cases p1) apply auto sorry
      hence ‹∀i∈I. conjunct_of_price p2 (Ψ i)› using HML_conj by auto
      then show ?case
        using HML_conj.prems less_eq_distinction_price.elims(2) apply (induct p2) apply auto defer 
        apply fastforce
        sorry
    next
      case (HML_obs α φ)
      hence ‹formula_of_price (price_dec_obs p1) φ› by (simp, argo)
      moreover have ‹price_dec_obs p1 ≤ price_dec_obs p2›
        using HML_obs(2) ediff1_le_mono by (cases p1, cases p2, auto)
      ultimately have ‹formula_of_price (price_dec_obs p2) φ› using HML_obs by blast
      then show ?case
        using HML_obs.prems less_eq_distinction_price_def by force
    next
      case (HML_pos φ)
      then show ?case sorry
    next
      case (HML_neg φ)
      then show ?case sorry
    qed
  }
  thus ?thesis using assms by auto
qed

end